Safe Haskell | None |
---|---|

Language | Haskell98 |

- class Targetable a where
- qquery :: Targetable a => Proxy a -> Int -> SpecType -> Target Symbol
- unfold :: Symbol -> SpecType -> Target [(Symbol, SpecType)]
- apply :: Symbol -> SpecType -> [Expr] -> Target Expr
- unapply :: Symbol -> Target (Symbol, [Symbol])
- oneOf :: Symbol -> [(Expr, Expr)] -> Target ()
- whichOf :: Symbol -> Target Symbol
- constrain :: (?loc :: CallStack) => Expr -> Target ()
- ofReft :: Reft -> Expr -> Expr

# 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

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.

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.

Targetable Bool Source # | |

Targetable Char Source # | |

Targetable Int Source # | |

Targetable Integer Source # | |

Targetable Word8 Source # | |

Targetable () Source # | |

Targetable a => Targetable [a] Source # | |

Targetable a => Targetable (Maybe a) Source # | |

(Targetable a, Targetable b) => Targetable (Either a b) Source # | |

(Targetable a, Targetable b) => Targetable (a, b) Source # | |

(Targetable a, Targetable b, Targetable c) => Targetable (a, b, c) Source # | |

(Targetable a, Targetable b, Targetable c, Targetable d) => Targetable (a, b, c, d) Source # | |

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

Given a data constuctor `d`

and a refined type for `d`

s 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 `var`

s in
`choices`

.

whichOf :: Symbol -> Target Symbol Source #

Given a symbolic variable `x`

, figure out which of `x`

s choice varaibles
was picked and return it.