Skip to content

Commit

Permalink
Merge pull request #29 from jystic/topic/zero-not-ideal
Browse files Browse the repository at this point in the history 
Support for 'where' and 'counterexample' custom operations
  • Loading branch information
@jacobstanley
jacobstanley authored Oct 16, 2016
2 parents 3fa181e + 5c4fb3c commit da6fd28
Show file tree
Hide file tree
Showing 2 changed files with 158 additions and 72 deletions.
204 changes: 144 additions & 60 deletions Jack/Property.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,83 +2,153 @@

open FSharpx.Collections

type Result =
| Failure of List<string>
| Success
type Report =
| Report of List<string>

type Result<'a> =
| Failure
| Discard
| Success of 'a

type Property<'a> =
| Property of Gen<Report * Result<'a>>

module Tuple =
let first (f : 'a -> 'c) (x : 'a, y : 'b) : 'c * 'b =
f x, y

type Property =
| Property of Gen<Result>
let second (f : 'b -> 'c) (x : 'a, y : 'b) : 'a * 'c =
x, f y

[<CompilationRepresentation(CompilationRepresentationFlags.ModuleSuffix)>]
module Result =
let isFailure (x : Result) : bool =
let map (f : 'a -> 'b) (r : Result<'a>) : Result<'b> =
match r with
| Failure ->
Failure
| Discard ->
Discard
| Success x ->
Success (f x)

let filter (f : 'a -> bool) (r : Result<'a>) : Result<'a> =
match r with
| Failure ->
Failure
| Discard ->
Discard
| Success x ->
if f x then
Success x
else
Discard

let isFailure (x : Result<'a>) : bool =
match x with
| Failure _ ->
| Failure ->
true
| Success ->
false
| Discard ->
false
| Success _ ->
false

let mapFailure (f : List<string> -> List<string>) (x : Result) : Result =
match x with
| Failure msgs ->
Failure (f msgs)
| Success ->
Success
| Discard ->
Discard
[<CompilationRepresentation(CompilationRepresentationFlags.ModuleSuffix)>]
module Report =
let ofList (xs : List<string>) : Report =
Report xs

let toList (Report xs : Report) : List<string> =
xs

let empty : Report =
List.empty |> ofList

let map (f : List<string> -> List<string>) (xs : Report) : Report =
toList xs |> f |> ofList

let addFailure (msg : string) (x : Report) : Report =
map (List.cons msg) x

let append (xs : Report) (ys : Report) : Report =
toList xs @ toList ys |> ofList

[<CompilationRepresentation(CompilationRepresentationFlags.ModuleSuffix)>]
module Property =
open Tuple

let ofGen (x : Gen<Result>) : Property =
let ofGen (x : Gen<Report * Result<'a>>) : Property<'a> =
Property x

let toGen (Property x : Property) : Gen<Result> =
let toGen (Property x : Property<'a>) : Gen<Report * Result<'a>> =
x

let ofResult (x : Result) : Property =
x |> Gen.constant |> ofGen
let ofResult (x : Result<'a>) : Property<'a> =
(Report.empty, x) |> Gen.constant |> ofGen

let ofBool (x : bool) : Property =
if x then
Success |> ofResult
else
Failure [] |> ofResult
let failure : Property<unit> =
Failure |> ofResult

let discard : Property =
let discard : Property<unit> =
Discard |> ofResult

let mapGen (f : Gen<Result> -> Gen<Result>) (Property x : Property) : Property =
Property <| f x
let success (x : 'a) : Property<'a> =
Success x |> ofResult

let counterexample (msg : string) (x : Property) : Property =
(mapGen << Gen.map << Result.mapFailure) (List.cons msg) x

let forAll (gen : Gen<'a>) (f : 'a -> Property) : Property =
let ofBool (x : bool) : Property<unit> =
if x then
success ()
else
failure

let private mapGen
(f : Gen<Report * Result<'a>> -> Gen<Report * Result<'b>>)
(x : Property<'a>) : Property<'b> =
toGen x |> f |> ofGen

let map (f : 'a -> 'b) (x : Property<'a>) : Property<'b> =
(mapGen << Gen.map << second << Result.map) f x

let counterexample (msg : string) (x : Property<'a>) : Property<'a> =
(mapGen << Gen.map << first << Report.addFailure) msg x

let private bindGen
(m : Gen<Report * Result<'a>>)
(k : 'a -> Gen<Report * Result<'b>>) : Gen<Report * Result<'b>> =
Gen.bind m <| fun (report, result) ->
match result with
| Failure ->
Gen.constant (report, Failure)
| Discard ->
Gen.constant (report, Discard)
| Success x ->
Gen.map (first (Report.append report)) (k x)

let bind (m : Property<'a>) (k : 'a -> Property<'b>) : Property<'b> =
bindGen (toGen m) (toGen << k) |> ofGen

let forAll (gen : Gen<'a>) (k : 'a -> Property<'b>) : Property<'b> =
let prepend (x : 'a) =
counterexample (sprintf "%A" x) (f x) |> toGen
counterexample (sprintf "%A" x) (k x) |> toGen
Gen.bind gen prepend |> ofGen


//
// Runner
//

let rec private takeSmallest (Node (x, xs) : Tree<Result>) (nshrinks : int) : Option<int * List<string>> =
let rec private takeSmallest
(Node ((report, x), xs) : Tree<Report * Result<'a>>)
(nshrinks : int) : Option<Report * int> =
match x with
| Success ->
None
| Discard ->
None
| Failure msgs ->
match LazyList.tryFind (Result.isFailure << Tree.outcome) xs with
| Failure ->
match LazyList.tryFind (Result.isFailure << snd << Tree.outcome) xs with
| None ->
Some (nshrinks, msgs)
Some (report, nshrinks)
| Some tree ->
takeSmallest tree (nshrinks + 1)
| Discard ->
None
| Success _ ->
None

let private renderTests : int -> string = function
| 1 ->
Expand All @@ -102,7 +172,7 @@ module Property =
| n ->
sprintf " and %d discards" n

let check' (n : int) (p : Property) : bool =
let check' (n : int) (p : Property<unit>) : bool =
let random = toGen p |> Gen.toRandom

let nextSize size =
Expand All @@ -113,15 +183,15 @@ module Property =

let rec loop seed size tests discards =
if tests = n then
tests, discards, Tree.singleton Success
tests, discards, Tree.singleton (Report.empty, Success ())
else
let seed1, seed2 = Seed.split seed
let result = Random.run seed1 size random

match Tree.outcome result with
| Failure _ ->
match snd (Tree.outcome result) with
| Failure ->
tests + 1, discards, result
| Success ->
| Success () ->
loop seed2 (nextSize size) (tests + 1) discards
| Discard ->
loop seed2 size tests (discards + 1)
Expand All @@ -133,33 +203,47 @@ module Property =
| None ->
printfn "+++ OK, passed %s." (renderTests tests)
true
| Some (nshrinks, msgs) ->
| Some (report, nshrinks) ->
printfn "*** Failed! Falsifiable (after %s%s%s):"
(renderTests tests)
(renderShrinks nshrinks)
(renderDiscards discards)
List.map (printfn "%s") msgs |> ignore
List.map (printfn "%s") (Report.toList report) |> ignore
false

let check (p : Property) : bool =
let check (p : Property<unit>) : bool =
check' 100 p

[<AutoOpen>]
module ForAllBuilder =
module PropertyBuilder =
open Tuple

type Builder internal () =
member __.Return(b : bool) : Property =
Property.ofBool b
member __.For(m : Property<'a>, k : 'a -> Property<'b>) : Property<'b> =
Property.bind m k

member __.ReturnFrom(p : Property) : Property =
p
member __.Yield(x : 'a) : Property<'a> =
Property.success x

member __.Bind(m : Gen<'a>, k : 'a -> Property) : Property =
member __.Bind(m : Gen<'a>, k : 'a -> Property<'b>) : Property<'b> =
Property.forAll m k

member __.Delay(f : unit -> Property) : Property=
member __.Return(b : bool) : Property<unit> =
Property.ofBool b

member __.Delay(f : unit -> Property<'a>) : Property<'a> =
Gen.delay (Property.toGen << f) |> Property.ofGen

member __.Zero() : Property =
member __.Zero() : Property<unit> =
Property.discard

let forAll = Builder ()
[<CustomOperation("counterexample", MaintainsVariableSpace = true)>]
member __.Counterexample(g : Property<'a>, [<ProjectionParameter>] f : 'a -> string) : Property<'a> =
Property.bind g <| fun x ->
Property.counterexample (f x) (Property.success x)

[<CustomOperation("where", MaintainsVariableSpace = true)>]
member __.Where(g : Property<'a>, [<ProjectionParameter>] p : 'a -> bool) : Property<'a> =
Gen.map (second <| Result.filter p) (Property.toGen g) |> Property.ofGen

let property = Builder ()
26 changes: 14 additions & 12 deletions Jack/Script.fsx
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,13 +16,14 @@ open System
// Combinators
//

Property.check <| forAll {
Property.check <| property {
let! x = Gen.range 1 100
let! ys = Gen.item ["a"; "b"; "c"; "d"] |> Gen.seq1
return x < 50 || Seq.length ys <= 3 || Seq.contains "a" ys
let! ys = Gen.item ["a"; "b"; "c"; "d"] |> Gen.seq
counterexample (sprintf "tryHead ys = %A" <| Seq.tryHead ys)
return x < 25 || Seq.length ys <= 3 || Seq.contains "a" ys
}

Property.check <| forAll {
Property.check <| property {
let! xs = Gen.string
return String.length xs <= 5
}
Expand Down Expand Up @@ -57,7 +58,7 @@ let rec genExp =
Add <!> Gen.zip genExp genExp
]

Property.check <| forAll {
Property.check <| property {
let! x = genExp
match x with
| Add (Add _, Add _) when evalExp x > 100 ->
Expand All @@ -70,7 +71,7 @@ Property.check <| forAll {
// reverse (reverse xs) = xs, ∀xs :: [α] ― The standard "hello-world" property.
//

Property.check <| forAll {
Property.check <| property {
let! xs = Gen.list Gen.int
return xs
|> List.rev
Expand All @@ -92,21 +93,22 @@ Gen.printSample genLeapYear
//

// Fails due to integer overflow
Property.check <| forAll {
Property.check <| property {
let! x = Gen.int
let! y = Gen.int
if x > 0 && y > 0 then
return x * y > 0
where (x > 0 && y > 0)
counterexample (sprintf "x * y = %d" <| x * y)
return x * y > 0
}

//
// Lazy Properties
//

Property.check <| forAll {
Property.check <| property {
let! n = Gen.int
if n <> 0 then
return 1 / n = 1 / n
where (n <> 0)
return 1 / n = 1 / n
}

//
Expand Down

0 comments on commit da6fd28

Please sign in to comment.