| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Test.Target.Targetable
- class Targetable a where
- unfold :: Symbol -> SpecType -> Target [(Symbol, SpecType)]
- apply :: Symbol -> [Expr] -> Target Expr
- unapply :: Symbol -> Target (Symbol, [Symbol])
- oneOf :: Symbol -> [(Expr, Expr)] -> Target ()
- whichOf :: Symbol -> Target Symbol
- constrain :: Pred -> Target ()
- ofReft :: Reft -> Expr -> Pred
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
Minimal complete definition
Nothing
Methods
query :: Proxy a -> Depth -> SpecType -> Target Symbol Source
Construct an SMT query describing all values of the given type up to the
given Depth.
Arguments
| :: Symbol | the symbolic variable corresponding to the root of the value |
| -> SpecType | the type of values we're generating (you can probably ignore this) |
| -> Target a |
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).
Instances
| Targetable Bool | |
| Targetable Char | |
| Targetable Int | |
| Targetable Integer | |
| Targetable Word8 | |
| Targetable () | |
| Targetable a => Targetable [a] | |
| Targetable a => Targetable (Maybe a) | |
| (Targetable a, Targetable b, Targetable c, Targetable d, (~) * d (Res (a -> b -> c -> d))) => Targetable (a -> b -> c -> d) | |
| (Targetable a, Targetable b, Targetable c, (~) * c (Res (a -> b -> c))) => Targetable (a -> b -> c) | |
| (Targetable a, Targetable b, (~) * b (Res (a -> b))) => Targetable (a -> b) | |
| (Targetable a, Targetable b) => Targetable (Either a b) | |
| (Targetable a, Targetable b) => Targetable (a, b) | |
| (Targetable a, Targetable b, Targetable c) => Targetable (a, b, c) | |
| (Targetable a, Targetable b, Targetable c, Targetable d) => Targetable (a, b, c, d) |
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 -> [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.