inspection-testing-0.6.2: GHC plugin to do inspection testing

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 Equivalence
  - = StrictEquiv
  - | IgnoreTypesAndTicksEquiv
  - | UnorderedLetsEquiv
- 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

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: `{-# 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

data Result Source #

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

Since: 0.2

Constructors

Failure String |
Success String |

#### Instances

Instances details

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

# 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

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.

  Since: 0.2

#### Instances

Instances details

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Obligation Source #

toConstr :: Obligation -> Constr Source #

dataTypeOf :: Obligation -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Obligation) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Obligation) Source #

gmapT :: (forall b. Data b => b -> b) -> Obligation -> Obligation Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Obligation -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Obligation -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Obligation -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Obligation -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Obligation -> m Obligation Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Obligation -> m Obligation Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Obligation -> m Obligation Source #

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

Constructors

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

Instances details

Data Equivalence 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) -> Equivalence -> c Equivalence Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Equivalence Source #

toConstr :: Equivalence -> Constr Source #

dataTypeOf :: Equivalence -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Equivalence) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Equivalence) Source #

gmapT :: (forall b. Data b => b -> b) -> Equivalence -> Equivalence Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Equivalence -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Equivalence -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Equivalence -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Equivalence -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Equivalence -> m Equivalence Source #

data Property Source #

Properties of the obligation target to be checked.

Since: 0.1

Constructors

EqualTo Name Equivalence | 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
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

Instances details

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Property Source #

toConstr :: Property -> Constr Source #

dataTypeOf :: Property -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Property) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Property) Source #

gmapT :: (forall b. Data b => b -> b) -> Property -> Property Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Property -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Property -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Property -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Property -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Property -> m Property Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Property -> m Property Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Property -> m Property Source #

# 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 as `(`==-`)` but also ignoring let bindings ordering (see `EqualTo`).

Since: 0.5

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

coreOf :: Name -> Obligation Source #

Dump the Core of the value.

    inspect $ coreOf 'foo

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

Since: 0.4.2