Bindings

Syntax

Binding =
     Source "::" HardExpression [ Rest ].

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'

Examples

The evaluation of the path
     100 :: sN, <Add sN 1> :: sN = sN
produces the number 101.
Related concepts
Sources
Hard Expressions
Rests