splitting BTL by introducing BTLmatchRTL

reduce also copy-paste between BTLtoRTLproof and RTLtoBTLproof
sharing is done in BTLmatchRTL

1 files changed, 10 insertions, 34 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index f2f99ef5..ef336de5 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -229,45 +229,21 @@ Qed.
 
 (** * Matching relation on functions *)
 
-Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := {
-  dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f);
-  dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f);
-  preserv_fnsig: fn_sig tf = RTL.fn_sig f;
-  preserv_fnparams: fn_params tf = RTL.fn_params f;
-  preserv_fnstacksize: fn_stacksize tf = RTL.fn_stacksize f
-}.
-
-Inductive match_fundef: RTL.fundef -> fundef -> Prop :=
-  | match_Internal dupmap f tf: match_function dupmap f tf -> match_fundef (Internal f) (Internal tf)
-  | match_External ef: match_fundef (External ef) (External ef).
-
-Inductive match_stackframes: RTL.stackframe -> stackframe -> Prop :=
-  | match_stackframe_intro 
-      dupmap res f sp pc rs f' pc'
-      (TRANSF: match_function dupmap f f')
-      (DUPLIC: dupmap!pc' = Some pc)
-      : match_stackframes (RTL.Stackframe res f sp pc rs) (Stackframe res f' sp pc' rs).
+(* we simply switch [f] and [tf] in the usual way *)
+Definition match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := 
+  BTLmatchRTL.match_function dupmap tf f.
 
-Lemma verify_function_correct dupmap f f' tt:
-  verify_function dupmap f' f = OK tt ->
-  fn_sig f' = RTL.fn_sig f ->
-  fn_params f' = RTL.fn_params f ->
-  fn_stacksize f' = RTL.fn_stacksize f ->
-  match_function dupmap f f'.
-Proof.
-  unfold verify_function; intro VERIF. monadInv VERIF.
-  constructor; eauto.
-  - eapply verify_cfg_correct; eauto.
-  - eapply verify_is_copy_correct; eauto.
-Qed.
+Definition match_fundef f tf := BTLmatchRTL.match_fundef tf f.
+
+Definition match_stackframes stk stk' := BTLmatchRTL.match_stackframes stk' stk.
 
 Lemma transf_function_correct f f':
   transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
-Proof. Admitted. (*
+Proof.
   unfold transf_function; unfold bind. repeat autodestruct.
   intros H _ _ X. inversion X; subst; clear X.
   eexists; eapply verify_function_correct; simpl; eauto.
-                    Qed.*)
+Qed.
 
 Lemma transf_fundef_correct f f':
   transf_fundef f = OK f' -> match_fundef f f'.
@@ -711,7 +687,7 @@ Proof.
     inv H.
     + (* Internal function *)
       inv TRANSF.
-      rename H0 into TRANSF.
+      rename H1 into TRANSF.
       eapply dupmap_entrypoint in TRANSF as ENTRY.
       eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
       apply DMC in ENTRY as DMC'.
@@ -739,7 +715,7 @@ Qed.
 Local Hint Resolve plus_one star_refl: core.
 
 Theorem transf_program_correct:
-  forward_simulation (RTL.semantics prog) (BTL.cfgsem tprog).
+  forward_simulation (RTL.semantics prog) (BTLmatchRTL.cfgsem tprog).
 Proof.
   eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=cfgsem tprog) (ltof _ omeasure) match_states).
   constructor 1; simpl.