(*******************************************************************************)
(* Coq Unit Testing project                                                    *)
(* Copyright 2019-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_fact n] is an exhaustive generator of factorials of length [n].
    Factorials are defined in [fact.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_fact (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 in the folder [why3/enum/generator/fact]: *)

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