Paths

The evaluation of a path produces either a ground expression, a failure, or an error.

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.

Notation

Paths are denoted by Q, rests by R, sources by S, pattern alternatives by Palt, and sentences by Snt.

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'