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

(** Samples and tests for [permline]s (permutations in one-line notation) defined
 in [permline.v]. The random generators are defined in [qc_permline.v]. *)

Require Import Arith List NPeano String Nat.

Require Import mathcomp.ssreflect.ssreflect.
From QuickChick Require Import QuickChick.

Require Import prelude cut listnat permline qc qc_endoline qc_permline.

Open Scope string_scope.

(* Uncomment the next line for ?? tests instead of 10000: *)
(* Extract Constant Test.defNumTests => "??". *)

(** * Samples *)

(** ** With [(genPermlineAsListnat 7)] *)

Sample (genPermlineAsListnat 7).

(**
 $[3, 2, 4, 6, 0, 1, 5], [0, 5, 3, 4, 6, 1, 2], [6, 2, 0, 3, 1, 4, 5],
 [0, 6, 1, 2, 4, 3, 5], [4, 3, 2, 1, 5, 0, 6]$,

 $[1, 5, 0, 2, 3, 4, 6], [3, 2, 6, 1, 4, 0, 5], [1, 5, 0, 3, 2, 4, 6], [1, 0, 2, 3, 4, 6, 5], [2, 1, 6, 3, 5, 0, 4]$, 

 $[4, 0, 5, 1, 2, 6, 3]$
*)

(** * Random testing *)

(* begin hide *)
Eval compute in "Random testing".
(* end hide *)

Eval compute in "List permutations generated by genPermlineAsListnat are permutations:".

QuickCheck (sized (fun n => forAll (genPermlineAsListnat n) is_permlineb)).

(** +++ Passed 10000 tests (0 discards) *)
