-- |
-- Description : Inspection Testing for Haskell
-- Copyright   : (c) Joachim Breitner, 2017
-- License     : MIT
-- Maintainer  : mail@joachim-breitner.de
-- Portability : GHC specifc
--
-- This module supports the accompanying GHC plugin "Test.Inspection.Plugin" and adds
-- to GHC the ability to do inspection testing.

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE CPP #-}
module Test.Inspection (
    -- * Synopsis
    -- $synopsis

    -- * Registering obligations
    inspect,
    inspectTest,
    Result(..),
    -- * Defining obligations
    Obligation(..), mkObligation, Equivalence (..), Property(..),
    -- * Convenience functions
    -- $convenience
    (===), (==-), (=/=), (=/-), (==~), (=/~),
    hasNoType, hasNoGenerics,
    hasNoTypeClasses, hasNoTypeClassesExcept,
    doesNotUse, coreOf,
) where

import Language.Haskell.TH
import Language.Haskell.TH.Syntax (Quasi(qNewName), liftData, addTopDecls)
#if MIN_VERSION_GLASGOW_HASKELL(8,4,0,0)
import Language.Haskell.TH.Syntax (addCorePlugin)
#endif
import Data.Data
import Data.Maybe
import GHC.Exts (lazy)
import GHC.Generics (V1(), U1(), M1(), K1(), (:+:), (:*:), (:.:), Rec1, Par1)

{- $synopsis

To use inspection testing, you need to

 1. enable the @TemplateHaskell@ language extension
 2. declare your proof obligations using 'inspect' or 'inspectTest'

An example module is

@
{-\# LANGUAGE TemplateHaskell \#-}
module Simple where

import Test.Inspection
import Data.Maybe

lhs, rhs :: (a -> b) -> Maybe a -> Bool
lhs f x = isNothing (fmap f x)
rhs f Nothing = True
rhs f (Just _) = False

inspect $ 'lhs === 'rhs
@

On GHC < 8.4, you have to explicitly load the plugin:
@
{&#45;\# OPTIONS_GHC -fplugin=Test.Inspection.Plugin \#&#45;}
@
-}

-- Description of test obligations

-- | This data type describes an inspection testing obligation.
--
-- It is recommended to build it using 'mkObligation', for backwards
-- compatibility when new fields are added. You can also use the more
-- mnemonic convenience functions like '(===)' or 'hasNoType'.
--
-- The obligation needs to be passed to 'inspect' or 'inspectTest'.
--
-- @since 0.1
data Obligation = Obligation
    { Obligation -> Name
target      :: Name
        -- ^ The target of a test obligation; invariably the name of a local
        -- definition. To get the name of a function @foo@, write @'foo@. This requires
        -- @{&#45;\# LANGUAGE TemplateHaskell \#&#45;}@.
    , Obligation -> Property
property    :: Property
        -- ^ The property of the target to be checked.
    , Obligation -> Maybe String
testName :: Maybe String
        -- ^ An optional name for the test
    , Obligation -> Bool
expectFail  :: Bool
        -- ^ Do we expect this property to fail?
        -- (Only used by 'inspect', not by 'inspectTest')
    , Obligation -> Maybe Loc
srcLoc :: Maybe Loc
        -- ^ The source location where this obligation is defined.
        -- This is filled in by 'inspect'.
    , Obligation -> Maybe String
storeResult :: Maybe String
        -- ^ If this is 'Nothing', then report errors during compilation.
        -- Otherwise, update the top-level definition with this name.
        --
        -- @since 0.2
    }
    deriving Typeable Obligation
Typeable Obligation =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Obligation -> c Obligation)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Obligation)
-> (Obligation -> Constr)
-> (Obligation -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Obligation))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c Obligation))
-> ((forall b. Data b => b -> b) -> Obligation -> Obligation)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Obligation -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Obligation -> r)
-> (forall u. (forall d. Data d => d -> u) -> Obligation -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Obligation -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Obligation -> m Obligation)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Obligation -> m Obligation)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Obligation -> m Obligation)
-> Data Obligation
Obligation -> Constr
Obligation -> DataType
(forall b. Data b => b -> b) -> Obligation -> Obligation
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Obligation -> u
forall u. (forall d. Data d => d -> u) -> Obligation -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Obligation -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Obligation -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Obligation -> m Obligation
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Obligation -> m Obligation
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Obligation
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Obligation -> c Obligation
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Obligation)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Obligation)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Obligation -> c Obligation
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Obligation -> c Obligation
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Obligation
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Obligation
$ctoConstr :: Obligation -> Constr
toConstr :: Obligation -> Constr
$cdataTypeOf :: Obligation -> DataType
dataTypeOf :: Obligation -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Obligation)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Obligation)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Obligation)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Obligation)
$cgmapT :: (forall b. Data b => b -> b) -> Obligation -> Obligation
gmapT :: (forall b. Data b => b -> b) -> Obligation -> Obligation
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Obligation -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Obligation -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Obligation -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Obligation -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Obligation -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Obligation -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Obligation -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Obligation -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Obligation -> m Obligation
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Obligation -> m Obligation
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Obligation -> m Obligation
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Obligation -> m Obligation
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Obligation -> m Obligation
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Obligation -> m Obligation
Data

