(*******************************************************************************)
(* Coq Unit Testing project                                                    *)
(* Copyright 2017-2018 Catherine Dubois 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 and derived random generators of permutations in one-line 
 notation, with QuickChick. See the file [val_qc_permline.v] for samples and
 tests with these generators. *)

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

Require Import List ZArith.
Import ListNotations.

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype.

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

Require Import prelude bFinFun listnat qc.
(* end hide *)

(** * Random generator of permutations in one-line notation, as lists *)

Fixpoint genPermlineAsListnat (n : nat) : G (list nat) :=
 match n with
   0     => returnGen nil
 | S n'  => do! p <- choose (0, n');
            liftGen (lift p) (genPermlineAsListnat n')
 end.