Factor out stuff from stlc case study into standard library

examples/stlc.pol

@@ -1,3 +1,7 @@
+use "../std/data/void.pol"
+use "../std/data/nat.pol"
+use "../std/data/ordering.pol"
+
 -- | Expressions of the object language
 data Exp {
     -- | Variables using a deBruijn representation
@@ -15,7 +19,7 @@ data Typ {
     VarT(x: Nat)
 }
 
--- | Typing contexts.
+-- | **Typing contexts**.
 -- | Because we use de Bruijn indices the typing context does not contain variable names.
 data Ctx {
     -- | The empty context
@@ -43,7 +47,7 @@ def Exp.subst(v: Nat, by: Exp): Exp {
     App(e1, e2) => App(e1.subst(v, by), e2.subst(v, by))
 }
 
-def Cmp.subst_result(x: Nat, by: Exp): Exp {
+def Ordering.subst_result(x: Nat, by: Exp): Exp {
     LT => Var(x),
     EQ => by,
     GT => Var(x.pred)
@@ -91,7 +95,7 @@ data Progress(e: Exp) {
 def (e: Exp).progress(t: Typ): HasType(Nil, e, t) -> Progress(e) {
     Var(x) =>
         \h_t. h_t.match {
-            TVar(_, _, _, elem) => elem.empty_absurd(x, t).elim_bot(Progress(Var(x))),
+            TVar(_, _, _, elem) => elem.empty_absurd(x, t).ex_falso(Progress(Var(x))),
             TLam(_, _, _, _, _) absurd,
             TApp(_, _, _, _, _, _, _) absurd
         },
@@ -185,7 +189,7 @@ def (e: Exp).subst_lemma(ctx1 ctx2: Ctx, t1 t2: Typ, by_e: Exp)
             TVar(_, _, _, h_elem) =>
                 x.cmp_reflect(ctx1.len).match {
                     IsLT(_, _, h_eq_lt, h_lt) =>
-                        h_eq_lt.transport(Cmp,
+                        h_eq_lt.transport(Ordering,
                                           LT,
                                           x.cmp(ctx1.len),
                                           comatch {
@@ -215,7 +219,7 @@ def (e: Exp).subst_lemma(ctx1 ctx2: Ctx, t1 t2: Typ, by_e: Exp)
                                                                Elem(x, t2, ctx1),
                                                                h_elem)))),
                     IsEQ(_, _, h_eq_eq, h_eq) =>
-                        h_eq_eq.transport(Cmp,
+                        h_eq_eq.transport(Ordering,
                                           EQ,
                                           x.cmp(ctx1.len),
                                           comatch {
@@ -253,7 +257,7 @@ def (e: Exp).subst_lemma(ctx1 ctx2: Ctx, t1 t2: Typ, by_e: Exp)
                                                                  },
                                                                  h_by))),
                     IsGT(_, _, h_eq_gt, h_gt) =>
-                        h_eq_gt.transport(Cmp,
+                        h_eq_gt.transport(Ordering,
                                           GT,
                                           x.cmp(ctx1.len),
                                           comatch {
@@ -419,7 +423,7 @@ def (ctx: Ctx).append_nil: Eq(Ctx, ctx, ctx.append(Nil)) {
     Cons(t, ts) => ts.append_nil.eq_cons(ts, ts.append(Nil), t)
 }
 
-def Elem(x, t, Nil).empty_absurd(x: Nat, t: Typ): Bot {
+def Elem(x, t, Nil).empty_absurd(x: Nat, t: Typ): Void {
     Here(_, _) absurd,
     There(_, _, _, _, _) absurd
 }
@@ -507,9 +511,6 @@ def (ctx1: Ctx).elem_append_pred(ctx2: Ctx, t1 t2: Typ, x: Nat)
         }
 }
 
-data Bot { }
-
-def Bot.elim_bot(a: Type): a { }
 
 codata Fun(a b: Type) {
     Fun(a, b).ap(a b: Type, x: a): b
@@ -535,21 +536,7 @@ def Eq(Ctx, xs, ys).eq_cons(xs ys: Ctx, t: Typ): Eq(Ctx, Cons(t, xs), Cons(t, ys
     Refl(_, _) => Refl(Ctx, Cons(t, xs))
 }
 
-data Nat { Z, S(n: Nat) }
-
-def Nat.pred: Nat {
-    Z => Z,
-    S(x) => x
-}
-
-data LE(x y: Nat) {
-    LERefl(x: Nat): LE(x, x),
-    LESucc(x y: Nat, h: LE(x, y)): LE(x, S(y))
-}
-
-data Cmp { LT, EQ, GT }
-
-def Nat.cmp(y: Nat): Cmp {
+def Nat.cmp(y: Nat): Ordering {
     Z =>
         y.match {
             Z => EQ,
@@ -563,20 +550,20 @@ def Nat.cmp(y: Nat): Cmp {
 }
 
 data CmpReflect(x y: Nat) {
-    IsLT(x y: Nat, h1: Eq(Cmp, LT, x.cmp(y)), h2: LE(S(x), y)): CmpReflect(x, y),
-    IsEQ(x y: Nat, h1: Eq(Cmp, EQ, x.cmp(y)), h2: Eq(Nat, x, y)): CmpReflect(x, y),
-    IsGT(x y: Nat, h1: Eq(Cmp, GT, x.cmp(y)), h2: LE(S(y), x)): CmpReflect(x, y)
+    IsLT(x y: Nat, h1: Eq(Ordering, LT, x.cmp(y)), h2: LE(S(x), y)): CmpReflect(x, y),
+    IsEQ(x y: Nat, h1: Eq(Ordering, EQ, x.cmp(y)), h2: Eq(Nat, x, y)): CmpReflect(x, y),
+    IsGT(x y: Nat, h1: Eq(Ordering, GT, x.cmp(y)), h2: LE(S(y), x)): CmpReflect(x, y)
 }
 
 def (x: Nat).cmp_reflect(y: Nat): CmpReflect(x, y) {
     Z =>
         y.match as y => CmpReflect(Z, y) {
-            Z => IsEQ(Z, Z, Refl(Cmp, EQ), Refl(Nat, Z)),
-            S(y) => IsLT(Z, S(y), Refl(Cmp, LT), y.z_le.le_succ(Z, y))
+            Z => IsEQ(Z, Z, Refl(Ordering, EQ), Refl(Nat, Z)),
+            S(y) => IsLT(Z, S(y), Refl(Ordering, LT), y.z_le.le_succ(Z, y))
         },
     S(x) =>
         y.match as y => CmpReflect(S(x), y) {
-            Z => IsGT(S(x), Z, Refl(Cmp, GT), x.z_le.le_succ(Z, x)),
+            Z => IsGT(S(x), Z, Refl(Ordering, GT), x.z_le.le_succ(Z, x)),
             S(y) =>
                 x.cmp_reflect(y).match {
                     IsLT(_, _, h1, h2) => IsLT(S(x), S(y), h1, h2.le_succ(S(x), y)),
@@ -586,26 +573,6 @@ def (x: Nat).cmp_reflect(y: Nat): CmpReflect(x, y) {
         }
 }
 
-def (x: Nat).z_le: LE(Z, x) {
-    Z => LERefl(Z),
-    S(x) => LESucc(Z, x, x.z_le)
-}
-
-def LE(x, y).le_succ(x y: Nat): LE(S(x), S(y)) {
-    LERefl(_) => LERefl(S(x)),
-    LESucc(x, y, h) => LESucc(S(x), S(y), h.le_succ(x, y))
-}
-
-def LE(S(x), S(y)).le_unsucc(x y: Nat): LE(x, y) {
-    LERefl(_) => LERefl(x),
-    LESucc(_, _, h) => h.s_le(x, y)
-}
-
-def LE(S(x), y).s_le(x y: Nat): LE(x, y) {
-    LERefl(_) => LESucc(x, x, LERefl(x)),
-    LESucc(_, y', h) => LESucc(x, y', h.s_le(x, y'))
-}
-
 def LE(S(x), y).s_pred(x y: Nat): Eq(Nat, S(y.pred), y) {
     LERefl(_) => Refl(Nat, y),
     LESucc(_, y', _) => Refl(Nat, y)

std/data/nat.pol

@@ -33,3 +33,40 @@ def Nat.fact: Nat {
     Z => 1,
     S(pred) => S(pred).mul(pred.fact)
 }
+
+-- | The predecessor of a natural number.
+-- | The predecessor of `Z` is `Z`.
+def Nat.pred: Nat {
+    Z => Z,
+    S(x) => x
+}
+
+-- | The lesser-or-equal relation on natural numbers.
+data LE(x y: Nat) {
+    LERefl(x: Nat): LE(x, x),
+    LESucc(x y: Nat, h: LE(x, y)): LE(x, S(y))
+}
+
+-- | Z is smaller than any natural number.
+def (x: Nat).z_le: LE(Z, x) {
+    Z => LERefl(Z),
+    S(x) => LESucc(Z, x, x.z_le)
+}
+
+-- | If x <= y, then S(x) <= S(y)
+def LE(x, y).le_succ(x y: Nat): LE(S(x), S(y)) {
+    LERefl(_) => LERefl(S(x)),
+    LESucc(x, y, h) => LESucc(S(x), S(y), h.le_succ(x, y))
+}
+
+-- | If S(x) <= S(y), then x <= y.
+def LE(S(x), S(y)).le_unsucc(x y: Nat): LE(x, y) {
+    LERefl(_) => LERefl(x),
+    LESucc(_, _, h) => h.s_le(x, y)
+}
+
+-- | If S(x) <= y, then x <= y
+def LE(S(x), y).s_le(x y: Nat): LE(x, y) {
+    LERefl(_) => LESucc(x, x, LERefl(x)),
+    LESucc(_, y', h) => LESucc(x, y', h.s_le(x, y'))
+}

std/data/ordering.pol

@@ -0,0 +1,9 @@
+-- | The result of comparing two totally-ordered values.
+data Ordering {
+    -- | Lesser than
+    LT,
+    -- | Equal
+    EQ,
+    -- | Greater than
+    GT,
+}

std/data/void.pol

@@ -1,2 +1,4 @@
 -- | The trivially uninhabitated data type.
 data Void { }
+
+def Void.ex_falso(a: Type): a { }