remove todos, clean

1 files changed, 46 insertions, 0 deletions

diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v
index 0662a357..78c597e0 100644
--- a/scheduling/BTL_Scheduler.v
+++ b/scheduling/BTL_Scheduler.v
@@ -46,6 +46,52 @@ Record match_function (f1 f2: BTL.function): Prop := {
                     exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2);
 }.
 
+Inductive match_fundef: fundef -> fundef -> Prop :=
+  | match_Internal f f': match_function f f' -> match_fundef (Internal f) (Internal f')
+  | match_External ef: match_fundef (External ef) (External ef).
+
+Inductive match_stackframes: stackframe -> stackframe -> Prop :=
+  | match_stackframe_intro 
+      res f sp pc rs rs' f'
+      (EQREGS: forall r, rs # r = rs' # r)
+      (TRANSF: match_function f f')
+      : match_stackframes (BTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc rs').
+
+Inductive match_states: state -> state -> Prop :=
+  | match_states_intro 
+      st f sp pc rs rs' m st' f'
+      (EQREGS: forall r, rs # r = rs' # r)
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: match_function f f')
+      : match_states (State st f sp pc rs m) (State st' f' sp pc rs' m)
+  | match_states_call
+      st st' f f' args m
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: match_fundef f f')
+      : match_states (Callstate st f args m) (Callstate st' f' args m)
+  | match_states_return
+      st st' v m
+      (STACKS: list_forall2 match_stackframes st st')
+      : match_states (Returnstate st v m) (Returnstate st' v m)
+   .
+
+Lemma match_stack_equiv stk1 stk2:
+  list_forall2 match_stackframes stk1 stk2 -> 
+  forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
+  list_forall2 match_stackframes stk1 stk3.
+Proof.
+  induction 1; intros stk3 EQ; inv EQ; constructor; eauto.
+  inv H3; inv H; econstructor; eauto.
+  intros; rewrite <- EQUIV; auto.
+Qed.
+
+Lemma match_states_equiv s1 s2 s3: match_states s1 s2 -> equiv_state s2 s3 -> match_states s1 s3.
+Proof.
+  Local Hint Resolve match_stack_equiv: core.
+  destruct 1; intros EQ; inv EQ; econstructor; eauto.
+  intros; rewrite <- EQUIV; auto.
+Qed.
+
 Local Open Scope error_monad_scope.
 
 Fixpoint check_symbolic_simu_rec (f1 f2: BTL.function) (lpc: list node): res unit :=