import Maybe
import Control.Monad.Reader
--- just for printing warnings
-import System.IO.Unsafe
import Core
import Printer()
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
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)
-- 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
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
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))),
(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)
++ " 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
(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 ()
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)))
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" ++
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
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
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)
"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
("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')
[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
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
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)
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)
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)
-- 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
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
-- 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
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
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
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
{-# 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
-- 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]
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
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)
_ -> 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)
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
++ 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/"
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
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/"
-- 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"
_ -> "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
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
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
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
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)] =
# 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
--- /dev/null
+{-# 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)
+
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
(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}
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)])
==== 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
projects / ghc-hetmet.git / commitdiff