test suite for pattern match elaboration into affine case-trees (λ-matches)

gistfile1.txt

λn.
  match n:
    case #Z:
      A
    case #S{a}:
      B(a)
//λ{#Z:A;#S:λa.B(a)}

λn.
  match n:
    case #Z:
      A
    case a:
      B(a)
//λ{#Z:A;λa.B(a)}

λn.
  match n:
    case a:
      A
    case a:
      B(a)
//fail: overlapping-patterns

λn.
  match n:
    case a:
      A
    case #S{a}:
      B(a)
//fail: overlapping-patterns

λn.
  match n:
    case #Z:
      A
    case #S{#Z}:
      B
    case #S{#S{a}}:
      C(a)
//λ{#Z:A;#S:λ{#Z:B;#S:λa.C(a)}}

λn.
  match n:
    case #Z:
      A
    case #S{a}:
      B(a)
    case #S{#S{a}}:
      C(a)
//fail: overlapping-patterns

λn.
  match n:
    case #Z:
      A
    case #S{#S{a}}:
      C(a)
    case #S{a}:
      B(a)
//λ{#Z:A;#S:λ{#S:λa.C(a);λa.B(a)}}

λn.
  match n:
    case #Z:
      A
    case #S{#S{a}}:
      C(a)
    case a:
      B(a)
//λ{#Z:A;#S:λ{#S:λa.C(a);λa.B(#S{a})};λa.B(a)}

λn.
  match n:
    case #Z:
      A
    case #S{#S{a}}:
      B(a)
    case #S{#S{#S{a}}}:
      C(a)
//fail: overlapping-patterns

λn.
  match n:
    case #Z:
      A
    case #S{#S{#S{a}}}:
      B(a)
    case #S{a}:
      C(a)
//λ{#Z:A;#S:λ{#S:λ{#S:λa.B(a);λa.C(#S{a})};λa.C(a)}}

λn.
  match n:
    case #S{a}:
      A(a)
//λ{#S:λa.A(a)}

λn.
  match n:
    case #S{#S{a}}:
      A(a)
    case #S{a}:
      B(a)
//λ{#S:λ{#S:λa.A(a);λa.B(a)}}

λn.
  match n:
    case #S{a}:
      A(a)
    case #S{b}:
      B(b)
//fail: overlapping-patterns

λx. λy.
  match x y:
    case a b:
      A(a,b)
//λa.λb.A(a,b)

λx. λy.
  match x y:
    case #Z b:
      A(b)
    case a b:
      B(a,b)
//λ{#Z:λb.A(b);λa.λb.B(a,b)}

λx. λy.
  match x y:
    case #S{a} #Z:
      A(a)
    case #S{a} b:
      B(a,b)
    case a b:
      C(a,b)
//λ{#S:λa.λ{#Z:A(a);λb.B(a,b)};λa.λb.C(a,b)}

λx. λy.
  match x y:
    case #S{a} #S{b}:
      A(a,b)
    case #Z b:
      B(b)
    case a b:
      C(a,b)
//λ{#S:λa.λ{#S:λb.A(a,b);λb.C(#S{a},b)};#Z:λb.B(b);λa.λb.C(a,b)}

λx. λy.
  match x y:
    case #S{a} #S{#S{b}}:
      A(a,b)
    case #S{a} #S{b}:
      B(a,b)
    case #S{a} #Z:
      C(a)
    case d e:
      D(d,e)
//λ{#S:λa.λ{#S:λ{#S:λb.A(a,b);λb.B(a,b)};#Z:C(a);λb.D(#S{a},b)};λa.λb.D(a,b)}

λx. λy.
  match x y:
    case #S{#S{a}} #S{b}:
      A(a,b)
    case #S{#S{a}} #Z:
      B(a)
    case #S{a} b:
      C(a,b)
    case a b:
      D(a,b)
//λ{#S:λ{#S:λa.λ{#S:λb.A(a,b);#Z:B(a);λb.C(#S{a},b)};λa.λb.C(a,b)};λa.λb.D(a,b)}

λx. λy.
  match x y:
    case #S{#S{a}} #S{#S{b}}:
      A(a,b)
    case #S{#S{a}} #S{b}:
      B(a,b)
    case #S{a} #Z:
      C(a)
    case #S{a} b:
      D(a,b)
    case a b:
      E(a,b)
//λ{#S:λ{#S:λa.λ{#S:λ{#S:λb.A(a,b);λb.B(a,b)};#Z:C(#S{a});λb.D(#S{a},b)};λa.λ{#Z:C(a);λb.D(a,b)}};λa.λb.E(a,b)}

