module DDC.Core.Check.Exp
(
Config (..)
, AnTEC (..)
, Mode (..)
, Context
, emptyContext
, checkExp
, typeOfExp
, Table (..)
, makeTable
, CheckM
, checkExpM
, CheckTrace (..)
, TaggedClosure(..))
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 Data.Monoid hiding ((<>))
import qualified DDC.Type.Env as Env
checkExp
:: (Ord n, Show n, Pretty n)
=> Config n
-> KindEnv n
-> TypeEnv n
-> Exp a n
-> Mode n
-> ( Either (Error a n)
( Exp (AnTEC a n) n
, Type n
, Effect n
, Closure n)
, CheckTrace)
checkExp !config !kenv !tenv !xx !mode
= (result, ct)
where
((ct, _, _), result)
= runCheck (mempty, 0, 0)
$ do
(xx', t, effs, clos, ctx)
<- checkExpM
(makeTable config
(Env.union kenv (configPrimKinds config))
(Env.union tenv (configPrimTypes config)))
emptyContext xx mode
let applyToAnnot (AnTEC t0 e0 c0 x0)
= AnTEC (applySolved ctx t0)
(applySolved ctx e0)
(applySolved ctx c0)
x0
let xx'' = reannotate applyToAnnot
$ mapT (applySolved ctx) xx'
let t' = applySolved ctx t
let e' = applySolved ctx $ TSum effs
let c' = applySolved ctx $ closureOfTaggedSet clos
return (xx'', t', e', c')
typeOfExp
:: (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 xx Recon of
Left err -> Left err
Right (_, t, _, _) -> Right t
checkExpM
:: (Show n, Pretty n, Ord n)
=> Table a n
-> Context n
-> Exp a n
-> Mode n
-> CheckM a n
( Exp (AnTEC a n) n
, Type n
, TypeSum n
, Set (TaggedClosure n)
, Context n)
checkExpM !table !ctx !xx !mode
= case xx of
XVar{} -> tableCheckVarCon table table ctx xx mode
XCon{} -> tableCheckVarCon table table ctx xx mode
XApp _ _ XType{} -> tableCheckAppT table table ctx xx mode
XApp{} -> tableCheckAppX table table ctx xx mode
XLAM{} -> tableCheckLamT table table ctx xx mode
XLam{} -> tableCheckLamX table table ctx xx mode
XLet _ LPrivate{} _ -> tableCheckLetPrivate table table ctx xx mode
XLet _ LWithRegion{} _ -> tableCheckLetPrivate table table ctx xx mode
XLet{} -> tableCheckLet table table ctx xx mode
XCase{} -> tableCheckCase table table ctx xx mode
XCast{} -> tableCheckCast table table ctx xx mode
XWitness{} -> tableCheckWitness table table ctx xx mode
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 }