-- | Properties of the obligation target to be checked.
--
-- @since 0.1
data Property
    -- | Are the two functions equal?
    --
    -- More precisely: @f@ is equal to @g@ if either the definition of @f@ is
    -- @f = g@, or the definition of @g@ is @g = f@, or if the definitions are
    -- @f = e@ and @g = e@.
    --
    -- In general @f@ and @g@ need to be defined in this module, so that their
    -- actual defintions can be inspected.
    --
    -- The `Equivalence` indicates how strict to check for equality
    = EqualTo Name Equivalence

    -- | Do none of these types appear anywhere in the definition of the function
    -- (neither locally bound nor passed as arguments)
    --
    -- @since 0.3
    | NoTypes [Name]

    -- | Does this function perform no heap allocations.
    | NoAllocation

    -- | Does this value contain dictionaries (/except/ of the listed classes).
    --
    -- @since 0.3
    | NoTypeClasses [Name]

    -- | Does not contain this value (in terms or patterns)
    --
    -- @since 0.4.1
    | NoUseOf [Name]

    -- | Always satisfied, but dumps the value in non-quiet mode.
    --
    -- @since 0.4.2
    | CoreOf
    deriving Typeable Property
Typeable Property =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Property -> c Property)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Property)
-> (Property -> Constr)
-> (Property -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Property))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Property))
-> ((forall b. Data b => b -> b) -> Property -> Property)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Property -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Property -> r)
-> (forall u. (forall d. Data d => d -> u) -> Property -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Property -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Property -> m Property)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Property -> m Property)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Property -> m Property)
-> Data Property
Property -> Constr
Property -> DataType
(forall b. Data b => b -> b) -> Property -> Property
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Property -> u
forall u. (forall d. Data d => d -> u) -> Property -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Property -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Property -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Property -> m Property
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Property -> m Property
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Property
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Property -> c Property
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Property)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Property)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Property -> c Property
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Property -> c Property
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Property
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Property
$ctoConstr :: Property -> Constr
toConstr :: Property -> Constr
$cdataTypeOf :: Property -> DataType
dataTypeOf :: Property -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Property)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Property)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Property)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Property)
$cgmapT :: (forall b. Data b => b -> b) -> Property -> Property
gmapT :: (forall b. Data b => b -> b) -> Property -> Property
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Property -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Property -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Property -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Property -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Property -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Property -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Property -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Property -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Property -> m Property
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Property -> m Property
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Property -> m Property
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Property -> m Property
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Property -> m Property
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Property -> m Property
Data

-- | Equivalence of terms.
--
-- @since 0.5
data Equivalence
    = StrictEquiv               -- ^ strict term equality
    | IgnoreTypesAndTicksEquiv  -- ^ ignore types and hpc ticks during the comparison
    | UnorderedLetsEquiv        -- ^ allow permuted let bindings, ignore types and hpc tick during comparison
    deriving Typeable Equivalence
