| Copyright | (c) Joachim Breitner 2017 |
|---|---|
| License | MIT |
| Maintainer | mail@joachim-breitner.de |
| Portability | GHC specifc |
| Safe Haskell | None |
| Language | Haskell2010 |
Test.Inspection
Description
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 Property
- (===) :: 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
TemplateHaskelllanguage extension - declare your proof obligations using
inspectorinspectTest
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:
{-# LANGUAGE TemplateHaskell #-}
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.
inspectTest :: Obligation -> Q Exp Source #
This is a variant 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)
The result of inspectTest, which has a more or less helpful text message
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.
Constructors
| Obligation | |
Fields
| |
Instances
| Data Obligation Source # | |
Defined in Test.Inspection Methods 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 :: (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.
Properties of the obligation target to be checked.
Constructors
| EqualTo Name Bool | Are the two functions equal? More precisely: In general If the boolean flag is true, then ignore types during the comparison. |
| NoTypes [Name] | Do none of these types appear anywhere in the definition of the function (neither locally bound nor passed as arguments) |
| NoAllocation | Does this function perform no heap allocations. |
| NoTypeClasses [Name] | Does this value contain dictionaries (except of the listed classes). |
| NoUseOf [Name] | Does not contain this value (in terms or patterns) |
| CoreOf | Always satisfied, but dumps the value in non-quiet mode. |
Instances
| Data Property Source # | |
Defined in Test.Inspection Methods 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 :: (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, but ignoring
type lambdas, type arguments and type casts (see EqualTo)
(=/=) :: 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.)
hasNoGenerics :: Name -> Obligation Source #
Declare that a function’s implementation does not contain any generic types.
This is just asNoType applied to the usual type constructors used in
GHC.Generics.
inspect $ hasNoGenerics genericFunction
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$hasNoTypeClassesspecializedFunction
hasNoTypeClassesExcept :: Name -> [Name] -> Obligation Source #
A variant of hasNoTypeClasses, which white-lists some type-classes.
inspect$ fieldLens `hasNoTypeClassesExcept` [''Functor]
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