Changeset 1331 for src/RTLabs

Timestamp:

Oct 10, 2011, 10:21:35 AM (9 years ago)

Author:

mulligan

Message:

some changes, but i now have two contradictory proof obligations.

File:

• src/RTLabs/RTLabsToRTL.ma (modified) (6 diffs)

src/RTLabs/RTLabsToRTL.ma

@@ -539 +539 @@
     translates @ tmp_destrs2'.
 
-(*
+axiom foldi_strong:
+  ∀a: Type[0].
+  ∀b: Type[0].
+  ∀the_list: list b.
+  ∀f: ∀n: nat. n ≤ |the_list| → a → b → a.
+  ∀seed: a.
+    a.
+  
 definition translate_mul ≝
   λglobals: list ident.
@@ -545 +552 @@
   λsrcrs1: list register.
   λsrcrs2: list register.
+  λregs_proof: |srcrs2| = |destrs|.
   λstart_lbl: label.
   λdest_lbl: label.
@@ -550 +558 @@
   let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
   let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
-  let 〈def, tmp_destrs〉 ≝ fresh_regs rtl_params0 globals def (|destrs|) in
-  let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
-  let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
-  let insts_init ≝ [
-    translate_move globals fresh_srcrs1 srcrs1;
-    translate_move globals fresh_srcrs2 srcrs2;
-    translate_cst globals (Ointconst I8 (zero …)) destrs
-  ]
-  in
-  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.
-*)
-
-axiom translate_mul:
-  ∀globals: list ident.
-  ∀destrs: list register.
-  ∀srcrs1: list register.
-  ∀srcrs2: list register.
-  ∀start_lbl: label.
-  ∀dest_lbl: label.
-  ∀def: rtl_internal_function globals.
-    rtl_internal_function globals.
+    match fresh_regs_strong rtl_params0 globals def (|destrs|) with
+    [ dp def_tmp_destrs tmp_destrs_prf ⇒
+      let def ≝ \fst def_tmp_destrs in
+      let tmp_destrs ≝ \snd def_tmp_destrs in
+      let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
+      let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
+      let insts_init ≝ [
+        translate_move globals fresh_srcrs1 srcrs1;
+        translate_move globals fresh_srcrs2 srcrs2;
+        translate_cst globals (Ointconst I8 (zero …)) destrs
+      ]
+      in
+        let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
+        let f' ≝ λi. λproof: i ≤ |srcrs2|. f i ? in
+        let insts_mul ≝ foldi_strong ? ? srcrs2 f' [ ] in
+          add_translates rtl_params1 globals (insts_init @ insts_mul) start_lbl dest_lbl def
+    ].
+  >tmp_destrs_prf
+  <regs_proof
+  assumption
+qed.
 
 definition translate_divumodu8 ≝
@@ -853 +859 @@
                                      but we need more dep. typ. in modu/divu
                                      cases *)
-  λsrcrs2_prf: 0 < |srcrs2|.
+  λsrcrs2_prf: |srcrs2| = |destrs|.
   λstart_lbl: label.
   λdest_lbl: label.
@@ -869 +875 @@
     translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
   | Omul ⇒
-    translate_mul globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
+    translate_mul globals destrs srcrs1 srcrs2 ? start_lbl dest_lbl def
   | Odivu ⇒
     match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
@@ -959 +965 @@
   | _ ⇒ ? (* assert false, implemented in run time or float op *)
   ].
-  [ 2,6: normalize in nil_absrd;
+  [ 3,7: normalize in nil_absrd;
          cases(not_le_Sn_O 0)
          #HYP cases(HYP nil_absrd)
-  | 3,7,12,17,13,15,18,19,20,21,14,16:
+  | 4,8,19,20,21,22,17,18,24:
+         >srcrs2_prf
+         assumption
+  | 1,23:
          assumption
   | *:   cases not_implemented (* yes, really *)