Hard expressions are patterns that accept ground expressions, decompose them, and bind parts of ground expressions to variables. At run-time, matching a ground expression against a hard expression always succeeds, which is guaranteed by the context dependent restrictions on Refal Plus programs checked at compile-time.
HardExpression =
{ HardCorner } |
{ HardCorner } e-variable { HardCorner } |
{ HardCorner } v-variable { HardCorner }.
HardCorner = { HardTerm | NamedExpression }.
HardTerm =
StaticSymbol | s-variable | t-variable |
"(" HardExpression ")".
Thus, any subexpression of a hard expression may contain no more that one occurrence of e-variable or v-variable at the top level of parentheses.
A variable may appear in a hard expression no more that once. If two different variables appear in the same hard expression, they must have different indices.
Hard expressions are denoted by He, and hard terms by Ht.
Hard expressions may be regarded as a particular case of pattern expressions. A feature of hard expressions is that there can exist no more that one way of matching a ground expression Ge against a hard expression He. Thus there holds either {} |- Ge : He => [ ] or {} |- Ge : He => [Env].
A judgment Env |- Ge :: He => Env' means that {} |- Ge : He => Env'' and Env' = Env+Env''. Consequently, Env' is produced from Env in the following way. First, Ge is matched against He in the empty environment. Thus, the variable values provided by the current environment Env are not taken into account. The environment Env'' thus obtained contains bindings for all variables appearing in He. Then the original environment Env is extended with the bindings from Env'' to produce the final environment Env'.
t.Head e.Tail
sX (eY) eZ (A eA)
{sX = XXX, eA = A B C} |- X Y Z :: sY eA
=> {sX = XXX, eA = Y Z, sY = X}
{sX = XXX, eA = A B C} |- X Y Z :: eA sY
=> {sX = XXX, eA = X Y, sY = Z}