Make conversion use a list of names instead

diff --git a/Eval.hs b/Eval.hs
index 5caceb1db34453cbc411cb478ca095d8d280a0b5..cb231ec02264e8c2c4f983e72838f98560bfc1a6 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -675,109 +675,109 @@ eqLemma e ts a = (t,VPath j theta'')
 -- | Conversion
 
 class Convertible a where
-  conv :: Int -> a -> a -> Bool
+  conv :: [String] -> a -> a -> Bool
 
-isIndep :: (Nominal a, Convertible a) => Int -> Name -> a -> Bool
-isIndep k i u = conv k u (u `face` (i ~> 0))
+isIndep :: (Nominal a, Convertible a) => [String] -> Name -> a -> Bool
+isIndep ns i u = conv ns u (u `face` (i ~> 0))
 
-isCompSystem :: (Nominal a, Convertible a) => Int -> System a -> Bool
-isCompSystem k ts = and [ conv k (getFace alpha beta) (getFace beta alpha)
-                        | (alpha,beta) <- allCompatible (keys ts) ]
+isCompSystem :: (Nominal a, Convertible a) => [String] -> System a -> Bool
+isCompSystem ns ts = and [ conv ns (getFace alpha beta) (getFace beta alpha)
+                         | (alpha,beta) <- allCompatible (keys ts) ]
     where getFace a b = face (ts ! a) (b `minus` a)
 
