-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Generate test-suites from refinement types.
--   
@package target
@version 0.2.0.1

module Test.Target.Expr
eq :: Expr -> Expr -> Pred
ge :: Expr -> Expr -> Pred
le :: Expr -> Expr -> Pred
gt :: Expr -> Expr -> Pred
lt :: Expr -> Expr -> Pred
iff :: Pred -> Pred -> Pred
imp :: Pred -> Pred -> Pred
app :: Symbolic a => a -> [Expr] -> Expr
var :: Symbolic a => a -> Expr
prop :: Expr -> Pred
instance Integral Expr
instance Enum Expr
instance Real Expr
instance Num Expr

module Test.Target.Util
type Depth = Int
io :: MonadIO m => IO a -> m a
myTrace :: Show a => String -> a -> a
reft :: SpecType -> Reft
data HList (a :: [*])
Nil :: HList []
(:::) :: a -> HList bs -> HList (a : bs)
type AllHave (c :: k -> Constraint) (xs :: [k]) = Constraints (Map c xs)
smt2Sort :: Sort -> Text
makeDecl :: Symbol -> Sort -> Text
safeFromJust :: String -> Maybe a -> a
applyPreds :: SpecType -> SpecType -> [(Symbol, SpecType)]
propPsToProp :: [(PVar t3, Ref t (UReft t2) t1)] -> Ref t (UReft t2) t1 -> Ref t (UReft t2) t1
propPToProp :: (PVar t3, Ref t (UReft t2) t1) -> Ref t (UReft t2) t1 -> Ref t (UReft t2) t1
stripQuals :: SpecType -> SpecType
fourth4 :: (t, t1, t2, t3) -> t3
getSpec :: [String] -> FilePath -> IO GhcSpec
runGhc :: [String] -> Ghc a -> IO a
loadModule :: FilePath -> Ghc ModSummary
instance (AllHave Show as) => Show (HList as)

module Test.Target.Types
data TargetException
SmtFailedToProduceOutput :: TargetException
SmtError :: String -> TargetException
ExpectedValues :: Response -> TargetException
PreconditionCheckFailed :: String -> TargetException
EvalError :: String -> TargetException
ensureValues :: MonadThrow m => m Response -> m Response
type Constraint = [Pred]
type Variable = (Symbol, Sort)
type Value = Text
type DataConEnv = [(Symbol, SpecType)]
type MeasureEnv = [Measure SpecType DataCon]
boolsort :: Sort
choicesort :: Sort
data Result
Passed :: !Int -> Result
Failed :: !String -> Result
Errored :: !String -> Result
instance Typeable TargetException
instance Typeable Result
instance Show Result
instance SMTLIB2 Constraint
instance Symbolic Variable
instance Exception TargetException
instance Show TargetException

module Test.Target.Monad
whenVerbose :: Target () -> Target ()
noteUsed :: (Symbol, Value) -> Target ()
addDep :: Symbol -> Expr -> Target ()
addConstraint :: Pred -> Target ()
addConstructor :: Variable -> Target ()
inModule :: Symbol -> Target a -> Target a
making :: Sort -> Target a -> Target a

-- | Find the refined type of a data constructor.
lookupCtor :: Symbol -> Target SpecType

-- | Given a data constructor <tt>d</tt> and an action, create a new choice
--   variable <tt>c</tt> and execute the action while guarding any
--   generated constraints with <tt>c</tt>. Returns <tt>(action-result,
--   c)</tt>.
guarded :: String -> Target Expr -> Target (Expr, Expr)

-- | Generate a fresh variable of the given <a>Sort</a>.
fresh :: Sort -> Target Symbol

-- | Given a data constructor <tt>d</tt>, create a new choice variable
--   corresponding to <tt>d</tt>.
freshChoice :: String -> Target Symbol
freshInt :: Target Int

