cleaner match_states

1 files changed, 21 insertions, 16 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 4f76d0b7..2116ac70 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -83,11 +83,11 @@ Local Open Scope nat_scope.
 (* TODO: 
   faire un dessin ASCII art de la simulation avec match_states_intro 
 
-Le iblock en paramètre représente l'état de l'exécution côté BTL 
+Le (option iblock) en paramètre représente l'état de l'exécution côté BTL 
 depuis le début de l'exécution du block
 *)
 
-Inductive match_states: iblock -> RTL.state -> state -> Prop :=
+Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
   | match_states_intro (* TODO: LES DETAILS SONT SANS DOUTE A REVOIR !!! *)
       ib dupmap st f sp pc rs m st' f' pc' pc0' pc0 rs0 m0 isfst ib0
       (STACKS: list_forall2 match_stackframes st st')
@@ -98,16 +98,16 @@ Inductive match_states: iblock -> RTL.state -> state -> Prop :=
       (RIGHTA: is_right_assoc ib)
       (RTL_RUN: star RTL.step ge (RTL.State st f sp pc0 rs0 m0) E0 (RTL.State st f sp pc rs m))
       (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs m)
-      : match_states ib (RTL.State st f sp pc rs m) (State st' f' sp pc' rs m)
+      : match_states (Some ib) (RTL.State st f sp pc rs m) (State st' f' sp pc' rs m)
   | match_states_call
-      ib st st' f f' args m
+      st st' f f' args m
       (STACKS: list_forall2 match_stackframes st st')
       (TRANSF: match_fundef f f')
-      : match_states ib (RTL.Callstate st f args m) (Callstate st' f' args m)
+      : match_states None (RTL.Callstate st f args m) (Callstate st' f' args m)
   | match_states_return
-      ib st st' v m
+      st st' v m
       (STACKS: list_forall2 match_stackframes st st')
-      : match_states ib (RTL.Returnstate st v m) (Returnstate st' v m)
+      : match_states None (RTL.Returnstate st v m) (Returnstate st' v m)
    .
 
 Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
@@ -161,7 +161,7 @@ Proof.
   - constructor; eauto.
     constructor.
     apply transf_fundef_correct; auto.
-Admitted. (* TODO *)
+Qed.
 
 Lemma transf_final_states ib s1 s2 r:
   match_states ib s1 s2 -> RTL.final_state s1 r -> final_state s2 r.
@@ -209,13 +209,18 @@ La hauteur de l'arbre aussi.
 *)
 Parameter measure: iblock -> nat.
 
-Theorem opt_simu s1 t s1':
+Definition omeasure (oib: option iblock): nat :=
+ match oib with
+ | None => 0
+ | Some ib => measure ib
+ end.
+
+Theorem opt_simu s1 t s1' oib s2:
  RTL.step ge s1 t s1' ->
- forall ib s2,
- match_states ib s1 s2 ->
- exists (ib' : iblock),
-     (exists s2', step tge s2 t s2' /\ match_states ib' s1' s2')
-  \/ (measure ib' < measure ib /\ t=E0 /\ match_states ib' s1' s2) 
+ match_states oib s1 s2 ->
+ exists (oib' : option iblock),
+     (exists s2', step tge s2 t s2' /\ match_states oib' s1' s2')
+  \/ (omeasure oib' < omeasure oib /\ t=E0 /\ match_states oib' s1' s2) 
  .
 Admitted.
 
@@ -224,13 +229,13 @@ Local Hint Resolve plus_one star_refl: core.
 Theorem transf_program_correct:
   forward_simulation (RTL.semantics prog) (BTL.semantics tprog).
 Proof.
-  eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ measure) match_states).
+  eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ omeasure) match_states).
   constructor 1; simpl.
   - apply well_founded_ltof.
   - eapply transf_initial_states.
   - eapply transf_final_states.
   - intros s1 t s1' STEP i s2 MATCH. exploit opt_simu; eauto. clear MATCH STEP.
-    destruct 1 as (ib' & [ (s2' & STEP & MATCH) | (MEASURE & TRACE & MATCH) ]).
+    destruct 1 as (oib' & [ (s2' & STEP & MATCH) | (MEASURE & TRACE & MATCH) ]).
     + repeat eexists; eauto.
     + subst. repeat eexists; eauto.
   - eapply senv_preserved.