(*
copyright (c) 2013, simon cruanes
all rights reserved.

redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:

redistributions of source code must retain the above copyright notice, this
list of conditions and the following disclaimer.  redistributions in binary
form must reproduce the above copyright notice, this list of conditions and the
following disclaimer in the documentation and/or other materials provided with
the distribution.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

(** {1 Quickcheck inspired property-based testing} *)

(** The library takes inspiration from Haskell's QuickCheck library. The
rough idea is that the programer describes invariants that values of
a certain type need to satisfy ("properties"), as functions from this type
to bool. She also needs to desribe how to generate random values of the type,
so that the property is tried and checked on a number of random instances.

This explains the organization of this module:

- {! Arbitrary} is used to describe how to generate random values. An
  ['a Arbitrary.t] is a random generator of values of type 'a.
- {! Prop} is used to describe and combine properties. Especially interesting
  is [Prop.(==>)], that is such that [a ==> b] only checks the property [b]
  on a value [x] if [a x] holds (precondition).
- {! PP} describes a few combinators to print values. This is used when a
  property fails on some instances, to print the failing instances.

Then, a few functions are provided to test properties. Optional parameters
allow to specify the random generator, the printer for failing cases, the
number of instances to generate and test...


Examples:

    - Not all lists are sorted:

{[QCheck.run ~n:10 ~pp:QCheck.PP.(list int)
  QCheck.Arbitrary.(list small_int) (fun l -> l = List.sort compare l);;
]}

    - List.rev is involutive:

{[QCheck.run ~n:1000 QCheck.Arbitrary.(list alpha)
  (fun l -> List.rev (List.rev l) = l)
]}

    - generate a tree using {! Arbitrary.fix} :

{[type tree = Int of int | Node of tree list;;
 
 let ar = QCheck.Arbitrary.(fix ~max:10
  ~base:(map small_int (fun i -> Int i))
  (fun t st -> Node (list t st)));;

 ar (Random.State.make_self_init ());;
 ]}
*)

(** {2 Description of how to generate arbitrary values for some type} *)
 
module Arbitrary : sig
  type 'a t = Random.State.t -> 'a
    (** A generator of arbitrary values of type 'a *)

  val int : int -> int t
    (** Any integer between 0 (inclusive) and the given higher bound (exclusive) *)

  val int_range : start:int -> stop:int -> int t
    (* Integer range start .. stop-1 *)

  val small_int : int t
    (** Ints lower than 100 *)

  val bool : bool t
    (** Arbitrary boolean *)

  val char : char t
    (** A (printable) char *)

  val alpha : char t
    (** Alphabetic char *)

  val float : float -> float t
    (** Random float *)

  val string : string t
    (** Random strings of small length *)

  val string_len : int t -> string t
    (** String of random length *)

  val map : 'a t -> ('a -> 'b) -> 'b t
    (** Transform an arbitrary into another *)

  val list : ?len:int t -> 'a t -> 'a list t
    (** List of arbitrary length *)

  val opt : 'a t -> 'a option t
    (** May return a value, or None *)

  val list_repeat : int -> 'a t -> 'a list t
    (** Lists of given length exactly *)

  val array : ?len:int t -> 'a t -> 'a array t
    (** Random array of random length *)

  val array_repeat : int -> 'a t -> 'a array t
    (** Random array of given length *)

  val among : 'a list -> 'a t
    (** Choose an element among those of the list *)

  val among_array : 'a array -> 'a t
    (** Choose in the array *)

  val choose : 'a t list -> 'a t
    (** Choice among combinations *)

  val fix : ?max:int -> base:'a t -> ('a t -> 'a t) -> 'a t
    (** Recursive arbitrary values. The optional value [max] defines
        the maximal depth, if needed. [base] is the base case. *)

  val fix_depth : depth:int t -> base:'a t -> ('a t -> 'a t) -> 'a t
    (** Recursive values of at most given random depth *)
end

(** {2 Pretty printing} *)

module PP : sig
  type 'a t = 'a -> string

  val int : int t
  val bool : bool t
  val float : float t
  val char : char t
  val string : string t

  val list : 'a t -> 'a list t
  val array : 'a t -> 'a array t
end

(** {2 Testing} *)

module Prop : sig
  type 'a t = 'a -> bool

  val (==>) : ('a -> bool) -> 'a t -> 'a t
    (** Precondition for a test *)

  val (&&&) : 'a t -> 'a t -> 'a t
    (** Logical 'and' on tests *)

  val (|||) : 'a t -> 'a t -> 'a t
    (** Logical 'or' on tests *)

  val (!!!) : 'a t -> 'a t
    (** Logical 'not' on tests *)
end

type 'a result =
  | Ok of int * int  (** total number of tests / number of failed preconditions *)
  | Failed of 'a list
  | Error of exn

val check : ?rand:Random.State.t -> ?n:int -> 
            'a Arbitrary.t -> 'a Prop.t -> 'a result
  (** Check that the property [prop] holds on [n] random instances of the type
      'a, as generated by the arbitrary instance [gen] *)

(** {2 Main} *)

val run : ?pp:('a -> string) -> ?n:int ->
          ?rand:Random.State.t -> ?name:string ->
          'a Arbitrary.t -> 'a Prop.t -> bool
  (** Run and print result *)

val run_tests : (rand:Random.State.t -> bool) list -> bool
  (** Run a list of tests, and print their results *)