module DDC.Core.Check.Judge.Type.Base
( Checker
, Demand (..)
, Table (..)
, returnX
, runForDemand
, module DDC.Core.Check.Base
, module DDC.Core.Check.Judge.Inst
, module DDC.Core.Check.Judge.Sub
, module DDC.Core.Check.Judge.Eq
, module DDC.Core.Check.Witness
, module DDC.Core.Check.Error
, module DDC.Core.Transform.Reannotate
, module DDC.Core.Transform.SubstituteTX
, module DDC.Core.Exp.Annot.AnTEC
, module DDC.Type.Transform.SubstituteT
, module DDC.Type.Transform.Instantiate
, module DDC.Type.Transform.BoundT)
where
import DDC.Core.Check.Base
import DDC.Core.Check.Judge.Inst
import DDC.Core.Check.Judge.Sub
import DDC.Core.Check.Judge.Eq
import DDC.Core.Check.Witness
import DDC.Core.Check.Error
import DDC.Core.Transform.Reannotate
import DDC.Core.Transform.SubstituteTX
import DDC.Core.Exp.Annot.AnTEC
import DDC.Type.Transform.SubstituteT
import DDC.Type.Transform.Instantiate
import DDC.Type.Transform.BoundT
data Demand
= DemandRun
| DemandNone
deriving Show
type Checker a n
= (Show a, Show n, Ord n, Pretty 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)
data Table a n
= Table
{ tableConfig :: Config n
, tableKindEnv :: KindEnv n
, tableTypeEnv :: TypeEnv n
, tableCheckExp :: Checker a n
, tableCheckVarCon :: Checker a n
, tableCheckAppT :: Checker a n
, tableCheckAppX :: Checker a n
, tableCheckLamT :: Checker a n
, tableCheckLamX :: Checker a n
, tableCheckLet :: Checker a n
, tableCheckLetPrivate :: Checker a n
, tableCheckCase :: Checker a n
, tableCheckCast :: Checker a n
, tableCheckWitness :: Checker a n }
returnX :: Ord n
=> a
-> (AnTEC a n
-> Exp (AnTEC a n) n)
-> Type n
-> TypeSum n
-> Context n
-> CheckM a n
( Exp (AnTEC a n) n
, Type n
, TypeSum n
, Context n)
returnX !a !f !t !es !ctx
= let e = TSum es
in return (f (AnTEC t e (tBot kClosure) a)
, t, es, ctx)
runForDemand
:: Ord n
=> Config n
-> a
-> Demand
-> Exp (AnTEC a n) n
-> Type n
-> Effect n
-> CheckM a n
( Exp (AnTEC a n) n
, Type n
, Effect n)
runForDemand _config _a DemandNone xExp tExp eExp
= return (xExp, tExp, eExp)
runForDemand config a DemandRun xExp tExp eExp
| isXCastBox xExp || isXCastRun xExp
= return (xExp, tExp, eExp)
| configImplicitRun config
, Just (eResult, tResult) <- takeTSusp tExp
= let
eTotal = tSum kEffect [eExp, eResult]
aCast = AnTEC tResult eTotal (tBot kClosure) a
in return ( XCast aCast CastRun xExp
, tResult
, eTotal)
| otherwise
= return (xExp, tExp, eExp)