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