Evaluation
The evaluation of a path S : P R proceeds as follows. The source
S is evaluated and a ground expression Ge obtained is
matched against the pattern P to produce a sequence of the variants of
matching. Then an attempt is made to find the first variant of matching appearing in this
sequence such that the evaluation of the rest R succeeds.
If the rest R is an empty delimited path (which always returns an empty
ground expression), it may be omitted.
To describe the semantics of matches, we need the following notation. A judgment
EnvList,m,St ||- Q => X,St' means that the evaluation of the path
Q at the level m with the list of environments
EnvList returns X.
Env,m,St |- Q => Ge,St'
----------------------------------
[Env]^EnvList,m,St ||- Q => Ge,St'
Env,m,St |- Q => $fail(0),St'
EnvList,m,St' ||- Q => X,St''
----------------------------------
[Env]^EnvList,m,St ||- Q => X,St''
Env,m,St |- Q => $fail(k+1),St'
------------------------------------------
[Env]^EnvList,m,St ||- Q => $fail(k+1),St'
Env,m,St |- Q => $error(Ge),St'
------------------------------------------
[Env]^EnvList,m,St ||- Q => $error(Ge),St'
[],m,St ||- Q => $fail(0),St.
Now we describe the semantics of matches.
S : P =>=> S : P ,
Env,0,St |- S => Ge,St'
Env |- Ge : P => EnvList
EnvList,m,St' ||- R => X,St''
-----------------------------
Env,m,St |- S : P R => X,St''
Env,0,St |- S => $fail(k),St'
-----------------------------------
Env,m,St |- S : P R => $fail(0),St'
Env,0,St |- S => $error(Ge),St'
-------------------------------------
Env,m,St |- S : P R => $error(Ge),St'