Make normal forms a property.

Weakening is now part of eval.

1 files changed, 28 insertions, 38 deletions

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