-- | See "Test.Inspection".
--
{-# 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

-- | The plugin. It supports some options:
--
-- * @-fplugin-opt=Test.Inspection.Plugin:keep-going@ to keep building despite failing obligations
-- * @-fplugin-opt=Test.Inspection.Plugin:keep-going-O0@ to keep building despite failing obligations, when optimisations are off
-- * @-fplugin-opt=Test.Inspection.Plugin:skip-O0@ to skip performing inspections when optimisations are off
-- * @-fplugin-opt=Test.Inspection.Plugin:quiet@ to be silent if all obligations are fulfilled
--
-- It makes sense to enable only one of @keep-going@, @keep-going-O0@ and
-- @skip-O0@ at a time. @skip-O0@ is useful when working with GHCi, to suppress
-- inspection failure messages and eliminate the overhead of inspection when
-- loading.


plugin :: Plugin
plugin :: Plugin
plugin = Plugin
defaultPlugin
    { installCoreToDos :: CorePlugin
installCoreToDos = CorePlugin
install
#if __GLASGOW_HASKELL__ >= 806
    , pluginRecompile :: [CommandLineOption] -> IO PluginRecompile
pluginRecompile = \[CommandLineOption]
_args -> PluginRecompile -> IO PluginRecompile
forall (f :: * -> *) a. Applicative f => a -> f a
pure PluginRecompile
NoForceRecompile
#endif
    }

data UponFailure = AbortCompilation | KeepGoingO0 | SkipO0 | KeepGoing deriving UponFailure -> UponFailure -> Bool
(UponFailure -> UponFailure -> Bool)
-> (UponFailure -> UponFailure -> Bool) -> Eq UponFailure
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
(ReportingMode -> ReportingMode -> Bool)
-> (ReportingMode -> ReportingMode -> Bool) -> Eq ReportingMode
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 [CommandLineOption]
args [CoreToDo]
passes = [CoreToDo] -> CoreM [CoreToDo]
forall (m :: * -> *) a. Monad m => a -> m a
return ([CoreToDo] -> CoreM [CoreToDo]) -> [CoreToDo] -> CoreM [CoreToDo]
forall a b. (a -> b) -> a -> b
$ [CoreToDo]
passes [CoreToDo] -> [CoreToDo] -> [CoreToDo]
forall a. [a] -> [a] -> [a]
++ [CoreToDo
pass]
  where
    pass :: CoreToDo
pass = CommandLineOption -> CorePluginPass -> CoreToDo
CoreDoPluginPass CommandLineOption
"Test.Inspection.Plugin" (UponFailure -> ReportingMode -> CorePluginPass
proofPass UponFailure
upon_failure ReportingMode
report)
    upon_failure :: UponFailure
upon_failure | CommandLineOption
"keep-going" CommandLineOption -> [CommandLineOption] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CommandLineOption]
args    = UponFailure
KeepGoing
                 | CommandLineOption
"keep-going-O0" CommandLineOption -> [CommandLineOption] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CommandLineOption]
args = UponFailure
KeepGoingO0
                 | CommandLineOption
"skip-O0" CommandLineOption -> [CommandLineOption] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CommandLineOption]
args       = UponFailure
SkipO0
                 | Bool
otherwise                   = UponFailure
AbortCompilation
    report :: ReportingMode
report | CommandLineOption
"quiet" CommandLineOption -> [CommandLineOption] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CommandLineOption]
args = ReportingMode
Quiet
           | Bool
otherwise           = ReportingMode
Verbose

extractObligations :: ModGuts -> (ModGuts, [(ResultTarget, Obligation)])
extractObligations :: ModGuts -> (ModGuts, [(ResultTarget, Obligation)])
extractObligations ModGuts
guts = (ModGuts
guts', [(ResultTarget, Obligation)]
obligations)
  where
    ([Annotation]
anns_clean, [(ResultTarget, Obligation)]
obligations) = (Annotation -> Maybe (ResultTarget, Obligation))
-> [Annotation] -> ([Annotation], [(ResultTarget, Obligation)])
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 <- ([Word8] -> Obligation) -> AnnPayload -> Maybe Obligation
forall a. Typeable a => ([Word8] -> a) -> AnnPayload -> Maybe a
fromSerialized [Word8] -> Obligation
forall a. Data a => [Word8] -> a
deserializeWithData AnnPayload
payload
    = (ResultTarget, Obligation) -> Maybe (ResultTarget, Obligation)
forall a. a -> Maybe a
Just (ResultTarget
PrintAndAbort, Obligation
obl)
findObligationAnn (Annotation (NamedTarget Name
n) AnnPayload
payload)
    | Just Obligation
