Define normal form.

2 files changed, 157 insertions, 0 deletions

diff --git a/obs.ipkg b/obs.ipkg
index 1ae6e84..e178c88 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -10,6 +10,7 @@ main = Obs.Main
 modules
   = Obs.Abstract
   , Obs.Main
+  , Obs.NormalForm
   , Obs.Parser
   , Obs.Sort
   , Obs.Substitution
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
new file mode 100644
index 0000000..c11c158
--- /dev/null
+++ b/src/Obs/NormalForm.idr
@@ -0,0 +1,156 @@
+module Obs.NormalForm
+
+import Data.Fin
+
+import Obs.Sort
+import Obs.Substitution
+
+import Text.PrettyPrint.Prettyprinter
+
+-- Definition ------------------------------------------------------------------
+
+data Constructor : Nat -> Type
+data Neutral     : Nat -> Type
+data NormalForm  : Nat -> Type
+
+public export
+data Constructor : Nat -> Type where
+  Sort : Sort -> Constructor n
+
+public export
+data Neutral : Nat -> Type where
+  Var : Fin n -> Neutral n
+
+public export
+data NormalForm : Nat -> Type where
+  Ntrl  : Neutral n -> NormalForm n
+  Cnstr : Constructor n -> NormalForm n
+
+public export
+record Definition (n : Nat) where
+  constructor MkDefinition
+  name   : Maybe String
+  sort   : Sort
+  ty     : NormalForm n
+  tm     : NormalForm n
+
+public export
+data Context : Nat -> Type where
+  Nil  : Context 0
+  (:<) : Context n -> Definition n -> Context (S n)
+
+-- Interfaces ------------------------------------------------------------------
+
+-- Naive equality tests
+eqCnstr : Constructor n -> Constructor n -> Bool
+eqNtrl  : Neutral n -> Neutral n -> Bool
+eqWhnf  : NormalForm n -> NormalForm n -> Bool
+
+eqCnstr (Sort s) (Sort s') = s == s'
+
+eqNtrl (Var i) (Var j) = i == j
+
+eqWhnf (Ntrl t)  (Ntrl u)  = eqNtrl t u
+eqWhnf (Cnstr t) (Cnstr u) = eqCnstr t u
+eqWhnf _ _ = False
+
+export
+Eq (Constructor n) where
+  t == u = eqCnstr t u
+
+export
+Eq (Neutral n) where
+  t == u = eqNtrl t u
+
+export
+Eq (NormalForm n) where
+  t == u = eqWhnf t u
+
+-- Pretty Print ----------------------------------------------------------------
+
+prettyPrecCnstr : Prec -> Constructor n -> Doc ann
+prettyPrecNtrl  : Prec -> Neutral n -> Doc ann
+prettyPrecWhnf  : Prec -> NormalForm n -> Doc ann
+
+prettyPrecCnstr d (Sort s) = prettyPrec d s
+
+prettyPrecNtrl d (Var i) = pretty "$\{show i}"
+
+prettyPrecWhnf d (Ntrl t)  = prettyPrecNtrl d t
+prettyPrecWhnf d (Cnstr t) = prettyPrecCnstr d t
+
+export
+Pretty (Constructor n) where
+  prettyPrec = prettyPrecCnstr
+
+export
+Pretty (Neutral n) where
+  prettyPrec = prettyPrecNtrl
+
+export
+Pretty (NormalForm n) where
+  prettyPrec = prettyPrecWhnf
+
+export
+Pretty (Definition n) where
+  pretty def = group $
+    pretty def.name <++> colon <+> softline <+> pretty def.ty <+> softline <+> colon <++> pretty def.sort <+> hardline <+>
+    pretty def.name <++> equals <+> softline <+> pretty def.tm
+
+export
+Pretty (Context n) where
+  pretty []           = neutral
+  pretty ([] :< def)  = pretty def
+  pretty (ctx :< def) = pretty ctx <+> hardline <+> hardline <+> pretty def
+
+-- Operations ------------------------------------------------------------------
+
+-- Renaming
+
+renameCnstr : Constructor n -> (Fin n -> Fin m) -> Constructor m
+renameNtrl  : Neutral n -> (Fin n -> Fin m) -> Neutral m
+renameWhnf  : NormalForm n -> (Fin n -> Fin m) -> NormalForm m
+
+renameCnstr (Sort s) f = Sort s
+
+renameNtrl (Var i) f = Var (f i)
+
+renameWhnf (Ntrl t)  f = Ntrl $ renameNtrl t f
+renameWhnf (Cnstr t) f = Cnstr $ renameCnstr t f
+
+export
+Rename Constructor where
+  rename = renameCnstr
+
+export
+Rename Neutral where
+  rename = renameNtrl
+
+export
+Rename NormalForm where
+  rename = renameWhnf
+
+-- Substitution
+
+substCnstr : Constructor n -> (Fin n -> NormalForm m) -> Constructor m
+substNtrl  : Neutral n -> (Fin n -> NormalForm m) -> NormalForm m
+substWhnf  : NormalForm n -> (Fin n -> NormalForm m) -> NormalForm m
+
+substCnstr (Sort s) f = Sort s
+
+substNtrl (Var i) f = f i
+
+substWhnf (Ntrl t)  f = substNtrl t f
+substWhnf (Cnstr t) f = Cnstr $ substCnstr t f
+
+export
+Subst Constructor NormalForm Constructor where
+  subst = substCnstr
+
+export
+Subst Neutral NormalForm NormalForm where
+  subst = substNtrl
+
+export
+Subst NormalForm NormalForm NormalForm where
+  subst = substWhnf