Changeset 1290 for src/RTLabs

Timestamp:

Oct 4, 2011, 2:00:54 AM (8 years ago)

Author:

sacerdot

Message:

One more function ported to new Joint.

File:

• src/RTLabs/RTLAbstoRTL.ma (modified) (4 diffs)

src/RTLabs/RTLAbstoRTL.ma

@@ -942 +942 @@
   let f ≝ λsrcr. sequential rtl_params_ globals (OP2 rtl_params_ globals Or tmpr tmpr srcr) in
   let def ≝ adds_graph rtl_params1 globals (init :: (map ? ? f srcrs)) start_lbl tmp_lbl def in
-    add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true lbl_false)) def.
+    add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true) lbl_false) def.
 
 definition translate_load ≝
@@ -966 +966 @@
         let translates ≝ translates @ [
           adds_graph [
-            rtl_st_int tmpr off start_lbl
+            INT tmpr off start_lbl
           ];
           translate_op2 Oaddp tmp_addr ? save_addr [tmpr] ? ?;
           adds_graph [
-            rtl_st_load r tmp_addr1 tmp_addr2 dest_lbl
+            LOAD r tmp_addr1 tmp_addr2 dest_lbl
           ]
         ]
@@ -1039 +1039 @@
   match stmt with
   [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def
-  | _ ⇒ ? ].
-(*
   | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
   | St_const destr cst lbl' ⇒
@@ -1080 +1078 @@
   |*: cases daemon (* TODO: proofs regarding lengths of lists, examine! *)
   ]
-*) cases daemon
 qed.