match ::= [ | ] branch { | branch }* branch ::= pattern [ guard ] -> expression guard ::= | expression |
{re = x, im = y} -> {re = x, im = -y}
Empty -> true
| Push {top = _, pop = rest} -> hasBottom? rest
| Empty -> true
| Push {top = _, pop = rest} -> hasBottom? rest
| Line(z0, z1) | z0 ~= z1 -> dist(z0, z1) |
Restriction. The type of the expression of a guard must be Boolean
Disambiguation. If a branch could belong to several open matches, it is interpreted as being a branch of the textually most recently introduced match. For example,
case x of
| A -> a
| B -> case y of
| C -> c
| D -> d |
case x of
| A -> a
| B -> (case y of
| C -> c
| D -> d) |
case x of
| A -> a
| B -> (case y of
| C -> c)
| D -> d |
Acceptance and return value y, if any, of a value x for a given match are determined as follows. If each branch of the match rejects x (see below), the whole match rejects x, and does not return a value. Otherwise, let B stand for the textually first branch accepting x. Then y is the return value of x for B.
The meaning of a "guardless" branch P -> R, where P is a pattern and R an expression, is the same as that of the branch P | true -> R with a guard that always succeeds.
Acceptance and return value y, if any, of a value x for a branch P | G -> R in an environment C are determined as follows. If pattern P rejects x, the branch rejects x, and does not return a value. (For acceptance by a pattern, see under Patterns.) Otherwise, let C' be environment C extended with the acceptance binding of pattern P for x. If pattern P accepts x, but the value of expression G in the environment C' is false, the branch also rejects x, and does not return a value. Otherwise, when the pattern accepts x and the guard succeeds, the branch accepts x and the return value y is the value of expression R in the environment C'.
For example, in
case z of
| (x, true) -> Some x
| (_, false) -> None |
Here is a way of achieving the same result using a guard:
case z of
| (x, b) | b -> Some x
| _ -> None |
pattern ::= annotated-pattern | tight-pattern tight-pattern ::= aliased-pattern | cons-pattern | embed-pattern | quotient-pattern | closed-pattern closed-pattern ::= variable-pattern | wildcard-pattern | literal-pattern | list-pattern | tuple-pattern | record-pattern | ( pattern ) |
annotated-pattern ::= pattern type-annotation aliased-pattern ::= variable-pattern as tight-pattern cons-pattern ::= closed-pattern :: tight-pattern embed-pattern ::= constructor [ closed-pattern ] quotient-pattern ::= quotient [ type-name ] variable-pattern ::= local-variable wildcard-pattern ::= _ literal-pattern ::= literal list-pattern ::= [ list-pattern-body ] list-pattern-body ::= [ pattern { , pattern }* ] tuple-pattern ::= ( tuple-pattern-body ) tuple-pattern-body ::= [ pattern , pattern { , pattern }* ] record-pattern ::= { record-pattern-body } record-pattern-body ::= [ field-patterner { , field-patterner }* ] field-patterner ::= field-name [ equals pattern ] |
(i, p) : Integer * Boolean
z as {re = x, im = y}
hd :: tail
Push {top, pop = rest}
embed Empty
x
_
#z
[0, x]
(c1 as (0, _), x)
{top, pop = rest} |
Disambiguation. A single simple-name used as a pattern is an embed-pattern if it is a constructor of the type of the pattern. Otherwise, the simple-name is a variable-pattern.
Restriction. Each local-variable in a pattern must be a different simple-name, disregarding any local-variables introduced in expressions or type-descriptors contained in the pattern. (For example, Line (z, z) is not a lawful pattern, since z is repeated; but n : {n : Nat | n < p} is lawful: the second n is "shielded" by the type-comprehension in which it occurs.)
To define acceptance and acceptance binding (if any) for a value and a pattern, we introduce a number of auxiliary definitions.
The accepting local-variables of a pattern P are the collection of local-variables occurring in P, disregarding any local-variables introduced in expressions or type-descriptors contained in the P. For example, in pattern u : {v : S | p v}, u is an accepting local-variable, but v is not. (The latter is an accepting local-variable of pattern v : S, but not of the larger pattern.)
The expressive descendants of a pattern are a finite set of expressions having the syntactic form of patterns, as determined in the following three steps (of which the order of steps 1 and 2 is actually immaterial).
Step 1. From pattern P, form some tame variant Pt by replacing each field-patterner consisting of a single field-name F by the field-patterner F = F and replacing each wildcard-pattern _ in P by a unique fresh simple-name, that is, any simple-name that does not already occur in the spec, directly or indirectly through an import. For example, assuming that the simple-name v7944 is fresh, a tame variant of
s0 as _ :: s1 as (Push {top, pop = rest}) :: ss |
s0 as v7944 :: s1 as (Push {top = top, pop = rest}) :: ss |
Step 2. Next, from Pt, form a (tamed) construed version Ptc by replacing each constituent cons-pattern H :: T by the embed-pattern Cons (H, T), where Cons denotes the constructor of the parameterized type List. For the example, the construed version is:
s0 as Cons (v7944,
s1 as Cons (Push {top = top, pop = rest}, ss)) |
Step 3. Finally, from Ptc, form the set EDP of expressive descendants of P, where expression E is an expressive descendant if E can be obtained by repeatedly replacing some constituent aliased-pattern L as R of Ptc by one of the two patterns L and R until no aliased-patterns remain, and then interpreting the result as an expression. For the example, the expressive descendants are the three expressions:
s0
Cons (v7944, s1)
Cons (v7944, Cons (Push {top = top, pop = rest}, ss)) |
An accepting binding of a pattern P for a value x in an environment C is some binding B of typed values to the accepting local-variables of the tame variant Pt, such that the value of each expressive descendant E in EDP in the environment C extended with binding B, is the same typed value as x.
Acceptance and acceptance binding, if any, for a value x and a pattern P are then determined as follows. If there is no accepting binding of P for x, x is rejected. If an accepting binding exists, the value x is accepted by pattern P. There is a unique binding B among the accepting bindings in which the type of each assigned value is as "restricted" as possible in the subtype-supertype hierarchy without violating well-typedness constraints (in other words, there are no avoidable implicit coercions). The acceptance binding is then the binding B projected on the accepting local-variables of P.
For the example, the accepting local-variables of Pt are the six local-variables s0, s1, ss, rest and v7944. In general, they are the accepting local-variables of the original pattern together with any fresh simple-names used for taming. Let the value x being matched against the pattern be
Cons (Empty, Cons (Push {top = 200, pop = Empty}, Nil)) |
s0 = Cons (Empty, Cons (Push {top = 200, pop = Empty}, Nil))
s1 = Cons (Push {top = 200, pop = Empty}, Nil)
ss = Nil
top = 200
rest = Empty
v7944 = Empty |
s0 = Cons (Empty, Cons (Push {top = 200, pop = Empty}, Nil))
s1 = Cons (Push {top = 200, pop = Empty}, Nil)
ss = Nil
top = 200
rest = Empty |