-module Check where
+{-# OPTIONS -Wall -fno-warn-name-shadowing #-}
+module Check(
+ checkModule, envsModule,
+ checkExpr, checkType,
+ primCoercionError,
+ Menv, Venv, Tvenv, Envs(..),
+ CheckRes(..), splitTy, substl) where
import Maybe
import Control.Monad.Reader
import Core
-import Printer
+import Printer()
import List
import Env
+import PrimEnv
{- Checking is done in a simple error monad. In addition to
allowing errors to be captured, this makes it easy to guarantee
instance Monad CheckRes where
OkC a >>= k = k a
- FailC s >>= k = fail s
+ FailC s >>= _ = fail s
return = OkC
fail = FailC
{- Environments. -}
type Tvenv = Env Tvar Kind -- type variables (local only)
-type Tcenv = Env Tcon Kind -- type constructors
+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
+ deriving Show
-{- Extend an environment, checking for illegal shadowing of identifiers. -}
-extendM :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
-extendM env (k,d) =
+{- Extend an environment, checking for illegal shadowing of identifiers (for term
+ variables -- shadowing type variables is allowed.) -}
+data EnvType = Tv | NotTv
+ deriving Eq
+
+extendM :: (Ord a, Show a) => EnvType -> Env a b -> (a,b) -> CheckResult (Env a b)
+extendM envType env (k,d) =
case elookup env k of
- Just _ -> fail ("multiply-defined identifier: " ++ show k)
- Nothing -> return (eextend env (k,d))
+ Just _ | envType == NotTv -> 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
+
+extendTvenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
+extendTvenv = extendM Tv
lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult b
lookupM env k =
{- Main entry point. -}
checkModule :: Menv -> Module -> CheckRes Menv
-checkModule globalEnv mod@(Module mn tdefs vdefgs) =
+checkModule globalEnv (Module mn tdefs vdefgs) =
runReaderT
(do (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs
- (e_venv,l_venv) <- foldM (checkVdefg True (tcenv,tsenv,eempty,cenv))
+ (e_venv,_) <- foldM (checkVdefg True (tcenv,tsenv,eempty,cenv))
(eempty,eempty)
vdefgs
return (eextend globalEnv
(mn,Envs{tcenv_=tcenv,tsenv_=tsenv,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, tsenv, cenv) = mkTypeEnvsNoChecking tdefs
+ e_venv = foldr vdefgTypes eempty vdefgs in
+ eextend globalEnv (mn,
+ (Envs{tcenv_=tcenv,tsenv_=tsenv,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 ((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
where
ch (Data (m,c) tbs _) =
do mn <- getMname
requireModulesEq m mn "data type declaration" tdef False
- tcenv' <- extendM tcenv (c,k)
+ tcenv' <- extendM NotTv tcenv (c, Kind k)
return (tcenv',tsenv)
where k = foldr Karrow Klifted (map snd tbs)
- -- TODO
- ch (Newtype (m,c) tbs axiom rhs) =
+ ch (Newtype (m,c) tbs ((_,coercion),cTbs,coercionKind) rhs) =
do mn <- getMname
requireModulesEq m mn "newtype declaration" tdef False
- tcenv' <- extendM tcenv (c,k)
+ tcenv' <- extendM NotTv tcenv (c, Kind k)
+ -- add newtype axiom to env
+ tcenv'' <- extendM NotTv tcenv'
+ (coercion, Coercion $ DefinedCoercion cTbs coercionKind)
tsenv' <- case rhs of
Nothing -> return tsenv
- Just rep -> extendM tsenv (c,(map fst tbs,rep))
- return (tcenv', tsenv')
+ Just rep -> extendM NotTv tsenv (c,(map fst tbs,rep))
+ return (tcenv'', tsenv')
+ where k = foldr Karrow Klifted (map snd tbs)
+
+processTdef0NoChecking :: (Tcenv,Tsenv) -> Tdef -> (Tcenv,Tsenv)
+processTdef0NoChecking (tcenv,tsenv) tdef = ch tdef
+ where
+ ch (Data (_,c) tbs _) = (eextend tcenv (c, Kind k), tsenv)
+ where k = foldr Karrow Klifted (map snd tbs)
+ ch (Newtype (_,c) tbs ((_,coercion),cTbs,coercionKind) rhs) =
+ let tcenv' = eextend tcenv (c, Kind k)
+ -- add newtype axiom to env
+ tcenv'' = eextend tcenv'
+ (coercion, Coercion $ DefinedCoercion cTbs coercionKind)
+ tsenv' = maybe tsenv
+ (\ rep -> eextend tsenv (c, (map fst tbs, rep))) rhs in
+ (tcenv'', tsenv')
where k = foldr Karrow Klifted (map snd tbs)
checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
where
ch (Data (_,c) utbs cdefs) =
do cbinds <- mapM checkCdef cdefs
- foldM extendM cenv cbinds
+ foldM (extendM NotTv) cenv cbinds
where checkCdef (cdef@(Constr (m,dcon) etbs ts)) =
do mn <- getMname
requireModulesEq m mn "constructor declaration" cdef
False
- tvenv <- foldM extendM eempty tbs
+ tvenv <- foldM (extendM Tv) eempty tbs
ks <- mapM (checkTy (tcenv,tvenv)) ts
mapM_ (\k -> require (baseKind k)
("higher-order kind in:\n" ++ show cdef ++ "\n" ++
(foldr tArrow
(foldl Tapp (Tcon (Just mn,c))
(map (Tvar . fst) utbs)) ts) tbs
- -- TODO
- ch (tdef@(Newtype c tbs axiom (Just t))) =
- do tvenv <- foldM extendM eempty tbs
+ ch (tdef@(Newtype _ tbs (_, coTbs, (coLhs, coRhs)) (Just t))) =
+ do tvenv <- foldM (extendM Tv) eempty tbs
k <- checkTy (tcenv,tvenv) t
- require (k `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
+ -- Makes sure GHC is eta-expanding things properly
+ require (length tbs == length coTbs) $
+ ("Arity mismatch between newtycon and newtype coercion: "
+ ++ show tdef)
+ require (k `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
+ axiomTvenv <- foldM (extendM Tv) eempty coTbs
+ kLhs <- checkTy (tcenv,axiomTvenv) coLhs
+ kRhs <- checkTy (tcenv,axiomTvenv) coRhs
+ require (kLhs `eqKind` kRhs)
+ ("Kind mismatch in newtype axiom types: " ++ show tdef
+ ++ " kinds: " ++
+ (show kLhs) ++ " and " ++ (show kRhs))
return cenv
- ch (tdef@(Newtype c tbs axiom Nothing)) =
+ ch (Newtype _ _ _ Nothing) =
{- should only occur for recursive Newtypes -}
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, Tsenv, Cenv)
mkTypeEnvs tdefs = do
(tcenv, tsenv) <- foldM checkTdef0 (eempty,eempty) tdefs
cenv <- foldM (checkTdef tcenv) eempty tdefs
return (tcenv, tsenv, cenv)
+mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Tsenv, Cenv)
+mkTypeEnvsNoChecking tdefs =
+ let (tcenv, tsenv) = foldl processTdef0NoChecking (eempty,eempty) tdefs
+ cenv = foldl processCdef eempty tdefs in
+ (tcenv, tsenv, cenv)
+
requireModulesEq :: Show a => Mname -> AnMname -> String -> a
-> Bool -> CheckResult ()
requireModulesEq (Just mn) m msg t _ = require (mn == m) (mkErrMsg msg t)
-requireModulesEq Nothing m msg t emptyOk = require emptyOk (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 top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg =
case vdefg of
Rec vdefs ->
- do e_venv' <- foldM extendM e_venv e_vts
- l_venv' <- foldM extendM l_venv l_vts
+ do e_venv' <- foldM extendVenv e_venv e_vts
+ l_venv' <- foldM extendVenv l_venv l_vts
let env' = (tcenv,tsenv,tvenv,cenv,e_venv',l_venv')
- mapM_ (\ (vdef@(Vdef ((m,v),t,e))) ->
+ mapM_ (\ (vdef@(Vdef ((m,_),t,e))) ->
do mn <- getMname
requireModulesEq m mn "value definition" vdef True
k <- checkTy (tcenv,tvenv) t
l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs]
Nonrec (vdef@(Vdef ((m,v),t,e))) ->
do mn <- getMname
- requireModulesEq m mn "value definition" vdef True
+ -- TODO: document this weirdness
+ let isZcMain = vdefIsMainWrapper mn m
+ unless isZcMain $
+ requireModulesEq m mn "value definition" vdef True
k <- checkTy (tcenv,tvenv) t
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)
+ require ((not top_level) || (not (k `eqKind` Kunlifted)))
+ ("top-level unlifted kind in:\n" ++ show vdef)
t' <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) e
requireM (equalTy tsenv t t')
- ("declared type doesn't match expression type in:\n" ++ show vdef ++ "\n" ++
+ ("declared type doesn't match expression type in:\n"
+ ++ show vdef ++ "\n" ++
"declared type: " ++ show t ++ "\n" ++
"expression type: " ++ show t')
if isNothing m then
- do l_venv' <- extendM l_venv (v,t)
+ do l_venv' <- extendVenv l_venv (v,t)
return (e_venv,l_venv')
else
- do e_venv' <- extendM e_venv (v,t)
+ -- awful, but avoids name shadowing --
+ -- otherwise we'd have two bindings for "main"
+ do e_venv' <- if isZcMain
+ then return e_venv
+ else extendVenv e_venv (v,t)
return (e_venv',l_venv)
+vdefIsMainWrapper :: AnMname -> Mname -> Bool
+vdefIsMainWrapper enclosing defining =
+ enclosing == mainMname && defining == wrapperMainMname
+
checkExpr :: AnMname -> Menv -> [Tdef] -> Venv -> Tvenv
-> Exp -> Ty
-checkExpr mn menv tdefs venv tvenv e = case (runReaderT (do
+checkExpr mn menv tdefs venv tvenv e = case runReaderT (do
(tcenv, tsenv, cenv) <- mkTypeEnvs tdefs
- checkExp (tcenv, tsenv, tvenv, cenv, venv, eempty) e)
- (mn, menv)) of
- OkC t -> t
- FailC s -> reportError s
+ -- 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
+ Nothing -> reportError e ("checkExpr: Environment for " ++
+ show mn ++ " not found")) (mn,menv) of
+ OkC t -> t
+ FailC s -> reportError e s
+
+checkType :: AnMname -> Menv -> [Tdef] -> Tvenv -> Ty -> Kind
+checkType mn menv tdefs tvenv t = case runReaderT (do
+ (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,tsenv,tvenv,cenv,e_venv,l_venv) = ch
where
ch e0 =
case e0 of
_ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++
"operator type: " ++ show t1)
Lam (Tb tb) e ->
- do tvenv' <- extendM tvenv tb
+ do tvenv' <- extendTvenv tvenv tb
t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv) e
return (Tforall tb t)
Lam (Vb (vb@(_,vt))) e ->
require (baseKind k)
("higher-order kind in:\n" ++ show e0 ++ "\n" ++
"kind: " ++ show k)
- l_venv' <- extendM l_venv vb
+ l_venv' <- extendVenv l_venv vb
t <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') e
require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0)
return (tArrow vt t)
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' <- extendM l_venv (v,t)
+ _ -> 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)
" match case return type in:\n" ++ show e0 ++ "\n" ++
"alt type: " ++ show t ++ " return type: " ++ show resultTy)
return t
- Cast e t ->
- do ch e
- checkTy (tcenv,tvenv) t
- return t
- Note s e ->
+ c@(Cast e t) ->
+ do eTy <- ch e
+ k <- checkTy (tcenv,tvenv) t
+ case k of
+ (Keq fromTy toTy) -> do
+ require (eTy == fromTy) ("Type mismatch in cast: c = "
+ ++ show c ++ " and " ++ show eTy
+ ++ " and " ++ show fromTy)
+ return toTy
+ _ -> fail ("Cast with non-equality kind: " ++ show e
+ ++ " and " ++ show t ++ " has kind " ++ show k)
+ Note _ e ->
ch e
External _ t ->
do checkTy (tcenv,eempty) t {- external types must be closed -}
("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 extendM tvenv etbs
+ tvenv' <- foldM extendTvenv tvenv etbs
{- check term variables -}
let vts = map snd vbs
mapM_ (\vt -> require ((not . isUtupleTy) vt)
("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 extendM l_venv vbs
+ l_venv' <- foldM extendVenv l_venv vbs
t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv') e
checkTy (tcenv,tvenv) t {- check that existentials don't escape in result type -}
return t
checkExp env e
checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
-checkTy (tcenv,tvenv) = ch
+checkTy es@(tcenv,tvenv) t = ch t
where
ch (Tvar tv) = lookupM tvenv tv
- ch (Tcon qtc) = qlookupM tcenv_ tcenv eempty qtc
+ 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)) =
- do k1 <- ch t1
- k2 <- ch t2
- case k1 of
- Karrow k11 k12 ->
- do require (k2 `subKindOf` k11)
- ("kinds don't match in type application: " ++ show t ++ "\n" ++
- "operator kind: " ++ show k11 ++ "\n" ++
- "operand kind: " ++ show k2)
- return k12
- _ -> fail ("applied type has non-arrow kind: " ++ show t)
+ case splitTyConApp_maybe t of
+ Just (tc, tys) -> do
+ tcK <- qlookupM tcenv_ tcenv eempty tc
+ case tcK of
+ Kind _ -> checkTapp t1 t2
+ Coercion (DefinedCoercion tbs (from,to)) -> do
+ -- makes sure coercion is fully applied
+ require (length tys == length tbs) $
+ ("Arity mismatch in coercion app: " ++ show t)
+ let (tvs, tks) = unzip tbs
+ argKs <- mapM (checkTy es) tys
+ require (all (uncurry eqKind) (zip tks argKs))
+ ("Kind mismatch in coercion app: " ++ show tks
+ ++ " and " ++ show argKs ++ " t = " ++ show t)
+ return $ Keq (substl tvs tys from) (substl tvs tys to)
+ Nothing -> checkTapp t1 t2
+ where checkTapp t1 t2 = do
+ k1 <- ch t1
+ k2 <- ch t2
+ case k1 of
+ Karrow k11 k12 ->
+ case k2 of
+ Keq eqTy1 eqTy2 -> do
+ -- Distribute the type operator over the
+ -- coercion
+ subK1 <- checkTy es eqTy1
+ subK2 <- checkTy es eqTy2
+ require (subK2 `subKindOf` k11 &&
+ subK1 `subKindOf` k11) $
+ kindError
+ return $ Keq (Tapp t1 eqTy1) (Tapp t1 eqTy2)
+ _ -> 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' <- extendM tvenv tb
- checkTy (tcenv,tvenv') t
-
+ do tvenv' <- extendTvenv tvenv tb
+ k <- checkTy (tcenv,tvenv') t
+ return $ case k of
+ -- distribute the forall
+ Keq t1 t2 -> Keq (Tforall tb t1) (Tforall tb t2)
+ _ -> k
+ ch (TransCoercion t1 t2) = do
+ k1 <- checkTy es t1
+ k2 <- checkTy es t2
+ case (k1, k2) of
+ (Keq ty1 ty2, Keq ty3 ty4) | ty2 == ty3 ->
+ return $ Keq ty1 ty4
+ _ -> fail ("Bad kinds in trans. coercion: " ++
+ show k1 ++ " " ++ show k2)
+ ch (SymCoercion t1) = do
+ k <- checkTy es t1
+ case k of
+ Keq ty1 ty2 -> return $ Keq ty2 ty1
+ _ -> fail ("Bad kind in sym. coercion: "
+ ++ show k)
+ ch (UnsafeCoercion t1 t2) = do
+ checkTy es t1
+ checkTy es t2
+ return $ Keq t1 t2
+ ch (LeftCoercion t1) = do
+ k <- checkTy es t1
+ case k of
+ Keq (Tapp u _) (Tapp w _) -> return $ Keq u w
+ _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
+ ch (RightCoercion t1) = do
+ k <- checkTy es t1
+ case k of
+ Keq (Tapp _ v) (Tapp _ x) -> return $ Keq v x
+ _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
+
{- Type equality modulo newtype synonyms. -}
equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool
equalTy tsenv 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
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)
+ 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 t ts =
do t' <- expand t
return (foldl Tapp t' ts)
-
-mlookupM :: (Envs -> Env a b) -> Env a b -> Env a b -> Mname
+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
-mlookupM selector external_env _ (Just m) = do
+mlookupM selector external_env local_env (Just m) = do
mn <- getMname
if m == mn
then return external_env
globalEnv <- getGlobalEnv
case elookup globalEnv m of
Just env' -> return (selector env')
- Nothing -> fail ("Check: undefined module name: " ++ show m)
+ Nothing -> fail ("Check: undefined module name: "
+ ++ show m ++ show (edomain local_env))
-qlookupM :: (Ord a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b
+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) =
+qlookupM selector external_env local_env (m,k) =
do env <- mlookupM selector external_env local_env m
- lookupM env k
-
+ lookupM env k
checkLit :: Lit -> CheckResult Ty
checkLit (Literal lit t) =
case lit of
- -- TODO: restore commented-out stuff.
Lint _ ->
- do {- require (elem t [tIntzh, {- tInt32zh,tInt64zh, -} tWordzh, {- tWord32zh,tWord64zh, -} tAddrzh, tCharzh])
- ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
+ do require (t `elem` intLitTypes)
+ ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
return t
Lrational _ ->
- do {- require (elem t [tFloatzh,tDoublezh])
- ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
+ do require (t `elem` ratLitTypes)
+ ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
return t
Lchar _ ->
- do {- require (t == tCharzh)
- ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
+ do require (t `elem` charLitTypes)
+ ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
return t
Lstring _ ->
- do {- require (t == tAddrzh)
- ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
+ do require (t `elem` stringLitTypes)
+ ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
return t
{- Utilities -}
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)
where free = foldr union [] (map (freeTvars.snd) env)
t' = freshTvar free
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
{- 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
+
-- todo
-reportError s = error $ ("Core parser error: checkExpr failed with " ++ s)
+reportError :: Show a => a -> String -> b
+reportError e s = error $ ("Core type error: checkExpr failed with "
+ ++ s ++ " and " ++ show e)
+
module Core where
+import Encoding
+
import List (elemIndex)
data Module
= Constr (Qual Dcon) [Tbind] [Ty]
-- Newtype coercion
-type Axiom = (Qual Tcon, Kind)
+type Axiom = (Qual Tcon, [Tbind], (Ty,Ty))
data Vdefg
= Rec [Vdef]
| Tcon (Qual Tcon)
| Tapp Ty Ty
| Tforall Tbind Ty
+-- Wired-in coercions:
+-- These are primitive tycons in GHC, but in ext-core,
+-- we make them explicit, to make the typechecker
+-- somewhat more clear.
+ | TransCoercion Ty Ty
+ | SymCoercion Ty
+ | UnsafeCoercion Ty Ty
+ | LeftCoercion Ty
+ | RightCoercion Ty
data Kind
= Klifted
| Karrow Kind Kind
| Keq Ty Ty
+-- A CoercionKind isn't really a Kind at all, but rather,
+-- corresponds to an arbitrary user-declared axiom.
+-- A tycon whose CoercionKind is (DefinedCoercion <tbs> (from, to))
+-- represents a tycon with arity (length tbs), whose kind is
+-- (from :=: to) (modulo substituting type arguments.
+-- It's not a Kind because a coercion must always be fully applied:
+-- whenever we see a tycon that has such a CoercionKind, it must
+-- be fully applied if it's to be assigned an actual Kind.
+-- So, a CoercionKind *only* appears in the environment (mapping
+-- newtype axioms onto CoercionKinds).
+-- Was that clear??
+data CoercionKind =
+ DefinedCoercion [Tbind] (Ty,Ty)
+
+-- The type constructor environment maps names that are
+-- either type constructors or coercion names onto either
+-- kinds or coercion kinds.
+data KindOrCoercion = Kind Kind | Coercion CoercionKind
+
data Lit = Literal CoreLit Ty
deriving Eq -- with nearlyEqualTy
-- module namespace, either when printing out
-- Core or (probably preferably) in a
-- preprocessor.
--- The empty module name (as in an unqualified name)
--- is represented as Nothing.
+-- We represent the empty module name (as in an unqualified name)
+-- with Nothing.
type Mname = Maybe AnMname
type AnMname = (Pname, [Id], Id)
eqKind _ _ = False -- no Keq kind is ever equal to any other...
-- maybe ok for now?
---- tjc: I haven't looked at the rest of this file. ---
+splitTyConApp_maybe :: Ty -> Maybe (Qual Tcon,[Ty])
+splitTyConApp_maybe (Tvar _) = Nothing
+splitTyConApp_maybe (Tcon t) = Just (t,[])
+splitTyConApp_maybe (Tapp rator rand) =
+ case (splitTyConApp_maybe rator) of
+ Just (r,rs) -> Just (r,rs++[rand])
+ Nothing -> case rator of
+ 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
subKindOf :: Kind -> Kind -> Bool
_ `subKindOf` Kopen = True
+(Karrow a1 r1) `subKindOf` (Karrow a2 r2) =
+ a2 `subKindOf` a1 && (r1 `subKindOf` r2)
k1 `subKindOf` k2 = k1 `eqKind` k2 -- doesn't worry about higher kinds
baseKind :: Kind -> Bool
isPrimVar (Just mn,_) = mn == primMname
isPrimVar _ = False
-primMname = mkBaseMname "Prim"
+primMname = mkPrimMname "Prim"
errMname = mkBaseMname "Err"
-mkBaseMname :: Id -> AnMname
+mkBaseMname,mkPrimMname :: Id -> AnMname
mkBaseMname mn = (basePkg, ghcPrefix, mn)
+mkPrimMname mn = (primPkg, ghcPrefix, mn)
basePkg = "base"
mainPkg = "main"
+primPkg = zEncodeString "ghc-prim"
ghcPrefix = ["GHC"]
mainPrefix = []
baseMname = mkBaseMname "Base"
+boolMname = mkPrimMname "Bool"
mainVar = qual mainMname "main"
mainMname = (mainPkg, mainPrefix, "Main")
+wrapperMainMname = Just (mainPkg, mainPrefix, "ZCMain")
tcArrow :: Qual Tcon
tcArrow = (Just primMname, "ZLzmzgZR")
{- Unboxed tuples -}
--- tjc: not sure whether anything that follows is right
-
maxUtuple :: Int
maxUtuple = 100
isUtupleTy _ = False
dcUtuple :: Int -> Qual Dcon
-dcUtuple n = (Just primMname,"ZdwZ" ++ (show n) ++ "H")
+-- TODO: Seems like Z2H etc. appears in ext-core files,
+-- not $wZ2H etc. Is this right?
+dcUtuple n = (Just primMname,"Z" ++ (show n) ++ "H")
isUtupleDc :: Qual Dcon -> Bool
isUtupleDc dc = dc `elem` [dcUtuple n | n <- [1..maxUtuple]]
Note that, if compiled under GHC, this requires a very large heap to run!
-}
+import Control.Exception
+import Data.List
+import Maybe
import Monad
-import System.Environment
+import Prelude hiding (catch)
import System.Cmd
+import System.Environment
import System.Exit
+import System.FilePath
import Core
import Printer
-- You may need to change this.
baseDir = "../../libraries/"
---------
+-- change to True to typecheck library files as well as reading type signatures
+typecheckLibs = False
+
+-- You shouldn't *need* to change anything below this line...
+libDir = map (baseDir ++)
--- Code for checking that the external and GHC printers print the same results
+-- Code to check that the external and GHC printers print the same results
testFlag = "-t"
validateResults :: FilePath -> FilePath -> IO ()
_ -> "Error diffing files: " ++ origFile ++ " " ++ genFile
------------------------------------------------------------------------------
-process :: Bool -> (Check.Menv,[Module]) -> String -> IO (Check.Menv,[Module])
-process doTest (senv,modules) f =
- do putStrLn ("Processing " ++ f)
+process :: Bool -> (Check.Menv,[Module]) -> FilePath
+ -> IO (Check.Menv,[Module])
+process doTest (senv,modules) f = catch
+ (do putStrLn ("Processing " ++ f)
resultOrErr <- parseCore f
case resultOrErr of
- Right m -> do
+ Right m@(Module mn _ _) -> do
putStrLn "Parse succeeded"
let outF = f ++ ".parsed"
writeFile outF (show m)
when doTest $ (validateResults f outF)
case checkModule senv m of
OkC senv' ->
- do putStrLn "Check succeeded"
+ do putStrLn $ "Check succeeded for " ++ show mn
let m' = prepModule senv' m
- {- writeFile (f ++ ".prepped") (show m') -}
- case checkModule senv m' of
+ let (dir,fname) = splitFileName f
+ let preppedFile = dir </> (fname ++ ".prepped")
+ writeFile preppedFile (show m')
+ case checkModule senv' m' of
OkC senv'' ->
do putStrLn "Recheck succeeded"
return (senv'',modules ++ [m'])
FailC s ->
do putStrLn ("Recheck failed: " ++ s)
error "quit"
- FailC s ->
- do putStrLn ("Check failed: " ++ s)
- error "quit"
- Left err -> do putStrLn ("Parse failed: " ++ show err)
- error "quit"
+ FailC s -> error ("Typechecking failed: " ++ s)
+ Left err -> error ("Parsing failed: " ++ show err)) handler
+ where handler e = do
+ putStrLn ("WARNING: we caught an exception " ++ show e
+ ++ " while processing " ++ f)
+ return (senv, modules)
main = do args <- getArgs
- let (doTest, fname) =
+ let (doTest, fnames) =
case args of
- (f:fn:_) | f == testFlag -> (True,fn)
- (fn:_) -> (False,fn)
+ (f:rest) | f == testFlag -> (True,rest)
+ rest@(_:_) -> (False,rest)
_ -> error $
"usage: ./Driver [filename]"
- mapM_ (process doTest (initialEnv,[])) (libs ++ [fname])
- (_,modules) <- foldM (process doTest) (initialEnv,[]) (libs ++ [fname])
- let result = evalProgram modules
- putStrLn ("Result = " ++ show result)
- putStrLn "All done"
- where libs = map (baseDir ++) ["./ghc-prim/GHC/Generics.hcr",
- "./ghc-prim/GHC/PrimopWrappers.hcr",
+ -- Note that we scan over the libraries twice:
+ -- first to gather together all type sigs, then to typecheck them
+ -- (the latter of which doesn't necessarily have to be done every time.)
+ -- This is a hack to avoid dealing with circular dependencies.
+
+ -- notice: scan over libraries *and* input modules first, not just libs
+ topEnv <- mkInitialEnv (map normalise libs `union` map normalise fnames)
+ doOneProgram doTest topEnv fnames
+ where doOneProgram doTest topEnv fns = do
+ putStrLn $ "========== Program " ++ (show fns) ++ " ================"
+ let numToDo = length (typecheckLibraries fns)
+ (_,modules) <- foldM (process doTest) (topEnv,[]) (typecheckLibraries fns)
+ let succeeded = length modules
+ putStrLn ("Finished typechecking. Successfully checked " ++ show succeeded
+ ++ " out of " ++ show numToDo ++ " modules.")
+ -- TODO: uncomment once interpreter works
+ --let result = evalProgram modules
+ --putStrLn ("Result = " ++ show result)
+ putStrLn "All done\n============================================="
+
+ typecheckLibraries = if typecheckLibs then (libs ++) else id
+ -- Just my guess as to what's needed from the base libs.
+ -- May well be missing some libraries and have some that
+ -- aren't commonly used.
+ -- However, the following is enough to check all of nofib.
+ -- This points to how nice it would be to have explicit import lists in ext-core.
+ libs = (libDir ["./ghc-prim/GHC/Generics.hcr",
"./ghc-prim/GHC/Bool.hcr",
"./ghc-prim/GHC/IntWord64.hcr",
"./base/GHC/Base.hcr",
+ "./base/Data/Tuple.hcr",
+ "./base/Data/Maybe.hcr",
+ "./integer-gmp/GHC/Integer.hcr",
"./base/GHC/List.hcr",
"./base/GHC/Enum.hcr",
+ "./base/Data/Ord.hcr",
+ "./base/Data/String.hcr",
+ "./base/Data/Either.hcr",
"./base/GHC/Show.hcr",
"./base/GHC/Num.hcr",
"./base/GHC/ST.hcr",
- "./base/GHC/Real.hcr",
"./base/GHC/STRef.hcr",
"./base/GHC/Arr.hcr",
- "./base/GHC/Float.hcr",
- "./base/GHC/Read.hcr",
- "./base/GHC/Ptr.hcr",
- "./base/GHC/Word.hcr",
+ "./base/GHC/Real.hcr",
+ "./base/Control/Monad.hcr",
"./base/GHC/Int.hcr",
"./base/GHC/Unicode.hcr",
- "./base/GHC/IOBase.hcr",
+ "./base/Text/ParserCombinators/ReadP.hcr",
+ "./base/Text/Read/Lex.hcr",
+ "./base/Text/ParserCombinators/ReadPrec.hcr",
+ "./base/GHC/Read.hcr",
+ "./base/GHC/Word.hcr",
+ "./base/Data/HashTable.hcr",
+ "./base/Unsafe/Coerce.hcr",
+ "./base/Foreign/Storable.hcr",
+ "./base/Foreign/C/Types.hcr",
+ "./base/GHC/IOBase.hcr",
+ "./base/GHC/ForeignPtr.hcr",
+ "./base/Data/Typeable.hcr",
+ "./base/Data/Dynamic.hcr",
"./base/GHC/Err.hcr",
+ "./base/Data/List.hcr",
+ "./base/Data/Char.hcr",
+ "./base/GHC/Pack.hcr",
+ "./base/GHC/Storable.hcr",
+ "./base/System/IO/Error.hcr",
+ "./base/Foreign/Ptr.hcr",
+ "./base/Foreign/Marshal/Error.hcr",
+ "./base/Foreign/ForeignPtr.hcr",
+ "./base/Foreign/Marshal/Alloc.hcr",
+ "./base/Foreign/Marshal/Utils.hcr",
+ "./base/Foreign/Marshal/Array.hcr",
+ "./base/Foreign/C/String.hcr",
+ "./base/Foreign/C/Error.hcr",
+ "./base/Foreign/C.hcr",
+ "./base/System/IO/Unsafe.hcr",
+ "./base/Foreign/Marshal.hcr",
+ "./base/Foreign/StablePtr.hcr",
+ "./base/Foreign.hcr",
+ "./base/System/Posix/Types.hcr",
+ "./base/System/Posix/Internals.hcr",
+ "./base/GHC/Conc.hcr",
+ "./base/Control/Exception.hcr",
+ "./base/GHC/TopHandler.hcr",
+ "./base/Data/Bits.hcr",
+ "./base/Numeric.hcr",
+ "./base/GHC/Ptr.hcr",
+ "./base/GHC/Float.hcr",
"./base/GHC/Exception.hcr",
"./base/GHC/Stable.hcr",
- "./base/GHC/Storable.hcr",
- "./base/GHC/Pack.hcr",
"./base/GHC/Weak.hcr",
"./base/GHC/Handle.hcr",
"./base/GHC/IO.hcr",
"./base/GHC/Environment.hcr",
"./base/GHC/Exts.hcr",
"./base/GHC/PArr.hcr",
- "./base/GHC/TopHandler.hcr",
- "./base/GHC/Desugar.hcr",
- "./base/Data/Ord.hcr",
- "./base/Data/Maybe.hcr",
- "./base/Data/Bits.hcr",
- "./base/Data/STRef/Lazy.hcr",
+ "./base/System/IO.hcr",
+ "./base/System/Environment.hcr",
"./base/Data/Generics/Basics.hcr",
- "./base/Data/Generics/Aliases.hcr",
- "./base/Data/Generics/Twins.hcr",
- "./base/Data/Generics/Instances.hcr",
- "./base/Data/Generics/Text.hcr",
- "./base/Data/Generics/Schemes.hcr",
- "./base/Data/Tuple.hcr",
- "./base/Data/String.hcr",
- "./base/Data/Either.hcr",
- "./base/Data/Char.hcr",
- "./base/Data/List.hcr",
- "./base/Data/HashTable.hcr",
- "./base/Data/Typeable.hcr",
- "./base/Data/Dynamic.hcr",
- "./base/Data/Function.hcr",
- "./base/Data/IORef.hcr",
- "./base/Data/Fixed.hcr",
- "./base/Data/Monoid.hcr",
- "./base/Data/Ratio.hcr",
- "./base/Data/STRef.hcr",
- "./base/Data/Version.hcr",
"./base/Data/Complex.hcr",
- "./base/Data/Unique.hcr",
- "./base/Data/Foldable.hcr",
- "./base/Data/Traversable.hcr"]
\ No newline at end of file
+ "./array/Data/Array/Base.hcr",
+ "./base/System/Exit.hcr",
+ "./base/Data/Ratio.hcr",
+ "./base/Control/Monad/ST/Lazy.hcr",
+ "./base/Prelude.hcr",
+ "./base/Control/Concurrent/MVar.hcr",
+ "./base/Data/Foldable.hcr"])
+
+mkInitialEnv :: [FilePath] -> IO Menv
+mkInitialEnv libs = foldM mkTypeEnv initialEnv libs
+
+mkTypeEnv :: Menv -> FilePath -> IO Menv
+mkTypeEnv globalEnv fn = catch (do
+ putStrLn $ "mkTypeEnv: reading library " ++ fn
+ resultOrErr <- parseCore fn
+ case resultOrErr of
+ Right mod@(Module mn _ _) -> do
+ let newE = envsModule globalEnv mod
+ return newE
+ Left err -> do putStrLn ("Failed to parse library module: " ++ show err)
+ error "quit") handler
+ where handler e = do
+ putStrLn ("WARNING: mkTypeEnv caught an exception " ++ show e
+ ++ " while processing " ++ fn)
+ return globalEnv
{- Environments.
- Uses lists for simplicity and to make the semantics clear.
- A real implementation should use balanced trees or hash tables.
+ The original version used lists. I changed it to use Data.Map.
+ Sadly it doesn't seem to matter much. --tjc
-}
module Env (Env,
eextend,
edomain,
efromlist,
+ etolist,
efilter,
eremove)
where
-import List
+import qualified Data.Map as M
+import Data.List
-data Env a b = Env [(a,b)]
- deriving (Show)
+data Env a b = Env (M.Map a b)
+ deriving Show
eempty :: Env a b
-eempty = Env []
+eempty = Env M.empty
{- In case of duplicates, returns most recently added entry. -}
-elookup :: (Eq a) => Env a b -> a -> Maybe b
-elookup (Env l) k = lookup k l
+elookup :: (Eq a, Ord a) => Env a b -> a -> Maybe b
+elookup (Env l) k = M.lookup k l
{- May hide existing entries. -}
-eextend :: Env a b -> (a,b) -> Env a b
-eextend (Env l) (k,d) = Env ((k,d):l)
+eextend :: Ord a => Env a b -> (a,b) -> Env a b
+eextend (Env l) (k,d) = Env (M.insert k d l)
edomain :: (Eq a) => Env a b -> [a]
-edomain (Env l) = nub (map fst l)
+edomain (Env l) = M.keys l
{- In case of duplicates, first entry hides others. -}
-efromlist :: [(a,b)] -> Env a b
-efromlist l = Env l
+efromlist :: Ord a => [(a,b)] -> Env a b
+efromlist = Env . M.fromList
-eremove :: (Eq a) => Env a b -> a -> Env a b
-eremove (Env l) k = Env (filter ((/= k).fst) l)
+etolist :: Env a b -> [(a,b)]
+etolist (Env l) = M.toList l
-efilter :: Env a b -> (a -> Bool) -> Env a b
-efilter (Env l) p = Env (filter (p.fst) l)
+eremove :: (Eq a, Ord a) => Env a b -> a -> Env a b
+eremove (Env l) k = Env (M.delete k l)
+
+efilter :: Ord a => Env a b -> (a -> Bool) -> Env a b
+efilter (Env l) p = Env (M.filterWithKey (\ k a -> p k) l)
Just a sampling of primitive types and operators are included.
-}
-module Interp where
+module Interp ( evalProgram ) where
import Core
import Printer
-all: Check.hs Core.hs Driver.hs Env.hs Interp.hs ParsecParser.hs ParseGlue.hs Prep.hs Prims.hs Printer.hs
- ghc --make -fglasgow-exts -o Driver Driver.hs
+all: Check.hs Core.hs Driver.hs Env.hs Interp.hs ParsecParser.hs ParseGlue.hs Prep.hs PrimCoercions.hs Prims.hs Printer.hs
+ ghc -O2 --make -fglasgow-exts -o Driver Driver.hs
+
+# Run this when the primops.txt file changes
+prims: ../../compiler/prelude/primops.txt
+ ../genprimopcode/genprimopcode --make-ext-core-source < ../../compiler/prelude/primops.txt > PrimEnv.hs
#Parser.hs: Parser.y
-# happy -ad -ihappy.debug -o Parser.hs Parser.y
\ No newline at end of file
+# happy -ad -ihappy.debug -o Parser.hs Parser.y
+
+# 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`
+
+# ...or built all the nofib programs with -fext-core.
+nofibtest: all
+ ./Driver `find ../../nofib -print | grep .hcr$$`
+
+clean:
+ rm -f Driver *.hi *.o
+
+reallyclean: clean
+ rm PrimEnv.hs
\ No newline at end of file
+{-# OPTIONS -Wall -Werror -fno-warn-missing-signatures #-}
+
module ParsecParser where
import Core
import ParseGlue
+import Check
+import PrimCoercions
import Text.ParserCombinators.Parsec
-import Text.ParserCombinators.Parsec.Expr
+--import Text.ParserCombinators.Parsec.Expr
import qualified Text.ParserCombinators.Parsec.Token as P
import Text.ParserCombinators.Parsec.Language
import Data.Ratio
return (pkgName, modHierarchy, baseName)
corePackageName :: Parser Pname
-corePackageName = identifier
+-- Package names can be lowercase or uppercase!
+-- TODO: update docs
+corePackageName = identifier <|> upperName
coreHierModuleNames :: Parser ([Id], Id)
coreHierModuleNames = do
coreQualifiedCon :: Parser (Mname, Id)
coreQualifiedCon = coreQualifiedGen upperName
-
+
coreQualifiedName = coreQualifiedGen identifier
coreQualifiedGen p = do
coreAxiom = parens (do
coercionName <- coreQualifiedCon
whiteSpace
+ tbs <- coreTbinds
+ whiteSpace
symbol "::"
whiteSpace
- coercionKind <- coreKind
- return (coercionName, coercionKind))
+ coercionK <- try equalityKind <|> parens equalityKind
+ return (coercionName, tbs, coercionK))
coreTbinds :: Parser [Tbind]
coreTbinds = many coreTbind
tBinds <- try $ coreTbindsGen (symbol "@")
-- This should be equivalent to (many coreAty)
-- But it isn't. WHY??
- tys <- sepBy coreAty whiteSpace
+ tys <- sepBy coreAtySaturated whiteSpace
return $ Constr dataConName tBinds tys
coreTRep :: Parser (Maybe Ty)
stuff -> foldl Tapp (Tcon tcArrow) (hd:stuff))
coreBty :: Parser Ty
-coreBty = arrowThing coreAty coreAty whiteSpace Tapp
-
-arrowThing :: Parser a -> Parser a -> Parser b -> (a -> a -> a) -> Parser a
-arrowThing hdThing restThing sep op = do
- hd <- hdThing
+coreBty = do
+ hd <- coreAty
-- The "try" is necessary:
-- otherwise, parsing "T " fails rather
-- than returning "T".
- maybeRest <- option [] (many1 (try (sep >> restThing)))
- return $ case maybeRest of
- [] -> hd
- stuff -> foldl op hd maybeRest
-
-coreAppTy :: Parser Ty
-coreAppTy = do
- bTy <- try coreBty
- whiteSpace
- aTy <- try coreAty
- return $ Tapp bTy aTy
-
-coreAty = try coreTcon <|> try coreTvar <|> parens coreType
-
+ maybeRest <- option [] (many1 (try (whiteSpace >> coreAtySaturated)))
+ return $ (case hd of
+ -- so I'm not sure I like this... it's basically doing
+ -- typechecking (kind-checking?) in the parser.
+ -- However, the type syntax as defined in Core.hs sort of
+ -- forces it.
+ ATy t -> foldl Tapp t maybeRest
+ Trans k -> app k 2 maybeRest "trans"
+ Sym k -> app k 1 maybeRest "sym"
+ Unsafe k -> app k 2 maybeRest "unsafe"
+ LeftCo k -> app k 1 maybeRest "left"
+ RightCo k -> app k 1 maybeRest "right")
+ where app k arity args _ | length args == arity = k args
+ app _ _ args err =
+ primCoercionError (err ++
+ ("Args were: " ++ show args))
+
+coreAtySaturated :: Parser Ty
+coreAtySaturated = do
+ t <- coreAty
+ case t of
+ ATy ty -> return ty
+ _ -> unexpected "coercion ty"
+
+coreAty :: Parser ATyOp
+coreAty = try coreTcon <|> ((try coreTvar <|> parens coreType)
+ >>= return . ATy)
coreTvar :: Parser Ty
coreTvar = try identifier >>= (return . Tvar)
-coreTcon :: Parser Ty
+coreTcon :: Parser ATyOp
-- TODO: Change the grammar
-- A Tcon can be an uppercase type constructor
-- or a lowercase (always qualified) coercion variable
-coreTcon = (try coreQualifiedCon <|> coreRequiredQualifiedName)
- >>= (return . Tcon)
-
-coreTyApp :: Parser Ty
-coreTyApp = do
- operTy <- coreType
- randTy <- coreType
- return $ Tapp operTy randTy
+coreTcon =
+ -- Special case is first so that (CoUnsafe .. ..) gets parsed as
+ -- a prim. coercion app and not a Tcon app.
+ -- But the whole thing is so bogus.
+ try (do
+ -- the "try"s are crucial; they force
+ -- backtracking
+ maybeCoercion <- choice [try symCo, try transCo, try unsafeCo,
+ try leftCo, rightCo]
+ return $ case maybeCoercion of
+ TransC -> Trans (\ [x,y] -> TransCoercion x y)
+ SymC -> Sym (\ [x] -> SymCoercion x)
+ UnsafeC -> Unsafe (\ [x,y] -> UnsafeCoercion x y)
+ LeftC -> LeftCo (\ [x] -> LeftCoercion x)
+ RightC -> RightCo (\ [x] -> RightCoercion x))
+ <|> (coreQualifiedCon >>= (return . ATy . Tcon))
+
+data CoercionTy = TransC | SymC | UnsafeC | LeftC | RightC
+
+symCo, transCo, unsafeCo :: Parser CoercionTy
+-- Would be better not to wire these in quite this way. Sigh
+symCo = string "^ghczmprim:GHCziPrim.sym" >> return SymC
+transCo = string "^ghczmprim:GHCziPrim.trans" >> return TransC
+unsafeCo = string "^ghczmprim:GHCziPrim.CoUnsafe" >> return UnsafeC
+leftCo = string "^ghczmprim:GHCziPrim.left" >> return LeftC
+rightCo = string "^ghczmprim:GHCziPrim.right" >> return RightC
coreFunTy :: Parser Ty
coreFunTy = do
coreKind = do
hd <- coreAtomicKind
maybeRest <- option [] (many1 (symbol "->" >> coreKind))
- return $ case maybeRest of
- [] -> hd
- stuff -> foldl Karrow hd maybeRest
+ return $ foldl Karrow hd maybeRest
coreAtomicKind = try liftedKind <|> try unliftedKind
- <|> try openKind <|> try (parens equalityKind)
+ <|> try openKind {- <|> try (parens equalityKind) -}
<|> try (parens coreKind)
liftedKind = do
ty1 <- coreBty
symbol ":=:"
ty2 <- coreBty
- return $ Keq ty1 ty2
+ return (ty1, ty2)
+
+-- Only used internally within the parser:
+-- represents either a Tcon, or a continuation
+-- for a primitive coercion
+data ATyOp =
+ ATy Ty
+ | Trans ([Ty] -> Ty)
+ | Sym ([Ty] -> Ty)
+ | Unsafe ([Ty] -> Ty)
+ | LeftCo ([Ty] -> Ty)
+ | RightCo ([Ty] -> Ty)
+
coreVdefGroups :: Parser [Vdefg]
coreVdefGroups = option [] (do
theFirstVdef <- coreVdefg
return res
coreFullExp = (choice [coreLam, coreLet,
- coreCase, coreCast, coreNote, coreExternal]) <|> (try coreAppExp)
+ coreCase, coreCast, coreNote, coreExternal, coreLabel]) <|> (try coreAppExp)
-- The "try" is necessary so that we backtrack
-- when we see a var (that is not an app)
<|> coreAtomicExp
args <- many1 (whiteSpace >> ((coreAtomicExp >>= (return . Left)) <|>
-- note this MUST be coreAty, not coreType, because otherwise:
-- "A @ B c" gets parsed as "A @ (B c)"
- ((symbol "@" >> coreAty) >>= (return . Right))))
+ ((symbol "@" >> coreAtySaturated) >>= (return . Right))))
return $ foldl (\ op ->
either (App op) (Appt op)) oper args
return $ Let vdefg body
coreCase = do
reserved "case"
- ty <- coreAty
+ ty <- coreAtySaturated
scrut <- coreAtomicExp
reserved "of"
vBind <- parens lambdaBind
-- The parens are CRUCIAL, o/w it's ambiguous
body <- try (parens coreFullExp)
whiteSpace
- ty <- try coreAty
+ ty <- try coreAtySaturated
return $ Cast body ty
coreNote = do
reserved "note"
s <- stringLiteral
e <- coreFullExp
return $ Note s e
-coreExternal = do
+coreExternal = (do
reserved "external"
-- TODO: This isn't in the grammar, but GHC
-- always prints "external ccall". investigate...
symbol "ccall"
s <- stringLiteral
- t <- coreAty
- return $ External s t
+ t <- coreAtySaturated
+ return $ External s t) <|>
+ -- TODO: I don't really understand what this does
+ (do
+ reserved "dynexternal"
+ symbol "ccall"
+ t <- coreAtySaturated
+ return $ External "[dynamic]" t)
+coreLabel = do
+-- TODO: Totally punting this, but it needs to go in the grammar
+-- or not at all
+ reserved "label"
+ s <- stringLiteral
+ return $ External s tAddrzh
coreLambdaBinds = many1 coreBind
+{-# OPTIONS -Wall -fno-warn-name-shadowing #-}
{-
Preprocess a module to normalize it in the following ways:
(1) Saturate all constructor and primop applications.
module Prep where
+import Data.Either
+
import Prims
import Core
-import Printer
import Env
import Check
+import Data.List
+
primArgTys :: Env Var [Ty]
-primArgTys = efromlist (map f Prims.primVals)
+primArgTys = efromlist (map f (etolist (venv_ primEnv)))
where f (v,t) = (v,atys)
where (_,atys,_) = splitTy t
prepModule globalEnv (Module mn tdefs vdefgs) =
Module mn tdefs vdefgs'
where
+
(_,vdefgs') = foldl prepTopVdefg (eempty,[]) vdefgs
prepTopVdefg (venv,vdefgs) vdefg = (venv',vdefgs ++ [vdefg'])
prepVdefg (env@(venv,_)) (Nonrec(Vdef((Nothing,x),t,e))) =
(eextend venv (x,t), Nonrec(Vdef((Nothing,x),t,prepExp env e)))
- prepVdefg (env@(venv,_)) (Nonrec(Vdef(qx,t,e))) =
- (venv, Nonrec(Vdef(qx,t,prepExp env e)))
+ prepVdefg (env@(venv,_)) (Nonrec(Vdef(qx,t,e))) =
+ (venv, Nonrec(Vdef(qx,t,prepExp env e)))
prepVdefg (venv,tvenv) (Rec vdefs) =
- (venv',Rec [Vdef(qx,t,prepExp (venv',tvenv) e) | Vdef(qx,t,e) <- vdefs])
+ (venv',Rec [ Vdef(qx,t,prepExp (venv',tvenv) e) | Vdef(qx,t,e) <- vdefs])
where venv' = foldl eextend venv [(x,t) | Vdef((Nothing,x),t,_) <- vdefs]
- prepExp env (Var qv) = Var qv
- prepExp env (Dcon qdc) = Dcon qdc
- prepExp env (Lit l) = Lit l
+ prepExp _ (Var qv) = Var qv
+ prepExp _ (Dcon qdc) = Dcon qdc
+ prepExp _ (Lit l) = Lit l
prepExp env e@(App _ _) = unwindApp env e []
prepExp env e@(Appt _ _) = unwindApp env e []
prepExp (venv,tvenv) (Lam (Vb vb) e) = Lam (Vb vb) (prepExp (eextend venv vb,tvenv) e)
prepExp (venv,tvenv) (Lam (Tb tb) e) = Lam (Tb tb) (prepExp (venv,eextend tvenv tb) e)
prepExp env@(venv,tvenv) (Let (Nonrec(Vdef((Nothing,x),t,b))) e)
- | kindof tvenv t `eqKind` Kunlifted && suspends b =
+ | (kindOfTy tvenv t `eqKind` Kunlifted && suspends b) =
-- There are two places where we call the typechecker, one of them
-- here.
-- We need to know the type of the let body in order to construct
-- a case expression.
- let eTy = typeOfExp env e in
- Case (prepExp env b) (x,t)
+ -- need to extend the env with the let-bound var too!
+ let eTy = typeOfExp (eextend venv (x, t), tvenv) e in
+ Case (prepExp env b) (x,t)
eTy
- [Adefault (prepExp (eextend venv (x,t),tvenv) e)]
+ [Adefault (prepExp (eextend venv (x,t),tvenv) e)]
prepExp (venv,tvenv) (Let vdefg e) = Let vdefg' (prepExp (venv',tvenv) e)
where (venv',vdefg') = prepVdefg (venv,tvenv) vdefg
prepExp env@(venv,tvenv) (Case e vb t alts) = Case (prepExp env e) vb t (map (prepAlt (eextend venv vb,tvenv)) alts)
prepExp env (Cast e t) = Cast (prepExp env e) t
prepExp env (Note s e) = Note s (prepExp env e)
- prepExp env (External s t) = External s t
+ prepExp _ (External s t) = External s t
prepAlt (venv,tvenv) (Acon qdc tbs vbs e) = Acon qdc tbs vbs (prepExp (foldl eextend venv vbs,foldl eextend tvenv tbs) e)
prepAlt env (Alit l e) = Alit l (prepExp env e)
unwindApp env (App e1 e2) as = unwindApp env e1 (Left e2:as)
unwindApp env (Appt e t) as = unwindApp env e (Right t:as)
- unwindApp env (op@(Dcon qdc)) as =
+ unwindApp env (op@(Dcon qdc)) as =
etaExpand (drop n atys) (rewindApp env op as)
where (tbs,atys0,_) = splitTy (qlookup cenv_ eempty qdc)
atys = map (substl (map fst tbs) ts) atys0
unwindApp env op as = rewindApp env op as
- etaExpand ts e = foldl g e [('$':(show i),t) | (i,t) <- zip [1..] ts]
- where g e (v,t) = Lam (Vb(v,t)) (App e (Var (unqual v)))
+ etaExpand :: [Ty] -> Exp -> Exp
+ etaExpand ts e =
+ let args = [('$':(show i),t) | (i,t) <- zip [(1::Integer)..] ts] in
+ foldr (\ (v,t) e -> Lam (Vb (v,t)) e)
+ (foldl (\ e (v,_) -> App e (Var (unqual v))) e args)
+ args
- rewindApp env e [] = e
- rewindApp env@(venv,tvenv) e1 (Left e2:as) | kindof tvenv t `eqKind` Kunlifted && suspends e2 =
+ rewindApp _ e [] = e
+ rewindApp env@(venv,tvenv) e1 (Left e2:as) | kindOfTy tvenv t `eqKind` Kunlifted && suspends e2 =
-- This is the other place where we call the typechecker.
- Case (prepExp env' e2) (v,t) (typeOfExp env rhs) [Adefault rhs]
- where rhs = (rewindApp env' (App e1 (Var (unqual v))) as)
- v = freshVar venv
+ Case newScrut (v,t) (typeOfExp env' rhs) [Adefault rhs]
+ where newScrut = prepExp env e2
+ rhs = (rewindApp env' (App e1 (Var (unqual v))) as)
+ -- note:
+ -- e1 gets moved inside rhs. so if we pick a case
+ -- var name (outside e1) equal to a name bound *inside*
+ -- e1, the binding *inside* e1 will shadow "v"
+ -- Which would be name capture!
+ -- So, we pass the bound vars of e1 to freshVar along with
+ -- the domain of the current env.
+ v = freshVar (edomain venv `union` (boundVars e1))
t = typeOfExp env e2
env' = (eextend venv (v,t),tvenv)
rewindApp env e1 (Left e2:as) = rewindApp env (App e1 (prepExp env e2)) as
rewindApp env e (Right t:as) = rewindApp env (Appt e t) as
- freshVar venv = maximum ("":edomain venv) ++ "x" -- one simple way!
+ freshVar vs = maximum ("":vs) ++ "x" -- one simple way!
typeOfExp :: (Venv, Tvenv) -> Exp -> Ty
typeOfExp = uncurry (checkExpr mn globalEnv tdefs)
+ kindOfTy :: Tvenv -> Ty -> Kind
+ kindOfTy tvenv = checkType mn globalEnv tdefs tvenv
+
{- Return false for those expressions for which Interp.suspendExp builds a thunk. -}
suspends (Var _) = False
suspends (Lit _) = False
suspends (External _ _) = False
suspends _ = True
- kindof :: Tvenv -> Ty -> Kind
- kindof tvenv (Tvar tv) =
- case elookup tvenv tv of
- Just k -> k
- Nothing -> error ("impossible Tyvar " ++ show tv)
- kindof tvenv (Tcon qtc) = qlookup tcenv_ eempty qtc
- kindof tvenv (Tapp t1 t2) = k2
- where Karrow _ k2 = kindof tvenv t1
- kindof tvenv (Tforall _ t) = kindof tvenv t
-
mlookup :: (Envs -> Env a b) -> Env a b -> Mname -> Env a b
mlookup _ local_env Nothing = local_env
mlookup selector _ (Just m) =
Just v -> v
Nothing -> error ("undefined identifier: " ++ show k)
+boundVars :: Exp -> [Id]
+boundVars (Lam (Vb (v,_)) e) = [v] `union` boundVars e
+boundVars (Lam _ e) = boundVars e
+boundVars (Let vds e) = (boundVarsVdefs vds) `union` boundVars e
+boundVars (Case scrut (v,_) _ alts) =
+ [v] `union` (boundVars scrut) `union` boundVarsAlts alts
+boundVars (Cast e _) = boundVars e
+boundVars (Note _ e) = boundVars e
+boundVars (App e1 e2) = boundVars e1 `union` boundVars e2
+boundVars (Appt e _) = boundVars e
+boundVars _ = []
+
+boundVarsVdefs :: Vdefg -> [Id]
+boundVarsVdefs (Rec vds) = nub (concatMap boundVarsVdef vds)
+boundVarsVdefs (Nonrec vd) = boundVarsVdef vd
+
+boundVarsVdef :: Vdef -> [Id]
+boundVarsVdef (Vdef ((_,v),_,e)) = [v] `union` boundVars e
+
+boundVarsAlts :: [Alt] -> [Var]
+boundVarsAlts as = nub (concatMap boundVarsAlt as)
+
+boundVarsAlt :: Alt -> [Var]
+boundVarsAlt (Acon _ _ vbs e) = (map fst vbs) `union` (boundVars e)
+boundVarsAlt (Alit _ e) = boundVars e
+boundVarsAlt (Adefault e) = boundVars e
\ No newline at end of file
--- /dev/null
+{-# OPTIONS -Wall -fno-warn-missing-signatures #-}
+module PrimCoercions where
+import Core
+
+-- Stuff the parser needs to know about
+
+pv :: a -> Qual a
+pv = qual primMname
+
+pvz :: Id -> Qual Id
+pvz = (qual primMname) . (++ "zh")
+
+{- Coercions -}
+symCoercion, transCoercion, unsafeCoercion :: Qual Tcon
+symCoercion = pv "sym"
+transCoercion = pv "trans"
+unsafeCoercion = pv "CoUnsafe"
+leftCoercion = pv "left"
+rightCoercion = pv "right"
+
+{- Addrzh -}
+tcAddrzh = pvz "Addr"
+tAddrzh = Tcon tcAddrzh
+ktAddrzh = Kunlifted
-{- This module really should be auto-generated from the master primops.txt file.
- It is roughly correct (but may be slightly incomplete) wrt/ GHC5.02. -}
+{-# OPTIONS -Wall #-}
-module Prims where
+{- This module contains a few primitive types that need to be wired in.
+ Most are defined in PrimEnv, which is automatically generated from
+ GHC's primops.txt. -}
+
+module Prims(initialEnv, primEnv) where
import Core
import Env
import Check
+import PrimCoercions
+
+import PrimEnv
initialEnv :: Menv
initialEnv = efromlist [(primMname,primEnv),
(errMname,errorEnv)]
primEnv :: Envs
-primEnv = Envs {tcenv_=efromlist primTcs,
+-- Tediously, we add defs for ByteArray# etc. because these are
+-- declared as ByteArr# (etc.) in primops.txt, and GHC has
+-- ByteArray# etc. wired-in.
+-- At least this is better than when all primops were wired-in here.
+primEnv = Envs {tcenv_=efromlist $ map (\ (t,k) -> (t,Kind k)) $
+ [(snd tcByteArrayzh,ktByteArrayzh),
+ (snd tcMutableArrayzh, ktMutableArrayzh),
+ (snd tcMutableByteArrayzh, ktMutableByteArrayzh)] ++
+ ([(snd $ tcUtuple n, ktUtuple n) | n <- [1..maxUtuple]]
+ ++ ((snd tcArrow,ktArrow):primTcs)),
tsenv_=eempty,
cenv_=efromlist primDcs,
- venv_=efromlist primVals}
+ venv_=efromlist (opsState ++ primVals)}
errorEnv :: Envs
errorEnv = Envs {tcenv_=eempty,
cenv_=eempty,
venv_=efromlist errorVals}
-{- Components of static environment -}
-
-primTcs :: [(Tcon,Kind)]
-primTcs =
- map (\ ((m,tc),k) -> (tc,k))
- ([(tcArrow,ktArrow),
- (tcAddrzh,ktAddrzh),
- (tcCharzh,ktCharzh),
- (tcDoublezh,ktDoublezh),
- (tcFloatzh,ktFloatzh),
- (tcIntzh,ktIntzh),
- (tcInt32zh,ktInt32zh),
- (tcInt64zh,ktInt64zh),
- (tcWordzh,ktWordzh),
- (tcWord32zh,ktWord32zh),
- (tcWord64zh,ktWord64zh),
- (tcRealWorld, ktRealWorld),
- (tcStatezh, ktStatezh),
- (tcArrayzh,ktArrayzh),
- (tcByteArrayzh,ktByteArrayzh),
- (tcMutableArrayzh,ktMutableArrayzh),
- (tcMutableByteArrayzh,ktMutableByteArrayzh),
- (tcMutVarzh,ktMutVarzh),
- (tcMVarzh,ktMVarzh),
- (tcWeakzh,ktWeakzh),
- (tcForeignObjzh, ktForeignObjzh),
- (tcStablePtrzh, ktStablePtrzh),
- (tcThreadIdzh, ktThreadIdzh),
- (tcZCTCCallable, ktZCTCCallable),
- (tcZCTCReturnable, ktZCTCReturnable)]
- ++ [(tcUtuple n, ktUtuple n) | n <- [1..maxUtuple]])
-
primDcs :: [(Dcon,Ty)]
-primDcs = map (\ ((m,c),t) -> (c,t))
+primDcs = map (\ ((_,c),t) -> (c,t))
[(dcUtuple n, dcUtupleTy n) | n <- [1..maxUtuple]]
-primVals :: [(Var,Ty)]
-primVals =
- opsAddrzh ++
- opsCharzh ++
- opsDoublezh ++
- opsFloatzh ++
- opsIntzh ++
- opsInt32zh ++
- opsInt64zh ++
- opsIntegerzh ++
- opsWordzh ++
- opsWord32zh ++
- opsWord64zh ++
- opsSized ++
- opsArray ++
- opsMutVarzh ++
- opsState ++
- opsExn ++
- opsMVar ++
- opsWeak ++
- opsForeignObjzh ++
- opsStablePtrzh ++
- opsConc ++
- opsMisc
-
-
-dcUtuples :: [(Qual Dcon,Ty)]
-dcUtuples = map ( \n -> (dcUtuple n, typ n)) [1..100]
- where typ n = foldr ( \tv t -> Tforall (tv,Kopen) t)
- (foldr ( \tv t -> tArrow (Tvar tv) t)
- (tUtuple (map Tvar tvs)) tvs) tvs
- where tvs = map ( \i -> ("a" ++ (show i))) [1..n]
-
-pv = qual primMname
-pvz = (qual primMname) . (++ "zh")
-
-{- Addrzh -}
-tcAddrzh = pvz "Addr"
-tAddrzh = Tcon tcAddrzh
-ktAddrzh = Kunlifted
-
-opsAddrzh = [
- ("gtAddrzh",tcompare tAddrzh),
- ("geAddrzh",tcompare tAddrzh),
- ("eqAddrzh",tcompare tAddrzh),
- ("neAddrzh",tcompare tAddrzh),
- ("ltAddrzh",tcompare tAddrzh),
- ("leAddrzh",tcompare tAddrzh),
- ("nullAddrzh", tAddrzh),
- ("plusAddrzh", tArrow tAddrzh (tArrow tIntzh tAddrzh)),
- ("minusAddrzh", tArrow tAddrzh (tArrow tAddrzh tIntzh)),
- ("remAddrzh", tArrow tAddrzh (tArrow tIntzh tIntzh))]
-
-{- Charzh -}
-
-tcCharzh = pvz "Char"
-tCharzh = Tcon tcCharzh
-ktCharzh = Kunlifted
-
-opsCharzh = [
- ("gtCharzh", tcompare tCharzh),
- ("geCharzh", tcompare tCharzh),
- ("eqCharzh", tcompare tCharzh),
- ("neCharzh", tcompare tCharzh),
- ("ltCharzh", tcompare tCharzh),
- ("leCharzh", tcompare tCharzh),
- ("ordzh", tArrow tCharzh tIntzh)]
-
-
-{- Doublezh -}
-
-tcDoublezh = pvz "Double"
-tDoublezh = Tcon tcDoublezh
-ktDoublezh = Kunlifted
-
-opsDoublezh = [
- ("zgzhzh", tcompare tDoublezh),
- ("zgzezhzh", tcompare tDoublezh),
- ("zezezhzh", tcompare tDoublezh),
- ("zszezhzh", tcompare tDoublezh),
- ("zlzhzh", tcompare tDoublezh),
- ("zlzezhzh", tcompare tDoublezh),
- ("zpzhzh", tdyadic tDoublezh),
- ("zmzhzh", tdyadic tDoublezh),
- ("ztzhzh", tdyadic tDoublezh),
- ("zszhzh", tdyadic tDoublezh),
- ("negateDoublezh", tmonadic tDoublezh),
- ("double2Intzh", tArrow tDoublezh tIntzh),
- ("double2Floatzh", tArrow tDoublezh tFloatzh),
- ("expDoublezh", tmonadic tDoublezh),
- ("logDoublezh", tmonadic tDoublezh),
- ("sqrtDoublezh", tmonadic tDoublezh),
- ("sinDoublezh", tmonadic tDoublezh),
- ("cosDoublezh", tmonadic tDoublezh),
- ("tanDoublezh", tmonadic tDoublezh),
- ("asinDoublezh", tmonadic tDoublezh),
- ("acosDoublezh", tmonadic tDoublezh),
- ("atanDoublezh", tmonadic tDoublezh),
- ("sinhDoublezh", tmonadic tDoublezh),
- ("coshDoublezh", tmonadic tDoublezh),
- ("tanhDoublezh", tmonadic tDoublezh),
- ("ztztzhzh", tdyadic tDoublezh),
- ("decodeDoublezh", tArrow tDoublezh (tUtuple[tIntzh,tIntzh,tByteArrayzh]))]
-
-
-{- Floatzh -}
-
-tcFloatzh = pvz "Float"
-tFloatzh = Tcon tcFloatzh
-ktFloatzh = Kunlifted
-
-opsFloatzh = [
- ("gtFloatzh", tcompare tFloatzh),
- ("geFloatzh", tcompare tFloatzh),
- ("eqFloatzh", tcompare tFloatzh),
- ("neFloatzh", tcompare tFloatzh),
- ("ltFloatzh", tcompare tFloatzh),
- ("leFloatzh", tcompare tFloatzh),
- ("plusFloatzh", tdyadic tFloatzh),
- ("minusFloatzh", tdyadic tFloatzh),
- ("timesFloatzh", tdyadic tFloatzh),
- ("divideFloatzh", tdyadic tFloatzh),
- ("negateFloatzh", tmonadic tFloatzh),
- ("float2Intzh", tArrow tFloatzh tIntzh),
- ("expFloatzh", tmonadic tFloatzh),
- ("logFloatzh", tmonadic tFloatzh),
- ("sqrtFloatzh", tmonadic tFloatzh),
- ("sinFloatzh", tmonadic tFloatzh),
- ("cosFloatzh", tmonadic tFloatzh),
- ("tanFloatzh", tmonadic tFloatzh),
- ("asinFloatzh", tmonadic tFloatzh),
- ("acosFloatzh", tmonadic tFloatzh),
- ("atanFloatzh", tmonadic tFloatzh),
- ("sinhFloatzh", tmonadic tFloatzh),
- ("coshFloatzh", tmonadic tFloatzh),
- ("tanhFloatzh", tmonadic tFloatzh),
- ("powerFloatzh", tdyadic tFloatzh),
- ("float2Doublezh", tArrow tFloatzh tDoublezh),
- ("decodeFloatzh", tArrow tFloatzh (tUtuple[tIntzh,tIntzh,tByteArrayzh]))]
-
-
-{- Intzh -}
-
-tcIntzh = pvz "Int"
-tIntzh = Tcon tcIntzh
-ktIntzh = Kunlifted
-
-opsIntzh = [
- ("zpzh", tdyadic tIntzh),
- ("zmzh", tdyadic tIntzh),
- ("ztzh", tdyadic tIntzh),
- ("quotIntzh", tdyadic tIntzh),
- ("remIntzh", tdyadic tIntzh),
- ("gcdIntzh", tdyadic tIntzh),
- ("negateIntzh", tmonadic tIntzh),
- ("addIntCzh", tArrow tIntzh (tArrow tIntzh (tUtuple [tIntzh, tIntzh]))),
- ("subIntCzh", tArrow tIntzh (tArrow tIntzh (tUtuple [tIntzh, tIntzh]))),
- ("mulIntCzh", tArrow tIntzh (tArrow tIntzh (tUtuple [tIntzh, tIntzh]))),
- ("zgzh", tcompare tIntzh),
- ("zgzezh", tcompare tIntzh),
- ("zezezh", tcompare tIntzh),
- ("zszezh", tcompare tIntzh),
- ("zlzh", tcompare tIntzh),
- ("zlzezh", tcompare tIntzh),
- ("chrzh", tArrow tIntzh tCharzh),
- ("int2Wordzh", tArrow tIntzh tWordzh),
- ("int2Floatzh", tArrow tIntzh tFloatzh),
- ("int2Doublezh", tArrow tIntzh tDoublezh),
- ("intToInt32zh", tArrow tIntzh tInt32zh),
- ("int2Integerzh", tArrow tIntzh tIntegerzhRes),
- ("iShiftLzh", tdyadic tIntzh),
- ("iShiftRAzh", tdyadic tIntzh),
- ("iShiftRLh", tdyadic tIntzh)]
-
-
-{- Int32zh -}
-
-tcInt32zh = pvz "Int32"
-tInt32zh = Tcon tcInt32zh
-ktInt32zh = Kunlifted
-
-opsInt32zh = [
- ("int32ToIntzh", tArrow tInt32zh tIntzh),
- ("int32ToIntegerzh", tArrow tInt32zh tIntegerzhRes)]
-
-
-{- Int64zh -}
-
-tcInt64zh = pvz "Int64"
-tInt64zh = Tcon tcInt64zh
-ktInt64zh = Kunlifted
-
-opsInt64zh = [
- ("int64ToIntegerzh", tArrow tInt64zh tIntegerzhRes)]
-
-{- Integerzh -}
-
--- not actuallly a primitive type
-tIntegerzhRes = tUtuple [tIntzh, tByteArrayzh]
-tIntegerzhTo t = tArrow tIntzh (tArrow tByteArrayzh t)
-tdyadicIntegerzh = tIntegerzhTo (tIntegerzhTo tIntegerzhRes)
-
-opsIntegerzh = [
- ("plusIntegerzh", tdyadicIntegerzh),
- ("minusIntegerzh", tdyadicIntegerzh),
- ("timesIntegerzh", tdyadicIntegerzh),
- ("gcdIntegerzh", tdyadicIntegerzh),
- ("gcdIntegerIntzh", tIntegerzhTo (tArrow tIntzh tIntzh)),
- ("divExactIntegerzh", tdyadicIntegerzh),
- ("quotIntegerzh", tdyadicIntegerzh),
- ("remIntegerzh", tdyadicIntegerzh),
- ("cmpIntegerzh", tIntegerzhTo (tIntegerzhTo tIntzh)),
- ("cmpIntegerIntzh", tIntegerzhTo (tArrow tIntzh tIntzh)),
- ("quotRemIntegerzh", tIntegerzhTo (tIntegerzhTo (tUtuple [tIntzh,tByteArrayzh,tIntzh,tByteArrayzh]))),
- ("divModIntegerzh", tIntegerzhTo (tIntegerzhTo (tUtuple [tIntzh,tByteArrayzh,tIntzh,tByteArrayzh]))),
- ("integer2Intzh", tIntegerzhTo tIntzh),
- ("integer2Wordzh", tIntegerzhTo tWordzh),
- ("integerToInt32zh", tIntegerzhTo tInt32zh),
- ("integerToWord32zh", tIntegerzhTo tWord32zh),
- ("integerToInt64zh", tIntegerzhTo tInt64zh),
- ("integerToWord64zh", tIntegerzhTo tWord64zh),
- ("andIntegerzh", tdyadicIntegerzh),
- ("orIntegerzh", tdyadicIntegerzh),
- ("xorIntegerzh", tdyadicIntegerzh),
- ("complementIntegerzh", tIntegerzhTo tIntegerzhRes)]
-
-
-
-{- Wordzh -}
-
-tcWordzh = pvz "Word"
-tWordzh = Tcon tcWordzh
-ktWordzh = Kunlifted
-
-opsWordzh = [
- ("plusWordzh", tdyadic tWordzh),
- ("minusWordzh", tdyadic tWordzh),
- ("timesWordzh", tdyadic tWordzh),
- ("quotWordzh", tdyadic tWordzh),
- ("remWordzh", tdyadic tWordzh),
- ("andzh", tdyadic tWordzh),
- ("orzh", tdyadic tWordzh),
- ("xorzh", tdyadic tWordzh),
- ("notzh", tmonadic tWordzh),
- ("shiftLzh", tArrow tWordzh (tArrow tIntzh tWordzh)),
- ("shiftRLzh", tArrow tWordzh (tArrow tIntzh tWordzh)),
- ("word2Intzh", tArrow tWordzh tIntzh),
- ("wordToWord32zh", tArrow tWordzh tWord32zh),
- ("word2Integerzh", tArrow tWordzh tIntegerzhRes),
- ("gtWordzh", tcompare tWordzh),
- ("geWordzh", tcompare tWordzh),
- ("eqWordzh", tcompare tWordzh),
- ("neWordzh", tcompare tWordzh),
- ("ltWordzh", tcompare tWordzh),
- ("leWordzh", tcompare tWordzh)]
-
-{- Word32zh -}
-
-tcWord32zh = pvz "Word32"
-tWord32zh = Tcon tcWord32zh
-ktWord32zh = Kunlifted
-
-opsWord32zh = [
- ("word32ToWordzh", tArrow tWord32zh tWordzh),
- ("word32ToIntegerzh", tArrow tWord32zh tIntegerzhRes)]
-
-{- Word64zh -}
-
-tcWord64zh = pvz "Word64"
-tWord64zh = Tcon tcWord64zh
-ktWord64zh = Kunlifted
-
-opsWord64zh = [
- ("word64ToIntegerzh", tArrow tWord64zh tIntegerzhRes)]
-
-{- Explicitly sized Intzh and Wordzh -}
+tRWS :: Ty
+tRWS = tStatezh tRealWorld
-opsSized = [
- ("narrow8Intzh", tmonadic tIntzh),
- ("narrow16Intzh", tmonadic tIntzh),
- ("narrow32Intzh", tmonadic tIntzh),
- ("narrow8Wordzh", tmonadic tWordzh),
- ("narrow16Wordzh", tmonadic tWordzh),
- ("narrow32Wordzh", tmonadic tWordzh)]
+opsState :: [(Var, Ty)]
+opsState = [
+ ("realWorldzh", tRWS)]
{- Arrays -}
-tcArrayzh = pvz "Array"
-tArrayzh t = Tapp (Tcon tcArrayzh) t
-ktArrayzh = Karrow Klifted Kunlifted
+tcByteArrayzh, tcMutableArrayzh, tcMutableByteArrayzh :: Qual Tcon
+ktByteArrayzh, ktMutableArrayzh, ktMutableByteArrayzh :: Kind
tcByteArrayzh = pvz "ByteArray"
-tByteArrayzh = Tcon tcByteArrayzh
ktByteArrayzh = Kunlifted
tcMutableArrayzh = pvz "MutableArray"
-tMutableArrayzh s t = Tapp (Tapp (Tcon tcMutableArrayzh) s) t
ktMutableArrayzh = Karrow Klifted (Karrow Klifted Kunlifted)
tcMutableByteArrayzh = pvz "MutableByteArray"
-tMutableByteArrayzh s = Tapp (Tcon tcMutableByteArrayzh) s
ktMutableByteArrayzh = Karrow Klifted Kunlifted
-opsArray = [
- ("newArrayzh", Tforall ("a",Klifted)
- (Tforall ("s",Klifted)
- (tArrow tIntzh
- (tArrow (Tvar "a")
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple [tStatezh (Tvar "s"),tMutableArrayzh (Tvar "s") (Tvar "a")])))))),
- ("newByteArrayzh", Tforall ("s",Klifted)
- (tArrow tIntzh
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple [tStatezh (Tvar "s"),tMutableByteArrayzh (Tvar "s")])))),
- ("newPinnedByteArrayzh", Tforall ("s",Klifted)
- (tArrow tIntzh
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple [tStatezh (Tvar "s"),tMutableByteArrayzh (Tvar "s")])))),
- ("byteArrayContentszh", tArrow tByteArrayzh tAddrzh),
- ("indexCharArrayzh", tArrow tByteArrayzh (tArrow tIntzh tCharzh)),
- ("indexWideCharArrayzh", tArrow tByteArrayzh (tArrow tIntzh tCharzh)),
- ("indexIntArrayzh", tArrow tByteArrayzh (tArrow tIntzh tIntzh)),
- ("indexWordArrayzh", tArrow tByteArrayzh (tArrow tIntzh tWordzh)),
- ("indexAddrArrayzh", tArrow tByteArrayzh (tArrow tIntzh tAddrzh)),
- ("indexFloatArrayzh", tArrow tByteArrayzh (tArrow tIntzh tFloatzh)),
- ("indexDoubleArrayzh", tArrow tByteArrayzh (tArrow tIntzh tDoublezh)),
- ("indexStablePtrArrayzh", Tforall ("a",Klifted) (tArrow tByteArrayzh (tArrow tIntzh (tStablePtrzh (Tvar "a"))))),
- ("indexInt8Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tIntzh)),
- ("indexInt16Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tIntzh)),
- ("indexInt32Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tInt32zh)),
- ("indexInt64Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tInt64zh)),
- ("indexWord8Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tWordzh)),
- ("indexWord16Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tWordzh)),
- ("indexWord32Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tWord32zh)),
- ("indexWord64Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tWord64zh)),
- ("readCharArrayzh", tReadMutableByteArrayzh tCharzh),
- ("readWideCharArrayzh", tReadMutableByteArrayzh tCharzh),
- ("readIntArrayzh", tReadMutableByteArrayzh tIntzh),
- ("readWordArrayzh", tReadMutableByteArrayzh tWordzh),
- ("readAddrArrayzh", tReadMutableByteArrayzh tAddrzh),
- ("readFloatArrayzh", tReadMutableByteArrayzh tFloatzh),
- ("readDoubleArrayzh", tReadMutableByteArrayzh tDoublezh),
- ("readStablePtrArrayzh", Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMutableByteArrayzh (Tvar "s"))
- (tArrow tIntzh
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple [tStatezh (Tvar "s"),tStablePtrzh (Tvar "a")])))))),
- ("readInt8Arrayzh", tReadMutableByteArrayzh tIntzh),
- ("readInt16Arrayzh", tReadMutableByteArrayzh tIntzh),
- ("readInt32Arrayzh", tReadMutableByteArrayzh tInt32zh),
- ("readInt64Arrayzh", tReadMutableByteArrayzh tInt64zh),
- ("readWord8Arrayzh", tReadMutableByteArrayzh tWordzh),
- ("readWord16Arrayzh", tReadMutableByteArrayzh tWordzh),
- ("readWord32Arrayzh", tReadMutableByteArrayzh tWord32zh),
- ("readWord64Arrayzh", tReadMutableByteArrayzh tWord64zh),
-
- ("writeCharArrayzh", tWriteMutableByteArrayzh tCharzh),
- ("writeWideCharArrayzh", tWriteMutableByteArrayzh tCharzh),
- ("writeIntArrayzh", tWriteMutableByteArrayzh tIntzh),
- ("writeWordArrayzh", tWriteMutableByteArrayzh tWordzh),
- ("writeAddrArrayzh", tWriteMutableByteArrayzh tAddrzh),
- ("writeFloatArrayzh", tWriteMutableByteArrayzh tFloatzh),
- ("writeDoubleArrayzh", tWriteMutableByteArrayzh tDoublezh),
- ("writeStablePtrArrayzh", Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMutableByteArrayzh (Tvar "s"))
- (tArrow tIntzh
- (tArrow (tStablePtrzh (Tvar "a"))
- (tArrow (tStatezh (Tvar "s"))
- (tStatezh (Tvar "s")))))))),
- ("writeInt8Arrayzh", tWriteMutableByteArrayzh tIntzh),
- ("writeInt16Arrayzh", tWriteMutableByteArrayzh tIntzh),
- ("writeInt32Arrayzh", tWriteMutableByteArrayzh tIntzh),
- ("writeInt64Arrayzh", tWriteMutableByteArrayzh tInt64zh),
- ("writeWord8Arrayzh", tWriteMutableByteArrayzh tWordzh),
- ("writeWord16Arrayzh", tWriteMutableByteArrayzh tWordzh),
- ("writeWord32Arrayzh", tWriteMutableByteArrayzh tWord32zh),
- ("writeWord64Arrayzh", tWriteMutableByteArrayzh tWord64zh),
-
- ("indexCharOffAddrzh", tArrow tAddrzh (tArrow tIntzh tCharzh)),
- ("indexWideCharOffAddrzh", tArrow tAddrzh (tArrow tIntzh tCharzh)),
- ("indexIntOffAddrzh", tArrow tAddrzh (tArrow tIntzh tIntzh)),
- ("indexWordOffAddrzh", tArrow tAddrzh (tArrow tIntzh tWordzh)),
- ("indexAddrOffAddrzh", tArrow tAddrzh (tArrow tIntzh tAddrzh)),
- ("indexFloatOffAddrzh", tArrow tAddrzh (tArrow tIntzh tFloatzh)),
- ("indexDoubleOffAddrzh", tArrow tAddrzh (tArrow tIntzh tDoublezh)),
- ("indexStablePtrOffAddrzh", Tforall ("a",Klifted) (tArrow tAddrzh (tArrow tIntzh (tStablePtrzh (Tvar "a"))))),
- ("indexInt8OffAddrzh", tArrow tAddrzh (tArrow tIntzh tIntzh)),
- ("indexInt16OffAddrzh", tArrow tAddrzh (tArrow tIntzh tIntzh)),
- ("indexInt32OffAddrzh", tArrow tAddrzh (tArrow tIntzh tInt32zh)),
- ("indexInt64OffAddrzh", tArrow tAddrzh (tArrow tIntzh tInt64zh)),
- ("indexWord8OffAddrzh", tArrow tAddrzh (tArrow tIntzh tWordzh)),
- ("indexWord16OffAddrzh", tArrow tAddrzh (tArrow tIntzh tWordzh)),
- ("indexWord32ffAddrzh", tArrow tAddrzh (tArrow tIntzh tWord32zh)),
- ("indexWord64OffAddrzh", tArrow tAddrzh (tArrow tIntzh tWord64zh)),
-
- ("indexCharOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tCharzh)),
- ("indexWideCharOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tCharzh)),
- ("indexIntOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tIntzh)),
- ("indexWordOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWordzh)),
- ("indexAddrOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tAddrzh)),
- ("indexFloatOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tFloatzh)),
- ("indexDoubleOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tDoublezh)),
- ("indexStablePtrOffForeignObjzh", Tforall ("a",Klifted) (tArrow tForeignObjzh (tArrow tIntzh (tStablePtrzh (Tvar "a"))))),
- ("indexInt8OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tIntzh)),
- ("indexInt16OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tIntzh)),
- ("indexInt32OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tInt32zh)),
- ("indexInt64OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tInt64zh)),
- ("indexWord8OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWordzh)),
- ("indexWord16OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWordzh)),
- ("indexWord32ffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWord32zh)),
- ("indexWord64OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWord64zh)),
-
- ("readCharOffAddrzh", tReadOffAddrzh tCharzh),
- ("readWideCharOffAddrzh", tReadOffAddrzh tCharzh),
- ("readIntOffAddrzh", tReadOffAddrzh tIntzh),
- ("readWordOffAddrzh", tReadOffAddrzh tWordzh),
- ("readAddrOffAddrzh", tReadOffAddrzh tAddrzh),
- ("readFloatOffAddrzh", tReadOffAddrzh tFloatzh),
- ("readDoubleOffAddrzh", tReadOffAddrzh tDoublezh),
- ("readStablePtrOffAddrzh", Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow tAddrzh
- (tArrow tIntzh
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple [tStatezh (Tvar "s"),tStablePtrzh (Tvar "a")])))))),
- ("readInt8OffAddrzh", tReadOffAddrzh tIntzh),
- ("readInt16OffAddrzh", tReadOffAddrzh tIntzh),
- ("readInt32OffAddrzh", tReadOffAddrzh tInt32zh),
- ("readInt64OffAddrzh", tReadOffAddrzh tInt64zh),
- ("readWord8OffAddrzh", tReadOffAddrzh tWordzh),
- ("readWord16OffAddrzh", tReadOffAddrzh tWordzh),
- ("readWord32OffAddrzh", tReadOffAddrzh tWord32zh),
- ("readWord64OffAddrzh", tReadOffAddrzh tWord64zh),
-
- ("writeCharOffAddrzh", tWriteOffAddrzh tCharzh),
- ("writeWideCharOffAddrzh", tWriteOffAddrzh tCharzh),
- ("writeIntOffAddrzh", tWriteOffAddrzh tIntzh),
- ("writeWordOffAddrzh", tWriteOffAddrzh tWordzh),
- ("writeAddrOffAddrzh", tWriteOffAddrzh tAddrzh),
- ("writeFloatOffAddrzh", tWriteOffAddrzh tFloatzh),
- ("writeDoubleOffAddrzh", tWriteOffAddrzh tDoublezh),
- ("writeStablePtrOffAddrzh", Tforall ("a",Klifted) (tWriteOffAddrzh (tStablePtrzh (Tvar "a")))),
- ("writeInt8OffAddrzh", tWriteOffAddrzh tIntzh),
- ("writeInt16OffAddrzh", tWriteOffAddrzh tIntzh),
- ("writeInt32OffAddrzh", tWriteOffAddrzh tInt32zh),
- ("writeInt64OffAddrzh", tWriteOffAddrzh tInt64zh),
- ("writeWord8OffAddrzh", tWriteOffAddrzh tWordzh),
- ("writeWord16OffAddrzh", tWriteOffAddrzh tWordzh),
- ("writeWord32OffAddrzh", tWriteOffAddrzh tWord32zh),
- ("writeWord64OffAddrzh", tWriteOffAddrzh tWord64zh),
-
- ("sameMutableArrayzh", Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
- (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
- tBool)))),
- ("sameMutableByteArrayzh", Tforall ("s",Klifted)
- (tArrow (tMutableByteArrayzh (Tvar "s"))
- (tArrow (tMutableByteArrayzh (Tvar "s"))
- tBool))),
- ("readArrayzh",Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
- (tArrow tIntzh
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple[tStatezh (Tvar "s"), Tvar "a"])))))),
- ("writeArrayzh",Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
- (tArrow tIntzh
- (tArrow (Tvar "a")
- (tArrow (tStatezh (Tvar "s"))
- (tStatezh (Tvar "s")))))))),
- ("indexArrayzh", Tforall ("a",Klifted)
- (tArrow (tArrayzh (Tvar "a"))
- (tArrow tIntzh
- (tUtuple[Tvar "a"])))),
- ("unsafeFreezzeArrayzh",Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple[tStatezh (Tvar "s"),tArrayzh (Tvar "a")]))))),
- ("unsafeFreezzeByteArrayzh",Tforall ("s",Klifted)
- (tArrow (tMutableByteArrayzh (Tvar "s"))
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple[tStatezh (Tvar "s"),tByteArrayzh])))),
- ("unsafeThawArrayzh",Tforall ("a",Klifted)
- (Tforall ("s",Klifted)
- (tArrow (tArrayzh (Tvar "a"))
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple[tStatezh (Tvar "s"),tMutableArrayzh (Tvar "s") (Tvar "a")]))))),
- ("sizzeofByteArrayzh", tArrow tByteArrayzh tIntzh),
- ("sizzeofMutableByteArrayzh", Tforall ("s",Klifted) (tArrow (tMutableByteArrayzh (Tvar "s")) tIntzh))]
- where
- tReadMutableByteArrayzh t =
- Tforall ("s",Klifted)
- (tArrow (tMutableByteArrayzh (Tvar "s"))
- (tArrow tIntzh
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple [tStatezh (Tvar "s"),t]))))
-
- tWriteMutableByteArrayzh t =
- Tforall ("s",Klifted)
- (tArrow (tMutableByteArrayzh (Tvar "s"))
- (tArrow tIntzh
- (tArrow t
- (tArrow (tStatezh (Tvar "s"))
- (tStatezh (Tvar "s"))))))
-
- tReadOffAddrzh t =
- Tforall ("s",Klifted)
- (tArrow tAddrzh
- (tArrow tIntzh
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple [tStatezh (Tvar "s"),t]))))
-
-
- tWriteOffAddrzh t =
- Tforall ("s",Klifted)
- (tArrow tAddrzh
- (tArrow tIntzh
- (tArrow t
- (tArrow (tStatezh (Tvar "s"))
- (tStatezh (Tvar "s"))))))
-
-{- MutVars -}
-
-tcMutVarzh = pvz "MutVar"
-tMutVarzh s t = Tapp (Tapp (Tcon tcMutVarzh) s) t
-ktMutVarzh = Karrow Klifted (Karrow Klifted Kunlifted)
-
-opsMutVarzh = [
- ("newMutVarzh", Tforall ("a",Klifted)
- (Tforall ("s",Klifted)
- (tArrow (Tvar "a") (tArrow (tStatezh (Tvar "s"))
- (tUtuple [tStatezh (Tvar "s"),
- tMutVarzh (Tvar "s") (Tvar "a")]))))),
- ("readMutVarzh", Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMutVarzh (Tvar "s")(Tvar "a"))
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple [tStatezh (Tvar "s"), Tvar "a"]))))),
- ("writeMutVarzh", Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMutVarzh (Tvar "s") (Tvar "a"))
- (tArrow (Tvar "a")
- (tArrow (tStatezh (Tvar "s"))
- (tStatezh (Tvar "s"))))))),
- ("sameMutVarzh", Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMutVarzh (Tvar "s") (Tvar "a"))
- (tArrow (tMutVarzh (Tvar "s") (Tvar "a"))
- tBool))))]
-
{- Real world and state. -}
-- tjc: why isn't this one unboxed?
+tcRealWorld :: Qual Tcon
tcRealWorld = pv "RealWorld"
+tRealWorld :: Ty
tRealWorld = Tcon tcRealWorld
-ktRealWorld = Klifted
+tcStatezh :: Qual Tcon
tcStatezh = pvz "State"
+tStatezh :: Ty -> Ty
tStatezh t = Tapp (Tcon tcStatezh) t
-ktStatezh = Karrow Klifted Kunlifted
-
-tRWS = tStatezh tRealWorld
-
-opsState = [
- ("realWorldzh", tRWS)]
-
-{- Exceptions -}
-
--- no primitive type
-opsExn = [
- ("catchzh",
- let t' = tArrow tRWS (tUtuple [tRWS, Tvar "a"]) in
- Tforall ("a",Klifted)
- (Tforall ("b",Klifted)
- (tArrow t'
- (tArrow (tArrow (Tvar "b") t')
- t')))),
- ("raisezh", Tforall ("a",Klifted)
- (Tforall ("b",Klifted)
- (tArrow (Tvar "a") (Tvar "b")))),
- ("blockAsyncExceptionszh", Tforall ("a",Klifted)
- (tArrow (tArrow tRWS (tUtuple[tRWS,Tvar "a"]))
- (tArrow tRWS (tUtuple[tRWS,Tvar "a"])))),
- ("unblockAsyncExceptionszh", Tforall ("a",Klifted)
- (tArrow (tArrow tRWS (tUtuple[tRWS,Tvar "a"]))
- (tArrow tRWS (tUtuple[tRWS,Tvar "a"]))))]
-
-{- Mvars -}
-
-tcMVarzh = pvz "MVar"
-tMVarzh s t = Tapp (Tapp (Tcon tcMVarzh) s) t
-ktMVarzh = Karrow Klifted (Karrow Klifted Kunlifted)
-
-opsMVar = [
- ("newMVarzh", Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple[tStatezh (Tvar "s"),tMVarzh (Tvar "s") (Tvar "a")])))),
- ("takeMVarzh", Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple[tStatezh (Tvar "s"),Tvar "a"]))))),
- ("tryTakeMVarzh", Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple[tStatezh (Tvar "s"),tIntzh,Tvar "a"]))))),
- ("putMVarzh", Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
- (tArrow (Tvar "a")
- (tArrow (tStatezh (Tvar "s"))
- (tStatezh (Tvar "s"))))))),
- ("tryPutMVarzh", Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
- (tArrow (Tvar "a")
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple [tStatezh (Tvar "s"), tIntzh])))))),
- ("sameMVarzh", Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
- (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
- tBool)))),
- ("isEmptyMVarzh", Tforall ("s",Klifted)
- (Tforall ("a",Klifted)
- (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
- (tArrow (tStatezh (Tvar "s"))
- (tUtuple[tStatezh (Tvar "s"),tIntzh])))))]
-
-
-{- Weak Objects -}
-tcWeakzh = pvz "Weak"
-tWeakzh t = Tapp (Tcon tcWeakzh) t
-ktWeakzh = Karrow Klifted Kunlifted
-
-opsWeak = [
- ("mkWeakzh", Tforall ("o",Kopen)
- (Tforall ("b",Klifted)
- (Tforall ("c",Klifted)
- (tArrow (Tvar "o")
- (tArrow (Tvar "b")
- (tArrow (Tvar "c")
- (tArrow tRWS (tUtuple[tRWS, tWeakzh (Tvar "b")])))))))),
- ("deRefWeakzh", Tforall ("a",Klifted)
- (tArrow (tWeakzh (Tvar "a"))
- (tArrow tRWS (tUtuple[tRWS, tIntzh, Tvar "a"])))),
- ("finalizeWeakzh", Tforall ("a",Klifted)
- (tArrow (tWeakzh (Tvar "a"))
- (tArrow tRWS
- (tUtuple[tRWS,tIntzh,
- tArrow tRWS (tUtuple[tRWS, tUnit])]))))]
-
-
-{- Foreign Objects -}
-
-tcForeignObjzh = pvz "ForeignObj"
-tForeignObjzh = Tcon tcForeignObjzh
-ktForeignObjzh = Kunlifted
-
-opsForeignObjzh = [
- ("mkForeignObjzh", tArrow tAddrzh
- (tArrow tRWS (tUtuple [tRWS,tForeignObjzh]))),
- ("writeForeignObjzh", Tforall ("s",Klifted)
- (tArrow tForeignObjzh
- (tArrow tAddrzh
- (tArrow (tStatezh (Tvar "s")) (tStatezh (Tvar "s")))))),
- ("foreignObjToAddrzh", tArrow tForeignObjzh tAddrzh),
- ("touchzh", Tforall ("o",Kopen)
- (tArrow (Tvar "o")
- (tArrow tRWS tRWS)))]
-
-
-{- Stable Pointers (but not names) -}
-
-tcStablePtrzh = pvz "StablePtr"
-tStablePtrzh t = Tapp (Tcon tcStablePtrzh) t
-ktStablePtrzh = Karrow Klifted Kunlifted
-
-opsStablePtrzh = [
- ("makeStablePtrzh", Tforall ("a",Klifted)
- (tArrow (Tvar "a")
- (tArrow tRWS (tUtuple[tRWS,tStablePtrzh (Tvar "a")])))),
- ("deRefStablePtrzh", Tforall ("a",Klifted)
- (tArrow (tStablePtrzh (Tvar "a"))
- (tArrow tRWS (tUtuple[tRWS,Tvar "a"])))),
- ("eqStablePtrzh", Tforall ("a",Klifted)
- (tArrow (tStablePtrzh (Tvar "a"))
- (tArrow (tStablePtrzh (Tvar "a")) tIntzh)))]
-
-{- Concurrency operations -}
-
-tcThreadIdzh = pvz "ThreadId"
-tThreadIdzh = Tcon tcThreadIdzh
-ktThreadIdzh = Kunlifted
-
-opsConc = [
- ("seqzh", Tforall ("a",Klifted)
- (tArrow (Tvar "a") tIntzh)),
- ("parzh", Tforall ("a",Klifted)
- (tArrow (Tvar "a") tIntzh)),
- ("delayzh", Tforall ("s",Klifted)
- (tArrow tIntzh (tArrow (tStatezh (Tvar "s")) (tStatezh (Tvar "s"))))),
- ("waitReadzh", Tforall ("s",Klifted)
- (tArrow tIntzh (tArrow (tStatezh (Tvar "s")) (tStatezh (Tvar "s"))))),
- ("waitWritezh", Tforall ("s",Klifted)
- (tArrow tIntzh (tArrow (tStatezh (Tvar "s")) (tStatezh (Tvar "s"))))),
- ("forkzh", Tforall ("a",Klifted)
- (tArrow (Tvar "a")
- (tArrow tRWS (tUtuple[tRWS,tThreadIdzh])))),
- ("killThreadzh", Tforall ("a",Klifted)
- (tArrow tThreadIdzh
- (tArrow (Tvar "a")
- (tArrow tRWS tRWS)))),
- ("yieldzh", tArrow tRWS tRWS),
- ("myThreadIdzh", tArrow tRWS (tUtuple[tRWS, tThreadIdzh]))]
-
-{- Miscellaneous operations -}
-
-opsMisc = [
- ("dataToTagzh", Tforall ("a",Klifted)
- (tArrow (Tvar "a") tIntzh)),
- ("tagToEnumzh", Tforall ("a",Klifted)
- (tArrow tIntzh (Tvar "a"))),
- ("unsafeCoercezh", Tforall ("a",Kopen)
- (Tforall ("b",Kopen)
- (tArrow (Tvar "a") (Tvar "b")))) -- maybe unneeded
- ]
-
-{- CCallable and CReturnable.
- We just define the type constructors for the dictionaries
- corresponding to these pseudo-classes. -}
-
-tcZCTCCallable = pv "ZCTCCallable"
-ktZCTCCallable = Karrow Kopen Klifted -- ??
-tcZCTCReturnable = pv "ZCTCReturnable"
-ktZCTCReturnable = Karrow Kopen Klifted -- ??
+{- Properly defined in PrelError, but needed in many modules before that. -}
+errorVals :: [(Var, Ty)]
+errorVals = [
+ ("error", Tforall ("a",Kopen) (tArrow tString (Tvar "a"))),
+ ("irrefutPatError", str2A),
+ ("patError", str2A),
+ ("divZZeroError", forallAA),
+ ("overflowError", forallAA)]
{- Non-primitive, but mentioned in the types of primitives. -}
+bv :: a -> Qual a
bv = qual baseMname
-tcUnit = bv "Unit"
-tUnit = Tcon tcUnit
-ktUnit = Klifted
-tcBool = bv "Bool"
-tBool = Tcon tcBool
-ktBool = Klifted
+str2A, forallAA :: Ty
+str2A = Tforall ("a",Kopen) (tArrow tAddrzh (Tvar "a"))
+forallAA = Tforall ("a",Kopen) (Tvar "a")
-{- Properly defined in PrelError, but needed in many modules before that. -}
-errorVals = [
- ("error", Tforall ("a",Kopen) (tArrow tString (Tvar "a"))),
- ("irrefutPatError", Tforall ("a",Kopen) (tArrow tString (Tvar "a"))),
- ("patError", Tforall ("a",Kopen) (tArrow tString (Tvar "a")))]
-
+tcChar :: Qual Tcon
tcChar = bv "Char"
+tChar :: Ty
tChar = Tcon tcChar
-ktChar = Klifted
+tcList :: Qual Tcon
tcList = bv "ZMZN"
+tList :: Ty -> Ty
tList t = Tapp (Tcon tcList) t
-ktList = Karrow Klifted Klifted
+tString :: Ty
tString = tList tChar
-
-{- Utilities for building types -}
-tmonadic t = tArrow t t
-tdyadic t = tArrow t (tArrow t t)
-tcompare t = tArrow t (tArrow t tBool)
-
+{-# OPTIONS -Werror -Wall -fno-warn-missing-signatures #-}
+
module Printer where
import Text.PrettyPrint.HughesPJ
-import Numeric (fromRat)
import Char
import Core
import Encoding
+import PrimCoercions
instance Show Module where
- showsPrec d m = shows (pmodule m)
+ showsPrec _ m = shows (pmodule m)
instance Show Tdef where
- showsPrec d t = shows (ptdef t)
+ showsPrec _ t = shows (ptdef t)
instance Show Cdef where
- showsPrec d c = shows (pcdef c)
+ showsPrec _ c = shows (pcdef c)
instance Show Vdefg where
- showsPrec d v = shows (pvdefg v)
+ showsPrec _ v = shows (pvdefg v)
instance Show Vdef where
- showsPrec d v = shows (pvdef v)
+ showsPrec _ v = shows (pvdef v)
instance Show Exp where
- showsPrec d e = shows (pexp e)
+ showsPrec _ e = shows (pexp e)
instance Show Alt where
- showsPrec d a = shows (palt a)
+ showsPrec _ a = shows (palt a)
instance Show Ty where
- showsPrec d t = shows (pty t)
+ showsPrec _ t = shows (pty t)
instance Show Kind where
- showsPrec d k = shows (pkind k)
+ showsPrec _ k = shows (pkind k)
instance Show Lit where
- showsPrec d l = shows (plit l)
+ showsPrec _ l = shows (plit l)
instance Show CoreLit where
- showsPrec d l = shows (pclit l)
+ showsPrec _ l = shows (pclit l)
+
+instance Show KindOrCoercion where
+ showsPrec _ (Kind k) = shows (text "<K" <+> pkind k <> text ">")
+ showsPrec _ (Coercion (DefinedCoercion tbs (t1,t2))) =
+ shows (text "<C" <+> hsep (map ptbind tbs) <+>
+ parens (pkind (Keq t1 t2)) <> text ">")
indent = nest 2
(text "%data" <+> pqname qtcon <+> (hsep (map ptbind tbinds)) <+> char '=')
$$ indent (braces ((vcat (punctuate (char ';') (map pcdef cdefs)))))
-ptdef (Newtype qtcon tbinds (coercion,k) tyopt) =
+ptdef (Newtype qtcon tbinds (coercion,cTbs,k) tyopt) =
text "%newtype" <+> pqname qtcon <+> (hsep (map ptbind tbinds))
$$ indent (axiomclause $$ repclause)
- where axiomclause = char '^' <+> parens (pqname coercion <+> text "::"
- <+> pkind k)
+ where axiomclause = char '^' <+> parens (pqname coercion <+>
+ (hsep (map ptbind cTbs)) <+>
+ text "::"
+ <+> peqkind k)
repclause = case tyopt of
Just ty -> char '=' <+> pty ty
Nothing -> empty
pcdef (Constr qdcon tbinds tys) =
(pqname qdcon) <+> (sep [hsep (map pattbind tbinds),sep (map paty tys)])
-pname id = text id
+pname = text
-pqname (m,id) = pmname m <> pname id
+pqname (m,v) = pmname m <> pname v
-- be sure to print the '.' here so we don't print out
-- ".foo" for unqualified foo...
-- "%module foo" doesn't get printed as "%module ^foo"
pmname (Just m) = char '^' <> panmname m <> char '.'
-panmname p@(pkgName, parents, name) =
+panmname (pkgName, parents, name) =
let parentStrs = map pname parents in
pname pkgName <> char ':' <>
-- This is to be sure to not print out:
pakind k = parens (pkind k)
pkind (Karrow k1 k2) = parens (pakind k1 <> text "->" <> pkind k2)
-pkind (Keq t1 t2) = parens (parens (pty t1) <+> text ":=:" <+> parens (pty t2))
+pkind (Keq from to) = peqkind (from,to)
pkind k = pakind k
+peqkind (t1, t2) = parens (parens (pty t1) <+> text ":=:" <+> parens (pty t2))
+
paty (Tvar n) = pname n
paty (Tcon c) = pqname c
+paty (TransCoercion t1 t2) =
+ parens (sep ([pqname transCoercion, pbty t1, pbty t2]))
+paty (SymCoercion t) =
+ parens (sep [pqname symCoercion, paty t])
+paty (UnsafeCoercion t1 t2) =
+ parens (sep [pqname unsafeCoercion, pbty t1, pbty t2])
+paty (LeftCoercion t) =
+ parens (pqname leftCoercion <+> paty t)
+paty (RightCoercion t) =
+ parens (pqname rightCoercion <+> paty t)
paty t = parens (pty t)
pbty (Tapp(Tapp(Tcon tc) t1) t2) | tc == tcArrow = parens(fsep [pbty t1, text "->",pty t2])
pappexp (App e1 e2) as = pappexp e1 (Left e2:as)
pappexp (Appt e t) as = pappexp e (Right t:as)
pappexp e as = fsep (paexp e : map pa as)
- where pa (Left e) = paexp e
+ where pa (Left ex) = paexp ex
pa (Right t) = char '@' <+> paty t
pexp (Lam b e) = char '\\' <+> plamexp [b] e
h0 = intToDigit r1
hs = dropWhile (=='0') $ reverse $ mkHex cv
mkHex 0 = ""
- mkHex cv = intToDigit r : mkHex q
- where (q,r) = quotRem cv 16
+ mkHex num = intToDigit r : mkHex q
+ where (q,r) = quotRem num 16
f cv rest = (chr cv):rest
In particular, typechecker and interpreter give a precise semantics.
To build, run "make".
+---------------------
+tjc April 2008:
+
+==== Notes ====
+
+The checker should work on most programs. Bugs I'm aware of:
+1. GHC generates some questionable coercion applications involving
+ partially-applied function arrows (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.
+
+2. 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.
+
+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
+better than I do, could update the old happy parser, which is still in the
+repo.)
+
+The interpreter is not working yet.
+
+==== Building ====
+
+To run the checker and interpreter, you need to generate External Core
+for all the base, integer and ghc-prim libraries. This can be done by
+adding "-fext-core" to the GhcLibHcOpts in your build.mk file, then
+running "make" under libraries/.
-To run the checker and interpreter (which currently aren't working anyway),
-you need to generate External Core for all the base, integer and ghc-prim
-libraries. This can be done by adding "-fext-core" to the GhcLibHcOpts in
-your build.mk file, then running "make" under libraries/.
Then you need to edit Driver.hs and change "baseDir" to point to your GHC
libraries directory.
-Most recently tested with GHC 6.8.2. I make no claims of portability. --tjc
+Once you've done that:
+1. make prims (to generate the primops file)
+2. make
+3. make nofibtest (to run the parser/checker on all nofib programs...
+ for example.)
+
+Tested with GHC 6.8.2. I make no claims of portability.
+
projects / ghc-hetmet.git / commitdiff