From ab24547842a26878e8052de904e55aa7c5b78cea Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Thu, 16 Apr 2015 15:15:58 +0200 Subject: [PATCH] reintroduce nicer mkVar --- CTT.hs | 18 ++++++++++-------- Eval.hs | 18 +++++++++--------- TypeChecker.hs | 6 +++--- 3 files changed, 22 insertions(+), 20 deletions(-) diff --git a/CTT.hs b/CTT.hs index 998cd96..eea02fd 100644 --- a/CTT.hs +++ b/CTT.hs @@ -197,7 +197,6 @@ isNeutralTrans (VPath i a) u = foo i a u let shasBeta = (shape as) `face` (i ~> 0) in shasBeta /= Map.empty && eps `Map.notMember` shasBeta && isNeutral u foo _ _ _ = False --- foo i a w = error $ "oops!! :\n" ++ show a ++ "\n" ++ show w isNeutralTrans u _ = isNeutral u isNeutralComp :: Val -> Val -> System Val -> Bool @@ -211,8 +210,9 @@ isNeutralComp (VGlue _ as) u ts | isNeutral u = True in isNeutralSystem (Map.filterWithKey testFace ts) isNeutralComp _ _ _ = False -mkVar :: Int -> Val -> Val -mkVar k = VVar ("X" ++ show k) + +mkVar :: Int -> String -> Val -> Val +mkVar k x = VVar (x ++ show k) unCon :: Val -> [Val] unCon (VCon _ vs) = vs @@ -270,7 +270,8 @@ domainEnv rho = case rho of contextOfEnv :: Env -> [String] contextOfEnv rho = case rho of Empty -> [] - Upd e (x,v) -> (x ++ " : " ++ show v) : contextOfEnv e + Upd e (x, VVar n t) -> (n ++ " : " ++ show t) : contextOfEnv e + Upd e (x, v) -> (x ++ " = " ++ show v) : contextOfEnv e Def ts e -> contextOfEnv e Sub e (i,phi) -> (show i ++ " = " ++ show phi) : contextOfEnv e @@ -284,10 +285,11 @@ showEnv, showEnv1 :: Env -> Doc showEnv e = case e of Empty -> PP.empty Def _ env -> showEnv env - Upd env (x,u) -> parens (showEnv1 env <> showVal u) - Sub env (i,phi) -> parens (showEnv1 env <> text (show phi)) -showEnv1 (Upd env (x,u)) = showEnv1 env <> showVal u <> text ", " -showEnv1 e = showEnv e + Upd env (_,u) -> parens (showEnv1 env <> showVal u) + Sub env (_,phi) -> parens (showEnv1 env <> text (show phi)) +showEnv1 (Upd env (_,u)) = showEnv1 env <> showVal u <> text ", " +showEnv1 (Sub env (_,phi)) = showEnv1 env <> text (show phi) <> text ", " +showEnv1 e = showEnv e instance Show Loc where show = render . showLoc diff --git a/Eval.hs b/Eval.hs index c3591e5..e9c18b3 100644 --- a/Eval.hs +++ b/Eval.hs @@ -690,25 +690,25 @@ instance Convertible Val where let j = fresh (u,v) in case (simplify k j u, simplify k j v) of (Ter (Lam x a u) e,Ter (Lam x' a' u') e') -> - let v = mkVar k (eval e a) + let v = mkVar k x (eval e a) in conv (k+1) (eval (Upd e (x,v)) u) (eval (Upd e' (x',v)) u') (Ter (Lam x a u) e,u') -> - let v = mkVar k (eval e a) + let v = mkVar k x (eval e a) in conv (k+1) (eval (Upd e (x,v)) u) (app u' v) (u',Ter (Lam x a u) e) -> - let v = mkVar k (eval e a) + let v = mkVar k x (eval e a) in conv (k+1) (app u' v) (eval (Upd e (x,v)) u) (Ter (Split _ p _ _) e,Ter (Split _ p' _ _) e') -> (p == p') && conv k e e' (Ter (Sum p _ _) e,Ter (Sum p' _ _) e') -> (p == p') && conv k e e' (Ter (Undef p _) e,Ter (Undef p' _) e') -> p == p' && conv k e e' --- (Ter Hole{} e,Ter Hole{} e') -> conv k e e' - (Ter Hole{} e,_) -> True - (_,Ter Hole{} e') -> True + (Ter (Hole p) e,Ter (Hole p') e') -> p == p' && conv k e e' + -- (Ter Hole{} e,_) -> True + -- (_,Ter Hole{} e') -> True (VPi u v,VPi u' v') -> - let w = mkVar k u + let w = mkVar k "X" u in conv k u u' && conv (k+1) (app v w) (app v' w) (VSigma u v,VSigma u' v') -> - let w = mkVar k u + let w = mkVar k "X" u in conv k u u' && conv (k+1) (app v w) (app v' w) (VCon c us,VCon c' us') -> (c == c') && conv k us us' (VPair u v,VPair u' v') -> conv k u u' && conv k v v' @@ -789,7 +789,7 @@ 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 + 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) diff --git a/TypeChecker.hs b/TypeChecker.hs index 456da62..aa90d9d 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -65,7 +65,7 @@ runInfer lenv e = runTyping lenv (infer e) addTypeVal :: (Ident,Val) -> TEnv -> TEnv addTypeVal (x,a) (TEnv k ind rho v) = - TEnv (k+1) ind (Upd rho (x,mkVar k a)) v + TEnv (k+1) ind (Upd rho (x,mkVar k x a)) v addSub :: (Name,Formula) -> TEnv -> TEnv addSub iphi (TEnv k ind rho v) = TEnv k ind (Sub rho iphi) v @@ -115,7 +115,7 @@ constPath = VPath (Name "_") mkVars :: Int -> Tele -> Env -> [(Ident,Val)] mkVars k [] _ = [] mkVars k ((x,a):xas) nu = - let w = mkVar k (eval nu a) + let w = mkVar k x (eval nu a) in (x,w) : mkVars (k+1) xas (Upd nu (x,w)) -- Construct a fuction "(_ : va) -> vb" @@ -177,7 +177,7 @@ check a t = case (a,t) of rho <- asks env unlessM (a === eval rho a') $ throwError "check: lam types don't match" - let var = mkVar k a + let var = mkVar k x a local (addTypeVal (x,a)) $ check (app f var) t (VSigma a f, Pair t1 t2) -> do check a t1 -- 2.34.1