{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
module GHC.HsToCore.Pmc.Check (
CheckAction(..),
checkMatchGroup, checkGRHSs, checkPatBind, checkEmptyCase
) where
import GHC.Prelude
import GHC.Builtin.Names ( hasKey, considerAccessibleIdKey, trueDataConKey )
import GHC.HsToCore.Monad ( DsM )
import GHC.HsToCore.Pmc.Types
import GHC.HsToCore.Pmc.Utils
import GHC.HsToCore.Pmc.Solver
import GHC.Driver.Session
import GHC.Utils.Outputable
import GHC.Tc.Utils.TcType (evVarPred)
import GHC.Data.OrdList
import qualified Data.Semigroup as Semi
import Data.List.NonEmpty ( NonEmpty(..) )
import qualified Data.List.NonEmpty as NE
import Data.Coerce
newtype CheckAction a = CA { forall a. CheckAction a -> Nablas -> DsM (CheckResult a)
unCA :: Nablas -> DsM (CheckResult a) }
deriving (forall a b. (a -> b) -> CheckAction a -> CheckAction b)
-> (forall a b. a -> CheckAction b -> CheckAction a)
-> Functor CheckAction
forall a b. a -> CheckAction b -> CheckAction a
forall a b. (a -> b) -> CheckAction a -> CheckAction b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> CheckAction a -> CheckAction b
fmap :: forall a b. (a -> b) -> CheckAction a -> CheckAction b
$c<$ :: forall a b. a -> CheckAction b -> CheckAction a
<$ :: forall a b. a -> CheckAction b -> CheckAction a
Functor
topToBottom :: (top -> bot -> ret)
-> CheckAction top
-> CheckAction bot
-> CheckAction ret
topToBottom :: forall top bot ret.
(top -> bot -> ret)
-> CheckAction top -> CheckAction bot -> CheckAction ret
topToBottom top -> bot -> ret
f (CA Nablas -> DsM (CheckResult top)
top) (CA Nablas -> DsM (CheckResult bot)
bot) = (Nablas -> DsM (CheckResult ret)) -> CheckAction ret
forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA ((Nablas -> DsM (CheckResult ret)) -> CheckAction ret)
-> (Nablas -> DsM (CheckResult ret)) -> CheckAction ret
forall a b. (a -> b) -> a -> b
$ \Nablas
inc -> do
CheckResult top
t <- Nablas -> DsM (CheckResult top)
top Nablas
inc
CheckResult bot
b <- Nablas -> DsM (CheckResult bot)
bot (CheckResult top -> Nablas
forall a. CheckResult a -> Nablas
cr_uncov CheckResult top
t)
CheckResult ret -> DsM (CheckResult ret)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult { cr_ret :: ret
cr_ret = top -> bot -> ret
f (CheckResult top -> top
forall a. CheckResult a -> a
cr_ret CheckResult top
t) (CheckResult bot -> bot
forall a. CheckResult a -> a
cr_ret CheckResult bot
b)
, cr_uncov :: Nablas
cr_uncov = CheckResult bot -> Nablas
forall a. CheckResult a -> Nablas
cr_uncov CheckResult bot
b
, cr_approx :: Precision
cr_approx = CheckResult top -> Precision
forall a. CheckResult a -> Precision
cr_approx CheckResult top
t Precision -> Precision -> Precision
forall a. Semigroup a => a -> a -> a
Semi.<> CheckResult bot -> Precision
forall a. CheckResult a -> Precision
cr_approx CheckResult bot
b }
leftToRight :: (RedSets -> right -> ret)
-> CheckAction RedSets
-> CheckAction right
-> CheckAction ret
leftToRight :: forall right ret.
(Post -> right -> ret)
-> CheckAction Post -> CheckAction right -> CheckAction ret
leftToRight Post -> right -> ret
f (CA Nablas -> DsM (CheckResult Post)
left) (CA Nablas -> DsM (CheckResult right)
right) = (Nablas -> DsM (CheckResult ret)) -> CheckAction ret
forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA ((Nablas -> DsM (CheckResult ret)) -> CheckAction ret)
-> (Nablas -> DsM (CheckResult ret)) -> CheckAction ret
forall a b. (a -> b) -> a -> b
$ \Nablas
inc -> do
CheckResult Post
l <- Nablas -> DsM (CheckResult Post)
left Nablas
inc
CheckResult right
r <- Nablas -> DsM (CheckResult right)
right (Post -> Nablas
rs_cov (CheckResult Post -> Post
forall a. CheckResult a -> a
cr_ret CheckResult Post
l))
Int
limit <- DynFlags -> Int
maxPmCheckModels (DynFlags -> Int)
-> IOEnv (Env DsGblEnv DsLclEnv) DynFlags
-> IOEnv (Env DsGblEnv DsLclEnv) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
let uncov :: Nablas
uncov = CheckResult Post -> Nablas
forall a. CheckResult a -> Nablas
cr_uncov CheckResult Post
l Nablas -> Nablas -> Nablas
forall a. Semigroup a => a -> a -> a
Semi.<> CheckResult right -> Nablas
forall a. CheckResult a -> Nablas
cr_uncov CheckResult right
r
let (Precision
prec', Nablas
uncov') = Int -> Nablas -> Nablas -> (Precision, Nablas)
throttle Int
limit Nablas
inc Nablas
uncov
CheckResult ret -> DsM (CheckResult ret)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult { cr_ret :: ret
cr_ret = Post -> right -> ret
f (CheckResult Post -> Post
forall a. CheckResult a -> a
cr_ret CheckResult Post
l) (CheckResult right -> right
forall a. CheckResult a -> a
cr_ret CheckResult right
r)
, cr_uncov :: Nablas
cr_uncov = Nablas
uncov'
, cr_approx :: Precision
cr_approx = Precision
prec' Precision -> Precision -> Precision
forall a. Semigroup a => a -> a -> a
Semi.<> CheckResult Post -> Precision
forall a. CheckResult a -> Precision
cr_approx CheckResult Post
l Precision -> Precision -> Precision
forall a. Semigroup a => a -> a -> a
Semi.<> CheckResult right -> Precision
forall a. CheckResult a -> Precision
cr_approx CheckResult right
r }
throttle :: Int -> Nablas -> Nablas -> (Precision, Nablas)
throttle :: Int -> Nablas -> Nablas -> (Precision, Nablas)
throttle Int
limit old :: Nablas
old@(MkNablas Bag Nabla
old_ds) new :: Nablas
new@(MkNablas Bag Nabla
new_ds)
| Bag Nabla -> Int
forall a. Bag a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Bag Nabla
new_ds Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
limit (Bag Nabla -> Int
forall a. Bag a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Bag Nabla
old_ds) = (Precision
Approximate, Nablas
old)
| Bool
otherwise = (Precision
Precise, Nablas
new)
checkSequence :: (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
checkSequence :: forall grdtree anntree.
(grdtree -> CheckAction anntree)
-> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
checkSequence grdtree -> CheckAction anntree
act (grdtree
t :| []) = (anntree -> [anntree] -> NonEmpty anntree
forall a. a -> [a] -> NonEmpty a
:| []) (anntree -> NonEmpty anntree)
-> CheckAction anntree -> CheckAction (NonEmpty anntree)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> grdtree -> CheckAction anntree
act grdtree
t
checkSequence grdtree -> CheckAction anntree
act (grdtree
t1 :| (grdtree
t2:[grdtree]
ts)) =
(anntree -> NonEmpty anntree -> NonEmpty anntree)
-> CheckAction anntree
-> CheckAction (NonEmpty anntree)
-> CheckAction (NonEmpty anntree)
forall top bot ret.
(top -> bot -> ret)
-> CheckAction top -> CheckAction bot -> CheckAction ret
topToBottom anntree -> NonEmpty anntree -> NonEmpty anntree
forall a. a -> NonEmpty a -> NonEmpty a
(NE.<|) (grdtree -> CheckAction anntree
act grdtree
t1) ((grdtree -> CheckAction anntree)
-> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
forall grdtree anntree.
(grdtree -> CheckAction anntree)
-> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
checkSequence grdtree -> CheckAction anntree
act (grdtree
t2grdtree -> [grdtree] -> NonEmpty grdtree
forall a. a -> [a] -> NonEmpty a
:|[grdtree]
ts))
emptyRedSets :: RedSets
emptyRedSets :: Post
emptyRedSets = Nablas -> Nablas -> OrdList (Nablas, SrcInfo) -> Post
RedSets Nablas
forall a. Monoid a => a
mempty Nablas
forall a. Monoid a => a
mempty OrdList (Nablas, SrcInfo)
forall a. Monoid a => a
mempty
checkGrd :: PmGrd -> CheckAction RedSets
checkGrd :: PmGrd -> CheckAction Post
checkGrd PmGrd
grd = (Nablas -> DsM (CheckResult Post)) -> CheckAction Post
forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA ((Nablas -> DsM (CheckResult Post)) -> CheckAction Post)
-> (Nablas -> DsM (CheckResult Post)) -> CheckAction Post
forall a b. (a -> b) -> a -> b
$ \Nablas
inc -> case PmGrd
grd of
PmLet Id
x CoreExpr
e -> do
Nablas
matched <- Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas Nablas
inc (Id -> CoreExpr -> PhiCt
PhiCoreCt Id
x CoreExpr
e)
String -> SDoc -> DsM ()
tracePm String
"check:Let" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> Char -> SDoc
char Char
'=' SDoc -> SDoc -> SDoc
<+> CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e)
CheckResult Post -> DsM (CheckResult Post)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult { cr_ret :: Post
cr_ret = Post
emptyRedSets { rs_cov :: Nablas
rs_cov = Nablas
matched }
, cr_uncov :: Nablas
cr_uncov = Nablas
forall a. Monoid a => a
mempty
, cr_approx :: Precision
cr_approx = Precision
Precise }
PmBang Id
x Maybe SrcInfo
mb_info -> do
Nablas
div <- Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas Nablas
inc (Id -> PhiCt
PhiBotCt Id
x)
Nablas
matched <- Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas Nablas
inc (Id -> PhiCt
PhiNotBotCt Id
x)
let bangs :: OrdList (Nablas, SrcInfo)
bangs | Just SrcInfo
info <- Maybe SrcInfo
mb_info = (Nablas, SrcInfo) -> OrdList (Nablas, SrcInfo)
forall a. a -> OrdList a
unitOL (Nablas
div, SrcInfo
info)
| Bool
otherwise = OrdList (Nablas, SrcInfo)
forall a. OrdList a
NilOL
String -> SDoc -> DsM ()
tracePm String
"check:Bang" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> Nablas -> SDoc
forall a. Outputable a => a -> SDoc
ppr Nablas
div)
CheckResult Post -> DsM (CheckResult Post)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult { cr_ret :: Post
cr_ret = RedSets { rs_cov :: Nablas
rs_cov = Nablas
matched, rs_div :: Nablas
rs_div = Nablas
div, rs_bangs :: OrdList (Nablas, SrcInfo)
rs_bangs = OrdList (Nablas, SrcInfo)
bangs }
, cr_uncov :: Nablas
cr_uncov = Nablas
forall a. Monoid a => a
mempty
, cr_approx :: Precision
cr_approx = Precision
Precise }
PmCon Id
x (PmAltConLike ConLike
con) [Id]
_ [Id]
_ [Id]
_
| Id
x Id -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
considerAccessibleIdKey
, ConLike
con ConLike -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
trueDataConKey
-> CheckResult Post -> DsM (CheckResult Post)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult { cr_ret :: Post
cr_ret = Post
emptyRedSets { rs_cov :: Nablas
rs_cov = Nablas
initNablas }
, cr_uncov :: Nablas
cr_uncov = Nablas
forall a. Monoid a => a
mempty
, cr_approx :: Precision
cr_approx = Precision
Precise }
PmCon Id
x PmAltCon
con [Id]
tvs [Id]
dicts [Id]
args -> do
!Nablas
div <- if PmAltCon -> Bool
isPmAltConMatchStrict PmAltCon
con
then Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas Nablas
inc (Id -> PhiCt
PhiBotCt Id
x)
else Nablas -> DsM Nablas
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nablas
forall a. Monoid a => a
mempty
!Nablas
matched <- Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas Nablas
inc (Id -> PmAltCon -> [Id] -> [PredType] -> [Id] -> PhiCt
PhiConCt Id
x PmAltCon
con [Id]
tvs ((Id -> PredType) -> [Id] -> [PredType]
forall a b. (a -> b) -> [a] -> [b]
map Id -> PredType
evVarPred [Id]
dicts) [Id]
args)
!Nablas
uncov <- Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas Nablas
inc (Id -> PmAltCon -> PhiCt
PhiNotConCt Id
x PmAltCon
con)
String -> SDoc -> DsM ()
tracePm String
"check:Con" (SDoc -> DsM ()) -> SDoc -> DsM ()
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
[ PmGrd -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmGrd
grd
, Nablas -> SDoc
forall a. Outputable a => a -> SDoc
ppr Nablas
inc
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"div") Int
2 (Nablas -> SDoc
forall a. Outputable a => a -> SDoc
ppr Nablas
div)
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"matched") Int
2 (Nablas -> SDoc
forall a. Outputable a => a -> SDoc
ppr Nablas
matched)
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"uncov") Int
2 (Nablas -> SDoc
forall a. Outputable a => a -> SDoc
ppr Nablas
uncov)
]
CheckResult Post -> DsM (CheckResult Post)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult { cr_ret :: Post
cr_ret = Post
emptyRedSets { rs_cov :: Nablas
rs_cov = Nablas
matched, rs_div :: Nablas
rs_div = Nablas
div }
, cr_uncov :: Nablas
cr_uncov = Nablas
uncov
, cr_approx :: Precision
cr_approx = Precision
Precise }
checkGrds :: [PmGrd] -> CheckAction RedSets
checkGrds :: [PmGrd] -> CheckAction Post
checkGrds [] = (Nablas -> DsM (CheckResult Post)) -> CheckAction Post
forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA ((Nablas -> DsM (CheckResult Post)) -> CheckAction Post)
-> (Nablas -> DsM (CheckResult Post)) -> CheckAction Post
forall a b. (a -> b) -> a -> b
$ \Nablas
inc ->
CheckResult Post -> DsM (CheckResult Post)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult { cr_ret :: Post
cr_ret = Post
emptyRedSets { rs_cov :: Nablas
rs_cov = Nablas
inc }
, cr_uncov :: Nablas
cr_uncov = Nablas
forall a. Monoid a => a
mempty
, cr_approx :: Precision
cr_approx = Precision
Precise }
checkGrds (PmGrd
g:[PmGrd]
grds) = (Post -> Post -> Post)
-> CheckAction Post -> CheckAction Post -> CheckAction Post
forall right ret.
(Post -> right -> ret)
-> CheckAction Post -> CheckAction right -> CheckAction ret
leftToRight Post -> Post -> Post
merge (PmGrd -> CheckAction Post
checkGrd PmGrd
g) ([PmGrd] -> CheckAction Post
checkGrds [PmGrd]
grds)
where
merge :: Post -> Post -> Post
merge Post
ri_g Post
ri_grds =
RedSets { rs_cov :: Nablas
rs_cov = Post -> Nablas
rs_cov Post
ri_grds
, rs_div :: Nablas
rs_div = Post -> Nablas
rs_div Post
ri_g Nablas -> Nablas -> Nablas
forall a. Semigroup a => a -> a -> a
Semi.<> Post -> Nablas
rs_div Post
ri_grds
, rs_bangs :: OrdList (Nablas, SrcInfo)
rs_bangs = Post -> OrdList (Nablas, SrcInfo)
rs_bangs Post
ri_g OrdList (Nablas, SrcInfo)
-> OrdList (Nablas, SrcInfo) -> OrdList (Nablas, SrcInfo)
forall a. Semigroup a => a -> a -> a
Semi.<> Post -> OrdList (Nablas, SrcInfo)
rs_bangs Post
ri_grds }
checkMatchGroup :: PmMatchGroup Pre -> CheckAction (PmMatchGroup Post)
checkMatchGroup :: PmMatchGroup Pre -> CheckAction (PmMatchGroup Post)
checkMatchGroup (PmMatchGroup NonEmpty (PmMatch Pre)
matches) =
NonEmpty (PmMatch Post) -> PmMatchGroup Post
forall p. NonEmpty (PmMatch p) -> PmMatchGroup p
PmMatchGroup (NonEmpty (PmMatch Post) -> PmMatchGroup Post)
-> CheckAction (NonEmpty (PmMatch Post))
-> CheckAction (PmMatchGroup Post)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PmMatch Pre -> CheckAction (PmMatch Post))
-> NonEmpty (PmMatch Pre) -> CheckAction (NonEmpty (PmMatch Post))
forall grdtree anntree.
(grdtree -> CheckAction anntree)
-> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
checkSequence PmMatch Pre -> CheckAction (PmMatch Post)
checkMatch NonEmpty (PmMatch Pre)
matches
checkMatch :: PmMatch Pre -> CheckAction (PmMatch Post)
checkMatch :: PmMatch Pre -> CheckAction (PmMatch Post)
checkMatch (PmMatch { pm_pats :: forall p. PmMatch p -> p
pm_pats = GrdVec [PmGrd]
grds, pm_grhss :: forall p. PmMatch p -> PmGRHSs p
pm_grhss = PmGRHSs Pre
grhss }) =
(Post -> PmGRHSs Post -> PmMatch Post)
-> CheckAction Post
-> CheckAction (PmGRHSs Post)
-> CheckAction (PmMatch Post)
forall right ret.
(Post -> right -> ret)
-> CheckAction Post -> CheckAction right -> CheckAction ret
leftToRight Post -> PmGRHSs Post -> PmMatch Post
forall p. p -> PmGRHSs p -> PmMatch p
PmMatch ([PmGrd] -> CheckAction Post
checkGrds [PmGrd]
grds) (PmGRHSs Pre -> CheckAction (PmGRHSs Post)
checkGRHSs PmGRHSs Pre
grhss)
checkGRHSs :: PmGRHSs Pre -> CheckAction (PmGRHSs Post)
checkGRHSs :: PmGRHSs Pre -> CheckAction (PmGRHSs Post)
checkGRHSs (PmGRHSs { pgs_lcls :: forall p. PmGRHSs p -> p
pgs_lcls = GrdVec [PmGrd]
lcls, pgs_grhss :: forall p. PmGRHSs p -> NonEmpty (PmGRHS p)
pgs_grhss = NonEmpty (PmGRHS Pre)
grhss }) =
(Post -> NonEmpty (PmGRHS Post) -> PmGRHSs Post)
-> CheckAction Post
-> CheckAction (NonEmpty (PmGRHS Post))
-> CheckAction (PmGRHSs Post)
forall right ret.
(Post -> right -> ret)
-> CheckAction Post -> CheckAction right -> CheckAction ret
leftToRight Post -> NonEmpty (PmGRHS Post) -> PmGRHSs Post
forall p. p -> NonEmpty (PmGRHS p) -> PmGRHSs p
PmGRHSs ([PmGrd] -> CheckAction Post
checkGrds [PmGrd]
lcls) ((PmGRHS Pre -> CheckAction (PmGRHS Post))
-> NonEmpty (PmGRHS Pre) -> CheckAction (NonEmpty (PmGRHS Post))
forall grdtree anntree.
(grdtree -> CheckAction anntree)
-> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
checkSequence PmGRHS Pre -> CheckAction (PmGRHS Post)
checkGRHS NonEmpty (PmGRHS Pre)
grhss)
checkGRHS :: PmGRHS Pre -> CheckAction (PmGRHS Post)
checkGRHS :: PmGRHS Pre -> CheckAction (PmGRHS Post)
checkGRHS (PmGRHS { pg_grds :: forall p. PmGRHS p -> p
pg_grds = GrdVec [PmGrd]
grds, pg_rhs :: forall p. PmGRHS p -> SrcInfo
pg_rhs = SrcInfo
rhs_info }) =
(Post -> SrcInfo -> PmGRHS Post) -> SrcInfo -> Post -> PmGRHS Post
forall a b c. (a -> b -> c) -> b -> a -> c
flip Post -> SrcInfo -> PmGRHS Post
forall p. p -> SrcInfo -> PmGRHS p
PmGRHS SrcInfo
rhs_info (Post -> PmGRHS Post)
-> CheckAction Post -> CheckAction (PmGRHS Post)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PmGrd] -> CheckAction Post
checkGrds [PmGrd]
grds
checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase
checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase
checkEmptyCase pe :: PmEmptyCase
pe@(PmEmptyCase { pe_var :: PmEmptyCase -> Id
pe_var = Id
var }) = (Nablas -> DsM (CheckResult PmEmptyCase))
-> CheckAction PmEmptyCase
forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA ((Nablas -> DsM (CheckResult PmEmptyCase))
-> CheckAction PmEmptyCase)
-> (Nablas -> DsM (CheckResult PmEmptyCase))
-> CheckAction PmEmptyCase
forall a b. (a -> b) -> a -> b
$ \Nablas
inc -> do
Nablas
unc <- Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas Nablas
inc (Id -> PhiCt
PhiNotBotCt Id
var)
CheckResult PmEmptyCase -> DsM (CheckResult PmEmptyCase)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult { cr_ret :: PmEmptyCase
cr_ret = PmEmptyCase
pe, cr_uncov :: Nablas
cr_uncov = Nablas
unc, cr_approx :: Precision
cr_approx = Precision
forall a. Monoid a => a
mempty }
checkPatBind :: (PmPatBind Pre) -> CheckAction (PmPatBind Post)
checkPatBind :: PmPatBind Pre -> CheckAction (PmPatBind Post)
checkPatBind = (PmGRHS Pre -> CheckAction (PmGRHS Post))
-> PmPatBind Pre -> CheckAction (PmPatBind Post)
forall a b. Coercible a b => a -> b
coerce PmGRHS Pre -> CheckAction (PmGRHS Post)
checkGRHS