module DDC.Core.Check.CheckWitness
( checkWitness
, typeOfWitness
, typeOfWiCon
, typeOfWbCon
, CheckM
, checkWitnessM)
where
import DDC.Core.DataDef
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)
=> DataDefs n
-> Env n
-> Env n
-> Witness n
-> Either (Error a n) (Type n)
checkWitness defs kenv tenv xx
= result $ checkWitnessM defs kenv tenv xx
typeOfWitness
:: (Ord n, Pretty n)
=> DataDefs n
-> Witness n
-> Either (Error a n) (Type n)
typeOfWitness defs ww
= result
$ checkWitnessM defs Env.empty Env.empty ww
checkWitnessM
:: (Ord n, Pretty n)
=> DataDefs n
-> Env n
-> Env n
-> Witness n
-> CheckM a n (Type n)
checkWitnessM _defs _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 _defs _kenv _tenv (WCon wc)
= return $ typeOfWiCon wc
checkWitnessM defs kenv tenv ww@(WApp w1 (WType t2))
= do t1 <- checkWitnessM defs kenv tenv w1
k2 <- checkTypeM defs 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 defs kenv tenv ww@(WApp w1 w2)
= do t1 <- checkWitnessM defs kenv tenv w1
t2 <- checkWitnessM defs 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 defs kenv tenv ww@(WJoin w1 w2)
= do t1 <- checkWitnessM defs kenv tenv w1
t2 <- checkWitnessM defs 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 defs kenv _tenv (WType t)
= checkTypeM defs 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)
=> DataDefs n
-> Env n
-> Type n
-> CheckM a n (Kind n)
checkTypeM defs kenv tt
= case T.checkType defs kenv tt of
Left err -> throw $ ErrorType err
Right k -> return k