Patterns

Patterns accept ground expressions, decompose them, and bind parts of ground expressions to variables. At run-time, matching a ground expression against a pattern either succeeds or fails.

Syntax

Pattern = DirectionDesignator PatternExpression.
DirectionDesignator = [ "$l" | "$r" ].

PatternExpression =
     { PatternTerm | NamedExpression }.
PatternTerm =
     StaticSymbol | Variable |
     "(" PatternExpression ")".

A pattern is a pattern expression, which may be preceded by a direction designator $l or $r. The designator $l indicates that the pattern matching must be done from left to right. The designator $r indicates that it must be done from right to left. If the direction designator is omitted, the designator $l is implied.

If two different variables appear in the same pattern expression, they must have different indices.

Notation

Patterns are denoted by P, pattern expressions by Pe, pattern terms by Pt, and direction designators by D.

Pattern Matching

An environment Env is said to be a result of matching a ground expression Ge against a pattern P in an initial environment Env₀, if the following conditions holds.

The environment Env is an extension of Env₀, i.e. dom[Env] includes dom[Env₀], and for all V in dom[Env₀] holds Env(V)=Env₀(V).
If each variable V appearing in P is replaced with Env(V), and the direction designator is removed, the ground expression thus obtained is Ge.

This environment Env is said to be a variant of matching Ge against P in the environment Env₀, and the set of such variants of matching is denoted by Match(Env₀,Ge,P).

The set Match(Env₀,Ge,P) is assumed to be equipped with the order relation defined by the following rules.

Suppose Match(Env₀,Ge,P) contains two different variants of matching Env₁ and Env₂. Consider all occurrences of variables in P.

If P has the direction designator $l, find the leftmost occurrence that is given different values by the matching variants Env₁ and Env₂.

If P has the direction designator $r, find the rightmost occurrence that is given different values by the matching variants Env₁ and Env₂.

Suppose the occurrence found is an occurrence of a variable V. Then compare Env₁(V) to Env₂(V). If Env₁(V) is shorter than Env₂(V), then Env₁ is taken to precede Env₂. Otherwise Env₂ is taken to precede Env₁.

A finite sequence of environments Env₁, Env₂, ..., Env_n is written as [Env₁, Env₂, ... , Env_n], and the empty sequence as [].

[Env₀]^[Env₁,...,Env_n] denotes [Env₀, Env₁,..., Env_n].

A judgment Env₀ |- Ge : P => [Env₁,...Env_n] means that Match(Env₀,Ge,P) = {Env₁,...,Env_n}, where Env_i precedes Env_j for all i<j.

Examples

Here are examples of patterns:

          t.Head e.Tail
          eX (eY)
          eA '+' eB
          $l eA '+' eB
          $r eA '+' eB

Here are examples of pattern matching:

{} |- A () C D E : $l sX tY tZ e1
     =>  [ {sX = A, tY = (), tZ = C, e1 = D E} ]

{} |- 1 2 3 : $l eA eB =>  [
                    {eA = ,         eB = 1 2 3},
                    {eA = 1,        eB = 2 3},
                    {eA = 1 2,      eB = 3},
                    {eA = 1 2 3,    eB = }  ]

{} |- 1 2 3 : $r eA eB => [
                    {eA = 1 2 3,    eB =       },
                    {eA = 1 2,      eB = 3     },
                    {eA = 1,        eB = 2 3   },
                    {eA = ,         eB = 1 2 3 }  ]

{eA = 1 2} |- $l 1 2 3 4 5 : eA eB
     =>  [ {eA = 1 2, eB = 3 4 5} ]