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

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

(* begin hide *)
Require Import List Arith Program.
Require Import mathcomp.ssreflect.ssreflect.
From QuickChick Require Import QuickChick.
Import QcDefaultNotation. Open Scope qc_scope.
Import GenLow GenHigh.
Set Warnings "-extraction-opaque-accessed,-extraction".

Require Import List ZArith.
Import ListNotations.

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import seq ssreflect ssrbool ssrnat eqtype.

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

Require Import prelude bFinFun endofun permut cut revsubex qc.
(* end hide *)

(** * Random generator of RSL as lists of natural numbers *)

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

(** * For the refinement type [rsl] *)

(** ** Display function *)

Definition show_Rsl (n : nat) (r : rsl n) := show (rsl_val r).

Instance showRsl (n : nat) : Show (rsl n) := { show := show_Rsl n }.

(** ** Random generator of RSL (refinement type) *)

Program Fixpoint genRsl (n : nat) {measure n} : G (rsl n) :=
 match n with
   O    => returnGen rsl0
 | S n' => do2! i, H <- choose (0, n');
           liftGen (@rslS i n' _) (genRsl n')
 end.
Next Obligation.
apply semChoose in H; auto.
simpl in H.
apply /leP.
apply H.
Qed.

(** * For the structure type [rslType] *)

(** ** Display function *)

Definition show_RslType (n : nat) (r : rslType n) := show (rslType2listnat r).

Instance showRslType (n : nat) : Show (rslType n) := { show := show_RslType n }.

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

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

Program Fixpoint genRslType (n : nat) {measure n} : G (rslType n) :=
 match n with
   O    => returnGen R0
 | S n' => do2! i, H <- choose (0, n');
           liftGen (@RS n' i _) (genRslType n')
 end.
Next Obligation.
apply semChoose in H; auto.
simpl in H.
apply /leP.
apply H.
Defined.

(** *** Some functions for testing *)
Definition rslTypehd  n (p : rslType (S n)) : nat :=
  match p with
  | @RS _ h _ _ => h
  end.

Definition rslTypetail  n (p : rslType (S n)) : rslType n :=
  match p with
  | @RS _ _ _ t => t
  end.

Fixpoint eq_rslTypeb (n : nat) (p1 : rslType n) : rslType n -> bool :=
  match p1 in (rslType n) return rslType n -> bool with
    R0 => fun _ => true
  | @RS n0 i _ q1   => fun p => andb (i =? (@rslTypehd n0 p))%nat
     (@eq_rslTypeb n0 q1 (@rslTypetail n0 p))
  end.

(** * Random generator of permutations in one-line notation from RSLs

 With the permutation code [transpoCode]. *)

Definition genPermlineFromRslAsListnat (n : nat) : G (list nat) := 
 liftGen (@transpoCode n) (genRslType n).
 
(* TODO: CLEAN FROM HERE

(* for [rslType] *)


(** * Derived generator for reversed subexcedant lists *)

Derive ArbitrarySizedSuchThat for (fun l => is_rsl b l).
(*
input0_0 : nat
aux_arb : nat -> nat -> G (option (seq nat))
size0, input0_, size', n : nat
______________________________________(1/1)
GenSuchThat nat (fun i : nat => (i <= n)%coq_nat)
*)

(* GenSizedSuchThatis_rsl is defined *)
Check GenSuchThatis_rsl.

Definition gsubexb : nat -> G (option (list nat)) := fun b =>
 @arbitrarySizeST _ (is_subex b) (GenSizedSuchThatis_subex b) b.

Sample (gsubexb 5).

(** Samples:

- $Some [4, 2, 1, 1, 0], Some [4, 3, 0, 1, 0], Some [4, 3, 0, 1, 0],
    Some [0, 2, 2, 0, 0], Some [4, 3, 2, 0, 0], Some [4, 0, 2, 0, 0],
    Some [4, 3, 0, 0, 0], Some [4, 1, 2, 1, 0], Some [3, 3, 0, 0, 0],
    Some [4, 3, 2, 1, 0], Some [4, 3, 2, 1, 0]$
*)


(** * Random generator for blistType *)

Program Fixpoint gen_blistTypele_nb (n : nat)(b : nat) : 
G (blistType_le (S b) n) :=
 match n with
   0 => returnGen (tle0 (S b))
 | S m => (*do! b <- arbitraryNat;*)
          bindGen' (choose (0, b)) (fun i H => 
          liftGen (@tleS b i m _) (gen_blistTypele_nb m b))
 end.
