Add normalization function

diff --git a/CTT.hs b/CTT.hs
index 93bd1c2f189430274f51e6d5caba3044482b1c64..dc40a98ba74678c7afc09a69fc407e2c602537aa 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -160,6 +160,7 @@ data Val = VU
          | VSplit Val Val
          | VApp Val Val
          | VAppFormula Val Formula
+         | VLam Ident Val Val
   deriving Eq
 
 isNeutral :: Val -> Bool
@@ -350,6 +351,7 @@ showVal v = case v of
   VPair u v         -> parens (showVal u <> comma <> showVal v)
   VSigma u v        -> text "Sigma" <+> showVals [u,v]
   VApp u v          -> showVal u <+> showVal1 v
+  VLam x t e        -> char '\\' <> text x <+> text "->" <+> showVal e
   VSplit u v        -> showVal u <+> showVal1 v
   VVar x t          -> text x
   VFst u            -> showVal u <> text ".1"

diff --git a/Eval.hs b/Eval.hs
index f58f0579065b4b3409aeb84385911a962f22b8b6..b67e64e9f86daac42206110e3ea51802f2f642b6 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -60,6 +60,7 @@ instance Nominal Val where
   support (VPCon _ a vs phi)    = support (a,vs,phi)
   support (VVar _ v)            = support v
   support (VApp u v)            = support (u,v)
+  support (VLam _ u v)          = support (u,v)
   support (VAppFormula u phi)   = support (u,phi)
   support (VSplit u v)          = support (u,v)
   support (VGlue a ts)          = support (a,ts)
@@ -91,6 +92,7 @@ instance Nominal Val where
          VVar x v   -> VVar x (acti v)
          VAppFormula u psi -> acti u @@ acti psi
          VApp u v   -> app (acti u) (acti v)
+         VLam x t u -> VLam x (acti t) (acti u)
          VSplit u v -> app (acti u) (acti v)
          VGlue a ts -> glue (acti a) (acti ts)
          VGlueElem a ts -> glueElem (acti a) (acti ts)
@@ -118,6 +120,7 @@ instance Nominal Val where
          VVar x v            -> VVar x (sw v)
          VAppFormula u psi   -> VAppFormula (sw u) (sw psi)
          VApp u v            -> VApp (sw u) (sw v)
+         VLam x u v          -> VLam x (sw u) (sw v)
          VSplit u v          -> VSplit (sw u) (sw v)
          VGlue a ts          -> VGlue (sw a) (sw ts)
          VGlueElem a ts      -> VGlueElem (sw a) (sw ts)
@@ -212,7 +215,7 @@ app kan@(VComp (VPi a f) li0 ts) ui1 =
     in comp j (app f ui1) (app li0 ui1)
               (intersectionWith app tsj (border ui1 tsj))
 app r s | isNeutral r = VApp r s
-app _ _ = error "app"
+app r s = error $ "app \n" ++ show r ++ "\n" ++ show s
 
 fstVal, sndVal :: Val -> Val
 fstVal (VPair a b)    = a
@@ -761,3 +764,53 @@ instance Convertible a => Convertible (System a) where
 
 instance Convertible Formula where
   conv _ phi psi = dnf phi == dnf psi
+
+
+
+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 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 (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
+
+instance Normal a => Normal (Map k a) where
+  normal k us = Map.map (normal k) us
+
+instance (Normal a,Normal b) => Normal (a,b) where
+  normal k (u,v) = (normal k u,normal k v)
+
+instance (Normal a,Normal b,Normal c) => Normal (a,b,c) where
+  normal k (u,v,w) = (normal k u,normal k v,normal k w)
+
+instance (Normal a,Normal b,Normal c,Normal d) => Normal (a,b,c,d) where
+  normal k (u,v,w,x) =
+    (normal k u,normal k v,normal k w, normal k x)
+
+instance Normal a => Normal [a] where
+  normal k us = map (normal k) us

diff --git a/Main.hs b/Main.hs
index 71fdab4432a9fce83add6b5a08cac02a53635ee7..b40a266cad86b8c95d4451bd330716f7e798acd9 100644 (file)
--- a/Main.hs
+++ b/Main.hs
@@ -114,7 +114,12 @@ loop flags f names tenv@(TC.TEnv _ rho _) = do
     Just (':':'c':'d':' ':str) -> do lift (setCurrentDirectory str)
                                      loop flags f names tenv
     Just ":h"  -> outputStrLn help >> loop flags f names tenv
-    Just str   -> case pExp (lexer str) of
+    Just str'  ->
+      let (msg,str,mod) = case str' of
+            (':':'n':' ':str) ->
+              ("NORMEVAL: ",str,E.normal 0)
+            str -> ("EVAL: ",str,id)
+      in case pExp (lexer str) of
       Bad err -> outputStrLn ("Parse error: " ++ err) >> loop flags f names tenv
       Ok  exp ->
         case runResolver $ local (insertIdents names) $ resolveExp exp of
@@ -126,9 +131,9 @@ loop flags f names tenv@(TC.TEnv _ rho _) = do
             Left err -> do outputStrLn ("Could not type-check: " ++ err)
                            loop flags f names tenv
             Right _  -> do
-              let e = E.eval rho body
+              let e = mod $ E.eval rho body
               -- Let's not crash if the evaluation raises an error:
-              liftIO $ catch (putStrLn ("EVAL: " ++ show e))
+              liftIO $ catch (putStrLn (msg ++ show e))
                              (\e -> putStrLn ("Exception: " ++
                                               show (e :: SomeException)))
               loop flags f names tenv