module DDC.Type.Check
(
checkType
, kindOfType
, takeSortOfKiCon
, kindOfTwCon
, kindOfTcCon
, Error(..))
where
import DDC.Type.Check.CheckError
import DDC.Type.Check.CheckCon
import DDC.Type.Compounds
import DDC.Type.Predicates
import DDC.Type.Transform.LiftT
import DDC.Core.DataDef
import DDC.Type.Exp
import DDC.Base.Pretty
import Data.List
import Control.Monad
import DDC.Type.Check.Monad (throw, result)
import DDC.Type.Pretty ()
import DDC.Type.Env (Env)
import qualified DDC.Type.Sum as TS
import qualified DDC.Type.Env as Env
import qualified DDC.Type.Check.Monad as G
import qualified Data.Map as Map
type CheckM n = G.CheckM (Error n)
checkType :: (Ord n, Pretty n)
=> DataDefs n
-> Env n
-> Type n
-> Either (Error n) (Kind n)
checkType defs env tt
= result $ checkTypeM defs env tt
kindOfType :: (Ord n, Pretty n)
=> DataDefs n
-> Type n
-> Either (Error n) (Kind n)
kindOfType defs tt
= result $ checkTypeM defs Env.empty tt
checkTypeM
:: (Ord n, Pretty n)
=> DataDefs n
-> Env n
-> Type n
-> CheckM n (Kind n)
checkTypeM defs env tt
=
checkTypeM' defs env tt
checkTypeM' _defs env (TVar u)
= do let tBound = typeOfBound u
let mtEnv = Env.lookup u env
let mkResult
| Just tEnv <- mtEnv
, isBot tBound
= return tEnv
| Just tEnv <- mtEnv
, UIx i _ <- u
, tBound == liftT (i + 1) tEnv
= return tBound
| Just tEnv <- mtEnv
, tBound == tEnv
= return tBound
| Just tEnv <- mtEnv
= throw $ ErrorVarAnnotMismatch u tEnv
| _ <- mtEnv
= throw $ ErrorUndefined u
mkResult
checkTypeM' defs _env tt@(TCon tc)
= case tc of
TyConSort _ -> throw $ ErrorNakedSort tt
TyConKind kc
-> case takeSortOfKiCon kc of
Just s -> return s
Nothing -> throw $ ErrorUnappliedKindFun
TyConWitness tcw -> return $ kindOfTwCon tcw
TyConSpec tcc -> return $ kindOfTcCon tcc
TyConBound u
-> case u of
UName n _
| Just _ <- Map.lookup n (dataDefsTypes defs)
-> return $ typeOfBound u
| otherwise
-> throw $ ErrorUndefinedCtor u
UPrim{} -> return $ typeOfBound u
UIx{} -> error "sorry"
checkTypeM' defs env tt@(TForall b1 t2)
= do _ <- checkTypeM defs env (typeOfBind b1)
k2 <- checkTypeM defs (Env.extend b1 env) t2
when ( (not $ isDataKind k2)
&& (not $ isWitnessKind k2))
$ throw $ ErrorForallKindInvalid tt t2 k2
return k2
checkTypeM' defs env (TApp (TApp (TCon (TyConKind KiConFun)) k1) k2)
= do _ <- checkTypeM defs env k1
s2 <- checkTypeM defs env k2
return s2
checkTypeM' defs env tt@(TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2)
= do k1 <- checkTypeM defs env t1
k2 <- checkTypeM defs env t2
if isWitnessKind k1 && isWitnessKind k2
then return kWitness
else if isWitnessKind k1 && isDataKind k2
then return kData
else throw $ ErrorWitnessImplInvalid tt t1 k1 t2 k2
checkTypeM' defs env tt@(TApp t1 t2)
= do k1 <- checkTypeM defs env t1
k2 <- checkTypeM defs env t2
case k1 of
TApp (TApp (TCon (TyConKind KiConFun)) k11) k12
| k11 == k2 -> return k12
| otherwise -> throw $ ErrorAppArgMismatch tt k1 k2
_ -> throw $ ErrorAppNotFun tt t1 k1 t2 k2
checkTypeM' defs env (TSum ts)
= do ks <- mapM (checkTypeM defs env) $ TS.toList ts
k <- case nub ks of
[] -> return $ TS.kindOfSum ts
[k] -> return k
_ -> throw $ ErrorSumKindMismatch
(TS.kindOfSum ts) ts ks
if (k == kEffect || k == kClosure)
then return k
else throw $ ErrorSumKindInvalid ts k