module DDC.Core.Check.Module
( checkModule
, checkModuleM)
where
import DDC.Core.Check.Base (checkTypeM, applySolved)
import DDC.Core.Check.Exp
import DDC.Core.Check.Error
import DDC.Core.Transform.Reannotate
import DDC.Core.Transform.MapT
import DDC.Core.Module
import DDC.Core.Exp
import DDC.Type.Check.Context
import DDC.Type.Check.Data
import DDC.Type.Compounds
import DDC.Type.Predicates
import DDC.Type.DataDef
import DDC.Type.Equiv
import DDC.Type.Universe
import DDC.Base.Pretty
import DDC.Type.Env (KindEnv, TypeEnv)
import DDC.Control.Monad.Check (runCheck, throw)
import DDC.Data.ListUtils
import Control.Monad
import qualified DDC.Type.Env as Env
import qualified Data.Map.Strict as Map
checkModule
:: (Show a, Ord n, Show n, Pretty n)
=> Config n
-> Module a n
-> Mode n
-> ( Either (Error a n) (Module (AnTEC a n) n)
, CheckTrace )
checkModule !config !xx !mode
= let (s, result) = runCheck (mempty, 0, 0)
$ checkModuleM config
(configPrimKinds config)
(configPrimTypes config)
xx mode
(tr, _, _) = s
in (result, tr)
checkModuleM
:: (Show a, Ord n, Show n, Pretty n)
=> Config n
-> KindEnv n
-> TypeEnv n
-> Module a n
-> Mode n
-> CheckM a n (Module (AnTEC a n) n)
checkModuleM !config !kenv !tenv mm@ModuleCore{} !mode
= do
nksImported' <- checkImportTypes config mode
$ moduleImportTypes mm
let defsImported = moduleImportDataDefs mm
defsImported' <- case checkDataDefs config defsImported of
(err : _, _) -> throw $ ErrorData err
([], defsImported') -> return defsImported'
let config_import = config
{ configDataDefs = unionDataDefs (configDataDefs config)
(fromListDataDefs defsImported') }
let kenv_import = Env.union kenv
$ Env.fromList [ BName n (kindOfImportType isrc)
| (n, isrc) <- nksImported' ]
ntsImportCap' <- checkImportCaps config_import kenv_import mode
$ moduleImportCaps mm
let bsImportCap = [ BName n (typeOfImportCap isrc)
| (n, isrc) <- ntsImportCap' ]
ntsImportValue' <- checkImportValues config_import kenv_import mode
$ moduleImportValues mm
let defsLocal = moduleDataDefsLocal mm
defsLocal' <- case checkDataDefs config defsLocal of
(err : _, _) -> throw $ ErrorData err
([], defsLocal') -> return defsLocal'
let defs_top = unionDataDefs (configDataDefs config)
$ unionDataDefs (fromListDataDefs defsImported')
(fromListDataDefs defsLocal')
let caps_top = Env.fromList
$ [BName n t | (n, ImportCapAbstract t) <- ntsImportCap' ]
let config_top = config
{ configDataDefs = defs_top
, configGlobalCaps = caps_top }
let kenv_top = kenv_import
let tenv_top = Env.unions
[ tenv
, Env.fromList [ BName n (typeOfImportValue isrc)
| (n, isrc) <- ntsImportValue' ]
, Env.fromList [ BName n (typeOfImportCap isrc)
| (n, isrc) <- ntsImportCap' ]
]
let ctx_top = pushTypes bsImportCap emptyContext
esrcsType' <- checkExportTypes config_top
$ moduleExportTypes mm
esrcsValue' <- checkExportValues config_top kenv_top
$ moduleExportValues mm
(x', _, _effs, ctx)
<- checkExpM (makeTable config_top kenv_top tenv_top)
ctx_top mode DemandNone (moduleBody mm)
let applyToAnnot (AnTEC t0 e0 _ x0)
= do t0' <- applySolved ctx t0
e0' <- applySolved ctx e0
return $ AnTEC t0' e0' (tBot kClosure) x0
xx_solved <- mapT (applySolved ctx) x'
xx_annot <- reannotateM applyToAnnot xx_solved
let mm_inferred
= mm
{ moduleExportTypes = esrcsType'
, moduleImportTypes = nksImported'
, moduleImportCaps = ntsImportCap'
, moduleImportValues = ntsImportValue'
, moduleBody = xx_annot }
tenv_binds <- checkModuleBinds
(moduleExportTypes mm_inferred)
(moduleExportValues mm_inferred)
xx_annot
let tenv_exportable = Env.union tenv_top tenv_binds
when (not $ moduleIsHeader mm_inferred)
$ mapM_ (checkBindDefined tenv_exportable)
$ map fst $ moduleExportValues mm_inferred
let updateExportSource e
| ExportSourceLocalNoType n <- e
, Just t <- Env.lookup (UName n) tenv_exportable
= ExportSourceLocal n t
| otherwise = e
let esrcsValue_updated
= [ (n, updateExportSource e) | (n, e) <- esrcsValue' ]
let mm_final
= mm_inferred
{ moduleExportValues = esrcsValue_updated }
return mm_final
checkExportTypes
:: (Show n, Pretty n, Ord n)
=> Config n
-> [(n, ExportSource n)]
-> CheckM a n [(n, ExportSource n)]
checkExportTypes config nesrcs
= let check (n, esrc)
| Just k <- takeTypeOfExportSource esrc
= do (k', _, _) <- checkTypeM config Env.empty emptyContext UniverseKind k Recon
return $ (n, mapTypeOfExportSource (const k') esrc)
| otherwise
= return (n, esrc)
in do
let dups = findDuplicates $ map fst nesrcs
(case takeHead dups of
Just n -> throw $ ErrorExportDuplicate n
_ -> return ())
mapM check nesrcs
checkExportValues
:: (Show n, Pretty n, Ord n)
=> Config n -> KindEnv n
-> [(n, ExportSource n)]
-> CheckM a n [(n, ExportSource n)]
checkExportValues config kenv nesrcs
= let check (n, esrc)
| Just t <- takeTypeOfExportSource esrc
= do (t', _, _) <- checkTypeM config kenv emptyContext UniverseSpec t Recon
return $ (n, mapTypeOfExportSource (const t') esrc)
| otherwise
= return (n, esrc)
in do
let dups = findDuplicates $ map fst nesrcs
(case takeHead dups of
Just n -> throw $ ErrorExportDuplicate n
_ -> return ())
mapM check nesrcs
checkImportTypes
:: (Ord n, Show n, Pretty n)
=> Config n -> Mode n
-> [(n, ImportType n)]
-> CheckM a n [(n, ImportType n)]
checkImportTypes config mode nisrcs
= let
modeCheckImportTypes
= case mode of
Recon -> Recon
_ -> Synth
check (n, isrc)
= do let k = kindOfImportType isrc
(k', _, _) <- checkTypeM config Env.empty emptyContext UniverseKind
k modeCheckImportTypes
return (n, mapKindOfImportType (const k') isrc)
pack !mm []
= return $ Map.toList mm
pack !mm ((n, isrc) : nis)
= case Map.lookup n mm of
Just isrc'
| compat isrc isrc' -> pack mm nis
| otherwise -> throw $ ErrorImportDuplicate n
Nothing -> pack (Map.insert n isrc mm) nis
compat (ImportTypeAbstract k1) (ImportTypeAbstract k2) = equivT k1 k2
compat (ImportTypeBoxed k1) (ImportTypeBoxed k2) = equivT k1 k2
compat _ _ = False
in do
nisrcs' <- mapM check nisrcs
pack Map.empty nisrcs'
checkImportCaps
:: (Ord n, Show n, Pretty n)
=> Config n -> KindEnv n -> Mode n
-> [(n, ImportCap n)]
-> CheckM a n [(n, ImportCap n)]
checkImportCaps config kenv mode nisrcs
= let
modeCheckImportCaps
= case mode of
Recon -> Recon
_ -> Check kEffect
check (n, isrc)
= do let t = typeOfImportCap isrc
(t', k, _) <- checkTypeM config kenv emptyContext UniverseSpec
t modeCheckImportCaps
when (not $ isEffectKind k)
$ throw $ ErrorImportCapNotEffect n
return (n, mapTypeOfImportCap (const t') isrc)
pack !mm []
= return $ Map.toList mm
pack !mm ((n, isrc) : nis)
= case Map.lookup n mm of
Just isrc'
| compat isrc isrc' -> pack mm nis
| otherwise -> throw $ ErrorImportDuplicate n
Nothing -> pack (Map.insert n isrc mm) nis
compat (ImportCapAbstract t1) (ImportCapAbstract t2) = equivT t1 t2
in do
nisrcs' <- mapM check nisrcs
pack Map.empty nisrcs'
checkImportValues
:: (Ord n, Show n, Pretty n)
=> Config n -> KindEnv n -> Mode n
-> [(n, ImportValue n)]
-> CheckM a n [(n, ImportValue n)]
checkImportValues config kenv mode nisrcs
= let
modeCheckImportTypes
= case mode of
Recon -> Recon
_ -> Check kData
check (n, isrc)
= do let t = typeOfImportValue isrc
(t', k, _) <- checkTypeM config kenv emptyContext UniverseSpec
t modeCheckImportTypes
when (not $ isDataKind k)
$ throw $ ErrorImportValueNotData n
return (n, mapTypeOfImportValue (const t') isrc)
pack !mm []
= return $ Map.toList mm
pack !mm ((n, isrc) : nis)
= case Map.lookup n mm of
Just isrc'
| compat isrc isrc' -> pack mm nis
| otherwise -> throw $ ErrorImportDuplicate n
Nothing -> pack (Map.insert n isrc mm) nis
compat (ImportValueModule _ _ t1 a1)
(ImportValueModule _ _ t2 a2)
= equivT t1 t2 && a1 == a2
compat (ImportValueSea _ t1)
(ImportValueSea _ t2)
= equivT t1 t2
compat _ _ = False
in do
nisrcs' <- mapM check nisrcs
pack Map.empty nisrcs'
checkModuleBinds
:: Ord n
=> [(n, ExportSource n)]
-> [(n, ExportSource 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 _ (LPrivate _ _ _) x2
-> checkModuleBinds ksExports tsExports x2
_ -> return Env.empty
checkModuleBind
:: Ord n
=> [(n, ExportSource n)]
-> [(n, ExportSource n)]
-> Bind n
-> CheckM a n ()
checkModuleBind !_ksExports !tsExports !b
| BName n tDef <- b
= case join $ liftM takeTypeOfExportSource $ 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