module DDC.Core.Check.Exp
(
Config (..)
, AnTEC (..)
, Mode (..)
, Demand (..)
, Context
, emptyContext
, checkExp
, typeOfExp
, Table (..)
, makeTable
, CheckM
, checkExpM
, CheckTrace (..))
where
import DDC.Core.Check.Judge.Type.VarCon
import DDC.Core.Check.Judge.Type.LamT
import DDC.Core.Check.Judge.Type.LamX
import DDC.Core.Check.Judge.Type.AppT
import DDC.Core.Check.Judge.Type.AppX
import DDC.Core.Check.Judge.Type.Let
import DDC.Core.Check.Judge.Type.LetPrivate
import DDC.Core.Check.Judge.Type.Case
import DDC.Core.Check.Judge.Type.Cast
import DDC.Core.Check.Judge.Type.Witness
import DDC.Core.Check.Judge.Type.Base
import DDC.Core.Transform.MapT
import qualified DDC.Type.Env as Env
checkExp
:: (Show a, Ord n, Show n, Pretty n)
=> Config n
-> KindEnv n
-> TypeEnv n
-> Mode n
-> Demand
-> Exp a n
-> ( Either (Error a n)
( Exp (AnTEC a n) n
, Type n
, Effect n)
, CheckTrace)
checkExp !config !kenv !tenv !mode !demand !xx
= (result, ct)
where
((ct, _, _), result)
= runCheck (mempty, 0, 0)
$ do
(xx', t, effs, ctx)
<- checkExpM
(makeTable config
(Env.union kenv (configPrimKinds config))
(Env.union tenv (configPrimTypes config)))
emptyContext mode demand xx
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) xx'
xx_annot <- reannotateM applyToAnnot xx_solved
t' <- applySolved ctx t
e' <- applySolved ctx $ TSum effs
return (xx_annot, t', e')
typeOfExp
:: (Show a, Ord n, Pretty n, Show n)
=> Config n
-> KindEnv n
-> TypeEnv n
-> Exp a n
-> Either (Error a n) (Type n)
typeOfExp !config !kenv !tenv !xx
= case fst $ checkExp config kenv tenv Recon DemandNone xx of
Left err -> Left err
Right (_, t, _) -> Right t
checkExpM
:: (Show a, Show n, Pretty n, Ord n)
=> Table a n
-> Context n
-> Mode n
-> Demand
-> Exp a n
-> CheckM a n
( Exp (AnTEC a n) n
, Type n
, TypeSum n
, Context n)
checkExpM !table !ctx !mode !demand !xx
= case xx of
XVar{} -> tableCheckVarCon table table ctx mode demand xx
XCon{} -> tableCheckVarCon table table ctx mode demand xx
XApp _ _ XType{} -> tableCheckAppT table table ctx mode demand xx
XApp{} -> tableCheckAppX table table ctx mode demand xx
XLAM{} -> tableCheckLamT table table ctx mode demand xx
XLam{} -> tableCheckLamX table table ctx mode demand xx
XLet _ LPrivate{} _ -> tableCheckLetPrivate table table ctx mode demand xx
XLet{} -> tableCheckLet table table ctx mode demand xx
XCase{} -> tableCheckCase table table ctx mode demand xx
XCast{} -> tableCheckCast table table ctx mode demand xx
XWitness{} -> tableCheckWitness table table ctx mode demand xx
XType a _ -> throw $ ErrorNakedType a xx
makeTable :: Config n -> KindEnv n -> TypeEnv n -> Table a n
makeTable config kenv tenv
= Table
{ tableConfig = config
, tableKindEnv = kenv
, tableTypeEnv = tenv
, tableCheckExp = checkExpM
, tableCheckVarCon = checkVarCon
, tableCheckAppT = checkAppT
, tableCheckAppX = checkAppX
, tableCheckLamT = checkLamT
, tableCheckLamX = checkLamX
, tableCheckLet = checkLet
, tableCheckLetPrivate = checkLetPrivate
, tableCheckCase = checkCase
, tableCheckCast = checkCast
, tableCheckWitness = checkWit }