obl <- ([Word8] -> Obligation) -> AnnPayload -> Maybe Obligation
forall a. Typeable a => ([Word8] -> a) -> AnnPayload -> Maybe a
fromSerialized [Word8] -> Obligation
forall a. Data a => [Word8] -> a
deserializeWithData AnnPayload
payload
    = (ResultTarget, Obligation) -> Maybe (ResultTarget, Obligation)
forall a. a -> Maybe a
Just (Name -> ResultTarget
StoreAt Name
n, Obligation
obl)
findObligationAnn Annotation
_
    = Maybe (ResultTarget, Obligation)
forall a. Maybe a
Nothing

prettyObligation :: Module -> Obligation -> String -> String
prettyObligation :: Module -> Obligation -> CommandLineOption -> CommandLineOption
prettyObligation Module
mod (Obligation {Bool
Maybe CommandLineOption
Maybe Loc
Name
Property
storeResult :: Obligation -> Maybe CommandLineOption
srcLoc :: Obligation -> Maybe Loc
expectFail :: Obligation -> Bool
testName :: Obligation -> Maybe CommandLineOption
property :: Obligation -> Property
target :: Obligation -> Name
storeResult :: Maybe CommandLineOption
srcLoc :: Maybe Loc
expectFail :: Bool
testName :: Maybe CommandLineOption
property :: Property
target :: Name
..}) CommandLineOption
result =
    CommandLineOption
-> (Loc -> CommandLineOption) -> Maybe Loc -> CommandLineOption
forall b a. b -> (a -> b) -> Maybe a -> b
maybe CommandLineOption
"" Loc -> CommandLineOption
myPrettySrcLoc Maybe Loc
srcLoc CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
": " CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
name CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
" " CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
result
  where
    name :: CommandLineOption
name = case Maybe CommandLineOption
testName of
        Just CommandLineOption
n -> CommandLineOption
n
        Maybe CommandLineOption
Nothing -> (Name -> CommandLineOption)
-> Name -> Property -> CommandLineOption
prettyProperty (Module -> Name -> CommandLineOption
showTHName Module
mod) Name
target Property
property

prettyProperty :: (TH.Name -> String) -> TH.Name -> Property -> String
prettyProperty :: (Name -> CommandLineOption)
-> Name -> Property -> CommandLineOption
prettyProperty Name -> CommandLineOption
showName Name
target = \case
  EqualTo Name
n2 Equivalence
eqv   -> Name -> CommandLineOption
showName Name
target CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
" " CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ Equivalence -> CommandLineOption
showEquiv Equivalence
eqv CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
" " CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ Name -> CommandLineOption
showName Name
n2
  NoTypes [Name
t]      -> Name -> CommandLineOption
showName Name
target CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
" `hasNoType` " CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ Name -> CommandLineOption
showName Name
t
  NoTypes [Name]
ts       -> Name -> CommandLineOption
showName Name
target CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
" mentions none of " CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption -> [CommandLineOption] -> CommandLineOption
forall a. [a] -> [[a]] -> [a]
intercalate CommandLineOption
", " ((Name -> CommandLineOption) -> [Name] -> [CommandLineOption]
forall a b. (a -> b) -> [a] -> [b]
map Name -> CommandLineOption
showName [Name]
ts)
  Property
NoAllocation     -> Name -> CommandLineOption
showName Name
target CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
" does not allocate"
  NoTypeClasses [] -> Name -> CommandLineOption
showName Name
target CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
" does not contain dictionary values"
  NoTypeClasses [Name]
ts -> Name -> CommandLineOption
showName Name
target CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
" does not contain dictionary values except of " CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption -> [CommandLineOption] -> CommandLineOption
forall a. [a] -> [[a]] -> [a]
intercalate CommandLineOption
", " ((Name -> CommandLineOption) -> [Name] -> [CommandLineOption]
forall a b. (a -> b) -> [a] -> [b]
map Name -> CommandLineOption
showName [Name]
ts)
  NoUseOf [Name]
ns       -> Name -> CommandLineOption
showName Name
target CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
" uses none of " CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption -> [CommandLineOption] -> CommandLineOption
forall a. [a] -> [[a]] -> [a]
intercalate CommandLineOption
", " ((Name -> CommandLineOption) -> [Name] -> [CommandLineOption]
forall a b. (a -> b) -> [a] -> [b]
map Name -> CommandLineOption
showName [Name]
ns)
  Property
CoreOf           -> Name -> CommandLineOption
showName Name
target CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ CommandLineOption
" core dump" -- :)
  where
    showEquiv :: Equivalence -> CommandLineOption
showEquiv Equivalence
StrictEquiv              = CommandLineOption
"==="
    showEquiv Equivalence
IgnoreTypesAndTicksEquiv = CommandLineOption
"==-"
    showEquiv Equivalence
UnorderedLetsEquiv       = CommandLineOption
"==~"

