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

(** Random generator of ROM terms encoding rooted ordinary maps. *)

Require Import Coq.Logic.JMeq Coq.Arith.Arith Coq.Arith.PeanoNat Omega Even List String.
Require Import Eqdep_dec EqdepFacts.
Require Import Coq.Program.Wf.

Import ListNotations.

Require Import prelude bFinFun cut endofun permut operations trans map rom.
Require Import qc revsubex qc_revsubex.

Require Import Program.

(** *** Some trivial lemmas with omega: *)

Lemma plus2 (m : nat) : m+m = 2*m.
Proof. omega. Qed.

Lemma minusle (m e1 : nat) : m - e1 <= m.
Proof. omega. Qed.

Lemma minusplus (m e1 : nat) : e1 <= m -> e1 + (m - e1) = m.
Proof. omega. Qed.

From QuickChick Require Import QuickChick Tactics.

From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.

Open Scope string_scope.

Fixpoint show_ROMterm (n : nat) (t : rom n) :=
 match t with
 | mty => show "V"
 | bin e1 e2 t1 t2 => "B(" ++ show_ROMterm e1 t1 ++ "," ++ 
                           show_ROMterm e2 t2 ++ ")"
 | unl e k _ t => "U" ++  show k ++ "(" ++ show_ROMterm e t ++ ")" 
 end.

Instance showROMterm (n : nat) : Show (rom n) := { show := show_ROMterm n }.

Require Import mathcomp.ssreflect.ssreflect.

Program Definition bin2 (m e1 : nat) (H : semGen (choose (0, m)) e1) : 
rom e1 -> rom (m-e1) -> rom (S m) := @bin e1 (m-e1).
Next Obligation.
apply semChoose in H; auto.
simpl in H.
rewrite minusplus.
rewrite plusE. apply /addn1.
apply /leP. apply H.
Defined.

(** * Random generator of ROM terms *)

(* TODO: see if simpler with Local Obligation Tactic := intros; try omega. *)

Program Fixpoint genRom (e : nat) {measure e} : G (rom e) :=
 match e with
   0    => returnGen mty
 | S e' => oneOf_
           (bindGen' (choose (0, 2*e')) (fun k H =>
            liftGen (@unl e' k _) (genRom e')))
          [
           (bindGen' (choose (0, e')) (fun e1 H =>
            liftGen2 (@bin2 e' e1 H) (genRom e1) (genRom (e' - e1))));
           (bindGen' (choose (0, 2*e')) (fun k H =>
            liftGen (@unl e' k _) (genRom e')))
          ]
end.
Next Obligation.
apply semChoose in H; auto.
simpl in H.
apply /leP.
move/leP: H => H.
rewrite Nat.add_assoc.
rewrite Nat.add_0_r.
apply /leP. rewrite plus2.
apply H.
Defined.
Next Obligation.
apply semChoose in H; auto.
simpl in H.
apply /ltP.
rewrite ltnS. apply H.
Defined.
Next Obligation.
apply semChoose in H; auto.
simpl in H.
apply /ltP. rewrite ltnS.
apply /leP. apply minusle.
Defined.
Next Obligation.
apply semChoose in H; auto.
simpl in H.
apply /leP.
move/leP: H => H.
rewrite Nat.add_assoc.
rewrite Nat.add_0_r.
apply /leP. rewrite plus2.
apply H.
Defined.

(** * Random generator of RSLs representing maps *)

Definition genRomMapRslType (e : nat) : G (rslType (2*e)) := 
 liftGen (rom2rslType e) (genRom e).


Local Obligation Tactic := intros; try omega.

(** * Random generator of local maps *)

Definition genRomMap (e : nat) : G (map e) := 
 liftGen (rom2map e) (genRom e).

Definition genRomTransPermut (e : nat) : G (permut (2*e)%coq_nat) := 
 liftGen (@rotation e) (genRomMap e).

Definition genRomRotationAsListNat (e : nat) : G (list nat) := 
 liftGen (fun p => fun2list (2*e)%coq_nat (fct p)) (genRomTransPermut e).
 
(** * Random generator of local map rotations *)

(*
Definition genRomRotationAsListnat (e : nat) : G (list nat) := 
 liftGen (@transpoCode (2*e)) (genRomMapRslType e).
*)
