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

(** Bounded exhaustive tests for [endoline]s defined in [endoline.v], with
 the bounded exhaustive generator [it_endo] defined in [sc_endoline.v].

 This OCaml generator in the folder [OCaml/enum/cursor/barray] is derived from 
 a generator in WhyML in the folder [why3/enum/cursor/barray]. *)

Require Import Arith List NPeano String Nat.

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

Require Import prelude cut listnat blist endoline Sc sc_interval sc_endoline.

Open Scope string_scope.

(* begin hide *)
Eval compute in "SmallCheckWhy3".
(* end hide *)

(** * Generator soundness

 Bounded exhaustive check that the structures enumerated by the bounded exhaustive generator really are
 endofunctions in one-line notation. *)

(* begin hide *)
Eval compute in "Endofunctions enumerated by Why3 are endofunctions in one-line notation:".
(* end hide *)

(** *** [SmallCheckWhy3 "../../OCaml/enum/cursor/barray" (it_endo 7) (fun l => is_endolineb l).] *)

SmallCheckWhy3 "../../OCaml/enum/cursor/barray" (it_endo 7) (fun l => is_endolineb l).

(** Expected output: Success *)

(** * Invariance lemmas *)

(** ** Conditional preservation of endofunctions by [cons] *)

(** For all the endofunctions [f] of size [lf] in [0..7] and all numbers [n]
 in [0..lf]. *)

SmallCheckWhy3 "../../OCaml/enum/cursor/barray"
 (it_interval 7) (fun lf : nat =>
 (smallCheckb (it_endo lf) (fun f =>
 (smallCheckb (it_interval lf) (fun n => is_endolineb (n::f)))))).

(** Expected output: Success *)

(** ** Preservation of endofunctions by [lift] *)

(** For all positions in [0..8] and all endofunctions of size 6. *)

SmallCheckWhy3 "../../OCaml/enum/cursor/barray"
 (it_interval 8) (fun p => 
 (smallCheckb (it_endo 6) (fun f : list nat => is_endolineb (lift p f)))).

(** Expected output: Success *)