-- | Like show, but omit the module name if it is he current module
showTHName :: Module -> TH.Name -> String
showTHName :: Module -> Name -> CommandLineOption
showTHName Module
mod (TH.Name OccName
occ (TH.NameQ ModName
m))
    | ModuleName -> CommandLineOption
moduleNameString (Module -> ModuleName
moduleName Module
mod) CommandLineOption -> CommandLineOption -> Bool
forall a. Eq a => a -> a -> Bool
== ModName -> CommandLineOption
TH.modString ModName
m = OccName -> CommandLineOption
TH.occString OccName
occ
showTHName Module
mod (TH.Name OccName
occ (TH.NameG NameSpace
_ PkgName
_ ModName
m))
    | ModuleName -> CommandLineOption
moduleNameString (Module -> ModuleName
moduleName Module
mod) CommandLineOption -> CommandLineOption -> Bool
forall a. Eq a => a -> a -> Bool
== ModName -> CommandLineOption
TH.modString ModName
m = OccName -> CommandLineOption
TH.occString OccName
occ
showTHName Module
_ Name
n = Name -> CommandLineOption
forall a. Show a => a -> CommandLineOption
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]
(Stat -> Stat)
-> (Stat -> Stat)
-> (Int -> Stat)
-> (Stat -> Int)
-> (Stat -> [Stat])
-> (Stat -> Stat -> [Stat])
-> (Stat -> Stat -> [Stat])
-> (Stat -> Stat -> Stat -> [Stat])
-> Enum 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
(Stat -> Stat -> Bool) -> (Stat -> Stat -> Bool) -> Eq Stat
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
Eq Stat
-> (Stat -> Stat -> Ordering)
-> (Stat -> Stat -> Bool)
-> (Stat -> Stat -> Bool)
-> (Stat -> Stat -> Bool)
-> (Stat -> Stat -> Bool)
-> (Stat -> Stat -> Stat)
-> (Stat -> Stat -> Stat)
-> Ord 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
$cp1Ord :: Eq Stat
Ord, Stat
Stat -> Stat -> Bounded 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 = Stat -> Int -> Stats
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
                -- Property holds
                (CheckResult
ResSuccess, Bool
False) -> do
                    Bool -> CoreM () -> CoreM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ReportingMode
report ReportingMode -> ReportingMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReportingMode
Quiet) (CoreM () -> CoreM ()) -> CoreM () -> CoreM ()
forall a b. (a -> b) -> a -> b
$
                        CommandLineOption -> CoreM ()
putMsgS (CommandLineOption -> CoreM ()) -> CommandLineOption -> CoreM ()
forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> CommandLineOption -> CommandLineOption
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl CommandLineOption
expSuccess
                    Stat -> CoreM Stat
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
ExpSuccess
                (CheckResult
ResSuccess, Bool
True) -> do
                    CommandLineOption -> CoreM ()
putMsgS (CommandLineOption -> CoreM ()) -> CommandLineOption -> CoreM ()
forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> CommandLineOption -> CommandLineOption
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl CommandLineOption
unexpSuccess
                    Stat -> CoreM Stat
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
UnexpSuccess
                -- Property holds, with extra message
                (ResSuccessWithMessage SDoc
reportDoc, Bool
False) -> do
                    Bool -> CoreM () -> CoreM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ReportingMode
report ReportingMode -> ReportingMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReportingMode
Quiet) (CoreM () -> CoreM ()) -> CoreM () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ do
                        CommandLineOption -> CoreM ()
putMsgS (CommandLineOption -> CoreM ()) -> CommandLineOption -> CoreM ()
forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> CommandLineOption -> CommandLineOption
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl CommandLineOption
expSuccess
                        SDoc -> CoreM ()
putMsg SDoc
reportDoc
                    Stat -> CoreM Stat
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
ExpSuccess
                (ResSuccessWithMessage SDoc
reportDoc, Bool
True) -> do
                    CommandLineOption -> CoreM ()
putMsgS (CommandLineOption -> CoreM ()) -> CommandLineOption -> CoreM ()
forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> CommandLineOption -> CommandLineOption
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl CommandLineOption
unexpSuccess
                    SDoc -> CoreM ()
putMsg SDoc
reportDoc
                    Stat -> CoreM Stat
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
UnexpSuccess
                -- Property does not hold
                (ResFailure SDoc
reportDoc, Bool
False) -> do
                    CommandLineOption -> CoreM ()
putMsgS (CommandLineOption -> CoreM ()) -> CommandLineOption -> CoreM ()
forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> CommandLineOption -> CommandLineOption
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl CommandLineOption
unexpFailure
                    SDoc -> CoreM ()
putMsg (SDoc -> CoreM ()) -> SDoc -> CoreM ()
forall a b. (a -> b) -> a -> b
$ SDoc
reportDoc
                    Stat -> CoreM Stat
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
UnexpFailure
                (ResFailure SDoc
_, Bool
True) -> do
                    Bool -> CoreM () -> CoreM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ReportingMode
