Changeset 1149 for src/RTL/RTLtoERTL.ma


Ignore:
Timestamp:
Aug 30, 2011, 4:22:54 PM (9 years ago)
Author:
mulligan
Message:

changes to get everything type checking again after changing names of registers in i8051

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r1138 r1149  
    222222  [ nil ⇒ [get_params_hdw_internal]
    223223  | _ ⇒
    224     let l ≝ zip_pottier ? ? params parameters in
     224    let l ≝ zip_pottier ? ? params RegisterParams in
    225225      save_hdws l
    226226  ].
     
    258258definition get_params ≝
    259259  λparams.
    260   let n ≝ min (length ? params) (length ? parameters) in
     260  let n ≝ min (length ? params) (length ? RegisterParams) in
    261261  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
    262262  let hdw_params ≝ get_params_hdw hdw_params in
     
    394394  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
    395395  | _ ⇒
    396     let l ≝ zip_pottier ? ? params parameters in
     396    let l ≝ zip_pottier ? ? params RegisterParams in
    397397      restore_hdws l
    398398  ].
     
    434434definition set_params ≝
    435435  λparams.
    436   let n ≝ min (|params|) (|parameters|) in
     436  let n ≝ min (|params|) (|RegisterParams|) in
    437437  let hdw_stack_params ≝ split ? params n ? in
    438438  let hdw_params ≝ \fst hdw_stack_params in
     
    530530  λdef.
    531531  let nb_params ≝ |rtl_if_params def| in
    532   let added_stacksize ≝ max 0 (nb_params - |parameters|) in
     532  let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
    533533  let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
    534534  let entry' ≝ rtl_if_entry def in
Note: See TracChangeset for help on using the changeset viewer.