checkExpr, checkType,
primCoercionError,
Menv, Venv, Tvenv, Envs(..),
- CheckRes(..), splitTy, substl) where
+ CheckRes(..), splitTy, substl,
+ mkTypeEnvsNoChecking) where
import Language.Core.Core
import Language.Core.Printer()
import Language.Core.PrimEnv
import Language.Core.Env
+import Language.Core.Environments
import Control.Monad.Reader
import Data.List
require False s = fail s
require True _ = return ()
-{- Environments. -}
-type Tvenv = Env Tvar Kind -- type variables (local only)
-type Tcenv = Env Tcon KindOrCoercion -- type constructors
-type Cenv = Env Dcon Ty -- data constructors
-type Venv = Env Var Ty -- values
-type Menv = Env AnMname Envs -- modules
-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
- 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) =
lookupM env k =
case elookup env k of
Just v -> return v
- Nothing -> fail ("undefined identifier: " ++ show k)
+ Nothing -> fail ("undefined identifier: " ++ show k ++ " e = " ++ show (edomain env))
{- Main entry point. -}
checkModule :: Menv -> Module -> CheckRes Menv
vdefIsMainWrapper enclosing defining =
enclosing == mainMname && defining == wrapperMainAnMname
-checkExpr :: AnMname -> Menv -> [Tdef] -> Venv -> Tvenv
+checkExpr :: AnMname -> Menv -> Tcenv -> Cenv -> Venv -> Tvenv
-> Exp -> Ty
-checkExpr mn menv tdefs venv tvenv e = case runReaderT (do
- (tcenv, cenv) <- mkTypeEnvs tdefs
+checkExpr mn menv _tcenv _cenv venv tvenv e = case runReaderT (do
+ --(tcenv, cenv) <- mkTypeEnvs tdefs
-- Since the preprocessor calls checkExpr after code has been
-- typechecked, we expect to find the external env in the Menv.
case (elookup menv mn) of
Just thisEnv ->
- checkExp (tcenv, tvenv, cenv, (venv_ thisEnv), venv) e
+ checkExp ({-tcenv-}tcenv_ thisEnv, tvenv, {-cenv-}cenv_ thisEnv, (venv_ thisEnv), venv) e
Nothing -> reportError e ("checkExpr: Environment for " ++
show mn ++ " not found")) (mn,menv) of
OkC t -> t
FailC s -> reportError e s
-checkType :: AnMname -> Menv -> [Tdef] -> Tvenv -> Ty -> Kind
-checkType mn menv tdefs tvenv t = case runReaderT (do
- (tcenv, _) <- mkTypeEnvs tdefs
- checkTy (tcenv, tvenv) t) (mn, menv) of
+checkType :: AnMname -> Menv -> Tcenv -> Tvenv -> Ty -> Kind
+checkType mn menv _tcenv tvenv t =
+ case runReaderT (checkTy (tcenv_ (fromMaybe (error "checkType") (elookup menv mn)), tvenv) t) (mn, menv) of
OkC k -> k
- FailC s -> reportError tvenv s
+ FailC s -> reportError tvenv (s ++ "\n " ++ show menv ++ "\n mname =" ++ show mn)
checkExp :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
checkExp (tcenv,tvenv,cenv,e_venv,l_venv) = ch
import Language.Core.Core
import Language.Core.Env
import Language.Core.Check
+import Language.Core.Environments
+import Language.Core.Encoding
prepModule :: Menv -> Module -> Module
prepModule globalEnv (Module mn tdefs vdefgs) =
Module mn tdefs vdefgs'
where
- (_,vdefgs') = foldl prepTopVdefg (eempty,[]) vdefgs
+ (tcenv, cenv) = mkTypeEnvsNoChecking tdefs
+ (_,vdefgs') = foldl' prepTopVdefg (eempty,[]) vdefgs
prepTopVdefg (venv,vdefgs) vdefg = (venv',vdefgs ++ [vdefg'])
where (venv',vdefg') = prepVdefg (venv,eempty) vdefg
(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])
- where venv' = foldl eextend venv [(x,t) | Vdef((Nothing,x),t,_) <- vdefs]
+ where venv' = foldl' eextend venv [(x,t) | Vdef((Nothing,x),t,_) <- vdefs]
prepExp _ (Var qv) = Var qv
prepExp _ (Dcon qdc) = Dcon qdc
-- We need to know the type of the let body in order to construct
-- a case expression.
-- need to extend the env with the let-bound var too!
- let eTy = typeOfExp (eextend venv (x, t), tvenv) e in
+ 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)]
prepExp env (Note s e) = Note s (prepExp env e)
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 (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)
prepAlt env (Adefault e) = Adefault (prepExp env e)
etaExpand :: [Kind] -> [Ty] -> Exp -> Exp
etaExpand ks ts e =
-- what a pain
- let tyArgs = [("$t_"++(show i),k) | (i, k) <- zip [(1::Integer)..] ks]
- termArgs = [ ('$':(show i),t) | (i,t) <- zip [(1::Integer)..] ts] in
+ let tyArgs = [(zEncodeString $ "$t_"++(show i),k) | (i, k) <- zip [(1::Integer)..] ks]
+ termArgs = [ (zEncodeString $ '$':(show i),t) | (i,t) <- zip [(1::Integer)..] ts] in
foldr (\ (t1,k1) e -> Lam (Tb (t1,k1)) e)
(foldr (\ (v,t) e -> Lam (Vb (v,t)) e)
- (foldl (\ e (v,_) -> App e (Var (unqual v)))
- (foldl (\ e (tv,_) -> Appt e (Tvar tv))
+ (foldl' (\ e (v,_) -> App e (Var (unqual v)))
+ (foldl' (\ e (tv,_) -> Appt e (Tvar tv))
e tyArgs)
termArgs) termArgs)
tyArgs
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 newScrut (v,t) (typeOfExp env' rhs) [Adefault rhs]
+ Case newScrut (v,t) (typeOfExp venv' tvenv rhs) [Adefault rhs]
where newScrut = prepExp env e2
- rhs = (rewindApp env' (App e1 (Var (unqual v))) as)
+ rhs = (rewindApp (venv', tvenv) (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*
-- 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)
+ t = typeOfExp venv tvenv e2
+ venv' = eextend venv (v,t)
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 vs = maximum ("":vs) ++ "x" -- one simple way!
-
- typeOfExp :: (Venv, Tvenv) -> Exp -> Ty
- typeOfExp = uncurry (checkExpr mn globalEnv tdefs)
+
+ typeOfExp :: Venv -> Tvenv -> Exp -> Ty
+ typeOfExp = checkExpr mn globalEnv tcenv cenv
kindOfTy :: Tvenv -> Ty -> Kind
- kindOfTy tvenv = checkType mn globalEnv tdefs tvenv
+ kindOfTy tvenv = checkType mn globalEnv tcenv tvenv
{- Return false for those expressions for which Interp.suspendExp builds a thunk. -}
suspends (Var _) = False