λx. λy.
  match x y:
    case #S{#S{a}} #S{#S{b}}:
      A(a,b)
    case #S{#S{a}} #S{b}:
      B(a,b)
    case #S{a} #Z:
      C(a)
    case #S{a} b:
      D(a,b)
    case a #S{b}:
      E(a,b)
    case a #Z:
      F(a)
//λ{#S:λ{#S:λa.λ{#S:λ{#S:λb.A(a,b);λb.B(a,b)};#Z:C(#S{a});λb.D(#S{a},b)};λa.λ{#Z:C(a);λb.D(a,b)}};λa.λ{#S:λb.E(a,b);#Z:F(a)}}

λx. λy.
  match x y:
    case a #S{b}:
      A(a,b)
    case #Z #S{b}:
      B(b)
    case a b:
      C(a,b)
//fail: overlapping-patterns

λx. λy.
  match x y:
    case #Z b:
      A(b)
    case a #S{b}:
      B(a,b)
    case a #Z:
      C(a)
//λ{#Z:λb.A(b);λa.λ{#S:λb.B(a,b);#Z:C(a)}}

λx. λy.
  match x y:
    case a #S{b}:
      A(a,b)
    case a #Z:
      B(a)
//λa.λ{#S:λb.A(a,b);#Z:B(a)}

λx. λy.
  match x y:
    case #S{a} #S{#Z}:
      A(a)
    case a #S{b}:
      B(a,b)
    case a #Z:
      C(a)
//λ{#S:λa.λ{#S:λ{#Z:A(a);λb.B(#S{a},b)};#Z:C(#S{a})};λa.λ{#S:λb.B(a,b);#Z:C(a)}}

λx. λy.
  match x y:
    case #S{a} #S{b}:
      A(a,b)
    case #S{a} #Z:
      B(a)
    case #Z #S{b}:
      C(b)
    case #Z #Z:
      D
//λ{#S:λa.λ{#S:λb.A(a,b);#Z:B(a)};#Z:λ{#S:λb.C(b);#Z:D}}

λx. λy.
  match x y:
    case #S{a} #S{b}:
      A(a,b)
    case a #S{b}:
      B(a,b)
    case #Z #Z:
      C
    case #S{a} #Z:
      D(a)
//λ{#S:λa.λ{#S:λb.A(a,b);#Z:D(a)};#Z:λ{#S:λb.B(#Z,b);#Z:C};λa.λ{#S:λb.B(a,b)}}

λx. λy.
  match x y:
    case #S{a} #S{b}:
      A(a,b)
    case #Z #S{b}:
      B(b)
    case c #Z:
      C(c)
//λ{#S:λa.λ{#S:λb.A(a,b);#Z:C(#S{a})};#Z:λ{#S:λb.B(b);#Z:C(#Z)};λa.λ{#Z:C(a)}}

λx. λy.
  match x y:
    case #S{a} b:
      A(a,b)
    case c #S{d}:
      B(c,d)
    case #S{a} #S{b}:
      C(a,b)
//fail: overlapping-patterns

λx. λy. λz.
  match x y z:
    case #S{a} #S{b} #S{c}:
      A(a,b,c)
    case #S{a} #S{b} c:
      B(a,b,c)
    case #S{a} b #Z:
      C(a,b)
    case a b c:
      D(a,b,c)
//λ{#S:λa.λ{#S:λb.λ{#S:λc.A(a,b,c);λc.B(a,b,c)};λb.λ{#Z:C(a,b);λc.D(#S{a},b,c)}};λa.λb.λc.D(a,b,c)}

λx. λy. λz.
  match x y z:
    case #S{a} #S{b} #S{c}:
      A(a,b,c)
    case #S{a} #S{b} #Z:
      B(a,b)
    case #S{a} #Z #S{c}:
      C(a,c)
    case #S{a} #Z #Z:
      D(a)
    case #Z #S{b} #S{c}:
      E(b,c)
    case #Z #S{b} #Z:
      F(b)
    case #Z #Z #S{c}:
      G(c)
    case #Z #Z #Z:
      H
//λ{#S:λa.λ{#S:λb.λ{#S:λc.A(a,b,c);#Z:B(a,b)};#Z:λ{#S:λc.C(a,c);#Z:D(a)}};#Z:λ{#S:λb.λ{#S:λc.E(b,c);#Z:F(b)};#Z:λ{#S:λc.G(c);#Z:H}}}

λx. λy. λz.
  match x y z:
    case #S{a} b c:
      A(a,b,c)
    case a #S{b} c:
      B(a,b,c)
    case #S{a} #S{b} c:
      C(a,b,c)
    case a b c:
      D(a,b,c)