+simplify :: [String] -> Name -> Val -> Val
+simplify ns j v = case v of
+  VTrans p u | isIndep ns j (p @@ j) -> simplify ns j u
+  VComp a u ts ->
+    let (indep,ts') = Map.partition (\t -> isIndep ns j (t @@ j)) ts
+    in if Map.null ts' then simplify ns j u else VComp a u ts'
+  VCompElem a es u us ->
+    let (indep,es') = Map.partition (\e -> isIndep ns j (e @@ j)) es
+        us'         = intersection us es'
+    in if Map.null es' then simplify ns j u else VCompElem a es' u us'
+  VElimComp a es u ->
+    let (indep,es') = Map.partition (\e -> isIndep ns j (e @@ j)) es
+        u'          = simplify ns j u
+    in if Map.null es' then u' else case u' of
+      VCompElem _ _ w _ -> simplify ns j w
+      _ -> VElimComp a es' u'
+  _ -> v
+
 instance Convertible Val where
-  conv k u v | u == v    = True
-             | otherwise =
+  conv ns u v | u == v    = True
+              | otherwise =
     let j = fresh (u,v)
-    in case (simplify k j u, simplify k j v) of
+    in case (simplify ns j u, simplify ns j v) of
       (Ter (Lam x a u) e,Ter (Lam x' a' u') e') ->
-        let v = mkVar k x (eval e a)
-        in conv (k+1) (eval (Upd e (x,v)) u) (eval (Upd e' (x',v)) u')
+        let v@(VVar n _) = mkVarNice ns x (eval e a)
+        in conv (n:ns) (eval (Upd e (x,v)) u) (eval (Upd e' (x',v)) u')
       (Ter (Lam x a u) e,u') ->
-        let v = mkVar k x (eval e a)
-        in conv (k+1) (eval (Upd e (x,v)) u) (app u' v)
+        let v@(VVar n _) = mkVarNice ns x (eval e a)
+        in conv (n:ns) (eval (Upd e (x,v)) u) (app u' v)
       (u',Ter (Lam x a u) e) ->
-        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 p) e,Ter (Hole p') e') -> p == p' && conv k e e'
+        let v@(VVar n _) = mkVarNice ns x (eval e a)
+        in conv (n:ns) (app u' v) (eval (Upd e (x,v)) u)
+      (Ter (Split _ p _ _) e,Ter (Split _ p' _ _) e') -> (p == p') && conv ns e e'
+      (Ter (Sum p _ _) e,Ter (Sum p' _ _) e')         -> (p == p') && conv ns e e'
+      (Ter (Undef p _) e,Ter (Undef p' _) e') -> p == p' && conv ns e e'
+      (Ter (Hole p) e,Ter (Hole p') e') -> p == p' && conv ns e e'
       -- (Ter Hole{} e,_) -> True
       -- (_,Ter Hole{} e') -> True
       (VPi u v,VPi u' v') ->
-        let w = mkVar k "X" u
-        in conv k u u' && conv (k+1) (app v w) (app v' w)
+        let w@(VVar n _) = mkVarNice ns "X" u
+        in conv ns u u' && conv (n:ns) (app v w) (app v' w)
       (VSigma u v,VSigma u' v') ->
-        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'
+        let w@(VVar n _) = mkVarNice ns "X" u
+        in conv ns u u' && conv (n:ns) (app v w) (app v' w)
+      (VCon c us,VCon c' us')   -> (c == c') && conv ns us us'
       (VPCon c v us phis,VPCon c' v' us' phis') ->
-        (c == c') && conv k (v,us,phis) (v',us',phis')
-      (VPair u v,VPair u' v')    -> conv k u u' && conv k v v'
-      (VPair u v,w)              -> conv k u (fstVal w) && conv k v (sndVal w)
-      (w,VPair u v)              -> conv k (fstVal w) u && conv k (sndVal w) v
-      (VFst u,VFst u')           -> conv k u u'
-      (VSnd u,VSnd u')           -> conv k u u'
-      (VApp u v,VApp u' v')      -> conv k u u' && conv k v v'
-      (VSplit u v,VSplit u' v')  -> conv k u u' && conv k v v'
+        (c == c') && conv ns (v,us,phis) (v',us',phis')
+      (VPair u v,VPair u' v')    -> conv ns u u' && conv ns v v'
+      (VPair u v,w)              -> conv ns u (fstVal w) && conv ns v (sndVal w)
+      (w,VPair u v)              -> conv ns (fstVal w) u && conv ns (sndVal w) v
+      (VFst u,VFst u')           -> conv ns u u'
+      (VSnd u,VSnd u')           -> conv ns u u'
+      (VApp u v,VApp u' v')      -> conv ns u u' && conv ns v v'
+      (VSplit u v,VSplit u' v')  -> conv ns u u' && conv ns v v'
       (VVar x _, VVar x' _)      -> x == x'
-      (VIdP a b c,VIdP a' b' c') -> conv k a a' && conv k b b' && conv k c c'
-      (VPath i a,VPath i' a')    -> conv k (a `swap` (i,j)) (a' `swap` (i',j))
-      (VPath i a,p')             -> conv k (a `swap` (i,j)) (p' @@ j)
-      (p,VPath i' a')            -> conv k (p @@ j) (a' `swap` (i',j))
-      (VTrans p u,VTrans p' u')  -> conv k p p' && conv k u u'
-      (VAppFormula u x,VAppFormula u' x') -> conv k (u,x) (u',x')
-      (VComp a u ts,VComp a' u' ts') -> conv k (a,u,ts) (a',u',ts')
-      (VGlue v hisos,VGlue v' hisos') -> conv k (v,hisos) (v',hisos')
-      (VGlueElem u us,VGlueElem u' us') -> conv k (u,us) (u',us')
+      (VIdP a b c,VIdP a' b' c') -> conv ns a a' && conv ns b b' && conv ns c c'
+      (VPath i a,VPath i' a')    -> conv ns (a `swap` (i,j)) (a' `swap` (i',j))
+      (VPath i a,p')             -> conv ns (a `swap` (i,j)) (p' @@ j)
+      (p,VPath i' a')            -> conv ns (p @@ j) (a' `swap` (i',j))
+      (VTrans p u,VTrans p' u')  -> conv ns p p' && conv ns u u'
+      (VAppFormula u x,VAppFormula u' x') -> conv ns (u,x) (u',x')
+      (VComp a u ts,VComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts')
+      (VGlue v hisos,VGlue v' hisos') -> conv ns (v,hisos) (v',hisos')
+      (VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us')
       (VCompElem a es u us,VCompElem a' es' u' us') ->
-        conv k (a,es,u,us) (a',es',u',us')
-      (VElimComp a es u,VElimComp a' es' u') -> conv k (a,es,u) (a',es',u')
+        conv ns (a,es,u,us) (a',es',u',us')
+      (VElimComp a es u,VElimComp a' es' u') -> conv ns (a,es,u) (a',es',u')
       _                         -> False
 
-simplify :: Int -> Name -> Val -> Val
-simplify k j v = case v of
-  VTrans p u | isIndep k j (p @@ j) -> simplify k j u
-  VComp a u ts ->
-    let (indep,ts') = Map.partition (\t -> isIndep k j (t @@ j)) ts
-    in if Map.null ts' then simplify k j u else VComp a u ts'
-  VCompElem a es u us ->
-    let (indep,es') = Map.partition (\e -> isIndep k j (e @@ j)) es
-        us'         = intersection us es'
-    in if Map.null es' then simplify k j u else VCompElem a es' u us'
-  VElimComp a es u ->
-    let (indep,es') = Map.partition (\e -> isIndep k j (e @@ j)) es
-        u'          = simplify k j u
-    in if Map.null es' then u' else case u' of
-      VCompElem _ _ w _ -> simplify k j w
-      _ -> VElimComp a es' u'
-  _ -> v
-
 instance Convertible Env where
-  conv k e e' = conv k (valAndFormulaOfEnv e) (valAndFormulaOfEnv e')
+  conv ns e e' = conv ns (valAndFormulaOfEnv e) (valAndFormulaOfEnv e')
 
 instance Convertible () where
   conv _ _ _ = True
 
 instance (Convertible a, Convertible b) => Convertible (a, b) where
-  conv k (u, v) (u', v') = conv k u u' && conv k v v'
+  conv ns (u, v) (u', v') = conv ns u u' && conv ns v v'
 
 instance (Convertible a, Convertible b, Convertible c)
       => Convertible (a, b, c) where
-  conv k (u, v, w) (u', v', w') = conv k (u,(v,w)) (u',(v',w'))
+  conv ns (u, v, w) (u', v', w') = conv ns (u,(v,w)) (u',(v',w'))
 
 instance (Convertible a,Convertible b,Convertible c,Convertible d)
       => Convertible (a,b,c,d) where
-  conv k (u,v,w,x) (u',v',w',x') = conv k (u,v,(w,x)) (u',v',(w',x'))
+  conv ns (u,v,w,x) (u',v',w',x') = conv ns (u,v,(w,x)) (u',v',(w',x'))
 
 instance Convertible a => Convertible [a] where
-  conv k us us' = length us == length us' &&
-                  and [conv k u u' | (u,u') <- zip us us']
+  conv ns us us' = length us == length us' &&
+                  and [conv ns u u' | (u,u') <- zip us us']
 
 instance Convertible a => Convertible (System a) where
-  conv k ts ts' = keys ts == keys ts' &&
-                  and (elems (intersectionWith (conv k) ts ts'))
+  conv ns ts ts' = keys ts == keys ts' &&
+                   and (elems (intersectionWith (conv ns) ts ts'))
 
 instance Convertible Formula where
   conv _ phi psi = dnf phi == dnf psi

diff --git a/TypeChecker.hs b/TypeChecker.hs
index b5544e656cb16b8cbd5a9e55a45fd63e71b0634e..08e75b0a2c486512d7a4742dad9c24c819900f4c 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -20,15 +20,15 @@ type Typing a = ReaderT TEnv (ExceptT String IO) a
 \r
 -- Environment for type checker\r
 data TEnv =\r
-  TEnv { index   :: Int   -- for de Bruijn levels\r
+  TEnv { names   :: [String]  -- generated names\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 0 Empty True\r
-silentEnv  = TEnv 0 0 Empty False\r
+verboseEnv = TEnv [] 0 Empty True\r
+silentEnv  = TEnv [] 0 Empty False\r
 \r
 -- Trace function that depends on the verbosity flag\r
 trace :: String -> Typing ()\r
@@ -62,11 +62,12 @@ runInfer lenv e = runTyping lenv (infer e)
 -- | Modifiers for the environment\r
 \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 x a)) v\r
+addTypeVal (x,a) (TEnv ns ind rho v) =\r
+  let w@(VVar n _) = mkVarNice ns x a\r
+  in TEnv (n:ns) ind (Upd rho (x,w)) v\r
 \r
 addSub :: (Name,Formula) -> TEnv -> TEnv\r
-addSub iphi (TEnv k ind rho v) = TEnv k ind (Sub rho iphi) v\r
+addSub iphi (TEnv ns ind rho v) = TEnv ns ind (Sub rho iphi) v\r
 \r
 addSubs :: [(Name,Formula)] -> TEnv -> TEnv\r
 addSubs = flip $ foldr addSub\r
@@ -75,11 +76,11 @@ addType :: (Ident,Ter) -> TEnv -> TEnv
 addType (x,a) tenv@(TEnv _ _ rho _) = addTypeVal (x,eval rho a) tenv\r
 \r
 addBranch :: [(Ident,Val)] -> Env -> TEnv -> TEnv\r
-addBranch nvs env (TEnv k ind rho v) =\r
-  TEnv (k + length nvs) ind (upds rho nvs) v\r
+addBranch nvs env (TEnv ns ind rho v) =\r
+  TEnv ([n | (_,VVar n _) <- nvs] ++ ns) ind (upds rho nvs) v\r
 \r
 addDecls :: [Decl] -> TEnv -> TEnv\r
-addDecls d (TEnv k ind rho v) = TEnv k ind (Def d rho) v\r
+addDecls d (TEnv ns ind rho v) = TEnv ns ind (Def d rho) v\r
 \r
 addTele :: Tele -> TEnv -> TEnv\r
 addTele xas lenv = foldl (flip addType) lenv xas\r
@@ -106,11 +107,11 @@ unlessM mb x = mb >>= flip unless x
 constPath :: Val -> Val\r
 constPath = VPath (Name "_")\r
 \r
-mkVars :: Int -> Tele -> Env -> [(Ident,Val)]\r
+mkVars :: [String] -> Tele -> Env -> [(Ident,Val)]\r
 mkVars _ [] _           = []\r
-mkVars k ((x,a):xas) nu =\r
-  let w = mkVar k x (eval nu a)\r
-  in (x,w) : mkVars (k+1) xas (Upd nu (x,w))\r
+mkVars ns ((x,a):xas) nu =\r
+  let w@(VVar n _) = mkVarNice ns x (eval nu a)\r
+  in (x,w) : mkVars (n:ns) xas (Upd nu (x,w))\r
 \r
 -- Construct a fuction "(_ : va) -> vb"\r
 mkFun :: Val -> Val -> Val\r
@@ -126,7 +127,7 @@ mkSection vb vf vg =
 \r
 -- Test if two values are convertible\r
 (===) :: Convertible a => a -> a -> Typing Bool\r
-u === v = conv <$> asks index <*> pure u <*> pure v\r
+u === v = conv <$> asks names <*> pure u <*> pure v\r
 \r
 -- eval in the typing monad\r
 evalTyping :: Ter -> Typing Val\r
@@ -142,10 +143,9 @@ check a t = case (a,t) of
   (_,Hole l)  -> do\r
       rho <- asks env\r
       let e = unlines (reverse (contextOfEnv rho))\r
---      k <- asks index\r
-      -- TODO: Fix\r
+      ns <- asks names\r
       trace $ "\nHole at " ++ show l ++ ":\n\n" ++\r
-              e ++ replicate 80 '-' ++ "\n" ++ show (normal [] a)  ++ "\n"\r
+              e ++ replicate 80 '-' ++ "\n" ++ show (normal ns a)  ++ "\n"\r
   (_,Con c es) -> do\r
     (bs,nu) <- getLblType c a\r
     checks (bs,nu) es\r
@@ -177,11 +177,11 @@ check a t = case (a,t) of
        else throwError "case branches does not match the data type"\r
   (VPi a f,Lam x a' t)  -> do\r
     check VU a'\r
-    k <- asks index\r
+    ns <- asks names\r
     rho <- asks env\r
     unlessM (a === eval rho a') $\r
       throwError "check: lam types don't match"\r
-    let var = mkVar k x a\r
+    let var = mkVarNice ns 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
@@ -196,8 +196,8 @@ check a t = case (a,t) of
     check a1 e1\r
   (VIdP p a0 a1,Path _ e) -> do\r
     (u0,u1) <- checkPath p t\r
-    k <- asks index\r
-    unless (conv k a0 u0 && conv k a1 u1) $\r
+    ns <- asks names\r
+    unless (conv ns a0 u0 && conv ns a1 u1) $\r
       throwError $ "path endpoints don't match for " ++ show e ++ ", got " ++\r
                    show (u0,u1) ++ ", but expected " ++ show (a0,a1)\r
   (VU,Glue a ts) -> do\r
@@ -241,8 +241,8 @@ checkFam x = throwError $ "checkFam: " ++ show x
 -- Check that a system is compatible\r
 checkCompSystem :: System Val -> Typing ()\r
 checkCompSystem vus = do\r
-  k <- asks index\r
-  unless (isCompSystem k vus)\r
+  ns <- asks names\r
+  unless (isCompSystem ns vus)\r
     (throwError $ "Incompatible system " ++ show vus)\r
 \r
 -- Check the values at corresponding faces with a function, assumes\r
@@ -294,13 +294,13 @@ checkIso vb (Pair a (Pair f (Pair g (Pair s t)))) = do
 \r
 checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing ()\r
 checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do\r
-  k <- asks index\r
-  let us = map snd $ mkVars k tele nu\r
+  ns' <- asks names\r
+  let us = map snd $ mkVars ns' tele nu\r
   local (addBranch (zip ns us) nu) $ check (app f (VCon c us)) e\r
 checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do\r
-  k <- asks index\r
+  ns' <- asks names\r
   mapM_ checkFresh js\r
-  let us   = mkVars k tele nu\r
+  let us   = mkVars ns' tele nu\r
       vus  = map snd us\r
       js'  = map Atom js\r
       vts  = evalSystem (subs (upds nu us) (zip is js')) ts\r