Define a partial evaluator inductively.

4 files changed, 145 insertions, 11 deletions

diff --git a/church-eval.ipkg b/church-eval.ipkg
index eeb9b67..4d4cb31 100644
--- a/church-eval.ipkg
+++ b/church-eval.ipkg
@@ -5,5 +5,7 @@ sourcedir = "src"
 options = "--total"
 
 modules
-  = Term
+  = Level0
+  , NormalForm
+  , Term
   , Thinning
diff --git a/src/Level0.idr b/src/Level0.idr
new file mode 100644
index 0000000..bccaa4f
--- /dev/null
+++ b/src/Level0.idr
@@ -0,0 +1,72 @@
+module Level0
+
+import Data.SnocList.Elem
+import NormalForm
+import Term
+import Thinning
+
+Res : Type -> Type
+Res = Pair ()
+
+public export
+data NormSubst : SnocList Ty -> SnocList Ty -> Type where
+  Base : ctx' `Thins` ctx -> NormSubst ctx ctx'
+  (:<) : NormSubst ctx ctx' -> Normal ctx ty -> NormSubst ctx (ctx' :< ty)
+
+%name NormSubst sub
+
+shift : NormSubst ctx ctx' -> NormSubst (ctx :< ty) ctx'
+shift (Base thin) = Base (Drop thin)
+shift (sub :< t) = shift sub :< wknNorm t (Drop Id)
+
+lift : NormSubst ctx ctx' -> NormSubst (ctx :< ty) (ctx' :< ty)
+lift (Base thin) = Base (keep thin)
+lift (sub :< t) = shift (sub :< t) :< Ntrl (Var Here)
+
+index : NormSubst ctx' ctx -> Elem ty ctx -> Normal ctx' ty
+index (Base thin) i = Ntrl (Var $ index thin i)
+index (sub :< t) Here = t
+index (sub :< t) (There i) = index sub i
+
+restrict : NormSubst ctx1 ctx2 -> ctx3 `Thins` ctx2 -> NormSubst 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
+
+-- Evaluates a term in a context of normal forms.
+partial
+eval : Term ctx ty -> NormSubst ctx' ctx -> Res (Normal ctx' ty)
+partial
+evalSub : Subst ctx ctx'' -> NormSubst ctx' ctx -> Res (NormSubst ctx' ctx'')
+partial
+rec : Normal ctx N -> Normal ctx ty -> Normal (ctx :< ty) ty -> Res (Normal ctx ty)
+
+eval (Var i) sub = pure (index sub i)
+eval (Abs t) sub = [| Abs (eval t $ lift sub) |]
+eval (App t u) sub = do
+  t <- eval t sub
+  case t of
+    Abs t => do
+      u <- eval u sub
+      eval (forgetNorm t) (Base Id :< u)
+    Ntrl t => Ntrl <$> App t <$> eval u sub
+eval Zero sub = pure Zero
+eval (Succ t) sub = [| Succ (eval t sub) |]
+eval (Rec t u v) sub = do
+  t <- eval t sub
+  u <- eval u sub
+  v <- eval v (lift sub)
+  rec t u v
+eval (Sub t sub') sub = do
+  sub' <- evalSub sub' sub
+  eval t sub'
+
+evalSub (Base thin) sub' = pure (restrict sub' thin)
+evalSub (sub :< t) sub' = [| evalSub sub sub' :< eval t sub' |]
+
+rec Zero u v = pure u
+rec (Succ t) u v = do
+  val <- rec t u v
+  eval (forgetNorm v) (Base Id :< val)
+rec (Ntrl t) u v = pure (Ntrl $ Rec t u v)
diff --git a/src/NormalForm.idr b/src/NormalForm.idr
new file mode 100644
index 0000000..64b6a27
--- /dev/null
+++ b/src/NormalForm.idr
@@ -0,0 +1,58 @@
+module NormalForm
+
+import Data.SnocList.Elem
+import Term
+import Thinning
+
+-- Neutrals and Normals --------------------------------------------------------
+
+public export
+data Neutral : SnocList Ty -> Ty -> Type
+public export
+data Normal : SnocList Ty -> Ty -> Type
+
+data Neutral where
+  Var : (i : Elem ty ctx) -> Neutral ctx ty
+  App : Neutral ctx (ty ~> ty') -> Normal ctx ty -> Neutral ctx ty'
+  Rec : Neutral ctx N -> Normal ctx ty -> Normal (ctx :< ty) ty -> Neutral ctx ty
+
+data Normal where
+  Ntrl : Neutral ctx ty -> Normal ctx ty
+  Abs : Normal (ctx :< ty) ty' -> Normal ctx (ty ~> ty')
+  Zero : Normal ctx N
+  Succ : Normal ctx N -> Normal ctx N
+
+%name Neutral n, m, k
+%name Normal n, m, k
+
+-- Forgetting ------------------------------------------------------------------
+
+export
+forgetNtrl : Neutral ctx ty -> Term ctx ty
+export
+forgetNorm : Normal ctx ty -> Term ctx ty
+
+forgetNtrl (Var i) = Var i
+forgetNtrl (App n m) = App (forgetNtrl n) (forgetNorm m)
+forgetNtrl (Rec n m k) = Rec (forgetNtrl n) (forgetNorm m) (forgetNorm k)
+
+forgetNorm (Ntrl n) = forgetNtrl n
+forgetNorm (Abs n) = Abs (forgetNorm n)
+forgetNorm Zero = Zero
+forgetNorm (Succ n) = Succ (forgetNorm n)
+
+-- Weakening -------------------------------------------------------------------
+
+export
+wknNtrl : Neutral ctx ty -> ctx `Thins` ctx' -> Neutral ctx' ty
+export
+wknNorm : Normal ctx ty -> ctx `Thins` ctx' -> Normal ctx' ty
+
+wknNtrl (Var i) thin = Var (index thin i)
+wknNtrl (App n m) thin = App (wknNtrl n thin) (wknNorm m thin)
+wknNtrl (Rec n m k) thin = Rec (wknNtrl n thin) (wknNorm m thin) (wknNorm k $ keep thin)
+
+wknNorm (Ntrl n) thin = Ntrl (wknNtrl n thin)
+wknNorm (Abs n) thin = Abs (wknNorm n $ keep thin)
+wknNorm Zero thin = Zero
+wknNorm (Succ n) thin = Succ (wknNorm n thin)
diff --git a/src/Term.idr b/src/Term.idr
index a21f50a..e6cf25c 100644
--- a/src/Term.idr
+++ b/src/Term.idr
@@ -1,14 +1,13 @@
 module Term
 
