Add indentation to Checking and start changing mkVar (not working as expected wrt...

diff --git a/CTT.hs b/CTT.hs
index 2ddb021db5e2afca5ad510e298e3fb80cb4bce26..7cf14d91c71fd8423e5bc922cbc3059a93c7d31f 100644 (file)
--- 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 9c8fcfd7080599e3aa8f201f5a28c41f8c1bcda3..5cd01319eca3335ee7f7ca2da2dda51a79307b5f 100644 (file)
--- 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 9728f4731170c6bbc22d57015c6191214765470f..412aad78848c8948f7cb05dc87971c3962118892 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -23,13 +23,14 @@ type Typing a = ReaderT TEnv (ErrorT String IO) a
 -- Environment for type checker\r
 data TEnv =\r
   TEnv { index   :: Int   -- for de Bruijn levels\r
+       , indent  :: Int\r
        , env     :: Env\r
        , verbose :: Bool  -- Should it be verbose and print what it typechecks?\r
        } deriving (Eq,Show)\r
 \r
 verboseEnv, silentEnv :: TEnv\r
-verboseEnv = TEnv 0 Empty True\r
-silentEnv  = TEnv 0 Empty False\r
+verboseEnv = TEnv 0 0 Empty True\r
+silentEnv  = TEnv 0 0 Empty False\r
 \r
 -- Trace function that depends on the verbosity flag\r
 trace :: String -> Typing ()\r
@@ -63,21 +64,21 @@ runInfer lenv e = runTyping lenv (infer e)
 -- | Modifiers for the environment\r
 \r
 addTypeVal :: (Ident,Val) -> TEnv -> TEnv\r
-addTypeVal (x,a) (TEnv k rho v) =\r
-  TEnv (k+1) (Upd rho (x,mkVar k a)) v\r
+addTypeVal (x,a) (TEnv k ind rho v) =\r
+  TEnv (k+1) ind (Upd rho (x,mkVar k (show a) a)) v\r
 \r
 addSub :: (Name,Formula) -> TEnv -> TEnv\r
-addSub iphi (TEnv k rho v) = TEnv k (Sub rho iphi) v\r
+addSub iphi (TEnv k ind rho v) = TEnv k ind (Sub rho iphi) v\r
 \r
 addType :: (Ident,Ter) -> TEnv -> Typing TEnv\r
-addType (x,a) tenv@(TEnv _ rho _) = return $ addTypeVal (x,eval rho a) tenv\r
+addType (x,a) tenv@(TEnv _ _ rho _) = return $ addTypeVal (x,eval rho a) tenv\r
 \r
 addBranch :: [(Ident,Val)] -> (Tele,Env) -> TEnv -> TEnv\r
-addBranch nvs (tele,env) (TEnv k rho v) =\r
-  TEnv (k + length nvs) (upds rho nvs) v\r
+addBranch nvs (tele,env) (TEnv k ind rho v) =\r
+  TEnv (k + length nvs) ind (upds rho nvs) v\r
 \r
 addDecls :: [Decl] -> TEnv -> TEnv\r
-addDecls d (TEnv k rho v) = TEnv k (Def d rho) v\r
+addDecls d (TEnv k ind rho v) = TEnv k ind (Def d rho) v\r
 \r
 addTele :: Tele -> TEnv -> Typing TEnv\r
 addTele xas lenv = foldM (flip addType) lenv xas\r
@@ -114,7 +115,7 @@ constPath = VPath (Name "_")
 mkVars :: Int -> Tele -> Env -> [(Ident,Val)]\r
 mkVars k [] _ = []\r
 mkVars k ((x,a):xas) nu =\r
-  let w = mkVar k (eval nu a)\r
+  let w = mkVar k (show a) (eval nu a)\r
   in (x,w) : mkVars (k+1) xas (Upd nu (x,w))\r
 \r
 -- Construct a fuction "(_ : va) -> vb"\r
@@ -176,14 +177,14 @@ check a t = case (a,t) of
     rho <- asks env\r
     unlessM (a === eval rho a') $\r
       throwError "check: lam types don't match"\r
-    let var = mkVar k a\r
+    let var = mkVar k (show a) a\r
     local (addTypeVal (x,a)) $ check (app f var) t\r
   (VSigma a f, Pair t1 t2) -> do\r
     check a t1\r
     v <- evalTyping t1\r
     check (app f v) t2\r
   (_,Where e d) -> do\r
-    checkDecls d\r
+    local (\tenv@TEnv{indent=i} -> tenv{indent=i + 2}) $ checkDecls d\r
     local (addDecls d) $ check a e\r
   (VU,IdP a e0 e1) -> do\r
     (a0,a1) <- checkPath (constPath VU) a\r
@@ -212,7 +213,8 @@ check a t = case (a,t) of
 checkDecls :: [Decl] -> Typing ()\r
 checkDecls d = do\r
   let (idents,tele,ters) = (declIdents d,declTele d,declTers d)\r
-  trace ("Checking: " ++ unwords idents)\r
+  ind <- asks indent\r
+  trace (replicate ind ' ' ++ "Checking: " ++ unwords idents)\r
   checkTele tele\r
   local (addDecls d) $ do\r
     rho <- asks env\r