Add normalization of environments

diff --git a/CTT.hs b/CTT.hs
index 27be0be258d8f9c92b250f7c3e622102d608f850..e4c49ff06d85bfecc248477fe61c9b3dad8d327f 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -381,7 +381,7 @@ showVal v = case v of
   VPCon c a us phis -> text c <+> braces (showVal a) <+> showVals us
                        <+> (hsep $ map ((char '@' <+>) . showFormula) phis)
   VPi a l@(VLam x t b)
-    | "_" `isPrefixOf` x -> showVal1 a <+> text "->" <+> showVal1 b
+    | "_" `isPrefixOf` x -> showVal a <+> text "->" <+> showVal1 b
     | otherwise          -> char '(' <> showLam v
   VPi a b           -> text "Pi" <+> showVals [a,b]
   VPair u v         -> parens (showVal u <> comma <> showVal v)

diff --git a/Eval.hs b/Eval.hs
index cb231ec02264e8c2c4f983e72838f98560bfc1a6..c42632979e8f7a0e8819204ec3d9087a47a333f4 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -795,6 +795,7 @@ instance Normal Val where
     Ter (Lam x t u) e   -> let w = eval e t
                                v@(VVar n _) = mkVarNice ns x w
                            in VLam n (normal ns w) $ normal (n:ns) (eval (Upd e (x,v)) u)
+    Ter t e             -> Ter t (normal ns e)
     VPi u v             -> VPi (normal ns u) (normal ns v)
     VSigma u v          -> VSigma (normal ns u) (normal ns v)
     VPair u v           -> VPair (normal ns u) (normal ns v)
@@ -816,6 +817,9 @@ instance Normal Val where
     VAppFormula u phi   -> VAppFormula (normal ns u) phi
     _                   -> v
 
+instance Normal Env where
+  normal ns = mapEnv (normal ns) id
+
 instance Normal a => Normal (Map k a) where
   normal ns us = Map.map (normal ns) us