-- | Ask the SMT solver for the <a>Value</a> of the given variable.
getValue :: Symbol -> Target Value
data Target a
runTarget :: TargetOpts -> TargetState -> Target a -> IO a
data TargetState
TargetState :: ![Variable] -> ![Variable] -> !Constraint -> !(HashMap Symbol [Symbol]) -> ![(Symbol, Value)] -> ![(Symbol, DataConP)] -> !DataConEnv -> !MeasureEnv -> !(TCEmb TyCon) -> !(HashMap TyCon RTyCon) -> ![(Symbol, Symbol)] -> ![Variable] -> ![(Symbol, SpecType)] -> !(Maybe Symbol) -> !(HashSet Sort) -> !Symbol -> !FilePath -> !Sort -> !Context -> TargetState
variables :: TargetState -> ![Variable]
choices :: TargetState -> ![Variable]
constraints :: TargetState -> !Constraint
deps :: TargetState -> !(HashMap Symbol [Symbol])
realized :: TargetState -> ![(Symbol, Value)]
dconEnv :: TargetState -> ![(Symbol, DataConP)]
ctorEnv :: TargetState -> !DataConEnv
measEnv :: TargetState -> !MeasureEnv
embEnv :: TargetState -> !(TCEmb TyCon)
tyconInfo :: TargetState -> !(HashMap TyCon RTyCon)
freesyms :: TargetState -> ![(Symbol, Symbol)]
constructors :: TargetState -> ![Variable]
sigs :: TargetState -> ![(Symbol, SpecType)]
chosen :: TargetState -> !(Maybe Symbol)
sorts :: TargetState -> !(HashSet Sort)
modName :: TargetState -> !Symbol
filePath :: TargetState -> !FilePath
makingTy :: TargetState -> !Sort
smtContext :: TargetState -> !Context
initState :: FilePath -> GhcSpec -> Context -> TargetState
data TargetOpts
TargetOpts :: !Int -> !SMTSolver -> !Bool -> !Bool -> !Bool -> !(Maybe Int) -> !Bool -> ![String] -> TargetOpts
depth :: TargetOpts -> !Int
solver :: TargetOpts -> !SMTSolver
verbose :: TargetOpts -> !Bool
logging :: TargetOpts -> !Bool

-- | whether to keep going after finding a counter-example, useful for
--   checking coverage
keepGoing :: TargetOpts -> !Bool

-- | whether to stop after a certain number of successful tests, or
--   enumerate the whole input space
maxSuccess :: TargetOpts -> !(Maybe Int)

-- | whether to use SmallCheck's notion of depth
scDepth :: TargetOpts -> !Bool

-- | extra options to pass to GHC
ghcOpts :: TargetOpts -> ![String]
defaultOpts :: TargetOpts
instance Lift TargetOpts
instance Lift SMTSolver
instance Functor Target
instance Applicative Target
instance Monad Target
instance MonadIO Target
instance Alternative Target
instance MonadState TargetState Target
instance MonadCatch Target
instance MonadReader TargetOpts Target
instance MonadThrow Target
instance Symbolic Text

module Test.Target.Eval

-- | Evaluate a refinement with the given expression substituted for the
--   value variable.
eval :: Reft -> Expr -> Target Bool

-- | Evaluate a refinement with the given expression substituted for the
--   value variable, in the given environment of free symbols.
evalWith :: HashMap Symbol Expr -> Reft -> Expr -> Target Bool

module Test.Target.Targetable

-- | 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 <a>GHC.Generics</a>, e.g.
--   
--   <pre>
--   import GHC.Generics
--   import Test.Target.Targetable
--   
--   data Foo = ... deriving Generic
--   instance Targetable Foo
--   </pre>
class Targetable a where getType _ = FObj $ qualifiedDatatypeName (undefined :: Rep a a) query p = gquery (reproxyRep p) toExpr = gtoExpr . from decode v _ = do { x <- whichOf v; (c, fs) <- unapply x; to <$> gdecode c fs } check v t = gcheck (from v) t
query :: Targetable a => Proxy a -> Depth -> SpecType -> Target Symbol
decode :: Targetable a => Symbol -> SpecType -> Target a
check :: Targetable a => a -> SpecType -> Target (Bool, Expr)
toExpr :: Targetable a => a -> Expr
getType :: Targetable a => Proxy a -> Sort

-- | Given a data constuctor <tt>d</tt> and a refined type for <tt>d</tt>s
--   output, return a list of types representing suitable arguments for
--   <tt>d</tt>.
unfold :: Symbol -> SpecType -> Target [(Symbol, SpecType)]

-- | Given a data constructor <tt>d</tt> and a list of expressions
--   <tt>xs</tt>, construct a new expression corresponding to <tt>d
--   xs</tt>.
apply :: Symbol -> [Expr] -> Target Expr

