module DDC.Core.Check.CheckWitness
( Config(..)
, configOfProfile
, checkWitness
, typeOfWitness
, typeOfWiCon
, typeOfWbCon
, CheckM
, checkWitnessM
, checkTypeM)
where
import DDC.Core.Exp
import DDC.Core.Pretty
import DDC.Core.Check.Error
import DDC.Core.Check.ErrorMessage ()
import DDC.Type.DataDef
import DDC.Type.Transform.SubstituteT
import DDC.Type.Compounds
import DDC.Type.Universe
import DDC.Type.Sum as Sum
import DDC.Type.Env (KindEnv, TypeEnv)
import DDC.Control.Monad.Check (throw, result)
import DDC.Base.Pretty ()
import qualified DDC.Control.Monad.Check as G
import qualified DDC.Type.Env as Env
import qualified DDC.Type.Check as T
import qualified DDC.Core.Fragment as F
type CheckM a n = G.CheckM (Error a n)
data Config n
= Config
{
configPrimDataDefs :: DataDefs n
, configPrimKinds :: KindEnv n
, configPrimTypes :: TypeEnv n
, configSuppressClosures :: Bool }
configOfProfile :: F.Profile n -> Config n
configOfProfile profile
= Config
{ configPrimDataDefs = F.profilePrimDataDefs profile
, configPrimKinds = F.profilePrimKinds profile
, configPrimTypes = F.profilePrimTypes profile
, configSuppressClosures
= F.featuresUntrackedClosures
$ F.profileFeatures profile }
checkWitness
:: (Ord n, Show n, Pretty n)
=> Config n
-> KindEnv n
-> TypeEnv n
-> Witness n
-> Either (Error a n) (Type n)
checkWitness config kenv tenv xx
= result $ checkWitnessM config kenv tenv xx
typeOfWitness
:: (Ord n, Show n, Pretty n)
=> Config n
-> Witness n
-> Either (Error a n) (Type n)
typeOfWitness config ww
= result
$ checkWitnessM config Env.empty Env.empty ww
checkWitnessM
:: (Ord n, Show n, Pretty n)
=> Config n
-> KindEnv n
-> TypeEnv n
-> Witness n
-> CheckM a n (Type n)
checkWitnessM !_config !_kenv !tenv (WVar u)
= case Env.lookup u tenv of
Nothing -> throw $ ErrorUndefinedVar u UniverseWitness
Just t -> return t
checkWitnessM !_config !_kenv !_tenv (WCon wc)
= return $ typeOfWiCon wc
checkWitnessM !config !kenv !tenv ww@(WApp w1 (WType t2))
= do t1 <- checkWitnessM config kenv tenv w1
k2 <- checkTypeM config kenv t2
case t1 of
TForall b11 t12
| typeOfBind b11 == k2
-> return $ substituteT b11 t2 t12
| otherwise -> throw $ ErrorWAppMismatch ww (typeOfBind b11) k2
_ -> throw $ ErrorWAppNotCtor ww t1 t2
checkWitnessM !config !kenv !tenv ww@(WApp w1 w2)
= do t1 <- checkWitnessM config kenv tenv w1
t2 <- checkWitnessM config kenv tenv w2
case t1 of
TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12
| t11 == t2
-> return t12
| otherwise -> throw $ ErrorWAppMismatch ww t11 t2
_ -> throw $ ErrorWAppNotCtor ww t1 t2
checkWitnessM !config !kenv !tenv ww@(WJoin w1 w2)
= do t1 <- checkWitnessM config kenv tenv w1
t2 <- checkWitnessM config kenv tenv w2
case (t1, t2) of
( TApp (TCon (TyConWitness TwConPure)) eff1
, TApp (TCon (TyConWitness TwConPure)) eff2)
-> return $ TApp (TCon (TyConWitness TwConPure))
(TSum $ Sum.fromList kEffect [eff1, eff2])
( TApp (TCon (TyConWitness TwConEmpty)) clo1
, TApp (TCon (TyConWitness TwConEmpty)) clo2)
-> return $ TApp (TCon (TyConWitness TwConEmpty))
(TSum $ Sum.fromList kClosure [clo1, clo2])
_ -> throw $ ErrorCannotJoin ww w1 t1 w2 t2
checkWitnessM !config !kenv !_tenv (WType t)
= checkTypeM config kenv t
typeOfWiCon :: WiCon n -> Type n
typeOfWiCon wc
= case wc of
WiConBuiltin wb -> typeOfWbCon wb
WiConBound _ t -> t
typeOfWbCon :: WbCon -> Type n
typeOfWbCon wb
= case wb of
WbConPure -> tPure (tBot kEffect)
WbConEmpty -> tEmpty (tBot kClosure)
WbConUse -> tForall kRegion $ \r -> tGlobal r `tImpl` (tEmpty $ tUse r)
WbConRead -> tForall kRegion $ \r -> tConst r `tImpl` (tPure $ tRead r)
WbConAlloc -> tForall kRegion $ \r -> tConst r `tImpl` (tPure $ tAlloc r)
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 (configPrimDataDefs config) kenv tt of
Left err -> throw $ ErrorType err
Right k -> return k