target- Generate test-suites from refinement types.

Safe HaskellNone




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) 

unfold :: Symbol -> SpecType -> Target [(Symbol, SpecType)] Source

Given a data constuctor d and a refined type for ds output, return a list of types representing suitable arguments for d.

apply :: Symbol -> [Expr] -> Target Expr Source

Given a data constructor d and a list of expressions xs, construct a new expression corresponding to d xs.

unapply :: Symbol -> Target (Symbol, [Symbol]) Source

Split a symbolic variable representing the application of a data constructor into a pair of the data constructor and the sub-variables.

oneOf :: Symbol -> [(Expr, Expr)] -> Target () Source

Given a symbolic variable and a list of (choice, var) pairs, oneOf x choices asserts that x must equal one of the vars in choices.

whichOf :: Symbol -> Target Symbol Source

Given a symbolic variable x, figure out which of xs choice varaibles was picked and return it.

constrain :: Pred -> Target () Source

Assert a logical predicate, guarded by the current choice variable.

ofReft :: Reft -> Expr -> Pred Source

Given a refinement {v | p} and an expression e, construct the predicate p[e/v].