Specware 4.1 Language Manual
PrevChapter 2. MetaslangNext

Matches and Patterns

Matches

match ::= [ | ] branch { | branch }*

branch ::= pattern -> expression
Sample matches: 
    {re = x, im = y} -> {re = x, im = -y}

      Empty -> true
    | Push {top = _, pop = rest} -> hasBottom? rest

    | Empty -> true
    | Push {top = _, pop = rest} -> hasBottom? rest
Restriction. In a match, given the environment, there must be a unique type T to which the pattern of each branch conforms, and a unique type T to which the expression of each branch conforms, and then the match has type S -> T. The pattern of each branch then has type S.

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
is not interpreted as suggested by the indentation, but as 
   case x of
     | A -> a
     | B -> (case y of
               | C -> c
               | D -> d)
If the other interpretation is intended, the expression introducing the inner match needs to be parenthesized: 
   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.

Acceptance and return value y, if any, of a value x for a branch P -> E 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, y is the value of expression E in the environment C extended with the acceptance binding of pattern P for x.

For example, in 
   case z of
     | (x, true)  -> Some x
     | (_, false) -> None
if z has value (3, true), the first branch accepts this value with acceptance binding x = 3. The value of Some x in the extended environment is then Some 3. If z has value (3, false), the second branch accepts this value with empty acceptance binding (empty since there are no "accepting" local-variables in pattern (_, false)), and the return value is None (interpreted in the original environment).

Patterns

pattern ::=
      annotated-pattern
    | tight-pattern

tight-pattern ::=
      aliased-pattern
    | cons-pattern
    | embed-pattern
    | quotient-pattern
    | relax-pattern
    | closed-pattern

closed-pattern ::=
      variable-pattern
    | wildcard-pattern
    | literal-pattern
    | list-pattern
    | tuple-pattern
    | record-pattern
    | ( pattern )
(As for expressions, the distinctions tight- and closed- for patterns have no semantic significance, but merely serve to avoid grammatical ambiguities.) 

annotated-pattern ::= pattern : type-descriptor

aliased-pattern ::= variable-pattern as tight-pattern

cons-pattern ::= closed-pattern :: tight-pattern

embed-pattern ::= constructor [ closed-pattern ]

quotient-pattern ::= quotient closed-expression tight-pattern

relax-pattern ::= relax closed-expression tight-pattern

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 ]
Sample patterns: 
    (i, p) : Integer * Boolean
    z as {re = x, im = y}
    hd :: tail
    Push {top, pop = rest}
    embed Empty
    quotient congMod3 n
    relax even e
    x
    _
    #z
    [0, x]
    (c1 as (0, _), x)
    {top, pop = rest}
Restriction. Like all polymorphic or type-ambiguous constructs, a pattern may only be used in a context where its type can be uniquely inferred.

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.)

Restriction. The closed-expression of a quotient-pattern must have some type T * T -> Boolean; in addition, it must be an equivalence relation, as explained under Type-quotients.

Restriction. Quotient-patterns may only be used in a definition or claim if the result is insensitive to the choice of representative from the equivalence class. Specware 4.1 does not attempt to generate proof obligations for establishing this.

Restriction. The closed-expression of a relax-pattern must have some function type T -> Boolean.

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
is 
    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 relaxations). 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))
Under the accepting binding 
    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
the value of each E in EDP amounts to the value x. Therefore, x is accepted by the original pattern, with acceptance binding 
    s0 = Cons (Empty, Cons (Push {top = 200, pop = Empty}, Nil))
    s1 = Cons (Push {top = 200, pop = Empty}, Nil)
    ss = Nil
    top = 200
    rest = Empty
obtained by "forgetting" the fresh simple-name v7944.

PrevHomeNext
ExpressionsUpMetaslang Grammar