{-# LANGUAGE CPP #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE LambdaCase #-}
module Test.Inspection.Plugin
( plugin
, checkProperty
, CheckResult(..)
, prettyProperty
) where
import Control.Monad
import System.Exit
import Data.Either
import Data.Maybe
import Data.Bifunctor
import Data.List
import qualified Data.Map.Strict as M
import qualified Language.Haskell.TH.Syntax as TH
#if MIN_VERSION_ghc(9,4,0)
import GHC.Types.Error
import GHC.Driver.Session
#endif
#if MIN_VERSION_ghc(9,0,0)
import GHC.Plugins hiding (SrcLoc)
import GHC.Utils.Outputable as Outputable
#else
import GhcPlugins hiding (SrcLoc)
import Outputable
#endif
#if MIN_VERSION_ghc(9,2,0)
import GHC.Types.TyThing
#endif
import Test.Inspection (Obligation(..), Equivalence (..), Property(..), Result(..))
import Test.Inspection.Core
plugin :: Plugin
plugin :: Plugin
plugin = Plugin
defaultPlugin
{ installCoreToDos :: CorePlugin
installCoreToDos = CorePlugin
install
#if __GLASGOW_HASKELL__ >= 806
, pluginRecompile :: [String] -> IO PluginRecompile
pluginRecompile = \[String]
_args -> forall (f :: * -> *) a. Applicative f => a -> f a
pure PluginRecompile
NoForceRecompile
#endif
}
data UponFailure = AbortCompilation | KeepGoingO0 | SkipO0 | KeepGoing deriving UponFailure -> UponFailure -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UponFailure -> UponFailure -> Bool
$c/= :: UponFailure -> UponFailure -> Bool
== :: UponFailure -> UponFailure -> Bool
$c== :: UponFailure -> UponFailure -> Bool
Eq
data ReportingMode = Verbose | Quiet deriving ReportingMode -> ReportingMode -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ReportingMode -> ReportingMode -> Bool
$c/= :: ReportingMode -> ReportingMode -> Bool
== :: ReportingMode -> ReportingMode -> Bool
$c== :: ReportingMode -> ReportingMode -> Bool
Eq
data ResultTarget = PrintAndAbort | StoreAt Name
install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
install :: CorePlugin
install [String]
args [CoreToDo]
passes = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [CoreToDo]
passes forall a. [a] -> [a] -> [a]
++ [CoreToDo
pass]
where
pass :: CoreToDo
pass = String -> CorePluginPass -> CoreToDo
CoreDoPluginPass String
"Test.Inspection.Plugin" (UponFailure -> ReportingMode -> CorePluginPass
proofPass UponFailure
upon_failure ReportingMode
report)
upon_failure :: UponFailure
upon_failure | String
"keep-going" forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
args = UponFailure
KeepGoing
| String
"keep-going-O0" forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
args = UponFailure
KeepGoingO0
| String
"skip-O0" forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
args = UponFailure
SkipO0
| Bool
otherwise = UponFailure
AbortCompilation
report :: ReportingMode
report | String
"quiet" forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
args = ReportingMode
Quiet
| Bool
otherwise = ReportingMode
Verbose
extractObligations :: ModGuts -> (ModGuts, [(ResultTarget, Obligation)])
ModGuts
guts = (ModGuts
guts', [(ResultTarget, Obligation)]
obligations)
where
([Annotation]
anns_clean, [(ResultTarget, Obligation)]
obligations) = forall a b. (a -> Maybe b) -> [a] -> ([a], [b])
partitionMaybe Annotation -> Maybe (ResultTarget, Obligation)
findObligationAnn (ModGuts -> [Annotation]
mg_anns ModGuts
guts)
guts' :: ModGuts
guts' = ModGuts
guts { mg_anns :: [Annotation]
mg_anns = [Annotation]
anns_clean }
findObligationAnn :: Annotation -> Maybe (ResultTarget, Obligation)
findObligationAnn :: Annotation -> Maybe (ResultTarget, Obligation)
findObligationAnn (Annotation (ModuleTarget Module
_) AnnPayload
payload)
| Just Obligation
obl <- forall a. Typeable a => ([Word8] -> a) -> AnnPayload -> Maybe a
fromSerialized forall a. Data a => [Word8] -> a
deserializeWithData AnnPayload
payload
= forall a. a -> Maybe a
Just (ResultTarget
PrintAndAbort, Obligation
obl)
findObligationAnn (Annotation (NamedTarget Name
n) AnnPayload
payload)
| Just Obligation
obl <- forall a. Typeable a => ([Word8] -> a) -> AnnPayload -> Maybe a
fromSerialized forall a. Data a => [Word8] -> a
deserializeWithData AnnPayload
payload
= forall a. a -> Maybe a
Just (Name -> ResultTarget
StoreAt Name
n, Obligation
obl)
findObligationAnn Annotation
_
= forall a. Maybe a
Nothing
prettyObligation :: Module -> Obligation -> String -> String
prettyObligation :: Module -> Obligation -> String -> String
prettyObligation Module
mod (Obligation {Bool
Maybe String
Maybe Loc
Name
Property
storeResult :: Obligation -> Maybe String
srcLoc :: Obligation -> Maybe Loc
expectFail :: Obligation -> Bool
testName :: Obligation -> Maybe String
property :: Obligation -> Property
target :: Obligation -> Name
storeResult :: Maybe String
srcLoc :: Maybe Loc
expectFail :: Bool
testName :: Maybe String
property :: Property
target :: Name
..}) String
result =
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" Loc -> String
myPrettySrcLoc Maybe Loc
srcLoc forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ String
name forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
result
where
name :: String
name = case Maybe String
testName of
Just String
n -> String
n
Maybe String
Nothing -> (Name -> String) -> Name -> Property -> String
prettyProperty (Module -> Name -> String
showTHName Module
mod) Name
target Property
property
prettyProperty :: (TH.Name -> String) -> TH.Name -> Property -> String
prettyProperty :: (Name -> String) -> Name -> Property -> String
prettyProperty Name -> String
showName Name
target = \case
EqualTo Name
n2 Equivalence
eqv -> Name -> String
showName Name
target forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Equivalence -> String
showEquiv Equivalence
eqv forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Name -> String
showName Name
n2
NoTypes [Name
t] -> Name -> String
showName Name
target forall a. [a] -> [a] -> [a]
++ String
" `hasNoType` " forall a. [a] -> [a] -> [a]
++ Name -> String
showName Name
t
NoTypes [Name]
ts -> Name -> String
showName Name
target forall a. [a] -> [a] -> [a]
++ String
" mentions none of " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map Name -> String
showName [Name]
ts)
Property
NoAllocation -> Name -> String
showName Name
target forall a. [a] -> [a] -> [a]
++ String
" does not allocate"
NoTypeClasses [] -> Name -> String
showName Name
target forall a. [a] -> [a] -> [a]
++ String
" does not contain dictionary values"
NoTypeClasses [Name]
ts -> Name -> String
showName Name
target forall a. [a] -> [a] -> [a]
++ String
" does not contain dictionary values except of " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map Name -> String
showName [Name]
ts)
NoUseOf [Name]
ns -> Name -> String
showName Name
target forall a. [a] -> [a] -> [a]
++ String
" uses none of " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map Name -> String
showName [Name]
ns)
Property
CoreOf -> Name -> String
showName Name
target forall a. [a] -> [a] -> [a]
++ String
" core dump"
where
showEquiv :: Equivalence -> String
showEquiv Equivalence
StrictEquiv = String
"==="
showEquiv Equivalence
IgnoreTypesAndTicksEquiv = String
"==-"
showEquiv Equivalence
UnorderedLetsEquiv = String
"==~"
showTHName :: Module -> TH.Name -> String
showTHName :: Module -> Name -> String
showTHName Module
mod (TH.Name OccName
occ (TH.NameQ ModName
m))
| ModuleName -> String
moduleNameString (forall unit. GenModule unit -> ModuleName
moduleName Module
mod) forall a. Eq a => a -> a -> Bool
== ModName -> String
TH.modString ModName
m = OccName -> String
TH.occString OccName
occ
showTHName Module
mod (TH.Name OccName
occ (TH.NameG NameSpace
_ PkgName
_ ModName
m))
| ModuleName -> String
moduleNameString (forall unit. GenModule unit -> ModuleName
moduleName Module
mod) forall a. Eq a => a -> a -> Bool
== ModName -> String
TH.modString ModName
m = OccName -> String
TH.occString OccName
occ
showTHName Module
_ Name
n = forall a. Show a => a -> String
show Name
n
data Stat = ExpSuccess | ExpFailure | UnexpSuccess | UnexpFailure | StoredResult
deriving (Int -> Stat
Stat -> Int
Stat -> [Stat]
Stat -> Stat
Stat -> Stat -> [Stat]
Stat -> Stat -> Stat -> [Stat]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Stat -> Stat -> Stat -> [Stat]
$cenumFromThenTo :: Stat -> Stat -> Stat -> [Stat]
enumFromTo :: Stat -> Stat -> [Stat]
$cenumFromTo :: Stat -> Stat -> [Stat]
enumFromThen :: Stat -> Stat -> [Stat]
$cenumFromThen :: Stat -> Stat -> [Stat]
enumFrom :: Stat -> [Stat]
$cenumFrom :: Stat -> [Stat]
fromEnum :: Stat -> Int
$cfromEnum :: Stat -> Int
toEnum :: Int -> Stat
$ctoEnum :: Int -> Stat
pred :: Stat -> Stat
$cpred :: Stat -> Stat
succ :: Stat -> Stat
$csucc :: Stat -> Stat
Enum, Stat -> Stat -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Stat -> Stat -> Bool
$c/= :: Stat -> Stat -> Bool
== :: Stat -> Stat -> Bool
$c== :: Stat -> Stat -> Bool
Eq, Eq Stat
Stat -> Stat -> Bool
Stat -> Stat -> Ordering
Stat -> Stat -> Stat
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Stat -> Stat -> Stat
$cmin :: Stat -> Stat -> Stat
max :: Stat -> Stat -> Stat
$cmax :: Stat -> Stat -> Stat
>= :: Stat -> Stat -> Bool
$c>= :: Stat -> Stat -> Bool
> :: Stat -> Stat -> Bool
$c> :: Stat -> Stat -> Bool
<= :: Stat -> Stat -> Bool
$c<= :: Stat -> Stat -> Bool
< :: Stat -> Stat -> Bool
$c< :: Stat -> Stat -> Bool
compare :: Stat -> Stat -> Ordering
$ccompare :: Stat -> Stat -> Ordering
Ord, Stat
forall a. a -> a -> Bounded a
maxBound :: Stat
$cmaxBound :: Stat
minBound :: Stat
$cminBound :: Stat
Bounded)
type Stats = M.Map Stat Int
type Updates = [(Name, Result)]
tick :: Stat -> Stats
tick :: Stat -> Stats
tick Stat
s = forall k a. k -> a -> Map k a
M.singleton Stat
s Int
1
checkObligation :: ReportingMode -> ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats)
checkObligation :: ReportingMode
-> ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats)
checkObligation ReportingMode
report ModGuts
guts (ResultTarget
reportTarget, Obligation
obl) = do
CheckResult
res <- ModGuts -> Name -> Property -> CoreM CheckResult
checkProperty ModGuts
guts (Obligation -> Name
target Obligation
obl) (Obligation -> Property
property Obligation
obl)
case ResultTarget
reportTarget of
ResultTarget
PrintAndAbort -> do
Stat
category <- case (CheckResult
res, Obligation -> Bool
expectFail Obligation
obl) of
(CheckResult
ResSuccess, Bool
False) -> do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ReportingMode
report forall a. Eq a => a -> a -> Bool
== ReportingMode
Quiet) forall a b. (a -> b) -> a -> b
$
String -> CoreM ()
putMsgS forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
expSuccess
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
ExpSuccess
(CheckResult
ResSuccess, Bool
True) -> do
String -> CoreM ()
putMsgS forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
unexpSuccess
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
UnexpSuccess
(ResSuccessWithMessage SDoc
reportDoc, Bool
False) -> do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ReportingMode
report forall a. Eq a => a -> a -> Bool
== ReportingMode
Quiet) forall a b. (a -> b) -> a -> b
$ do
String -> CoreM ()
putMsgS forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
expSuccess
SDoc -> CoreM ()
putMsg SDoc
reportDoc
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
ExpSuccess
(ResSuccessWithMessage SDoc
reportDoc, Bool
True) -> do
String -> CoreM ()
putMsgS forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
unexpSuccess
SDoc -> CoreM ()
putMsg SDoc
reportDoc
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
UnexpSuccess
(ResFailure SDoc
reportDoc, Bool
False) -> do
String -> CoreM ()
putMsgS forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
unexpFailure
SDoc -> CoreM ()
putMsg forall a b. (a -> b) -> a -> b
$ SDoc
reportDoc
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
UnexpFailure
(ResFailure SDoc
_, Bool
True) -> do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ReportingMode
report forall a. Eq a => a -> a -> Bool
== ReportingMode
Quiet) forall a b. (a -> b) -> a -> b
$
String -> CoreM ()
putMsgS forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
expFailure
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
ExpFailure
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Stat -> Stats
tick Stat
category)
StoreAt Name
name -> do
DynFlags
dflags <- forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
let result :: Result
result = case CheckResult
res of
CheckResult
ResSuccess -> String -> Result
Success forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> String
showSDoc DynFlags
dflags forall a b. (a -> b) -> a -> b
$
String -> SDoc
text (Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
expSuccess)
ResSuccessWithMessage SDoc
msg -> String -> Result
Success forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> String
showSDoc DynFlags
dflags forall a b. (a -> b) -> a -> b
$
String -> SDoc
text (Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
expSuccess) SDoc -> SDoc -> SDoc
$$
SDoc
msg
ResFailure SDoc
reportMsg -> String -> Result
Failure forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> String
showSDoc DynFlags
dflags forall a b. (a -> b) -> a -> b
$
String -> SDoc
text (Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
unexpFailure) SDoc -> SDoc -> SDoc
$$
SDoc
reportMsg
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Name
name, Result
result)], Stat -> Stats
tick Stat
StoredResult)
where
expSuccess :: String
expSuccess = String
"passed."
unexpSuccess :: String
unexpSuccess = String
"passed unexpectedly!"
unexpFailure :: String
unexpFailure = String
"failed:"
expFailure :: String
expFailure = String
"failed expectedly."
data CheckResult
= ResSuccess
| ResSuccessWithMessage SDoc
| ResFailure SDoc
lookupNameInGuts :: ModGuts -> Name -> Maybe (Var, CoreExpr)
lookupNameInGuts :: ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n = forall a. [a] -> Maybe a
listToMaybe
[ (CoreBndr
v,CoreExpr
e)
| (CoreBndr
v,CoreExpr
e) <- forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> CoreProgram
mg_binds ModGuts
guts)
, forall a. NamedThing a => a -> Name
getName CoreBndr
v forall a. Eq a => a -> a -> Bool
== Name
n
]
updateNameInGuts :: Name -> CoreExpr -> ModGuts -> ModGuts
updateNameInGuts :: Name -> CoreExpr -> ModGuts -> ModGuts
updateNameInGuts Name
n CoreExpr
expr ModGuts
guts =
ModGuts
guts {mg_binds :: CoreProgram
mg_binds = forall a b. (a -> b) -> [a] -> [b]
map (Name -> CoreExpr -> CoreBind -> CoreBind
updateNameInGut Name
n CoreExpr
expr) (ModGuts -> CoreProgram
mg_binds ModGuts
guts) }
updateNameInGut :: Name -> CoreExpr -> CoreBind -> CoreBind
updateNameInGut :: Name -> CoreExpr -> CoreBind -> CoreBind
updateNameInGut Name
n CoreExpr
e (NonRec CoreBndr
v CoreExpr
_) | forall a. NamedThing a => a -> Name
getName CoreBndr
v forall a. Eq a => a -> a -> Bool
== Name
n = forall b. b -> Expr b -> Bind b
NonRec CoreBndr
v CoreExpr
e
updateNameInGut Name
_ CoreExpr
_ CoreBind
bind = CoreBind
bind
checkProperty :: ModGuts -> TH.Name -> Property -> CoreM CheckResult
checkProperty :: ModGuts -> Name -> Property -> CoreM CheckResult
checkProperty ModGuts
guts Name
thn1 (EqualTo Name
thn2 Equivalence
ignore_types) = do
Name
n1 <- Name -> CoreM Name
fromTHName Name
thn1
Name
n2 <- Name -> CoreM Name
fromTHName Name
thn2
let p1 :: Maybe (CoreBndr, CoreExpr)
p1 = ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n1
let p2 :: Maybe (CoreBndr, CoreExpr)
p2 = ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n2
if | Name
n1 forall a. Eq a => a -> a -> Bool
== Name
n2
-> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
| Just (CoreBndr
_, Var CoreBndr
other) <- Maybe (CoreBndr, CoreExpr)
p1, forall a. NamedThing a => a -> Name
getName CoreBndr
other forall a. Eq a => a -> a -> Bool
== Name
n2
-> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
| Just (CoreBndr
_, Var CoreBndr
other) <- Maybe (CoreBndr, CoreExpr)
p2, forall a. NamedThing a => a -> Name
getName CoreBndr
other forall a. Eq a => a -> a -> Bool
== Name
n1
-> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
| Just (CoreBndr
v1, CoreExpr
_) <- Maybe (CoreBndr, CoreExpr)
p1
, Just (CoreBndr
v2, CoreExpr
_) <- Maybe (CoreBndr, CoreExpr)
p2
, let slice1 :: [(CoreBndr, CoreExpr)]
slice1 = [(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
slice [(CoreBndr, CoreExpr)]
binds CoreBndr
v1
, let slice2 :: [(CoreBndr, CoreExpr)]
slice2 = [(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
slice [(CoreBndr, CoreExpr)]
binds CoreBndr
v2
-> if Equivalence
-> [(CoreBndr, CoreExpr)] -> [(CoreBndr, CoreExpr)] -> Bool
eqSlice Equivalence
ignore_types [(CoreBndr, CoreExpr)]
slice1 [(CoreBndr, CoreExpr)]
slice2
then forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
else forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure forall a b. (a -> b) -> a -> b
$ [(CoreBndr, CoreExpr)] -> [(CoreBndr, CoreExpr)] -> SDoc
pprSliceDifference [(CoreBndr, CoreExpr)]
slice1 [(CoreBndr, CoreExpr)]
slice2
| Maybe (CoreBndr, CoreExpr)
Nothing <- Maybe (CoreBndr, CoreExpr)
p1
, Maybe (CoreBndr, CoreExpr)
Nothing <- Maybe (CoreBndr, CoreExpr)
p2
-> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr Name
n1 SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
" and " SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Name
n2 SDoc -> SDoc -> SDoc
<+>
String -> SDoc
text String
"are different external names"
| Maybe (CoreBndr, CoreExpr)
Nothing <- Maybe (CoreBndr, CoreExpr)
p1
-> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr Name
n1 SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is an external name"
| Maybe (CoreBndr, CoreExpr)
Nothing <- Maybe (CoreBndr, CoreExpr)
p2
-> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr Name
n2 SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is an external name"
where
binds :: [(CoreBndr, CoreExpr)]
binds = forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> CoreProgram
mg_binds ModGuts
guts)
checkProperty ModGuts
guts Name
thn (NoUseOf [Name]
thns) = do
Name
n <- Name -> CoreM Name
fromTHName Name
thn
[Name]
ns <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> CoreM Name
fromTHName [Name]
thns
case ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n of
Maybe (CoreBndr, CoreExpr)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr Name
n SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is not a local name"
Just (CoreBndr
v, CoreExpr
_) -> case [(CoreBndr, CoreExpr)] -> [Name] -> Maybe (CoreBndr, CoreExpr)
freeOfTerm ([(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
slice [(CoreBndr, CoreExpr)]
binds CoreBndr
v) [Name]
ns of
Just (CoreBndr, CoreExpr)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure forall a b. (a -> b) -> a -> b
$ [(CoreBndr, CoreExpr)] -> SDoc
pprSlice ([(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
slice [(CoreBndr, CoreExpr)]
binds CoreBndr
v)
Maybe (CoreBndr, CoreExpr)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
where binds :: [(CoreBndr, CoreExpr)]
binds = forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> CoreProgram
mg_binds ModGuts
guts)
checkProperty ModGuts
guts Name
thn (NoTypes [Name]
thts) = do
Name
n <- Name -> CoreM Name
fromTHName Name
thn
[Name]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> CoreM Name
fromTHName [Name]
thts
case ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n of
Maybe (CoreBndr, CoreExpr)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr Name
n SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is not a local name"
Just (CoreBndr
v, CoreExpr
_) -> case [(CoreBndr, CoreExpr)] -> [Name] -> Maybe (CoreBndr, CoreExpr)
freeOfType ([(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
slice [(CoreBndr, CoreExpr)]
binds CoreBndr
v) [Name]
ts of
Just (CoreBndr, CoreExpr)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure forall a b. (a -> b) -> a -> b
$ [(CoreBndr, CoreExpr)] -> SDoc
pprSlice ([(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
slice [(CoreBndr, CoreExpr)]
binds CoreBndr
v)
Maybe (CoreBndr, CoreExpr)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
where binds :: [(CoreBndr, CoreExpr)]
binds = forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> CoreProgram
mg_binds ModGuts
guts)
checkProperty ModGuts
guts Name
thn Property
NoAllocation = do
Name
n <- Name -> CoreM Name
fromTHName Name
thn
case ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n of
Maybe (CoreBndr, CoreExpr)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr Name
n SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is not a local name"
Just (CoreBndr
v, CoreExpr
_) -> case [(CoreBndr, CoreExpr)] -> Maybe (CoreBndr, CoreExpr)
doesNotAllocate ([(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
slice [(CoreBndr, CoreExpr)]
binds CoreBndr
v) of
Just (CoreBndr
v',CoreExpr
e') -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure forall a b. (a -> b) -> a -> b
$ Int -> SDoc -> SDoc
nest Int
4 (forall a. Outputable a => a -> SDoc
ppr CoreBndr
v' SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr CoreExpr
e')
Maybe (CoreBndr, CoreExpr)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
where binds :: [(CoreBndr, CoreExpr)]
binds = forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> CoreProgram
mg_binds ModGuts
guts)
checkProperty ModGuts
guts Name
thn (NoTypeClasses [Name]
thts) = do
Name
n <- Name -> CoreM Name
fromTHName Name
thn
[Name]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> CoreM Name
fromTHName [Name]
thts
case ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n of
Maybe (CoreBndr, CoreExpr)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr Name
n SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is not a local name"
Just (CoreBndr
v, CoreExpr
_) -> case [(CoreBndr, CoreExpr)]
-> [Name] -> Maybe (CoreBndr, CoreExpr, [TyCon])
doesNotContainTypeClasses ([(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
slice [(CoreBndr, CoreExpr)]
binds CoreBndr
v) [Name]
ts of
Just (CoreBndr
v',CoreExpr
e',[TyCon]
tc) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure
forall a b. (a -> b) -> a -> b
$ Int -> SDoc -> SDoc
nest Int
4 forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
[ String -> SDoc
text String
"Found type classes: " SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr [TyCon]
tc
, forall a. Outputable a => a -> SDoc
ppr CoreBndr
v' SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr CoreExpr
e'
]
Maybe (CoreBndr, CoreExpr, [TyCon])
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
where binds :: [(CoreBndr, CoreExpr)]
binds = forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> CoreProgram
mg_binds ModGuts
guts)
checkProperty ModGuts
guts Name
thn Property
CoreOf = do
Name
n <- Name -> CoreM Name
fromTHName Name
thn
case ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n of
Maybe (CoreBndr, CoreExpr)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr Name
n SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"is not a local name"
Just (CoreBndr
v, CoreExpr
_) -> do
let s :: [(CoreBndr, CoreExpr)]
s = [(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
slice [(CoreBndr, CoreExpr)]
binds CoreBndr
v
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SDoc -> CheckResult
ResSuccessWithMessage forall a b. (a -> b) -> a -> b
$ Int -> SDoc -> SDoc
nest Int
4 forall a b. (a -> b) -> a -> b
$ [(CoreBndr, CoreExpr)] -> SDoc
pprSlice [(CoreBndr, CoreExpr)]
s
where binds :: [(CoreBndr, CoreExpr)]
binds = forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> CoreProgram
mg_binds ModGuts
guts)
fromTHName :: TH.Name -> CoreM Name
fromTHName :: Name -> CoreM Name
fromTHName Name
thn = Name -> CoreM (Maybe Name)
thNameToGhcName Name
thn forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe Name
Nothing -> do
SDoc -> CoreM ()
errorMsg forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"Could not resolve TH name" SDoc -> SDoc -> SDoc
<+> String -> SDoc
text (forall a. Show a => a -> String
show Name
thn)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IO a
exitFailure
Just Name
n -> forall (m :: * -> *) a. Monad m => a -> m a
return Name
n
storeResults :: Updates -> ModGuts -> CoreM ModGuts
storeResults :: Updates -> CorePluginPass
storeResults = forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Result -> CorePluginPass
go)))
where
go :: Name -> Result -> ModGuts -> CoreM ModGuts
go :: Name -> Result -> CorePluginPass
go Name
name Result
res ModGuts
guts = do
CoreExpr
e <- Result -> CoreM CoreExpr
resultToExpr Result
res
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Name -> CoreExpr -> ModGuts -> ModGuts
updateNameInGuts Name
name CoreExpr
e ModGuts
guts
dcExpr :: TH.Name -> CoreM CoreExpr
dcExpr :: Name -> CoreM CoreExpr
dcExpr Name
thn = do
Name
name <- Name -> CoreM Name
fromTHName Name
thn
DataCon
dc <- forall (m :: * -> *). MonadThings m => Name -> m DataCon
lookupDataCon Name
name
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall b. CoreBndr -> Expr b
Var (DataCon -> CoreBndr
dataConWrapId DataCon
dc)
resultToExpr :: Result -> CoreM CoreExpr
resultToExpr :: Result -> CoreM CoreExpr
resultToExpr (Success String
s) = forall b. Expr b -> Expr b -> Expr b
App forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> CoreM CoreExpr
dcExpr 'Success forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). MonadThings m => String -> m CoreExpr
mkStringExpr String
s
resultToExpr (Failure String
s) = forall b. Expr b -> Expr b -> Expr b
App forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> CoreM CoreExpr
dcExpr 'Failure forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). MonadThings m => String -> m CoreExpr
mkStringExpr String
s
proofPass :: UponFailure -> ReportingMode -> ModGuts -> CoreM ModGuts
proofPass :: UponFailure -> ReportingMode -> CorePluginPass
proofPass UponFailure
upon_failure ReportingMode
report ModGuts
guts = do
case UponFailure
upon_failure of
UponFailure
SkipO0 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ModGuts
guts
UponFailure
_ -> do
let (ModGuts
guts', [(ResultTarget, Obligation)]
obligations) = ModGuts -> (ModGuts, [(ResultTarget, Obligation)])
extractObligations ModGuts
guts
(Updates
toStore, Stats
stats) <- (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
`bimap` forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith forall a. Num a => a -> a -> a
(+)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [(a, b)] -> ([a], [b])
unzip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ReportingMode
-> ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats)
checkObligation ReportingMode
report ModGuts
guts') [(ResultTarget, Obligation)]
obligations
let n :: Int
n = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum Stats
stats :: Int
ModGuts
guts'' <- Updates -> CorePluginPass
storeResults Updates
toStore ModGuts
guts'
let q :: Stat -> Int
q :: Stat -> Int
q Stat
s = forall a. a -> Maybe a -> a
fromMaybe Int
0 forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Stat
s Stats
stats
let summary_message :: SDoc
summary_message = Int -> SDoc -> SDoc
nest Int
2 forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ Int -> SDoc -> SDoc
nest Int
2 (Stat -> SDoc
desc Stat
s) SDoc -> SDoc -> SDoc
Outputable.<> SDoc
colon SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (Stat -> Int
q Stat
s)
| Stat
s <- [forall a. Bounded a => a
minBound..forall a. Bounded a => a
maxBound], Stat -> Int
q Stat
s forall a. Ord a => a -> a -> Bool
> Int
0 ]
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Stat -> Int
q Stat
StoredResult forall a. Eq a => a -> a -> Bool
== Int
n) forall a b. (a -> b) -> a -> b
$ do
if Stat -> Int
q Stat
ExpSuccess forall a. Num a => a -> a -> a
+ Stat -> Int
q Stat
ExpFailure forall a. Num a => a -> a -> a
+ Stat -> Int
q Stat
StoredResult forall a. Eq a => a -> a -> Bool
== Int
n
then forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ReportingMode
report forall a. Eq a => a -> a -> Bool
== ReportingMode
Quiet) forall a b. (a -> b) -> a -> b
$
SDoc -> CoreM ()
putMsg forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"inspection testing successful" SDoc -> SDoc -> SDoc
$$ SDoc
summary_message
else do
SDoc -> CoreM ()
errorMsg forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"inspection testing unsuccessful" SDoc -> SDoc -> SDoc
$$ SDoc
summary_message
case UponFailure
upon_failure of
UponFailure
KeepGoing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
UponFailure
_ -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IO a
exitFailure
forall (m :: * -> *) a. Monad m => a -> m a
return ModGuts
guts''
desc :: Stat -> SDoc
desc :: Stat -> SDoc
desc Stat
ExpSuccess = String -> SDoc
text String
" expected successes"
desc Stat
UnexpSuccess = String -> SDoc
text String
"unexpected successes"
desc Stat
ExpFailure = String -> SDoc
text String
" expected failures"
desc Stat
UnexpFailure = String -> SDoc
text String
" unexpected failures"
desc Stat
StoredResult = String -> SDoc
text String
" results stored"
partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b])
partitionMaybe :: forall a b. (a -> Maybe b) -> [a] -> ([a], [b])
partitionMaybe a -> Maybe b
f = forall a b. [Either a b] -> ([a], [b])
partitionEithers forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\a
x -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a b. a -> Either a b
Left a
x) forall a b. b -> Either a b
Right (a -> Maybe b
f a
x))
myPrettySrcLoc :: TH.Loc -> String
myPrettySrcLoc :: Loc -> String
myPrettySrcLoc TH.Loc {String
CharPos
loc_end :: Loc -> CharPos
loc_filename :: Loc -> String
loc_module :: Loc -> String
loc_package :: Loc -> String
loc_start :: Loc -> CharPos
loc_end :: CharPos
loc_start :: CharPos
loc_module :: String
loc_package :: String
loc_filename :: String
..}
= forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. [a] -> [a] -> [a]
(++) String
""
[ String
loc_filename, String
":"
, forall a. Show a => a -> String
show (forall a b. (a, b) -> a
fst CharPos
loc_start), String
":"
, forall a. Show a => a -> String
show (forall a b. (a, b) -> b
snd CharPos
loc_start)
]