Patterns
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)
- succeeds when applied to
FunDef(Id("decode"),Return(Int(0)))
-
fn will have the value "decode"
-
fb will have the value Return(Int(0))
- fails when applied to e.g. term
VarDef(Id("i"),TypeDecl(Int))
Matching on lists
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 []
Special Patterns
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.
See also