Changeset 2074 for src/Clight/SimplifyCasts.ma

Timestamp:

Jun 14, 2012, 10:23:08 AM (8 years ago)

Author:

garnier

Message:

Prophylactic renaming of a relation

File:

• src/Clight/SimplifyCasts.ma (modified) (8 diffs)

src/Clight/SimplifyCasts.ma

@@ -211 +211 @@
 
 (* Simulation relation used for expression evaluation. *)
-inductive simulate (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝
-| SimOk   :  (∀a:A. r1 = OK ? a → r2 = OK ? a) → simulate A r1 r2
-| SimFail : (∃err. r1 = Error ? err) → simulate A r1 r2.
+inductive res_sim (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝
+| SimOk   :  (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2
+| SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2.
 
 (* Invariant of simplify_expr *)
@@ -221 +221 @@
      result_flag = false →
      typeof e1 = typeof e2 →
-     simulate ? (exec_expr ge en m e1) (exec_expr ge en m e2) →
-     simulate ? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) →     
+     res_sim ? (exec_expr ge en m e1) (exec_expr ge en m e2) →
+     res_sim ? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) →     
      simplify_inv ge en m e1 e2 target_sz target_sg result_flag
 (* Inv_coerce_ok states that we successfuly squeezed the source expression to [target_sz]. The details are hidden in [smaller_integer_val]. *)
@@ -233 +233 @@
 (* Invariant of simplify_inside *)     
 definition conservation ≝ λe,result:expr.
-∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result)
-                                                    ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
+∀ge,en,m. res_sim ? (exec_expr ge en m e) (exec_expr ge en m result)
+                                                    ∧ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
                                                     ∧ typeof e = typeof result.
 
@@ -2077 +2077 @@
  (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
  
-lemma simulation_transitive : ∀A,r0,r1,r2. simulate A r0 r1 → simulate A r1 r2 → simulate A r0 r2.
+lemma simulation_transitive : ∀A,r0,r1,r2. res_sim A r0 r1 → res_sim A r1 r2 → res_sim A r0 r2.
 #A #r0 #r1 #r2 *
 [ 2: * #error #H >H #_ @SimFail /2 by ex_intro/
@@ -2086 +2086 @@
 
 lemma sim_related_globals : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' → 
-  (∀e. simulate ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧
-  (∀ed, ty. simulate ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)).
+  (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧
+  (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)).
 #ge #ge' #en #m #Hrelated @expr_lvalue_ind_combined
 [ 1: #sz #ty #i @SimOk #a normalize //
@@ -2237 +2237 @@
 lemma related_globals_expr_simulation : ∀ge,ge',en,m. 
   related_globals ? simplify_fundef ge ge' →
-  ∀e. simulate ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧
+  ∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧
       typeof e = typeof (simplify_e e).
 #ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?);
@@ -2253 +2253 @@
 lemma related_globals_lvalue_simulation : ∀ge,ge',en,m. 
   related_globals ? simplify_fundef ge ge' →
-  ∀e. simulate ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧
+  ∀e. res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧
       typeof e = typeof (simplify_e e).
 #ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?);
@@ -2272 +2272 @@
 lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
 related_globals ? simplify_fundef ge ge' →
-∀args. simulate ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)).
+∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)).
 #ge #ge' #en #m #Hrelated #args
 elim args