inspection-testing-0.1: GHC plugin to do inspection esting

Copyright(c) Joachim Breitner 2017
LicenseMIT
Maintainermail@joachim-breitner.de
PortabilityGHC specifc
Safe HaskellNone
LanguageHaskell2010

Test.Inspection

Contents

Description

This module supports the accompanying GHC plugin Test.Inspection.Plugin and adds to GHC the ability to do inspeciton testing.

Synopsis

Synopsis

To use inspection testing, you need to

  1. enable the TemplateHaskell langauge extension
  2. load the plugin using -fplugin Test.Inspection.Plugin
  3. declare your proof obligations using inspect

An example module is

{-# LANGAUGE TemplateHaskell #-}
{-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}
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

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.

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 memonic 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 {-# LANGAUGE 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?

  • srcLoc :: Maybe Loc

    The source location where this obligation is defined. This is filled in by inspect.

Instances

Data Obligation Source # 

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

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.

NoType Name

Does this type not occur anywhere in the definition of the function (neither locally bound nor passed as arguments)

NoAllocation

Does this function perform no heap allocations.

Instances

Data Property Source # 

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 #

(===) :: Name -> Name -> Obligation infix 1 Source #

Convenience function to declare two functions to be equal

(=/=) :: Name -> Name -> Obligation infix 1 Source #

Convenience function to declare two functions to be equal, but expect the test to fail (This is useful for documentation purposes, or as a TODO list.)

hasNoType :: Name -> Name -> Obligation Source #

Convenience function to declare that a function’s implementation does not mention a type

inspect $ fusedFunction hasNoType ''[]