module DDC.Core.Check.CheckModule
( checkModule
, checkModuleM)
where
import DDC.Core.Module
import DDC.Core.Exp
import DDC.Core.Check.CheckExp
import DDC.Core.Check.Error
import DDC.Type.Compounds
import DDC.Base.Pretty
import DDC.Type.Equiv
import DDC.Type.Env (KindEnv, TypeEnv)
import DDC.Control.Monad.Check (result, throw)
import Data.Map (Map)
import qualified DDC.Type.Check as T
import qualified DDC.Type.Env as Env
import qualified Data.Map as Map
checkModule
:: (Ord n, Show n, Pretty n)
=> Config n
-> Module a n
-> Either (Error a n) (Module (AnTEC a n) n)
checkModule !config !xx
= result
$ checkModuleM
config
(configPrimKinds config)
(configPrimTypes config)
xx
checkModuleM
:: (Ord n, Show n, Pretty n)
=> Config n
-> KindEnv n
-> TypeEnv n
-> Module a n
-> CheckM a n (Module (AnTEC a n) n)
checkModuleM !config !kenv !tenv mm@ModuleCore{}
= do
let bksImport = [BName n k | (n, (_, k)) <- Map.toList $ moduleImportKinds mm]
let btsImport = [BName n t | (n, (_, t)) <- Map.toList $ moduleImportTypes mm]
mapM_ (checkTypeM config kenv) $ map typeOfBind bksImport
let kenv' = Env.union kenv $ Env.fromList bksImport
mapM_ (checkTypeM config kenv') $ map typeOfBind btsImport
let tenv' = Env.union tenv $ Env.fromList btsImport
mapM_ (checkTypeM config kenv') $ Map.elems $ moduleExportKinds mm
mapM_ (checkTypeM config kenv') $ Map.elems $ moduleExportTypes mm
(x', _, _effs, _) <- checkExpM config kenv' tenv' (moduleBody mm)
envDef <- checkModuleBinds (moduleExportKinds mm) (moduleExportTypes mm) x'
mapM_ (checkBindDefined envDef) $ Map.keys $ moduleExportTypes mm
let mm' = mm { moduleBody = x' }
return mm'
checkModuleBinds
:: Ord n
=> Map n (Kind n)
-> Map n (Type n)
-> Exp (AnTEC a n) n
-> CheckM a n (TypeEnv n)
checkModuleBinds !ksExports !tsExports !xx
= case xx of
XLet _ (LLet b _) x2
-> do checkModuleBind ksExports tsExports b
env <- checkModuleBinds ksExports tsExports x2
return $ Env.extend b env
XLet _ (LRec bxs) x2
-> do mapM_ (checkModuleBind ksExports tsExports) $ map fst bxs
env <- checkModuleBinds ksExports tsExports x2
return $ Env.extends (map fst bxs) env
XLet _ (LLetRegions _ _) x2
-> checkModuleBinds ksExports tsExports x2
_ -> return Env.empty
checkModuleBind
:: Ord n
=> Map n (Kind n)
-> Map n (Type n)
-> Bind n
-> CheckM a n ()
checkModuleBind !_ksExports !tsExports !b
| BName n tDef <- b
= case Map.lookup n tsExports of
Nothing -> return ()
Just tExport
| equivT tDef tExport -> return ()
| otherwise -> throw $ ErrorExportMismatch n tExport tDef
| otherwise
= return ()
checkBindDefined
:: Ord n
=> TypeEnv n
-> n
-> CheckM a n ()
checkBindDefined env n
= case Env.lookup (UName n) env of
Just _ -> return ()
_ -> throw $ ErrorExportUndefined n
checkTypeM :: (Ord n, Show n, Pretty n)
=> Config n
-> KindEnv n
-> Type n
-> CheckM a n (Kind n)
checkTypeM !config !kenv !tt
= case T.checkType config kenv tt of
Left err -> throw $ ErrorType err
Right k -> return k