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=9f7a27670d011035af3f82d9e72304cb9bd02634;hp=2331ea06327877269b0ccf9459dee6ff2cec71ae;hb=5a4c6ef6e909fbd978ff81bb3453489e884d1885;hpb=7a410061004cedc1de8856b4f049a58c09ee6c38 diff --git a/utils/ext-core/Language/Core/Check.hs b/utils/ext-core/Language/Core/Check.hs index 2331ea0..9f7a276 100644 --- a/utils/ext-core/Language/Core/Check.hs +++ b/utils/ext-core/Language/Core/Check.hs @@ -7,7 +7,10 @@ module Language.Core.Check( CheckRes(..), splitTy, substl, mkTypeEnvsNoChecking) where +--import Debug.Trace + import Language.Core.Core +import Language.Core.CoreUtils import Language.Core.Printer() import Language.Core.PrimEnv import Language.Core.Env @@ -43,25 +46,22 @@ require False s = fail s require True _ = return () -extendM :: (Ord a, Show a) => EnvType -> Env a b -> (a,b) -> CheckResult (Env a b) -extendM envType env (k,d) = +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 -> fail ("multiply-defined identifier: " + Just _ | envType == NotTv && checkNameShadowing -> fail ("multiply-defined identifier: " ++ show k) _ -> return (eextend env (k,d)) -extendVenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b) -extendVenv = extendM NotTv +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 Tv +extendTvenv = extendM True Tv -lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult b -lookupM env k = - case elookup env k of - Just v -> return v - Nothing -> fail ("undefined identifier: " ++ show k ++ " e = " ++ show (edomain env)) - +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) = @@ -72,8 +72,7 @@ checkModule globalEnv (Module mn tdefs vdefgs) = vdefgs return (eextend globalEnv (mn,Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv}))) - -- avoid name shadowing - (mn, eremove globalEnv mn) + (mn, globalEnv) -- Like checkModule, but doesn't typecheck the code, instead just -- returning declared types for top-level defns. @@ -93,8 +92,7 @@ envsModule globalEnv (Module mn tdefs vdefgs) = add :: [(Qual Var,Ty)] -> Venv -> Venv add pairs e = foldr addOne e pairs addOne :: (Qual Var, Ty) -> Venv -> Venv - addOne ((Nothing,_),_) e = e - addOne ((Just _,v),t) e = eextend e (v,t) + addOne ((_,v),t) e = eextend e (v,t) checkTdef0 :: Tcenv -> Tdef -> CheckResult Tcenv checkTdef0 tcenv tdef = ch tdef @@ -102,12 +100,12 @@ checkTdef0 tcenv tdef = ch tdef ch (Data (m,c) tbs _) = do mn <- getMname requireModulesEq m mn "data type declaration" tdef False - extendM NotTv tcenv (c, Kind k) + 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 NotTv tcenv (c, Kind k) + tcenv' <- extendM True NotTv tcenv (c, Kind k) -- add newtype axiom to env tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs return tcenv'' @@ -128,7 +126,7 @@ processTdef0NoChecking tcenv tdef = ch tdef envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Ty -> CheckResult Tcenv -envPlusNewtype tcenv tyCon coVar tbs rep = extendM NotTv 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))), @@ -139,12 +137,12 @@ checkTdef tcenv cenv = ch where ch (Data (_,c) utbs cdefs) = do cbinds <- mapM checkCdef cdefs - foldM (extendM NotTv) cenv cbinds + 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 Tv) eempty tbs + 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" ++ @@ -156,7 +154,7 @@ checkTdef tcenv cenv = ch (foldl Tapp (Tcon (Just mn,c)) (map (Tvar . fst) utbs)) ts) tbs ch (tdef@(Newtype tc _ tbs t)) = - do tvenv <- foldM (extendM Tv) eempty tbs + 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) @@ -209,7 +207,7 @@ checkVdefg top_level (tcenv,tvenv,cenv) (e_venv,l_venv) vdefg = do case vdefg of Rec vdefs -> do (e_venv', l_venv') <- makeEnv mn vdefs - let env' = (tcenv,tvenv,cenv,e_venv',l_venv') + 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 @@ -223,8 +221,8 @@ checkVdefg top_level (tcenv,tvenv,cenv) (e_venv,l_venv) vdefg = do makeEnv mn [vdef] where makeEnv mn vdefs = do - ev <- foldM extendVenv e_venv e_vts - lv <- foldM extendVenv l_venv l_vts + 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))] @@ -311,7 +309,7 @@ checkExp (tcenv,tvenv,cenv,e_venv,l_venv) = ch require (baseKind k) ("higher-order kind in:\n" ++ show e0 ++ "\n" ++ "kind: " ++ show k) - l_venv' <- extendVenv l_venv vb + 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) @@ -347,7 +345,7 @@ checkExp (tcenv,tvenv,cenv,e_venv,l_venv) = ch in ok as [l] [Adefault _] -> return () _ -> fail ("no alternatives in case:\n" ++ show e0) - l_venv' <- extendVenv l_venv (v,t) + 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" ++ @@ -413,7 +411,7 @@ checkAlt (env@(tcenv,tvenv,cenv,e_venv,l_venv)) t0 = ch ("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 l_venv vbs + 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 @@ -430,7 +428,11 @@ checkAlt (env@(tcenv,tvenv,cenv,e_venv,l_venv)) t0 = ch checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind checkTy es@(tcenv,tvenv) = ch where - ch (Tvar tv) = lookupM tvenv tv + 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 @@ -443,11 +445,11 @@ checkTy es@(tcenv,tvenv) = ch tcK <- qlookupM tcenv_ tcenv eempty tc case tcK of Kind _ -> checkTapp t1 t2 - Coercion (DefinedCoercion tbs (from,to)) -> do + Coercion co@(DefinedCoercion tbs _) -> do -- makes sure coercion is fully applied require (length tys == length tbs) $ ("Arity mismatch in coercion app: " ++ show t) - let (tvs, tks) = unzip tbs + let (_, tks) = unzip tbs argKs <- mapM (checkTy es) tys let kPairs = zip argKs tks -- Simon says it's okay for these to be @@ -456,7 +458,7 @@ checkTy es@(tcenv,tvenv) = ch require kindsOk ("Kind mismatch in coercion app: " ++ show tks ++ " and " ++ show argKs ++ " t = " ++ show t) - return $ Keq (substl tvs tys from) (substl tvs tys to) + return $ (uncurry Keq) (applyNewtype co tys) Nothing -> checkTapp t1 t2 where checkTapp t1 t2 = do k1 <- ch t1 @@ -521,17 +523,17 @@ checkTyCo es@(tcenv,_) t@(Tapp t1 t2) = -- todo: avoid duplicating this code -- blah, this almost calls for a different syntactic form -- (for a defined-coercion app): (TCoercionApp Tcon [Ty]) - Coercion (DefinedCoercion tbs (from, to)) -> do + Coercion co@(DefinedCoercion tbs _) -> do require (length tys == length tbs) $ ("Arity mismatch in coercion app: " ++ show t) - let (tvs, tks) = unzip tbs + 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 (substl tvs tys from, substl tvs tys to) + return (applyNewtype co tys) _ -> checkTapp t1 t2 _ -> checkTapp t1 t2) where checkTapp t1 t2 = do @@ -552,15 +554,17 @@ checkTyCo es t = do -- otherwise, expand by the "refl" rule _ -> return (t, t) -mlookupM :: (Eq a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname +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 = return local_env +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 return external_env - else do - globalEnv <- getGlobalEnv + 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: " @@ -568,9 +572,27 @@ mlookupM selector external_env local_env (Just m) = do 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 (m,k) = - do env <- mlookupM selector external_env local_env m - lookupM env k +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) = @@ -603,50 +625,6 @@ splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr) splitTy t = ([],[],t) -{- Simultaneous substitution on types for type variables, - renaming as neceessary to avoid capture. - No checks for correct kindedness. -} -substl :: [Tvar] -> [Ty] -> Ty -> Ty -substl tvs ts t = f (zip tvs ts) t - where - f env t0 = - case t0 of - Tcon _ -> t0 - Tvar v -> case lookup v env of - Just t1 -> t1 - Nothing -> t0 - Tapp t1 t2 -> Tapp (f env t1) (f env t2) - Tforall (t,k) t1 -> - if t `elem` free then - Tforall (t',k) (f ((t,Tvar t'):env) t1) - else - Tforall (t,k) (f (filter ((/=t).fst) env) t1) - TransCoercion t1 t2 -> TransCoercion (f env t1) (f env t2) - SymCoercion t1 -> SymCoercion (f env t1) - UnsafeCoercion t1 t2 -> UnsafeCoercion (f env t1) (f env t2) - LeftCoercion t1 -> LeftCoercion (f env t1) - RightCoercion t1 -> RightCoercion (f env t1) - InstCoercion t1 t2 -> InstCoercion (f env t1) (f env t2) - where free = foldr union [] (map (freeTvars.snd) env) - t' = freshTvar free - -{- Return free tvars in a type -} -freeTvars :: Ty -> [Tvar] -freeTvars (Tcon _) = [] -freeTvars (Tvar v) = [v] -freeTvars (Tapp t1 t2) = freeTvars t1 `union` freeTvars t2 -freeTvars (Tforall (t,_) t1) = delete t (freeTvars t1) -freeTvars (TransCoercion t1 t2) = freeTvars t1 `union` freeTvars t2 -freeTvars (SymCoercion t) = freeTvars t -freeTvars (UnsafeCoercion t1 t2) = freeTvars t1 `union` freeTvars t2 -freeTvars (LeftCoercion t) = freeTvars t -freeTvars (RightCoercion t) = freeTvars t -freeTvars (InstCoercion t1 t2) = freeTvars t1 `union` freeTvars t2 - -{- Return any tvar *not* in the argument list. -} -freshTvar :: [Tvar] -> Tvar -freshTvar tvs = maximum ("":tvs) ++ "x" -- one simple way! - primCoercionError :: Show a => a -> b primCoercionError s = error $ "Bad coercion application: " ++ show s