report ReportingMode -> ReportingMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReportingMode
Quiet) (CoreM () -> CoreM ()) -> CoreM () -> CoreM ()
forall a b. (a -> b) -> a -> b
$
                        CommandLineOption -> CoreM ()
putMsgS (CommandLineOption -> CoreM ()) -> CommandLineOption -> CoreM ()
forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> CommandLineOption -> CommandLineOption
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl CommandLineOption
expFailure
                    Stat -> CoreM Stat
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
ExpFailure
            (Updates, Stats) -> CoreM (Updates, Stats)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Stat -> Stats
tick Stat
category)
        StoreAt Name
name -> do
            DynFlags
dflags <- CoreM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
            let result :: Result
result = case CheckResult
res of
                    CheckResult
ResSuccess -> CommandLineOption -> Result
Success (CommandLineOption -> Result) -> CommandLineOption -> Result
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> CommandLineOption
showSDoc DynFlags
dflags (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$
                        CommandLineOption -> SDoc
text (Module -> Obligation -> CommandLineOption -> CommandLineOption
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl CommandLineOption
expSuccess)
                    ResSuccessWithMessage SDoc
msg -> CommandLineOption -> Result
Success (CommandLineOption -> Result) -> CommandLineOption -> Result
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> CommandLineOption
showSDoc DynFlags
dflags (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$
                        CommandLineOption -> SDoc
text (Module -> Obligation -> CommandLineOption -> CommandLineOption
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl CommandLineOption
expSuccess) SDoc -> SDoc -> SDoc
$$
                        SDoc
msg
                    ResFailure SDoc
reportMsg -> CommandLineOption -> Result
Failure (CommandLineOption -> Result) -> CommandLineOption -> Result
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> CommandLineOption
showSDoc DynFlags
dflags (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$
                        CommandLineOption -> SDoc
text (Module -> Obligation -> CommandLineOption -> CommandLineOption
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl CommandLineOption
unexpFailure) SDoc -> SDoc -> SDoc
$$
                        SDoc
reportMsg
            (Updates, Stats) -> CoreM (Updates, Stats)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Name
name, Result
result)], Stat -> Stats
tick Stat
StoredResult)

  where
    expSuccess :: CommandLineOption
expSuccess   = CommandLineOption
"passed."
    unexpSuccess :: CommandLineOption
unexpSuccess = CommandLineOption
"passed unexpectedly!"
    unexpFailure :: CommandLineOption
unexpFailure = CommandLineOption
"failed:"
    expFailure :: CommandLineOption
expFailure   = CommandLineOption
"failed expectedly."


data CheckResult
    = ResSuccess
    | ResSuccessWithMessage SDoc
    | ResFailure SDoc

