Changeset 1076


Ignore:
Timestamp:
Jul 18, 2011, 5:40:33 PM (8 years ago)
Author:
mulligan
Message:

small changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r1075 r1076  
    11include "RTL/RTL.ma".
    22include "utilities/RegisterSet.ma".
     3include "common/Identifiers.ma".
    34include "ERTL/ERTL.ma".
    45
     
    500501qed.   
    501502
     503definition 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   
     517definition 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'〉.
    502526   
    503527   
Note: See TracChangeset for help on using the changeset viewer.