Next Obligation.
  apply semChoose in H;auto.
  apply/leP;auto.
Defined.

Open Scope string.

Fixpoint show_blistType_le (n : nat) (b : nat) 
(t : blistType_le b n) :=
 match t in (blistType_le b n) with 
 | @tle0 b0 => "(t0 "  ++ show b0 ++ " )"
 | @tleS b0 i n0 _ q => "(tS " ++ show i ++ " " ++ "b=" ++ show b ++ " " ++ 
                        show_blistType_le n0 (S b0) q ++ ")"
 end.

Instance showblistType_le (n : nat) (b :nat) : 
 Show (blistType_le b n) := 
{ show := show_blistType_le n b }.

Sample (gen_blistTypele_nb 4 5).
(*
[(tS 3 b=6 (tS 0 b=6 (tS 2 b=6 (tS 2 b=6 (t0 6 ))))), 
(tS 5 b=6 (tS 3 b=6 (tS 4 b=6 (tS 5 b=6 (t0 6 ))))), 
(tS 5 b=6 (tS 4 b=6 (tS 4 b=6 (tS 5 b=6 (t0 6 ))))), 
(tS 5 b=6 (tS 1 b=6 (tS 4 b=6 (tS 5 b=6 (t0 6 ))))), 
(tS 1 b=6 (tS 4 b=6 (tS 0 b=6 (tS 3 b=6 (t0 6 ))))), 
(tS 5 b=6 (tS 5 b=6 (tS 1 b=6 (tS 5 b=6 (t0 6 ))))), 
(tS 3 b=6 (tS 2 b=6 (tS 2 b=6 (tS 4 b=6 (t0 6 ))))), 
(tS 0 b=6 (tS 1 b=6 (tS 1 b=6 (tS 5 b=6 (t0 6 ))))), 
(tS 5 b=6 (tS 5 b=6 (tS 1 b=6 (tS 1 b=6 (t0 6 ))))), 
(tS 5 b=6 (tS 0 b=6 (tS 0 b=6 (tS 2 b=6 (t0 6 ))))), 
(tS 0 b=6 (tS 5 b=6 (tS 2 b=6 (tS 5 b=6 (t0 6 )))))]
*)

Definition gsubexb : nat -> G (option (list nat)) := fun b =>
 @arbitrarySizeST _ (is_subex_le b) (GenSizedSuchThatis_subex_le b) b.

Sample (gsubexb 5).


(*
File "./qc.v", line 227, characters 0-61:
Error:
Anomaly "Uncaught exception Failure("Unsupported range: (leq $  i b)")." 
Please report at http://coq.inria.fr/bugs/.

File "./qc.v", line 227, characters 0-61:
Error:
Anomaly
"Uncaught exception Failure("Unsupported range: (leq $  i Coq.Init.Datatypes.S  b)")."
Please report at http://coq.inria.fr/bugs/.
*)

(* Model: goodFoo' in exemples_leo *)

Derive ArbitrarySizedSuchThat for (fun l => subex_spec l).

(* GenSizedSuchThatsubex_spec is defined *)

Definition gsubex : G (option (list nat)) := 
 @arbitrarySizeST _ (subex_spec) (GenSizedSuchThatsubex_spec).

Sample (gsubex 5).
(*
File "./qc.v", line 220, characters 0-58:
Error:
Anomaly
"Uncaught exception Failure("Unsupported range: (length $  nat  l)")." 
Please report at http://coq.inria.fr/bugs/.
*)

*)