-- | Split a symbolic variable representing the application of a data
--   constructor into a pair of the data constructor and the sub-variables.
unapply :: Symbol -> Target (Symbol, [Symbol])

-- | Given a symbolic variable and a list of <tt>(choice, var)</tt> pairs,
--   <tt>oneOf x choices</tt> asserts that <tt>x</tt> must equal one of the
--   <tt>var</tt>s in <tt>choices</tt>.
oneOf :: Symbol -> [(Expr, Expr)] -> Target ()

-- | Given a symbolic variable <tt>x</tt>, figure out which of <tt>x</tt>s
--   choice varaibles was picked and return it.
whichOf :: Symbol -> Target Symbol

-- | Assert a logical predicate, guarded by the current choice variable.
constrain :: Pred -> Target ()

-- | Given a refinement <tt>{v | p}</tt> and an expression <tt>e</tt>,
--   construct the predicate <tt>p[e/v]</tt>.
ofReft :: Reft -> Expr -> Pred
instance GCheckFields U1
instance GDecodeFields U1
instance GQueryFields U1
instance GRecursive U1
instance GToExprFields U1
instance GCheckFields f => GCheckFields (S1 c f)
instance GDecodeFields f => GDecodeFields (S1 c f)
instance GQuery f => GQueryFields (S1 c f)
instance Targetable a => GRecursive (S1 c (K1 i a))
instance GToExpr f => GToExprFields (S1 c f)
instance (GCheckFields f, GCheckFields g) => GCheckFields (f :*: g)
instance (GDecodeFields f, GDecodeFields g) => GDecodeFields (f :*: g)
instance (GQueryFields f, GQueryFields g) => GQueryFields (f :*: g)
instance (GRecursive f, GRecursive g) => GRecursive (f :*: g)
instance (GToExprFields f, GToExprFields g) => GToExprFields (f :*: g)
instance (Constructor c, GCheckFields f) => GCheck (C1 c f)
instance (Constructor c, GDecodeFields f) => GDecode (C1 c f)
instance (Constructor c, GRecursive f, GQueryFields f) => GQueryCtors (C1 c f)
instance (Constructor c, GToExprFields f) => GToExprCtor (C1 c f)
instance (GCheck f, GCheck g) => GCheck (f :+: g)
instance (GDecode f, GDecode g) => GDecode (f :+: g)
instance (GQueryCtors f, GQueryCtors g) => GQueryCtors (f :+: g)
instance (GToExprCtor f, GToExprCtor g) => GToExprCtor (f :+: g)
instance Targetable a => GCheckFields (K1 i a)
instance Targetable a => GDecodeFields (K1 i a)
instance Targetable a => GQuery (K1 i a)
instance Targetable a => GToExpr (K1 i a)
instance (Datatype c, GCheck f) => GCheck (D1 c f)
instance (Datatype c, GDecode f) => GDecode (D1 c f)
instance (Datatype c, GQueryCtors f) => GQuery (D1 c f)
instance (Datatype c, GToExprCtor f) => GToExpr (D1 c f)
instance (Targetable a, Targetable b, Targetable c, Targetable d) => Targetable (a, b, c, d)
instance (Targetable a, Targetable b, Targetable c) => Targetable (a, b, c)
instance (Targetable a, Targetable b) => Targetable (a, b)
instance (Targetable a, Targetable b) => Targetable (Either a b)
instance Targetable a => Targetable (Maybe a)
instance Targetable a => Targetable [a]
instance Targetable Bool
instance Targetable Word8
instance Targetable Char
instance Targetable Integer
instance Targetable Int
instance Targetable ()

module Test.Target.Testable

-- | Test that a function inhabits the given refinement type by enumerating
--   valid inputs and calling the function on the inputs.
test :: Testable f => f -> SpecType -> Target Result

