-- | 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 = install
#if __GLASGOW_HASKELL__ >= 806
    , pluginRecompile = \[String]
_args -> PluginRecompile -> IO PluginRecompile
forall a. a -> IO a
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
$c== :: UponFailure -> UponFailure -> Bool
== :: UponFailure -> UponFailure -> Bool
$c/= :: UponFailure -> UponFailure -> Bool
/= :: 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
$c== :: ReportingMode -> ReportingMode -> Bool
== :: ReportingMode -> ReportingMode -> Bool
$c/= :: ReportingMode -> ReportingMode -> Bool
/= :: ReportingMode -> ReportingMode -> Bool
Eq

data ResultTarget = PrintAndAbort | StoreAt Name

install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
install :: [String] -> [CoreToDo] -> CoreM [CoreToDo]
install [String]
args [CoreToDo]
passes = [CoreToDo] -> CoreM [CoreToDo]
forall a. a -> CoreM a
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 = 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" String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
args    = UponFailure
KeepGoing
                 | String
"keep-going-O0" String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
args = UponFailure
KeepGoingO0
                 | String
"skip-O0" String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
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" String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
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)])
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 = 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 -> String -> String
prettyObligation Module
mod (Obligation {Bool
Maybe String
Maybe Loc
Name
Property
target :: Name
property :: Property
testName :: Maybe String
expectFail :: Bool
srcLoc :: Maybe Loc
storeResult :: Maybe String
target :: Obligation -> Name
property :: Obligation -> Property
testName :: Obligation -> Maybe String
expectFail :: Obligation -> Bool
srcLoc :: Obligation -> Maybe Loc
storeResult :: Obligation -> Maybe String
..}) String
result =
    String -> (Loc -> String) -> Maybe Loc -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" Loc -> String
myPrettySrcLoc Maybe Loc
srcLoc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> 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 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Equivalence -> String
showEquiv Equivalence
eqv String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
showName Name
n2
  NoTypes [Name
t]      -> Name -> String
showName Name
target String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" `hasNoType` " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
showName Name
t
  NoTypes [Name]
ts       -> Name -> String
showName Name
target String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" mentions none of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Name -> String
showName [Name]
ts)
  Property
NoAllocation     -> Name -> String
showName Name
target String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" does not allocate"
  NoTypeClasses [] -> Name -> String
showName Name
target String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" does not contain dictionary values"
  NoTypeClasses [Name]
ts -> Name -> String
showName Name
target String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" does not contain dictionary values except of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Name -> String
showName [Name]
ts)
  NoUseOf [Name]
ns       -> Name -> String
showName Name
target String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" uses none of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Name -> String
showName [Name]
ns)
  Property
CoreOf           -> Name -> String
showName Name
target String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" core dump" -- :)
  where
    showEquiv :: Equivalence -> String
showEquiv Equivalence
StrictEquiv              = String
"==="
    showEquiv Equivalence
IgnoreTypesAndTicksEquiv = String
"==-"
    showEquiv Equivalence
UnorderedLetsEquiv       = String
"==~"

-- | Like show, but omit the module name if it is he current module
showTHName :: Module -> TH.Name -> String
showTHName :: Module -> Name -> String
showTHName Module
mod (TH.Name OccName
occ (TH.NameQ ModName
m))
    | ModuleName -> String
