reintroduce nicer mkVar

diff --git a/CTT.hs b/CTT.hs
index 998cd9689c0fc5f676d47729866c7c816f878edc..eea02fd58830cd81187b785f4ca2040cc3d9d2ac 100644 (file)
--- 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 c3591e51b6c305cbfe434fc2d4387e6365792fac..e9c18b3a636e8890818e091e5b00e7bbc2b1e8b3 100644 (file)
--- 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 456da6264a7b28026fcab464d9f3b30feba294d2..aa90d9d50d39a75aaff9e838f5cb92205c704ce5 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -65,7 +65,7 @@ runInfer lenv e = runTyping lenv (infer e)
 \r
 addTypeVal :: (Ident,Val) -> TEnv -> TEnv\r
 addTypeVal (x,a) (TEnv k ind rho v) =\r
-  TEnv (k+1) ind (Upd rho (x,mkVar k a)) v\r
+  TEnv (k+1) ind (Upd rho (x,mkVar k x a)) v\r
 \r
 addSub :: (Name,Formula) -> TEnv -> TEnv\r
 addSub iphi (TEnv k ind rho v) = TEnv k ind (Sub rho iphi) v\r
@@ -115,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 x (eval nu a)\r
   in (x,w) : mkVars (k+1) xas (Upd nu (x,w))\r
 \r
 -- Construct a fuction "(_ : va) -> vb"\r
@@ -177,7 +177,7 @@ 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 x a\r
     local (addTypeVal (x,a)) $ check (app f var) t\r
   (VSigma a f, Pair t1 t2) -> do\r
     check a t1\r