Typeable Equivalence =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Equivalence -> c Equivalence)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Equivalence)
-> (Equivalence -> Constr)
-> (Equivalence -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Equivalence))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c Equivalence))
-> ((forall b. Data b => b -> b) -> Equivalence -> Equivalence)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Equivalence -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Equivalence -> r)
-> (forall u. (forall d. Data d => d -> u) -> Equivalence -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Equivalence -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence)
-> Data Equivalence
Equivalence -> Constr
Equivalence -> DataType
(forall b. Data b => b -> b) -> Equivalence -> Equivalence
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Equivalence -> u
forall u. (forall d. Data d => d -> u) -> Equivalence -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Equivalence -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Equivalence -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Equivalence
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Equivalence -> c Equivalence
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Equivalence)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Equivalence)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Equivalence -> c Equivalence
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Equivalence -> c Equivalence
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Equivalence
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Equivalence
$ctoConstr :: Equivalence -> Constr
toConstr :: Equivalence -> Constr
$cdataTypeOf :: Equivalence -> DataType
dataTypeOf :: Equivalence -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Equivalence)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Equivalence)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Equivalence)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Equivalence)
$cgmapT :: (forall b. Data b => b -> b) -> Equivalence -> Equivalence
gmapT :: (forall b. Data b => b -> b) -> Equivalence -> Equivalence
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Equivalence -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Equivalence -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Equivalence -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Equivalence -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Equivalence -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Equivalence -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Equivalence -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Equivalence -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
Data

-- | Creates an inspection obligation for the given function name
-- with default values for the optional fields.
--
-- @since 0.1
mkObligation :: Name -> Property -> Obligation
mkObligation :: Name -> Property -> Obligation
mkObligation Name
target Property
prop = Obligation
    { target :: Name
target = Name
target
    , property :: Property
property = Property
prop
    , testName :: Maybe String
testName = Maybe String
forall a. Maybe a
Nothing
    , srcLoc :: Maybe Loc
srcLoc = Maybe Loc
forall a. Maybe a
Nothing
    , expectFail :: Bool
expectFail = Bool
False
    , storeResult :: Maybe String
storeResult = Maybe String
forall a. Maybe a
Nothing
    }

{- $convenience

These convenience functions create common test obligations directly.
-}

-- | Declare two functions to be equal (see 'EqualTo')
--
-- @since 0.1
(===) :: Name -> Name -> Obligation
=== :: Name -> Name -> Obligation
(===) = Bool -> Equivalence -> Name -> Name -> Obligation
mkEquality Bool
False Equivalence
StrictEquiv
infix 9 ===

-- | Declare two functions to be equal, but ignoring
-- type lambdas, type arguments, type casts and hpc ticks (see 'EqualTo').
-- Note that @-fhpc@ can prevent some optimizations; build without for more reliable analysis.
--
-- @since 0.1.1
(==-) :: Name -> Name -> Obligation
==- :: Name -> Name -> Obligation
(==-) = Bool -> Equivalence -> Name -> Name -> Obligation
mkEquality Bool
False Equivalence
IgnoreTypesAndTicksEquiv
infix 9 ==-

-- | Declare two functions to be equal as @('==-')@ but also ignoring
-- let bindings ordering (see 'EqualTo').
--
-- @since 0.5
(==~) :: Name -> Name -> Obligation
==~ :: Name -> Name -> Obligation
(==~) = Bool -> Equivalence -> Name -> Name -> Obligation
mkEquality Bool
False Equivalence
UnorderedLetsEquiv
infix 9 ==~

-- | Declare two functions to be equal, but expect the test to fail (see 'EqualTo' and 'expectFail')
-- (This is useful for documentation purposes, or as a TODO list.)
--
-- @since 0.1
(=/=) :: Name -> Name -> Obligation
=/= :: Name -> Name -> Obligation
(=/=) = Bool -> Equivalence -> Name -> Name -> Obligation
mkEquality Bool
True Equivalence
StrictEquiv
infix 9 =/=

-- | Declare two functions to be equal up to types (see '(==-)'),
-- but expect the test to fail (see 'expectFail').
--
-- @since 0.4.3.0
(=/-) :: Name -> Name -> Obligation
=/- :: Name -> Name -> Obligation
(=/-) = Bool -> Equivalence -> Name -> Name -> Obligation
mkEquality Bool
False Equivalence
IgnoreTypesAndTicksEquiv
infix 9 =/-

-- | Declare two functions to be equal up to let binding ordering (see '(==~)'),
-- but expect the test to fail (see 'expectFail').
--
-- @since 0.5
(=/~) :: Name -> Name -> Obligation
=/~ :: Name -> Name -> Obligation
(=/~) = Bool -> Equivalence -> Name -> Name -> Obligation
mkEquality Bool
False Equivalence
UnorderedLetsEquiv
infix 9 =/~

