From db301a8818a48f03ec8f41982298b090c081d63f Mon Sep 17 00:00:00 2001 From: Anders Date: Thu, 9 Apr 2015 14:29:01 +0200 Subject: [PATCH] Add normalization function --- CTT.hs | 2 ++ Eval.hs | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++++++- Main.hs | 11 ++++++++--- 3 files changed, 64 insertions(+), 4 deletions(-) diff --git a/CTT.hs b/CTT.hs index 93bd1c2..dc40a98 100644 --- 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 f58f057..b67e64e 100644 --- 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 71fdab4..b40a266 100644 --- 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 -- 2.34.1