Changeset 1954
 Timestamp:
 May 16, 2012, 2:44:05 PM (8 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r1930 r1954 7 7 8 8 (* TODO: make something general that can live in common/Globalenvs.ma. *) 9 record related_globals ( ge:genv) (ge':genv) : Prop ≝ {9 record related_globals (F:Type[0]) (t:F → F) (ge:genv_t Genv F) (ge':genv_t Genv F) : Prop ≝ { 10 10 rg_find_symbol: ∀s. 11 11 find_symbol ?? ge s = find_symbol ?? ge' s; 12 12 rg_find_funct: ∀v,f. 13 13 find_funct ?? ge v = Some ? f → 14 find_funct ?? ge' v = Some ? (label_fundef f) 14 find_funct ?? ge' v = Some ? (t f); 15 rg_find_funct_ptr: ∀b,f. 16 find_funct_ptr ?? ge b = Some ? f → 17 find_funct_ptr ?? ge' b = Some ? (t f) 15 18 }. 19 20 (* FIXME with a more general result *) 21 axiom transform_program_related : ∀F,V,init,t,p. 22 related_globals F t (globalenv Genv ? V init p) (globalenv Genv ? V init (transform_program ??? p t)). 23 (* 24 #F #V #init #t * #vars #fns #main 25 whd in match (transform_program ?????); 26 whd in match (transf_program ????); 27 elim fns 28 [ % [ //  * [  #sz #i  #f  #r  #ptr ] #f #F1 whd in F1:(??%?); destruct 29 cases (eq_offset ??) in F1; #F1 whd in F1:(??%?); 30 whd in match (globalenv ?????) in F1; 31 whd in match (globalenv_allocmem ????) in F1; 32 elim 33 % 34 [ #s 35 *) 16 36 17 37 (* Useful for breaking up the labeling functions, because we don't care about … … 22 42 #A #B #C #D * // 23 43 qed. 44 24 45 25 46 (* Similarly, lemma to break up label_expr, label_exprs and label_statement in … … 71 92 72 93 theorem label_expr_ok : ∀ge,ge',en,m. 73 related_globals ge ge' →94 related_globals ? label_fundef ge ge' → 74 95 (∀e,v,tr. 75 96 exec_expr ge en m e = OK … 〈v,tr〉 → … … 261 282 262 283 lemma label_exprs_ok : ∀ge,ge'. 263 related_globals ge ge' →284 related_globals ? label_fundef ge ge' → 264 285 ∀en,m,es,vs,tr. 265 286 exec_exprlist ge en m es = OK … 〈vs,tr〉 → … … 384 405 385 406 lemma opt_find_funct : ∀ge,ge',m,vf,fd. 386 related_globals ge ge' →407 related_globals ? label_fundef ge ge' → 387 408 opt_to_io io_out io_in … m (find_funct ?? ge vf) = Value … fd → 388 409 opt_to_io io_out io_in … m (find_funct ?? ge' vf) = Value … (label_fundef fd). … … 671 692 for labeled_statements. *) 672 693 lemma step_with_labels_partial : ∀ge,ge'. 673 related_globals ge ge' →694 related_globals ? label_fundef ge ge' → 674 695 ∀s1,s1',tr,s2. 675 696 state_with_labels_partial s1 s1' → … … 1052 1073 1053 1074 theorem step_with_labels : ∀ge,ge'. 1054 related_globals ge ge' →1075 related_globals ? label_fundef ge ge' → 1055 1076 ∀s1,s1',tr,s2. 1056 1077 state_with_labels s1 s1' → … … 1081 1102 ] qed. 1082 1103 1083 1084 1085 1086 1104 (* FIXME: to globalenvs and prove *) 1105 axiom transform_program_init_mem : ∀A,B,V,p,f,init. 1106 init_mem Genv ?? init p = init_mem Genv ?? init (transform_program A B V p f). 1107 1108 1109 lemma initial_state_in_simulation : ∀p,s. 1110 make_initial_state p = OK ? s → 1111 ∃s'. make_initial_state (clight_label p) = OK ? s' ∧ state_with_labels s s'. 1112 * #vars #fns #main #s 1113 whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX 1114 cases (bind_inversion ????? EX) EX #m * #Em #EX 1115 cases (bind_inversion ????? EX) EX #b * #Emain #EX 1116 cases (bind_inversion ????? EX) EX #fd * #Emain' #EX 1117 whd in EX:(??%%); destruct 1118 whd in match (make_initial_state ?); 1119 letin ge' ≝ (make_global ?) 1120 cut (related_globals ? label_fundef ge ge') 1121 [ // ] #RG 1122 % [2: % 1123 [ whd in ⊢ (??%?); 1124 change with (transform_program ??? (mk_program …) label_fundef) in match (mk_program ??? (transf_program ????) ?); 1125 <transform_program_init_mem >Em in ⊢ (??%?); 1126 whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?); 1127 whd in ⊢ (??%?); >(rg_find_funct_ptr … RG … Emain') 1128 whd in ⊢ (??%?); @refl 1129  /3/ 1130 ]  skip ] 1131 qed. 1132 1133 1134 
src/common/Errors.ma
r1949 r1954 232 232 qed. 233 233 234 lemma opt_eq_from_res : ∀T,m,e,v. 235 opt_to_res T m e = return v → 236 e = Some T v. 237 #T #m * [ #v #E normalize in E; destruct  #e' #v #E normalize in E; destruct % ] 238 qed. 239 240 coercion opt_eq_from_res : 241 ∀T,m,e,v. ∀E:opt_to_res T m e = return v. e = Some T v ≝ opt_eq_from_res 242 on _E:eq (res ?) ?? to eq (option ?) ??. 243 234 244 (* A variation of bind and its notation that provides an equality proof for 235 245 later use. *)
Note: See TracChangeset
for help on using the changeset viewer.