mkEquality :: Bool -> Equivalence -> Name -> Name -> Obligation
mkEquality :: Bool -> Equivalence -> Name -> Name -> Obligation
mkEquality Bool
expectFail Equivalence
ignore_types Name
n1 Name
n2 =
    (Name -> Property -> Obligation
mkObligation Name
n1 (Name -> Equivalence -> Property
EqualTo Name
n2 Equivalence
ignore_types))
        { expectFail = expectFail }

-- | Declare that in a function’s implementation, the given type does not occur.
--
-- More precisely: No locally bound variable (let-bound, lambda-bound or
-- pattern-bound) has a type that contains the given type constructor.
--
-- @'inspect' $ fusedFunction ``hasNoType`` ''[]@
--
-- @since 0.1
hasNoType :: Name -> Name -> Obligation
hasNoType :: Name -> Name -> Obligation
hasNoType Name
n Name
tn = Name -> Property -> Obligation
mkObligation Name
n ([Name] -> Property
NoTypes [Name
tn])

-- | Declare that a function’s implementation does not contain any generic types.
-- This is just 'hasNoType' applied to the usual type constructors used in
-- "GHC.Generics".
--
-- @inspect $ hasNoGenerics genericFunction@
--
-- @since 0.3
hasNoGenerics :: Name -> Obligation
hasNoGenerics :: Name -> Obligation
hasNoGenerics Name
n =
    Name -> Property -> Obligation
mkObligation Name
n
        ([Name] -> Property
NoTypes [ ''V1, ''U1, ''M1, ''K1, ''(:+:), ''(:*:), ''(:.:), ''Rec1
                 , ''Par1
                 ])

-- | Declare that a function's implementation does not include dictionaries.
--
-- More precisely: No locally bound variable (let-bound, lambda-bound or
-- pattern-bound) has a type that contains a type that mentions a type class.
--
-- @'inspect' $ 'hasNoTypeClasses' specializedFunction@
--
-- @since 0.3
hasNoTypeClasses :: Name -> Obligation
hasNoTypeClasses :: Name -> Obligation
hasNoTypeClasses Name
n = Name -> [Name] -> Obligation
hasNoTypeClassesExcept Name
n []

-- | A variant of 'hasNoTypeClasses', which white-lists some type-classes.
--
-- @'inspect' $ fieldLens ``hasNoTypeClassesExcept`` [''Functor]@
--
-- @since 0.3
hasNoTypeClassesExcept :: Name -> [Name] -> Obligation
hasNoTypeClassesExcept :: Name -> [Name] -> Obligation
hasNoTypeClassesExcept Name
n [Name]
tns = Name -> Property -> Obligation
mkObligation Name
n ([Name] -> Property
NoTypeClasses [Name]
tns)

-- | Declare that a function's implementation does not use the given
-- variable (either in terms or -- if it is a constructor -- in patterns).
--
-- @'inspect' $ foo ``doesNotUse`` 'error@
--
-- @since 0.4.1
doesNotUse :: Name -> Name -> Obligation
doesNotUse :: Name -> Name -> Obligation
doesNotUse Name
n Name
ns = Name -> Property -> Obligation
mkObligation Name
n ([Name] -> Property
NoUseOf [Name
ns])

-- | Dump the Core of the value.
--
-- @'inspect' $ 'coreOf' 'foo@
--
-- This is useful when you need to inspect some values manually.
--
-- @since 0.4.2
coreOf :: Name -> Obligation
coreOf :: Name -> Obligation
coreOf Name
n = Name -> Property -> Obligation
mkObligation Name
n Property
CoreOf

-- The exported TH functions

inspectCommon :: AnnTarget -> Obligation -> Q [Dec]
inspectCommon :: AnnTarget -> Obligation -> Q [Dec]
inspectCommon AnnTarget
annTarget Obligation
obl = do
#if MIN_VERSION_GLASGOW_HASKELL(8,4,0,0)
    String -> Q ()
addCorePlugin String
"Test.Inspection.Plugin"
#endif
    Loc
loc <- Q Loc
location
    Exp
