Syntax
Path =
Condition | Binding | Search | Match |
Rest | Source.
The syntax of paths seems to be rather complicated. This is due to the desire to save the
user the trouble of writing redundant delimiters without real necessity.
This is achieved by distinguishing two particular cases of paths: "rests" and "sources",
which possess some useful syntax properties. Rests begin with key words, which are easy to
recognize. Thus, if a result expression or a pattern is followed by a rest, there is no
danger that they could "stick" together. Sources cannot contain commas at the top level of
curly brackets, for which reason they can be unambiguously separated from the constructs
they are followed by.
Evaluation
A path Q is evaluated with respect to an environment Env
and a non-negative integer m. The environment Env
associates variables with their values, which may be necessary to evaluate the path. The
integer m, which is referred to as the level of the path, specifies
the number of fences \? that surrounds Q without being
closed by cuts \!.
If the evaluation of Q terminates, it returns either a ground expression
Ge, a failure $fail(k), the non-negative integer
k being the "level" of the failure, or an error
$error(Ge), Ge being an error message.
If evaluating a path at the level m returns a failure
$fail(k), the failure level is certain to satisfy the restriction 0
<= k <= m+1 . In particular, if a path is evaluated at the level
0, there holds either k=0 or k=1.
A judgment Env,m,St |- Q => X,St' means that evaluating the path
Q in the environment Env at the level m
returns X, and if the evaluation of Q starts in the global
state St, it terminates in the global state St'.
Rests and sources are particular cases of paths, for which reason the above notation is
also used for describing the evaluation of rests and sources.
The meaning of a path Q can often be reduced to the meaning of other path
Q'. To put it more exactly, the evaluation of Q is done
by evaluating Q', and the result thus obtained is taken to be the result of
evaluating Q. This may be formulated by means of the following inference
rule:
Env,m,St |- Q' => X,St'
-----------------------
Env,m,St |- Q => X,St'
Such rules are rather frequent, for which reason they will be abbreviated in the following
way:
Q =>=> Q'