-- | A class of functions that Target can test. A function is
--   <tt>Testable</tt> <i>iff</i> all of its component types are
--   <a>Targetable</a> and all of its argument types are <a>Show</a>able.
--   
--   You should <b>never</b> have to define a new <a>Testable</a> instance.
class (AllHave Targetable (Args f), Targetable (Res f), AllHave Show (Args f)) => Testable f
instance [overlap ok] (Targetable a, Args a ~ '[], Res a ~ a) => Testable a
instance [overlap ok] (Show a, Targetable a, Testable b) => Testable (a -> b)

module Test.Target.Targetable.Function
instance [overlap ok] (Targetable a, Targetable b, Targetable c, Targetable d, d ~ Res (a -> b -> c -> d)) => Targetable (a -> b -> c -> d)
instance [overlap ok] (Targetable a, Targetable b, Targetable c, c ~ Res (a -> b -> c)) => Targetable (a -> b -> c)
instance [overlap ok] (Targetable a, Targetable b, b ~ Res (a -> b)) => Targetable (a -> b)

module Test.Target

-- | Test whether a function inhabits its refinement type by enumerating
--   valid inputs and calling the function.
target :: Testable f => f -> String -> FilePath -> IO ()

-- | Like <a>target</a>, but returns the <a>Result</a> instead of printing
--   to standard out.
targetResult :: Testable f => f -> String -> FilePath -> IO Result

-- | Like <a>target</a>, but accepts options to control the enumeration
--   depth, solver, and verbosity.
targetWith :: Testable f => f -> String -> FilePath -> TargetOpts -> IO ()

-- | Like <a>targetWith</a>, but returns the <a>Result</a> instead of
--   printing to standard out.
targetResultWith :: Testable f => f -> String -> FilePath -> TargetOpts -> IO Result
targetTH :: Name -> FilePath -> ExpQ
targetResultTH :: Name -> FilePath -> ExpQ
targetWithTH :: Name -> FilePath -> TargetOpts -> ExpQ
targetResultWithTH :: Name -> FilePath -> TargetOpts -> ExpQ
data Result
Passed :: !Int -> Result
Failed :: !String -> Result
Errored :: !String -> Result

-- | A class of functions that Target can test. A function is
--   <tt>Testable</tt> <i>iff</i> all of its component types are
--   <a>Targetable</a> and all of its argument types are <a>Show</a>able.
--   
--   You should <b>never</b> have to define a new <a>Testable</a> instance.
class (AllHave Targetable (Args f), Targetable (Res f), AllHave Show (Args f)) => Testable f

-- | 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 <a>GHC.Generics</a>, e.g.
--   
--   <pre>
--   import GHC.Generics
--   import Test.Target.Targetable
--   
--   data Foo = ... deriving Generic
--   instance Targetable Foo
--   </pre>
class Targetable a where getType _ = FObj $ qualifiedDatatypeName (undefined :: Rep a a) query p = gquery (reproxyRep p) toExpr = gtoExpr . from decode v _ = do { x <- whichOf v; (c, fs) <- unapply x; to <$> gdecode c fs } check v t = gcheck (from v) t
query :: Targetable a => Proxy a -> Depth -> SpecType -> Target Symbol
decode :: Targetable a => Symbol -> SpecType -> Target a
check :: Targetable a => a -> SpecType -> Target (Bool, Expr)
toExpr :: Targetable a => a -> Expr
getType :: Targetable a => Proxy a -> Sort
data TargetOpts
TargetOpts :: !Int -> !SMTSolver -> !Bool -> !Bool -> !Bool -> !(Maybe Int) -> !Bool -> ![String] -> TargetOpts
depth :: TargetOpts -> !Int
solver :: TargetOpts -> !SMTSolver
verbose :: TargetOpts -> !Bool
logging :: TargetOpts -> !Bool

-- | whether to keep going after finding a counter-example, useful for
--   checking coverage
keepGoing :: TargetOpts -> !Bool

-- | whether to stop after a certain number of successful tests, or
--   enumerate the whole input space
maxSuccess :: TargetOpts -> !(Maybe Int)

-- | whether to use SmallCheck's notion of depth
scDepth :: TargetOpts -> !Bool

-- | extra options to pass to GHC
ghcOpts :: TargetOpts -> ![String]
defaultOpts :: TargetOpts
data Test
T :: t -> Test

-- | Monomorphise an arbitrary property by defaulting all type variables to
--   <a>Integer</a>.
--   
--   For example, if <tt>f</tt> has type <tt><a>Ord</a> a =&gt; [a] -&gt;
--   [a]</tt> then <tt>$(<a>monomorphic</a> 'f)</tt> has type
--   <tt>[<a>Integer</a>] -&gt; [<a>Integer</a>]</tt>.
--   
--   If you want to use <a>monomorphic</a> in the same file where you
--   defined the property, the same scoping problems pop up as in
--   <a>quickCheckAll</a>: see the note there about <tt>return []</tt>.
monomorphic :: Name -> ExpQ