Also normalize the type of lambdas and print VPi nicer

diff --git a/CTT.hs b/CTT.hs
index 7d48bc3d216baf8ac5277cf23af34b75489b94b6..4f40cd6f25e65bb0f37948b5301b2f9a3c7ed6e4 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -367,6 +367,7 @@ showVal v = case v of
   VCon c us         -> text c <+> showVals us
   VPCon c a us phi  -> text c <+> char '{' <+> showVal a <+> char '}' <+>
                        showVals us <+> showFormula phi
+  VPi a (VLam x t b) | "_" `isPrefixOf` x -> showVal1 a <+> text "->" <+> showVal1 b
   VPi a b           -> text "Pi" <+> showVals [a,b]
   VPair u v         -> parens (showVal u <> comma <> showVal v)
   VSigma u v        -> text "Sigma" <+> showVals [u,v]

diff --git a/Eval.hs b/Eval.hs
index e9c18b3a636e8890818e091e5b00e7bbc2b1e8b3..3e57ecc0b23ce491fd3b9e17f12c1fbca0570bc7 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -184,7 +184,7 @@ evalSystem rho ts =
 
 -- TODO: Write using case-of
 app :: Val -> Val -> Val
-app (Ter (Lam x _ t) e) u                  = eval (Upd e (x,u)) t
+app (Ter (Lam x _ t) e) u                 = eval (Upd e (x,u)) t
 app (Ter (Split _ _ _ nvs) e) (VCon c us) = case lookupBranch c nvs of
   Just (OBranch _ xs t) -> eval (upds e (zip xs us)) t
   _     -> error $ "app: Split with insufficient arguments; " ++
@@ -779,38 +779,39 @@ instance Convertible a => Convertible (System a) where
 instance Convertible Formula where
   conv _ phi psi = dnf phi == dnf psi
 
-
+-------------------------------------------------------------------------------
+-- | Normalization
 
 class Normal a where
   normal :: Int -> a -> a
 
 -- Does neither normalize formulas nor environments.
 instance Normal Val where
-  normal _ VU = VU
-  normal k (Ter (Lam x t u) e) = VLam name w $ normal (k+1) (eval (Upd e (x,v)) u)
-    where w = eval e t
-          v@(VVar name _) = mkVar k x w
-  normal k (VPi u v) = VPi (normal k u) (normal k v)
-  normal k (VSigma u v) = VSigma (normal k u) (normal k v)
-  normal k (VPair u v) = VPair (normal k u) (normal k v)
-  normal k (VCon n us) = VCon n (normal k us)
-  normal k (VPCon n u us phi) = VPCon n (normal k u) (normal k us) phi
-  normal k (VIdP a u0 u1) = VIdP a' u0' u1'
-    where (a',u0',u1') = normal k (a,u0,u1)
-  normal k (VPath i u) = VPath i (normal k u)
-  normal k (VComp u v vs) = compLine (normal k u) (normal k v) (normal k vs)
-  normal k (VTrans u v) = transLine (normal k u) (normal k v)
-  normal k (VGlue u hisos) = glue (normal k u) (normal k hisos)
-  normal k (VGlueElem u us) = glueElem (normal k u) (normal k us)
-  normal k (VCompElem a es u us) = compElem (normal k a) (normal k es) (normal k u) (normal k us)
-  normal k (VElimComp a es u) = elimComp (normal k a) (normal k es) (normal k u)
-  normal k (VVar x t) = VVar x t -- (normal k t)
-  normal k (VFst t) = fstVal (normal k t)
-  normal k (VSnd t) = sndVal (normal k t)
-  normal k (VSplit u t) = VSplit (normal k u) (normal k t)
-  normal k (VApp u v) = app (normal k u) (normal k v)
-  normal k (VAppFormula u phi) = VAppFormula (normal k u) phi
-  normal k u = u
+  normal k v = case v of
+    VU                  -> VU
+    Ter (Lam x t u) e   -> let w = eval e t
+                               v@(VVar name _) = mkVar k x w
+                           in VLam name (normal k w) $ normal (k+1) (eval (Upd e (x,v)) u)
+    VPi u v             -> VPi (normal k u) (normal k v)
+    VSigma u v          -> VSigma (normal k u) (normal k v)
+    VPair u v           -> VPair (normal k u) (normal k v)
+    VCon n us           -> VCon n (normal k us)
+    VPCon n u us phi    -> VPCon n (normal k u) (normal k us) phi
+    VIdP a u0 u1        -> VIdP (normal k a) (normal k u0) (normal k u1)
+    VPath i u           -> VPath i (normal k u)
+    VComp u v vs        -> compLine (normal k u) (normal k v) (normal k vs)
+    VTrans u v          -> transLine (normal k u) (normal k v)
+    VGlue u hisos       -> glue (normal k u) (normal k hisos)
+    VGlueElem u us      -> glueElem (normal k u) (normal k us)
+    VCompElem a es u us -> compElem (normal k a) (normal k es) (normal k u) (normal k us)
+    VElimComp a es u    -> elimComp (normal k a) (normal k es) (normal k u)
+    VVar x t            -> VVar x t -- (normal k t)
+    VFst t              -> fstVal (normal k t)
+    VSnd t              -> sndVal (normal k t)
+    VSplit u t          -> VSplit (normal k u) (normal k t)
+    VApp u v            -> app (normal k u) (normal k v)
+    VAppFormula u phi   -> VAppFormula (normal k u) phi
+    _                   -> v
 
 instance Normal a => Normal (Map k a) where
   normal k us = Map.map (normal k) us

diff --git a/Exp.cf b/Exp.cf
index 76e78712facbb12b0ab7f3294ffa78b0cd3ddf98..b84064e1e663e994e9270a91b6c925e8b9908167 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -84,7 +84,7 @@ terminator Tele "" ;
 PTele.    PTele ::= "(" Exp ":" Exp ")" ;
 terminator nonempty PTele "" ;
 
-position token AIdent (letter|'_')(letter|digit|'\''|'_')* ;
+position token AIdent ('_')|(letter)(letter|digit|'\''|'_')* ;
 separator AIdent "" ;
 
 token CIdent '/''\\' ;