1 files changed, 17 insertions, 15 deletions
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index 8ee3b19..a15c3c1 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -18,14 +18,14 @@ data NormalForm  : Nat -> Type
 public export
 data Constructor : Nat -> Type where
   Sort   : Sort -> Constructor n
-  Pi     : Sort -> Sort -> NormalForm n -> NormalForm (S n) -> Constructor n
-  Lambda : NormalForm (S n) -> Constructor n
+  Pi     : Sort -> Sort -> String -> NormalForm n -> NormalForm (S n) -> Constructor n
+  Lambda : String -> NormalForm (S n) -> Constructor n
   Top    : Constructor n
   Bottom : Constructor n
 
 public export
 data Neutral : Nat -> Type where
-  Var    : Fin n -> Neutral n
+  Var    : String -> Fin n -> Neutral n
   App    : Neutral n -> NormalForm n -> Neutral n
   Absurd : Neutral n
 
@@ -56,13 +56,13 @@ eqNtrl  : Neutral n -> Neutral n -> Bool
 eqWhnf  : NormalForm n -> NormalForm n -> Bool
 
 eqCnstr (Sort s) (Sort s') = s == s'
-eqCnstr (Pi s s' a b) (Pi l l' a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
-eqCnstr (Lambda t) (Lambda u) = eqWhnf t u
+eqCnstr (Pi s s' _ a b) (Pi l l' _ a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
+eqCnstr (Lambda _ t) (Lambda _ u) = eqWhnf t u
 eqCnstr Top Top = True
 eqCnstr Bottom Bottom = True
 eqCnstr _ _ = False
 
-eqNtrl (Var i) (Var j) = i == j
+eqNtrl (Var _ i) (Var _ j) = i == j
 eqNtrl (App t u) (App t' u') = eqNtrl t t' && eqWhnf u u'
 eqNtrl Absurd Absurd = True
 eqNtrl _ _ = False
@@ -99,20 +99,22 @@ prettyPrecNtrl  : Prec -> Neutral n -> Doc ann
 prettyPrecWhnf  : Prec -> NormalForm n -> Doc ann
 
 prettyPrecCnstr d (Sort s) = prettyPrec d s
-prettyPrecCnstr d (Pi _ _ a b) =
+prettyPrecCnstr d (Pi _ _ var a b) =
   parenthesise (d > Open) $
   group $
-  parens (prettyPrecWhnf Open a) <++>
+  parens (pretty var <++> colon <+> softline <+> prettyPrecWhnf Open a) <++>
   pretty "->" <+> softline <+>
   prettyPrecWhnf Open b
-prettyPrecCnstr d (Lambda t) =
+prettyPrecCnstr d (Lambda var t) =
   parenthesise (d > Open) $
   group $
-  backslash <+> softline <+> prettyPrecWhnf Open t
+  backslash <+> pretty var <++>
+  pretty "=>" <+> softline <+>
+  prettyPrecWhnf Open t
 prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
-prettyPrecNtrl d (Var i) = pretty "$\{show i}"
+prettyPrecNtrl d (Var var i) = pretty "\{show var}@\{show i}"
 prettyPrecNtrl d (App t u) =
   parenthesise (d >= App) $
   group $
@@ -156,12 +158,12 @@ renameNtrl  : Neutral n -> (Fin n -> Fin m) -> Neutral m
 renameWhnf  : NormalForm n -> (Fin n -> Fin m) -> NormalForm m
 
 renameCnstr (Sort s) f = Sort s
-renameCnstr (Pi s s' a b) f = Pi s s' (renameWhnf a f) (renameWhnf b $ lift 1 f)
-renameCnstr (Lambda t) f = Lambda (renameWhnf t $ lift 1 f)
+renameCnstr (Pi s s' var a b) f = Pi s s' var (renameWhnf a f) (renameWhnf b $ lift 1 f)
+renameCnstr (Lambda var t) f = Lambda var (renameWhnf t $ lift 1 f)
 renameCnstr Top f = Top
 renameCnstr Bottom f = Bottom
 
-renameNtrl (Var i) f = Var (f i)
+renameNtrl (Var var i) f = Var var (f i)
 renameNtrl (App t u) f = App (renameNtrl t f) (renameWhnf u f)
 renameNtrl Absurd f = Absurd
 
@@ -183,7 +185,7 @@ Rename NormalForm where
 
 export
 PointedRename Neutral where
-  point = Var
+  point = Var ""
 
 export
 PointedRename NormalForm where