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

(** Definition and interpretation of terms representing Rooted Ordinary Maps (ROM). *)

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

Require Import prelude bFinFun cut endofun permut revsubex operations trans map.
(* Set Implicit Parameters. removed for Coq 8.7 *)

Require Import Program.

Local Obligation Tactic := intros; try omega.

(** * Recursive dependent type for rooted ordinary maps

 [(rom e)] is the type of terms representing rooted ordinary maps with [e] edges. *)

Inductive rom : nat -> Type :=
| mty : rom 0                                           (* leaf node *)
| bin : forall e1 e2, rom e1 -> rom e2 -> rom (e1+e2+1) (* binary nodes *)
| unl : forall e k, k <= 2*e -> rom e -> rom (S e).     (* unary labeled nodes *)


(** * First map code: map semantics of ROM terms *)

Program Fixpoint rom2map (e : nat) (t : rom e) : map e :=
 match t with
 | mty => map0
 | bin e1 e2 t1 t2 => isthmic (rom2map e1 t1) (rom2map e2 t2)
 | unl e _ p t => non_isthmic (rom2map e t) p
end.
(*
Solving obligations automatically...
rom2map_obligation_1 is defined
No more obligations remaining
rom2map is defined
rom2map is recursively defined (decreasing on 2nd argument)
*)

(* Program is required for type-checking: with

Fixpoint rom2map (e : nat) (t : rom e) : map e :=
 match t with
 | mty => map0
 | bin e1 e2 t1 t2 => isthmic (rom2map e1 t1) (rom2map e2 t2)
 | unl e _ p t => non_isthmic (rom2map e t) p
end.

we get the typing error

The term "non_isthmic (rom2map e0 t0) p" has type "map (e0 + 1)"
while it is expected to have type "map (S e0)". *)

(** * Map operations on RSL *)

(* First version, with numbers of edges *)

(** ** Isthmic operation *)

Program Definition isth (e1 : nat) (r1 : rslType (2*e1)) (e2 : nat) (r2 : rslType (2*e2)) : rslType (2*(e1+e2+1)) :=
 let d1 := 2*e1 in
 let d2 := 2*e2 in
 match d1 with
 | 0     =>
            match d2 with
            | 0     => @RS 1 1 _ (@RS 0 0 _ r2)
            | S d2' => @RS (d2+1) (d2+1) _ (@RS d2 d2' _ r2)
    end
 | S d1' =>
            match d2 with
            | 0   => @RS (d1+1) d1' _ (@RS d1 d1 _ r1)
            | S _ => @RS (d1+d2+1) d1' _ (@RS (d1+d2) (d1'+d2) _ (@sum_rslType d1 r1 d2 r2))
            end
 end.
(* No longer necessary, with Coq 8.9.0:

Next Obligation.
change (d2 = 0) ; auto.
Qed.
Next Obligation.
assert (2 * (e1 + e2 + 1) = 2 * e1 + 2 * e2 +2) by omega.
rewrite H ; change (2 = d1 + d2 + 2) ; omega.
Qed.
Next Obligation.
assert (2 * (e1 + e2 + 1) = 2 * e1 + 2 * e2 +2) by omega.
rewrite H.
change (S (d2 + 1) = d1 + d2 + 2)  ; omega.
Qed.
Next Obligation.
assert (2 * (e1 + e2 + 1) = 2 * e1 + 2 * e2 +2) by omega.
rewrite H.
change (S (d1 + 1) = d1 + d2 + 2)  ; omega.
Qed.
Next Obligation.
assert (2 * (e1 + e2 + 1) = 2 * e1 + 2 * e2 +2) by omega.
rewrite H.
change (S (d1 + d2 +1) = d1 + d2 + 2)  ; omega.
Qed.
*)

(** ** Non-isthmic operation *)

Program Definition noni e (r : rslType (2*e)) k (k_le_2e : k <= 2*e) : rslType (2*(e+1)) :=
 let d := 2*e in
 match d with
 | 0    => @RS 1 0 _ (@RS 0 0 _ r)
 | S d' => @RS (d+1) k _ (@RS d d' _ r)
 end.
(* No longer necessary, with Coq 8.9.0:

Next Obligation.
change (d =0); omega.
Qed.
Next Obligation.
assert ( 2 * (e + 1) = 2 * e + 2) by omega.
rewrite H; change (2 = d + 2); omega.
Qed.
Next Obligation.
change (k <= 2 * e + 1) ; omega.
Qed.
Next Obligation.
assert ( 2 * (e + 1) = 2 * e + 2) by omega.
rewrite H; change (S (d + 1) =  d + 2) ; omega.
Qed.
*)


(** * Second map code: RSL semantics of ROM terms *)

Program Fixpoint rom2rslType (e : nat) (t : rom e) : rslType (2*e) :=
 match t with
 | mty => R0
 | bin e1 e2 t1 t2 => isth e1 (rom2rslType e1 t1) e2 (rom2rslType e2 t2)
 | unl e k k_le_2e t => noni e (rom2rslType e t) k k_le_2e
end.
(*
Solving obligations automatically...
rom2rslType_obligation_1 is defined
No more obligations remaining
rom2rslType is defined
rom2rslType is recursively defined (decreasing on 2nd argument)
*)



(* TODO:

(** * Soundness lemma *)

Lemma map_code_sound: forall e (r : rom e),
 is_transitive (rslType2permut (rom2rslType e r)).
Proof.
Admitted.

*)


(* Local Variables: *)
(* coq-prog-name: "/Users/magaud/.opam/4.07.0/bin/coqtop" *)
(* suffixes: .v *)
(* End: *)