lookupNameInGuts :: ModGuts -> Name -> Maybe (Var, CoreExpr)
lookupNameInGuts :: ModGuts -> Name -> Maybe (Var, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n = [(Var, CoreExpr)] -> Maybe (Var, CoreExpr)
forall a. [a] -> Maybe a
listToMaybe
    [ (Var
v,CoreExpr
e)
    | (Var
v,CoreExpr
e) <- [Bind Var] -> [(Var, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> [Bind Var]
mg_binds ModGuts
guts)
    , Var -> Name
forall a. NamedThing a => a -> Name
getName Var
v Name -> Name -> Bool
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 :: [Bind Var]
mg_binds = (Bind Var -> Bind Var) -> [Bind Var] -> [Bind Var]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> CoreExpr -> Bind Var -> Bind Var
updateNameInGut Name
n CoreExpr
expr) (ModGuts -> [Bind Var]
mg_binds ModGuts
guts) }

updateNameInGut :: Name -> CoreExpr -> CoreBind -> CoreBind
updateNameInGut :: Name -> CoreExpr -> Bind Var -> Bind Var
updateNameInGut Name
n CoreExpr
e (NonRec Var
v CoreExpr
_) | Var -> Name
forall a. NamedThing a => a -> Name
getName Var
v Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n = Var -> CoreExpr -> Bind Var
forall b. b -> Expr b -> Bind b
NonRec Var
v CoreExpr
e
updateNameInGut Name
_ CoreExpr
_ Bind Var
bind                          = Bind Var
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 (Var, CoreExpr)
p1 = ModGuts -> Name -> Maybe (Var, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n1
    let p2 :: Maybe (Var, CoreExpr)
p2 = ModGuts -> Name -> Maybe (Var, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n2

    if | Name
n1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n2
       -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
       -- Ok if one points to another
       | Just (Var
_, Var Var
other) <- Maybe (Var, CoreExpr)
p1, Var -> Name
forall a. NamedThing a => a -> Name
getName Var
other Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n2
       -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
       | Just (Var
_, Var Var
other) <- Maybe (Var, CoreExpr)
p2, Var -> Name
forall a. NamedThing a => a -> Name
getName Var
other Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n1
       -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
       | Just (Var
v1, CoreExpr
_) <- Maybe (Var, CoreExpr)
p1
       , Just (Var
v2, CoreExpr
_) <- Maybe (Var, CoreExpr)
p2
       , let slice1 :: [(Var, CoreExpr)]
slice1 = [(Var, CoreExpr)] -> Var -> [(Var, CoreExpr)]
slice [(Var, CoreExpr)]
binds Var
v1
       , let slice2 :: [(Var, CoreExpr)]
slice2 = [(Var, CoreExpr)] -> Var -> [(Var, CoreExpr)]
slice [(Var, CoreExpr)]
binds Var
v2
       -> if Equivalence -> [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> Bool
eqSlice Equivalence
ignore_types [(Var, CoreExpr)]
slice1 [(Var, CoreExpr)]
slice2
          -- OK if they have the same expression
          then CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
          -- Not ok if the expression differ
          else CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult -> CoreM CheckResult)
-> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
forall a b. (a -> b) -> a -> b
$ [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> SDoc
pprSliceDifference [(Var, CoreExpr)]
slice1 [(Var, CoreExpr)]
slice2
       -- Not ok if both names are bound externally
       | Maybe (Var, CoreExpr)
Nothing <- Maybe (Var, CoreExpr)
p1
       , Maybe (Var, CoreExpr)
Nothing <- Maybe (Var, CoreExpr)
p2
       -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult -> CoreM CheckResult)
-> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
forall a b. (a -> b) -> a -> b
$ Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
n1 SDoc -> SDoc -> SDoc
<+> CommandLineOption -> SDoc
text CommandLineOption
" and " SDoc -> SDoc -> SDoc
<+> Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
n2 SDoc -> SDoc -> SDoc
<+>
                CommandLineOption -> SDoc
text CommandLineOption
"are different external names"
       | Maybe (Var, CoreExpr)
Nothing <- Maybe (Var, CoreExpr)
p1
       -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult -> CoreM CheckResult)
-> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
forall a b. (a -> b) -> a -> b
$ Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
n1 SDoc -> SDoc -> SDoc
<+> CommandLineOption -> SDoc
text CommandLineOption
"is an external name"
       | Maybe (Var, CoreExpr)
Nothing <- Maybe (Var, CoreExpr)
p2
       -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult -> CoreM CheckResult)
-> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
forall a b. (a -> b) -> a -> b
$ Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
n2 SDoc -> SDoc -> SDoc
<+> CommandLineOption -> SDoc
text CommandLineOption
"is an external name"
  where
    binds :: [(Var, CoreExpr)]
binds = [Bind Var] -> [(Var, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> [Bind Var]
mg_binds ModGuts
guts)

checkProperty ModGuts
guts Name
thn (NoUseOf [Name]
thns) = do
    Name
n <- Name -> CoreM Name
fromTHName Name
thn
    [Name]
ns <- (Name -> CoreM Name) -> [Name] -> CoreM [Name]
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 (Var, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n of
        Maybe (Var, CoreExpr)
Nothing -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult -> CoreM CheckResult)
-> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
forall a b. (a -> b) -> a -> b
$ Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
n SDoc -> SDoc -> SDoc
<+> CommandLineOption -> SDoc
text CommandLineOption
"is not a local name"
        Just (Var
v, CoreExpr
_) -> case [(Var, CoreExpr)] -> [Name] -> Maybe (Var, CoreExpr)
freeOfTerm ([(Var, CoreExpr)] -> Var -> [(Var, CoreExpr)]
slice [(Var, CoreExpr)]
binds Var
v) [Name]
ns of
            Just (Var, CoreExpr)
_ -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult -> CoreM CheckResult)
-> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
forall a b. (a -> b) -> a -> b
$ [(Var, CoreExpr)] -> SDoc
pprSlice ([(Var, CoreExpr)] -> Var -> [(Var, CoreExpr)]
slice [(Var, CoreExpr)]
binds Var
v)
            Maybe (Var, CoreExpr)
Nothing -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
  where binds :: [(Var, CoreExpr)]
binds = [Bind Var] -> [(Var, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> [Bind Var]
mg_binds ModGuts
guts)

checkProperty ModGuts
guts Name
thn (NoTypes [Name]
thts) = do
    Name
n <- Name -> CoreM Name
fromTHName Name
thn
    [Name]
ts <- (Name -> CoreM Name) -> [Name] -> CoreM [Name]
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 (Var, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n of
        Maybe (Var, CoreExpr)
Nothing -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult -> CoreM CheckResult)
-> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
forall a b. (a -> b) -> a -> b
$ Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
n SDoc -> SDoc -> SDoc
<+> CommandLineOption -> SDoc
text CommandLineOption
"is not a local name"
        Just (Var
v, CoreExpr
_) -> case [(Var, CoreExpr)] -> [Name] -> Maybe (Var, CoreExpr)
freeOfType ([(Var, CoreExpr)] -> Var -> [(Var, CoreExpr)]
slice [(Var, CoreExpr)]
binds Var
v) [Name]
ts of
            Just (Var, CoreExpr)
_ -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult -> CoreM CheckResult)
-> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
forall a b. (a -> b) -> a -> b
$ [(Var, CoreExpr)] -> SDoc
pprSlice ([(Var, CoreExpr)] -> Var -> [(Var, CoreExpr)]
slice [(Var, CoreExpr)]
binds Var
v)
            Maybe (Var, CoreExpr)
Nothing -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
  where binds :: [(Var, CoreExpr)]
binds = [Bind Var] -> [(Var, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> [Bind Var]
mg_binds ModGuts
guts)

checkProperty ModGuts
guts Name
thn Property
NoAllocation = do
    Name
n <- Name -> CoreM Name
fromTHName Name
thn
    case ModGuts -> Name -> Maybe (Var, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n of
        Maybe (Var, CoreExpr)
Nothing -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult -> CoreM CheckResult)
-> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
forall a b. (a -> b) -> a -> b
$ Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
n SDoc -> SDoc -> SDoc
<+> CommandLineOption -> SDoc
text CommandLineOption
"is not a local name"
        Just (Var
v, CoreExpr
_) -> case [(Var, CoreExpr)] -> Maybe (Var, CoreExpr)
doesNotAllocate ([(Var, CoreExpr)] -> Var -> [(Var, CoreExpr)]
slice [(Var, CoreExpr)]
binds Var
v) of
            Just (Var
v',CoreExpr
e') -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult -> CoreM CheckResult)
-> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
forall a b. (a -> b) -> a -> b
$ Int -> SDoc -> SDoc
nest Int
4 (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v' SDoc -> SDoc -> SDoc
<+> CommandLineOption -> SDoc
text CommandLineOption
"=" SDoc -> SDoc -> SDoc
<+> CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e')
            Maybe (Var, CoreExpr)
Nothing -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
  where binds :: [(Var, CoreExpr)]
binds = [Bind Var] -> [(Var, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> [Bind Var]
mg_binds ModGuts
guts)

checkProperty ModGuts
guts Name
thn (NoTypeClasses [Name]
thts) = do
    Name
n <- Name -> CoreM Name
fromTHName Name
thn
    [Name]
ts <- (Name -> CoreM Name) -> [Name] -> CoreM [Name]
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 (Var, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n of
        Maybe (Var, CoreExpr)
Nothing -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult -> CoreM CheckResult)
-> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
forall a b. (a -> b) -> a -> b
$ Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
n SDoc -> SDoc -> SDoc
<+> CommandLineOption -> SDoc
text CommandLineOption
"is not a local name"
        Just (Var
v, CoreExpr
_) -> case [(Var, CoreExpr)] -> [Name] -> Maybe (Var, CoreExpr, [TyCon])
doesNotContainTypeClasses ([(Var, CoreExpr)] -> Var -> [(Var, CoreExpr)]
slice [(Var, CoreExpr)]
binds Var
v) [Name]
ts of
            Just (Var
v',CoreExpr
e',[TyCon]
tc) -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult -> CoreM CheckResult)
-> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure
                (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
forall a b. (a -> b) -> a -> b
$ Int -> SDoc -> SDoc
nest Int
4 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
                    [ CommandLineOption -> SDoc
text CommandLineOption
"Found type classes: " SDoc -> SDoc -> SDoc
<+> [TyCon] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyCon]
tc
                    , Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v' SDoc -> SDoc -> SDoc
<+> CommandLineOption -> SDoc
text CommandLineOption
"=" SDoc -> SDoc -> SDoc
<+> CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e'
                    ]
            Maybe (Var, CoreExpr, [TyCon])
Nothing -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
  where binds :: [(Var, CoreExpr)]
binds = [Bind Var] -> [(Var, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> [Bind Var]
mg_binds ModGuts
guts)

checkProperty ModGuts
guts Name
thn Property
CoreOf = do
    Name
n <- Name -> CoreM Name
fromTHName Name
thn
    case ModGuts -> Name -> Maybe (Var, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n of
        Maybe (Var, CoreExpr)
Nothing -> CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult -> CoreM CheckResult)
-> (SDoc -> CheckResult) -> SDoc -> CoreM CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> CheckResult
ResFailure (SDoc -> CoreM CheckResult) -> SDoc -> CoreM CheckResult
forall a b. (a -> b) -> a -> b
$ Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
n SDoc -> SDoc -> SDoc
<+> CommandLineOption -> SDoc
text CommandLineOption
"is not a local name"
        Just (Var
v, CoreExpr
_) -> do
            let s :: [(Var, CoreExpr)]
s = [(Var, CoreExpr)] -> Var -> [(Var, CoreExpr)]
slice [(Var, CoreExpr)]
binds Var
v
            CheckResult -> CoreM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult -> CoreM CheckResult)
-> CheckResult -> CoreM CheckResult
forall a b. (a -> b) -> a -> b
$ SDoc -> CheckResult
ResSuccessWithMessage (SDoc -> CheckResult) -> SDoc -> CheckResult
forall a b. (a -> b) -> a -> b
$ Int -> SDoc -> SDoc
nest Int
4 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [(Var, CoreExpr)] -> SDoc
pprSlice [(Var, CoreExpr)]
s
  where binds :: [(Var, CoreExpr)]
binds = [Bind Var] -> [(Var, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> [Bind Var]
mg_binds ModGuts
guts)

fromTHName :: TH.Name -> CoreM Name
fromTHName :: Name -> CoreM Name
fromTHName Name
thn = Name -> CoreM (Maybe Name)
thNameToGhcName Name
thn CoreM (Maybe Name) -> (Maybe Name -> CoreM Name) -> CoreM Name
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe Name
Nothing -> do
        SDoc -> CoreM ()
errorMsg (SDoc -> CoreM ()) -> SDoc -> CoreM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> SDoc
text CommandLineOption
"Could not resolve TH name" SDoc -> SDoc -> SDoc
<+> CommandLineOption -> SDoc
text (Name -> CommandLineOption
forall a. Show a => a -> CommandLineOption
show Name
thn)
        IO Name -> CoreM Name
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Name -> CoreM Name) -> IO Name -> CoreM Name
forall a b. (a -> b) -> a -> b
$ IO Name
forall a. IO a
exitFailure -- kill the compiler. Is there a nicer way?
    Just Name
n -> Name -> CoreM Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n

storeResults :: Updates -> ModGuts -> CoreM ModGuts
storeResults :: Updates -> CorePluginPass
storeResults = (ModGuts -> Updates -> CoreM ModGuts) -> Updates -> CorePluginPass
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((ModGuts -> (Name, Result) -> CoreM ModGuts)
-> ModGuts -> Updates -> CoreM ModGuts
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (((Name, Result) -> CorePluginPass)
-> ModGuts -> (Name, Result) -> CoreM ModGuts
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Name -> Result -> CorePluginPass)
-> (Name, Result) -> CorePluginPass
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
        CorePluginPass
forall (f :: * -> *) a. Applicative f => a -> f a
pure CorePluginPass -> CorePluginPass
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 <- Name -> CoreM DataCon
forall (m :: * -> *). MonadThings m => Name -> m DataCon
lookupDataCon Name
name
    CoreExpr -> CoreM CoreExpr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreExpr -> CoreM CoreExpr) -> CoreExpr -> CoreM CoreExpr
forall a b. (a -> b) -> a -> b
$ Var -> CoreExpr
forall b. Var -> Expr b
Var (DataCon -> Var
dataConWrapId DataCon
dc)

resultToExpr :: Result -> CoreM CoreExpr
resultToExpr :: Result -> CoreM CoreExpr
resultToExpr (Success CommandLineOption
s) = CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App (CoreExpr -> CoreExpr -> CoreExpr)
-> CoreM CoreExpr -> CoreM (CoreExpr -> CoreExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> CoreM CoreExpr
dcExpr 'Success CoreM (CoreExpr -> CoreExpr) -> CoreM CoreExpr -> CoreM CoreExpr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CommandLineOption -> CoreM CoreExpr
forall (m :: * -> *).
MonadThings m =>
CommandLineOption -> m CoreExpr
mkStringExpr CommandLineOption
s
resultToExpr (Failure CommandLineOption
s) = CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App (CoreExpr -> CoreExpr -> CoreExpr)
-> CoreM CoreExpr -> CoreM (CoreExpr -> CoreExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> CoreM CoreExpr
dcExpr 'Failure CoreM (CoreExpr -> CoreExpr) -> CoreM CoreExpr -> CoreM CoreExpr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CommandLineOption -> CoreM CoreExpr
forall (m :: * -> *).
MonadThings m =>
CommandLineOption -> m CoreExpr
mkStringExpr CommandLineOption
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 -> CorePluginPass
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) <- ([Updates] -> Updates
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Updates] -> Updates)
-> ([Stats] -> Stats) -> ([Updates], [Stats]) -> (Updates, Stats)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
`bimap` (Int -> Int -> Int) -> [Stats] -> Stats
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+)) (([Updates], [Stats]) -> (Updates, Stats))
-> ([(Updates, Stats)] -> ([Updates], [Stats]))
-> [(Updates, Stats)]
-> (Updates, Stats)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Updates, Stats)] -> ([Updates], [Stats])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Updates, Stats)] -> (Updates, Stats))
-> CoreM [(Updates, Stats)] -> CoreM (Updates, Stats)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                ((ResultTarget, Obligation) -> CoreM (Updates, Stats))
-> [(ResultTarget, Obligation)] -> CoreM [(Updates, Stats)]
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 = Stats -> Int
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 = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Stat -> Stats -> Maybe Int
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 (SDoc -> SDoc) -> SDoc -> SDoc
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
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Stat -> Int
q Stat
s)
                         | Stat