annExpr <- Obligation -> Q Exp
forall (m :: * -> *) a. (Quote m, Data a) => a -> m Exp
liftData (Obligation
obl { srcLoc = Just $ fromMaybe loc $ srcLoc obl })
    [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Pragma -> Dec
PragmaD (AnnTarget -> Exp -> Pragma
AnnP AnnTarget
annTarget Exp
annExpr)]

-- | As seen in the example above, the entry point to inspection testing is the
-- 'inspect' function, to which you pass an 'Obligation'.
-- It will report test failures at compile time.
--
-- @since 0.1
inspect :: Obligation -> Q [Dec]
inspect :: Obligation -> Q [Dec]
inspect = AnnTarget -> Obligation -> Q [Dec]
inspectCommon AnnTarget
ModuleAnnotation

-- | The result of 'inspectTest', which has a more or less helpful text message
--
-- @since 0.2
data Result = Failure String | Success String
    deriving Int -> Result -> ShowS
[Result] -> ShowS
Result -> String
(Int -> Result -> ShowS)
-> (Result -> String) -> ([Result] -> ShowS) -> Show Result
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Result -> ShowS
showsPrec :: Int -> Result -> ShowS
$cshow :: Result -> String
show :: Result -> String
$cshowList :: [Result] -> ShowS
showList :: [Result] -> ShowS
Show

didNotRunPluginError :: Result
didNotRunPluginError :: Result
didNotRunPluginError = Result -> Result
forall a. a -> a
lazy (String -> Result
forall a. HasCallStack => String -> a
error String
"Test.Inspection.Plugin did not run")
{-# NOINLINE didNotRunPluginError #-}

-- | This is a variant of 'inspect' that allows compilation to succeed in any case,
-- and instead indicates the result as a value of type 'Result',
-- which allows seamless integration into test frameworks.
--
-- This variant ignores the 'expectFail' field of the obligation. Instead,
-- it is expected that you use the corresponding functionality in your test
-- framework (e.g. [@tasty-expected-failure@](https://hackage.haskell.org/package/tasty-expected-failure))
--
-- @since 0.2
inspectTest :: Obligation -> Q Exp
inspectTest :: Obligation -> Q Exp
inspectTest Obligation
obl = do
    String
nameS <- Q String
genName
    Name
name <- String -> Q Name
forall (q :: * -> *). Quasi q => String -> q Name
newUniqueName String
nameS
    [Dec]
anns <- AnnTarget -> Obligation -> Q [Dec]
inspectCommon (Name -> AnnTarget
ValueAnnotation Name
name) Obligation
obl
    [Dec] -> Q ()
addTopDecls ([Dec] -> Q ()) -> [Dec] -> Q ()
forall a b. (a -> b) -> a -> b
$
        [ Name -> Type -> Dec
SigD Name
name (Name -> Type
ConT ''Result)
        , Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
name) (Exp -> Body
NormalB (Name -> Exp
VarE 'didNotRunPluginError)) []
        , Pragma -> Dec
PragmaD (Name -> Inline -> RuleMatch -> Phases -> Pragma
InlineP Name
name Inline
NoInline RuleMatch
FunLike Phases
AllPhases)
        ] [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
anns
    Exp -> Q Exp
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> Q Exp) -> Exp -> Q Exp
forall a b. (a -> b) -> a -> b
$ Name -> Exp
VarE Name
name
  where
    genName :: Q String
genName = do
        (Int
r,Int
c) <- Loc -> (Int, Int)
loc_start (Loc -> (Int, Int)) -> Q Loc -> Q (Int, Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Q Loc
location
        String -> Q String
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Q String) -> String -> Q String
forall a b. (a -> b) -> a -> b
$ String
"inspect_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
c

-- | Like newName, but even more unique (unique across different splices),
-- and with unique @nameBase@s. Precondition: the string is a valid Haskell
-- alphanumeric identifier (could be upper- or lower-case).
newUniqueName :: Quasi q => String -> q Name
newUniqueName :: forall (q :: * -> *). Quasi q => String -> q Name
newUniqueName String
str = do
  Name
n <- String -> q Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName String
str
  String -> q Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName (String -> q Name) -> String -> q Name
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
n
-- This is from https://ghc.haskell.org/trac/ghc/ticket/13054#comment:1