(*******************************************************************************)
(* 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 endofunctions defined in [endofun.v], with
 the bounded exhaustive generator [it_endofun] defined in [sc_endofun.v]. *)

Require Import Arith List NPeano String Nat.

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

Require Import prelude cut listnat blist endoline endofun.
Require Import cut sc_interval sc_endoline sc_endofun.

Open Scope string_scope.

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

(* begin hide *)
Eval compute in "SmallCheck".

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

(** *** Endofunctions enumerated by Why3 are endofunctions in one-line notation. *)

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

(** Expected output: Success *)
