Changeset 763


Ignore:
Timestamp:
Apr 20, 2011, 11:33:35 AM (9 years ago)
Author:
mulligan
Message:

Changes to RTL-ERTL pass.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r759 r763  
    118118  ].
    119119 
    120 definition fresh_register ≝
    121   λdef.
    122    
     120axiom fresh_reg: ertl_internal_function → ertl_internal_function × register.
     121
     122let rec fresh_regs (def: ertl_internal_function) (n: nat) on n ≝
     123  match n with
     124  [ O ⇒ 〈def, [ ]〉
     125  | S n' ⇒
     126    let 〈def', regs'〉 ≝ fresh_regs def n' in
     127    let 〈def', reg〉 ≝ fresh_reg def' in
     128      〈def', reg :: regs'〉
     129  ].
     130 
     131definition save_hdws ≝
     132  λ
Note: See TracChangeset for help on using the changeset viewer.