The match strategy (?
) Compares the current term to a pattern. A pattern is a term that might contain variables. If a variable in a term pattern is already bound to a term , then the variable in the pattern will be replaced with this value. If variables in term are not yet bound, then these variables will be bound to the actual values in the current term to which the pattern is applied.
For example, ?FunDef(Id(fn),fb)
FunDef(Id("decode"),Return(Int(0)))
fn
will have the value "decode"
fb
will have the value Return(Int(0))
VarDef(Id("i"),TypeDecl(Int))
Explained using some examples:
0: ?[x | xs] applied to [] will fail 1: ?[x | xs] applied to [1] will yield x = 1, xs = [] 2: ?[x | xs] applied to [1,2] will yield x = 1, xs = [2] 3: ?[x | xs] applied to [1,2,3,4] will yield x = 1, xs = [2,3,4] 4: ?[x , xs] applied to [] will fail 5: ?[x , xs] applied to [1] will fail 6: ?[x , xs] applied to [1,2] will yield x = 1, xs = 2 7: ?[x , xs] applied to [1,2,3,4] will fail ?[] will only succeed on an empty list []
Pattern matching is not restricted to terms containing variables. Some special matching operators exist. The generic term (de)construction pattern #
is explained in Generic Term Deconstruction.
The pattern @
allows takes a variable (v
) at its left-hand side and a pattern p
at the right-hand side. The current term will be matched against the pattern p
and in addition the current will be bound to v
. Thus, ?x@p
is equal to ?p; ?x
and ?x; ?p
.