Changeset 1995 for src/RTL

Timestamp:

May 24, 2012, 7:18:35 PM (9 years ago)

Author:

campbell

Message:

Overall compiler definition; bits and pieces to
make everything happy(ish).

File:

• src/RTL/RTLToERTL.ma (modified) (2 diffs)

src/RTL/RTLToERTL.ma

@@ -4 +4 @@
 include "ERTL/ERTL.ma".
 include "joint/TranslateUtils.ma".
+
+include alias "basics/lists/list.ma".
 
 definition save_hdws ≝
@@ -412 +414 @@
 definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
 
-definition translate : rtl_program → ertl_program ≝
+definition rtl_to_ertl : rtl_program → ertl_program ≝
  λp.
   let p ≝ tailcall_simplify p in (* tailcall simplification here *)