{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE CPP #-}
module Test.Inspection (
inspect,
inspectTest,
Result(..),
Obligation(..), mkObligation, Equivalence (..), Property(..),
(===), (==-), (=/=), (=/-), (==~), (=/~),
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)
data Obligation = Obligation
{ Obligation -> Name
target :: Name
, Obligation -> Property
property :: Property
, Obligation -> Maybe String
testName :: Maybe String
, Obligation -> Bool
expectFail :: Bool
, Obligation -> Maybe Loc
srcLoc :: Maybe Loc
, Obligation -> Maybe String
storeResult :: Maybe String
}
deriving Typeable Obligation
DataType
Constr
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 -> DataType
Obligation -> Constr
(forall b. Data b => b -> b) -> Obligation -> Obligation
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Obligation -> c Obligation
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cObligation :: Constr
$tObligation :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d) -> Obligation -> m Obligation
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Obligation -> m Obligation
gmapQi :: Int -> (forall d. Data d => d -> u) -> Obligation -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Obligation -> u
gmapQ :: (forall d. Data d => d -> u) -> Obligation -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Obligation -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Obligation -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Obligation -> r
gmapT :: (forall b. Data b => b -> b) -> Obligation -> Obligation
$cgmapT :: (forall b. Data b => b -> b) -> Obligation -> Obligation
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Obligation)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Obligation)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Obligation)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Obligation)
dataTypeOf :: Obligation -> DataType
$cdataTypeOf :: Obligation -> DataType
toConstr :: Obligation -> Constr
$ctoConstr :: Obligation -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Obligation
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Obligation
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Obligation -> c Obligation
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Obligation -> c Obligation
$cp1Data :: Typeable Obligation
Data
data Property
= EqualTo Name Equivalence
| NoTypes [Name]
| NoAllocation
| NoTypeClasses [Name]
| NoUseOf [Name]
| CoreOf
deriving Typeable Property
DataType
Constr
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 -> DataType
Property -> Constr
(forall b. Data b => b -> b) -> Property -> Property
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Property -> c Property
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cCoreOf :: Constr
$cNoUseOf :: Constr
$cNoTypeClasses :: Constr
$cNoAllocation :: Constr
$cNoTypes :: Constr
$cEqualTo :: Constr
$tProperty :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d) -> Property -> m Property
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Property -> m Property
gmapQi :: Int -> (forall d. Data d => d -> u) -> Property -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Property -> u
gmapQ :: (forall d. Data d => d -> u) -> Property -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Property -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Property -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Property -> r
gmapT :: (forall b. Data b => b -> b) -> Property -> Property
$cgmapT :: (forall b. Data b => b -> b) -> Property -> Property
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Property)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Property)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Property)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Property)
dataTypeOf :: Property -> DataType
$cdataTypeOf :: Property -> DataType
toConstr :: Property -> Constr
$ctoConstr :: Property -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Property
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Property
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Property -> c Property
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Property -> c Property
$cp1Data :: Typeable Property
Data
data Equivalence
= StrictEquiv
| IgnoreTypesAndTicksEquiv
| UnorderedLetsEquiv
deriving Typeable Equivalence
DataType
Constr
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 -> DataType
Equivalence -> Constr
(forall b. Data b => b -> b) -> Equivalence -> Equivalence
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Equivalence -> c Equivalence
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cUnorderedLetsEquiv :: Constr
$cIgnoreTypesAndTicksEquiv :: Constr
$cStrictEquiv :: Constr
$tEquivalence :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Equivalence -> m Equivalence
gmapQi :: Int -> (forall d. Data d => d -> u) -> Equivalence -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Equivalence -> u
gmapQ :: (forall d. Data d => d -> u) -> Equivalence -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Equivalence -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Equivalence -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Equivalence -> r
gmapT :: (forall b. Data b => b -> b) -> Equivalence -> Equivalence
$cgmapT :: (forall b. Data b => b -> b) -> Equivalence -> Equivalence
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Equivalence)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Equivalence)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Equivalence)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Equivalence)
dataTypeOf :: Equivalence -> DataType
$cdataTypeOf :: Equivalence -> DataType
toConstr :: Equivalence -> Constr
$ctoConstr :: Equivalence -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Equivalence
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Equivalence
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Equivalence -> c Equivalence
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Equivalence -> c Equivalence
$cp1Data :: Typeable Equivalence
Data
mkObligation :: Name -> Property -> Obligation
mkObligation :: Name -> Property -> Obligation
mkObligation Name
target Property
prop = Obligation :: Name
-> Property
-> Maybe String
-> Bool
-> Maybe Loc
-> Maybe String
-> Obligation
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
}
(===) :: Name -> Name -> Obligation
=== :: Name -> Name -> Obligation
(===) = Bool -> Equivalence -> Name -> Name -> Obligation
mkEquality Bool
False Equivalence
StrictEquiv
infix 9 ===
(==-) :: Name -> Name -> Obligation
==- :: Name -> Name -> Obligation
(==-) = Bool -> Equivalence -> Name -> Name -> Obligation
mkEquality Bool
False Equivalence
IgnoreTypesAndTicksEquiv
infix 9 ==-
(==~) :: Name -> Name -> Obligation
==~ :: Name -> Name -> Obligation
(==~) = Bool -> Equivalence -> Name -> Name -> Obligation
mkEquality Bool
False Equivalence
UnorderedLetsEquiv
infix 9 ==~
(=/=) :: Name -> Name -> Obligation
=/= :: Name -> Name -> Obligation
(=/=) = Bool -> Equivalence -> Name -> Name -> Obligation
mkEquality Bool
True Equivalence
StrictEquiv
infix 9 =/=
(=/-) :: Name -> Name -> Obligation
=/- :: Name -> Name -> Obligation
(=/-) = Bool -> Equivalence -> Name -> Name -> Obligation
mkEquality Bool
False Equivalence
IgnoreTypesAndTicksEquiv
infix 9 =/-
(=/~) :: 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 :: Bool
expectFail = Bool
expectFail }
hasNoType :: Name -> Name -> Obligation
hasNoType :: Name -> Name -> Obligation
hasNoType Name
n Name
tn = Name -> Property -> Obligation
mkObligation Name
n ([Name] -> Property
NoTypes [Name
tn])
hasNoGenerics :: Name -> Obligation
hasNoGenerics :: Name -> Obligation
hasNoGenerics Name
n =
Name -> Property -> Obligation
mkObligation Name
n
([Name] -> Property
NoTypes [ ''V1, ''U1, ''M1, ''K1, ''(:+:), ''(:*:), ''(:.:), ''Rec1
, ''Par1
])
hasNoTypeClasses :: Name -> Obligation
hasNoTypeClasses :: Name -> Obligation
hasNoTypeClasses Name
n = Name -> [Name] -> Obligation
hasNoTypeClassesExcept Name
n []
hasNoTypeClassesExcept :: Name -> [Name] -> Obligation
hasNoTypeClassesExcept :: Name -> [Name] -> Obligation
hasNoTypeClassesExcept Name
n [Name]
tns = Name -> Property -> Obligation
mkObligation Name
n ([Name] -> Property
NoTypeClasses [Name]
tns)
doesNotUse :: Name -> Name -> Obligation
doesNotUse :: Name -> Name -> Obligation
doesNotUse Name
n Name
ns = Name -> Property -> Obligation
mkObligation Name
n ([Name] -> Property
NoUseOf [Name
ns])
coreOf :: Name -> Obligation
coreOf :: Name -> Obligation
coreOf Name
n = Name -> Property -> Obligation
mkObligation Name
n Property
CoreOf
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 a. Data a => a -> Q Exp
liftData (Obligation
obl { srcLoc :: Maybe Loc
srcLoc = Loc -> Maybe Loc
forall a. a -> Maybe a
Just (Loc -> Maybe Loc) -> Loc -> Maybe Loc
forall a b. (a -> b) -> a -> b
$ Loc -> Maybe Loc -> Loc
forall a. a -> Maybe a -> a
fromMaybe Loc
loc (Maybe Loc -> Loc) -> Maybe Loc -> Loc
forall a b. (a -> b) -> a -> b
$ Obligation -> Maybe Loc
srcLoc Obligation
obl })
[Dec] -> Q [Dec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Pragma -> Dec
PragmaD (AnnTarget -> Exp -> Pragma
AnnP AnnTarget
annTarget Exp
annExpr)]
inspect :: Obligation -> Q [Dec]
inspect :: Obligation -> Q [Dec]
inspect = AnnTarget -> Obligation -> Q [Dec]
inspectCommon AnnTarget
ModuleAnnotation
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
showList :: [Result] -> ShowS
$cshowList :: [Result] -> ShowS
show :: Result -> String
$cshow :: Result -> String
showsPrec :: Int -> Result -> ShowS
$cshowsPrec :: Int -> 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 #-}
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 (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 (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
newUniqueName :: Quasi q => String -> q Name
newUniqueName :: 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