9.9. Pattern Match

9.9.1. Ideas from “Implementation of Functional Languages” of Simon Peyton Jones.

We transform a pattern match expression:

case
    \ p11 p12 ... p1m := e1
    ...
    \ pn1 pn2 ... pnm := e2

into:

\ x1 x2 ... xm :=
    inspect
        x1 x2 ... xm
    case
        \ p11 p12 ... p1m := e1
        ...
        \ pn1 pn2 ... pnm := e2

• All p11, p21, … and pn1 are variable pattern (say y):

  \ x1 x2 ... xm :=
      inspect
          x2 ... xm
      case
          \ p12[y:=x1] ... p1m[y:=x1] := e1[y:=x1]
          ...
          \ pn2[y:=x1] ... pnm[y:=x1] := en[y:=x1]
  

• All p11, p21, … and pn1 are constructor pattern:

  \ x1 x2 ... xm :=
      inspect
          x1
      case
          \ p11 :=
              inspect x2 ... xm case
                  \ p12 ... p1m := e1
                  ...
                  \ pn2 ... pnm := en
          \ p21 :=
              -- same
          ...
  

9.9.2. Examples

Less equal and greater equal:

(<=?): Natural -> Natural -> Bool := case
    \ zero :=
        \ _ := true
    \ succ n := case
        \ zero   := false
        \ succ m := n <=? m

(>=?): Natural -> Natural -> Bool := case
    \ zero := case
        \ zero   := true
        \ succ m := false
    \ succ n := case
        \ zero   := true
        \ succ m := n >=? m

map2:

map2 {A B C: Any} (f: A -> B -> C): List A -> List B -> List C
:= case
    \ [] :=
        \ _ := []
    \ x :: xs := case
        \ []        := []
        \ y :: ys   := f x y :: map2 xs ys

-- the same with vectors
map2
    {A B C: Any} (f: A -> B -> C)
    : all {n}: Vector A n -> Vector B n -> Vector C n
:=
    \ {_} := case
        \ [] := case
            \ [] := []
        \ x :: xs := case
            \ y :: ys :=
                f x y :: map2 xs ys

nodups:

nodups {A: Any} ((=?): A -> A -> Bool): List A -> List A := case
    \ [] := []
    \ x :: xs :=
        inspect xs case
            \ [] := [x]
            \ y :: ys :=
                (if x =? y then res else x :: res)
                where
                    res := nodups (y :: ys)

A data type for a bounded natural number:

type Below: Natural -> Any :=
    start {k}: Below (succ k)
    next  {k}: Below k -> Below (succ k)

Look up in a vector:

-- cascaded form
at {A: Any}: all {n}: Below n -> Vector A n -> A :=
    \ {k} := case
        \ (start {k}) := case
            \ x :: _ := x
        \ (next {k} below) :=
            \ _ :: xs := at below xs

-- flat form
at {A: Any}: all {n}: Below n -> Vector A n -> A := case
    \ start (x :: _) :=
        x
    \ (next below) (_ :: xs) :=
        at below xs