Copyright	(c) Joachim Breitner 2017
License	MIT
Maintainer	mail@joachim-breitner.de
Portability	GHC specifc
Safe Haskell	None
Language	Haskell2010

Test.Inspection

Contents

Synopsis
Registering obligations
Defining obligations
Convenience functions

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
- = Failure String
- | Success String
data Obligation = Obligation {
- target :: Name
- property :: Property
- testName :: Maybe String
- expectFail :: Bool
- srcLoc :: Maybe Loc
- storeResult :: Maybe String
}
mkObligation :: Name -> Property -> Obligation
data Property
- = EqualTo Name Bool
- | NoTypes [Name]
- | NoAllocation
- | NoTypeClasses [Name]
- | NoUseOf [Name]
- | CoreOf
(===) :: 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 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: {-# 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)

data Result Source #

The result of inspectTest, which has a more or less helpful text message

Constructors

Failure String
Success String

Instances

Show Result Source #
Instance details Defined in Test.Inspection Methods showsPrec :: Int -> Result -> ShowS # show :: Result -> String # showList :: [Result] -> ShowS #

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

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 {-# LANGUAGE TemplateHaskell #-}.
property :: Property
The property of the target to be checked.
testName :: Maybe String
An optional name for the test
expectFail :: Bool
Do we expect this property to fail? (Only used by inspect, not by inspectTest)
srcLoc :: Maybe Loc
The source location where this obligation is defined. This is filled in by inspect.
storeResult :: Maybe String
If this is Nothing, then report errors during compilation. Otherwise, update the top-level definition with this name.

Instances

Data Obligation Source #

Instance details

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.

data Property Source #

Properties of the obligation target to be checked.

Constructors

EqualTo Name Bool	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. 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 #

Instance details

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 (see EqualTo)

(==-) :: 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.)

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` ''[]

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 $ hasNoTypeClasses specializedFunction

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

coreOf :: Name -> Obligation Source #

Dump the Core of the value.

inspect $ coreOf 'foo

This is useful when you need to inspect some values manually.