s <- [Stat
forall a. Bounded a => a
minBound..Stat
forall a. Bounded a => a
maxBound], Stat -> Int
q Stat
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 ]

            -- Only print a message if there are some compile-time results to report
            Bool -> CoreM () -> CoreM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Stat -> Int
q Stat
StoredResult Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n) (CoreM () -> CoreM ()) -> CoreM () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ do
                if Stat -> Int
q Stat
ExpSuccess Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Stat -> Int
q Stat
ExpFailure Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Stat -> Int
q Stat
StoredResult Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n
                then Bool -> CoreM () -> CoreM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ReportingMode
report ReportingMode -> ReportingMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReportingMode
Quiet) (CoreM () -> CoreM ()) -> CoreM () -> CoreM ()
forall a b. (a -> b) -> a -> b
$
                        SDoc -> CoreM ()
putMsg (SDoc -> CoreM ()) -> SDoc -> CoreM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> SDoc
text CommandLineOption
"inspection testing successful" SDoc -> SDoc -> SDoc
$$ SDoc
summary_message
                else do
                    SDoc -> CoreM ()
errorMsg (SDoc -> CoreM ()) -> SDoc -> CoreM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> SDoc
text CommandLineOption
"inspection testing unsuccessful" SDoc -> SDoc -> SDoc
$$ SDoc
summary_message
                    case UponFailure
