{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
module GHC.HsToCore.Pmc.Check (
CheckAction(..),
checkMatchGroup, checkGRHSs, checkPatBind, checkEmptyCase
) where
#include "HsVersions.h"
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 -> 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
<$ :: forall a b. a -> CheckAction b -> CheckAction a
$c<$ :: forall a b. a -> CheckAction b -> CheckAction a
fmap :: forall a b. (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 :: 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) = forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA 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 (forall a. CheckResult a -> Nablas
cr_uncov CheckResult top
t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult { cr_ret :: ret
cr_ret = top -> bot -> ret
f (forall a. CheckResult a -> a
cr_ret CheckResult top
t) (forall a. CheckResult a -> a
cr_ret CheckResult bot
b)
, cr_uncov :: Nablas
cr_uncov = forall a. CheckResult a -> Nablas
cr_uncov CheckResult bot
b
, cr_approx :: Precision
cr_approx = forall a. CheckResult a -> Precision
cr_approx CheckResult top
t forall a. Semigroup a => a -> a -> a
Semi.<> 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) = forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA 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 (forall a. CheckResult a -> a
cr_ret CheckResult Post
l))
Int
limit <- DynFlags -> Int
maxPmCheckModels forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
let uncov :: Nablas
uncov = forall a. CheckResult a -> Nablas
cr_uncov CheckResult Post
l forall a. Semigroup a => a -> a -> a
Semi.<> 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
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult { cr_ret :: ret
cr_ret = Post -> right -> ret
f (forall a. CheckResult a -> a
cr_ret CheckResult Post
l) (forall a. CheckResult a -> a
cr_ret CheckResult right
r)
, cr_uncov :: Nablas
cr_uncov = Nablas
uncov'
, cr_approx :: Precision
cr_approx = Precision
prec' forall a. Semigroup a => a -> a -> a
Semi.<> forall a. CheckResult a -> Precision
cr_approx CheckResult Post
l forall a. Semigroup a => a -> a -> a
Semi.<> 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)
| forall (t :: * -> *) a. Foldable t => t a -> Int
length Bag Nabla
new_ds forall a. Ord a => a -> a -> Bool
> forall a. Ord a => a -> a -> a
max Int
limit (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 :| []) = (forall a. a -> [a] -> NonEmpty a
:| []) 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)) =
forall top bot ret.
(top -> bot -> ret)
-> CheckAction top -> CheckAction bot -> CheckAction ret
topToBottom forall a. a -> NonEmpty a -> NonEmpty a
(NE.<|) (grdtree -> CheckAction anntree
act grdtree
t1) (forall grdtree anntree.
(grdtree -> CheckAction anntree)
-> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
checkSequence grdtree -> CheckAction anntree
act (grdtree
t2forall a. a -> [a] -> NonEmpty a
:|[grdtree]
ts))
emptyRedSets :: RedSets
emptyRedSets :: Post
emptyRedSets = Nablas -> Nablas -> OrdList (Nablas, SrcInfo) -> Post
RedSets forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
checkGrd :: PmGrd -> CheckAction RedSets
checkGrd :: PmGrd -> CheckAction Post
checkGrd PmGrd
grd = forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA 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" (forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> Char -> SDoc
char Char
'=' SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr CoreExpr
e)
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 = 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 = forall a. a -> OrdList a
unitOL (Nablas
div, SrcInfo
info)
| Bool
otherwise = forall a. OrdList a
NilOL
String -> SDoc -> DsM ()
tracePm String
"check:Bang" (forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Nablas
div)
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 = forall a. Monoid a => a
mempty
, cr_approx :: Precision
cr_approx = Precision
Precise }
PmCon Id
x (PmAltConLike ConLike
con) [Id]
_ [Id]
_ [Id]
_
| Id
x forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
considerAccessibleIdKey
, ConLike
con forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
trueDataConKey
-> 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 = 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 forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 (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" forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
[ forall a. Outputable a => a -> SDoc
ppr PmGrd
grd
, forall a. Outputable a => a -> SDoc
ppr Nablas
inc
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"div") Int
2 (forall a. Outputable a => a -> SDoc
ppr Nablas
div)
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"matched") Int
2 (forall a. Outputable a => a -> SDoc
ppr Nablas
matched)
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"uncov") Int
2 (forall a. Outputable a => a -> SDoc
ppr Nablas
uncov)
]
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 [] = forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA forall a b. (a -> b) -> a -> b
$ \Nablas
inc ->
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 = forall a. Monoid a => a
mempty
, cr_approx :: Precision
cr_approx = Precision
Precise }
checkGrds (PmGrd
g:[PmGrd]
grds) = 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 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 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) =
forall p. NonEmpty (PmMatch p) -> PmMatchGroup p
PmMatchGroup forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 }) =
forall right ret.
(Post -> right -> ret)
-> CheckAction Post -> CheckAction right -> CheckAction ret
leftToRight 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 }) =
forall right ret.
(Post -> right -> ret)
-> CheckAction Post -> CheckAction right -> CheckAction ret
leftToRight forall p. p -> NonEmpty (PmGRHS p) -> PmGRHSs p
PmGRHSs ([PmGrd] -> CheckAction Post
checkGrds [PmGrd]
lcls) (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 }) =
forall a b c. (a -> b -> c) -> b -> a -> c
flip forall p. p -> SrcInfo -> PmGRHS p
PmGRHS SrcInfo
rhs_info 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 }) = forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA forall a b. (a -> b) -> a -> b
$ \Nablas
inc -> do
Nablas
unc <- Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas Nablas
inc (Id -> PhiCt
PhiNotBotCt Id
var)
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 = forall a. Monoid a => a
mempty }
checkPatBind :: (PmPatBind Pre) -> CheckAction (PmPatBind Post)
checkPatBind :: PmPatBind Pre -> CheckAction (PmPatBind Post)
checkPatBind = coerce :: forall a b. Coercible a b => a -> b
coerce PmGRHS Pre -> CheckAction (PmGRHS Post)
checkGRHS