Changeset 2105 for src/Clight/labelSimulation.ma
 Timestamp:
 Jun 21, 2012, 5:21:04 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r2103 r2105 3 3 include "Clight/Cexec.ma". 4 4 include "Clight/CexecInd.ma". 5 6 (* TODO: make something general that can live in common/Globalenvs.ma. *)7 record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {8 rg_find_symbol: ∀s.9 find_symbol … ge s = find_symbol … ge' s;10 rg_find_funct: ∀v,f.11 find_funct … ge v = Some ? f →12 find_funct … ge' v = Some ? (t f);13 rg_find_funct_ptr: ∀b,f.14 find_funct_ptr … ge b = Some ? f →15 find_funct_ptr … ge' b = Some ? (t f)16 }.17 18 (* FIXME with a more general result *)19 axiom transform_program_related : ∀F,V,init,t,p.20 related_globals F t (globalenv (λ_.F) V init p) (globalenv (λ_.F) V init (transform_program … p (λ_.t))).21 (*22 #F #V #init #t * #vars #fns #main23 whd in match (transform_program ?????);24 whd in match (transf_program ????);25 elim fns26 [ % [ //  * [  #sz #i  #f  #r  #ptr ] #f #F1 whd in F1:(??%?); destruct27 cases (eq_offset ??) in F1; #F1 whd in F1:(??%?);28 whd in match (globalenv ?????) in F1;29 whd in match (globalenv_allocmem ????) in F1;30 elim31 %32 [ #s33 *)34 5 35 6 (* Useful for breaking up the labeling functions, because we don't care about … … 84 55 85 56 theorem label_expr_ok : ∀ge,ge',en,m. 86 related_globals ?label_fundef ge ge' →57 related_globals … label_fundef ge ge' → 87 58 (∀e,v,tr. 88 59 exec_expr ge en m e = OK … 〈v,tr〉 → … … 274 245 275 246 lemma label_exprs_ok : ∀ge,ge'. 276 related_globals ?label_fundef ge ge' →247 related_globals … label_fundef ge ge' → 277 248 ∀en,m,es,vs,tr. 278 249 exec_exprlist ge en m es = OK … 〈vs,tr〉 → … … 397 368 398 369 lemma opt_find_funct : ∀ge,ge',m,vf,fd. 399 related_globals ?label_fundef ge ge' →370 related_globals … label_fundef ge ge' → 400 371 opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd → 401 372 opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (label_fundef fd). … … 684 655 for labeled_statements. *) 685 656 lemma step_with_labels_partial : ∀ge,ge'. 686 related_globals ?label_fundef ge ge' →657 related_globals … label_fundef ge ge' → 687 658 ∀s1,s1',tr,s2. 688 659 state_with_labels_partial s1 s1' → … … 1065 1036 1066 1037 theorem step_with_labels : ∀ge,ge'. 1067 related_globals ?label_fundef ge ge' →1038 related_globals … label_fundef ge ge' → 1068 1039 ∀s1,s1',tr,s2. 1069 1040 state_with_labels s1 s1' → … … 1110 1081 whd in match (make_initial_state ?); 1111 1082 letin ge' ≝ (make_global ?) 1112 cut (related_globals ?label_fundef ge ge')1083 cut (related_globals … label_fundef ge ge') 1113 1084 [ // ] #RG 1114 1085 % [2: %
Note: See TracChangeset
for help on using the changeset viewer.