Copyright | (c) Joachim Breitner 2017 |
---|---|
License | MIT |
Maintainer | mail@joachim-breitner.de |
Portability | GHC specifc |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
This module supports the accompanying GHC plugin Test.Inspection.Plugin and adds to GHC the ability to do inspection testing.
Synopsis
- inspect :: Obligation -> Q [Dec]
- inspectTest :: Obligation -> Q Exp
- data Result
- data Obligation = Obligation {}
- mkObligation :: Name -> Property -> Obligation
- data Equivalence
- data Property
- = EqualTo Name Equivalence
- | NoTypes [Name]
- | NoAllocation
- | NoTypeClasses [Name]
- | NoUseOf [Name]
- | CoreOf
- (===) :: Name -> Name -> Obligation
- (==-) :: Name -> Name -> Obligation
- (=/=) :: Name -> Name -> Obligation
- (=/-) :: Name -> Name -> Obligation
- (==~) :: Name -> Name -> Obligation
- (=/~) :: Name -> Name -> Obligation
- hasNoType :: Name -> Name -> Obligation
- hasNoGenerics :: Name -> Obligation
- hasNoTypeClasses :: Name -> Obligation
- hasNoTypeClassesExcept :: Name -> [Name] -> Obligation
- doesNotUse :: Name -> Name -> Obligation
- coreOf :: Name -> Obligation
Synopsis
To use inspection testing, you need to
- enable the
TemplateHaskell
language extension - declare your proof obligations using
inspect
orinspectTest
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:
{-# OPTIONS_GHC -fplugin=Test.Inspection.Plugin #-}
Registering obligations
inspect :: Obligation -> Q [Dec] Source #
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
inspectTest :: Obligation -> Q Exp Source #
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
)
Since: 0.2
The result of inspectTest
, which has a more or less helpful text message
Since: 0.2
Defining obligations
data Obligation Source #
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
Obligation | |
|
Instances
Data Obligation Source # | |
Defined in Test.Inspection gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Obligation -> c Obligation # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Obligation # toConstr :: Obligation -> Constr # dataTypeOf :: Obligation -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Obligation) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Obligation) # gmapT :: (forall b. Data b => b -> b) -> Obligation -> Obligation # gmapQl :: (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 # gmapQ :: (forall d. Data d => d -> u) -> Obligation -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Obligation -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Obligation -> m Obligation # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Obligation -> m Obligation # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Obligation -> m Obligation # |
mkObligation :: Name -> Property -> Obligation Source #
Creates an inspection obligation for the given function name with default values for the optional fields.
Since: 0.1
data Equivalence Source #
Equivalence of terms.
Since: 0.5
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 |
Instances
Data Equivalence Source # | |
Defined in Test.Inspection gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Equivalence -> c Equivalence # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Equivalence # toConstr :: Equivalence -> Constr # dataTypeOf :: Equivalence -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Equivalence) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Equivalence) # gmapT :: (forall b. Data b => b -> b) -> Equivalence -> Equivalence # gmapQl :: (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 # gmapQ :: (forall d. Data d => d -> u) -> Equivalence -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Equivalence -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence # |
Properties of the obligation target to be checked.
Since: 0.1
EqualTo Name Equivalence | Are the two functions equal? More precisely: In general The |
NoTypes [Name] | Do none of these types appear anywhere in the definition of the function (neither locally bound nor passed as arguments) Since: 0.3 |
NoAllocation | Does this function perform no heap allocations. |
NoTypeClasses [Name] | Does this value contain dictionaries (except of the listed classes). Since: 0.3 |
NoUseOf [Name] | Does not contain this value (in terms or patterns) Since: 0.4.1 |
CoreOf | Always satisfied, but dumps the value in non-quiet mode. Since: 0.4.2 |
Instances
Data Property Source # | |
Defined in Test.Inspection gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Property -> c Property # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Property # toConstr :: Property -> Constr # dataTypeOf :: Property -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Property) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Property) # gmapT :: (forall b. Data b => b -> b) -> Property -> Property # gmapQl :: (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 # gmapQ :: (forall d. Data d => d -> u) -> Property -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Property -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Property -> m Property # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Property -> m Property # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Property -> m Property # |
Convenience functions
These convenience functions create common test obligations directly.
(===) :: Name -> Name -> Obligation infix 9 Source #
Declare two functions to be equal (see EqualTo
)
Since: 0.1
(==-) :: Name -> Name -> Obligation infix 9 Source #
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 infix 9 Source #
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 infix 9 Source #
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 infix 9 Source #
Declare two functions to be equal up to let binding ordering (see (==~)
),
but expect the test to fail (see expectFail
).
Since: 0.5
hasNoType :: Name -> Name -> Obligation Source #
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
hasNoGenerics :: Name -> Obligation Source #
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
hasNoTypeClasses :: Name -> Obligation Source #
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
hasNoTypeClassesExcept :: Name -> [Name] -> Obligation Source #
A variant of hasNoTypeClasses
, which white-lists some type-classes.
inspect
$ fieldLens`hasNoTypeClassesExcept`
[''Functor]
Since: 0.3
doesNotUse :: Name -> Name -> Obligation Source #
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