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

(** Bounded exhaustive generators for permutations defined in [permline.v]. *)

Require Import Arith List NPeano String Nat.

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

Require Import Sc.

(** * First generator [it_permline n] *)

(** This iterator is based on an OCaml generator with a non-trivial function has_next 
  and a function next returning an array. *)

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

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

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

(** * Second generator [it_permline2 n] *)

(** This iterator is based on an OCaml generator with a trivial function has_next 
  and a function next modifying an array by side-effect. *)

Parameter cursor2 : Type.
Parameter create2 : nat -> cursor2.
Parameter next_list2 : cursor2 -> (option (list nat)) * cursor2.
Parameter hasnext_list2 : cursor2 -> bool.

Definition it_permline2 (n : nat) := {|
 st_t := cursor2;
 start := create2 n;
 next := next_list2;
 hasnext := hasnext_list2
|}.

Extract Constant cursor2 => "Permutation__Enum.cursor".
Extract Constant create2 => "fun n -> 
 Permutation__Enum.create_cursor (Z.of_int n)".
Extract Constant next_list2 => "(fun c ->
 Permutation__Enum.next c;
 let a = c.current in
 (Some (List.map Z.to_int (Array.to_list a)), c))".
Extract Constant hasnext_list2 => "Permutation__Enum.has_next".
