Define terms with substitution as an operation.

4 files changed, 168 insertions, 0 deletions

diff --git a/church-eval.ipkg b/church-eval.ipkg
index 3ac853c..21fe018 100644
--- a/church-eval.ipkg
+++ b/church-eval.ipkg
@@ -10,3 +10,6 @@ modules
   , NormalForm
   , Term
   , Thinning
+  , Total.NormalForm
+  , Total.Reduction
+  , Total.Term
diff --git a/src/Total/NormalForm.idr b/src/Total/NormalForm.idr
new file mode 100644
index 0000000..7421ca9
--- /dev/null
+++ b/src/Total/NormalForm.idr
@@ -0,0 +1,31 @@
+module Total.NormalForm
+
+import Total.Reduction
+import Total.Term
+
+public export
+data Neutral : Term ctx ty -> Type
+public export
+data Normal : Term ctx ty -> Type
+
+data Neutral where
+  Var : Neutral (Var i)
+  App : Neutral t -> Normal u -> Neutral (App t u)
+  Rec : Neutral t -> Normal u -> Normal v -> Neutral (Rec t u v)
+
+data Normal where
+  Ntrl : Neutral t -> Normal t
+  Abs : Normal t -> Normal (Abs t)
+  Zero : Normal Zero
+  Suc : Normal t -> Normal (Suc t)
+
+%name Neutral n, m, k
+%name Normal n, m, k
+
+record NormalForm (0 t : Term ctx ty) where
+  constructor MkNf
+  term : Term ctx ty
+  0 steps : t >= term
+  0 normal : Normal term
+
+%name NormalForm nf
diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr
new file mode 100644
index 0000000..efa6f74
--- /dev/null
+++ b/src/Total/Reduction.idr
@@ -0,0 +1,65 @@
+module Total.Reduction
+
+import Total.Term
+
+public export
+data (>) : Term ctx ty -> Term ctx ty -> Type where
+  AbsCong : t > u -> Abs t > Abs u
+  AppCong1 : t > u -> App t v > App u v
+  AppCong2 : u > v -> App t u > App t v
+  AppBeta : App (Abs t) u > subst t (Base Id :< u)
+  SucCong : t > u -> Suc t > Suc u
+  RecCong1 : t1 > t2 -> Rec t1 u v > Rec t2 u v
+  RecCong2 : u1 > u2 -> Rec t u1 v > Rec t u2 v
+  RecCong3 : v1 > v2 -> Rec t u v1 > Rec t u v2
+  RecZero : Rec Zero u v > u
+  RecSuc : Rec (Suc t) u v > App v (Rec t u v)
+
+%name Reduction.(>) step
+
+public export
+data (>=) : Term ctx ty -> Term ctx ty -> Type where
+  Lin : t >= t
+  (:<) : t >= u -> u > v -> t >= v
+
+%name Reduction.(>=) steps
+
+export
+(++) : t >= u -> u >= v -> t >= v
+steps ++ [<] = steps
+steps ++ steps' :< step = (steps ++ steps') :< step
+
+export
+AbsCong' : t >= u -> Abs t >= Abs u
+AbsCong' [<] = [<]
+AbsCong' (steps :< step) = AbsCong' steps :< AbsCong step
+
+export
+AppCong1' : t >= u -> App t v >= App u v
+AppCong1' [<] = [<]
+AppCong1' (steps :< step) = AppCong1' steps :< AppCong1 step
+
+export
+AppCong2' : u >= v -> App t u >= App t v
+AppCong2' [<] = [<]
+AppCong2' (steps :< step) = AppCong2' steps :< AppCong2 step
+
+export
+SucCong' : t >= u -> Suc t >= Suc u
+SucCong' [<] = [<]
+SucCong' (steps :< step) = SucCong' steps :< SucCong step
+
+export
+RecCong1' : t1 >= t2 -> Rec t1 u v >= Rec t2 u v
+RecCong1' [<] = [<]
+RecCong1' (steps :< step) = RecCong1' steps :< RecCong1 step
+
+export
+RecCong2' : u1 >= u2 -> Rec t u1 v >= Rec t u2 v
+RecCong2' [<] = [<]
+RecCong2' (steps :< step) = RecCong2' steps :< RecCong2 step
+
+export
+RecCong3' : v1 >= v2 -> Rec t u v1 >= Rec t u v2
+RecCong3' [<] = [<]
+RecCong3' (steps :< step) = RecCong3' steps :< RecCong3 step
diff --git a/src/Total/Term.idr b/src/Total/Term.idr
new file mode 100644
index 0000000..22a9a39
--- /dev/null
+++ b/src/Total/Term.idr
@@ -0,0 +1,69 @@
+module Total.Term
+
+import public Data.SnocList.Elem
+import public Thinning
+
+%prefix_record_projections off
+
+infixr 10 ~>
+
+public export
+data Ty : Type where
+  N : Ty
+  (~>) : Ty -> Ty -> Ty
+
+%name Ty ty
+
+public export
+data Term : SnocList Ty -> Ty -> Type where
+  Var : (i : Elem ty ctx) -> Term ctx ty
+  Abs : Term (ctx :< ty) ty' -> Term ctx (ty ~> ty')
+  App : {ty : Ty} -> Term ctx (ty ~> ty') -> Term ctx ty -> Term ctx ty'
+  Zero : Term ctx N
+  Suc : Term ctx N -> Term ctx N
+  Rec : Term ctx N -> Term ctx ty -> Term ctx (ty ~> ty) -> Term ctx ty
+
+%name Term t, u, v
+
+wkn : Term ctx ty -> ctx `Thins` ctx' -> Term ctx' ty
+wkn (Var i) thin = Var (index thin i)
+wkn (Abs t) thin = Abs (wkn t $ keep thin)
+wkn (App t u) thin = App (wkn t thin) (wkn u thin)
+wkn Zero thin = Zero
+wkn (Suc t) thin = Suc (wkn t thin)
+wkn (Rec t u v) thin = Rec (wkn t thin) (wkn u thin) (wkn v thin)
+
+public export
+data Terms : SnocList Ty -> SnocList Ty -> Type where
+  Base : ctx `Thins` ctx' -> Terms ctx' ctx
+  (:<) : Terms ctx' ctx -> Term ctx' ty -> Terms ctx' (ctx :< ty)
+
+%name Terms sub
+
+index : Terms ctx' ctx -> Elem ty ctx -> Term ctx' ty
+index (Base thin) i = Var (index thin i)
+index (sub :< t) Here = t
+index (sub :< t) (There i) = index sub i
+
+wknAll : Terms ctx' ctx -> ctx' `Thins` ctx'' -> Terms ctx'' ctx
+wknAll (Base thin') thin = Base (thin . thin')
+wknAll (sub :< t) thin = wknAll sub thin :< wkn t thin
+
+export
+subst : Term ctx ty -> Terms ctx' ctx -> Term ctx' ty
+subst (Var i) sub = index sub i
+subst (Abs t) sub = Abs (subst t $ wknAll sub (Drop Id) :< Var Here)
+subst (App t u) sub = App (subst t sub) (subst u sub)
+subst Zero sub = Zero
+subst (Suc t) sub = Suc (subst t sub)
+subst (Rec t u v) sub = Rec (subst t sub) (subst u sub) (subst v sub)
+
+restrict : Terms ctx'' ctx' -> ctx `Thins` ctx' -> Terms ctx'' ctx
+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
+
+(.) : Terms ctx'' ctx' -> Terms ctx' ctx -> Terms ctx'' ctx
+sub2 . (Base thin) = restrict sub2 thin
+sub2 . (sub1 :< t) = sub2 . sub1 :< subst t sub2