X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=utils%2Fext-core%2FLanguage%2FCore%2FCheck.hs;fp=utils%2Fext-core%2FLanguage%2FCore%2FCheck.hs;h=0000000000000000000000000000000000000000;hp=3ae94e3697eb5641b42a9a1cc892c80a5c085d79;hb=0434f5bf9a2712a99e9e6c99d67991a3f09af91d;hpb=e6232609a0b08ff7136a479f2e2d7d2be5040b1d diff --git a/utils/ext-core/Language/Core/Check.hs b/utils/ext-core/Language/Core/Check.hs deleted file mode 100644 index 3ae94e3..0000000 --- a/utils/ext-core/Language/Core/Check.hs +++ /dev/null @@ -1,649 +0,0 @@ -{-# OPTIONS -Wall -fno-warn-name-shadowing #-} -module Language.Core.Check( - checkModule, envsModule, - checkExpr, checkType, - primCoercionError, - Menv, Venv, Tvenv, Envs(..), - CheckRes(..), splitTy, substl, - mkTypeEnvsNoChecking, NtEnv, mkNtEnv) where - ---import Debug.Trace - -import Language.Core.Core -import Language.Core.CoreUtils -import Language.Core.Printer() -import Language.Core.PrimEnv -import Language.Core.Env -import Language.Core.Environments - -import Control.Monad.Reader -import Data.List -import qualified Data.Map as M -import Data.Maybe - -{- Checking is done in a simple error monad. In addition to - allowing errors to be captured, this makes it easy to guarantee - that checking itself has been completed for an entire module. -} - -{- We use the Reader monad transformer in order to thread the - top-level module name throughout the computation simply. - This is so that checkExp can also be an entry point (we call it - from Prep.) -} -data CheckRes a = OkC a | FailC String -type CheckResult a = ReaderT (AnMname, Menv) CheckRes a -getMname :: CheckResult AnMname -getMname = ask >>= (return . fst) -getGlobalEnv :: CheckResult Menv -getGlobalEnv = ask >>= (return . snd) - -instance Monad CheckRes where - OkC a >>= k = k a - FailC s >>= _ = fail s - return = OkC - fail = FailC - -require :: Bool -> String -> CheckResult () -require False s = fail s -require True _ = return () - - -extendM :: (Ord a, Show a) => Bool -> EnvType -> Env a b -> (a,b) -> CheckResult (Env a b) -extendM checkNameShadowing envType env (k,d) = - case elookup env k of - Just _ | envType == NotTv && checkNameShadowing -> fail ("multiply-defined identifier: " - ++ show k) - _ -> return (eextend env (k,d)) - -extendVenv :: (Ord a, Show a) => Bool -> Env a b -> (a,b) -> CheckResult (Env a b) -extendVenv check = extendM check NotTv - -extendTvenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b) -extendTvenv = extendM True Tv - -lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult (Maybe b) -lookupM env k = return $ elookup env k - -{- Main entry point. -} -checkModule :: Menv -> Module -> CheckRes Menv -checkModule globalEnv (Module mn tdefs vdefgs) = - runReaderT - (do (tcenv, cenv) <- mkTypeEnvs tdefs - (e_venv,_) <- foldM (checkVdefg True (tcenv,eempty,cenv)) - (eempty,eempty) - vdefgs - return (eextend globalEnv - (mn,Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv}))) - (mn, globalEnv) - --- Like checkModule, but doesn't typecheck the code, instead just --- returning declared types for top-level defns. --- This is necessary in order to handle circular dependencies, but it's sort --- of unpleasant. -envsModule :: Menv -> Module -> Menv -envsModule globalEnv (Module mn tdefs vdefgs) = - let (tcenv, cenv) = mkTypeEnvsNoChecking tdefs - e_venv = foldr vdefgTypes eempty vdefgs in - eextend globalEnv (mn, - (Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv})) - where vdefgTypes :: Vdefg -> Venv -> Venv - vdefgTypes (Nonrec (Vdef (v,t,_))) e = - add [(v,t)] e - vdefgTypes (Rec vds) e = - add (map (\ (Vdef (v,t,_)) -> (v,t)) vds) e - add :: [(Qual Var,Ty)] -> Venv -> Venv - add pairs e = foldr addOne e pairs - addOne :: (Qual Var, Ty) -> Venv -> Venv - addOne ((_,v),t) e = eextend e (v,t) - -checkTdef0 :: Tcenv -> Tdef -> CheckResult Tcenv -checkTdef0 tcenv tdef = ch tdef - where - ch (Data (m,c) tbs _) = - do mn <- getMname - requireModulesEq m mn "data type declaration" tdef False - extendM True NotTv tcenv (c, Kind k) - where k = foldr Karrow Klifted (map snd tbs) - ch (Newtype (m,c) coVar tbs rhs) = - do mn <- getMname - requireModulesEq m mn "newtype declaration" tdef False - tcenv' <- extendM True NotTv tcenv (c, Kind k) - -- add newtype axiom to env - tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs - return tcenv'' - where k = foldr Karrow Klifted (map snd tbs) - -processTdef0NoChecking :: Tcenv -> Tdef -> Tcenv -processTdef0NoChecking tcenv tdef = ch tdef - where - ch (Data (_,c) tbs _) = eextend tcenv (c, Kind k) - where k = foldr Karrow Klifted (map snd tbs) - ch (Newtype tc@(_,c) coercion tbs rhs) = - let tcenv' = eextend tcenv (c, Kind k) in - -- add newtype axiom to env - eextend tcenv' - (snd coercion, Coercion $ DefinedCoercion tbs - (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rhs)) - where k = foldr Karrow Klifted (map snd tbs) - -envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Ty - -> CheckResult Tcenv -envPlusNewtype tcenv tyCon coVar tbs rep = extendM True NotTv tcenv - (snd coVar, Coercion $ DefinedCoercion tbs - (foldl Tapp (Tcon tyCon) - (map Tvar (fst (unzip tbs))), - rep)) - -checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv -checkTdef tcenv cenv = ch - where - ch (Data (_,c) utbs cdefs) = - do cbinds <- mapM checkCdef cdefs - foldM (extendM True NotTv) cenv cbinds - where checkCdef (cdef@(Constr (m,dcon) etbs ts)) = - do mn <- getMname - requireModulesEq m mn "constructor declaration" cdef - False - tvenv <- foldM (extendM True Tv) eempty tbs - ks <- mapM (checkTy (tcenv,tvenv)) ts - mapM_ (\k -> require (baseKind k) - ("higher-order kind in:\n" ++ show cdef ++ "\n" ++ - "kind: " ++ show k) ) ks - return (dcon,t mn) - where tbs = utbs ++ etbs - t mn = foldr Tforall - (foldr tArrow - (foldl Tapp (Tcon (Just mn,c)) - (map (Tvar . fst) utbs)) ts) tbs - ch (tdef@(Newtype tc _ tbs t)) = - do tvenv <- foldM (extendM True Tv) eempty tbs - kRhs <- checkTy (tcenv,tvenv) t - require (kRhs `eqKind` Klifted) ("bad kind:\n" ++ show tdef) - kLhs <- checkTy (tcenv,tvenv) - (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs)))) - require (kLhs `eqKind` kRhs) - ("Kind mismatch in newtype axiom types: " ++ show tdef - ++ " kinds: " ++ - (show kLhs) ++ " and " ++ (show kRhs)) - return cenv - -processCdef :: Cenv -> Tdef -> Cenv -processCdef cenv = ch - where - ch (Data (_,c) utbs cdefs) = do - let cbinds = map checkCdef cdefs - foldl eextend cenv cbinds - where checkCdef (Constr (mn,dcon) etbs ts) = - (dcon,t mn) - where tbs = utbs ++ etbs - t mn = foldr Tforall - (foldr tArrow - (foldl Tapp (Tcon (mn,c)) - (map (Tvar . fst) utbs)) ts) tbs - ch _ = cenv - -mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Cenv) -mkTypeEnvs tdefs = do - tcenv <- foldM checkTdef0 eempty tdefs - cenv <- foldM (checkTdef tcenv) eempty tdefs - return (tcenv, cenv) - -mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Cenv) -mkTypeEnvsNoChecking tdefs = - let tcenv = foldl processTdef0NoChecking eempty tdefs - cenv = foldl processCdef eempty tdefs in - (tcenv, cenv) - -requireModulesEq :: Show a => Mname -> AnMname -> String -> a - -> Bool -> CheckResult () -requireModulesEq (Just mn) m msg t _ = require (mn == m) (mkErrMsg msg t) -requireModulesEq Nothing _ msg t emptyOk = require emptyOk (mkErrMsg msg t) - -mkErrMsg :: Show a => String -> a -> String -mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t - -checkVdefg :: Bool -> (Tcenv,Tvenv,Cenv) -> (Venv,Venv) - -> Vdefg -> CheckResult (Venv,Venv) -checkVdefg top_level (tcenv,tvenv,cenv) (e_venv,l_venv) vdefg = do - mn <- getMname - case vdefg of - Rec vdefs -> - do (e_venv', l_venv') <- makeEnv mn vdefs - let env' = (tcenv,tvenv,cenv,e_venv',l_venv') - mapM_ (checkVdef (\ vdef k -> require (k `eqKind` Klifted) - ("unlifted kind in:\n" ++ show vdef)) env') - vdefs - return (e_venv', l_venv') - Nonrec vdef -> - do let env' = (tcenv, tvenv, cenv, e_venv, l_venv) - checkVdef (\ vdef k -> do - require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef) - require ((not top_level) || (not (k `eqKind` Kunlifted))) - ("top-level unlifted kind in:\n" ++ show vdef)) env' vdef - makeEnv mn [vdef] - - where makeEnv mn vdefs = do - ev <- foldM (extendVenv False) e_venv e_vts - lv <- foldM (extendVenv False) l_venv l_vts - return (ev, lv) - where e_vts = [ (v,t) | Vdef ((Just m,v),t,_) <- vdefs, - not (vdefIsMainWrapper mn (Just m))] - l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs] - checkVdef checkKind env (vdef@(Vdef ((m,_),t,e))) = do - mn <- getMname - let isZcMain = vdefIsMainWrapper mn m - unless isZcMain $ - requireModulesEq m mn "value definition" vdef True - k <- checkTy (tcenv,tvenv) t - checkKind vdef k - t' <- checkExp env e - require (t == t') - ("declared type doesn't match expression type in:\n" - ++ show vdef ++ "\n" ++ - "declared type: " ++ show t ++ "\n" ++ - "expression type: " ++ show t') - -vdefIsMainWrapper :: AnMname -> Mname -> Bool -vdefIsMainWrapper enclosing defining = - enclosing == mainMname && defining == wrapperMainAnMname - -checkExpr :: AnMname -> Menv -> Tcenv -> Cenv -> Venv -> Tvenv - -> Exp -> Ty -checkExpr mn menv _tcenv _cenv venv tvenv e = case runReaderT (do - --(tcenv, cenv) <- mkTypeEnvs tdefs - -- Since the preprocessor calls checkExpr after code has been - -- typechecked, we expect to find the external env in the Menv. - case (elookup menv mn) of - Just thisEnv -> - checkExp ({-tcenv-}tcenv_ thisEnv, tvenv, {-cenv-}cenv_ thisEnv, (venv_ thisEnv), venv) e - Nothing -> reportError e ("checkExpr: Environment for " ++ - show mn ++ " not found")) (mn,menv) of - OkC t -> t - FailC s -> reportError e s - -checkType :: AnMname -> Menv -> Tcenv -> Tvenv -> Ty -> Kind -checkType mn menv _tcenv tvenv t = - case runReaderT (checkTy (tcenv_ (fromMaybe (error "checkType") (elookup menv mn)), tvenv) t) (mn, menv) of - OkC k -> k - FailC s -> reportError tvenv (s ++ "\n " ++ show menv ++ "\n mname =" ++ show mn) - -checkExp :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty -checkExp (tcenv,tvenv,cenv,e_venv,l_venv) = ch - where - ch e0 = - case e0 of - Var qv -> - qlookupM venv_ e_venv l_venv qv - Dcon qc -> - qlookupM cenv_ cenv eempty qc - Lit l -> - checkLit l - Appt e t -> - do t' <- ch e - k' <- checkTy (tcenv,tvenv) t - case t' of - Tforall (tv,k) t0 -> - do require (k' `subKindOf` k) - ("kind doesn't match at type application in:\n" ++ show e0 ++ "\n" ++ - "operator kind: " ++ show k ++ "\n" ++ - "operand kind: " ++ show k') - return (substl [tv] [t] t0) - _ -> fail ("bad operator type in type application:\n" ++ show e0 ++ "\n" ++ - "operator type: " ++ show t') - App e1 e2 -> - do t1 <- ch e1 - t2 <- ch e2 - case t1 of - Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow -> - do require (t2 == t') - ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++ - "operator type: " ++ show t' ++ "\n" ++ - "operand type: " ++ show t2) - return t0 - _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++ - "operator type: " ++ show t1) - Lam (Tb tb) e -> - do tvenv' <- extendTvenv tvenv tb - t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv) e - return (Tforall tb t) - Lam (Vb (vb@(_,vt))) e -> - do k <- checkTy (tcenv,tvenv) vt - require (baseKind k) - ("higher-order kind in:\n" ++ show e0 ++ "\n" ++ - "kind: " ++ show k) - l_venv' <- extendVenv True l_venv vb - t <- checkExp (tcenv,tvenv,cenv,e_venv,l_venv') e - require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0) - return (tArrow vt t) - Let vdefg e -> - do (e_venv',l_venv') <- checkVdefg False (tcenv,tvenv,cenv) - (e_venv,l_venv) vdefg - checkExp (tcenv,tvenv,cenv,e_venv',l_venv') e - Case e (v,t) resultTy alts -> - do t' <- ch e - checkTy (tcenv,tvenv) t - require (t == t') - ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++ - "declared type: " ++ show t ++ "\n" ++ - "expression type: " ++ show t') - case (reverse alts) of - (Acon c _ _ _):as -> - let ok ((Acon c _ _ _):as) cs = do require (notElem c cs) - ("duplicate alternative in case:\n" ++ show e0) - ok as (c:cs) - ok ((Alit _ _):_) _ = fail ("invalid alternative in constructor case:\n" ++ show e0) - ok [Adefault _] _ = return () - ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0) - ok [] _ = return () - in ok as [c] - (Alit l _):as -> - let ok ((Acon _ _ _ _):_) _ = fail ("invalid alternative in literal case:\n" ++ show e0) - ok ((Alit l _):as) ls = do require (notElem l ls) - ("duplicate alternative in case:\n" ++ show e0) - ok as (l:ls) - ok [Adefault _] _ = return () - ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0) - ok [] _ = fail ("missing default alternative in literal case:\n" ++ show e0) - in ok as [l] - [Adefault _] -> return () - _ -> fail ("no alternatives in case:\n" ++ show e0) - l_venv' <- extendVenv True l_venv (v,t) - t:ts <- mapM (checkAlt (tcenv,tvenv,cenv,e_venv,l_venv') t) alts - require (all (== t) ts) - ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++ - "types: " ++ show (t:ts)) - checkTy (tcenv,tvenv) resultTy - require (t == resultTy) ("case alternative type doesn't " ++ - " match case return type in:\n" ++ show e0 ++ "\n" ++ - "alt type: " ++ show t ++ " return type: " ++ show resultTy) - return t - c@(Cast e t) -> - do eTy <- ch e - (fromTy, toTy) <- checkTyCo (tcenv,tvenv) t - require (eTy == fromTy) ("Type mismatch in cast: c = " - ++ show c ++ "\nand eTy = " ++ show eTy - ++ "\n and " ++ show fromTy) - return toTy - Note _ e -> - ch e - External _ t -> - do checkTy (tcenv,eempty) t {- external types must be closed -} - return t - -checkAlt :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty -checkAlt (env@(tcenv,tvenv,cenv,e_venv,l_venv)) t0 = ch - where - ch a0 = - case a0 of - Acon qc etbs vbs e -> - do let uts = f t0 - where f (Tapp t0 t) = f t0 ++ [t] - f _ = [] - ct <- qlookupM cenv_ cenv eempty qc - let (tbs,ct_args0,ct_res0) = splitTy ct - {- get universals -} - let (utbs,etbs') = splitAt (length uts) tbs - let utvs = map fst utbs - {- check existentials -} - let (etvs,eks) = unzip etbs - let (etvs',eks') = unzip etbs' - require (all (uncurry eqKind) - (zip eks eks')) - ("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++ - "kinds declared in data constructor: " ++ show eks ++ - "kinds declared in case alternative: " ++ show eks') - tvenv' <- foldM extendTvenv tvenv etbs - {- check term variables -} - let vts = map snd vbs - mapM_ (\vt -> require ((not . isUtupleTy) vt) - ("pattern-bound unboxed tuple in:\n" ++ show a0 ++ "\n" ++ - "pattern type: " ++ show vt)) vts - vks <- mapM (checkTy (tcenv,tvenv')) vts - mapM_ (\vk -> require (baseKind vk) - ("higher-order kind in:\n" ++ show a0 ++ "\n" ++ - "kind: " ++ show vk)) vks - let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0) - zipWithM_ - (\ct_arg vt -> - require (ct_arg == vt) - ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++ - "pattern variable type: " ++ show ct_arg ++ "\n" ++ - "constructor argument type: " ++ show vt)) ct_args vts - require (ct_res == t0) - ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++ - "pattern constructor type: " ++ show ct_res ++ "\n" ++ - "scrutinee type: " ++ show t0) - l_venv' <- foldM (extendVenv True) l_venv vbs - t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv') e - checkTy (tcenv,tvenv) t {- check that existentials don't escape in result type -} - return t - Alit l e -> - do t <- checkLit l - require (t == t0) - ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++ - "pattern type: " ++ show t ++ "\n" ++ - "scrutinee type: " ++ show t0) - checkExp env e - Adefault e -> - checkExp env e - -checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind -checkTy es@(tcenv,tvenv) = ch - where - ch (Tvar tv) = do - res <- lookupM tvenv tv - case res of - Just k -> return k - Nothing -> fail ("Undefined tvar: " ++ show tv) - ch (Tcon qtc) = do - kOrC <- qlookupM tcenv_ tcenv eempty qtc - case kOrC of - Kind k -> return k - Coercion (DefinedCoercion [] (t1,t2)) -> return $ Keq t1 t2 - Coercion _ -> fail ("Unsaturated coercion app: " ++ show qtc) - ch (t@(Tapp t1 t2)) = - case splitTyConApp_maybe t of - Just (tc, tys) -> do - tcK <- qlookupM tcenv_ tcenv eempty tc - case tcK of - Kind _ -> checkTapp t1 t2 - Coercion co@(DefinedCoercion tbs _) -> do - -- makes sure coercion is fully applied - require (length tys == length tbs) $ - ("Arity mismatch in coercion app: " ++ show t) - let (_, tks) = unzip tbs - argKs <- mapM (checkTy es) tys - let kPairs = zip argKs tks - -- Simon says it's okay for these to be - -- subkinds - let kindsOk = all (uncurry subKindOf) kPairs - require kindsOk - ("Kind mismatch in coercion app: " ++ show tks - ++ " and " ++ show argKs ++ " t = " ++ show t) - return $ (uncurry Keq) (applyNewtype co tys) - Nothing -> checkTapp t1 t2 - where checkTapp t1 t2 = do - k1 <- ch t1 - k2 <- ch t2 - case k1 of - Karrow k11 k12 -> do - require (k2 `subKindOf` k11) kindError - return k12 - where kindError = - "kinds don't match in type application: " - ++ show t ++ "\n" ++ - "operator kind: " ++ show k11 ++ "\n" ++ - "operand kind: " ++ show k2 - _ -> fail ("applied type has non-arrow kind: " ++ show t) - - ch (Tforall tb t) = - do tvenv' <- extendTvenv tvenv tb - checkTy (tcenv,tvenv') t - ch (TransCoercion t1 t2) = do - (ty1,ty2) <- checkTyCo es t1 - (ty3,ty4) <- checkTyCo es t2 - require (ty2 == ty3) ("Types don't match in trans. coercion: " ++ - show ty2 ++ " and " ++ show ty3) - return $ Keq ty1 ty4 - ch (SymCoercion t1) = do - (ty1,ty2) <- checkTyCo es t1 - return $ Keq ty2 ty1 - ch (UnsafeCoercion t1 t2) = do - checkTy es t1 - checkTy es t2 - return $ Keq t1 t2 - ch (LeftCoercion t1) = do - k <- checkTyCo es t1 - case k of - ((Tapp u _), (Tapp w _)) -> return $ Keq u w - _ -> fail ("Bad coercion kind in operand of left: " ++ show k) - ch (RightCoercion t1) = do - k <- checkTyCo es t1 - case k of - ((Tapp _ v), (Tapp _ x)) -> return $ Keq v x - _ -> fail ("Bad coercion kind in operand of left: " ++ show k) - ch (InstCoercion ty arg) = do - forallK <- checkTyCo es ty - case forallK of - ((Tforall (v1,k1) b1), (Tforall (v2,k2) b2)) -> do - require (k1 `eqKind` k2) ("Kind mismatch in argument of inst: " - ++ show ty) - argK <- checkTy es arg - require (argK `eqKind` k1) ("Kind mismatch in type being " - ++ "instantiated: " ++ show arg) - let newLhs = substl [v1] [arg] b1 - let newRhs = substl [v2] [arg] b2 - return $ Keq newLhs newRhs - _ -> fail ("Non-forall-ty in argument to inst: " ++ show ty) - -checkTyCo :: (Tcenv, Tvenv) -> Ty -> CheckResult (Ty, Ty) -checkTyCo es@(tcenv,_) t@(Tapp t1 t2) = - (case splitTyConApp_maybe t of - Just (tc, tys) -> do - tcK <- qlookupM tcenv_ tcenv eempty tc - case tcK of - -- todo: avoid duplicating this code - -- blah, this almost calls for a different syntactic form - -- (for a defined-coercion app): (TCoercionApp Tcon [Ty]) - Coercion co@(DefinedCoercion tbs _) -> do - require (length tys == length tbs) $ - ("Arity mismatch in coercion app: " ++ show t) - let (_, tks) = unzip tbs - argKs <- mapM (checkTy es) tys - let kPairs = zip argKs tks - let kindsOk = all (uncurry subKindOf) kPairs - require kindsOk - ("Kind mismatch in coercion app: " ++ show tks - ++ " and " ++ show argKs ++ " t = " ++ show t) - return (applyNewtype co tys) - _ -> checkTapp t1 t2 - _ -> checkTapp t1 t2) - where checkTapp t1 t2 = do - (lhsRator, rhsRator) <- checkTyCo es t1 - (lhs, rhs) <- checkTyCo es t2 - -- Comp rule from paper - checkTy es (Tapp lhsRator lhs) - checkTy es (Tapp rhsRator rhs) - return (Tapp lhsRator lhs, Tapp rhsRator rhs) -checkTyCo (tcenv, tvenv) (Tforall tb t) = do - tvenv' <- extendTvenv tvenv tb - (t1,t2) <- checkTyCo (tcenv, tvenv') t - return (Tforall tb t1, Tforall tb t2) -checkTyCo es t = do - k <- checkTy es t - case k of - Keq t1 t2 -> return (t1, t2) - -- otherwise, expand by the "refl" rule - _ -> return (t, t) - -mlookupM :: (Eq a, Show a, Show b) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname - -> CheckResult (Env a b) -mlookupM _ _ local_env Nothing = -- (trace ("mlookupM_: returning " ++ show local_env)) $ - return local_env -mlookupM selector external_env local_env (Just m) = do - mn <- getMname - globalEnv <- getGlobalEnv - if m == mn - then -- trace ("global env would b e " ++ show (elookup globalEnv m)) $ - return external_env - else - case elookup globalEnv m of - Just env' -> return (selector env') - Nothing -> fail ("Check: undefined module name: " - ++ show m ++ show (edomain local_env)) - -qlookupM :: (Ord a, Show a,Show b) => (Envs -> Env a b) -> Env a b -> Env a b - -> Qual a -> CheckResult b -qlookupM selector external_env local_env v@(m,k) = - do env <- -- trace ("qlookupM: " ++ show v) $ - mlookupM selector external_env local_env m - -- argh, hack for unqualified top-level names - maybeRes <- lookupM env k - case maybeRes of - Just r -> return r - Nothing -> do mn <- getMname - currentMenv <- -- trace ("qlookupM: trying module for " ++ show mn) $ - mlookupM selector external_env local_env (Just mn) - maybeRes1 <- -- trace ("qlookupM: trying in " ++ show currentMenv) $ - lookupM currentMenv k - case maybeRes1 of - Just r1 -> return r1 - Nothing -> do - globalEnv <- getGlobalEnv - case elookup globalEnv mn of - Just e1 -> case elookup (selector e1) k of - Just r2 -> return r2 - Nothing -> fail ("Undefined id " ++ show v) - Nothing -> fail ("Undefined id " ++ show v) - -checkLit :: Lit -> CheckResult Ty -checkLit (Literal lit t) = - case lit of - Lint _ -> - do require (t `elem` intLitTypes) - ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) - return t - Lrational _ -> - do require (t `elem` ratLitTypes) - ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) - return t - Lchar _ -> - do require (t `elem` charLitTypes) - ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) - return t - Lstring _ -> - do require (t `elem` stringLitTypes) - ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) - return t - -{- Utilities -} - -{- Split off tbs, arguments and result of a (possibly abstracted) arrow type -} -splitTy :: Ty -> ([Tbind],[Ty],Ty) -splitTy (Tforall tb t) = (tb:tbs,ts,tr) - where (tbs,ts,tr) = splitTy t -splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr) - where (tbs,ts,tr) = splitTy t -splitTy t = ([],[],t) - - -primCoercionError :: Show a => a -> b -primCoercionError s = error $ "Bad coercion application: " ++ show s - --- todo -reportError :: Show a => a -> String -> b -reportError e s = error $ ("Core type error: checkExpr failed with " - ++ s ++ " and " ++ show e) - -type NtEnv = M.Map Tcon CoercionKind - -mkNtEnv :: Menv -> NtEnv -mkNtEnv menv = - foldl M.union M.empty $ - map (\ (_,e) -> - foldr (\ (_,thing) rest -> - case thing of - Kind _ -> rest - Coercion d@(DefinedCoercion _ (lhs,_)) -> - case splitTyConApp_maybe lhs of - Just ((_,tc1),_) -> M.insert tc1 d rest - _ -> rest) M.empty (etolist (tcenv_ e))) (etolist menv)