moduleNameString (Module -> ModuleName
forall unit. GenModule unit -> ModuleName
moduleName Module
mod) String -> String -> Bool
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 (Module -> ModuleName
forall unit. GenModule unit -> ModuleName
moduleName Module
mod) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== ModName -> String
TH.modString ModName
m = OccName -> String
TH.occString OccName
occ
showTHName Module
_ Name
n = Name -> String
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]
(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
$csucc :: Stat -> Stat
succ :: Stat -> Stat
$cpred :: Stat -> Stat
pred :: Stat -> Stat
$ctoEnum :: Int -> Stat
toEnum :: Int -> Stat
$cfromEnum :: Stat -> Int
fromEnum :: Stat -> Int
$cenumFrom :: Stat -> [Stat]
enumFrom :: Stat -> [Stat]
$cenumFromThen :: Stat -> Stat -> [Stat]
enumFromThen :: Stat -> Stat -> [Stat]
$cenumFromTo :: Stat -> Stat -> [Stat]
enumFromTo :: Stat -> Stat -> [Stat]
$cenumFromThenTo :: Stat -> Stat -> Stat -> [Stat]
enumFromThenTo :: Stat -> Stat -> Stat -> [Stat]
Enum, Stat -> Stat -> Bool
(Stat -> Stat -> Bool) -> (Stat -> Stat -> Bool) -> Eq Stat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Stat -> Stat -> Bool
== :: Stat -> Stat -> Bool
$c/= :: Stat -> Stat -> Bool
/= :: 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
$ccompare :: Stat -> Stat -> Ordering
compare :: Stat -> Stat -> Ordering
$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
>= :: Stat -> Stat -> Bool
$cmax :: Stat -> Stat -> Stat
max :: Stat -> Stat -> Stat
$cmin :: Stat -> Stat -> Stat
min :: Stat -> Stat -> Stat
Ord, Stat
Stat -> Stat -> Bounded Stat
forall a. a -> a -> Bounded a
$cminBound :: Stat
minBound :: Stat
$cmaxBound :: Stat
maxBound :: 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
$
                        String -> CoreM ()
putMsgS (String -> CoreM ()) -> String -> CoreM ()
forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
expSuccess
                    Stat -> CoreM Stat
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
ExpSuccess
                (CheckResult
ResSuccess, Bool
True) -> do
                    String -> CoreM ()
putMsgS (String -> CoreM ()) -> String -> CoreM ()
forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
unexpSuccess
                    Stat -> CoreM Stat
forall a. a -> CoreM a
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
                        String -> CoreM ()
putMsgS (String -> CoreM ()) -> String -> CoreM ()
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
                    Stat -> CoreM Stat
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
ExpSuccess
                (ResSuccessWithMessage SDoc
reportDoc, Bool
True) -> do
                    String -> CoreM ()
putMsgS (String -> CoreM ()) -> String -> CoreM ()
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
                    Stat -> CoreM Stat
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
UnexpSuccess
                -- Property does not hold
                (ResFailure SDoc
reportDoc, Bool
False) -> do
                    String -> CoreM ()
putMsgS (String -> CoreM ()) -> String -> CoreM ()
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 (SDoc -> CoreM ()) -> SDoc -> CoreM ()
forall a b. (a -> b) -> a -> b
$ SDoc
reportDoc
                    Stat -> CoreM Stat
forall a. a -> CoreM a
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
$
                        String -> CoreM ()
putMsgS (String -> CoreM ()) -> String -> CoreM ()
forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
expFailure
                    Stat -> CoreM Stat
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return Stat
ExpFailure
            (Updates, Stats) -> CoreM (Updates, Stats)
forall a. a -> CoreM a
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 -> String -> Result
Success (String -> Result) -> String -> Result
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> String
showSDoc DynFlags
dflags (SDoc -> String) -> SDoc -> String
forall a b. (a -> b) -> a -> b
$
                        String -> SDoc
forall doc. IsLine doc => String -> doc
text (Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
expSuccess)
                    ResSuccessWithMessage SDoc
msg -> String -> Result
Success (String -> Result) -> String -> Result
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> String
showSDoc DynFlags
dflags (SDoc -> String) -> SDoc -> String
forall a b. (a -> b) -> a -> b
$
                        String -> SDoc
forall doc. IsLine doc => String -> doc
text (Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
expSuccess) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
                        SDoc
msg
                    ResFailure SDoc
reportMsg -> String -> Result
Failure (String -> Result) -> String -> Result
forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> String
showSDoc DynFlags
dflags (SDoc -> String) -> SDoc -> String
forall a b. (a -> b) -> a -> b
$
                        String -> SDoc
forall doc. IsLine doc => String -> doc
text (Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
unexpFailure) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
                        SDoc
reportMsg
            (Updates, Stats) -> CoreM (Updates, Stats)
forall a. a -> CoreM a
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 = [(CoreBndr, CoreExpr)] -> Maybe (CoreBndr, CoreExpr)
forall a. [a] -> Maybe a
listToMaybe
    [ (CoreBndr
v,CoreExpr
e)
    | (CoreBndr
v,CoreExpr
e) <- [Bind CoreBndr] -> [(CoreBndr, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> [Bind CoreBndr]
mg_binds ModGuts
guts)
    , CoreBndr -> Name
forall a. NamedThing a => a -> Name
getName CoreBndr
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 = map (updateNameInGut n expr) (mg_binds guts) }

updateNameInGut :: Name -> CoreExpr -> CoreBind -> CoreBind
updateNameInGut :: Name -> CoreExpr -> Bind CoreBndr -> Bind CoreBndr
updateNameInGut Name
n CoreExpr
e (NonRec CoreBndr
v CoreExpr
_) | CoreBndr -> Name
forall a. NamedThing a => a -> Name
getName CoreBndr
v Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n = CoreBndr -> CoreExpr -> Bind CoreBndr
forall b. b -> Expr b -> Bind b
NonRec CoreBndr
v CoreExpr
e
updateNameInGut Name
_ CoreExpr
_ Bind CoreBndr
bind                          = Bind CoreBndr
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n2
       -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
       -- Ok if one points to another
       | Just (CoreBndr
_, Var CoreBndr
other) <- Maybe (CoreBndr, CoreExpr)
p1, CoreBndr -> Name
forall a. NamedThing a => a -> Name
getName CoreBndr
other Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n2
       -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
       | Just (CoreBndr
_, Var CoreBndr
other) <- Maybe (CoreBndr, CoreExpr)
p2, CoreBndr -> Name
forall a. NamedThing a => a -> Name
getName CoreBndr
other Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n1
       -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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
          -- OK if they have the same expression
          then CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
          -- Not ok if the expression differ
          else CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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
$ [(CoreBndr, CoreExpr)] -> [(CoreBndr, CoreExpr)] -> SDoc
pprSliceDifference [(CoreBndr, CoreExpr)]
slice1 [(CoreBndr, CoreExpr)]
slice2
       -- Not ok if both names are bound externally
       | Maybe (CoreBndr, CoreExpr)
Nothing <- Maybe (CoreBndr, CoreExpr)
p1
       , Maybe (CoreBndr, CoreExpr)
Nothing <- Maybe (CoreBndr, CoreExpr)
p2
       -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
" and " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
n2 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+>
                String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"are different external names"
       | Maybe (CoreBndr, CoreExpr)
Nothing <- Maybe (CoreBndr, CoreExpr)
p1
       -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"is an external name"
       | Maybe (CoreBndr, CoreExpr)
Nothing <- Maybe (CoreBndr, CoreExpr)
p2
       -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"is an external name"
  where
    binds :: [(CoreBndr, CoreExpr)]
binds = [Bind CoreBndr] -> [(CoreBndr, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> [Bind CoreBndr]
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Name -> CoreM Name
fromTHName [Name]
thns
    case ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n of
        Maybe (CoreBndr, CoreExpr)
Nothing -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
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)
_ -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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
$ [(CoreBndr, CoreExpr)] -> SDoc
pprSlice ([(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
slice [(CoreBndr, CoreExpr)]
binds CoreBndr
v)
            Maybe (CoreBndr, CoreExpr)
Nothing -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
  where binds :: [(CoreBndr, CoreExpr)]
binds = [Bind CoreBndr] -> [(CoreBndr, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> [Bind CoreBndr]
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Name -> CoreM Name
fromTHName [Name]
thts
    case ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n of
        Maybe (CoreBndr, CoreExpr)
Nothing -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
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)
_ -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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
$ [(CoreBndr, CoreExpr)] -> SDoc
pprSlice ([(CoreBndr, CoreExpr)] -> CoreBndr -> [(CoreBndr, CoreExpr)]
slice [(CoreBndr, CoreExpr)]
binds CoreBndr
v)
            Maybe (CoreBndr, CoreExpr)
Nothing -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
  where binds :: [(CoreBndr, CoreExpr)]
binds = [Bind CoreBndr] -> [(CoreBndr, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> [Bind CoreBndr]
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 -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
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') -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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 (CoreBndr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreBndr
v' SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e')
            Maybe (CoreBndr, CoreExpr)
Nothing -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
  where binds :: [(CoreBndr, CoreExpr)]
binds = [Bind CoreBndr] -> [(CoreBndr, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> [Bind CoreBndr]
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Name -> CoreM Name
fromTHName [Name]
thts
    case ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n of
        Maybe (CoreBndr, CoreExpr)
Nothing -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
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) -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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
forall doc. IsDoc doc => [doc] -> doc
vcat
                    [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Found type classes: " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [TyCon] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyCon]
tc
                    , CoreBndr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreBndr
v' SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e'
                    ]
            Maybe (CoreBndr, CoreExpr, [TyCon])
Nothing -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
ResSuccess
  where binds :: [(CoreBndr, CoreExpr)]
binds = [Bind CoreBndr] -> [(CoreBndr, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> [Bind CoreBndr]
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 -> CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
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
            CheckResult -> CoreM CheckResult
forall a. a -> CoreM a
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
$ [(CoreBndr, CoreExpr)] -> SDoc
pprSlice [(CoreBndr, CoreExpr)]
s
  where binds :: [(CoreBndr, CoreExpr)]
binds = [Bind CoreBndr] -> [(CoreBndr, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> [Bind CoreBndr]
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 a b. CoreM a -> (a -> CoreM b) -> CoreM b
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
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Could not resolve TH name" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text (Name -> String
forall a. Show a => a -> String
show Name
thn)
        IO Name -> CoreM Name
forall a. IO a -> CoreM a
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 a. a -> CoreM a
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 a. a -> CoreM a
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 a. a -> CoreM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreExpr -> CoreM CoreExpr) -> CoreExpr -> CoreM CoreExpr
forall a b. (a -> b) -> a -> b
$ CoreBndr -> CoreExpr
forall b. CoreBndr -> Expr b
Var (DataCon -> CoreBndr
dataConWrapId DataCon
dc)

resultToExpr :: Result -> CoreM CoreExpr
resultToExpr :: Result -> CoreM CoreExpr
resultToExpr (Success String
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 a b. CoreM (a -> b) -> CoreM a -> CoreM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> CoreM CoreExpr
forall (m :: * -> *). MonadThings m => String -> m CoreExpr
mkStringExpr String
s
resultToExpr (Failure String
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 a b. CoreM (a -> b) -> CoreM a -> CoreM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> CoreM CoreExpr
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 -> CorePluginPass
forall a. a -> CoreM a
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 a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ReportingMode
-> ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats)
checkObligation ReportingMode
report ModGuts
guts') [(ResultTarget, Obligation)]
obligations
            let n :: Int
n = Stats -> Int
forall a. Num a => Map Stat a -> a
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
forall doc. IsDoc doc => [doc] -> doc
vcat [ Int -> SDoc -> SDoc
nest Int
2 (Stat -> SDoc
desc Stat
s) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
Outputable.<> SDoc
forall doc. IsLine doc => doc
colon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> 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
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"inspection testing successful" SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ SDoc
summary_message
                else do
                    SDoc -> CoreM ()
errorMsg (SDoc -> CoreM ()) -> SDoc -> CoreM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"inspection testing unsuccessful" SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ SDoc
summary_message
                    case UponFailure
upon_failure of
                        UponFailure
KeepGoing           -> () -> CoreM ()
forall a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                        UponFailure
_                   -> IO () -> CoreM ()
forall a. IO a -> CoreM a
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 a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return ModGuts
guts''


desc :: Stat -> SDoc
desc :: Stat -> SDoc
desc Stat
ExpSuccess   = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"  expected successes"
desc Stat
UnexpSuccess = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"unexpected successes"
desc Stat
ExpFailure   = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"   expected failures"
desc Stat
UnexpFailure = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
" unexpected failures"
desc Stat
StoredResult = String -> SDoc
forall doc. IsLine doc => String -> doc
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 = [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 -> String
myPrettySrcLoc TH.Loc {String
CharPos
loc_filename :: String
loc_package :: String
loc_module :: String
loc_start :: CharPos
loc_end :: CharPos
loc_filename :: Loc -> String
loc_package :: Loc -> String
loc_module :: Loc -> String
loc_start :: Loc -> CharPos
loc_end :: Loc -> CharPos
..}
  = (String -> String -> String) -> String -> [String] -> String
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> String -> String
forall a. [a] -> [a] -> [a]
(++) String
""
      [ String
loc_filename, String
":"
      , Int -> String
forall a. Show a => a -> String
show (CharPos -> Int
forall a b. (a, b) -> a
fst CharPos
loc_start), String
":"
      , Int -> String
forall a. Show a => a -> String
show (CharPos -> Int
forall a b. (a, b) -> b
snd CharPos
loc_start)
      ]