(*******************************************************************************)
(* Coq Unit Testing project                                                    *)
(* Copyright 2018-2020 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                         *)
(*******************************************************************************)

(** [it_blist n b] is a bounded exhaustive generator of [blist]s with bound [b]
  and size [n], i.e., lists of [n] natural numbers in [[0..b-1]]. [blist]s are
  defined in [blist.v]. *)

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 Sc.

Open Scope string_scope.

Parameter cursor : Type.
Parameter create : nat -> nat -> cursor.
Parameter next_list : cursor -> (option (list nat)) * cursor.
Parameter hasnext_list : cursor -> bool.

Definition it_blist (n b : nat) := {|
 st_t := cursor;
 start := create n b;
 next := next_list;
 hasnext := hasnext_list
|}.

(** The generator comes from OCaml code generated by extraction with Why3 of 
  a generator written in WhyML in the folder [why3/enum/generator/barray]: *)

Extract Constant cursor => "Barray__Enum.cursor".
Extract Constant create => "fun n -> fun b -> 
 Barray__Enum.create_cursor (Z.of_int n) (Z.of_int b)".
Extract Constant next_list => "(fun c -> 
 Barray__Enum.next c;
 let a = c.current in
 (Some (List.map Z.to_int (Array.to_list a)), c))".
Extract Constant hasnext_list => "Barray__Enum.has_next".
