Make normal forms a property.

Weakening is now part of eval.

3 files changed, 107 insertions, 74 deletions

diff --git a/src/Level0.idr b/src/Level0.idr
index 3c71111..bbe141f 100644
--- a/src/Level0.idr
+++ b/src/Level0.idr
@@ -19,64 +19,105 @@ Applicative Cont where
 Monad Cont where
   join (Then f) = Then (\k => f (\c => runCont c k))
 
-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)
+data IsNormSubst : Subst ctx ctx' -> Type where
+  Base : IsNormSubst (Base thin)
+  (:<) : IsNormSubst sub -> IsNormal t -> IsNormSubst (sub :< t)
 
-%name NormSubst sub
+%name IsNormSubst prf
+
+record NormSubst (ctx, ctx' : SnocList Ty) where
+  constructor MkNormSubst
+  forget : Subst ctx ctx'
+  0 isNormSubst : IsNormSubst forget
 
-shift : NormSubst ctx ctx' -> NormSubst (ctx :< ty) ctx'
-shift (Base thin) = Base (Drop thin)
-shift (sub :< t) = shift sub :< wknNorm t (Drop Id)
+%name NormSubst sub
 
-lift : NormSubst ctx ctx' -> NormSubst (ctx :< ty) (ctx' :< ty)
-lift (Base thin) = Base (keep thin)
-lift (sub :< t) = shift (sub :< t) :< Ntrl (Var Here)
+indexNormal : IsNormSubst sub -> (i : Elem ty ctx) -> IsNormal (index sub i)
+indexNormal Base i = Ntrl Var
+indexNormal (sub :< t) Here = t
+indexNormal (sub :< t) (There i) = indexNormal sub i
 
 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
+index sub i = MkNormal (index (forget sub) i) (indexNormal (isNormSubst sub) i)
+
+restrictNormal : IsNormSubst sub -> (thin : ctx3 `Thins` ctx2) -> IsNormSubst (restrict sub thin)
+restrictNormal Base thin = Base
+restrictNormal (sub :< t) Id = sub :< t
+restrictNormal (sub :< t) (Drop thin) = restrictNormal sub thin
+restrictNormal (sub :< t) (Keep thin) = restrictNormal sub thin :< t
 
 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
+restrict sub thin =
+  MkNormSubst
+    (restrict (forget sub) thin)
+    (restrictNormal (isNormSubst sub) thin)
 
 data Case : Type -> Type where
