(*******************************************************************************)
(* 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                         *)
(*******************************************************************************)

(** Handwritten random generators for lists of natural numbers, with QuickChick.
 See the file [val_qc_listnat.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 qc.
(* end hide *)

(* For QuickChick *)

(* 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)).

(** * Random generator of lists of natural numbers 

 The following generator randomly generates lists of [n] natural numbers. *)

Fixpoint genListnat (n : nat) : G (list nat) :=
 match n with
   0 => returnGen nil
 | S p  => do! m <- arbitraryNat;
          liftGen (cons m) (genListnat p)
 end.

