-- | 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 :: [String] -> IO PluginRecompile
pluginRecompile = \[String]
_args -> forall (f :: * -> *) a. Applicative f => a -> f a
pure PluginRecompile
NoForceRecompile
#endif
    }

data UponFailure = AbortCompilation | KeepGoingO0 | SkipO0 | KeepGoing deriving UponFailure -> UponFailure -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UponFailure -> UponFailure -> Bool
$c/= :: UponFailure -> UponFailure -> Bool
== :: UponFailure -> UponFailure -> Bool
$c== :: UponFailure -> UponFailure -> Bool
Eq

data ReportingMode = Verbose | Quiet deriving ReportingMode -> ReportingMode -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ReportingMode -> ReportingMode -> Bool
$c/= :: ReportingMode -> ReportingMode -> Bool
== :: ReportingMode -> ReportingMode -> Bool
$c== :: ReportingMode -> ReportingMode -> Bool
Eq

data ResultTarget = PrintAndAbort | StoreAt Name

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

extractObligations :: ModGuts -> (ModGuts, [(ResultTarget, Obligation)])
extractObligations :: ModGuts -> (ModGuts, [(ResultTarget, Obligation)])
extractObligations ModGuts
guts = (ModGuts
guts', [(ResultTarget, Obligation)]
obligations)
  where
    ([Annotation]
anns_clean, [(ResultTarget, Obligation)]
obligations) = forall a b. (a -> Maybe b) -> [a] -> ([a], [b])
partitionMaybe Annotation -> Maybe (ResultTarget, Obligation)
findObligationAnn (ModGuts -> [Annotation]
mg_anns ModGuts
guts)
    guts' :: ModGuts
guts' = ModGuts
guts { mg_anns :: [Annotation]
mg_anns = [Annotation]
anns_clean }

findObligationAnn :: Annotation -> Maybe (ResultTarget, Obligation)
findObligationAnn :: Annotation -> Maybe (ResultTarget, Obligation)
findObligationAnn (Annotation (ModuleTarget Module
_) AnnPayload
payload)
    | Just Obligation
obl <- forall a. Typeable a => ([Word8] -> a) -> AnnPayload -> Maybe a
fromSerialized forall a. Data a => [Word8] -> a
deserializeWithData AnnPayload
payload
    = forall a. a -> Maybe a
Just (ResultTarget
PrintAndAbort, Obligation
obl)
findObligationAnn (Annotation (NamedTarget Name
n) AnnPayload
payload)
    | Just Obligation
obl <- forall a. Typeable a => ([Word8] -> a) -> AnnPayload -> Maybe a
fromSerialized forall a. Data a => [Word8] -> a
deserializeWithData AnnPayload
payload
    = forall a. a -> Maybe a
Just (Name -> ResultTarget
StoreAt Name
n, Obligation
obl)
findObligationAnn Annotation
_
    = forall a. Maybe a
Nothing

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

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

-- | 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 (forall unit. GenModule unit -> ModuleName
moduleName Module
mod) forall a. Eq a => a -> a -> Bool
== ModName -> String
TH.modString ModName
m = OccName -> String
TH.occString OccName
occ
showTHName Module
mod (TH.Name OccName
occ (TH.NameG NameSpace
_ PkgName
_ ModName
m))
    | ModuleName -> String
moduleNameString (forall unit. GenModule unit -> ModuleName
moduleName Module
mod) forall a. Eq a => a -> a -> Bool
== ModName -> String
TH.modString ModName
m = OccName -> String
TH.occString OccName
occ
showTHName Module
_ Name
n = forall a. Show a => a -> String
show Name
n

