Fences

Syntax

Fence =
     "\?" Path.

Evaluation

The evaluation of a rest \? Q proceeds as follows. The path Q is evaluated. If the result obtained is a failure $fail(k), where k>0, then the "weakened" failure $fail(k-1) is taken to be the result of the whole construct. Otherwise, the result of evaluating Q is taken to be the result of the whole construct.

The path Q is evaluated at the level m+1, where m is the level at which the whole construct is evaluated.

     Env,m+1,St |- Q => Ge,St'
     --------------------------
     Env,m,St |- \? Q => Ge,St'


     Env,m+1,St |- Q => $fail(0),St'
     --------------------------------
     Env,m,St |- \? Q => $fail(0),St'


     Env,m+1,St |- Q => $fail(k+1),St'
     ---------------------------------
     Env,m,St |- \? Q => $fail(k),St'


     Env,m+1,St |- Q => $error(Ge),St'
     ----------------------------------
     Env,m,St |- \? Q => $error(Ge),St'