RTL -> RTLpath -> RTL

1 files changed, 70 insertions, 1 deletions

diff --git a/mppa_k1c/lib/RTLpath.v b/mppa_k1c/lib/RTLpath.v
index 228bc95b..f170e0c3 100644
--- a/mppa_k1c/lib/RTLpath.v
+++ b/mppa_k1c/lib/RTLpath.v
@@ -135,6 +135,15 @@ Coercion fundef_RTL: fundef >-> RTL.fundef.
 Definition program_RTL (p: program) : RTL.program := transform_program fundef_RTL p.
 Coercion program_RTL: program >-> RTL.program.
 
+Definition match_program_RTL (p: RTLpath.program) (tp: RTL.program) :=
+  match_program (fun ctx f tf => tf = fundef_RTL f) eq p tp.
+
+Lemma transf_program_match:
+  forall p, match_program_RTL p (program_RTL p).
+Proof.
+  intros. eapply match_transform_program; eauto.
+Qed.
+
 (** * Path-step semantics of RTLpath programs *)
 
 (* Semantics of internal instructions (mimicking RTL semantics) *)
@@ -330,7 +339,6 @@ Definition final_state (st: state) (i:int): Prop
 Definition semantics (p: program) :=
   Semantics (step (Genv.globalenv (program_RTL p))) (initial_state p) final_state (Genv.globalenv p).
 
-
 (** * Proving the bisimulation between (semantics p) and (RTL.semantics p). *)
 
 (** ** Preliminaries: simple tactics for option-monad *)
@@ -516,6 +524,67 @@ Qed.
 
 End CORRECTNESS.
 
+Lemma program_equals {A B: Type} : forall (p1 p2: AST.program A B),
+  prog_defs p1 = prog_defs p2 ->
+  prog_public p1 = prog_public p2 ->
+  prog_main p1 = prog_main p2 ->
+  p1 = p2.
+Proof.
+  intros. destruct p1. destruct p2. simpl in *. subst. auto.
+Qed.
+
+Lemma cons_extract {A: Type} : forall (l: list A) a b, a = b -> a::l = b::l.
+Proof.
+  intros. congruence.
+Qed.
+
+(* Definition transf_program : RTLpath.program -> RTL.program := transform_program fundef_RTL.
+
+Lemma transf_program_proj: forall p, program_RTL (transf_program p) = p.
+Proof.
+  intros p. destruct p as [defs pub main]. unfold program_proj. simpl.
+  apply program_equals; simpl; auto.
+  induction defs.
+  - simpl; auto.
+  - simpl. rewrite IHdefs. 
+    destruct a as [id gd]; simpl.
+    destruct gd as [f|v]; simpl; auto.
+    rewrite transf_fundef_proj. auto.
+Qed. *)
+
+Lemma match_program_transf:
+  forall p tp, match_program_RTL p tp -> program_RTL p = tp.
+Proof.
+  intros p tp H. inversion_clear H. inv H1.
+  destruct p as [defs pub main]. destruct tp as [tdefs tpub tmain]. simpl in *.
+  subst. unfold program_RTL. unfold transform_program. simpl.
+  apply program_equals; simpl; auto.
+  induction H0; simpl; auto.
+  rewrite IHlist_forall2. apply cons_extract.
+  destruct a1 as [ida gda]. destruct b1 as [idb gdb].
+  simpl in *.
+  inv H. inv H2.
+  - simpl in *. subst. auto.
+  - simpl in *. subst. inv H. auto.
+Qed.
+
+
+Section PRESERVATION.
+
+Variable prog: RTLpath.program.
+Variable tprog: RTL.program.
+Hypothesis TRANSF: match_program_RTL prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Theorem transf_program_correct:
+  forward_simulation (RTLpath.semantics prog) (RTL.semantics tprog).
+Proof.
+  pose proof (match_program_transf prog tprog TRANSF) as TR. subst.
+  eapply RTLpath_correct.
+Qed.
+
+End PRESERVATION.