Safe Haskell	None
Language	Haskell98

Test.Target.Targetable

Synopsis

Documentation

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 #

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

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

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

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

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

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

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

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

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

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

ofReft :: Reft -> Expr -> Expr Source #

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