cryptol-2.10.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
Safe HaskellTrustworthy



This module generates random values for Cryptol types.



type Gen g x = Integer -> g -> (SEval x (GenValue x), g) Source #

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 TestReport Source #




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


FailFalse [Value] 
FailError EvalError [Value] 

returnTests Source #


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

exhaustiveTests Source #


:: MonadIO m 
=> (Integer -> m ())

progress callback

-> Value

function under test

-> [[Value]]

exhaustive set of test values

-> m (TestResult, Integer) 

randomTests Source #


:: (MonadIO m, RandomGen g) 
=> (Integer -> m ())

progress callback

-> Integer

Maximum number of tests to run

-> Value

function under test

-> [Gen g Concrete]

input value generators

-> g

Inital random generator

-> m (TestResult, Integer)