Test.Target

Documentation

target

Arguments

:: 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

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

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

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

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

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

targetTH :: Name -> Q (TExp (FilePath -> IO ()))

targetResultTH :: Name -> Q (TExp (FilePath -> IO Result))

targetWithTH :: Name -> Q (TExp (FilePath -> TargetOpts -> IO ()))

targetResultWithTH :: Name -> Q (TExp (FilePath -> TargetOpts -> IO Result))

data Result

Constructors

Passed !Int

Failed !String

Errored !String

Instances

Show Result

Methods

showsPrec :: Int -> Result -> ShowS

show :: Result -> String

showList :: [Result] -> ShowS

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

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

Instances

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

Methods

queryArgs :: a -> Int -> SpecType -> Target [Symbol]

decodeArgs :: a -> [Symbol] -> [SpecType] -> Target (HList (Args a))

apply :: a -> HList (Args a) -> Res a

mkExprs :: a -> [Symbol] -> HList (Args a) -> [(Symbol, Expr)]

(Show a, Targetable a, Testable b) => Testable (a -> b)

Methods

queryArgs :: (a -> b) -> Int -> SpecType -> Target [Symbol]

decodeArgs :: (a -> b) -> [Symbol] -> [SpecType] -> Target (HList (Args (a -> b)))

apply :: (a -> b) -> HList (Args (a -> b)) -> Res (a -> b)

mkExprs :: (a -> b) -> [Symbol] -> HList (Args (a -> b)) -> [(Symbol, Expr)]

class Targetable a where

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

Methods

query :: (?loc :: CallStack) => Proxy a -> Depth -> Symbol -> SpecType -> Target Symbol

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

decode :: Symbol -> SpecType -> Target a

Reconstruct a Haskell value from the SMT model.

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

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

toExpr :: a -> Expr

Translate a Haskell value into a logical expression.

getType :: Proxy a -> Sort

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

getType :: (Generic a, Rep a ~ D1 d f, Datatype d) => Proxy a -> Sort

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

query :: (?loc :: CallStack) => (Generic a, GQuery (Rep a)) => Proxy a -> Int -> Symbol -> SpecType -> Target Symbol

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

toExpr :: (Generic a, GToExpr (Rep a)) => a -> Expr

Translate a Haskell value into a logical expression.

decode :: (Generic a, GDecode (Rep a)) => Symbol -> SpecType -> Target a

Reconstruct a Haskell value from the SMT model.

check :: (Generic a, GCheck (Rep a)) => a -> SpecType -> Target (Bool, Expr)

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

Instances

Targetable Bool

Methods

query :: Proxy * Bool -> Depth -> Symbol -> SpecType -> Target Symbol

decode :: Symbol -> SpecType -> Target Bool

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

toExpr :: Bool -> Expr

getType :: Proxy * Bool -> Sort

Targetable Char

Methods

query :: Proxy * Char -> Depth -> Symbol -> SpecType -> Target Symbol

decode :: Symbol -> SpecType -> Target Char

check :: Char -> SpecType -> Target (Bool, Expr)

toExpr :: Char -> Expr

getType :: Proxy * Char -> Sort

Targetable Int

Methods

query :: Proxy * Int -> Depth -> Symbol -> SpecType -> Target Symbol

decode :: Symbol -> SpecType -> Target Int

check :: Int -> SpecType -> Target (Bool, Expr)

toExpr :: Int -> Expr

getType :: Proxy * Int -> Sort

Targetable Integer

Methods

query :: Proxy * Integer -> Depth -> Symbol -> SpecType -> Target Symbol

decode :: Symbol -> SpecType -> Target Integer

check :: Integer -> SpecType -> Target (Bool, Expr)

toExpr :: Integer -> Expr

getType :: Proxy * Integer -> Sort

Targetable Word8

Methods

query :: Proxy * Word8 -> Depth -> Symbol -> SpecType -> Target Symbol

decode :: Symbol -> SpecType -> Target Word8

check :: Word8 -> SpecType -> Target (Bool, Expr)

toExpr :: Word8 -> Expr

getType :: Proxy * Word8 -> Sort

Targetable ()

Methods

query :: Proxy * () -> Depth -> Symbol -> SpecType -> Target Symbol

decode :: Symbol -> SpecType -> Target ()

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

toExpr :: () -> Expr

getType :: Proxy * () -> Sort

Targetable a => Targetable [a]

Methods

query :: Proxy * [a] -> Depth -> Symbol -> SpecType -> Target Symbol

decode :: Symbol -> SpecType -> Target [a]

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

toExpr :: [a] -> Expr

getType :: Proxy * [a] -> Sort

Targetable a => Targetable (Maybe a)

Methods

query :: Proxy * (Maybe a) -> Depth -> Symbol -> SpecType -> Target Symbol

decode :: Symbol -> SpecType -> Target (Maybe a)

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

toExpr :: Maybe a -> Expr

getType :: Proxy * (Maybe a) -> Sort

(Targetable a, Targetable b) => Targetable (Either a b)

Methods

query :: Proxy * (Either a b) -> Depth -> Symbol -> SpecType -> Target Symbol

decode :: Symbol -> SpecType -> Target (Either a b)

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

toExpr :: Either a b -> Expr

getType :: Proxy * (Either a b) -> Sort

(Targetable a, Targetable b) => Targetable (a, b)

Methods

query :: Proxy * (a, b) -> Depth -> Symbol -> SpecType -> Target Symbol

decode :: Symbol -> SpecType -> Target (a, b)

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

toExpr :: (a, b) -> Expr

getType :: Proxy * (a, b) -> Sort

(Targetable a, Targetable b, Targetable c) => Targetable (a, b, c)

Methods

query :: Proxy * (a, b, c) -> Depth -> Symbol -> SpecType -> Target Symbol

decode :: Symbol -> SpecType -> Target (a, b, c)

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

toExpr :: (a, b, c) -> Expr

getType :: Proxy * (a, b, c) -> Sort

(Targetable a, Targetable b, Targetable c, Targetable d) => Targetable (a, b, c, d)

Methods

query :: Proxy * (a, b, c, d) -> Depth -> Symbol -> SpecType -> Target Symbol

decode :: Symbol -> SpecType -> Target (a, b, c, d)

check :: (a, b, c, d) -> SpecType -> Target (Bool, Expr)

toExpr :: (a, b, c, d) -> Expr

getType :: Proxy * (a, b, c, d) -> Sort

data TargetOpts

Constructors

TargetOpts

Fields

• 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

Instances

MonadReader TargetOpts Target

Methods

ask :: Target TargetOpts

local :: (TargetOpts -> TargetOpts) -> Target a -> Target a

reader :: (TargetOpts -> a) -> Target a

defaultOpts :: TargetOpts

data Test

Constructors

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 [].