-  Eval : Term ctx ty -> NormSubst ctx' ctx -> Case (Normal ctx' ty)
-  EvalSub : Subst ctx' ctx -> NormSubst ctx'' ctx' -> Case (NormSubst ctx'' ctx)
-  App : Normal ctx (ty ~> ty') -> Normal ctx ty -> Case (Normal ctx ty')
-  Rec : Normal ctx N -> Normal ctx ty -> Normal (ctx :< ty) ty -> Case (Normal ctx ty)
+  Eval :
+    Term ctx ty ->
+    NormSubst ctx' ctx ->
+    Case (Normal ctx' ty)
+  EvalSub :
+    Subst ctx' ctx ->
+    NormSubst ctx'' ctx' ->
+    Case (NormSubst ctx'' ctx)
+  App :
+    Normal ctx (ty ~> ty') ->
+    Normal ctx ty ->
+    Case (Normal ctx ty')
+  Rec :
+    Normal ctx N ->
+    Normal ctx ty ->
+    Normal (ctx :< ty) ty ->
+    Case (Normal ctx ty)
 
 partial
 eval : Case ret -> Cont (ret)
 eval (Eval (Var i) sub) = pure (index sub i)
-eval (Eval (Abs t) sub) = [| Abs (eval (Eval t (lift sub))) |]
+eval (Eval (Abs t) sub) = do
+  sub <- eval (EvalSub (forget sub) (MkNormSubst (Base $ Drop Id) Base))
+  let sub = MkNormSubst (forget sub :< Var Here) (isNormSubst sub :< Ntrl Var)
+  t <- eval (Eval t sub)
+  pure (MkNormal (Abs $ forget t) (Abs $ isNormal t))
 eval (Eval (App t u) sub) = do
   t <- eval (Eval t sub)
   u <- eval (Eval u sub)
   eval (App t u)
-eval (Eval (Zero) sub) = pure Zero
-eval (Eval (Succ t) sub) = [| Succ (eval (Eval t sub)) |]
+eval (Eval (Zero) sub) = pure (MkNormal Zero Zero)
+eval (Eval (Succ t) sub) = {forget $= Succ, isNormal $= Succ} <$> eval (Eval t sub)
 eval (Eval (Rec t u v) sub) = do
   t <- eval (Eval t sub)
   u <- eval (Eval u sub)
-  v <- eval (Eval v (lift sub))
+  sub <- eval (EvalSub (forget sub) (MkNormSubst (Base $ Drop Id) Base))
+  let sub = MkNormSubst (forget sub :< Var Here) (isNormSubst sub :< Ntrl Var)
+  v <- eval (Eval v sub)
   eval (Rec t u v)
 eval (Eval (Sub t sub') sub) = do
   sub' <- eval (EvalSub sub' sub)
   eval (Eval t sub')
 eval (EvalSub (Base thin) sub') = pure (restrict sub' thin)
 eval (EvalSub (sub :< t) sub') =
-  [| eval (EvalSub sub sub') :< eval (Eval t sub') |]
-eval (App (Abs t) u) =
-  eval (Eval (forgetNorm t) (Base Id :< u))
-eval (App (Ntrl t) u) = pure (Ntrl $ App t u)
-eval (Rec (Zero) u v) = pure u
-eval (Rec (Succ t) u v) = do
-  val <- eval (Rec t u v)
-  eval (Eval (forgetNorm v) (Base Id :< val))
-eval (Rec (Ntrl t) u v) = pure (Ntrl $ Rec t u v)
+  pure (\sub, t => MkNormSubst (forget sub :< forget t) (isNormSubst sub :< isNormal t)) <*>
+  eval (EvalSub sub sub') <*>
+  eval (Eval t sub')
+eval (App (MkNormal (Abs t) prf) u) =
+  eval (Eval t (MkNormSubst (Base Id :< forget u) (Base :< isNormal u)))
+eval (App (MkNormal t@(Var _) prf) u) =
+  pure (MkNormal (App t (forget u)) (Ntrl $ App Var (isNormal u)))
+eval (App (MkNormal t@(App _ _) prf) u) =
+  pure (MkNormal (App t (forget u)) (Ntrl $ App (appNtrl prf) (isNormal u)))
+eval (App (MkNormal t@(Rec _ _ _) prf) u) =
+  pure (MkNormal (App t (forget u)) (Ntrl $ App (recNtrl prf) (isNormal u)))
+eval (Rec (MkNormal Zero prf) u v) = pure u
+eval (Rec (MkNormal (Succ t) prf) u v) = do
+  val <- eval (Rec (MkNormal t (predNorm prf)) u v)
+  eval (Eval (forget v) (MkNormSubst (Base Id :< forget val) (Base :< isNormal val)))
+eval (Rec (MkNormal t@(Var _) prf) u v) =
+  pure $
+  MkNormal (Rec t (forget u) (forget v)) (Ntrl $ Rec Var (isNormal u) (isNormal v))
+eval (Rec (MkNormal t@(App _ _) prf) u v) =
+  pure $
+  MkNormal (Rec t (forget u) (forget v)) (Ntrl $ Rec (appNtrl prf) (isNormal u) (isNormal v))
+eval (Rec (MkNormal t@(Rec _ _ _) prf) u v) =
+  pure $
+  MkNormal (Rec t (forget u) (forget v)) (Ntrl $ Rec (recNtrl prf) (isNormal u) (isNormal v))
diff --git a/src/NormalForm.idr b/src/NormalForm.idr
index 64b6a27..f4697f5 100644
--- a/src/NormalForm.idr
+++ b/src/NormalForm.idr
@@ -7,52 +7,42 @@ import Thinning
 -- Neutrals and Normals --------------------------------------------------------
 
 public export
-data Neutral : SnocList Ty -> Ty -> Type
+data IsNeutral : Term ctx ty -> Type
 public export
-data Normal : SnocList Ty -> Ty -> Type
+data IsNormal : Term ctx 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 IsNeutral where
+  Var : IsNeutral (Var i)
+  App : IsNeutral t -> IsNormal u -> IsNeutral (App t u)
+  Rec : IsNeutral t -> IsNormal u -> IsNormal v -> IsNeutral (Rec t u v)
 
-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
+data IsNormal where
+  Ntrl : IsNeutral t -> IsNormal t
+  Abs : IsNormal t -> IsNormal (Abs t)
+  Zero : IsNormal Zero
+  Succ : IsNormal t -> IsNormal (Succ t)
 
-%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
+%name IsNeutral prf
+%name IsNormal prf
 
-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)
+public export
+record Normal (ctx : SnocList Ty) (ty : Ty) where
+  constructor MkNormal
+  forget : Term ctx ty
+  0 isNormal : IsNormal forget
 
-forgetNorm (Ntrl n) = forgetNtrl n
-forgetNorm (Abs n) = Abs (forgetNorm n)
-forgetNorm Zero = Zero
-forgetNorm (Succ n) = Succ (forgetNorm n)
+%name Normal n, m, k
 
--- Weakening -------------------------------------------------------------------
+-- Inversions ------------------------------------------------------------------
 
 export
-wknNtrl : Neutral ctx ty -> ctx `Thins` ctx' -> Neutral ctx' ty
-export
-wknNorm : Normal ctx ty -> ctx `Thins` ctx' -> Normal ctx' ty
+predNorm : IsNormal (Succ t) -> IsNormal t
+predNorm (Succ prf) = prf
 
-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)
+export
+appNtrl : IsNormal (App t u) -> IsNeutral (App t u)
+appNtrl (Ntrl prf) = prf
 
-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)
+export
+recNtrl : IsNormal (Rec t u v) -> IsNeutral (Rec t u v)
+recNtrl (Ntrl prf) = prf
diff --git a/src/Term.idr b/src/Term.idr
index e6cf25c..fde8d9f 100644
--- a/src/Term.idr
+++ b/src/Term.idr
@@ -46,18 +46,20 @@ lift : Subst ctx ctx' -> Subst (ctx :< ty) (ctx' :< ty)
 lift (Base thin) = Base (keep thin)
 lift (sub :< t) = shift (sub :< t) :< Var Here
 
-export
+public 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
 
+public export
 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
 
+export
 (.) : Subst ctx1 ctx2 -> Subst ctx2 ctx3 -> Subst ctx1 ctx3
 sub2 . Base thin = restrict sub2 thin
 sub2 . (sub1 :< t) = sub2 . sub1 :< Sub t sub2