Evaluation
The evaluation of a rest
$trap Q $with Palt
proceeds as follows. An attempt is made to evaluate the path Q. If the
result obtained is an error $error(Ge), then the alternative match
Ge : Palt
is evaluated, and the result obtained is taken to be
the result of the whole construct.
The path Q is evaluated at the level 0.
Env,0,St |- Q => Ge,St'
----------------------------------------
Env,m,St |- $trap Q $with Palt => Ge,St'
Env,0,St |- Q => $fail(k),St'
Env,m,St' |- Fname "Unexpected fail" : Palt => X,St''
-----------------------------------------------------
Env,m,St |- $trap Q $with Palt => X,St''
Fname is the name of the function in which
the construct appears.
Env,0,St |- Q => $error(Ge),St'
Env,m,St' |- Ge : Palt => X,St''
----------------------------------------
Env,m,St |- $trap Q $with Palt => X,St''