(*******************************************************************************)
(* Coq Unit Testing project                                                    *)
(* Copyright 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 with the generators of reversed excedant lists defined in
 [qc_revsubex.v]. *)

(* 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 seq ssreflect ssrbool ssrnat eqtype.

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

Require Import prelude bFinFun endofun permut cut revsubex qc qc_revsubex.
(* end hide *)

(** * Sampling *)

(** ** With [genRslAsListnat] *)

(** *** Reversed excendant lists with 6 elements: *)

Sample (genRslAsListnat 6).

(** 

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

(** ** With [genRsl] *)

(** *** Field [rsl_val] of some [rsl] terms with 6 elements: *)

Sample (genRsl 6).

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

(** ** With [genRslType] *)

(** *** Some [rslType] terms with 6 elements, displayed with [showRslType]: *)

Sample (genRslType 6).

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

(** ** Samples of sums *)

Extract Constant Test.defNumTests => "10".

QuickCheck (sized (fun n1 =>
 forAll (genRslType n1) (fun l1 =>
   collect (show l1)
 (sized (fun n2 =>
 forAll (genRslType n2) (fun l2 => 
   collect (show l2)
   (collect (show (sum_rslType l1 l2)) (true)))))))).

(** Output:

 2 : "[ ]" , "[ ]" , "[ ]"

2 : "[0]" , "[0]" , "[1, 0]"

1 : "[4, 0, 2, 1, 0]" , "[2, 1, 2, 0, 0]" , "[7, 6, 7, 5, 5, 4, 0, 2, 1, 0]"

1 : "[3, 0, 3, 0, 1, 0]" , "[5, 0, 2, 2, 1, 0]" , "[11, 6, 8, 8, 7, 6, 3, 0, 3, 0, 1, 0]"

1 : "[1, 2, 0, 0]" , "[3, 2, 0, 0]" , "[7, 6, 4, 4, 1, 2, 0, 0]"

1 : "[1, 1, 0]" , "[2, 1, 0]" , "[5, 4, 3, 1, 1, 0]"

1 : "[1, 0]" , "[1, 0]" , "[3, 2, 1, 0]"

1 : "[0, 0]" , "[0, 0]" , "[2, 2, 0, 0]"

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

(** ** Permutations in one-line notation from RSL with [lift]: *)

Sample (genPermlineFromRslAsListnat 5).

(** Samples:

 - $[4, 0, 1, 2, 3], [2, 4, 1, 0, 3], [2, 4, 1, 0, 3], [3, 1, 4, 0, 2], [3, 4, 1, 0, 2], [0, 1, 3, 2, 4], [1, 2, 3, 0, 4]$,

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

(** * Random testing *)

Extract Constant Test.defNumTests => "10000".

(** ** Soundness of the random generator [genRslAsListnat]

 Tested with [is_rslb]. *)

QuickCheck (sized (fun n => forAll (genRslAsListnat n) is_rslb)).

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

(** ** Soundness of the interpretation [rslType2listnat] of RSL terms as reversed
 subexcedant lists *)

QuickCheck (sized (fun n => 
 forAll (genRslType n) (fun r => is_rslb (rslType2listnat r)))).

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

(** ** The permutation code [rslType2permut] indeed generates permutations

 Tested with [is_permutb]. *)

(* begin hide *)
Eval compute in "rslType2permut is sound".
(* end hide *)

QuickCheck (sized (fun n => 
 forAll (genRslType n) (fun p => 
   is_permutb n (fct (rslType2permut p))))).

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

(** ** Random testing cancellation lemma [rslType2permutK] *)
 
(* begin hide *)
Eval compute in "Testing Lemma rslType2permutK".
(* end hide *)

QuickCheck (sized (fun n => 
  forAll (genRslType n) (fun t =>
   eq_rslTypeb n (permut2rslType (rslType2permut t)) t))).

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