| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
Cryptol.Testing.Random
Description
This module generates random values for Cryptol types.
Synopsis
- type Gen g x = Integer -> g -> (SEval x (GenValue x), g)
- randomValue :: (Backend sym, RandomGen g) => sym -> TValue -> Maybe (Gen g sym)
- dumpableType :: forall g. RandomGen g => TValue -> Maybe [Gen g Concrete]
- testableType :: RandomGen g => TValue -> Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
- data TestResult
- = Pass
- | FailFalse [Value]
- | FailError EvalErrorEx [Value]
- isPass :: TestResult -> Bool
- returnTests :: RandomGen g => g -> [Gen g Concrete] -> Value -> Int -> IO [([Value], Value)]
- exhaustiveTests :: MonadIO m => (Integer -> m ()) -> Value -> [[Value]] -> m (TestResult, Integer)
- randomTests :: (MonadIO m, RandomGen g) => (Integer -> m ()) -> Integer -> Value -> [Gen g Concrete] -> g -> m (TestResult, Integer)
Documentation
randomValue :: (Backend sym, RandomGen g) => sym -> TValue -> Maybe (Gen g sym) Source #
A generator for values of the given type. This fails if we are given a type that lacks a suitable random value generator.
dumpableType :: forall g. RandomGen g => TValue -> Maybe [Gen g Concrete] Source #
Given a (function) type, compute generators for the function's arguments.
testableType :: RandomGen g => TValue -> Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete]) Source #
Given a (function) type, compute data necessary for random or exhaustive testing.
The first returned component is a count of the number of possible input test vectors, if the input types are finite. The second component is a list of all the types of the function inputs. The third component is a list of all input test vectors for exhaustive testing. This will be empty unless the input types are finite. The final argument is a list of generators for the inputs of the function.
This function will return Nothing if the input type does not
eventually return Bit, or if we cannot compute a generator
for one of the inputs.
data TestResult Source #
A test result is either a pass, a failure due to evaluating to
False, or a failure due to an exception raised during evaluation
Constructors
| Pass | |
| FailFalse [Value] | |
| FailError EvalErrorEx [Value] |
isPass :: TestResult -> Bool Source #
Arguments
| :: RandomGen g | |
| => g | The random generator state |
| -> [Gen g Concrete] | Generators for the function arguments |
| -> Value | The function itself |
| -> Int | How many tests? |
| -> IO [([Value], Value)] | A list of pairs of random arguments and computed outputs |
Return a collection of random tests.
Arguments
| :: MonadIO m | |
| => (Integer -> m ()) | progress callback |
| -> Value | function under test |
| -> [[Value]] | exhaustive set of test values |
| -> m (TestResult, Integer) |