upon_failure of
                        UponFailure
KeepGoing           -> () -> CoreM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                        UponFailure
_                   -> IO () -> CoreM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ IO ()
forall a. IO a
exitFailure -- kill the compiler. Is there a nicer way?

            CorePluginPass
forall (m :: * -> *) a. Monad m => a -> m a
return ModGuts
guts''


desc :: Stat -> SDoc
desc :: Stat -> SDoc
desc Stat
ExpSuccess   = CommandLineOption -> SDoc
text CommandLineOption
"  expected successes"
desc Stat
UnexpSuccess = CommandLineOption -> SDoc
text CommandLineOption
"unexpected successes"
desc Stat
ExpFailure   = CommandLineOption -> SDoc
text CommandLineOption
"   expected failures"
desc Stat
UnexpFailure = CommandLineOption -> SDoc
text CommandLineOption
" unexpected failures"
desc Stat
StoredResult = CommandLineOption -> SDoc
text CommandLineOption
"      results stored"

partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b])
partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b])
partitionMaybe a -> Maybe b
f = [Either a b] -> ([a], [b])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either a b] -> ([a], [b]))
-> ([a] -> [Either a b]) -> [a] -> ([a], [b])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Either a b) -> [a] -> [Either a b]
forall a b. (a -> b) -> [a] -> [b]
map (\a
x -> Either a b -> (b -> Either a b) -> Maybe b -> Either a b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (a -> Either a b
forall a b. a -> Either a b
Left a
x) b -> Either a b
forall a b. b -> Either a b
Right (a -> Maybe b
f a
x))

