add hid in BTL_SEtheory: this avoids duplication of types (and should not be harmful)

1 files changed, 15 insertions, 23 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index da680e63..9c84532b 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -1,13 +1,5 @@
 (** Refinement of BTL_SEtheory data-structures
     in order to introduce (and prove correct) a lower-level specification of the simulation test.
-
-    Ceci est un "bac à sable". 
-
-    - On introduit une représentation plus concrète pour les types d'état symbolique [sistate] et [sstate].
-    - Etant donné une spécification intuitive "*_simu" pour tester la simulation sur cette représentation des états symboliques,
-      on essaye déjà de trouver les bonnes notions de raffinement "*_refines" qui permette de prouver les lemmes "*_simu_correct".
-    - Il faudra ensuite vérifier que l'exécution symbolique préserve ces relations de raffinement !
-
 *)
 
 Require Import Coqlib Maps Floats.
@@ -41,7 +33,7 @@ Record ristate :=
 
 Definition ris_sreg_get (ris: ristate) r: sval :=
    match PTree.get r ris with
-   | None => if ris_input_init ris then Sinput r else Sundef
+   | None => if ris_input_init ris then fSinput r else fSundef
    | Some sv => sv
    end.
 Coercion ris_sreg_get: ristate >-> Funclass.
@@ -211,7 +203,7 @@ Fixpoint get_routcome ctx (rst:rstate): option routcome :=
   match rst with
   | Rfinal ris rfv => Some (rout ris rfv)
   | Rcond cond args ifso ifnot =>
-     SOME b <- seval_condition ctx cond args IN
+     SOME b <- eval_scondition ctx cond args IN
      get_routcome ctx (if b then ifso else ifnot)
   | Rabort => None
   end.
@@ -241,7 +233,7 @@ Lemma rst_simu_lroutcome rst1 rst2:
    exists ris2 rfv2, get_routcome (bctx2 ctx) rst2 = Some (rout ris2 rfv2) /\ ris_simu ris1 ris2 /\ rfv_simu rfv1 rfv2.
 Proof.
   induction 1; simpl; intros f1 f2 ctx lris1 lrfv1 ROUT; try_simplify_someHyps.
-  erewrite <- seval_condition_preserved.
+  erewrite <- eval_scondition_preserved.
   autodestruct.
   destruct b; simpl; auto.
 Qed.
@@ -252,9 +244,9 @@ Inductive rst_refines ctx: rstate -> sstate -> Prop :=
       (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv)
       : rst_refines ctx (Rfinal ris rfv) (Sfinal sis sfv)
   | Refcond cond rargs args rifso rifnot ifso ifnot
-      (RCOND: seval_condition ctx cond rargs = seval_condition ctx cond args)
-      (REFso: seval_condition ctx cond rargs = Some true -> rst_refines ctx rifso ifso)
-      (REFnot: seval_condition ctx cond rargs = Some false -> rst_refines ctx rifnot ifnot)
+      (RCOND: eval_scondition ctx cond rargs = eval_scondition ctx cond args)
+      (REFso: eval_scondition ctx cond rargs = Some true -> rst_refines ctx rifso ifso)
+      (REFnot: eval_scondition ctx cond rargs = Some false -> rst_refines ctx rifnot ifnot)
       : rst_refines ctx (Rcond cond rargs rifso rifnot) (Scond cond args ifso ifnot)
   | Refabort
       : rst_refines ctx Rabort Sabort
@@ -464,7 +456,7 @@ Proof.
   destruct i; simpl; unfold sum_left_map; try autodestruct; eauto.
 Qed.
 
-Definition ris_init: ristate := {| ris_smem:= Sinit; ris_input_init:=true; ok_rsval := nil; ris_sreg := PTree.empty _ |}.
+Definition ris_init: ristate := {| ris_smem:= fSinit; ris_input_init:=true; ok_rsval := nil; ris_sreg := PTree.empty _ |}.
 
 Lemma ris_init_correct ctx:
   ris_refines ctx ris_init sis_init.
@@ -507,7 +499,7 @@ Qed.
 Definition rexec_store chunk addr args src ris: ristate :=
    let args := list_sval_inj (List.map (ris_sreg_get ris) args) in
    let src := ris_sreg_get ris src in
-   let rm := Sstore ris.(ris_smem) chunk addr args src in
+   let rm := fSstore ris.(ris_smem) chunk addr args src in
    rset_smem rm ris.
 
 Lemma rexec_store_correct ctx chunk addr args src ris sis:
@@ -554,7 +546,7 @@ Qed.
 
 Definition rexec_op op args dst (ris:ristate): ristate :=
    let args := list_sval_inj (List.map ris args) in
-   rset_sreg dst (Sop op args) ris.
+   rset_sreg dst (fSop op args) ris.
 
 Lemma rexec_op_correct ctx op args dst ris sis:
   ris_refines ctx ris sis ->
@@ -566,7 +558,7 @@ Qed.
 
 Definition rexec_load trap chunk addr args dst (ris:ristate): ristate :=
    let args := list_sval_inj (List.map ris args) in
-   rset_sreg dst (Sload ris.(ris_smem) trap chunk addr args) ris.
+   rset_sreg dst (fSload ris.(ris_smem) trap chunk addr args) ris.
 
 Lemma rexec_load_correct ctx trap chunk addr args dst ris sis:
   ris_refines ctx ris sis ->
@@ -576,12 +568,12 @@ Proof.
   intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ; eauto.
 Qed.
 
-Lemma seval_condition_refpreserv ctx cond args ris sis:
+Lemma eval_scondition_refpreserv ctx cond args ris sis:
   ris_refines ctx ris sis ->
   ris_ok ctx ris ->
-  seval_condition ctx cond (list_sval_inj (map ris args)) = seval_condition ctx cond (list_sval_inj (map sis args)).
+  eval_scondition ctx cond (list_sval_inj (map ris args)) = eval_scondition ctx cond (list_sval_inj (map sis args)).
 Proof.
-  intros; unfold seval_condition.
+  intros; unfold eval_scondition.
   erewrite eval_list_sval_refpreserv; eauto.
 Qed.
 
@@ -745,7 +737,7 @@ Proof.
     generalize OUT; clear OUT; simpl.
     autodestruct.
     intros COND; generalize COND.
-    erewrite <- seval_condition_refpreserv; eauto.
+    erewrite <- eval_scondition_refpreserv; eauto.
     econstructor; try_simplify_someHyps.
 Qed.
 
@@ -823,7 +815,7 @@ Proof.
     generalize OUT; clear OUT; simpl.
     autodestruct.
     intros COND; generalize COND.
-    erewrite seval_condition_refpreserv; eauto.
+    erewrite eval_scondition_refpreserv; eauto.
     econstructor; try_simplify_someHyps.
 Qed.