Changeset 1062 for src/RTLabs

Timestamp:

Jul 11, 2011, 2:09:03 PM (10 years ago)

Author:

mulligan

Message:

separated jmeq and coercions from foldstuff.ma in order to fix the ongoing mess in util.ma surrounding reduce_strong

File:

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

src/RTLabs/RTLAbstoRTL.ma

@@ -3 +3 @@
 include "common/AssocList.ma".
 include "common/Graphs.ma".
-(* include "common/IntValue.ma". *)
 include "common/FrontEndOps.ma".
 
@@ -463 +462 @@
   λdest_lbl.
   λdef.
-  λprf: | destrs | = | srcrs |.
+  λprf: |destrs| = |srcrs|.
   match op1 with
   [ intermediate_op1_cast src_size src_sign dest_size ⇒
@@ -523 +522 @@
     ]
   ].
-  [ 1: @third_reduced_proof
-  | 3: @first_reduced_proof
-  
-let translate_op op destrs srcrs1 srcrs2 start_lbl dest_lbl def =
-  let ((srcrs1_common, srcrs1_rest), (srcrs2_common, srcrs2_rest)) =
-    MiscPottier.reduce srcrs1 srcrs2 in
-  let srcrs_rest = choose_rest srcrs1_rest srcrs2_rest in
-  let ((destrs_common, destrs_rest), _) =
-    MiscPottier.reduce destrs srcrs1_common in
-  let ((destrs_cted, destrs_rest), (srcrs_cted, _)) =
-    MiscPottier.reduce destrs_rest srcrs_rest in
-  let (def, tmpr) = fresh_reg def in
-  let insts_init =
-    [RTL.St_clear_carry start_lbl ;
-     RTL.St_int (tmpr, 0, start_lbl)] in
-  let f_add destr srcr1 srcr2 =
-    RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
-  let insts_add =
-    MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in
-  let f_add_cted destr srcr =
-    RTL.St_op2 (op, destr, srcr, tmpr, start_lbl) in
-  let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in
-  let f_rest destr =
-    RTL.St_op2 (op, destr, tmpr, tmpr, start_lbl) in
-  let insts_rest = List.map f_rest destrs_rest in
-  adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest)
-    start_lbl dest_lbl def
+cases not_implemented (* problem here with lengths of lists: possible bug? *)
+qed.
+
+let rec translate_mul1
+  (dummy: register) (tmpr: register) (destrs: list register)
+  (srcrs1: list register) (srcr2: register) (start_lbl: label)
+    on srcrs1 ≝
+  match destrs with
+  [ nil ⇒ adds_graph [ rtl_st_skip start_lbl ] start_lbl
+  | cons destr tl ⇒
+    match tl with
+    [ nil ⇒
+      match srcrs1 with
+      [ nil ⇒
+        adds_graph [
+          rtl_st_int tmpr (zero ?) start_lbl;
+          rtl_st_op2 Addc destr destr tmpr start_lbl
+        ] start_lbl
+      | cons srcr1 tl' ⇒
+        adds_graph [
+          rtl_st_opaccs Mul tmpr dummy srcr2 srcr1 start_lbl;
+          rtl_st_op2 Addc destr destr tmpr start_lbl
+        ] start_lbl
+      ]
+    | cons destr2 destrs ⇒
+      match srcrs1 with
+      [ nil ⇒
+        add_translates [
+          adds_graph [
+            rtl_st_int tmpr (zero ?) start_lbl;
+            rtl_st_op2 Addc destr destr tmpr start_lbl;
+            rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
+          ];
+          translate_cst (Ointconst I8 (zero ?)) destrs
+        ] start_lbl
+      | cons srcr1 srcrs1 ⇒
+        match destrs with
+        [ nil ⇒
+          add_translates [
+            adds_graph [
+              rtl_st_int tmpr (zero ?) start_lbl;
+              rtl_st_op2 Addc destr destr tmpr start_lbl;
+              rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
+            ];
+            translate_cst (Ointconst I8 (zero ?)) destrs
+          ] start_lbl
+        | cons destr2 destrs ⇒
+          add_translates [
+            adds_graph [
+              rtl_st_opaccs Mul tmpr destr2 srcr2 srcr1 start_lbl;
+              rtl_st_op2 Addc destr destr tmpr start_lbl
+            ];
+            translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2
+          ] start_lbl
+        ]
+      ]
+    ]
+  ].
+
+definition translate_muli ≝
+  λdummy: register.
+  λtmpr: register.
+  λdestrs: list register.
+  λtmp_destrs: list register.
+  λsrcrs1: list register.
+  λdummy_lbl: label.
+  λi: nat.
+  λtranslates.
+  λsrcr2i.
+  let 〈tmp_destrs1, tmp_destrs2〉 ≝ ? in ?.
+
+let translate_muli dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates
+    srcr2i =
+  let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in
+  translates @
+    (match tmp_destrs2 with
+      | [] -> []
+      | tmp_destr2 :: tmp_destrs2 ->
+        [adds_graph [RTL.St_clear_carry dummy_lbl ;
+                     RTL.St_int (tmp_destr2, 0, dummy_lbl)] ;
+         translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
+         translate_cst (AST.Cst_int 0) tmp_destrs1 ;
+         adds_graph [RTL.St_clear_carry dummy_lbl] ;
+         translate_op I8051.Addc destrs destrs tmp_destrs])
 
 definition filter_and_to_list_local_env_internal ≝