Skip to content
{{ message }}

Instantly share code, notes, and snippets.

# moodmosaic/LightCheck.fs

Last active Dec 13, 2020
LightCheck is a QuickCheck-based clone, written in F# for educational use.
 // Port of Haskell // - https://hackage.haskell.org/package/QuickCheck-1.2.0.1 // - https://hackage.haskell.org/package/random-1.1 namespace LightCheck /// /// 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. /// /// /// 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. /// [] module internal Random = type StdGen = private | StdGen of int * int /// /// 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. /// 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'')) /// /// 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. /// 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')) /// /// 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. /// /// /// 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. /// 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 /// /// Provides a way of producing an initial generator using a random seed. /// let createNew() = let s = r.Next() &&& 2147483647 let (q, s1) = (s / 2147483562, s % 2147483562) let s2 = q % 2147483398 StdGen (s1 + 1, s2 + 1) /// /// 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 /// module Gen = /// /// A generator for values of type 'a. /// type Gen<'a> = private | Gen of (int -> StdGen -> 'a) /// /// Sequentially compose two actions, passing any value produced by the first /// as an argument to the second. /// /// /// The action that produces a value to be passed as argument to the generator. /// 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) /// /// Injects a value into a generator. /// /// The value to inject into a generator. let init a = Gen(fun n r -> a) /// /// Returns a new generator obtained by applying a function to an existing /// generator. /// /// The function to apply to an existing generator. /// The existing generator. let map f m = bind m (fun m' -> init (f m')) /// /// Generates a random element in the given inclusive range, uniformly /// distributed in the closed interval [lo,hi]. /// /// The lower bound. /// The upper bound. let choose (lo, hi) = Gen(fun n r -> r) |> map (Random.range (lo, hi) >> fst) /// /// Generates one of the given values. /// /// The input list. /// /// The input list must be non-empty. /// 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) /// /// Randomly uses one of the given generators. /// /// The input list of generators to use. /// /// The input list must be non-empty. /// let oneof gens = let join x = bind x id join (elements gens) /// /// Used to construct generators that depend on the size parameter. /// /// A generator for values of type 'a. let sized g = Gen(fun n r -> let (Gen m) = g n m n r) /// /// Overrides the size parameter. Returns a generator which uses the given size /// instead of the runtime-size parameter. /// /// The size that's going to override the runtime-size. let resize n (Gen m) = Gen(fun _ r -> m n r) /// /// 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. /// /// The list of generators of type 'a. /// /// 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 LightCheck.Gen::'init' let sequence l = let k m m' = bind m (fun x -> bind m' (fun xs -> init (x :: xs))) init [] |> List.foldBack k l /// /// Generates a list of the given length. /// /// The number of elements to replicate. /// The generator to replicate. let vector n g = sequence [ for _ in [ 1..n ] -> g ] [] 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() /// /// Generates a list of random length. The maximum length of the list depends /// on the size parameter. /// /// The generator from which to create a list from. let list g = sized (fun s -> gen { let! n = choose (0, s) return! vector n g }) /// /// Unpacks a function wrapped inside a generator, applying it into a new /// generator. /// /// The function wrapped inside a generator. /// The generator, to apply the function to. let apply f m = bind f (fun f' -> bind m (fun m' -> init (f' m'))) /// /// Returns a new generator obtained by applying a function to three existing /// generators. /// /// The function to apply to the existing generators. /// The existing generator. /// The existing generator. /// The existing generator. let lift3 f m1 m2 m3 = apply (apply (apply (init f) m1) m2) m3 /// /// Generates a random byte. /// let byte = choose (0, 255) |> map Operators.byte /// /// Generates a random character. /// let char = oneof [ choose ( 32, 126) choose (127, 255) ] |> map Operators.char /// /// Generates a random boolean. /// let bool = oneof [ init true init false ] /// /// Generates a 32-bit integer (with absolute value bounded by the generation /// size). /// let int = sized (fun n -> choose (-n, n)) /// /// Generates a 64-bit integer (with absolute value bounded by the generation /// size multiplied by 16-bit integer's largest possible value). /// let int64 = int |> map (fun n -> Operators.int64 (n * 32767)) /// /// Generates a random string. /// let string = char |> list |> map (List.toArray >> System.String) /// /// Generates a random real number. /// let float = let fraction a b c = float a + float b / (abs (float c) + 1.0) lift3 fraction int int int /// /// Runs a generator. The size passed to the generator is up to 30; if you want /// another size then you should explicitly use 'resize'. /// let generate (Gen m) = let (size, rand) = Random.createNew() |> Random.range (0, 30) m size rand /// /// Generates some example values. /// /// The generator to run for generating example values. let sample g = [ for n in [ 0..2..20 ] -> resize n g |> generate ] /// /// 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 /// module Shrink = open FSharp.Core.LanguagePrimitives /// /// A shrinker for values of type 'a. /// type Shrink<'a> = private | Shrink of ('a -> 'a seq) /// /// Shrinks towards smaller numeric values. /// /// The numeric value to shrink. 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 /// /// 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. /// /// /// The shrinker function, to be applied on each element of the list. /// /// The input sequence to shrink. 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 /// /// A generator of values Gen, in order to make it possible to mix and /// match Property combinators and Gen computations. /// type Property = private | Prop of Gen and Result = { Status : option Stamps : list Args : list } /// /// Returns a value of type Gen Result out of a property. Useful for mixing and /// matching Property combinators and Gen computations. /// /// A property to extract the Gen Result from. 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 as b -> boolProperty b.Value | :? Property as p -> p | :? bool as b -> boolProperty b | _ -> unitProperty /// /// Returns a property that holds for all values that can be generated by Gen. /// /// A generator of values for which the property holds. /// /// The property for checking whether it holds for all values that can be /// generated by a given Gen. /// let forAll g f = Prop(gen { let! arg = g let! res = f arg |> convert |> evaluate return { res with Args = arg.ToString() :: res.Args } }) /// /// 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. /// /// The precondition's predicate result. /// The actual result, to be turned into a property. let implies b a = if b then a |> convert else () |> convert /// /// 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. /// /// The precondition's predicate result. /// The actual result, to be turned into a property. let (==>) b a = implies b a /// /// Labels a test case. /// /// The label. /// The test case. let label s a = a |> evaluate |> map (fun result -> { result with Stamps = s :: result.Stamps }) |> Prop /// /// Conditionally labels a test case. /// /// /// The condition to check whether the test case should be labelled. /// /// The label. /// The test case. let classify b s a = if b then a |> label s else () |> convert /// /// Conditionally labels a test case as trivial. /// /// /// The condition to check whether the test case should be labelled as trivial. /// /// The label. /// The test case. let trivial b p = classify b "trivial" p /// /// Gathers all values that are passed to it. /// /// The value. /// The property. let collect a p = label (a.ToString()) p
to join this conversation on GitHub. Already have an account? Sign in to comment