 Timestamp:
 Jul 19, 2011, 12:23:32 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1076 r1077 7 7 λl: label. 8 8 λp: ertl_internal_function. 9 λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?. 9 10 let ertl_if_luniverse' ≝ ertl_if_luniverse p in 10 11 let ertl_if_runiverse' ≝ ertl_if_runiverse p in … … 18 19 ertl_if_params' ertl_if_locals' ertl_if_stacksize' 19 20 ertl_if_graph' ertl_if_entry' ertl_if_exit'. 21 @prf 22 qed. 20 23 21 24 definition change_entry_label ≝ 22 25 λl: label. 23 26 λp: ertl_internal_function. 27 λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?. 24 28 let ertl_if_luniverse' ≝ ertl_if_luniverse p in 25 29 let ertl_if_runiverse' ≝ ertl_if_runiverse p in … … 33 37 ertl_if_params' ertl_if_locals' ertl_if_stacksize' 34 38 ertl_if_graph' ertl_if_entry' ertl_if_exit'. 39 @prf 40 qed. 35 41 36 42 definition add_graph ≝ … … 48 54 mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse' 49 55 ertl_if_params' ertl_if_locals' ertl_if_stacksize' 50 ertl_if_graph' ertl_if_entry' ertl_if_exit'. 56 ertl_if_graph' ? ?. 57 normalize nodelta; 58 [1: generalize in match ertl_if_entry'; 59 #HYP 60 cases HYP 61 #LBL #LBL_PRF 62 % 63 [1: @LBL 64 2: @graph_add_lookup 65 @LBL_PRF 66 ] 67 2: generalize in match ertl_if_exit'; 68 #HYP 69 cases HYP 70 #LBL #LBL_PRF 71 % 72 [1: @LBL 73 2: @graph_add_lookup 74 @LBL_PRF 75 ] 76 ] 77 qed. 51 78 52 79 definition fresh_label ≝ … … 325 352 in 326 353 let def ≝ add_graph tmp_lbl last_stmt def in 327 change_exit_label tmp_lbl def 354 change_exit_label tmp_lbl def ? 328 355 ] ?. 329 cases not_implemented (* dep types here *)356 cases not_implemented (* dep types here, bug in matita too! *) 330 357 qed. 331 358 … … 471 498 ertl_st_get_hdw r2 RegisterSPH lbl 472 499 ] lbl lbl' def 473  rtl_st_int r i lbl' ⇒ add_graph lbl (ertl_st_int r i lbl') def500  rtl_st_int r i lbl' ⇒ add_graph lbl (ertl_st_int r i lbl') def 474 501  rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def 475 502  rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒ … … 506 533 let added_stacksize ≝ max 0 (nb_params  parameters) in 507 534 let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in 535 let entry' ≝ rtl_if_entry def in 536 let exit' ≝ rtl_if_exit def in 508 537 let def' ≝ 509 538 mk_ertl_internal_function 510 539 (rtl_if_luniverse def) (rtl_if_runiverse def) 511 540 nb_params new_locals ((rtl_if_stacksize def) + added_stacksize) 512 (empty_map ? ?) (rtl_if_entry def) (rtl_if_exit def)in513 let def' ≝ fold ? ? translate_stmt (rtl_if_graph def) def' in541 (empty_map ? ?) ? ? in 542 let def' ≝ foldi ? ? ? translate_stmt (rtl_if_graph def) def' in 514 543 let def' ≝ add_pro_and_epilogue (rtl_if_params def) (rtl_if_result def) def' in 515 544 def'. 545 [1: cases entry' 546 #LBL #LBL_PRF 547 % 548 [1: @LBL 549 2: @LBL_PRF 516 550 517 551 definition translate_funct ≝ … … 520 554 let def' ≝ 521 555 match def with 522 [ rtl_f_internal def ⇒ ertl_f_internal(translate_funct_internal def)523  rtl_f_external def ⇒ ertl_f_externaldef556 [ Internal def ⇒ Internal ? (translate_funct_internal def) 557  External def ⇒ External ? def 524 558 ] in 525 559 〈id, def'〉. 526 527 560 561 definition generate ≝ 562 λstmt. 563 λdef. 564 let 〈entry, nuniv〉 ≝ fresh_label def in 565 let graph ≝ add ? ? (ertl_if_graph def) entry stmt in 566 mk_ertl_internal_function 567 nuniv (ertl_if_runiverse def) (ertl_if_params def) 568 (ertl_if_locals def) (ertl_if_stacksize def) graph 569 entry (ertl_if_exit def). 570 571 let generate stmt def = 572 let entry = Label.Gen.fresh def.ERTL.f_luniverse in 573 let def = 574 { def with ERTL.f_graph = Label.Map.add entry stmt def.ERTL.f_graph } in 575 { def with ERTL.f_entry = entry } 576 577 528 578 definition save_return_internal ≝ 529 579 λr.
Note: See TracChangeset
for help on using the changeset viewer.