From: Anders <mortberg@chalmers.se>
Date: Tue, 21 Apr 2015 15:59:11 +0000 (+0200)
Subject: Add normalization of environments
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=81074932263f58ada989f8a85d6b1f81be8c78b7;p=cubicaltt.git

Add normalization of environments
---

diff --git a/CTT.hs b/CTT.hs
index 27be0be..e4c49ff 100644
--- 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 cb231ec..c426329 100644
--- 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