Define terms and thinnings.

4 files changed, 153 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..796b96d
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/build
diff --git a/church-eval.ipkg b/church-eval.ipkg
new file mode 100644
index 0000000..eeb9b67
--- /dev/null
+++ b/church-eval.ipkg
@@ -0,0 +1,9 @@
+package church-eval
+authors = "Greg Brown"
+sourcedir = "src"
+
+options = "--total"
+
+modules
+  = Term
+  , Thinning
diff --git a/src/Term.idr b/src/Term.idr
new file mode 100644
index 0000000..a21f50a
--- /dev/null
+++ b/src/Term.idr
@@ -0,0 +1,83 @@
+module Term
+
+import Data.SnocList
+import Data.SnocList.Elem
+import Data.SnocList.Quantifiers
+import Thinning
+
+infixr 20 ~>
+
+-- Types -----------------------------------------------------------------------
+
+data Ty : Type where
+  N : Ty
+  (~>) : Ty -> Ty -> Ty
+
+%name Ty ty
+
+-- Terms -----------------------------------------------------------------------
+
+data Term : SnocList Ty -> Ty -> Type
+data Subst : SnocList Ty -> SnocList Ty -> Type
+
+data Term where
+  Var : (i : Elem ty ctx) -> Term ctx ty
+  Abs : Term (ctx :< ty) ty' -> Term ctx (ty ~> ty')
+  App : Term ctx (ty ~> ty') -> Term ctx ty -> Term ctx ty'
+  Zero : Term ctx N
+  Succ : Term ctx N -> Term ctx N
+  Rec : Term ctx N -> Term ctx ty -> Term (ctx :< ty) ty -> Term ctx ty
+  Sub : Term ctx ty -> Subst ctx' ctx -> Term ctx' ty
+
+data Subst where
+  Base : ctx' `Thins` ctx -> Subst ctx ctx'
+  (:<) : Subst ctx ctx' -> Term ctx ty -> Subst ctx (ctx' :< ty)
+
+%name Term t, u, v
+%name Subst sub
+
+shift : Subst ctx ctx' -> Subst (ctx :< ty) ctx'
+shift (Base thin) = Base (Drop thin)
+shift (sub :< t) = shift sub :< Sub t (Base (Drop Id))
+
+lift : Subst ctx ctx' -> Subst (ctx :< ty) (ctx' :< ty)
+lift (Base thin) = Base (keep thin)
+lift (sub :< t) = shift (sub :< t) :< Var Here
+
+indexSubst : Subst ctx' ctx -> Elem ty ctx -> Term ctx' ty
+indexSubst (Base thin) i = Var (index thin i)
+indexSubst (sub :< t) Here = t
+indexSubst (sub :< t) (There i) = indexSubst sub i
+
+restrict : Subst ctx1 ctx2 -> ctx3 `Thins` ctx2 -> Subst ctx1 ctx3
+restrict (Base thin') thin = Base (thin' . thin)
+restrict (sub :< t) Id = sub :< t
+restrict (sub :< t) (Drop thin) = restrict sub thin
+restrict (sub :< t) (Keep thin) = restrict sub thin :< t
+
+(.) : Subst ctx1 ctx2 -> Subst ctx2 ctx3 -> Subst ctx1 ctx3
+sub2 . Base thin = restrict sub2 thin
+sub2 . (sub1 :< t) = sub2 . sub1 :< Sub t sub2
+
+-- Equivalence -----------------------------------------------------------------
+
+data Equiv : Term ctx ty -> Term ctx ty -> Type
+
+data Equiv where
+  Refl : Equiv t t
+  Sym : Equiv t u -> Equiv u t
+  Trans : Equiv t u -> Equiv u v -> Equiv t v
+  AbsCong : Equiv t u -> Equiv (Abs t) (Abs u)
+  AppCong : Equiv t1 t2 -> Equiv u1 u2 -> Equiv (App t1 u1) (App t2 u2)
+  SuccCong : Equiv t u -> Equiv (Succ t) (Succ u)
+  RecCong : Equiv t1 t2 -> Equiv u1 u2 -> Equiv v1 v2 -> Equiv (Rec t1 u1 v1) (Rec t2 u2 v2)
+  PiBeta : Equiv (App (Abs t) u) (Sub t (Base Id :< u))
+  NatBetaZ : Equiv (Rec Zero t u) t
+  NatBetaS : Equiv (Rec (Succ t) u v) (Sub v (Base Id :< Rec t u v))
+  SubVar : Equiv (Sub (Var i) sub) (indexSubst sub i)
+  SubAbs : Equiv (Sub (Abs t) sub) (Abs (Sub t $ lift sub))
+  SubApp : Equiv (Sub (App t u) sub) (App (Sub t sub) (Sub u sub))
+  SubZero : Equiv (Sub Zero sub) Zero
+  SubSucc : Equiv (Sub (Succ t) sub) (Succ (Sub t sub))
+  SubRec : Equiv (Sub (Rec t u v) sub) (Rec (Sub t sub) (Sub u sub) (Sub v $ lift sub))
+  SubSub : Equiv (Sub (Sub t sub1) sub2) (Sub t (sub2 . sub1))
diff --git a/src/Thinning.idr b/src/Thinning.idr
new file mode 100644
index 0000000..9de57fb
--- /dev/null
+++ b/src/Thinning.idr
@@ -0,0 +1,60 @@
+module Thinning
+
+import Data.SnocList.Elem
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Thins : SnocList a -> SnocList a -> Type
+public export
+data NotId : Thins sx sy -> Type
+
+data Thins where
+  Id : sx `Thins` sx
+  Drop : sx `Thins` sy -> sx `Thins` sy :< z
+  Keep :
+    (thin : sx `Thins` sy) ->
+    {auto 0 prf : NotId thin} ->
+    sx :< z `Thins` sy :< z
+
+data NotId where
+  DropNotId : NotId (Drop thin)
+  KeepNotId : (0 prf : NotId thin) -> NotId (Keep thin)
+
+%name Thins thin
+
+-- Smart Constructors ----------------------------------------------------------
+
+export
+keep : sx `Thins` sy -> sx :< z `Thins` sy :< z
+keep Id = Id
+keep (Drop thin) = Keep (Drop thin)
+keep (Keep thin) = Keep (Keep thin)
+
+-- Operations ------------------------------------------------------------------
+
+export
+index : sx `Thins` sy -> Elem z sx -> Elem z sy
+index Id i = i
+index (Drop thin) i = There (index thin i)
+index (Keep thin) Here = Here
+index (Keep thin) (There i) = There (index thin i)
+
+export
+(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz
+compNotId :
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
+  {auto 0 _ : NotId thin2} ->
+  {auto 0 _ : NotId thin1} ->
+  NotId (thin2 . thin1)
+
+Id . thin1 = thin1
+(Drop thin2) . thin1 = Drop (thin2 . thin1)
+(Keep thin2) . Id = Keep thin2
+(Keep thin2) . (Drop thin1) = Drop (thin2 . thin1)
+(Keep thin2) . (Keep thin1) = Keep {prf = compNotId thin2 thin1} (thin2 . thin1)
+
+compNotId (Drop thin2) thin1 = DropNotId
+compNotId (Keep thin2) (Drop thin1) = DropNotId
+compNotId (Keep thin2) (Keep thin1) = KeepNotId (compNotId thin2 thin1)