Safe Haskell	None
Language	Haskell98

Test.Target

Synopsis

Documentation

target Source #

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

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

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

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

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

data Result Source #

Constructors

Passed !Int
Failed !String
Errored !String

Instances

Show Result Source #
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 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

Instances

(Targetable a, (~) [] (Args a) ([] ), (~) * (Res a) a) => Testable a Source #
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) Source #
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 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

Methods

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

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

decode :: Symbol -> SpecType -> Target a Source #

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).

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

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 Source #

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

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

Translate a Haskell value into a logical expression.

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

Reconstruct a Haskell value from the SMT model.

check :: (Generic a, GCheck (Rep a)) => 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.

Instances

Targetable Bool Source #
Methods query :: Proxy * Bool -> Depth -> Symbol -> SpecType -> Target Symbol Source # decode :: Symbol -> SpecType -> Target Bool Source # check :: Bool -> SpecType -> Target (Bool, Expr) Source # toExpr :: Bool -> Expr Source # getType :: Proxy * Bool -> Sort Source #
Targetable Char Source #
Methods query :: Proxy * Char -> Depth -> Symbol -> SpecType -> Target Symbol Source # decode :: Symbol -> SpecType -> Target Char Source # check :: Char -> SpecType -> Target (Bool, Expr) Source # toExpr :: Char -> Expr Source # getType :: Proxy * Char -> Sort Source #
Targetable Int Source #
Methods query :: Proxy * Int -> Depth -> Symbol -> SpecType -> Target Symbol Source # decode :: Symbol -> SpecType -> Target Int Source # check :: Int -> SpecType -> Target (Bool, Expr) Source # toExpr :: Int -> Expr Source # getType :: Proxy * Int -> Sort Source #
Targetable Integer Source #
Methods query :: Proxy * Integer -> Depth -> Symbol -> SpecType -> Target Symbol Source # decode :: Symbol -> SpecType -> Target Integer Source # check :: Integer -> SpecType -> Target (Bool, Expr) Source # toExpr :: Integer -> Expr Source # getType :: Proxy * Integer -> Sort Source #
Targetable Word8 Source #
Methods query :: Proxy * Word8 -> Depth -> Symbol -> SpecType -> Target Symbol Source # decode :: Symbol -> SpecType -> Target Word8 Source # check :: Word8 -> SpecType -> Target (Bool, Expr) Source # toExpr :: Word8 -> Expr Source # getType :: Proxy * Word8 -> Sort Source #
Targetable () Source #
Methods query :: Proxy * () -> Depth -> Symbol -> SpecType -> Target Symbol Source # decode :: Symbol -> SpecType -> Target () Source # check :: () -> SpecType -> Target (Bool, Expr) Source # toExpr :: () -> Expr Source # getType :: Proxy * () -> Sort Source #
Targetable a => Targetable [a] Source #
Methods query :: Proxy * [a] -> Depth -> Symbol -> SpecType -> Target Symbol Source # decode :: Symbol -> SpecType -> Target [a] Source # check :: [a] -> SpecType -> Target (Bool, Expr) Source # toExpr :: [a] -> Expr Source # getType :: Proxy * [a] -> Sort Source #
Targetable a => Targetable (Maybe a) Source #
Methods query :: Proxy * (Maybe a) -> Depth -> Symbol -> SpecType -> Target Symbol Source # decode :: Symbol -> SpecType -> Target (Maybe a) Source # check :: Maybe a -> SpecType -> Target (Bool, Expr) Source # toExpr :: Maybe a -> Expr Source # getType :: Proxy * (Maybe a) -> Sort Source #
(Targetable a, Targetable b) => Targetable (Either a b) Source #
Methods query :: Proxy * (Either a b) -> Depth -> Symbol -> SpecType -> Target Symbol Source # decode :: Symbol -> SpecType -> Target (Either a b) Source # check :: Either a b -> SpecType -> Target (Bool, Expr) Source # toExpr :: Either a b -> Expr Source # getType :: Proxy * (Either a b) -> Sort Source #
(Targetable a, Targetable b) => Targetable (a, b) Source #
Methods query :: Proxy * (a, b) -> Depth -> Symbol -> SpecType -> Target Symbol Source # decode :: Symbol -> SpecType -> Target (a, b) Source # check :: (a, b) -> SpecType -> Target (Bool, Expr) Source # toExpr :: (a, b) -> Expr Source # getType :: Proxy * (a, b) -> Sort Source #
(Targetable a, Targetable b, Targetable c) => Targetable (a, b, c) Source #
Methods query :: Proxy * (a, b, c) -> Depth -> Symbol -> SpecType -> Target Symbol Source # decode :: Symbol -> SpecType -> Target (a, b, c) Source # check :: (a, b, c) -> SpecType -> Target (Bool, Expr) Source # toExpr :: (a, b, c) -> Expr Source # getType :: Proxy * (a, b, c) -> Sort Source #
(Targetable a, Targetable b, Targetable c, Targetable d) => Targetable (a, b, c, d) Source #
Methods query :: Proxy * (a, b, c, d) -> Depth -> Symbol -> SpecType -> Target Symbol Source # decode :: Symbol -> SpecType -> Target (a, b, c, d) Source # check :: (a, b, c, d) -> SpecType -> Target (Bool, Expr) Source # toExpr :: (a, b, c, d) -> Expr Source # getType :: Proxy * (a, b, c, d) -> Sort Source #

data TargetOpts Source #

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 Source #
Methods ask :: Target TargetOpts # local :: (TargetOpts -> TargetOpts) -> Target a -> Target a # reader :: (TargetOpts -> a) -> Target a #

defaultOpts :: TargetOpts Source #

data Test Source #

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