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

Language | Haskell2010 |

- 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

Nothing

query :: Proxy a -> Depth -> SpecType -> Target Symbol Source

Construct an SMT query describing all values of the given type up to the
given `Depth`

.

:: 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).

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 `d`

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