 Timestamp:
 Aug 30, 2011, 4:22:54 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1138 r1149 222 222 [ nil ⇒ [get_params_hdw_internal] 223 223  _ ⇒ 224 let l ≝ zip_pottier ? ? params parameters in224 let l ≝ zip_pottier ? ? params RegisterParams in 225 225 save_hdws l 226 226 ]. … … 258 258 definition get_params ≝ 259 259 λparams. 260 let n ≝ min (length ? params) (length ? parameters) in260 let n ≝ min (length ? params) (length ? RegisterParams) in 261 261 let 〈hdw_params, stack_params〉 ≝ list_split ? n params in 262 262 let hdw_params ≝ get_params_hdw hdw_params in … … 394 394 [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl] 395 395  _ ⇒ 396 let l ≝ zip_pottier ? ? params parameters in396 let l ≝ zip_pottier ? ? params RegisterParams in 397 397 restore_hdws l 398 398 ]. … … 434 434 definition set_params ≝ 435 435 λparams. 436 let n ≝ min (params) ( parameters) in436 let n ≝ min (params) (RegisterParams) in 437 437 let hdw_stack_params ≝ split ? params n ? in 438 438 let hdw_params ≝ \fst hdw_stack_params in … … 530 530 λdef. 531 531 let nb_params ≝ rtl_if_params def in 532 let added_stacksize ≝ max 0 (nb_params   parameters) in532 let added_stacksize ≝ max 0 (nb_params  RegisterParams) in 533 533 let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in 534 534 let entry' ≝ rtl_if_entry def in
Note: See TracChangeset
for help on using the changeset viewer.