Specware 4.0 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 sort S to which the pattern of each branch conforms, and a unique sort T to which the expression of each branch conforms, and then the match has sort S -> T. The pattern of each branch then has sort 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 : sort

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 sort-ambiguous constructs, a pattern may only be used in a context where its sort can be uniquely inferred.

Disambiguation. A single name used as a pattern is an embed-pattern if it is a constructor of the sort of the pattern. Otherwise, the name is a variable-pattern.

Restriction. Each local-variable in a pattern must be a different name, disregarding any local-variables introduced in expressions or sorts 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 sort-comprehension in which it occurs.)

Restriction. The closed-expression of a quotient-pattern must have some sort S * S -> Boolean; in addition, it must be an equivalence relation, as explained under Sort-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.0 does not attempt to generate proof obligations for establishing this.

Restriction. The closed-expression of a relax-pattern must have some function sort S -> 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 sorts 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 name, that is, any name that does not already occur in the spec, directly or indirectly through an import. For example, assuming that the 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 sort 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 sorted 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 sorted 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 sort of each assigned value is as "restricted" as possible in the subsort-supersort hierarchy without violating well-sortedness 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 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 name v7944.

PrevHomeNext
ExpressionsUpMetaslang Grammar