Changeset 1306 for src/RTLabs

Timestamp:

Oct 6, 2011, 11:19:25 AM (9 years ago)

Author:

mulligan

Message:

small changes to rtlabs. what axioms remain look hard to close. need to discuss with csc

File:

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

src/RTLabs/RTLAbstoRTL.ma

@@ -508 +508 @@
   ]
   in
-  let f ≝ λi. translate_muli globals dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in
-  let insts_mul ≝ foldi … [ ] srcrs2 in ?. [5: check insts_init.
+  let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
+  let insts_mul ≝ foldi … f [ ] srcrs2 in ?.
     add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
 *)
@@ -680 +680 @@
   λglobals: list ident.
   λdestrs: list register.
-  λprf_destrs: lt 0 (|destrs|).
+  λprf_destrs: 0 < |destrs|.
   λsrcrs1: list register.
   λsrcrs2: list register.
@@ -748 +748 @@
   λglobals: list ident.
   λdestrs: list register.
-  λdestrs_prf: lt 0 (|destrs|).
+  λdestrs_prf: 0 < |destrs|.
   λsrcrs1: list register.
   λsrcrs2: list register.
@@ -786 +786 @@
   λop2.
   λdestrs: list register.
-  λdestrs_prf: lt 0 (|destrs|).
+  λdestrs_prf: 0 < |destrs|.
   λsrcrs1: list register.
   λsrcrs2: list register.
-  λsrcrs1_prf: lt 0 (|srcrs1|). (* can this be relaxed? i think it can
-                                   but we need more dep. typ. in modu/divu
-                                   cases *)
-  λsrcrs2_prf: lt 0 (|srcrs2|).
+  λsrcrs1_prf: 0 < |srcrs1|. (* XXX: can this be relaxed? i think it can
+                                     but we need more dep. typ. in modu/divu
+                                     cases *)
+  λsrcrs2_prf: 0 < |srcrs2|.
   λstart_lbl: label.
   λdest_lbl: label.
@@ -988 +988 @@
           sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
         ];
-        translate_op2 globals Oaddp tmp_addr ? addr [tmpr] ? ?;
+        translate_op2 globals Oaddp tmp_addr … addr [tmpr] ? ?;
         adds_graph rtl_params1 globals [
           sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr)
@@ -997 +997 @@
           〈translates, result〉
     in
-    let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero ?〉 srcrs in
+    let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero …〉 srcrs in
       add_translates rtl_params1 globals translates start_lbl dest_lbl def
   ].
@@ -1028 +1028 @@
     translate_op1 globals op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
   | 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
+    translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
   | St_load ignore addr destr lbl' ⇒
-    translate_load globals (find_local_env addr lenv) … (find_local_env destr lenv) lbl lbl' def
+    translate_load globals (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
   | St_store ignore addr srcr lbl' ⇒
-    translate_store globals (find_local_env addr lenv) … (find_local_env srcr lenv) lbl lbl' def
+    translate_store globals (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
   | St_call_id f args retr lbl' ⇒
     match retr with