(*******************************************************************************)
(* 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 [blist]s defined in [blist.v], with
 the bounded exhaustive generator [it_blist] defined in [sc_blist.v].

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

Require Import Arith List NPeano String Nat.

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

(* begin hide *)
Set Warnings "-extraction-opaque-accessed,-extraction".
(* end hide *)

Require Import prelude cut listnat blist Sc sc_blist.

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 bounded lists with the right length and bound.

 Here for length $n=5$ and bound $b=7$. *)

(** *** [SmallCheckWhy3 "../../OCaml/enum/generator/barray" (it_blist 5 7) (is_blistb 7).] *)

SmallCheckWhy3 "../../OCaml/enum/generator/barray" (it_blist 5 7) (is_blistb 7).

(** Expected output: Success *)

(** * Example in [GDL19]: *)

Eval compute in "Lemma rev_blist (example in [GDL19]):".

SmallCheckWhy3 "../../OCaml/enum/generator/barray" (it_blist 7 4) (fun l => is_blistb 4 (rev l)).

(** Expected output: Success *)