-- | like prettySrcLoc, but omits the module name
myPrettySrcLoc :: TH.Loc -> String
myPrettySrcLoc :: Loc -> CommandLineOption
myPrettySrcLoc TH.Loc {CommandLineOption
CharPos
loc_filename :: Loc -> CommandLineOption
loc_package :: Loc -> CommandLineOption
loc_module :: Loc -> CommandLineOption
loc_start :: Loc -> CharPos
loc_end :: Loc -> CharPos
loc_end :: CharPos
loc_start :: CharPos
loc_module :: CommandLineOption
loc_package :: CommandLineOption
loc_filename :: CommandLineOption
..}
  = (CommandLineOption -> CommandLineOption -> CommandLineOption)
-> CommandLineOption -> [CommandLineOption] -> CommandLineOption
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
(++) CommandLineOption
""
      [ CommandLineOption
loc_filename, CommandLineOption
":"
      , Int -> CommandLineOption
forall a. Show a => a -> CommandLineOption
show (CharPos -> Int
forall a b. (a, b) -> a
fst CharPos
loc_start), CommandLineOption
":"
      , Int -> CommandLineOption
forall a. Show a => a -> CommandLineOption
show (CharPos -> Int
forall a b. (a, b) -> b
snd CharPos
loc_start)
      ]