Changeset 1131 for src/RTL

Timestamp:

Aug 29, 2011, 5:19:31 PM (10 years ago)

Author:

mulligan

Message:

changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h in favourn of unified instruction ertl_st_addr

File:

• src/RTL/RTLtoERTL.ma (modified) (3 diffs)

src/RTL/RTLtoERTL.ma

@@ -97 +97 @@
   | ertl_st_pop r _ ⇒ ertl_st_pop r l
   | ertl_st_push r _ ⇒ ertl_st_push r l
-  | ertl_st_addr_h r id _ ⇒ ertl_st_addr_h r id l
-  | ertl_st_addr_l r id _ ⇒ ertl_st_addr_l r id l
+  | ertl_st_addr r1 r2 x _ ⇒ ertl_st_addr r1 r2 x l
   | ertl_st_int r i _ ⇒ ertl_st_int r i l
   | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
@@ -489 +488 @@
   [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def
   | rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def
-  | rtl_st_addr r1 r2 x lbl' ⇒
-    adds_graph [
-      ertl_st_addr_l r1 x lbl;
-      ertl_st_addr_h r2 x lbl
-    ] lbl lbl' def
+  | rtl_st_addr r1 r2 x lbl' ⇒ add_graph lbl (ertl_st_addr r1 r2 x lbl') def
   | rtl_st_stack_addr r1 r2 lbl' ⇒
     adds_graph [
@@ -619 +614 @@
       | ertl_st_pop _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes' 
       | ertl_st_push _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_addr_h _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
-      | ertl_st_addr_l _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
+      | ertl_st_addr _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
       | ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
       | ertl_st_move _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'