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

(** Handwritten and derived random generators for blists, with QuickChick.
 See the file [val_qc_blist.v] for samples and tests with these generators. *)

(* begin hide *)
Require Import List Arith Program.

From QuickChick Require Import QuickChick Tactics Instances Classes DependentClasses.
Import QcDefaultNotation. Open Scope qc_scope.
Import GenLow GenHigh.

Require Import ZArith.
Import ListNotations.

From mathcomp Require Import seq ssreflect ssrbool ssrnat eqtype.

Require Import Coq.Strings.String.
Local Open Scope string.

Require Import cut listnat blist qc.
(* end hide *)

(** * Handwritten generators related to [blist]s

 The first two generators randomly generate lists of natural numbers
 expected to be [blist]s. *)

(** ** The output is a list of natural numbers *)

Fixpoint genBlistAsListnat (n : nat) (b : nat) : G (list nat) :=
 match n with
   0     => returnGen nil
 | S n'  => match b with 
              0    => returnGen nil
            | S b' => do! m <- choose (0, b');
                      liftGen (cons m) (genBlistAsListnat n' b)
            end
 end.

(** ** Random generator of [blist]s (refinement type) *)

Program Fixpoint genBlist (size : nat) (b : nat) {measure size} : G (blist b) :=
 match size with
   O       => returnGen (blist0 b)
 | S size' => match b with
                   O => returnGen (blist0 0)
              | S b' => do2! v, H <- choose (0, b');
                        liftGen (@blistS (S b') v _) (genBlist size' (S b'))
              end
 end.
Next Obligation.
apply semChoose in H; auto.
simpl in H.
apply /leP.
rewrite ltnS. auto.
Defined.

(** ** Random generator of [blistType] terms

 The following function generates terms of type [blistType] of size [n] or 
 less, with values [b] or less. *)

Program Fixpoint genBlistType (n : nat) (b : nat) {measure n} : G (blistType b) :=
 match n with
   O    => returnGen (B0 b)
 | S n' => match b with
             O    => returnGen (B0 0)
           | S b' => bindGen' (choose (0, b'))
                      (fun v H => liftGen (@BS b'.+1 v _) (genBlistType n' b'.+1))
           end
 end.
Next Obligation.
apply semChoose in H; auto.
simpl in H.
apply /leP.
rewrite ltnS. auto.
Defined.

(** ** Derived generator for [blist]s *)

(** [Derive ArbitrarySizedSuchThat for (fun n => le n m).] 

 generates the class instance [GenSizedSuchThatle]. The free variable [m] will
 be an input of the generator while the bound variable [n] will be the output
 of the generator. *)

Derive ArbitrarySizedSuchThat for (fun n => le n m).

(** [Derive ArbitrarySizedSuchThat for (fun l => is_blist_le b l).]

 generates the class instance [GenSizedSuchThatis_blist_le]. The free variable
 [b] will be an input of the generator while the bound variable [l] will be 
 the output of the generator. *)

Derive ArbitrarySizedSuchThat for (fun l => is_blist_le b l).

(*
GenSizedSuchThatis_blist_le
     : forall input0_ : nat,
       GenSizedSuchThat (seq nat)
         (fun _forGen : seq nat => is_blist_le input0_ _forGen)
*)

(** *** Derived random generator: *)

Definition genSTblist : nat -> G (option (list nat)) := fun b =>
 @arbitrarySizeST _ (is_blist_le b) (GenSizedSuchThatis_blist_le b) b.