{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
module GHC.HsToCore.Pmc.Check (
CheckAction(..),
checkMatchGroup, checkGRHSs, checkPatBind, checkEmptyCase
) where
#include "GhclibHsVersions.h"
import GHC.Prelude
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 { CheckAction a -> Nablas -> DsM (CheckResult a)
unCA :: Nablas -> DsM (CheckResult a) }
deriving a -> CheckAction b -> CheckAction a
(a -> b) -> CheckAction a -> CheckAction b
(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
<$ :: a -> CheckAction b -> CheckAction a
$c<$ :: forall a b. a -> CheckAction b -> CheckAction a
fmap :: (a -> b) -> CheckAction a -> CheckAction b
$cfmap :: forall a b. (a -> b) -> CheckAction a -> CheckAction b
Functor
topToBottom :: (top -> bot -> ret)
-> CheckAction top
-> CheckAction bot
-> CheckAction ret
topToBottom :: (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 (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult :: forall a. a -> Nablas -> Precision -> CheckResult a
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 :: (RedSets -> right -> ret)
-> CheckAction RedSets -> CheckAction right -> CheckAction ret
leftToRight RedSets -> right -> ret
f (CA Nablas -> DsM (CheckResult RedSets)
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 RedSets
l <- Nablas -> DsM (CheckResult RedSets)
left Nablas
inc
CheckResult right
r <- Nablas -> DsM (CheckResult right)
right (RedSets -> Nablas
rs_cov (CheckResult RedSets -> RedSets
forall a. CheckResult a -> a
cr_ret CheckResult RedSets
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 RedSets -> Nablas
forall a. CheckResult a -> Nablas
cr_uncov CheckResult RedSets
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 (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult :: forall a. a -> Nablas -> Precision -> CheckResult a
CheckResult { cr_ret :: ret
cr_ret = RedSets -> right -> ret
f (CheckResult RedSets -> RedSets
forall a. CheckResult a -> a
cr_ret CheckResult RedSets
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 RedSets -> Precision
forall a. CheckResult a -> Precision
cr_approx CheckResult RedSets
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 (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 (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 :: (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 :: RedSets
emptyRedSets = Nablas -> Nablas -> OrdList (Nablas, SrcInfo) -> RedSets
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 RedSets
checkGrd PmGrd
grd = (Nablas -> DsM (CheckResult RedSets)) -> CheckAction RedSets
forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA ((Nablas -> DsM (CheckResult RedSets)) -> CheckAction RedSets)
-> (Nablas -> DsM (CheckResult RedSets)) -> CheckAction RedSets
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 RedSets -> DsM (CheckResult RedSets)
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult :: forall a. a -> Nablas -> Precision -> CheckResult a
CheckResult { cr_ret :: RedSets
cr_ret = RedSets
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 RedSets -> DsM (CheckResult RedSets)
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult :: forall a. a -> Nablas -> Precision -> CheckResult a
CheckResult { cr_ret :: RedSets
cr_ret = RedSets :: Nablas -> Nablas -> OrdList (Nablas, SrcInfo) -> RedSets
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 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 (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 RedSets -> DsM (CheckResult RedSets)
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult :: forall a. a -> Nablas -> Precision -> CheckResult a
CheckResult { cr_ret :: RedSets
cr_ret = RedSets
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 RedSets
checkGrds [] = (Nablas -> DsM (CheckResult RedSets)) -> CheckAction RedSets
forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA ((Nablas -> DsM (CheckResult RedSets)) -> CheckAction RedSets)
-> (Nablas -> DsM (CheckResult RedSets)) -> CheckAction RedSets
forall a b. (a -> b) -> a -> b
$ \Nablas
inc ->
CheckResult RedSets -> DsM (CheckResult RedSets)
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult :: forall a. a -> Nablas -> Precision -> CheckResult a
CheckResult { cr_ret :: RedSets
cr_ret = RedSets
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) = (RedSets -> RedSets -> RedSets)
-> CheckAction RedSets
-> CheckAction RedSets
-> CheckAction RedSets
forall right ret.
(RedSets -> right -> ret)
-> CheckAction RedSets -> CheckAction right -> CheckAction ret
leftToRight RedSets -> RedSets -> RedSets
merge (PmGrd -> CheckAction RedSets
checkGrd PmGrd
g) ([PmGrd] -> CheckAction RedSets
checkGrds [PmGrd]
grds)
where
merge :: RedSets -> RedSets -> RedSets
merge RedSets
ri_g RedSets
ri_grds =
RedSets :: Nablas -> Nablas -> OrdList (Nablas, SrcInfo) -> RedSets
RedSets { rs_cov :: Nablas
rs_cov = RedSets -> Nablas
rs_cov RedSets
ri_grds
, rs_div :: Nablas
rs_div = RedSets -> Nablas
rs_div RedSets
ri_g Nablas -> Nablas -> Nablas
forall a. Semigroup a => a -> a -> a
Semi.<> RedSets -> Nablas
rs_div RedSets
ri_grds
, rs_bangs :: OrdList (Nablas, SrcInfo)
rs_bangs = RedSets -> OrdList (Nablas, SrcInfo)
rs_bangs RedSets
ri_g OrdList (Nablas, SrcInfo)
-> OrdList (Nablas, SrcInfo) -> OrdList (Nablas, SrcInfo)
forall a. Semigroup a => a -> a -> a
Semi.<> RedSets -> OrdList (Nablas, SrcInfo)
rs_bangs RedSets
ri_grds }
checkMatchGroup :: PmMatchGroup Pre -> CheckAction (PmMatchGroup Post)
checkMatchGroup :: PmMatchGroup Pre -> CheckAction (PmMatchGroup RedSets)
checkMatchGroup (PmMatchGroup NonEmpty (PmMatch Pre)
matches) =
NonEmpty (PmMatch RedSets) -> PmMatchGroup RedSets
forall p. NonEmpty (PmMatch p) -> PmMatchGroup p
PmMatchGroup (NonEmpty (PmMatch RedSets) -> PmMatchGroup RedSets)
-> CheckAction (NonEmpty (PmMatch RedSets))
-> CheckAction (PmMatchGroup RedSets)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PmMatch Pre -> CheckAction (PmMatch RedSets))
-> NonEmpty (PmMatch Pre)
-> CheckAction (NonEmpty (PmMatch RedSets))
forall grdtree anntree.
(grdtree -> CheckAction anntree)
-> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
checkSequence PmMatch Pre -> CheckAction (PmMatch RedSets)
checkMatch NonEmpty (PmMatch Pre)
matches
checkMatch :: PmMatch Pre -> CheckAction (PmMatch Post)
checkMatch :: PmMatch Pre -> CheckAction (PmMatch RedSets)
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 }) =
(RedSets -> PmGRHSs RedSets -> PmMatch RedSets)
-> CheckAction RedSets
-> CheckAction (PmGRHSs RedSets)
-> CheckAction (PmMatch RedSets)
forall right ret.
(RedSets -> right -> ret)
-> CheckAction RedSets -> CheckAction right -> CheckAction ret
leftToRight RedSets -> PmGRHSs RedSets -> PmMatch RedSets
forall p. p -> PmGRHSs p -> PmMatch p
PmMatch ([PmGrd] -> CheckAction RedSets
checkGrds [PmGrd]
grds) (PmGRHSs Pre -> CheckAction (PmGRHSs RedSets)
checkGRHSs PmGRHSs Pre
grhss)
checkGRHSs :: PmGRHSs Pre -> CheckAction (PmGRHSs Post)
checkGRHSs :: PmGRHSs Pre -> CheckAction (PmGRHSs RedSets)
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 }) =
(RedSets -> NonEmpty (PmGRHS RedSets) -> PmGRHSs RedSets)
-> CheckAction RedSets
-> CheckAction (NonEmpty (PmGRHS RedSets))
-> CheckAction (PmGRHSs RedSets)
forall right ret.
(RedSets -> right -> ret)
-> CheckAction RedSets -> CheckAction right -> CheckAction ret
leftToRight RedSets -> NonEmpty (PmGRHS RedSets) -> PmGRHSs RedSets
forall p. p -> NonEmpty (PmGRHS p) -> PmGRHSs p
PmGRHSs ([PmGrd] -> CheckAction RedSets
checkGrds [PmGrd]
lcls) ((PmGRHS Pre -> CheckAction (PmGRHS RedSets))
-> NonEmpty (PmGRHS Pre) -> CheckAction (NonEmpty (PmGRHS RedSets))
forall grdtree anntree.
(grdtree -> CheckAction anntree)
-> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
checkSequence PmGRHS Pre -> CheckAction (PmGRHS RedSets)
checkGRHS NonEmpty (PmGRHS Pre)
grhss)
checkGRHS :: PmGRHS Pre -> CheckAction (PmGRHS Post)
checkGRHS :: PmGRHS Pre -> CheckAction (PmGRHS RedSets)
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 }) =
(RedSets -> SrcInfo -> PmGRHS RedSets)
-> SrcInfo -> RedSets -> PmGRHS RedSets
forall a b c. (a -> b -> c) -> b -> a -> c
flip RedSets -> SrcInfo -> PmGRHS RedSets
forall p. p -> SrcInfo -> PmGRHS p
PmGRHS SrcInfo
rhs_info (RedSets -> PmGRHS RedSets)
-> CheckAction RedSets -> CheckAction (PmGRHS RedSets)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PmGrd] -> CheckAction RedSets
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 (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult :: forall a. a -> Nablas -> Precision -> CheckResult a
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 RedSets)
checkPatBind = (PmGRHS Pre -> CheckAction (PmGRHS RedSets))
-> PmPatBind Pre -> CheckAction (PmPatBind RedSets)
coerce PmGRHS Pre -> CheckAction (PmGRHS RedSets)
checkGRHS