//fail: overlapping-patterns

λx. λy. λz.
  match x y z:
    case #S{a} #Z #S{b}:
      A(a,b)
    case #S{a} b #Z:
      B(a,b)
    case #Z #S{a} b:
      C(a,b)
    case a b c:
      D(a,b,c)
//λ{#S:λa.λ{#Z:λ{#S:λb.A(a,b);#Z:B(a,#Z);λb.D(#S{a},#Z,b)};λb.λ{#Z:B(a,b);λc.D(#S{a},b,c)}};#Z:λ{#S:λa.λb.C(a,b);λa.λb.D(#Z,a,b)};λa.λb.λc.D(a,b,c)}

λxs.
  match xs:
    case #C{#F, a}:
      A(a)
    case #C{#T, a}:
      B(a)
    case #N:
      C
//λ{#C:λ{#F:λa.A(a);#T:λa.B(a)};#N:C}

λxs.
  match xs:
    case #C{#S{a}, b}:
      A(a,b)
    case #C{#Z, a}:
      B(a)
    case #N:
      C
//λ{#C:λ{#S:λa.λb.A(a,b);#Z:λa.B(a)};#N:C}

λxs.
  match xs:
    case #C{#S{#S{a}}, b}:
      A(a,b)
    case #C{a, b}:
      B(a,b)
    case #N:
      C
//λ{#C:λ{#S:λ{#S:λa.λb.A(a,b);λa.λb.B(#S{a},b)};λa.λb.B(a,b)};#N:C}

λxs.
  match xs:
    case #C{#S{a}, #C{b, c}}:
      A(a,b,c)
    case #C{a, b}:
      B(a,b)
    case #N:
      C
//λ{#C:λ{#S:λa.λ{#C:λb.λc.A(a,b,c);λb.B(#S{a},b)};λa.λb.B(a,b)};#N:C}

λxs.
  match xs:
    case #C{#S{a}, b}:
      A(a,b)
    case #C{#Z, #N}:
      B
    case #C{#Z, #C{a, b}}:
      C(a,b)
    case #N:
      D
//λ{#C:λ{#S:λa.λb.A(a,b);#Z:λ{#N:B;#C:λa.λb.C(a,b)}};#N:D}

λxs.
  match xs:
    case #C{#S{#S{a}}, #C{#Z, b}}:
      A(a,b)
    case #C{#S{a}, #C{b, c}}:
      B(a,b,c)
    case #C{#S{a}, #N}:
      C(a)
    case #C{#Z, #C{#S{a}, b}}:
      D(a,b)
    case #C{a, b}:
      E(a,b)
    case #N:
      F
//λ{#C:λ{#S:λ{#S:λa.λ{#C:λ{#Z:λb.A(a,b);λb.λc.B(#S{a},b,c)};#N:C(#S{a});λb.E(#S{#S{a}},b)};λa.λ{#C:λb.λc.B(a,b,c);#N:C(a);λb.E(#S{a},b)}};#Z:λ{#C:λ{#S:λa.λb.D(a,b);λa.λb.E(#Z,#C{a,b})};λa.E(#Z,a)};λa.λb.E(a,b)};#N:F}

λxs. λys.
  match xs ys:
    case #C{#S{a}, b} #C{#S{c}, d}:
      A(a,b,c,d)
    case #C{#S{a}, b} #C{c, d}:
      B(a,b,c,d)
    case #C{#Z, b} #C{#S{c}, d}:
      C(b,c,d)
    case #C{a, b} #N:
      D(a,b)
    case #N #C{a, b}:
      E(a,b)
    case #N #N:
      F
//λ{#C:λ{#S:λa.λb.λ{#C:λ{#S:λc.λd.A(a,b,c,d);λc.λd.B(a,b,c,d)};#N:D(#S{a},b)};#Z:λb.λ{#C:λ{#S:λc.λd.C(b,c,d)};#N:D(#Z,b)};λa.λb.λ{#N:D(a,b)}};#N:λ{#C:λa.λb.E(a,b);#N:F}}

λn. λxs. λys.
  match n xs ys:
    case #Z a b:
      A
    case #S{a} #N b:
      B(a,b)
    case #S{a} #C{#Z,b} c:
      C(a,b,c)
    case #S{a} #C{#S{b},c} d:
      D(a,b,c,d)
//λ{#Z:λa.λb.A;#S:λa.λ{#N:λb.B(a,b);#C:λ{#Z:λb.λc.C(a,b,c);#S:λb.λc.λd.D(a,b,c,d)}}}