module TypeChecker where\r
\r
import Data.Map (Map,(!),mapWithKey,assocs,filterWithKey,elems,keys\r
- ,intersection,intersectionWith,intersectionWithKey)\r
+ ,intersection,intersectionWith,intersectionWithKey\r
+ ,toList,fromList)\r
import qualified Data.Map as Map\r
+import qualified Data.Traversable as T\r
import Control.Monad\r
import Control.Monad.Trans\r
import Control.Monad.Trans.Error hiding (throwError)\r
type Typing a = ReaderT TEnv (ErrorT String IO) a\r
\r
-- Environment for type checker\r
-data TEnv = TEnv { index :: Int -- for de Bruijn levels\r
- , env :: Env\r
- , verbose :: Bool -- Should it be verbose and print\r
- -- what it typechecks?\r
- }\r
- deriving (Eq,Show)\r
+data TEnv =\r
+ TEnv { index :: Int -- for de Bruijn levels\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
\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
-\r
-addSub :: (Name,Formula) -> TEnv -> TEnv\r
-addSub iphi (TEnv k rho v) = TEnv k (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
-\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
-\r
-addDecls :: [Decl] -> TEnv -> TEnv\r
-addDecls d (TEnv k rho v) = TEnv k (Def d rho) v\r
-\r
-addTele :: Tele -> TEnv -> Typing TEnv\r
-addTele xas lenv = foldM (flip addType) lenv xas\r
-\r
-faceEnv :: Face -> TEnv -> TEnv\r
-faceEnv alpha tenv = tenv{env=env tenv `face` alpha}\r
-\r
+-- Trace function that depends on the verbosity flag\r
trace :: String -> Typing ()\r
trace s = do\r
- b <- verbose <$> ask\r
+ b <- asks verbose\r
when b $ liftIO (putStrLn s)\r
\r
+-------------------------------------------------------------------------------\r
+-- | Functions for running computations in the type checker monad\r
+\r
runTyping :: TEnv -> Typing a -> IO (Either String a)\r
runTyping env t = runErrorT $ runReaderT t env\r
\r
--- Used in the interaction loop\r
runDecls :: TEnv -> [Decl] -> IO (Either String TEnv)\r
runDecls tenv d = runTyping tenv $ do\r
checkDecls d\r
return $ addDecls d tenv\r
\r
runDeclss :: TEnv -> [[Decl]] -> IO (Maybe String,TEnv)\r
-runDeclss tenv [] = return (Nothing, tenv)\r
+runDeclss tenv [] = return (Nothing, tenv)\r
runDeclss tenv (d:ds) = do\r
x <- runDecls tenv d\r
case x of\r
runInfer :: TEnv -> Ter -> IO (Either String Val)\r
runInfer lenv e = runTyping lenv (infer e)\r
\r
+-------------------------------------------------------------------------------\r
+-- | 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
+\r
+addSub :: (Name,Formula) -> TEnv -> TEnv\r
+addSub iphi (TEnv k rho v) = TEnv k (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
+\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
+\r
+addDecls :: [Decl] -> TEnv -> TEnv\r
+addDecls d (TEnv k rho v) = TEnv k (Def d rho) v\r
+\r
+addTele :: Tele -> TEnv -> Typing TEnv\r
+addTele xas lenv = foldM (flip addType) lenv xas\r
+\r
+-------------------------------------------------------------------------------\r
+-- | Various useful functions\r
+\r
-- Extract the type of a label as a closure\r
-getLblType :: String -> Val -> Typing (Tele, Env)\r
+getLblType :: LIdent -> Val -> Typing (Tele, Env)\r
getLblType c (Ter (Sum _ _ cas) r) = case lookupLabel c cas of\r
Just as -> return (as,r)\r
Nothing -> throwError ("getLblType: " ++ show c)\r
getLblType c u = throwError ("expected a data type for the constructor "\r
++ c ++ " but got " ++ show u)\r
\r
--- Useful monadic versions of functions:\r
+-- Monadic version of local\r
localM :: (TEnv -> Typing TEnv) -> Typing a -> Typing a\r
localM f r = do\r
e <- ask\r
a <- f e\r
local (const a) r\r
\r
-getFresh :: Val -> Typing Val\r
-getFresh a = do\r
- k <- index <$> ask\r
- e <- asks env\r
- return $ mkVar k a\r
+-- Monadic version of unless\r
+unlessM :: Monad m => m Bool -> m () -> m ()\r
+unlessM mb x = mb >>= flip unless x\r
\r
-checkDecls :: [Decl] -> Typing ()\r
-checkDecls d = do\r
- let (idents, tele, ters) = (declIdents d, declTele d, declTers d)\r
- trace ("Checking: " ++ unwords idents)\r
- checkTele tele\r
- rho <- asks env\r
- localM (addTele tele) $ checks (tele,rho) ters\r
+-- Constant path: <_> v\r
+constPath :: Val -> Val\r
+constPath = VPath (Name "_")\r
\r
-checkTele :: Tele -> Typing ()\r
-checkTele [] = return ()\r
-checkTele ((x,a):xas) = do\r
- check VU a\r
- localM (addType (x,a)) $ checkTele xas\r
+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
+ in (x,w) : mkVars (k+1) xas (Upd nu (x,w))\r
\r
-checkFam :: Ter -> Typing ()\r
-checkFam (Lam x a b) = do\r
- check VU a\r
- localM (addType (x,a)) $ check VU b\r
-checkFam _ = throwError "checkFam"\r
+-- Construct a fuction "(_ : va) -> vb"\r
+mkFun :: Val -> Val -> Val\r
+mkFun va vb = VPi va (eval rho (Lam "_" (Var "a") (Var "b")))\r
+ where rho = Upd (Upd Empty ("a",va)) ("b",vb)\r
\r
-constPath :: Val -> Val\r
-constPath v = VPath (Name "_") v\r
+-- Construct "(x : b) -> IdP (<_> b) (f (g x)) x"\r
+mkSection :: Val -> Val -> Val -> Val\r
+mkSection vb vf vg =\r
+ VPi vb (eval rho (Lam "x" b (IdP (Path (Name "_") b) (App f (App g x)) x)))\r
+ where [b,x,f,g] = map Var ["b","x","f","g"]\r
+ rho = Upd (Upd (Upd Empty ("b",vb)) ("f",vf)) ("g",vg)\r
+\r
+-- Test if two values are convertible\r
+(===) :: Val -> Val -> Typing Bool\r
+u === v = conv <$> asks index <*> pure u <*> pure v\r
+\r
+-- eval in the typing monad\r
+evalTyping :: Ter -> Typing Val\r
+evalTyping t = eval <$> asks env <*> pure t\r
+\r
+-------------------------------------------------------------------------------\r
+-- | The bidirectional type checker\r
\r
-- Check that t has type a\r
check :: Val -> Ter -> Typing ()\r
(_,Con c es) -> do\r
(bs,nu) <- getLblType c a\r
checks (bs,nu) es\r
- (VU,Pi f) -> checkFam f\r
- (VU,Sigma f) -> checkFam f\r
+ (VU,Pi f) -> checkFam f\r
+ (VU,Sigma f) -> checkFam f\r
(VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of\r
OLabel _ tele -> checkTele tele\r
- PLabel n tele t0 t1 -> do\r
+ PLabel _ tele t0 t1 -> do\r
checkTele tele\r
rho <- asks env\r
localM (addTele tele) $ do\r
check (Ter t rho) t1\r
(VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ f' ces) -> do\r
checkFam f'\r
- k <- asks index\r
rho <- asks env\r
- unless (conv k f (eval rho f')) $ throwError "check: split annotations"\r
+ unlessM (f === eval rho f') $ throwError "check: split annotations"\r
if map labelName cas == map branchName ces\r
then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va\r
| (brc, lbl) <- zip ces cas ]\r
check VU a'\r
k <- asks index\r
rho <- asks env\r
- unless (conv k a (eval rho a')) $ throwError "check: lam types don't match"\r
- var <- getFresh a\r
+ unlessM (a === eval rho a') $\r
+ throwError "check: lam types don't match"\r
+ let var = mkVar k a\r
local (addTypeVal (x,a)) $ check (app f var) t\r
(VSigma a f, Pair t1 t2) -> do\r
check a t1\r
- e <- asks env\r
- let v = eval e t1\r
+ v <- evalTyping t1\r
check (app f v) t2\r
(_,Where e d) -> do\r
checkDecls d\r
(a0,a1) <- checkPath (constPath VU) a\r
check a0 e0\r
check a1 e1\r
- (VIdP p a0 a1,Path i e) -> do\r
- rho <- asks env\r
- k <- asks index\r
- when (i `elem` support rho)\r
- (throwError (show i ++ " is already declared"))\r
- local (addSub (i,Atom i)) $ check (p @@ i) e\r
- let u0 = eval (Sub rho (i,Dir 0)) e\r
- u1 = eval (Sub rho (i,Dir 1)) e\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
- throwError $ "path endpoints don't match " ++ show e ++\r
- " \nu0 = " ++ show u0 ++ " \nu1 = " ++ show u1 ++\r
- " \na0 = " ++ show a0 ++ " \na1 = " ++ show a1 ++\r
- " \np = " ++ show p\r
+ throwError $ "path endpoints don't match " ++ show e\r
(VU,Glue a ts) -> do\r
check VU a\r
rho <- asks env\r
checkGlue (eval rho a) ts\r
(VGlue va ts,GlueElem u us) -> do\r
check va u\r
- rho <- asks env\r
- let vu = eval rho u\r
+ vu <- evalTyping u\r
checkGlueElem vu ts us\r
_ -> do\r
v <- infer t\r
- k <- index <$> ask\r
- unless (conv k v a) $\r
+ unlessM (v === a) $\r
throwError $ "check conv: " ++ show v ++ " /= " ++ show a\r
\r
+-- Check a list of declarations\r
+checkDecls :: [Decl] -> Typing ()\r
+checkDecls d = do\r
+ let (idents, tele, ters) = (declIdents d, declTele d, declTers d)\r
+ trace ("Checking: " ++ unwords idents)\r
+ checkTele tele\r
+ rho <- asks env\r
+ localM (addTele tele) $ checks (tele,rho) ters\r
+\r
+-- Check a telescope\r
+checkTele :: Tele -> Typing ()\r
+checkTele [] = return ()\r
+checkTele ((x,a):xas) = do\r
+ check VU a\r
+ localM (addType (x,a)) $ checkTele xas\r
+\r
+-- Check a family\r
+checkFam :: Ter -> Typing ()\r
+checkFam (Lam x a b) = do\r
+ check VU a\r
+ localM (addType (x,a)) $ check VU b\r
+checkFam x = throwError $ "checkFam: " ++ show x\r
+\r
+-- 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
+ (throwError $ "Incompatible system " ++ show vus)\r
+\r
+-- Check the values at corresponding faces with a function, assumes\r
+-- systems have the same faces\r
+checkSystemsWith ::\r
+ System a -> System b -> (Face -> a -> b -> Typing c) -> Typing ()\r
+checkSystemsWith us vs f = sequence_ $ elems $ intersectionWithKey f us vs\r
+\r
+-- Check the faces of a system\r
+checkSystemWith :: System a -> (Face -> a -> Typing b) -> Typing ()\r
+checkSystemWith us f = sequence_ $ elems $ mapWithKey f us\r
+\r
+-- Check a glueElem\r
checkGlueElem :: Val -> System Val -> System Ter -> Typing ()\r
checkGlueElem vu ts us = do\r
unless (keys ts == keys us)\r
(throwError ("Keys don't match in " ++ show ts ++ " and " ++ show us))\r
rho <- asks env\r
- k <- asks index\r
- sequence_ $ elems $ intersectionWithKey\r
- (\alpha vt u -> check (hisoDom vt) u) ts us\r
+ checkSystemsWith ts us (\_ vt u -> check (hisoDom vt) u)\r
let vus = evalSystem rho us\r
- sequence_ $ elems $ intersectionWithKey\r
- (\alpha vt vAlpha -> do\r
- unless (conv k (app (hisoFun vt) vAlpha) (vu `face` alpha))\r
- (throwError $ "Image of glueElem component " ++ show vAlpha ++\r
- " doesn't match " ++ show vu)) ts vus\r
- unless (isCompSystem k vus)\r
- (throwError $ "Incompatible system " ++ show vus)\r
+ checkSystemsWith ts vus (\alpha vt vAlpha ->\r
+ unlessM (app (hisoFun vt) vAlpha === (vu `face` alpha)) $\r
+ throwError $ "Image of glueElem component " ++ show vAlpha ++\r
+ " doesn't match " ++ show vu)\r
+ checkCompSystem vus\r
\r
checkGlue :: Val -> System Ter -> Typing ()\r
checkGlue va ts = do\r
- sequence_ $ elems $ mapWithKey\r
- (\alpha tAlpha -> checkIso (va `face` alpha) tAlpha) ts\r
- k <- asks index\r
+ checkSystemWith ts (\alpha tAlpha -> checkIso (va `face` alpha) tAlpha)\r
rho <- asks env\r
- unless (isCompSystem k (evalSystem rho ts))\r
- (throwError ("Incompatible system " ++ show ts))\r
+ checkCompSystem (evalSystem rho ts)\r
\r
--- An hiso for a type b is a five-tuple: (a,f,g,r,s) where\r
+-- An iso for a type b is a five-tuple: (a,f,g,r,s) where\r
-- a : U\r
-- f : a -> b\r
-- g : b -> a\r
checkIso :: Val -> Ter -> Typing ()\r
checkIso vb (Pair a (Pair f (Pair g (Pair s t)))) = do\r
check VU a\r
- rho <- asks env\r
- let va = eval rho a\r
+ va <- evalTyping a\r
check (mkFun va vb) f\r
check (mkFun vb va) g\r
- let vf = eval rho f\r
- vg = eval rho g\r
- check (mkSection va vb vf vg) s\r
- check (mkSection vb va vg vf) t\r
-\r
-mkFun :: Val -> Val -> Val\r
-mkFun va vb = VPi va (eval rho (Lam "_" (Var "a") (Var "b")))\r
- where rho = Upd (Upd Empty ("a",va)) ("b",vb)\r
-\r
-mkSection :: Val -> Val -> Val -> Val -> Val\r
-mkSection _ vb vf vg =\r
- VPi vb (eval rho (Lam "y" b (IdP (Path (Name "_") b) (App f (App g y)) y)))\r
- where [b,y,f,g] = map Var ["b","y","f","g"]\r
- rho = Upd (Upd (Upd Empty ("b",vb)) ("f",vf)) ("g",vg)\r
+ vf <- evalTyping f\r
+ vg <- evalTyping g\r
+ check (mkSection vb vf vg) s\r
+ check (mkSection va vg vf) t\r
\r
checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing ()\r
checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do\r
vt1 = eval (upds nu us) t1\r
checkFresh i\r
local (addBranch (zip ns vus) (tele,nu)) $ do\r
- local (addSub (i,Atom i))\r
- (check (app f (VPCon c va vus (Atom i))) e)\r
+ local (addSub (i,Atom i)) $\r
+ check (app f (VPCon c va vus (Atom i))) e\r
rho <- asks env\r
- k' <- asks index\r
+ k' <- asks index\r
unless (conv k' (eval (Sub rho (i,Dir 0)) e) (app g vt0) &&\r
conv k' (eval (Sub rho (i,Dir 1)) e) (app g vt1)) $\r
throwError "Endpoints of branch don't match"\r
\r
-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
- in (x,w) : mkVars (k+1) xas (Upd nu (x,w))\r
-\r
checkFormula :: Formula -> Typing ()\r
checkFormula phi = do\r
rho <- asks env\r
let dom = domainEnv rho\r
- if all (\x -> x `elem` dom) (support phi)\r
- then return ()\r
- else throwError ("checkFormula: " ++ show phi)\r
+ unless (all (\x -> x `elem` dom) (support phi)) $\r
+ throwError $ "checkFormula: " ++ show phi\r
+\r
+checkFresh :: Name -> Typing ()\r
+checkFresh i = do\r
+ rho <- asks env\r
+ when (i `elem` support rho)\r
+ (throwError $ show i ++ " is already declared")\r
+\r
+-- Check that a term is a path and output the source and target\r
+checkPath :: Val -> Ter -> Typing (Val,Val)\r
+checkPath v (Path i a) = do\r
+ rho <- asks env\r
+ checkFresh i\r
+ local (addSub (i,Atom i)) $ check (v @@ i) a\r
+ return (eval (Sub rho (i,Dir 0)) a,eval (Sub rho (i,Dir 1)) a)\r
+checkPath v t = do\r
+ vt <- infer t\r
+ case vt of\r
+ VIdP a a0 a1 -> do\r
+ unlessM (a === v) $ throwError "checkPath"\r
+ return (a0,a1)\r
+ _ -> throwError $ show vt ++ " is not a path"\r
+\r
+-- Return system such that:\r
+-- rhoalpha |- p_alpha : Id (va alpha) (t0 rhoalpha) ualpha\r
+-- Moreover, check that the system ps is compatible.\r
+checkPathSystem :: Ter -> Val -> System Ter -> Typing (System Val)\r
+checkPathSystem t0 va ps = do\r
+ rho <- asks env\r
+ checkCompSystem (evalSystem rho ps)\r
+ T.sequence $ mapWithKey (\alpha pAlpha -> do\r
+ (a0,a1) <- checkPath (constPath (va `face` alpha)) pAlpha\r
+ unlessM (a0 === eval (rho `face` alpha) t0) $\r
+ throwError $ "Incompatible system with " ++ show t0\r
+ return a1) ps\r
+\r
+checks :: (Tele,Env) -> [Ter] -> Typing ()\r
+checks _ [] = return ()\r
+checks ((x,a):xas,nu) (e:es) = do\r
+ check (eval nu a) e\r
+ v' <- evalTyping e\r
+ checks (xas,Upd nu (x,v')) es\r
+checks _ _ = throwError "checks"\r
\r
-- infer the type of e\r
infer :: Ter -> Typing Val\r
infer e = case e of\r
U -> return VU -- U : U\r
- Var n -> do\r
- rho <- env <$> ask\r
- return $ lookType n rho\r
+ Var n -> lookType n <$> asks env\r
App t u -> do\r
c <- infer t\r
case c of\r
VPi a f -> do\r
check a u\r
- rho <- asks env\r
- let v = eval rho u\r
+ v <- evalTyping u\r
return $ app f v\r
_ -> throwError $ show c ++ " is not a product"\r
Fst t -> do\r
c <- infer t\r
case c of\r
VSigma a f -> do\r
- e <- asks env\r
- let v = eval e t\r
+ v <- evalTyping t\r
return $ app f (fstVal v)\r
_ -> throwError $ show c ++ " is not a sigma-type"\r
Where t d -> do\r
return a1\r
Comp a t0 ps -> do\r
check VU a\r
- rho <- asks env\r
- let va = eval rho a\r
+ va <- evalTyping a\r
check va t0\r
checkPathSystem t0 va ps\r
return va\r
CompElem a es u us -> do\r
check VU a\r
rho <- asks env\r
- k <- asks index\r
let va = eval rho a\r
ts <- checkPathSystem a VU es\r
let ves = evalSystem rho es\r
(throwError ("Keys don't match in " ++ show es ++ " and " ++ show us))\r
check va u\r
let vu = eval rho u\r
- sequence_ $ elems $ intersectionWith check ts us\r
+ checkSystemsWith ts us (\_ -> check)\r
let vus = evalSystem rho us\r
- unless (isCompSystem k vus)\r
- (throwError ("Incompatible system " ++ show vus))\r
- sequence_ $ elems $ intersectionWithKey (\alpha eA vuA ->\r
- unless (conv k (transNegLine eA vuA) (vu `face` alpha))\r
- (throwError $ "Malformed compElem: " ++ show us)\r
- ) ves vus\r
+ checkCompSystem vus\r
+ checkSystemsWith ves vus (\alpha eA vuA ->\r
+ unlessM (transNegLine eA vuA === (vu `face` alpha)) $\r
+ throwError $ "Malformed compElem: " ++ show us)\r
return $ compLine VU va ves\r
ElimComp a es u -> do\r
check VU a\r
return va\r
PCon c a es phi -> do\r
check VU a\r
- rho <- asks env\r
- let va = eval rho a\r
+ va <- evalTyping a\r
(bs,nu) <- getLblType c va\r
checks (bs,nu) es\r
checkFormula phi\r
return va\r
_ -> throwError ("infer " ++ show e)\r
\r
--- Return system us such that:\r
--- rhoalpha |- p_alpha : Id (va alpha) (t0 rhoalpha) ualpha\r
--- Moreover, check that the system ps is compatible.\r
-checkPathSystem :: Ter -> Val -> System Ter -> Typing (System Val)\r
-checkPathSystem t0 va ps = do\r
- -- TODO: make this nicer!!\r
- -- Also return the evaluated ps\r
- k <- asks index\r
- let alist = Map.toList $ mapWithKey (\alpha pAlpha ->\r
- local (faceEnv alpha) $ do\r
- rhoAlpha <- asks env\r
- (a0,a1) <- checkPath (constPath (va `face` alpha)) pAlpha\r
- unless (conv k a0 (eval rhoAlpha t0))\r
- (throwError ("incompatible system with " ++ show t0))\r
- return a1\r
- ) ps\r
- rho <- asks env\r
- unless (isCompSystem k (evalSystem rho ps))\r
- (throwError ("Incompatible system " ++ show ps))\r
- Map.fromList <$> sequence [ (alpha,) <$> t | (alpha,t) <- alist ]\r
-\r
-checkFresh :: Name -> Typing ()\r
-checkFresh i = do\r
- rho <- asks env\r
- when (i `elem` support rho)\r
- (throwError $ show i ++ " is already declared")\r
-\r
-\r
--- Check that a term is a path and output the source and target\r
-checkPath :: Val -> Ter -> Typing (Val,Val)\r
-checkPath v (Path i a) = do\r
- rho <- asks env\r
- checkFresh i\r
- local (addSub (i,Atom i)) $ check (v @@ i) a\r
- return (eval (Sub rho (i,Dir 0)) a,eval (Sub rho (i,Dir 1)) a)\r
-checkPath v t = do\r
- vt <- infer t\r
- k <- asks index\r
- case vt of\r
- VIdP a a0 a1 -> do\r
- unless (conv k a v) (throwError "checkPath")\r
- return (a0,a1)\r
- _ -> throwError "checkPath"\r
-\r
-checks :: (Tele,Env) -> [Ter] -> Typing ()\r
-checks _ [] = return ()\r
-checks ((x,a):xas,nu) (e:es) = do\r
- let v = eval nu a\r
- check v e\r
- rho <- asks env\r
- let v' = eval rho e\r
- checks (xas,Upd nu (x,v')) es\r
-checks _ _ = throwError "checks"\r
-\r
-- Not used since we have U : U\r
--\r
-- (=?=) :: Typing Ter -> Ter -> Typing ()\r
projects / cubicaltt.git / commitdiff