data Stat = ExpSuccess | ExpFailure | UnexpSuccess | UnexpFailure | StoredResult
    deriving (Int -> Stat
Stat -> Int
Stat -> [Stat]
Stat -> Stat
Stat -> Stat -> [Stat]
Stat -> Stat -> Stat -> [Stat]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Stat -> Stat -> Stat -> [Stat]
$cenumFromThenTo :: Stat -> Stat -> Stat -> [Stat]
enumFromTo :: Stat -> Stat -> [Stat]
$cenumFromTo :: Stat -> Stat -> [Stat]
enumFromThen :: Stat -> Stat -> [Stat]
$cenumFromThen :: Stat -> Stat -> [Stat]
enumFrom :: Stat -> [Stat]
$cenumFrom :: Stat -> [Stat]
fromEnum :: Stat -> Int
$cfromEnum :: Stat -> Int
toEnum :: Int -> Stat
$ctoEnum :: Int -> Stat
pred :: Stat -> Stat
$cpred :: Stat -> Stat
succ :: Stat -> Stat
$csucc :: Stat -> Stat
Enum, Stat -> Stat -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Stat -> Stat -> Bool
$c/= :: Stat -> Stat -> Bool
== :: Stat -> Stat -> Bool
$c== :: Stat -> Stat -> Bool
Eq, Eq Stat
Stat -> Stat -> Bool
Stat -> Stat -> Ordering
Stat -> Stat -> Stat
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Stat -> Stat -> Stat
$cmin :: Stat -> Stat -> Stat
max :: Stat -> Stat -> Stat
$cmax :: Stat -> Stat -> Stat
>= :: Stat -> Stat -> Bool
$c>= :: Stat -> Stat -> Bool
> :: Stat -> Stat -> Bool
$c> :: Stat -> Stat -> Bool
<= :: Stat -> Stat -> Bool
$c<= :: Stat -> Stat -> Bool
< :: Stat -> Stat -> Bool
$c< :: Stat -> Stat -> Bool
compare :: Stat -> Stat -> Ordering
$ccompare :: Stat -> Stat -> Ordering
Ord, Stat
forall a. a -> a -> Bounded a
maxBound :: Stat
$cmaxBound :: Stat
minBound :: Stat
$cminBound :: Stat
Bounded)
type Stats = M.Map Stat Int

type Updates = [(Name, Result)]

tick :: Stat -> Stats
tick :: Stat -> Stats
tick Stat
s = forall k a. k -> a -> Map k a
M.singleton Stat
s Int
1

checkObligation :: ReportingMode -> ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats)
checkObligation :: ReportingMode
-> ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats)
checkObligation ReportingMode
report ModGuts
guts (ResultTarget
reportTarget, Obligation
obl) = do

    CheckResult
res <- ModGuts -> Name -> Property -> CoreM CheckResult
checkProperty ModGuts
guts (Obligation -> Name
target Obligation
obl) (Obligation -> Property
property Obligation
obl)
    case ResultTarget
reportTarget of
        ResultTarget
PrintAndAbort -> do
            Stat
category <- case (CheckResult
res, Obligation -> Bool
expectFail Obligation
obl) of
                -- Property holds
                (CheckResult
ResSuccess, Bool
False) -> do
                    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ReportingMode
report forall a. Eq a => a -> a -> Bool
== ReportingMode
Quiet) forall a b. (a -> b) -> a -> b
$
                        String -> CoreM ()
putMsgS forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
expSuccess
                    forall (m :: * -> *) a. Monad m => a -> m a
return Stat
ExpSuccess
                (CheckResult
ResSuccess, Bool
True) -> do
                    String -> CoreM ()
putMsgS forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
unexpSuccess
                    forall (m :: * -> *) a. Monad m => a -> m a
return Stat
UnexpSuccess
                -- Property holds, with extra message
                (ResSuccessWithMessage SDoc
reportDoc, Bool
False) -> do
                    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ReportingMode
report forall a. Eq a => a -> a -> Bool
== ReportingMode
Quiet) forall a b. (a -> b) -> a -> b
$ do
                        String -> CoreM ()
putMsgS forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
expSuccess
                        SDoc -> CoreM ()
putMsg SDoc
reportDoc
                    forall (m :: * -> *) a. Monad m => a -> m a
return Stat
ExpSuccess
                (ResSuccessWithMessage SDoc
reportDoc, Bool
True) -> do
                    String -> CoreM ()
putMsgS forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
unexpSuccess
                    SDoc -> CoreM ()
putMsg SDoc
reportDoc
                    forall (m :: * -> *) a. Monad m => a -> m a
return Stat
UnexpSuccess
                -- Property does not hold
                (ResFailure SDoc
reportDoc, Bool
False) -> do
                    String -> CoreM ()
