cryptol-2.2.6: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2015 Galois, Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.Testing.Random

Description

This module generates random values for Cryptol types.

Synopsis

- type Gen g = Int -> g -> (Value, g)
- runOneTest :: RandomGen g => Value -> [Gen g] -> Int -> g -> IO (TestResult, g)
- testableType :: RandomGen g => Type -> Maybe [Gen g]
- randomValue :: RandomGen g => Type -> Maybe (Gen g)
- randomBit :: RandomGen g => Gen g
- randomWord :: RandomGen g => Integer -> Gen g
- randomStream :: RandomGen g => Gen g -> Gen g
- randomSequence :: RandomGen g => Integer -> Gen g -> Gen g
- randomTuple :: RandomGen g => [Gen g] -> Gen g
- randomRecord :: RandomGen g => [(Name, Gen g)] -> Gen g

# Documentation

type Gen g = Int -> g -> (Value, g) Source

runOneTest Source

Arguments

:: RandomGen g |
=> Value | Function under test
-> [Gen g] | Argument generators
-> Int | Size
-> g |
-> IO (TestResult, g) |

Apply a testable value to some randomly-generated arguments. Returns `Nothing` if the function returned `True`, or `Just counterexample` if it returned `False`.

Please note that this function assumes that the generators match the supplied value, otherwise we'll panic.

testableType :: RandomGen g => Type -> Maybe [Gen g] Source

Given a (function) type, compute generators for the function's arguments. Currently we do not support polymorphic functions. In principle, we could apply these to random types, and test the results.

randomValue :: RandomGen g => Type -> Maybe (Gen g) Source

A generator for values of the given type. This fails if we are given a type that lacks a suitable random value generator.

randomBit :: RandomGen g => Gen g Source

Generate a random bit value.

randomWord :: RandomGen g => Integer -> Gen g Source

Generate a random word of the given length (i.e., a value of type `[w]`) The size parameter is assumed to vary between 1 and 100, and we use it to generate smaller numbers first.

randomStream :: RandomGen g => Gen g -> Gen g Source

Generate a random infinite stream value.

randomSequence :: RandomGen g => Integer -> Gen g -> Gen g Source

Generate a random sequence. Generally, this should be used for sequences other than bits. For sequences of bits use "randomWord". The difference is mostly about how the results will be displayed.

randomTuple :: RandomGen g => [Gen g] -> Gen g Source

Generate a random tuple value.

randomRecord :: RandomGen g => [(Name, Gen g)] -> Gen g Source

Generate a random record value.