-import Data.SnocList
 import Data.SnocList.Elem
-import Data.SnocList.Quantifiers
 import Thinning
 
 infixr 20 ~>
 
 -- Types -----------------------------------------------------------------------
 
+public export
 data Ty : Type where
   N : Ty
   (~>) : Ty -> Ty -> Ty
@@ -17,7 +16,9 @@ data Ty : Type where
 
 -- Terms -----------------------------------------------------------------------
 
+public export
 data Term : SnocList Ty -> Ty -> Type
+public export
 data Subst : SnocList Ty -> SnocList Ty -> Type
 
 data Term where
@@ -40,14 +41,16 @@ shift : Subst ctx ctx' -> Subst (ctx :< ty) ctx'
 shift (Base thin) = Base (Drop thin)
 shift (sub :< t) = shift sub :< Sub t (Base (Drop Id))
 
+export
 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
+export
+index : Subst 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
 
 restrict : Subst ctx1 ctx2 -> ctx3 `Thins` ctx2 -> Subst ctx1 ctx3
 restrict (Base thin') thin = Base (thin' . thin)
@@ -61,9 +64,8 @@ sub2 . (sub1 :< t) = sub2 . sub1 :< Sub t sub2
 
 -- Equivalence -----------------------------------------------------------------
 
-data Equiv : Term ctx ty -> Term ctx ty -> Type
-
-data Equiv where
+public export
+data Equiv : Term ctx ty -> Term ctx ty -> Type where
   Refl : Equiv t t
   Sym : Equiv t u -> Equiv u t
   Trans : Equiv t u -> Equiv u v -> Equiv t v
@@ -74,7 +76,7 @@ data Equiv where
   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)
+  SubVar : Equiv (Sub (Var i) sub) (index 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