putMsgS forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
unexpFailure
                    SDoc -> CoreM ()
putMsg forall a b. (a -> b) -> a -> b
$ SDoc
reportDoc
                    forall (m :: * -> *) a. Monad m => a -> m a
return Stat
UnexpFailure
                (ResFailure SDoc
_, Bool
True) -> do
                    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ReportingMode
report forall a. Eq a => a -> a -> Bool
== ReportingMode
Quiet) forall a b. (a -> b) -> a -> b
$
                        String -> CoreM ()
putMsgS forall a b. (a -> b) -> a -> b
$ Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
expFailure
                    forall (m :: * -> *) a. Monad m => a -> m a
return Stat
ExpFailure
            forall (m :: * -> *) a. Monad m => a -> m a
return ([], Stat -> Stats
tick Stat
category)
        StoreAt Name
name -> do
            DynFlags
dflags <- forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
            let result :: Result
result = case CheckResult
res of
                    CheckResult
ResSuccess -> String -> Result
Success forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> String
showSDoc DynFlags
dflags forall a b. (a -> b) -> a -> b
$
                        String -> SDoc
text (Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
expSuccess)
                    ResSuccessWithMessage SDoc
msg -> String -> Result
Success forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> String
showSDoc DynFlags
dflags forall a b. (a -> b) -> a -> b
$
                        String -> SDoc
text (Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
expSuccess) SDoc -> SDoc -> SDoc
$$
                        SDoc
msg
                    ResFailure SDoc
reportMsg -> String -> Result
Failure forall a b. (a -> b) -> a -> b
$ DynFlags -> SDoc -> String
showSDoc DynFlags
dflags forall a b. (a -> b) -> a -> b
$
                        String -> SDoc
text (Module -> Obligation -> String -> String
prettyObligation (ModGuts -> Module
mg_module ModGuts
guts) Obligation
obl String
unexpFailure) SDoc -> SDoc -> SDoc
$$
                        SDoc
reportMsg
            forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Name
name, Result
result)], Stat -> Stats
tick Stat
StoredResult)

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


data CheckResult
    = ResSuccess
    | ResSuccessWithMessage SDoc
    | ResFailure SDoc

lookupNameInGuts :: ModGuts -> Name -> Maybe (Var, CoreExpr)
lookupNameInGuts :: ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n = forall a. [a] -> Maybe a
listToMaybe
    [ (CoreBndr
v,CoreExpr
e)
    | (CoreBndr
v,CoreExpr
e) <- forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (ModGuts -> CoreProgram
mg_binds ModGuts
guts)
    , forall a. NamedThing a => a -> Name
getName CoreBndr
v forall a. Eq a => a -> a -> Bool
== Name
n
    ]

updateNameInGuts :: Name -> CoreExpr -> ModGuts -> ModGuts
updateNameInGuts :: Name -> CoreExpr -> ModGuts -> ModGuts
updateNameInGuts Name
n CoreExpr
expr ModGuts
guts =
    ModGuts
guts {mg_binds :: CoreProgram
mg_binds = forall a b. (a -> b) -> [a] -> [b]
map (Name -> CoreExpr -> CoreBind -> CoreBind
updateNameInGut Name
n CoreExpr
expr) (ModGuts -> CoreProgram
mg_binds ModGuts
guts) }

updateNameInGut :: Name -> CoreExpr -> CoreBind -> CoreBind
updateNameInGut :: Name -> CoreExpr -> CoreBind -> CoreBind
updateNameInGut Name
n CoreExpr
e (NonRec CoreBndr
v CoreExpr
_) | forall a. NamedThing a => a -> Name
getName CoreBndr
v forall a. Eq a => a -> a -> Bool
== Name
n = forall b. b -> Expr b -> Bind b
NonRec CoreBndr
v CoreExpr
e
updateNameInGut Name
_ CoreExpr
_ CoreBind
bind                          = CoreBind
bind

checkProperty :: ModGuts -> TH.Name -> Property -> CoreM CheckResult
checkProperty :: ModGuts -> Name -> Property -> CoreM CheckResult
checkProperty ModGuts
guts Name
thn1 (EqualTo Name
thn2 Equivalence
ignore_types) = do
    Name
