liquidhaskell-0.8.0.2: Liquid Types for Haskell

Safe HaskellNone
LanguageHaskell98

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 #

data Result Source #

Constructors

Passed !Int 
Failed !String 
Errored !String 

Instances

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

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