module DDC.Core.Check.Witness
( checkWitness
, checkWitnessM
, typeOfWitness
, typeOfWiCon)
where
import DDC.Core.Exp.Annot.AnT
import DDC.Core.Check.Error
import DDC.Core.Check.ErrorMessage ()
import DDC.Core.Check.Base
import DDC.Type.Transform.SubstituteT
import qualified DDC.Type.Env as Env
checkWitness
:: (Ord n, Show n, Pretty n)
=> Config n
-> KindEnv n
-> TypeEnv n
-> Witness a n
-> Either (Error a n)
( Witness (AnT a n) n
, Type n)
checkWitness config kenv tenv xx
= evalCheck (mempty, 0, 0)
$ checkWitnessM config kenv tenv emptyContext xx
typeOfWitness
:: (Ord n, Show n, Pretty n)
=> Config n
-> Witness a n
-> Either (Error a n) (Type n)
typeOfWitness config ww
= case checkWitness config Env.empty Env.empty ww of
Left err -> Left err
Right (_, t) -> Right t
checkWitnessM
:: (Ord n, Show n, Pretty n)
=> Config n
-> KindEnv n
-> TypeEnv n
-> Context n
-> Witness a n
-> CheckM a n
( Witness (AnT a n) n
, Type n)
checkWitnessM !_config !_kenv !tenv !ctx (WVar a u)
| Just t <- lookupType u ctx
= return ( WVar (AnT t a) u, t)
| Just t <- Env.lookup u tenv
= return ( WVar (AnT t a) u, t)
| otherwise
= throw $ ErrorUndefinedVar a u UniverseWitness
checkWitnessM !_config !_kenv !_tenv !_ctx (WCon a wc)
= let t' = typeOfWiCon wc
in return ( WCon (AnT t' a) wc
, t')
checkWitnessM !config !kenv !tenv !ctx ww@(WApp a1 w1 (WType a2 t2))
= do (w1', t1) <- checkWitnessM config kenv tenv ctx w1
(t2', k2, _) <- checkTypeM config kenv ctx UniverseSpec t2 Recon
case t1 of
TForall b11 t12
| typeOfBind b11 == k2
-> let t' = substituteT b11 t2' t12
in return ( WApp (AnT t' a1) w1' (WType (AnT k2 a2) t2')
, t')
| otherwise -> throw $ ErrorWAppMismatch a1 ww (typeOfBind b11) k2
_ -> throw $ ErrorWAppNotCtor a1 ww t1 t2'
checkWitnessM !config !kenv !tenv !ctx ww@(WApp a w1 w2)
= do (w1', t1) <- checkWitnessM config kenv tenv ctx w1
(w2', t2) <- checkWitnessM config kenv tenv ctx w2
case t1 of
TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12
| t11 == t2
-> return ( WApp (AnT t12 a) w1' w2'
, t12)
| otherwise -> throw $ ErrorWAppMismatch a ww t11 t2
_ -> throw $ ErrorWAppNotCtor a ww t1 t2
checkWitnessM !config !kenv !_tenv !ctx (WType a t)
= do (t', k, _) <- checkTypeM config kenv ctx UniverseSpec t Recon
return ( WType (AnT k a) t'
, k)
typeOfWiCon :: WiCon n -> Type n
typeOfWiCon wc
= case wc of
WiConBound _ t -> t