Test.Target.Targetable

Documentation

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

qquery :: Targetable a => Proxy a -> Int -> SpecType -> Target Symbol

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

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

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

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

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

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

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

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

constrain :: (?loc :: CallStack) => Expr -> Target ()

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

ofReft :: Reft -> Expr -> Expr

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