module DDC.Core.Check.CheckWitness
( checkWitness
, typeOfWitness
, typeOfWiCon
, typeOfWbCon
, CheckM
, checkWitnessM)
where
import DDC.Core.Exp
import DDC.Core.Pretty
import DDC.Core.Check.Error
import DDC.Core.Check.ErrorMessage ()
import DDC.Type.Transform.SubstituteT
import DDC.Type.Compounds
import DDC.Type.Predicates
import DDC.Type.Equiv
import DDC.Type.Transform.LiftT
import DDC.Type.Sum as Sum
import DDC.Type.Env (Env)
import DDC.Type.Check.Monad (result, throw)
import DDC.Base.Pretty ()
import qualified DDC.Type.Env as Env
import qualified DDC.Type.Check as T
import qualified DDC.Type.Check.Monad as G
type CheckM a n = G.CheckM (Error a n)
checkWitness
:: (Ord n, Pretty n)
=> Env n
-> Env n
-> Witness n
-> Either (Error a n) (Type n)
checkWitness kenv tenv xx
= result $ checkWitnessM kenv tenv xx
typeOfWitness
:: (Ord n, Pretty n)
=> Witness n
-> Either (Error a n) (Type n)
typeOfWitness ww
= result
$ checkWitnessM Env.empty Env.empty ww
checkWitnessM
:: (Ord n, Pretty n)
=> Env n
-> Env n
-> Witness n
-> CheckM a n (Type n)
checkWitnessM _kenv tenv (WVar u)
= do let tBound = typeOfBound u
let mtEnv = Env.lookup u tenv
let mkResult
| Just tEnv <- mtEnv
, isBot tBound
= return tEnv
| Just tEnv <- mtEnv
, UIx i _ <- u
, equivT tBound (liftT (i + 1) tEnv)
= return tBound
| Just tEnv <- mtEnv
, equivT tBound tEnv
= return tEnv
| Just tEnv <- mtEnv
= throw $ ErrorVarAnnotMismatch u tEnv
| otherwise
= return tBound
tResult <- mkResult
return tResult
checkWitnessM _kenv _tenv (WCon wc)
= return $ typeOfWiCon wc
checkWitnessM kenv tenv ww@(WApp w1 (WType t2))
= do t1 <- checkWitnessM kenv tenv w1
k2 <- checkTypeM 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 kenv tenv ww@(WApp w1 w2)
= do t1 <- checkWitnessM kenv tenv w1
t2 <- checkWitnessM 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 kenv tenv ww@(WJoin w1 w2)
= do t1 <- checkWitnessM kenv tenv w1
t2 <- checkWitnessM 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 kenv _tenv (WType t)
= checkTypeM kenv t
typeOfWiCon :: WiCon n -> Type n
typeOfWiCon wc
= case wc of
WiConBuiltin wb -> typeOfWbCon wb
WiConBound u -> typeOfBound u
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, Pretty n) => Env n -> Type n -> CheckM a n (Kind n)
checkTypeM kenv tt
= case T.checkType kenv tt of
Left err -> throw $ ErrorType err
Right k -> return k