Changeset 1072 for src/Cminor/toRTLabs.ma
 Timestamp:
 Jul 15, 2011, 4:56:04 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/toRTLabs.ma
r1070 r1072 21 21 〈add ?? en id r, gen'〉) 〈en, gen〉. 22 22 23 lemma lookup_sigma : ∀tag,A,m. ∀i:(Σl:identifier tag. lookup tag A m l ≠ None ?). 24 lookup tag A m i ≠ None ?. 25 #tag #A #m * #i #H @H 26 qed. 27 23 28 (* Add a statement to the graph, *without* updating the entry label. *) 24 29 definition fill_in_statement : label → statement → internal_function → internal_function ≝ … … 28 33 (f_stacksize f) (add ?? (f_graph f) l s) 29 34 (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?). 30 @lookup_add_oblivious [ cases (f_entry f)  cases (f_exit f) ] //35 @lookup_add_oblivious @lookup_sigma 31 36 qed. 32 37 … … 38 43 (f_stacksize f) (add ?? (f_graph f) l s) 39 44 (dp ?? l ?) (dp ?? (f_exit f) ?). 40 [ %{s} @lookup_add_hit41  @lookup_add_oblivious cases (f_exit f) //45 [ >lookup_add_hit % #E destruct 46  @lookup_add_oblivious @lookup_sigma 42 47 ] qed. 43 48 … … 52 57 (f_stacksize f) (add ?? (f_graph f) l s') 53 58 (dp ?? l ?) (dp ?? (f_exit f) ?)). 54 [ %{s'} @lookup_add_hit55  @lookup_add_oblivious cases (f_exit f) //59 [ >lookup_add_hit % #E destruct 60  @lookup_add_oblivious @lookup_sigma 56 61 ] qed. 57 (* 58 (* Generate a fresh label and use it as a dangling entry point, to be filled in 59 later with the loop head. *) 60 definition add_loop_label_to_graph : internal_function → internal_function ≝ 61 λf. 62 let 〈l,g〉 ≝ fresh … (f_labgen f) in 63 (mk_internal_function g (f_reggen f) 64 (f_result f) (f_params f) (f_locals f) 65 (f_stacksize f) (f_graph f) l (f_exit f)). 66 *) 62 67 63 definition fresh_reg : internal_function → typ → register × internal_function ≝ 68 64 λf,ty. … … 296 292 OK ? f 297 293 . 298 % [2,4: @lookup_add_hit  *: skip ] 294 >lookup_add_hit % #E destruct 299 295 qed. 300 296
Note: See TracChangeset
for help on using the changeset viewer.