Funcons-beta : Patterns.cbs | PRETTY | PDF

Patterns

[
  Datatype patterns
  Funcon   pattern
  Funcon   pattern-any
  Funcon   pattern-bind
  Funcon   pattern-type
  Funcon   pattern-else
  Funcon   pattern-unite
  Funcon   match
  Funcon   match-loosely
  Funcon   case-match
  Funcon   case-match-loosely
  Funcon   case-variant-value
]

General patterns are simple patterns or structured patterns. Matching a pattern to a value either computes an environment or fails.

Simple patterns are constructed from abstractions whose bodies depend on a given value, and whose executions either compute environments or fail.

Structured patterns are composite values whose components may include simple patterns as well as other values.

Matching a structured value to a structured pattern is similar to assigning a structured value to a structured variable, with simple pattern components matching component values analogously to simple variable components assigned component values.

Note that patterns match only values, not (empty or proper) sequences.

Meta-variables
  T, T′ <: values

Simple patterns

Datatype
  patterns ::= pattern(_:abstractions(values=>environments))

patterns is the type of simple patterns that can match values of a particular type.

pattern(abstraction(X)) constructs a pattern with dynamic bindings, and pattern(closure(X)) computes a pattern with static bindings. However, there is no difference between dynamic and static bindings when the pattern is matched in the same scope where it is constructed.

Funcon
  pattern-any : =>patterns
    ~> pattern(abstraction(map( )))

pattern-any matches any value, computing the empty environment.

Funcon
  pattern-bind(I:identifiers) : =>patterns
    ~> pattern(abstraction(bind-value(I, given)))

pattern-bind(I) matches any value, computing the environment binding I to that value.

Funcon
  pattern-type(T) : =>patterns
    ~> pattern(abstraction(if-true-else(is-in-type(given, T), map( ), fail)))

pattern-type(T) matches any value of type T, computing the empty environment.

Funcon
  pattern-else(_:values, _:values) : =>patterns
Rule
  pattern-else(P1:values, P2:values)
    ~> pattern(abstraction(else(match(given, P1), match(given, P2))))

pattern-else(P1, P2) matches all values matched by P1 or by P2. If a value matches P1, that match gives the computed environment; if a value does not match P1 but matches P2, that match gives the computed environment; otherwise the match fails.

Funcon
  pattern-unite(_:values, _:values) : =>patterns
Rule
  pattern-unite(P1:values, P2:values)
    ~> pattern(abstraction(collateral(match(given, P1), match(given, P2))))

pattern-unite(P1, P2) matches all values matched by both P1 and P2, then uniting the computed environments, which fails if the domains of the environments overlap.

Pattern matching

Funcon
  match(_:values, _:values) : =>environments

match(V, P) takes a (potentially structured) value V and a (potentially structured) pattern P. Provided that the structure and all components of P exactly match the structure and corresponding components of V, the environments computed by the simple pattern matches are united.

Rule
  match(V:values, pattern(abstraction(X))) ~> give(V, X)
Rule
  I2 =/= "pattern"
  --------------------------------------------
  match(datatype-value(I1:identifiers, V1*:values*),
        datatype-value(I2:identifiers, V2*:values*))
    ~> sequential(
         check-true(is-equal(I1, I2)),
         check-true(is-equal(length V1*, length V2*)),
         collateral(interleave-map(
           match(tuple-elements(given)),
           tuple-zip(tuple(V1*), tuple(V2*)))))
Rule
  dom(M2) == {}
  ------------------------------------------------------
  match(M1:maps(_,_), M2:maps(_,_))
    ~> if-true-else(is-equal(dom(M1), {}), map( ), fail)
Rule
  dom(M2) =/= {}
  some-element(dom(M2)) ~> K
  -------------------------------------------------------
  match(M1:maps(_,_), M2:maps(_,_))
    ~> if-true-else(
         is-in-set(K, dom(M1)),
         collateral(
           match(map-lookup(M1, K), map-lookup(M2, K)),
           match(map-delete(M1, {K}), map-delete(M2, {K}))),
         fail)
Rule
  P : ~(datatype-values|maps(_,_))
  -----------------------------------------------
  match(V:values, P:values)
    ~> if-true-else(is-equal(V, P), map( ), fail)

Funcon
  match-loosely(_:values, _:values) : =>environments

match-loosely(V, P) takes a (potentially structured) value V and a (potentially structured) pattern P. Provided that the structure and all components of P loosely match the structure and corresponding components of V, the environments computed by the simple pattern matches are united.

Rule
  match-loosely(V:values, pattern(abstraction(X))) ~> give(V, X)
Rule
  I2 =/= "pattern"
  ---------------------------------------------------
  match-loosely(datatype-value(I1:identifiers, V1*:values*),
        datatype-value(I2:identifiers, V2*:values*))
    ~> sequential(
         check-true(is-equal(I1, I2)),
         check-true(is-equal(length V1*, length V2*)),
         collateral(interleave-map(
           match-loosely(tuple-elements(given)),
           tuple-zip(tuple(V1*), tuple(V2*)))))
Rule
  dom(M2) == {}
  -------------------------------------------------
  match-loosely(M1:maps(_,_), M2:maps(_,_)) ~> map()
Rule
  dom(M2) =/= {}
  some-element(dom(M2)) ~> K
  --------------------------------------------------------------
  match-loosely(M1:maps(_,_), M2:maps(_,_))
    ~> if-true-else(
         is-in-set(K, dom(M1)),
         collateral(
           match-loosely(map-lookup(M1, K), map-lookup(M2, K)),
           match-loosely(map-delete(M1, {K}), map-delete(M2, {K}))),
         fail)
Rule
  P : ~(datatype-values|maps(_,_))
  -------------------------------------------
  match-loosely(DV:values, P:values)
    ~> if-true-else(is-equal(DV, P), map( ), fail)

Funcon
  case-match(_:values, _:=>T′) : =>T′

case-match(P, X) matches P exactly to the given value. If the match succeeds, the computed bindings have scope X.

Rule
  case-match(P:values, X) ~> scope(match(given, P), X)

Funcon
  case-match-loosely(_:values, _:=>T′) : =>T′

case-match(P, X) matches P loosely to the given value. If the match succeeds, the computed bindings have scope X.

Rule
  case-match-loosely(P:values, X) ~> scope(match-loosely(given, P), X)

Funcon
  case-variant-value(_:identifiers) : =>values

case-variant-value(I) matches values of variant I, then giving the value contained in the variant.

Rule
  case-variant-value(I:identifiers) ~>
    case-match(variant(I, pattern-any), variant-value(given))

← ↑