progress in BTL_SEsimuref

1 files changed, 22 insertions, 0 deletions

diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v
index bcddcf5d..ec83b3c1 100644
--- a/scheduling/BTL_Scheduler.v
+++ b/scheduling/BTL_Scheduler.v
@@ -9,6 +9,28 @@ Axiom scheduler: BTL.function -> BTL.code.
 
 Extract Constant scheduler => "BTLScheduleraux.btl_scheduler".
 
+(* TODO: could be useful ?
+Definition equiv_input_regs (f1 f2: BTL.function): Prop :=
+    (forall pc, (fn_code f1)!pc = None <-> (fn_code f2)!pc = None) 
+ /\ (forall pc ib1 ib2, (fn_code f1)!pc = Some ib1 -> (fn_code f2)!pc = Some ib2 -> ib1.(input_regs) = ib2.(input_regs)).
+
+Lemma equiv_input_regs_union f1 f2:
+ equiv_input_regs f1 f2 -> forall tbl, union_inputs f1 tbl = union_inputs f2 tbl.
+Proof.
+ intros (EQNone & EQSome). induction tbl as [|pc l']; simpl; auto.
+ generalize (EQNone pc) (EQSome pc); clear EQNone EQSome; intros EQN EQS.
+ do 2 autodestruct; intuition; try_simplify_someHyps. 
+ intros; exploit EQS; eauto; clear EQS. congruence.
+Qed.
+
+Lemma equiv_input_regs_pre f1 f2 tbl or:
+ equiv_input_regs f1 f2 -> pre_inputs f1 tbl or = pre_inputs f2 tbl or.
+Proof.
+   intros; unfold pre_inputs; erewrite equiv_input_regs_union; auto.
+Qed.
+*)
+
+
 (* a specification of the verification to do on each function *)
 Record match_function (f1 f2: BTL.function): Prop := {
   preserv_fnsig: fn_sig f1 = fn_sig f2;