Skip to content

Instantly share code, notes, and snippets.

@moodmosaic moodmosaic/LightCheck.fs
Last active Oct 16, 2017

Embed
What would you like to do?
Learn more about clone URLs
Download ZIP
Raw
LightCheck.fs
// Port of Haskell
// - https://hackage.haskell.org/package/QuickCheck-1.2.0.1
// - https://hackage.haskell.org/package/random-1.1
namespace LightCheck
/// <summary>
/// This module deals with the common task of pseudo-random number generation.
/// It makes it possible to generate repeatable results, by starting with a
/// specified initial random number generator, or to get different results on
/// each run by using the system-initialised generator or by supplying a seed
/// from some other source.
/// </summary>
/// <remarks>
/// This implementation uses the Portable Combined Generator of L'Ecuyer for
/// 32-bit computers, transliterated by Lennart Augustsson. It has a period of
/// roughly 2.30584e18.
/// </remarks>
[<AutoOpen>]
module internal Random =
type StdGen =
private
| StdGen of int * int
/// <summary>
/// The next operation returns an Int that is uniformly distributed in the
/// rangge of at least 30 bits, and a new generator. The result of repeatedly
/// using next should be at least as statistically robust as the Minimal
/// Standard Random Number Generator. Until more is known about implementations
/// of split, all we require is that split deliver generators that are (a) not
/// identical and (b) independently robust in the sense just given.
/// </summary>
let private next (StdGen (s1, s2)) =
let k = s1 / 53668
let k' = s2 / 52774
let s1' = 40014 * (s1 - k * 53668) - k * 12211
let s2' = 40692 * (s2 - k' * 52774) - k' * 3791
let s1'' = if s1' < 0 then s1' + 2147483563 else s1'
let s2'' = if s2' < 0 then s2' + 2147483399 else s2'
let z = s1'' - s2''
let z' = if z < 1 then z + 2147483562 else z
(z', StdGen (s1'', s2''))
/// <summary>
/// The split operation allows one to obtain two distinct random number
/// generators. This is very useful in functional programs (for example, when
/// passing a random number generator down to recursive calls), but very little
/// work has been done on statistically robust implementations of split.
/// </summary>
let split (StdGen (s1, s2) as std) =
let s1' = if s1 = 2147483562 then 1 else s1 + 1
let s2' = if s2 = 1 then 2147483398 else s2 - 1
let (StdGen (t1, t2)) = next std |> snd
(StdGen (s1', t2), StdGen (t1, s2'))
/// <summary>
/// The range operation takes a range (lo,hi) and a random number generator g,
/// and returns a random value, uniformly distributed, in the closed interval
/// [lo,hi], together with a new generator.
/// </summary>
/// <remarks>
/// It is unspecified what happens if lo > hi. For continuous types there is no
/// requirement that the values lo and hi are ever produced, although they very
/// well may be, depending on the implementation and the interval.
/// </remarks>
let rec range (l, h) rng =
if l > h then range (h, l) rng
else
let (l', h') = (32767, 2147483647)
let b = h' - l' + 1
let q = 1000
let k = h - l + 1
let magnitude = k * q
let rec f c v g =
if c >= magnitude then (v, g)
else
let (x, g') = next g
let v' = (v * b + (x - l'))
f (c * b) v' g'
let (v, rng') = f 1 0 rng
(l + v % k), rng'
let private r = int System.DateTime.UtcNow.Ticks |> System.Random
/// <summary>
/// Provides a way of producing an initial generator using a random seed.
/// </summary>
let createNew() =
let s = r.Next() &&& 2147483647
let (q, s1) = (s / 2147483562, s % 2147483562)
let s2 = q % 2147483398
StdGen (s1 + 1, s2 + 1)
/// <summary>
/// LightCheck exports some basic generators, and some combinators for making
/// new ones. Gen of 'a is the type for generators of 'a's and essentially is
/// a State Monad combining a pseudo-random generation seed, and a size value
/// for data structures (i.e. list length).
/// Using the type Gen of 'a, we can specify at the same time a set of values
/// that can be generated and a probability distribution on that set.
///
/// Read more about how it works here:
/// http://www.dcc.fc.up.pt/~pbv/aulas/tapf/slides/quickcheck.html#the-gen-monad
/// http://quviq.com/documentation/eqc/index.html
/// </summary>
module Gen =
/// <summary>
/// A generator for values of type 'a.
/// </summary>
type Gen<'a> =
private
| Gen of (int -> StdGen -> 'a)
/// <summary>
/// Sequentially compose two actions, passing any value produced by the first
/// as an argument to the second.
/// </summary>
/// <param name="f">
/// The action that produces a value to be passed as argument to the generator.
/// </param>
let bind (Gen m) f =
Gen(fun n r ->
let (r1, r2) = r |> Random.split
let (Gen m') = f (m n r1)
m' n r2)
/// <summary>
/// Injects a value into a generator.
/// </summary>
/// <param name="a">The value to inject into a generator.</param>
let init a = Gen(fun n r -> a)
/// <summary>
/// Returns a new generator obtained by applying a function to an existing
/// generator.
/// </summary>
/// <param name="f">The function to apply to an existing generator.</param>
/// <param name="m">The existing generator.</param>
let map f m =
bind m (fun m' ->
init (f m'))
/// <summary>
/// Generates a random element in the given inclusive range, uniformly
/// distributed in the closed interval [lo,hi].
/// </summary>
/// <param name="lo">The lower bound.</param>
/// <param name="hi">The upper bound.</param>
let choose (lo, hi) = Gen(fun n r -> r) |> map (Random.range (lo, hi) >> fst)
/// <summary>
/// Generates one of the given values.
/// </summary>
/// <param name="xs">The input list.</param>
/// <remarks>
/// The input list must be non-empty.
/// </remarks>
let elements xs =
// http://stackoverflow.com/a/1817654/467754
let flip f x y = f y x
choose (0, (Seq.length xs) - 1) |> map (flip Seq.item xs)
/// <summary>
/// Randomly uses one of the given generators.
/// </summary>
/// <param name="gens">The input list of generators to use.</param>
/// <remarks>
/// The input list must be non-empty.
/// </remarks>
let oneof gens =
let join x = bind x id
join (elements gens)
/// <summary>
/// Used to construct generators that depend on the size parameter.
/// </summary>
/// <param name="g">A generator for values of type 'a.</param>
let sized g =
Gen(fun n r ->
let (Gen m) = g n
m n r)
/// <summary>
/// Overrides the size parameter. Returns a generator which uses the given size
/// instead of the runtime-size parameter.
/// </summary>
/// <param name="n">The size that's going to override the runtime-size.</param>
let resize n (Gen m) = Gen(fun _ r -> m n r)
/// <summary>
/// Takes a list of generators of type 'a, evaluates each one of them, and
/// collect the result, into a new generator of type 'a list.
/// </summary>
/// <param name="l">The list of generators of type 'a.</param>
/// <remarks>
/// This is written so that the F# compiler will use a tail call, as shown in
/// the resulting excerpt of generated IL:
/// IL_0000: nop
/// IL_0001: call class [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<cl...
/// IL_0006: ldarg.0
/// IL_0007: call class [FSharp.Core]Microsoft.FSharp.Collections.FSharpLi...
/// IL_000c: call class LightCheck.Gen/Gen`1<!!0> LightCheck.Gen::'init'<c...
/// IL_0011: tail.
/// IL_0013: call !!1 [FSharp.Core]Microsoft.FSharp.Collections.ListModule...
/// IL_0018: ret
/// See also:
/// http://stackoverflow.com/a/6615060/467754,
/// http://stackoverflow.com/a/35132220/467754
/// </remarks>
let sequence l =
let k m m' =
bind m (fun x ->
bind m' (fun xs ->
init (x :: xs)))
init [] |> List.foldBack k l
/// <summary>
/// Generates a list of the given length.
/// </summary>
/// <param name="n">The number of elements to replicate.</param>
/// <param name="g">The generator to replicate.</param>
let vector n g =
sequence [ for _ in [ 1..n ] -> g ]
[<AutoOpen>]
module Builder =
type GenBuilder() =
member this.Bind (g1, g2) = bind g1 g2
member this.Return (x) = init x
member this.ReturnFrom (f) = f
let gen = GenBuilder()
/// <summary>
/// Generates a list of random length. The maximum length of the list depends
/// on the size parameter.
/// </summary>
/// <param name="g">The generator from which to create a list from.</param>
let list g = sized (fun s -> gen { let! n = choose (0, s)
return! vector n g })
/// <summary>
/// Unpacks a function wrapped inside a generator, applying it into a new
/// generator.
/// </summary>
/// <param name="f">The function wrapped inside a generator.</param>
/// <param name="m">The generator, to apply the function to.</param>
let apply f m =
bind f (fun f' ->
bind m (fun m' ->
init (f' m')))
/// <summary>
/// Returns a new generator obtained by applying a function to three existing
/// generators.
/// </summary>
/// <param name="f">The function to apply to the existing generators.</param>
/// <param name="m1">The existing generator.</param>
/// <param name="m2">The existing generator.</param>
/// <param name="m3">The existing generator.</param>
let lift3 f m1 m2 m3 = apply (apply (apply (init f) m1) m2) m3
/// <summary>
/// Generates a random byte.
/// </summary>
let byte = choose (0, 255) |> map Operators.byte
/// <summary>
/// Generates a random character.
/// </summary>
let char =
oneof [ choose ( 32, 126)
choose (127, 255) ]
|> map Operators.char
/// <summary>
/// Generates a random boolean.
/// </summary>
let bool =
oneof [ init true
init false ]
/// <summary>
/// Generates a 32-bit integer (with absolute value bounded by the generation
/// size).
/// </summary>
let int = sized (fun n -> choose (-n, n))
/// <summary>
/// Generates a 64-bit integer (with absolute value bounded by the generation
/// size multiplied by 16-bit integer's largest possible value).
/// </summary>
let int64 = int |> map (fun n -> Operators.int64 (n * 32767))
/// <summary>
/// Generates a random string.
/// </summary>
let string =
char
|> list
|> map (List.toArray >> System.String)
/// <summary>
/// Generates a random real number.
/// </summary>
let float =
let fraction a b c = float a + float b / (abs (float c) + 1.0)
lift3 fraction int int int
/// <summary>
/// Runs a generator. The size passed to the generator is up to 30; if you want
/// another size then you should explicitly use 'resize'.
/// </summary>
let generate (Gen m) =
let (size, rand) = Random.createNew() |> Random.range (0, 30)
m size rand
/// <summary>
/// Generates some example values.
/// </summary>
/// <param name="g">The generator to run for generating example values.</param>
let sample g =
[ for n in [ 0..2..20 ] -> resize n g |> generate ]
/// <summary>
/// This module deals with simplifying counter-examples. A property fails when
/// LightCheck finds a first counter-example. However, randomly-generated data
/// typically contains a lot of noise. Therefore it is a good idea to simplify
/// counter-examples before reporting them. This process is called shrinking.
///
/// Read more about how it works here:
/// http://www.dcc.fc.up.pt/~pbv/aulas/tapf/slides/quickcheck.html#shrinking
/// </summary>
module Shrink =
open FSharp.Core.LanguagePrimitives
/// <summary>
/// A shrinker for values of type 'a.
/// </summary>
type Shrink<'a> =
private
| Shrink of ('a -> 'a seq)
/// <summary>
/// Shrinks towards smaller numeric values.
/// </summary>
/// <param name="n">The numeric value to shrink.</param>
let inline shrinkNumber n =
let genericTwo = GenericOne + GenericOne
n
|> Seq.unfold (fun s -> Some(n - s, s / genericTwo))
|> Seq.tail
|> Seq.append [ GenericZero ]
|> Seq.takeWhile (fun el -> abs n > abs el)
|> Seq.append (if n < GenericZero then Seq.singleton -n
else Seq.empty)
|> Seq.distinct
/// <summary>
/// Shrinks a sequence of elements of type 'a. First it yields an empty
/// sequence, and then it iterates the input sequence, and shrinks each
/// one of the items given the shrinker which is passed as a parameter.
/// </summary>
/// <param name="f">
/// The shrinker function, to be applied on each element of the list.
/// </param>
/// <param name="xs">The input sequence to shrink.</param>
let shrinkList xs (Shrink shr) =
let rec shrinkImp xs =
match xs with
| [] -> Seq.empty
| (h :: t) ->
seq {
yield []
for h' in shr h -> h' :: t
for t' in (shrinkImp t) -> h :: t'
}
shrinkImp xs
module Property =
open Gen
/// <summary>
/// A generator of values Gen<Result>, in order to make it possible to mix and
/// match Property combinators and Gen computations.
/// </summary>
type Property =
private
| Prop of Gen<Result>
and Result =
{ Status : option<bool>
Stamps : list<string>
Args : list<string> }
/// <summary>
/// Returns a value of type Gen Result out of a property. Useful for mixing and
/// matching Property combinators and Gen computations.
/// </summary>
/// <param name="property">A property to extract the Gen Result from.</param>
let evaluate property =
let (Prop result) = property
result
let private boolProperty a =
{ Status = Some a
Stamps = []
Args = [] }
|> Gen.init
|> Prop
let private unitProperty =
{ Status = None
Stamps = []
Args = [] }
|> Gen.init
|> Prop
let private convert candidate =
match box candidate with
| :? Lazy<bool> as b -> boolProperty b.Value
| :? Property as p -> p
| :? bool as b -> boolProperty b
| _ -> unitProperty
/// <summary>
/// Returns a property that holds for all values that can be generated by Gen.
/// </summary>
/// <param name="g">A generator of values for which the property holds.</param>
/// <param name="f">
/// The property for checking whether it holds for all values that can be
/// generated by a given Gen.
/// </param>
let forAll g f =
Prop(gen {
let! arg = g
let! res = f arg
|> convert
|> evaluate
return { res with Args = arg.ToString() :: res.Args }
})
/// <summary>
/// Returns a property that holds under certain conditions. Laws which are
/// simple equations are conveniently represented by boolean function, but in
/// general many laws hold only under certain conditions.
/// This implication combinator represents such conditional laws.
/// </summary>
/// <param name="b">The precondition's predicate result.</param>
/// <param name="a">The actual result, to be turned into a property.</param>
let implies b a =
if b then a |> convert
else () |> convert
/// <summary>
/// Returns a property that holds under certain conditions. Laws which are
/// simple equations are conveniently represented by boolean function, but in
/// general many laws hold only under certain conditions.
/// This implication combinator represents such conditional laws.
/// </summary>
/// <param name="b">The precondition's predicate result.</param>
/// <param name="a">The actual result, to be turned into a property.</param>
let (==>) b a = implies b a
/// <summary>
/// Labels a test case.
/// </summary>
/// <param name="s">The label.</param>
/// <param name="a">The test case.</param>
let label s a =
a
|> evaluate
|> map (fun result -> { result with Stamps = s :: result.Stamps })
|> Prop
/// <summary>
/// Conditionally labels a test case.
/// </summary>
/// <param name="b">
/// The condition to check whether the test case should be labelled.
/// </param>
/// <param name="s">The label.</param>
/// <param name="a">The test case.</param>
let classify b s a =
if b then a |> label s
else () |> convert
/// <summary>
/// Conditionally labels a test case as trivial.
/// </summary>
/// <param name="b">
/// The condition to check whether the test case should be labelled as trivial.
/// </param>
/// <param name="s">The label.</param>
/// <param name="a">The test case.</param>
let trivial b p = classify b "trivial" p
/// <summary>
/// Gathers all values that are passed to it.
/// </summary>
/// <param name="a">The value.</param>
/// <param name="p">The property.</param>
let collect a p = label (a.ToString()) p
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.