From 8bfeb25ae78e99c7014113468b0057342db4208f Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Mon, 5 May 2008 00:10:50 +0000 Subject: [PATCH] External Core tools: track new syntax for newtypes Update External Core tools to reflect new syntax for newtypes. (Notice that the typechecker is 90 lines shorter!) Also: improve dependency-finding, miscellaneous refactoring. --- utils/ext-core/Check.hs | 212 ++++++++++++---------------------------- utils/ext-core/Core.hs | 15 +-- utils/ext-core/Dependencies.hs | 113 ++++++--------------- utils/ext-core/Driver.hs | 64 ++++++++---- utils/ext-core/Interp.hs | 13 ++- utils/ext-core/Makefile | 2 +- utils/ext-core/Overrides.hs | 93 ++++++++++++++++++ utils/ext-core/ParsecParser.hs | 6 +- utils/ext-core/Prims.hs | 2 - utils/ext-core/Printer.hs | 4 +- utils/ext-core/README | 26 +++-- 11 files changed, 266 insertions(+), 284 deletions(-) create mode 100644 utils/ext-core/Overrides.hs diff --git a/utils/ext-core/Check.hs b/utils/ext-core/Check.hs index 4d35676..e379cd7 100644 --- a/utils/ext-core/Check.hs +++ b/utils/ext-core/Check.hs @@ -8,8 +8,6 @@ module Check( import Maybe import Control.Monad.Reader --- just for printing warnings -import System.IO.Unsafe import Core import Printer() @@ -42,19 +40,13 @@ require :: Bool -> String -> CheckResult () require False s = fail s require True _ = return () -requireM :: CheckResult Bool -> String -> CheckResult () -requireM cond s = - do b <- cond - require b s - {- Environments. -} type Tvenv = Env Tvar Kind -- type variables (local only) type Tcenv = Env Tcon KindOrCoercion -- type constructors -type Tsenv = Env Tcon ([Tvar],Ty) -- type synonyms type Cenv = Env Dcon Ty -- data constructors type Venv = Env Var Ty -- values type Menv = Env AnMname Envs -- modules -data Envs = Envs {tcenv_::Tcenv,tsenv_::Tsenv,cenv_::Cenv,venv_::Venv} -- all the exportable envs +data Envs = Envs {tcenv_::Tcenv,cenv_::Cenv,venv_::Venv} -- all the exportable envs deriving Show {- Extend an environment, checking for illegal shadowing of identifiers (for term @@ -85,12 +77,12 @@ lookupM env k = checkModule :: Menv -> Module -> CheckRes Menv checkModule globalEnv (Module mn tdefs vdefgs) = runReaderT - (do (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs - (e_venv,_) <- foldM (checkVdefg True (tcenv,tsenv,eempty,cenv)) + (do (tcenv, cenv) <- mkTypeEnvs tdefs + (e_venv,_) <- foldM (checkVdefg True (tcenv,eempty,cenv)) (eempty,eempty) vdefgs return (eextend globalEnv - (mn,Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv}))) + (mn,Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv}))) -- avoid name shadowing (mn, eremove globalEnv mn) @@ -100,10 +92,10 @@ checkModule globalEnv (Module mn tdefs vdefgs) = -- of unpleasant. envsModule :: Menv -> Module -> Menv envsModule globalEnv (Module mn tdefs vdefgs) = - let (tcenv, tsenv, cenv) = mkTypeEnvsNoChecking tdefs + let (tcenv, cenv) = mkTypeEnvsNoChecking tdefs e_venv = foldr vdefgTypes eempty vdefgs in eextend globalEnv (mn, - (Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv})) + (Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv})) where vdefgTypes :: Vdefg -> Venv -> Venv vdefgTypes (Nonrec (Vdef (v,t,_))) e = add [(v,t)] e @@ -115,14 +107,13 @@ envsModule globalEnv (Module mn tdefs vdefgs) = addOne ((Nothing,_),_) e = e addOne ((Just _,v),t) e = eextend e (v,t) -checkTdef0 :: (Tcenv,Tsenv) -> Tdef -> CheckResult (Tcenv,Tsenv) -checkTdef0 (tcenv,tsenv) tdef = ch tdef +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 - tcenv' <- extendM NotTv tcenv (c, Kind k) - return (tcenv',tsenv) + extendM NotTv tcenv (c, Kind k) where k = foldr Karrow Klifted (map snd tbs) ch (Newtype (m,c) coVar tbs rhs) = do mn <- getMname @@ -130,37 +121,25 @@ checkTdef0 (tcenv,tsenv) tdef = ch tdef tcenv' <- extendM NotTv tcenv (c, Kind k) -- add newtype axiom to env tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs - tsenv' <- case rhs of - Nothing -> return tsenv - Just rep -> extendM NotTv tsenv (c,(map fst tbs,rep)) - return (tcenv'', tsenv') + return tcenv'' where k = foldr Karrow Klifted (map snd tbs) -processTdef0NoChecking :: (Tcenv,Tsenv) -> Tdef -> (Tcenv,Tsenv) -processTdef0NoChecking (tcenv,tsenv) tdef = ch tdef +processTdef0NoChecking :: Tcenv -> Tdef -> Tcenv +processTdef0NoChecking tcenv tdef = ch tdef where - ch (Data (_,c) tbs _) = (eextend tcenv (c, Kind k), tsenv) + 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) + let tcenv' = eextend tcenv (c, Kind k) in -- add newtype axiom to env - tcenv'' = case rhs of - Just rep -> - eextend tcenv' - (snd coercion, Coercion $ DefinedCoercion tbs - (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rep)) - Nothing -> tcenv' - tsenv' = maybe tsenv - (\ rep -> eextend tsenv (c, (map fst tbs, rep))) rhs in - (tcenv'', tsenv') + 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] -> Maybe Ty +envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Ty -> CheckResult Tcenv -envPlusNewtype tcenv tyCon coVar tbs rhs = - case rhs of - Nothing -> return tcenv - Just rep -> extendM NotTv tcenv +envPlusNewtype tcenv tyCon coVar tbs rep = extendM NotTv tcenv (snd coVar, Coercion $ DefinedCoercion tbs (foldl Tapp (Tcon tyCon) (map Tvar (fst (unzip tbs))), @@ -187,7 +166,7 @@ checkTdef tcenv cenv = ch (foldr tArrow (foldl Tapp (Tcon (Just mn,c)) (map (Tvar . fst) utbs)) ts) tbs - ch (tdef@(Newtype tc _ tbs (Just t))) = + ch (tdef@(Newtype tc _ tbs t)) = do tvenv <- foldM (extendM Tv) eempty tbs kRhs <- checkTy (tcenv,tvenv) t require (kRhs `eqKind` Klifted) ("bad kind:\n" ++ show tdef) @@ -198,9 +177,6 @@ checkTdef tcenv cenv = ch ++ " kinds: " ++ (show kLhs) ++ " and " ++ (show kRhs)) return cenv - ch (Newtype _ _ _ Nothing) = - {- should only occur for recursive Newtypes -} - return cenv processCdef :: Cenv -> Tdef -> Cenv processCdef cenv = ch @@ -217,17 +193,17 @@ processCdef cenv = ch (map (Tvar . fst) utbs)) ts) tbs ch _ = cenv -mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Tsenv, Cenv) +mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Cenv) mkTypeEnvs tdefs = do - (tcenv, tsenv) <- foldM checkTdef0 (eempty,eempty) tdefs + tcenv <- foldM checkTdef0 eempty tdefs cenv <- foldM (checkTdef tcenv) eempty tdefs - return (tcenv, tsenv, cenv) + return (tcenv, cenv) -mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Tsenv, Cenv) +mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Cenv) mkTypeEnvsNoChecking tdefs = - let (tcenv, tsenv) = foldl processTdef0NoChecking (eempty,eempty) tdefs - cenv = foldl processCdef eempty tdefs in - (tcenv, tsenv, cenv) + let tcenv = foldl processTdef0NoChecking eempty tdefs + cenv = foldl processCdef eempty tdefs in + (tcenv, cenv) requireModulesEq :: Show a => Mname -> AnMname -> String -> a -> Bool -> CheckResult () @@ -237,20 +213,20 @@ 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,Tsenv,Tvenv,Cenv) -> (Venv,Venv) +checkVdefg :: Bool -> (Tcenv,Tvenv,Cenv) -> (Venv,Venv) -> Vdefg -> CheckResult (Venv,Venv) -checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = do +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,tsenv,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 return (e_venv', l_venv') Nonrec vdef -> - do let env' = (tcenv, tsenv, tvenv, cenv, e_venv, l_venv) + 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))) @@ -272,7 +248,7 @@ checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = do k <- checkTy (tcenv,tvenv) t checkKind vdef k t' <- checkExp env e - requireM (equalTy tsenv t t') + require (t == t') ("declared type doesn't match expression type in:\n" ++ show vdef ++ "\n" ++ "declared type: " ++ show t ++ "\n" ++ @@ -285,12 +261,12 @@ vdefIsMainWrapper enclosing defining = checkExpr :: AnMname -> Menv -> [Tdef] -> Venv -> Tvenv -> Exp -> Ty checkExpr mn menv tdefs venv tvenv e = case runReaderT (do - (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs + (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, tsenv, tvenv, cenv, (venv_ thisEnv), venv) e + checkExp (tcenv, tvenv, cenv, (venv_ thisEnv), venv) e Nothing -> reportError e ("checkExpr: Environment for " ++ show mn ++ " not found")) (mn,menv) of OkC t -> t @@ -298,13 +274,13 @@ checkExpr mn menv tdefs venv tvenv e = case runReaderT (do checkType :: AnMname -> Menv -> [Tdef] -> Tvenv -> Ty -> Kind checkType mn menv tdefs tvenv t = case runReaderT (do - (tcenv, _, _) <- mkTypeEnvs tdefs + (tcenv, _) <- mkTypeEnvs tdefs checkTy (tcenv, tvenv) t) (mn, menv) of OkC k -> k FailC s -> reportError tvenv s -checkExp :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty -checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch +checkExp :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty +checkExp (tcenv,tvenv,cenv,e_venv,l_venv) = ch where ch e0 = case e0 of @@ -331,7 +307,7 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch t2 <- ch e2 case t1 of Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow -> - do requireM (equalTy tsenv t2 t') + do require (t2 == t') ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++ "operator type: " ++ show t' ++ "\n" ++ "operand type: " ++ show t2) @@ -340,7 +316,7 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch "operator type: " ++ show t1) Lam (Tb tb) e -> do tvenv' <- extendTvenv tvenv tb - t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv) e + 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 @@ -348,17 +324,17 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch ("higher-order kind in:\n" ++ show e0 ++ "\n" ++ "kind: " ++ show k) l_venv' <- extendVenv l_venv vb - t <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') e + 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,tsenv,tvenv,cenv) - (e_venv,l_venv) vdefg - checkExp (tcenv,tsenv,tvenv,cenv,e_venv',l_venv') 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 - requireM (equalTy tsenv t 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') @@ -384,9 +360,8 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch [Adefault _] -> return () _ -> fail ("no alternatives in case:\n" ++ show e0) l_venv' <- extendVenv l_venv (v,t) - t:ts <- mapM (checkAlt (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') t) alts - bs <- mapM (equalTy tsenv t) ts - require (and bs) + 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 @@ -407,8 +382,8 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch do checkTy (tcenv,eempty) t {- external types must be closed -} return t -checkAlt :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty -checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch +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 @@ -442,21 +417,21 @@ checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0) zipWithM_ (\ct_arg vt -> - requireM (equalTy tsenv 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 - requireM (equalTy tsenv ct_res t0) + 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 l_venv vbs - t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv') e + 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 - requireM (equalTy tsenv t t0) + require (t == t0) ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++ "pattern type: " ++ show t ++ "\n" ++ "scrutinee type: " ++ show t0) @@ -487,20 +462,10 @@ checkTy es@(tcenv,tvenv) = ch let (tvs, tks) = unzip tbs argKs <- mapM (checkTy es) tys let kPairs = zip argKs tks - let kindsOk = all (uncurry eqKind) kPairs - if not kindsOk && - all (uncurry subKindOf) kPairs - -- GHC occasionally generates code like: - -- :Co:TTypeable2 (->) - -- where in this case, :Co:TTypeable2 expects an - -- argument of kind (*->(*->*)) and (->) has kind - -- (?->(?->*)). I'm not sure whether or not it's - -- sound to apply an arbitrary coercion to an - -- argument that's a subkind of what it expects. - then warn $ "Applying coercion " ++ show tc ++ - " to arguments of kind " ++ show argKs - ++ " when it expects: " ++ show tks - else require kindsOk + -- 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 $ Keq (substl tvs tys from) (substl tvs tys to) @@ -574,16 +539,10 @@ checkTyCo es@(tcenv,_) t@(Tapp t1 t2) = let (tvs, tks) = unzip tbs argKs <- mapM (checkTy es) tys let kPairs = zip argKs tks - let kindsOk = all (uncurry eqKind) kPairs - if not kindsOk && - all (uncurry subKindOf) kPairs - -- see comments in checkTy about this - then warn $ "Applying coercion " ++ show tc ++ - " to arguments of kind " ++ show argKs - ++ " when it expects: " ++ show tks - else require kindsOk - ("Kind mismatch in coercion app: " ++ show tks - ++ " and " ++ show argKs ++ " t = " ++ show t) + 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) _ -> checkTapp t1 t2 _ -> checkTapp t1 t2) @@ -605,54 +564,6 @@ checkTyCo es t = do -- otherwise, expand by the "refl" rule _ -> return (t, t) -{- Type equality modulo newtype synonyms. -} -equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool -equalTy tsenv t1 t2 = - do t1' <- expand t1 - t2' <- expand t2 - return (t1' == t2') - where expand (Tvar v) = return (Tvar v) - expand (Tcon qtc) = return (Tcon qtc) - expand (Tapp t1 t2) = - do t2' <- expand t2 - expapp t1 [t2'] - expand (Tforall tb t) = - do t' <- expand t - return (Tforall tb t') - expand (TransCoercion t1 t2) = do - exp1 <- expand t1 - exp2 <- expand t2 - return $ TransCoercion exp1 exp2 - expand (SymCoercion t) = do - exp <- expand t - return $ SymCoercion exp - expand (UnsafeCoercion t1 t2) = do - exp1 <- expand t1 - exp2 <- expand t2 - return $ UnsafeCoercion exp1 exp2 - expand (LeftCoercion t1) = do - exp1 <- expand t1 - return $ LeftCoercion exp1 - expand (RightCoercion t1) = do - exp1 <- expand t1 - return $ RightCoercion exp1 - expand (InstCoercion t1 t2) = do - exp1 <- expand t1 - exp2 <- expand t2 - return $ InstCoercion exp1 exp2 - expapp (t@(Tcon (m,tc))) ts = - do env <- mlookupM tsenv_ tsenv eempty m - case elookup env tc of - Just (formals,rhs) | (length formals) == (length ts) -> - return (substl formals ts rhs) - _ -> return (foldl Tapp t ts) - expapp (Tapp t1 t2) ts = - do t2' <- expand t2 - expapp t1 (t2':ts) - expapp t ts = - do t' <- expand t - return (foldl Tapp t' ts) - mlookupM :: (Eq a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname -> CheckResult (Env a b) mlookupM _ _ local_env Nothing = return local_env @@ -755,6 +666,3 @@ primCoercionError s = error $ "Bad coercion application: " ++ show s reportError :: Show a => a -> String -> b reportError e s = error $ ("Core type error: checkExpr failed with " ++ s ++ " and " ++ show e) - -warn :: String -> CheckResult () -warn s = (unsafePerformIO $ putStrLn ("WARNING: " ++ s)) `seq` return () \ No newline at end of file diff --git a/utils/ext-core/Core.hs b/utils/ext-core/Core.hs index 9df300e..a581d3c 100644 --- a/utils/ext-core/Core.hs +++ b/utils/ext-core/Core.hs @@ -15,7 +15,7 @@ data Tdef -- If we have: (Newtype tc co tbs (Just t)) -- there is an implicit axiom: -- co tbs :: tc tbs :=: t - | Newtype (Qual Tcon) (Qual Tcon) [Tbind] (Maybe Ty) + | Newtype (Qual Tcon) (Qual Tcon) [Tbind] Ty deriving (Data, Typeable) data Cdef @@ -103,7 +103,7 @@ data CoercionKind = data KindOrCoercion = Kind Kind | Coercion CoercionKind data Lit = Literal CoreLit Ty - deriving (Data, Typeable, Eq) -- with nearlyEqualTy + deriving (Data, Typeable, Eq) data CoreLit = Lint Integer | Lrational Rational @@ -163,10 +163,11 @@ splitTyConApp_maybe (Tapp rator rand) = Tcon tc -> Just (tc,[rand]) _ -> Nothing splitTyConApp_maybe t@(Tforall _ _) = Nothing - -{- Doesn't expand out fully applied newtype synonyms - (for which an environment is needed). -} -nearlyEqualTy t1 t2 = eqTy [] [] t1 t2 + +-- This used to be called nearlyEqualTy, but now that +-- we don't need to expand newtypes anymore, it seems +-- like equality to me! +equalTy t1 t2 = eqTy [] [] t1 t2 where eqTy e1 e2 (Tvar v1) (Tvar v2) = case (elemIndex v1 e1,elemIndex v2 e2) of (Just i1, Just i2) -> i1 == i2 @@ -178,7 +179,7 @@ nearlyEqualTy t1 t2 = eqTy [] [] t1 t2 eqTy e1 e2 (Tforall (tv1,tk1) t1) (Tforall (tv2,tk2) t2) = tk1 `eqKind` tk2 && eqTy (tv1:e1) (tv2:e2) t1 t2 eqTy _ _ _ _ = False -instance Eq Ty where (==) = nearlyEqualTy +instance Eq Ty where (==) = equalTy subKindOf :: Kind -> Kind -> Bool diff --git a/utils/ext-core/Dependencies.hs b/utils/ext-core/Dependencies.hs index 578ecf3..eef2899 100644 --- a/utils/ext-core/Dependencies.hs +++ b/utils/ext-core/Dependencies.hs @@ -1,25 +1,9 @@ {-# OPTIONS -Wall #-} -{- - Besides computing dependencies between External Core modules, - this module encapsulates some magic regarding overridden modules. - - In the interpreter, we use "overridden" versions of certain - standard GHC library modules in order to avoid implementing - more primitives than we need to implement to run simple programs. - So, during the dependency-finding process (which, because the - dependency-finder maintains a module cache to make sure no - module is loaded/parsed more than once), references to overridden - modules are resolved to references to modules in our simplified - version of the standard library. - - It's kind of ugly. --} module Dependencies(getDependencies) where import Core import Encoding import ParsecParser -import Prims import Control.Monad.State import Data.Generics @@ -47,10 +31,14 @@ getDependencies ms = -- so we ignore the FilePath deps. ds <- go getDeps lefts (map Left) (map Right ms) return (f, ds)) ms) - (_,t,_) <- get + (_,t,c) <- get let modNames = nub $ concat (snd (unzip (leftsPairs (M.toList t)))) - (liftM catMaybes) $ mapM findModuleP (map Left modNames)) + + res1 <- (liftM catMaybes) $ mapM findModuleP (map Left modNames) + return $ res1 `unionByFirst` + (snd (unzip (M.toList c)))) (last ms, M.empty, M.empty) + where unionByFirst = unionBy (\ (f,_) (g,_) -> f == g) go :: (Show a, Show b, Eq b, MonadIO m) => (a -> m [b]) -> ([a] -> [b]) -> ([b] -> [a]) -> [a] -> m [b] @@ -73,7 +61,7 @@ tyRef _ = [] getDeps :: Either AnMname FilePath -> DepM [AnMname] getDeps mn = do - (a,t,b) <- get + (_,t,_) <- get case M.lookup mn t of Just ds -> return ds Nothing -> do @@ -81,12 +69,13 @@ getDeps mn = do case maybeM of Nothing -> return [] Just m@(Module mname _ _) -> do - let ds = (everything union ([] `mkQ` varRef) m) + let ds = (everything union ([] `mkQ` varRef) m) `union` (everything union ([] `mkQ` tyRef) m) in do - put (a, M.insert mn ds t, b) + liftIO $ putStrLn (show mn ++ " : " ++ show ds) + (a1,t1,b1) <- get -- in case we were given a filepath, register the -- module name too - put (a, M.insert (Left mname) ds t, b) + put (a1, M.insert mn ds (M.insert (Left mname) ds t1), b1) return ds findModule :: Either AnMname FilePath -> DepM (Maybe Module) @@ -97,8 +86,6 @@ findModule x = do _ -> return Nothing findModuleP :: Either AnMname FilePath -> DepM (Maybe (FilePath, Module)) -findModuleP (Left mn) | mn `elem` wiredInModules = - findWiredInModule mn >>= (return . Just) findModuleP (Left mn) | mn == wrapperMainMname || mn == mainMname = do (f,_,_) <- get findModuleP (Right f) @@ -114,13 +101,6 @@ tryFindModule k = do Just p -> return p Nothing -> findModuleNotCached k --- This function encapsulates all the business with overriden modules. --- The story is that if an "overridden" module exists for the given --- module, then we parse it in and rewrite all occurrences of the "base-extcore" --- package name inside it to "base". We have to do this b/c when compiling --- the overridden modules, we gave the package name "base-extcore", because --- GHC gets unhappy if we try to make it part of the "base" package. --- Was that clear? (No.) findModuleNotCached :: Either AnMname FilePath -> DepM (FilePath, Module) findModuleNotCached (Left m@(M (P pkgName, encHier, encLeafName))) = do let hier = map zDecodeString encHier @@ -129,46 +109,36 @@ findModuleNotCached (Left m@(M (P pkgName, encHier, encLeafName))) = do ++ map (dirs (zDecodeString pkgName:hier) leafName) searchPath in do match <- liftIO $ findM doesFileExist possibleFiles case match of - Just fp -> findModule' Nothing fp + Just fp -> findModule' fp Nothing -> error ("findModule: failed to find dependency " ++ show m ++ " tried " ++ show possibleFiles) -findModuleNotCached (Right fp) = findModule' Nothing fp +findModuleNotCached (Right fp) = findModule' fp dirs :: [String] -> String -> FilePath -> FilePath dirs modulePath leafName dir = dir (foldr () (addExtension leafName "hcr") modulePath) -findWiredInModule :: AnMname -> DepM (FilePath, Module) -findWiredInModule m@(M (pn, encHier, encLeafName)) = - findModule' (Just munged) (wiredInFileName m) - where hier = map zDecodeString encHier - leafName = zDecodeString encLeafName - munged = - M (pn, map (\ p -> if p == "GHC_ExtCore" then "GHC" else p) hier, - leafName) - -findModule' :: Mname -> FilePath -> DepM (FilePath, Module) -findModule' trueName fp = do +findModule' :: FilePath -> DepM (FilePath, Module) +findModule' fp = do res <- liftIO $ parseCore fp case res of Left _ -> error ("findModule: error parsing dependency " ++ fp) - Right parsedMod -> do - let resultMod@(Module mn _ _) = - case trueName of - Just _ -> mungePackageName parsedMod - Nothing -> parsedMod - cacheModule mn fp resultMod - return (fp, resultMod) + Right parsedMod@(Module mn _ _) -> do + cacheModule mn fp parsedMod + return (fp, parsedMod) cacheModule :: AnMname -> FilePath -> Module -> DepM () cacheModule mn fp m = modify (\ (a, b, cache) -> (a, b, M.insert (Left mn) (fp, m) (M.insert (Right fp) (fp, m) - cache))) + cache))) searchPath :: [FilePath] searchPath = overriddenDir:["../../libraries/", - "../../libraries/integer-gmp/"] + -- kludgy: we wouldn't need these if we parsed the + -- package.conf file, but for now, we are too lazy + "../../libraries/integer-gmp/", + "../../libraries/array/"] overriddenDir :: FilePath overriddenDir = "./lib/" @@ -189,34 +159,9 @@ leftsPairs = foldr leftsPairs' [] where leftsPairs' ((Left x), y) xs = (x, y):xs leftsPairs' _ xs = xs -mungePackageName :: Module -> Module --- for now: just substitute "base-extcore" for "base" --- and "GHC" for "GHC_ExtCore" in every module name -mungePackageName m@(Module mn _ _) = everywhere (mkT mungeMname) - (everywhere (mkT mungePname) - (everywhere (mkT mungeVarName) m)) - where mungePname (P s) | s == zEncodeString overriddenPname = - (P "base") - mungePname p = p - -- rewrite uses of fake primops - mungeVarName (Var (Just mn', v)) - | mn' == mn && v `elem` (fst (unzip newPrimVars)) = - Var (Just primMname, v) - mungeVarName e = e - -mungeMname :: AnMname -> AnMname -mungeMname (M (pname, (hd:rest), leaf)) - | zDecodeString hd == "GHC_ExtCore" = - (M (pname, ("GHC":rest), leaf)) -mungeMname mn = mn - -overriddenPname :: String -overriddenPname = "base-extcore" - -wiredInModules :: [AnMname] -wiredInModules = - map (\ m -> (mkBaseMname m)) ["Handle", "IO", "Unicode"] - -wiredInFileName :: AnMname -> FilePath -wiredInFileName (M (_,_,leafName)) = - "./lib/GHC_ExtCore/" leafName `addExtension` "hcr" +{- +rightsPairs :: [(Either a b, c)] -> [(b, c)] +rightsPairs = foldr rightsPairs' [] + where rightsPairs' ((Right x), y) xs = (x, y):xs + rightsPairs' _ xs = xs +-} \ No newline at end of file diff --git a/utils/ext-core/Driver.hs b/utils/ext-core/Driver.hs index 57d688e..927a95d 100644 --- a/utils/ext-core/Driver.hs +++ b/utils/ext-core/Driver.hs @@ -8,20 +8,25 @@ import Control.Exception import Data.List +import Data.Maybe import Monad import Prelude hiding (catch) import System.Cmd +import System.Console.GetOpt import System.Environment import System.Exit import System.FilePath import Core import Dependencies +import Overrides import Prims import Check import Prep import Interp +import ParsecParser + -- You may need to change this. baseDir :: FilePath baseDir = "../../libraries/" @@ -32,8 +37,6 @@ typecheckLibs = False -- You shouldn't *need* to change anything below this line... -- Code to check that the external and GHC printers print the same results -testFlag :: String -testFlag = "-t" validateResults :: FilePath -> Module -> IO () validateResults origFile m = do let genFile = origFile "parsed" @@ -45,6 +48,15 @@ validateResults origFile m = do _ -> "Error diffing files: " ++ origFile ++ " " ++ genFile ------------------------------------------------------------------------------ +data Flag = Test | NoDeps + deriving Eq + +options :: [OptDescr Flag] +options = + [Option ['t'] ["test"] (NoArg Test) "validate prettyprinted code", + Option ['n'] ["no-deps"] (NoArg NoDeps) "don't compute dependencies automatically" + ] + process :: Bool -> (Check.Menv,[Module]) -> (FilePath, Module) -> IO (Check.Menv,[Module]) process _ (senv,modules) p@(f,m) | isLib p && not typecheckLibs = do @@ -81,17 +93,20 @@ prepM senv' m _f = do main :: IO () main = do args <- getArgs - let (doTest, fnames) = - case args of - (f:rest) | f == testFlag -> (True,rest) - rest@(_:_) -> (False,rest) - _ -> error "usage: ./Driver [filename]" - doOneProgram doTest fnames - where doOneProgram :: Bool -> [FilePath] -> IO () - doOneProgram doTest fns = do - putStrLn $ "========== Program " ++ (show fns) ++ " ================" - deps <- getDependencies fns - -- putStrLn $ "deps = " ++ show (fst (unzip deps)) + case getOpt Permute options args of + (opts, fnames@(_:_), _) -> + let doTest = Test `elem` opts + computeDeps = NoDeps `notElem` opts in + doOneProgram computeDeps doTest fnames + _ -> error "usage: ./Driver [filename]" + where doOneProgram :: Bool -> Bool -> [FilePath] -> IO () + doOneProgram computeDeps doTest fns = do + putStrLn $ "========== Program " ++ (show fns) ++ " =============" + deps <- if computeDeps + then + getDependencies fns + else (liftM catMaybes) (mapM findModuleDirect fns) + putStrLn $ "deps = " ++ show (fst (unzip deps)) {- Note that we scan over the libraries twice: first to gather together all type sigs, then to typecheck them @@ -104,17 +119,30 @@ main = do let succeeded = length modules putStrLn ("Finished typechecking. Successfully checked " ++ show succeeded) - result <- evalProgram modules + overridden <- override modules + result <- evalProgram overridden putStrLn ("Result = " ++ show result) putStrLn "All done\n=============================================" - mkInitialEnv :: [Module] -> IO Menv - mkInitialEnv libs = foldM mkTypeEnv initialEnv libs + mkInitialEnv :: [Module] -> IO Menv + mkInitialEnv libs = foldM mkTypeEnv initialEnv libs - mkTypeEnv :: Menv -> Module -> IO Menv - mkTypeEnv globalEnv m@(Module mn _ _) = + mkTypeEnv :: Menv -> Module -> IO Menv + mkTypeEnv globalEnv m@(Module mn _ _) = catch (return (envsModule globalEnv m)) handler where handler e = do putStrLn ("WARNING: mkTypeEnv caught an exception " ++ show e ++ " while processing " ++ show mn) return globalEnv + +findModuleDirect :: FilePath -> IO (Maybe (FilePath, Module)) +-- kludge to let us run "make libtest" -- +-- this module (in the Cabal package) causes an uncaught exception +-- from Prelude.chr, which I haven't been able to track down +findModuleDirect fn | "PackageDescription.hcr" `isSuffixOf` fn = return Nothing +findModuleDirect fn = do + putStrLn $ "Finding " ++ show fn + res <- parseCore fn + case res of + Left err -> error (show err) + Right m -> return $ Just (fn,m) \ No newline at end of file diff --git a/utils/ext-core/Interp.hs b/utils/ext-core/Interp.hs index 3f07922..2c3f65e 100644 --- a/utils/ext-core/Interp.hs +++ b/utils/ext-core/Interp.hs @@ -437,6 +437,7 @@ evalPrimop "negateIntzh" = primIntUnop (\ i -> -i) evalPrimop "quotIntzh" = primIntBinop quot evalPrimop "remIntzh" = primIntBinop rem evalPrimop "subIntCzh" = primSubIntC +evalPrimop "addIntCzh" = primAddIntC evalPrimop "mulIntMayOflozh" = primIntBinop (\ i j -> case (fromIntegral i, fromIntegral j) of @@ -489,14 +490,20 @@ primCharCmpOp op [Vimm (PCharzh c), Vimm (PCharzh d)] = mkBool (c `op` d) primCharCmpOp _ _ = error "primCharCmpOp: wrong number of arguments" primSubIntC :: [Value] -> Eval Value -primSubIntC [Vimm (PIntzh i1), Vimm (PIntzh i2)] = +primSubIntC vs = carryOp subIntC# vs + +primAddIntC :: [Value] -> Eval Value +primAddIntC vs = carryOp addIntC# vs + +carryOp :: (Int# -> Int# -> (# Int#, Int# #)) -> [Value] -> Eval Value +carryOp op [Vimm (PIntzh i1), Vimm (PIntzh i2)] = case (fromIntegral i1, fromIntegral i2) of (I# int1, I# int2) -> - case (int1 `subIntC#` int2) of + case (int1 `op` int2) of (# res1, res2 #) -> return $ Vutuple [Vimm (PIntzh (fromIntegral (I# res1))), Vimm (PIntzh (fromIntegral (I# res2)))] -primSubIntC _ = error "primSubIntC: wrong number of arguments" +carryOp _ _ = error "carryOp: wrong number of arguments" primInt2Double :: [Value] -> Eval Value primInt2Double [Vimm (PIntzh i)] = diff --git a/utils/ext-core/Makefile b/utils/ext-core/Makefile index c26523a..ec228e7 100644 --- a/utils/ext-core/Makefile +++ b/utils/ext-core/Makefile @@ -13,7 +13,7 @@ prims: ../../compiler/prelude/primops.txt # The following assumes that you've built all the GHC libs with -fext-core... libtest: all - ./Driver `find ../../libraries -print | grep .hcr$$ | grep -v bootstrapping` + ./Driver -n `find ../../libraries -print | grep .hcr$$ | grep -v bootstrapping` # ...or built all the nofib programs with -fext-core. nofibtest: all diff --git a/utils/ext-core/Overrides.hs b/utils/ext-core/Overrides.hs new file mode 100644 index 0000000..1542e09 --- /dev/null +++ b/utils/ext-core/Overrides.hs @@ -0,0 +1,93 @@ +{-# OPTIONS -Wall #-} +{- + This module encapsulates some magic regarding overridden modules. + + In the interpreter, we use "overridden" versions of certain + standard GHC library modules in order to avoid implementing + more primitives than we need to implement to run simple programs. + So, after typechecking but before interpretation, references to overridden + modules are resolved to references to modules in our simplified + version of the standard library. + + It's kind of ugly. +-} +module Overrides (override) where + +import Core +import Encoding +import ParsecParser +import Prims + +import Data.Generics +import System.FilePath + +override :: [Module] -> IO [Module] +override = mapM overrideOne + where overrideOne :: Module -> IO Module + overrideOne (Module mn _ _) | mn `elem` wiredInModules = + findWiredInModule mn >>= (return . snd) + overrideOne m = return m + +-- This function encapsulates all the business with overriden modules. +-- The story is that if an "overridden" module exists for the given +-- module, then we parse it in and rewrite all occurrences of the "base-extcore" +-- package name inside it to "base". We have to do this b/c when compiling +-- the overridden modules, we gave the package name "base-extcore", because +-- GHC gets unhappy if we try to make it part of the "base" package. +-- Was that clear? (No.) +findWiredInModule :: AnMname -> IO (FilePath, Module) +findWiredInModule m@(M (pn, encHier, encLeafName)) = + findModuleIO (Just munged) (wiredInFileName m) + where hier = map zDecodeString encHier + leafName = zDecodeString encLeafName + munged = + M (pn, map (\ p -> if p == "GHC_ExtCore" then "GHC" else p) hier, + leafName) + + +wiredInModules :: [AnMname] +wiredInModules = + map (\ m -> (mkBaseMname m)) ["Handle", "IO", "Unicode"] + +wiredInFileName :: AnMname -> FilePath +wiredInFileName (M (_,_,leafName)) = + "./lib/GHC_ExtCore/" leafName `addExtension` "hcr" + + +mungePackageName :: Module -> Module +-- for now: just substitute "base-extcore" for "base" +-- and "GHC" for "GHC_ExtCore" in every module name +mungePackageName m@(Module mn _ _) = everywhere (mkT mungeMname) + (everywhere (mkT mungePname) + (everywhere (mkT mungeVarName) m)) + where mungePname (P s) | s == zEncodeString overriddenPname = + (P "base") + mungePname p = p + -- rewrite uses of fake primops + mungeVarName (Var (Just mn', v)) + | mn' == mn && v `elem` (fst (unzip newPrimVars)) = + Var (Just primMname, v) + mungeVarName e = e + +mungeMname :: AnMname -> AnMname +mungeMname (M (pname, (hd:rest), leaf)) + | zDecodeString hd == "GHC_ExtCore" = + (M (pname, ("GHC":rest), leaf)) +mungeMname mn = mn + +overriddenPname :: String +overriddenPname = "base-extcore" + + +findModuleIO :: Mname -> FilePath -> IO (FilePath, Module) +findModuleIO trueName fp = do + res <- parseCore fp + case res of + Left _ -> error ("findModule: error parsing dependency " ++ fp) + Right parsedMod -> do + let resultMod@(Module _ _ _) = + case trueName of + Just _ -> mungePackageName parsedMod + Nothing -> parsedMod + return (fp, resultMod) + diff --git a/utils/ext-core/ParsecParser.hs b/utils/ext-core/ParsecParser.hs index ab0d284..41a18a5 100644 --- a/utils/ext-core/ParsecParser.hs +++ b/utils/ext-core/ParsecParser.hs @@ -141,12 +141,10 @@ coreCdef = do tys <- sepBy coreAtySaturated whiteSpace return $ Constr dataConName tBinds tys -coreTRep :: Parser (Maybe Ty) +coreTRep :: Parser Ty -- note that the "=" is inside here since if there's -- no rhs for the newtype, there's no "=" -coreTRep = optionMaybe (do - symbol "=" - try coreType) +coreTRep = symbol "=" >> try coreType coreType :: Parser Ty coreType = coreForallTy <|> (do diff --git a/utils/ext-core/Prims.hs b/utils/ext-core/Prims.hs index 43c687c..5193848 100644 --- a/utils/ext-core/Prims.hs +++ b/utils/ext-core/Prims.hs @@ -29,13 +29,11 @@ primEnv = Envs {tcenv_=efromlist $ map (\ (t,k) -> (t,Kind k)) $ (snd tcMutableByteArrayzh, ktMutableByteArrayzh)] ++ ([(snd $ tcUtuple n, ktUtuple n) | n <- [1..maxUtuple]] ++ ((snd tcArrow,ktArrow):primTcs)), - tsenv_=eempty, cenv_=efromlist primDcs, venv_=efromlist (newPrimVars ++ opsState ++ primVals)} errorEnv :: Envs errorEnv = Envs {tcenv_=eempty, - tsenv_=eempty, cenv_=eempty, venv_=efromlist errorVals} diff --git a/utils/ext-core/Printer.hs b/utils/ext-core/Printer.hs index 0ae4b18..0acdc5d 100644 --- a/utils/ext-core/Printer.hs +++ b/utils/ext-core/Printer.hs @@ -69,9 +69,7 @@ ptdef (Data qtcon tbinds cdefs) = ptdef (Newtype qtcon coercion tbinds tyopt) = text "%newtype" <+> pqname qtcon <+> pqname coercion <+> (hsep (map ptbind tbinds)) $$ indent repclause - where repclause = case tyopt of - Just ty -> char '=' <+> pty ty - Nothing -> empty + where repclause = char '=' <+> pty tyopt pcdef (Constr qdcon tbinds tys) = (pqname qdcon) <+> (sep [hsep (map pattbind tbinds),sep (map paty tys)]) diff --git a/utils/ext-core/README b/utils/ext-core/README index 6091935..bb5f3aa 100644 --- a/utils/ext-core/README +++ b/utils/ext-core/README @@ -6,20 +6,26 @@ tjc April/May 2008: ==== Notes ==== -The checker should work on most programs. Bugs I'm aware of: -1. There's some business I don't quite understand involving - coercions and subkinding (for details, see: - http://www.haskell.org/pipermail/cvs-ghc/2008-April/041949.html) - This shows up when typechecking a few of the library modules. +The checker should work on most programs. Bugs (and infelicities) +I'm aware of: -2. There's some weirdness involving funny character literals. This can +1. There's some weirdness involving funny character literals. This can be fixed by writing a new lexer for chars rather than using Parsec's built-in charLiteral lexer. But I haven't done that. -3. When typechecking the ghc-prim:GHC.PrimopWrappers library module, - some declarations seem to have the wrong type signature (due to - confusion between (forall (t::*) ...) and (forall (t::?) ...).) - This is because the ? kind is not expressible in Haskell. +2. The test driver attempts to find module dependencies automatically, + but it's slow. You can turn it off with the "-n" flag to the driver, + and specify all dependencies on the command line (you have to include + standard library dependencies too.) + * It would help to cache dependency info for standard libraries + in a file, or something, but that's future work. + +3. To avoid implementing some of the I/O primitives and foreign calls, + I use a gross hack involving replacing certain standard library + modules with simplified versions (found under lib/) that depend on + fake "primops" that the Core interpreter implements. This makes it + difficult (if not impossible) to load optimized versions of standard + libraries right now. Fixing this is future work too. Typechecking all the GHC libraries eats about a gig of heap and takes a long time. I blame Parsec. (Someone who was bored, or understood happy -- 1.7.10.4