(*******************************************************************************)
(* Coq Unit Testing project                                                    *)
(* Copyright 2015-2020 Catherine Dubois, Richard Genestier and Alain Giorgetti *)
(* Samovar - FEMTO-ST institute                                                *)
(*******************************************************************************)

(*******************************************************************************)
(*      This file is distributed under the terms of the                        *)
(*       GNU Lesser General Public License Version 2.1                         *)
(*******************************************************************************)

(** General-purpose handwritten and derived random generators with QuickChick.
  See the other files [qc*.v] for custom generators. See the files 
  [val_qc_*.v] for samples and tests with these generators. *)

(* begin hide *)
From QuickChick Require Import QuickChick.
Import QcDefaultNotation. Open Scope qc_scope.
Import GenLow GenHigh.
Set Warnings "-extraction-opaque-accessed,-extraction".


Require Import List ZArith Program.
Import ListNotations.

Require Import mathcomp.ssreflect.ssreflect.

Require Import Coq.Strings.String.
Local Open Scope string.

Require Import cut listnat.
(* end hide *)

(* For QuickChick *)

Notation "'do!' X <- A ; B" :=
  (bindGen A (fun X => B))
    (at level 200, X ident, A at level 100, B at level 200).

Notation "'do2!' X , H <- A ; B" :=
  (bindGen' A (fun X H => B))
    (at level 200, X ident, H at level 50, A at level 100, B at level 200).

(* Added for compatibility with QC for Coq 8.7 (was defined in 
   QuickChick/src/Arbitrary.v for Coq 8.5): *)
Definition arbitraryNat := sized (fun x => choose (0, x)).

(** * Two simple generators

 Never used, just for syntax illustration. *)

(* Random generator of even natural numbers *)
Definition gen_even := 
 do! m <- arbitraryNat;
 returnGen (2 * m).

(* Random generator of odd natural numbers *)
Definition gen_odd := 
 do! m <- arbitraryNat;
 returnGen ((2 * m) + 1).
