 Timestamp:
 Jul 18, 2011, 5:40:33 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1075 r1076 1 1 include "RTL/RTL.ma". 2 2 include "utilities/RegisterSet.ma". 3 include "common/Identifiers.ma". 3 4 include "ERTL/ERTL.ma". 4 5 … … 500 501 qed. 501 502 503 definition translate_funct_internal ≝ 504 λdef. 505 let nb_params ≝ rtl_if_params def in 506 let added_stacksize ≝ max 0 (nb_params  parameters) in 507 let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in 508 let def' ≝ 509 mk_ertl_internal_function 510 (rtl_if_luniverse def) (rtl_if_runiverse def) 511 nb_params new_locals ((rtl_if_stacksize def) + added_stacksize) 512 (empty_map ? ?) (rtl_if_entry def) (rtl_if_exit def) in 513 let def' ≝ fold ? ? translate_stmt (rtl_if_graph def) def' in 514 let def' ≝ add_pro_and_epilogue (rtl_if_params def) (rtl_if_result def) def' in 515 def'. 516 517 definition translate_funct ≝ 518 λid_def: ident × ?. 519 let 〈id, def〉 ≝ id_def in 520 let def' ≝ 521 match def with 522 [ rtl_f_internal def ⇒ ertl_f_internal (translate_funct_internal def) 523  rtl_f_external def ⇒ ertl_f_external def 524 ] in 525 〈id, def'〉. 502 526 503 527
Note: See TracChangeset
for help on using the changeset viewer.