module DDC.Core.Eval.Check
( checkCapsX
, Error(..))
where
import DDC.Core.Eval.Compounds
import DDC.Core.Eval.Name
import DDC.Core.Exp
import DDC.Base.Pretty
import Control.Monad
import Data.Maybe
import DDC.Type.Check.Monad (throw, result)
import Data.Set (Set)
import qualified DDC.Type.Check.Monad as G
import qualified Data.Set as Set
type CheckM a = G.CheckM Error
checkCapsX :: Exp a Name -> Maybe Error
checkCapsX xx
= case result $ checkCapsXM xx of
Left err -> Just err
Right ws
-> let caps = foldr mustInsertCap emptyCapSet ws
in checkCapSet caps
data CapSet
= CapSet
{ capsGlobal :: Set Rgn
, capsConst :: Set Rgn
, capsMutable :: Set Rgn
, capsLazy :: Set Rgn
, capsManifest :: Set Rgn }
deriving Show
emptyCapSet :: CapSet
emptyCapSet
= CapSet
{ capsGlobal = Set.empty
, capsConst = Set.empty
, capsMutable = Set.empty
, capsLazy = Set.empty
, capsManifest = Set.empty }
mustInsertCap :: Witness Name -> CapSet -> CapSet
mustInsertCap ww caps
| WApp (WCon (WiConBound (UPrim nc _)))
(WType (TCon (TyConBound (UPrim nh _)))) <- ww
, NameCap c <- nc
, NameRgn r <- nh
= case c of
CapGlobal -> caps { capsGlobal = Set.insert r (capsGlobal caps) }
CapConst -> caps { capsConst = Set.insert r (capsConst caps) }
CapMutable -> caps { capsMutable = Set.insert r (capsMutable caps) }
CapLazy -> caps { capsLazy = Set.insert r (capsLazy caps) }
CapManifest -> caps { capsManifest = Set.insert r (capsManifest caps)}
| otherwise
= error "mustInsertCap: not a capability"
checkCapSet :: CapSet -> Maybe Error
checkCapSet cs
| r : _ <- Set.toList
$ Set.intersection (capsConst cs) (capsMutable cs)
= Just $ ErrorConflict r CapConst CapMutable
| r : _ <- Set.toList
$ Set.intersection (capsLazy cs) (capsManifest cs)
= Just $ ErrorConflict r CapLazy CapManifest
| otherwise
= Nothing
data Error
= ErrorConflict
{ errorRegions :: Rgn
, errorCap1 :: Cap
, errorCap2 :: Cap }
| ErrorPartial
{ errorWitness :: Witness Name }
| ErrorNonHandle
{ errorWitness :: Witness Name }
instance Pretty Error where
ppr err
= case err of
ErrorConflict r c1 c2
-> vcat [ text "Conflicting capabilities in core program."
, text " region: " <> ppr r
, text " can't be both: " <> ppr c1
, text " and: " <> ppr c2 ]
ErrorPartial w1
-> vcat [ text "Partially applied capability constructor."
, text "with: " <> ppr w1]
ErrorNonHandle w1
-> vcat [ text "Capability constructor applied to a non-region handle."
, text "with: " <> ppr w1]
checkCapsXM :: Exp a Name -> CheckM a [Witness Name]
checkCapsXM xx
= let none = return []
in case xx of
XVar{} -> none
XCon{} -> none
XLAM _ _ x -> checkCapsXM x
XLam _ _ x -> checkCapsXM x
XApp _ x1 x2 -> liftM2 (++) (checkCapsXM x1) (checkCapsXM x2)
XLet _ lts x1 -> liftM2 (++) (checkCapsLM lts) (checkCapsXM x1)
XCase _ x1 alts -> liftM2 (++) (checkCapsXM x1)
(liftM concat $ mapM checkCapsAM alts)
XCast _ cc x1 -> liftM2 (++) (checkCapsCM cc) (checkCapsXM x1)
XType{} -> none
XWitness w -> checkCapsWM w
checkCapsCM :: Cast Name -> CheckM a [Witness Name]
checkCapsCM cc
= let none = return []
in case cc of
CastWeakenEffect{} -> none
CastWeakenClosure{} -> none
CastPurify w -> checkCapsWM w
CastForget w -> checkCapsWM w
checkCapsLM :: Lets a Name -> CheckM a [Witness Name]
checkCapsLM ll
= let none = return []
in case ll of
LLet m _ x -> liftM2 (++) (checkCapsMM m) (checkCapsXM x)
LRec bxs -> liftM concat (mapM checkCapsXM $ map snd bxs)
LLetRegion{} -> none
LWithRegion{} -> none
checkCapsMM :: LetMode Name -> CheckM a [Witness Name]
checkCapsMM mm
= let none = return []
in case mm of
LetStrict -> none
LetLazy (Just w) -> checkCapsWM w
LetLazy Nothing -> none
checkCapsAM :: Alt a Name -> CheckM a [Witness Name]
checkCapsAM aa
= case aa of
AAlt _ x -> checkCapsXM x
checkCapsWM :: Witness Name -> CheckM a [Witness Name]
checkCapsWM ww
= let none = return []
in case ww of
WVar{} -> none
WCon{}
| isCapConW ww -> throw $ ErrorPartial ww
| otherwise -> none
WApp w1@WCon{} w2@(WType tR)
| isCapConW w1
-> if isJust $ takeHandleT tR
then return [ww]
else throw $ ErrorNonHandle ww
| otherwise
-> liftM2 (++) (checkCapsWM w1) (checkCapsWM w2)
WApp w1 w2 -> liftM2 (++) (checkCapsWM w1) (checkCapsWM w2)
WJoin w1 w2 -> liftM2 (++) (checkCapsWM w1) (checkCapsWM w2)
WType{} -> none