module DDC.Core.Check.CheckExp
( checkExp
, typeOfExp
, CheckM
, checkExpM
, TaggedClosure(..))
where
import DDC.Core.DataDef
import DDC.Core.Predicates
import DDC.Core.Compounds
import DDC.Core.Exp
import DDC.Core.Pretty
import DDC.Core.Collect
import DDC.Core.Check.Error
import DDC.Core.Check.CheckWitness
import DDC.Core.Check.TaggedClosure
import DDC.Type.Transform.SubstituteT
import DDC.Type.Transform.Crush
import DDC.Type.Transform.Trim
import DDC.Type.Transform.Instantiate
import DDC.Type.Transform.LiftT
import DDC.Type.Equiv
import DDC.Type.Universe
import DDC.Type.Compounds
import DDC.Type.Predicates
import DDC.Type.Sum as Sum
import DDC.Type.Env (Env)
import DDC.Type.Check.Monad (result, throw)
import DDC.Base.Pretty ()
import Data.Set (Set)
import qualified DDC.Type.Env as Env
import qualified DDC.Type.Check as T
import qualified Data.Set as Set
import Control.Monad
import Data.List as L
import Data.Maybe
checkExp
:: (Ord n, Pretty n)
=> DataDefs n
-> Env n
-> Env n
-> Exp a n
-> Either (Error a n)
( Exp a n
, Type n
, Effect n
, Closure n)
checkExp defs kenv tenv xx
= result
$ do (xx', t, effs, clos) <- checkExpM defs kenv tenv xx
return ( xx'
, t
, TSum effs
, closureOfTaggedSet clos)
typeOfExp
:: (Ord n, Pretty n)
=> DataDefs n
-> Exp a n
-> Either (Error a n) (Type n)
typeOfExp defs xx
= case checkExp defs Env.empty Env.empty xx of
Left err -> Left err
Right (_, t, _, _) -> Right t
checkExpM
:: (Ord n, Pretty n)
=> DataDefs n
-> Env n
-> Env n
-> Exp a n
-> CheckM a n
( Exp a n
, Type n
, TypeSum n
, Set (TaggedClosure n))
checkExpM defs kenv tenv xx
= checkExpM' defs kenv tenv xx
checkExpM' _defs _kenv tenv (XVar a 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 ( XVar a u
, tResult
, Sum.empty kEffect
, Set.singleton
$ taggedClosureOfValBound
$ replaceTypeOfBound tResult u)
checkExpM' _defs _kenv _tenv (XCon a u)
= return ( XCon a u
, typeOfBound u
, Sum.empty kEffect
, Set.empty)
checkExpM' defs kenv tenv xx@(XApp a x1 (XType t2))
= do (x1', t1, effs1, clos1) <- checkExpM defs kenv tenv x1
k2 <- checkTypeM kenv t2
case t1 of
TForall b11 t12
| typeOfBind b11 == k2
-> return ( XApp a x1' (XType t2)
, substituteT b11 t2 t12
, substituteT b11 t2 effs1
, clos1 `Set.union` taggedClosureOfTyArg t2)
| otherwise -> throw $ ErrorAppMismatch xx (typeOfBind b11) t2
_ -> throw $ ErrorAppNotFun xx t1 t2
checkExpM' defs kenv tenv xx@(XApp a x1 (XWitness w2))
= do (x1', t1, effs1, clos1) <- checkExpM defs kenv tenv x1
t2 <- checkWitnessM kenv tenv w2
case t1 of
TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12
| t11 `equivT` t2
-> return ( XApp a x1' (XWitness w2)
, t12
, effs1
, clos1)
| otherwise -> throw $ ErrorAppMismatch xx t11 t2
_ -> throw $ ErrorAppNotFun xx t1 t2
checkExpM' defs kenv tenv xx@(XApp a x1 x2)
= do (x1', t1, effs1, clos1) <- checkExpM defs kenv tenv x1
(x2', t2, effs2, clos2) <- checkExpM defs kenv tenv x2
case t1 of
TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t11) eff) _clo) t12
| t11 `equivT` t2
, effs <- Sum.fromList kEffect [eff]
-> return ( XApp a x1' x2'
, t12
, effs1 `Sum.union` effs2 `Sum.union` effs
, clos1 `Set.union` clos2)
| otherwise -> throw $ ErrorAppMismatch xx t11 t2
_ -> throw $ ErrorAppNotFun xx t1 t2
checkExpM' defs kenv tenv xx@(XLAM a b1 x2)
= do let t1 = typeOfBind b1
_ <- checkTypeM kenv t1
let kenv' = Env.extend b1 kenv
(x2', t2, e2, c2) <- checkExpM defs kenv' tenv x2
k2 <- checkTypeM kenv' t2
when (Env.memberBind b1 kenv)
$ throw $ ErrorLamShadow xx b1
when (e2 /= Sum.empty kEffect)
$ throw $ ErrorLamNotPure xx (TSum e2)
when (not $ isDataKind k2)
$ throw $ ErrorLamBodyNotData xx b1 t2 k2
let c2_cut = Set.fromList
$ mapMaybe (cutTaggedClosureT b1)
$ Set.toList c2
return ( XLAM a b1 x2'
, TForall b1 t2
, Sum.empty kEffect
, c2_cut)
checkExpM' defs kenv tenv xx@(XLam a b1 x2)
= do let t1 = typeOfBind b1
k1 <- checkTypeM kenv t1
let tenv' = Env.extend b1 tenv
(x2', t2, e2, c2) <- checkExpM defs kenv tenv' x2
k2 <- checkTypeM kenv t2
case universeFromType2 k1 of
Just UniverseData
| not $ isDataKind k1 -> throw $ ErrorLamBindNotData xx t1 k1
| not $ isDataKind k2 -> throw $ ErrorLamBodyNotData xx b1 t2 k2
| otherwise
-> let
c2_cut = Set.fromList
$ mapMaybe (cutTaggedClosureX b1)
$ Set.toList c2
Just c2_captured
= trimClosure $ closureOfTaggedSet c2_cut
in return ( XLam a b1 x2'
, tFun t1 (TSum e2) c2_captured t2
, Sum.empty kEffect
, c2_cut)
Just UniverseWitness
| e2 /= Sum.empty kEffect -> throw $ ErrorLamNotPure xx (TSum e2)
| not $ isDataKind k2 -> throw $ ErrorLamBodyNotData xx b1 t2 k2
| otherwise
-> return ( XLam a b1 x2'
, tImpl t1 t2
, Sum.empty kEffect
, c2)
_ -> throw $ ErrorMalformedType xx k1
checkExpM' defs kenv tenv xx@(XLet a (LLet mode b11 x12) x2)
= do
(x12', t12, effs12, clo12)
<- checkExpM defs kenv tenv x12
(b11', k11')
<- checkLetBindOfTypeM xx kenv tenv t12 b11
when (not $ isDataKind k11')
$ throw $ ErrorLetBindingNotData xx b11' k11'
let tenv1 = Env.extend b11' tenv
(x2', t2, effs2, c2) <- checkExpM defs kenv tenv1 x2
k2 <- checkTypeM kenv t2
when (not $ isDataKind k2)
$ throw $ ErrorLetBodyNotData xx t2 k2
let c2_cut = Set.fromList
$ mapMaybe (cutTaggedClosureX b11')
$ Set.toList c2
(case mode of
LetStrict -> return ()
LetLazy _
-> do let eff12' = TSum effs12
when (not $ isBot eff12')
$ throw $ ErrorLetLazyNotPure xx b11 eff12'
let clo12' = closureOfTaggedSet clo12
when (not $ isBot clo12')
$ throw $ ErrorLetLazyNotEmpty xx b11 clo12')
(case mode of
LetStrict -> return ()
LetLazy Nothing
-> do case takeDataTyConApps t12 of
Just (_tc, t1 : _)
-> do k1 <- checkTypeM kenv t1
when (isRegionKind k1)
$ throw $ ErrorLetLazyNoWitness xx b11 t12
_ -> return ()
LetLazy (Just wit)
-> do tWit <- checkWitnessM kenv tenv wit
let tWitExp = case takeDataTyConApps t12 of
Just (_tc, tR : _ts) -> tLazy tR
_ -> tHeadLazy t12
when (not $ equivT tWit tWitExp)
$ throw $ ErrorLetLazyWitnessTypeMismatch
xx b11 tWit t12 tWitExp)
return ( XLet a (LLet mode b11' x12') x2'
, t2
, effs12 `Sum.union` effs2
, clo12 `Set.union` c2_cut)
checkExpM' defs kenv tenv xx@(XLet a (LRec bxs) xBody)
= do
let (bs, xs) = unzip bxs
ks <- mapM (checkTypeM kenv) $ map typeOfBind bs
zipWithM_ (\b k
-> when (not $ isDataKind k)
$ throw $ ErrorLetBindingNotData xx b k)
bs ks
forM_ xs $ \x
-> when (not $ (isXLam x || isXLAM x))
$ throw $ ErrorLetrecBindingNotLambda xx x
let tenv' = Env.extends bs tenv
(xsRight', tsRight, _effssBinds, clossBinds)
<- liftM unzip4 $ mapM (checkExpM defs kenv tenv') xs
zipWithM_ (\b t
-> if not $ equivT (typeOfBind b) t
then throw $ ErrorLetMismatch xx b t
else return ())
bs tsRight
(xBody', tBody, effsBody, closBody)
<- checkExpM defs kenv tenv' xBody
kBody <- checkTypeM kenv tBody
when (not $ isDataKind kBody)
$ throw $ ErrorLetBodyNotData xx tBody kBody
let clos_cut
= Set.fromList
$ mapMaybe (cutTaggedClosureXs bs)
$ Set.toList
$ Set.unions (closBody : clossBinds)
return ( XLet a (LRec (zip bs xsRight')) xBody'
, tBody
, effsBody
, clos_cut)
checkExpM' defs kenv tenv xx@(XLet a (LLetRegion b bs) x)
= case takeSubstBoundOfBind b of
Nothing -> checkExpM defs kenv tenv x
Just u
-> do
let k = typeOfBind b
checkTypeM kenv k
when (not $ isRegionKind k)
$ throw $ ErrorLetRegionNotRegion xx b k
when (Env.memberBind b kenv)
$ throw $ ErrorLetRegionRebound xx b
let kenv' = Env.extend b kenv
mapM_ (checkTypeM kenv') $ map typeOfBind bs
checkWitnessBindsM xx u bs
let tenv' = Env.extends bs tenv
(xBody', tBody, effs, clo) <- checkExpM defs kenv' tenv' x
kBody <- checkTypeM kenv' tBody
when (not $ isDataKind kBody)
$ throw $ ErrorLetBodyNotData xx tBody kBody
let fvsT = freeT Env.empty tBody
when (Set.member u fvsT)
$ throw $ ErrorLetRegionFree xx b tBody
let effs' = Sum.delete (tRead (TVar u))
$ Sum.delete (tWrite (TVar u))
$ Sum.delete (tAlloc (TVar u))
$ effs
let clo_masked = Set.delete (GBoundRgnVar u)
$ clo
return ( XLet a (LLetRegion b bs) xBody'
, tBody
, effs'
, clo_masked)
checkExpM' defs kenv tenv xx@(XLet a (LWithRegion u) x)
= do
let k = typeOfBound u
checkTypeM kenv k
when (not $ isRegionKind k)
$ throw $ ErrorWithRegionNotRegion xx u k
(xBody', tBody, effs, clo)
<- checkExpM defs kenv tenv x
kBody <- checkTypeM kenv tBody
when (not $ isDataKind kBody)
$ throw $ ErrorLetBodyNotData xx tBody kBody
let tu = TCon $ TyConBound u
let effs' = Sum.delete (tRead tu)
$ Sum.delete (tWrite tu)
$ Sum.delete (tAlloc tu)
$ effs
let clo_masked = Set.delete (GBoundRgnCon u) clo
return ( XLet a (LWithRegion u) xBody'
, tBody
, effs'
, clo_masked)
checkExpM' defs kenv tenv xx@(XCase a xDiscrim alts)
= do
(xDiscrim', tDiscrim, effsDiscrim, closDiscrim)
<- checkExpM defs kenv tenv xDiscrim
(nTyCon, tsArgs)
<- case takeTyConApps tDiscrim of
Just (tc, ts)
| TyConBound (UName n t) <- tc
, takeResultKind t == kData
-> return (n, ts)
| TyConBound (UPrim n t) <- tc
, takeResultKind t == kData
-> return (n, ts)
_ -> throw $ ErrorCaseDiscrimNotAlgebraic xx tDiscrim
mode
<- case lookupModeOfDataType nTyCon defs of
Nothing -> throw $ ErrorCaseDiscrimTypeUndeclared xx tDiscrim
Just m -> return m
(alts', ts, effss, closs)
<- liftM unzip4
$ mapM (checkAltM xx defs kenv tenv tDiscrim tsArgs) alts
when (null ts)
$ throw $ ErrorCaseNoAlternatives xx
let (tAlt : _) = ts
forM_ ts $ \tAlt'
-> when (not $ equivT tAlt tAlt')
$ throw $ ErrorCaseAltResultMismatch xx tAlt tAlt'
let pats = [p | AAlt p _ <- alts]
let psDefaults = filter isPDefault pats
let nsCtorsMatched = mapMaybe takeCtorNameOfAlt alts
when (length psDefaults > 1)
$ throw $ ErrorCaseOverlapping xx
when (length (nub nsCtorsMatched) /= length nsCtorsMatched )
$ throw $ ErrorCaseOverlapping xx
(case pats of
[] -> throw $ ErrorCaseNoAlternatives xx
_ | or $ map isPDefault $ init pats
-> throw $ ErrorCaseOverlapping xx
| otherwise
-> return ())
(case mode of
DataModeSmall nsCtors
| any isPDefault [p | AAlt p _ <- alts]
-> return ()
| nsCtorsMissing <- nsCtors \\ nsCtorsMatched
, not $ null nsCtorsMissing
-> throw $ ErrorCaseNonExhaustive xx nsCtorsMissing
| otherwise
-> return ()
DataModeLarge
| any isPDefault [p | AAlt p _ <- alts] -> return ()
| otherwise
-> throw $ ErrorCaseNonExhaustiveLarge xx)
let effsMatch
= Sum.singleton kEffect
$ crushEffect $ tHeadRead tDiscrim
return ( XCase a xDiscrim' alts'
, tAlt
, Sum.unions kEffect (effsDiscrim : effsMatch : effss)
, Set.unions (closDiscrim : closs) )
checkExpM' defs kenv tenv xx@(XCast a c@(CastWeakenEffect eff) x1)
= do
kEff <- checkTypeM kenv eff
when (not $ isEffectKind kEff)
$ throw $ ErrorMaxeffNotEff xx eff kEff
(x1', t1, effs, clo) <- checkExpM defs kenv tenv x1
return ( XCast a c x1'
, t1
, Sum.insert eff effs
, clo)
checkExpM' defs kenv tenv xx@(XCast a c@(CastWeakenClosure clo2) x1)
= do
kClo <- checkTypeM kenv clo2
when (not $ isClosureKind kClo)
$ throw $ ErrorMaxcloNotClo xx clo2 kClo
clos2
<- case taggedClosureOfWeakClo clo2 of
Nothing -> throw $ ErrorMaxcloMalformed xx clo2
Just clos2' -> return clos2'
(x1', t1, effs, clos) <- checkExpM defs kenv tenv x1
return ( XCast a c x1'
, t1
, effs
, Set.union clos clos2)
checkExpM' defs kenv tenv xx@(XCast a c@(CastPurify w) x1)
= do tW <- checkWitnessM kenv tenv w
(x1', t1, effs, clo) <- checkExpM defs kenv tenv x1
effs' <- case tW of
TApp (TCon (TyConWitness TwConPure)) effMask
-> return $ Sum.delete effMask effs
_ -> throw $ ErrorWitnessNotPurity xx w tW
return ( XCast a c x1'
, t1
, effs'
, clo)
checkExpM' defs kenv tenv xx@(XCast a c@(CastForget w) x1)
= do tW <- checkWitnessM kenv tenv w
(x1', t1, effs, clos) <- checkExpM defs kenv tenv x1
clos' <- case tW of
TApp (TCon (TyConWitness TwConEmpty)) cloMask
-> return $ maskFromTaggedSet
(Sum.singleton kClosure cloMask)
clos
_ -> throw $ ErrorWitnessNotEmpty xx w tW
return ( XCast a c x1'
, t1
, effs
, clos')
checkExpM' _defs _kenv _tenv xx@(XType _)
= throw $ ErrorNakedType xx
checkExpM' _defs _kenv _tenv xx@(XWitness _)
= throw $ ErrorNakedWitness xx
checkAltM
:: (Pretty n, Ord n)
=> Exp a n
-> DataDefs n
-> Env n
-> Env n
-> Type n
-> [Type n]
-> Alt a n
-> CheckM a n
( Alt a n
, Type n
, TypeSum n
, Set (TaggedClosure n))
checkAltM _xx defs kenv tenv _tDiscrim _tsArgs (AAlt PDefault xBody)
= do (xBody', tBody, effBody, cloBody)
<- checkExpM defs kenv tenv xBody
return ( AAlt PDefault xBody'
, tBody
, effBody
, cloBody)
checkAltM xx defs kenv tenv tDiscrim tsArgs (AAlt (PData uCon bsArg) xBody)
= do
let tCtor = typeOfBound uCon
tCtor_inst
<- case instantiateTs tCtor tsArgs of
Nothing -> throw $ ErrorCaseCannotInstantiate xx tDiscrim tCtor
Just t -> return t
let (tsFields_ctor, tResult)
= takeTFunArgResult tCtor_inst
when (not $ equivT tDiscrim tResult)
$ throw $ ErrorCaseDiscrimTypeMismatch xx tDiscrim tResult
when (length tsFields_ctor < length bsArg)
$ throw $ ErrorCaseTooManyBinders xx uCon
(length tsFields_ctor)
(length bsArg)
tsFields <- zipWithM (mergeAnnot xx)
(map typeOfBind bsArg)
tsFields_ctor
let bsArg' = zipWith replaceTypeOfBind tsFields bsArg
let tenv' = Env.extends bsArg' tenv
(xBody', tBody, effsBody, closBody)
<- checkExpM defs kenv tenv' xBody
let closBody_cut
= Set.fromList
$ mapMaybe (cutTaggedClosureXs bsArg')
$ Set.toList closBody
return ( AAlt (PData uCon bsArg') xBody'
, tBody
, effsBody
, closBody_cut)
mergeAnnot :: Eq n => Exp a n -> Type n -> Type n -> CheckM a n (Type n)
mergeAnnot xx tAnnot tActual
| isBot tAnnot = return tActual
| tAnnot == tActual = return tActual
| otherwise
= throw $ ErrorCaseFieldTypeMismatch xx tAnnot tActual
checkWitnessBindsM :: Ord n => Exp a n -> Bound n -> [Bind n] -> CheckM a n ()
checkWitnessBindsM xx nRegion bsWits
= mapM_ (checkWitnessBindM xx nRegion bsWits) bsWits
checkWitnessBindM
:: Ord n
=> Exp a n
-> Bound n
-> [Bind n]
-> Bind n
-> CheckM a n ()
checkWitnessBindM xx uRegion bsWit bWit
= let btsWit
= [(typeOfBind b, b) | b <- bsWit]
checkWitnessArg t
= case t of
TVar u'
| uRegion /= u' -> throw $ ErrorLetRegionWitnessOther xx uRegion bWit
| otherwise -> return ()
TCon (TyConBound u')
| uRegion /= u' -> throw $ ErrorLetRegionWitnessOther xx uRegion bWit
| otherwise -> return ()
_ -> throw $ ErrorLetRegionWitnessInvalid xx bWit
in case typeOfBind bWit of
TApp (TCon (TyConWitness TwConGlobal)) t2
-> checkWitnessArg t2
TApp (TCon (TyConWitness TwConConst)) t2
| Just bConflict <- L.lookup (tMutable t2) btsWit
-> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict
| otherwise -> checkWitnessArg t2
TApp (TCon (TyConWitness TwConMutable)) t2
| Just bConflict <- L.lookup (tConst t2) btsWit
-> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict
| otherwise -> checkWitnessArg t2
TApp (TCon (TyConWitness TwConLazy)) t2
| Just bConflict <- L.lookup (tManifest t2) btsWit
-> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict
| otherwise -> checkWitnessArg t2
TApp (TCon (TyConWitness TwConManifest)) t2
| Just bConflict <- L.lookup (tLazy t2) btsWit
-> throw $ ErrorLetRegionWitnessConflict xx bWit bConflict
| otherwise -> checkWitnessArg t2
_ -> throw $ ErrorLetRegionWitnessInvalid xx bWit
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
checkLetBindOfTypeM
:: (Eq n, Ord n, Pretty n)
=> Exp a n
-> Env n
-> Env n
-> Type n
-> Bind n
-> CheckM a n (Bind n, Kind n)
checkLetBindOfTypeM xx kenv _tenv tRight b
| isBot (typeOfBind b)
= do k <- checkTypeM kenv tRight
return ( replaceTypeOfBind tRight b
, k)
| not $ equivT (typeOfBind b) tRight
= throw $ ErrorLetMismatch xx b tRight
| otherwise
= do k <- checkTypeM kenv (typeOfBind b)
return (b, k)