From: Anders Mörtberg Date: Thu, 16 Apr 2015 09:18:09 +0000 (+0200) Subject: Add indentation to Checking and start changing mkVar (not working as expected wrt... X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=13ddb7de939f746d332c1777884d89b520ec38d2;p=cubicaltt.git Add indentation to Checking and start changing mkVar (not working as expected wrt holes) --- diff --git a/CTT.hs b/CTT.hs index 2ddb021..7cf14d9 100644 --- a/CTT.hs +++ b/CTT.hs @@ -211,8 +211,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) +-- TODO: Use the String! +mkVar :: Int -> String -> Val -> Val +mkVar k x = VVar ("X_" ++ show k) unCon :: Val -> [Val] unCon (VCon _ vs) = vs @@ -372,7 +373,8 @@ showVal v = case v of VLam x t e -> char '\\' <> parens (text x <+> colon <+> showVal t) <+> text "->" <+> showVal e VSplit u v -> showVal u <+> showVal1 v - VVar x t -> text x + VVar x t | head x == '_' -> text x -- Special case, otherwise it is X_0 + | otherwise -> text x -- text (takeWhile (/= '_') x) VFst u -> showVal1 u <> text ".1" VSnd u -> showVal1 u <> text ".2" VIdP v0 v1 v2 -> text "IdP" <+> showVals [v0,v1,v2] diff --git a/Eval.hs b/Eval.hs index 9c8fcfd..5cd0131 100644 --- a/Eval.hs +++ b/Eval.hs @@ -690,13 +690,13 @@ 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' @@ -705,10 +705,10 @@ instance Convertible Val where (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 -- TODO: What string to put here? 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 -- TODO: What string to put here? 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 9728f47..412aad7 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -23,13 +23,14 @@ type Typing a = ReaderT TEnv (ErrorT String IO) a -- Environment for type checker data TEnv = TEnv { index :: Int -- for de Bruijn levels + , indent :: Int , env :: Env , verbose :: Bool -- Should it be verbose and print what it typechecks? } deriving (Eq,Show) verboseEnv, silentEnv :: TEnv -verboseEnv = TEnv 0 Empty True -silentEnv = TEnv 0 Empty False +verboseEnv = TEnv 0 0 Empty True +silentEnv = TEnv 0 0 Empty False -- Trace function that depends on the verbosity flag trace :: String -> Typing () @@ -63,21 +64,21 @@ runInfer lenv e = runTyping lenv (infer e) -- | Modifiers for the environment addTypeVal :: (Ident,Val) -> TEnv -> TEnv -addTypeVal (x,a) (TEnv k rho v) = - TEnv (k+1) (Upd rho (x,mkVar k a)) v +addTypeVal (x,a) (TEnv k ind rho v) = + TEnv (k+1) ind (Upd rho (x,mkVar k (show a) a)) v addSub :: (Name,Formula) -> TEnv -> TEnv -addSub iphi (TEnv k rho v) = TEnv k (Sub rho iphi) v +addSub iphi (TEnv k ind rho v) = TEnv k ind (Sub rho iphi) v addType :: (Ident,Ter) -> TEnv -> Typing TEnv -addType (x,a) tenv@(TEnv _ rho _) = return $ addTypeVal (x,eval rho a) tenv +addType (x,a) tenv@(TEnv _ _ rho _) = return $ addTypeVal (x,eval rho a) tenv addBranch :: [(Ident,Val)] -> (Tele,Env) -> TEnv -> TEnv -addBranch nvs (tele,env) (TEnv k rho v) = - TEnv (k + length nvs) (upds rho nvs) v +addBranch nvs (tele,env) (TEnv k ind rho v) = + TEnv (k + length nvs) ind (upds rho nvs) v addDecls :: [Decl] -> TEnv -> TEnv -addDecls d (TEnv k rho v) = TEnv k (Def d rho) v +addDecls d (TEnv k ind rho v) = TEnv k ind (Def d rho) v addTele :: Tele -> TEnv -> Typing TEnv addTele xas lenv = foldM (flip addType) lenv xas @@ -114,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 (show a) (eval nu a) in (x,w) : mkVars (k+1) xas (Upd nu (x,w)) -- Construct a fuction "(_ : va) -> vb" @@ -176,14 +177,14 @@ 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 (show a) a local (addTypeVal (x,a)) $ check (app f var) t (VSigma a f, Pair t1 t2) -> do check a t1 v <- evalTyping t1 check (app f v) t2 (_,Where e d) -> do - checkDecls d + local (\tenv@TEnv{indent=i} -> tenv{indent=i + 2}) $ checkDecls d local (addDecls d) $ check a e (VU,IdP a e0 e1) -> do (a0,a1) <- checkPath (constPath VU) a @@ -212,7 +213,8 @@ check a t = case (a,t) of checkDecls :: [Decl] -> Typing () checkDecls d = do let (idents,tele,ters) = (declIdents d,declTele d,declTers d) - trace ("Checking: " ++ unwords idents) + ind <- asks indent + trace (replicate ind ' ' ++ "Checking: " ++ unwords idents) checkTele tele local (addDecls d) $ do rho <- asks env