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

(** Bounded exhaustive tests with the generators defined in [sc_permline.v]. *)
 
Require Import Arith List NPeano String Nat.

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

Require Import prelude cut permline Sc sc_interval sc_permline.

Open Scope string_scope.

(** * Soundness of the first generator of permutations in one-line notation *)

(* begin hide *)
Eval compute in "Permutations in one-line notation enumerated by [it_permline] are permutations:".
(* end hide *)

(** *** With all permutations of size 7 *)

(* begin hide *)
Eval compute in "Sequential generation of all permutations of size 7:".
(* end hide *)

SmallCheckWhy3 "../../OCaml/enum/cursor/permutation"
 (it_permline 7) (fun l : list nat => is_permlineb l).

(** Expected output: Success *)

(** *** With all permutations of size 8 *)

(* begin hide *)
Eval compute in "Sequential generation of all permutations of size 8:".
(* end hide *)

SmallCheckWhy3 "../../OCaml/enum/cursor/permutation"
 (it_permline 8) (fun l : list nat => is_permlineb l).

(** Expected output: Success *)

(** *** With all permutations of size 9 *)

(* begin hide *)
Eval compute in "Sequential generation of all permutations of size 9:".
(* end hide *)

SmallCheckWhy3 "../../OCaml/enum/cursor/permutation"
 (it_permline 9) (fun l : list nat => is_permlineb l).

(** Expected output: Success *)

(** *** With all the permutations of length up to 8 *)

(* begin hide *)
Eval compute in "Sequential generation of all permutations of size 8 or less with [it_interval):".
(* end hide *)

SmallCheckWhy3 "../../OCaml/enum/cursor/permutation"
 (it_interval 8) (fun n => 
  (smallCheckb (it_permline n) (fun l : list nat => is_permlineb l))).

(** Expected output: Success *)


(** * Soundness of the second generator of permutations in one-line notation *)

(* begin hide *)
Eval compute in "Permutations in one-line notation enumerated by [it_permline2] are permutations:".
(* end hide *)

(** *** With all permutations of size 7 *)

(* begin hide *)
Eval compute in "Sequential generation of all permutations of size 7:".
(* end hide *)

SmallCheckWhy3 "../../OCaml/enum/generator/permutation"
 (it_permline2 7) (fun l : list nat => is_permlineb l).

(** Expected output: Success *)

(** *** With all permutations of size 8 *)

(* begin hide *)
Eval compute in "Sequential generation of all permutations of size 8:".
(* end hide *)

SmallCheckWhy3 "../../OCaml/enum/generator/permutation"
 (it_permline2 8) (fun l : list nat => is_permlineb l).

(** Expected output: Success *)

(** *** With all permutations of size 9 *)

(* begin hide *)
Eval compute in "Sequential generation of all permutations of size 9:".
(* end hide *)

SmallCheckWhy3 "../../OCaml/enum/generator/permutation"
 (it_permline2 9) (fun l : list nat => is_permlineb l).

(** Expected output: Success *)

(** *** With all the permutations of length up to 8 *)

(* begin hide *)
Eval compute in "Sequential generation of all permutations of size 8 or less with [it_interval):".
(* end hide *)

SmallCheckWhy3 "../../OCaml/enum/generator/permutation"
 (it_interval 8) (fun n => 
  (smallCheckb (it_permline2 n) (fun l : list nat => is_permlineb l))).

(** Expected output: Success *)
