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

(** [it_endo n] is a bounded exhaustive generator for [endoline]s, i.e. lists of
  [n] natural numbers in [[0..n-1]]. [endoline]s are defined in [endoline.v]. *)

Require Import Arith List NPeano String Nat.

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

Require Import Sc.

Open Scope string_scope.

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

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

(** The generator comes from OCaml code generated by extraction with Why3 of 
  a generator written in WhyML: *)

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