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.
Moduleinspection-testing-0.6.3Haskell2010
Test.Inspection
This module supports the accompanying GHC plugin Test.Inspection.Plugin and adds to GHC the ability to do inspection testing.
Synopsis
- value inspect
- value inspectTest
- data Result
- data Obligation
- value mkObligation
- data Equivalence
- data Property
- value ===
- value ==-
- value =/=
- value =/-
- value ==~
- value =/~
- value hasNoType
- value hasNoGenerics
- value hasNoTypeClasses
- value hasNoTypeClassesExcept
- value doesNotUse
- value coreOf
- Packageinspection-testing-0.6.3
- Exports19
- LanguageHaskell2010
- LicenceMIT
- SourceInspection.hs
Synopsis
To use inspection testing, you need to
enable the
TemplateHaskelllanguage extensiondeclare 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
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)
The result of inspectTest, which has a more or less helpful text message
Defining obligations
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.
Constructors
Obligationtarget :: NameThe 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 :: PropertyThe property of the target to be checked.
testName :: Maybe StringAn optional name for the test
expectFail :: BoolDo we expect this property to fail? (Only used by inspect, not by inspectTest)
srcLoc :: Maybe LocThe source location where this obligation is defined. This is filled in by inspect.
storeResult :: Maybe StringIf this is Nothing, then report errors during compilation. Otherwise, update the top-level definition with this name.
Instances1Data
Data ObligationDefined in inspection-testing-0.6.3 · Test.Inspection
Creates an inspection obligation for the given function name with default values for the optional fields.
Equivalence of terms.
Constructors
StrictEquivstrict term equality
IgnoreTypesAndTicksEquivignore types and hpc ticks during the comparison
UnorderedLetsEquivallow permuted let bindings, ignore types and hpc tick during comparison
Instances1Data
Data EquivalenceDefined in inspection-testing-0.6.3 · Test.Inspection
Properties of the obligation target to be checked.
Constructors
EqualTo Name EquivalenceAre the two functions equal?
More precisely:
fis equal togif either the definition offisf = g, or the definition ofgisg = f, or if the definitions aref = eandg = e.In general
fandgneed 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)
NoAllocationDoes 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)
CoreOfAlways satisfied, but dumps the value in non-quiet mode.
Convenience functions
These convenience functions create common test obligations directly.
Declare two functions to be equal (see EqualTo)
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.
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.)
Declare two functions to be equal up to types (see (==-)),
but expect the test to fail (see expectFail).
Declare two functions to be equal up to let binding ordering (see (==~)),
but expect the test to fail (see expectFail).
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` ''[]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 genericFunctionDeclare 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 specializedFunctionA variant of hasNoTypeClasses, which white-lists some type-classes.
inspect $ fieldLens `hasNoTypeClassesExcept` [''Functor]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