Evaluation
The evaluation of a path S :: He R proceeds as follows. The source
S is evaluated, and, if the evaluation succeeds, the ground expression
obtained is matched against He. The variables from He are
bound to new values, and the environments is extended with the new bindings. Then the tail
R is evaluated in the new environment.
The source S is considered to be at the zero level.
If the rest R is an empty delimited path (which always returns an empty
ground expression), it may be omitted.
S :: He =>=> S :: He ,
Env,0,St |- S => Ge,St'
Env |- Ge :: He => Env'
Env',m,St' |- R => X,St''
-------------------------------
Env,m,St |- S :: He R => X,St''
Env,0,St |- S => $fail(k),St'
-------------------------------------
Env,m,St |- S :: He R => $fail(0),St'
Env,0,St |- S => $error(Ge),St'
---------------------------------------
Env,m,St |- S :: He R => $error(Ge),St'