(*******************************************************************************)
(* 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 for endofunctions in one-line notation defined in [endoline.v]. *)

Require Import Arith List NPeano String Nat.

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

Require Import prelude cut listnat endoline qc qc_blist qc_endoline.

Open Scope string_scope.

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

(** * Sampling *)

(** ** Samples with [genEndolineAsListnat] *)

(** *** [Sample (genEndolineAsListnat 0)]: *)

Sample (genEndolineAsListnat 0).

(** [ [  ], [  ], [  ], [  ], [  ], [  ], [  ], [  ], [  ], [  ], [  ] ] *)

(** *** [Sample (genEndolineAsListnat 1)]: *)

Sample (genEndolineAsListnat 1).

(** [ [ 0 ], [ 0 ], [ 0 ], [ 0 ], [ 0 ], [ 0 ], [ 0 ], [ 0 ], [ 0 ], [ 0 ], [ 0 ] ] *)

(** *** Sample [(genEndolineAsListnat 7)], [endoline]s with (strict) bound 7: *)

Sample (genEndolineAsListnat 7).

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

(** * Random testing *)

Eval compute in "Random testing".

(** *** Lists generated by [genEndolineAsListnat] represent endofunctions, tested with [forallb]: *)

Eval compute in "Lists generated by genEndolineAsListnat represent endofunctions, test with forallb:".

QuickCheck (sized (fun n => 
 forAll (genEndolineAsListnat n) (fun l =>
  andb (beq_nat (List.length l) n) (forallb (fun x : nat => x <? n) l)))).

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

(** *** Lists generated by [genEndolineAsListnat] represent endofunctions, tested with [is_endolineb]: *)

Eval compute in "Lists generated by genEndolineAsListnat represent endofunctions, test with [is_endolineb]:".

QuickCheck (sized (fun n => 
 forAll (genEndolineAsListnat n) (fun l => is_endolineb l))).

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

(** *** The extension of an endofunction with cons is an endofunction under some conditions (Lemma [cons_endo]): *)

Eval compute in "The extension of an endofunction with cons is an endofunction under some conditions (Lemma cons_endo):".

QuickCheck (sized (fun n =>
 forAll (genEndolineAsListnat n) (fun f => 
 forAll (choose(0, List.length f)) (fun m => 
 is_endolineb (m :: f))))).

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

(** *** The lifting of an endofunction is an endofunction (Lemma [lift_endo]): *)

Eval compute in "The lifting of an endofunction is an endofunction (Lemma lift_endo):".

QuickCheck (sized (fun n =>
 forAll (genEndolineAsListnat n) (fun f =>
 forAll arbitraryNat (fun p =>
 is_endolineb (lift p f))))).

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