target- Generate test-suites from refinement types.

Safe HaskellNone




lookupCtor :: Symbol -> Target SpecType Source

Find the refined type of a data constructor.

guarded :: String -> Target Expr -> Target (Expr, Expr) Source

Given a data constructor d and an action, create a new choice variable c and execute the action while guarding any generated constraints with c. Returns (action-result, c).

fresh :: Sort -> Target Symbol Source

Generate a fresh variable of the given Sort.

freshChoice :: String -> Target Symbol Source

Given a data constructor d, create a new choice variable corresponding to d.

getValue :: Symbol -> Target Value Source

Ask the SMT solver for the Value of the given variable.

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