n1 <- Name -> CoreM Name
fromTHName Name
thn1
    Name
n2 <- Name -> CoreM Name
fromTHName Name
thn2

    let p1 :: Maybe (CoreBndr, CoreExpr)
p1 = ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n1
    let p2 :: Maybe (CoreBndr, CoreExpr)
p2 = ModGuts -> Name -> Maybe (CoreBndr, CoreExpr)
lookupNameInGuts ModGuts
guts Name
n2

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

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

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

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

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

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

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

storeResults :: Updates -> ModGuts -> CoreM ModGuts
storeResults :: Updates -> CorePluginPass
storeResults = forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Result -> CorePluginPass
go)))
  where
    go :: Name -> Result -> ModGuts -> CoreM ModGuts
    go :: Name -> Result -> CorePluginPass
go Name
name Result
res ModGuts
guts = do
        CoreExpr
e <- Result -> CoreM CoreExpr
resultToExpr Result
res
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Name -> CoreExpr -> ModGuts -> ModGuts
updateNameInGuts Name
name CoreExpr
e ModGuts
guts

dcExpr :: TH.Name -> CoreM CoreExpr
dcExpr :: Name -> CoreM CoreExpr
dcExpr Name
thn = do
    Name
name <- Name -> CoreM Name
fromTHName Name
thn
    DataCon
dc <- forall (m :: * -> *). MonadThings m => Name -> m DataCon
lookupDataCon Name
name
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall b. CoreBndr -> Expr b
Var (DataCon -> CoreBndr
dataConWrapId DataCon
dc)

resultToExpr :: Result -> CoreM CoreExpr
resultToExpr :: Result -> CoreM CoreExpr
resultToExpr (Success String
s) = forall b. Expr b -> Expr b -> Expr b
App forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> CoreM CoreExpr
dcExpr 'Success forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). MonadThings m => String -> m CoreExpr
mkStringExpr String
s
resultToExpr (Failure String
s) = forall b. Expr b -> Expr b -> Expr b
App forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> CoreM CoreExpr
dcExpr 'Failure forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). MonadThings m => String -> m CoreExpr
mkStringExpr String
s

proofPass :: UponFailure -> ReportingMode -> ModGuts -> CoreM ModGuts
proofPass :: UponFailure -> ReportingMode -> CorePluginPass
proofPass UponFailure
upon_failure ReportingMode
report ModGuts
guts = do
    case UponFailure
upon_failure of
        UponFailure
SkipO0 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ModGuts
guts
        UponFailure
_ -> do
            let (ModGuts
guts', [(ResultTarget, Obligation)]
obligations) = ModGuts -> (ModGuts, [(ResultTarget, Obligation)])
extractObligations ModGuts
guts
            (Updates
toStore, Stats
stats) <- (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
`bimap` forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith forall a. Num a => a -> a -> a
(+)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [(a, b)] -> ([a], [b])
unzip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ReportingMode
-> ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats)
checkObligation ReportingMode
report ModGuts
guts') [(ResultTarget, Obligation)]
obligations
            let n :: Int
n = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum Stats
stats :: Int

            ModGuts
guts'' <- Updates -> CorePluginPass
storeResults Updates
toStore  ModGuts
guts'

            let q :: Stat -> Int
                q :: Stat -> Int
q Stat
s = forall a. a -> Maybe a -> a
fromMaybe Int
0 forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Stat
s Stats
stats

            let summary_message :: SDoc
summary_message = Int -> SDoc -> SDoc
nest Int
2 forall a b. (a -> b) -> a -> b
$
                    [SDoc] -> SDoc
vcat [ Int -> SDoc -> SDoc
nest Int
2 (Stat -> SDoc
desc Stat
s) SDoc -> SDoc -> SDoc
Outputable.<> SDoc
colon SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (Stat -> Int
q Stat
s)
                         | Stat
s <- [forall a. Bounded a => a
minBound..forall a. Bounded a => a
maxBound], Stat -> Int
q Stat
s forall a. Ord a => a -> a -> Bool
> Int
0 ]

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

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


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

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

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