target- Generate test-suites from refinement types.

Safe HaskellNone




target Source


:: Testable f 
=> f

the function

-> String

the name of the function

-> FilePath

the path to the module that defines the function

-> IO () 

Test whether a function inhabits its refinement type by enumerating valid inputs and calling the function.

targetResult :: Testable f => f -> String -> FilePath -> IO Result Source

Like target, but returns the Result instead of printing to standard out.

targetWith :: Testable f => f -> String -> FilePath -> TargetOpts -> IO () Source

Like target, but accepts options to control the enumeration depth, solver, and verbosity.

targetResultWith :: Testable f => f -> String -> FilePath -> TargetOpts -> IO Result Source

Like targetWith, but returns the Result instead of printing to standard out.

data Result Source


Passed !Int 
Failed !String 
Errored !String 


class (AllHave Targetable (Args f), Targetable (Res f), AllHave Show (Args f)) => Testable f Source

A class of functions that Target can test. A function is Testable iff all of its component types are Targetable and all of its argument types are Showable.

You should never have to define a new Testable instance.

Minimal complete definition

queryArgs, decodeArgs, apply, mkExprs


(Targetable a, (~) [*] (Args a) ([] *), (~) * (Res a) a) => Testable a 
(Show a, Targetable a, Testable b) => Testable (a -> b) 

class Targetable a where Source

A class of datatypes for which we can efficiently generate constrained values by querying an SMT solver.

If possible, instances should not be written by hand, but rather by using the default implementations via GHC.Generics, e.g.

import GHC.Generics
import Test.Target.Targetable

data Foo = ... deriving Generic
instance Targetable Foo

Minimal complete definition



query :: Proxy a -> Depth -> SpecType -> Target Symbol Source

Construct an SMT query describing all values of the given type up to the given Depth.

decode Source


:: Symbol

the symbolic variable corresponding to the root of the value

-> SpecType

the type of values we're generating (you can probably ignore this)

-> Target a 

Reconstruct a Haskell value from the SMT model.

check :: a -> SpecType -> Target (Bool, Expr) Source

Check whether a Haskell value inhabits the given type. Also returns a logical expression corresponding to the Haskell value.

toExpr :: a -> Expr Source

Translate a Haskell value into a logical expression.

getType :: Proxy a -> Sort Source

What is the Haskell type? (Mainly used to make the SMT queries more readable).


Targetable Bool 
Targetable Char 
Targetable Int 
Targetable Integer 
Targetable Word8 
Targetable () 
Targetable a => Targetable [a] 
Targetable a => Targetable (Maybe a) 
(Targetable a, Targetable b, Targetable c, Targetable d, (~) * d (Res (a -> b -> c -> d))) => Targetable (a -> b -> c -> d) 
(Targetable a, Targetable b, Targetable c, (~) * c (Res (a -> b -> c))) => Targetable (a -> b -> c) 
(Targetable a, Targetable b, (~) * b (Res (a -> b))) => Targetable (a -> b) 
(Targetable a, Targetable b) => Targetable (Either a b) 
(Targetable a, Targetable b) => Targetable (a, b) 
(Targetable a, Targetable b, Targetable c) => Targetable (a, b, c) 
(Targetable a, Targetable b, Targetable c, Targetable d) => Targetable (a, b, c, d) 

data TargetOpts Source




depth :: !Int
solver :: !SMTSolver
verbose :: !Bool
logging :: !Bool
keepGoing :: !Bool

whether to keep going after finding a counter-example, useful for checking coverage

maxSuccess :: !(Maybe Int)

whether to stop after a certain number of successful tests, or enumerate the whole input space

scDepth :: !Bool

whether to use SmallCheck's notion of depth

ghcOpts :: ![String]

extra options to pass to GHC

data Test Source


forall t . Testable t => T t 

monomorphic :: Name -> ExpQ

Monomorphise an arbitrary property by defaulting all type variables to Integer.

For example, if f has type Ord a => [a] -> [a] then $(monomorphic 'f) has type [Integer] -> [Integer].

If you want to use monomorphic in the same file where you defined the property, the same scoping problems pop up as in quickCheckAll: see the note there about return [].