Changeset 763 for src

Timestamp:

Apr 20, 2011, 11:33:35 AM (10 years ago)

Author:

mulligan

Message:

Changes to RTL-ERTL pass.

File:

• src/RTL/RTLtoERTL.ma (modified) (1 diff)

src/RTL/RTLtoERTL.ma

@@ -118 +118 @@
   ].
   
-definition fresh_register ≝
-  λdef.
-    
+axiom fresh_reg: ertl_internal_function → ertl_internal_function × register.
+
+let rec fresh_regs (def: ertl_internal_function) (n: nat) on n ≝
+  match n with
+  [ O ⇒ 〈def, [ ]〉
+  | S n' ⇒
+    let 〈def', regs'〉 ≝ fresh_regs def n' in
+    let 〈def', reg〉 ≝ fresh_reg def' in
+      〈def', reg :: regs'〉
+  ].
+  
+definition save_hdws ≝
+  λ