Changeset 1307 for src/RTLabs

Timestamp:

Oct 6, 2011, 2:08:53 PM (8 years ago)

Author:

mulligan

Message:

adding translate_cst

Location:

src/RTLabs

Files:

• RTLAbstoRTL.ma (modified) (2 diffs)
• syntax.ma (modified) (1 diff)

src/RTLabs/RTLAbstoRTL.ma

@@ -127 +127 @@
   λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl.
 
-(*CSC: XXXXX *)
-axiom translate_cst:
-  ∀globals.
-  ∀cst: constant.
-  ∀destrs: list register.
-  ∀start_lbl: label.
-  ∀dest_lbl: label.
-  ∀def: rtl_internal_function globals.
-    rtl_internal_function globals.
-
+let rec translate_cst
+  (globals: list ident) (cst: constant) (destrs: list register)
+    (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function globals)
+      on cst: rtl_internal_function globals ≝
+  match cst with
+  [ Ointconst size const ⇒
+    match destrs with
+    [ nil        ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
+    | cons hd tl ⇒ ?
+    ]
+  | Ofloatconst float ⇒ ⊥
+  | Oaddrsymbol id offset ⇒ ?
+  | Oaddrstack offset ⇒ ?
+  ].
+  [5: cases not_implemented (* XXX: float, error_float in o'caml *)
+  ].
+  
 definition translate_move_internal ≝
   λglobals.
@@ -1029 +1036 @@
   | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
     translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
+    (* XXX: should we be ignoring this? *)
   | St_load ignore addr destr lbl' ⇒
     translate_load globals (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
+    (* XXX: should we be ignoring this? *)
   | St_store ignore addr srcr lbl' ⇒
     translate_store globals (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def

src/RTLabs/syntax.ma

@@ -1 @@
-
 include "basics/logic.ma".