Changeset 1636 for src/RTLabs/RTLabsToRTL_paolo.ma

Timestamp:

Jan 9, 2012, 12:38:32 PM (9 years ago)

Author:

tranquil

Message:

• added coercions to arguments (in RTL) and notation for ops (for the momenti in RTLabsToRTL)
• changed slightly notations for bindLists

File:

• src/RTLabs/RTLabsToRTL_paolo.ma (modified) (17 diffs)

src/RTLabs/RTLabsToRTL_paolo.ma

@@ -8 +8 @@
 include alias "ASM/BitVector.ma".
 include alias "arithmetics/nat.ma".
+
+
+(* Paolo: to be moved elsewhere *)
+
+notation "r ← a1 .op. a2" with precedence 50 for
+  @{'op2 $op $r $a1 $a2}.
+notation "r ← . op . a" with precedence 50 for
+  @{'op1 $op $r $a}.
+notation "r ← a" with precedence 50 for
+  @{'mov $r $a}.
+notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for
+  @{'opaccs $op $r $s $a1 $a2}.
+
+interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
+interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
+interpretation "move" 'mov r a = (MOVE ? ? (REG r a)).
+interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
+
 
 definition size_of_sig_type ≝
@@ -138 +156 @@
   λsrcrs2.
   λprf1,prf2.
-  let f_add ≝ λop,destr,srcr1,srcr2.
-    OP2 rtl_params globals op destr srcr1 srcr2 in
+  let f_add ≝ OP2 rtl_params globals in
   let res : list (rtl_instruction globals) ≝
     map3 ???? (f_add op) destrs srcrs1 srcrs2 ?? in
@@ -166 +183 @@
     ] (refl …)
   | _ ⇒ res
-  ]. 
+  ].
   [5,6: assumption
   |1: >prf1 in eq_destrs; >eq_srcrs1 normalize //
@@ -238 +255 @@
   |destrs| = |srcrs| → list (rtl_instruction globals) ≝ 
   λglobals,destrs,srcrs,length_eq.
-  map2 … (λdst,src.MOVE rtl_params … (REG dst src)) destrs srcrs length_eq.
+  map2 … (λdst,src.dst ← src) destrs srcrs length_eq.
 
 let rec make
@@ -269 +286 @@
      *)
   λglobals,destr,srcr.
-  [OP2 … Or destr (Reg srcr) (imm_nat 127) ;
-   OP1 … Rl destr destr ;
-   OP1 … Inc destr destr ;
-   OP1 … Cmpl destr destr ].
+  [destr ← srcr .Or. 127 ;
+   destr ← .Rl. destr ;
+   destr ← .Inc. destr ;
+   destr ← .Cmpl. destr ].
    
 definition translate_cast_signed :
@@ -354 +371 @@
     translate_cast_unsigned ? destrs' @ (* fill destrs' with 0 *)
     match srcrs with
-    [ nil ⇒ [reg_from_nat … destr 0]
+    [ nil ⇒ [destr ← 0]
     | cons srcr srcrs' ⇒
       let f : register → rtl_instruction globals ≝
@@ -364 +381 @@
       (* many uses of 0, better not use immediates *)
       ν tmp in
-      [reg_from_nat … tmp 0 ;
-       OP2 … Sub destr (Reg tmp) (Reg tmp) ;
+      [tmp ← 0 ;
+       destr ← tmp .Sub. tmp ;
        (* now carry bit is set iff destr was non-null *)
-       OP2 … Addc destr (Reg tmp) (Reg tmp)]
+       destr ← tmp .Addc. tmp]
      ]
    ].
@@ -461 +478 @@
       let tmp_destrs_view : list register ≝
         ltl ? tmp_destrs_dummy k in
-      OPACCS rtl_params globals Mul a b
-        (nth_safe ? i srcrs1 ?)
-        (nth_safe ? (k - i) srcrs2 ?) ::
+      ❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?) ::
       translate_op … Add tmp_destrs_view (map … Reg tmp_destrs_view) args ?? @
       acc
@@ -501 +516 @@
 (* temporary registers for the result are created, so to avoid overwriting
    sources *)
-ννtmp_destrs: |destrs| with tmp_destrs_prf in
+νν tmp_destrs × |destrs| with tmp_destrs_prf in
 νdummy in
 (* the step calculating all products with least significant byte going in the
@@ -520 +535 @@
      for i in 0 ... k do
        translate_mul_i … k … i *)
-foldr … translate_mul_k [ ] (range_strong (|destrs|)) @
+foldr … translate_mul_k [ ] (range_strong (|destrs|)) @ 
 (* epilogue: saving the result *)
 translate_move … destrs (map … Reg tmp_destrs) ?.
@@ -552 +567 @@
           let 〈destr1, destr2〉 ≝
             if div_not_mod then 〈destr, dummy〉 else 〈dummy, destr〉 in
-          [OPACCS rtl_params globals DivuModu destr1 destr2 srcr1 srcr2]
+          [❮destr1, destr2❯ ← srcr1 .DivuModu. srcr2]
         ] (refl …)
       ] (refl …)
@@ -561 +576 @@
 destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct qed.
 
+(* Paolo: to be moved elsewhere *)
 let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (f : A→B→C→C) (init : C) (l1 : list A) (l2 : list B)
   (prf : |l1| = |l2|) on l1 : C ≝
@@ -572 +588 @@
     ] (refl …)
   ] (refl …).
-[destruct normalize in prf; destruct
-|destruct normalize in prf; //
-] qed.
-
-let rec foldr3 (A : Type[0]) (B : Type[0]) (C : Type[0]) (D : Type[0])
-  (f : A→B→C→D→D) (init : D) (l1 : list A) (l2 : list B) (l3 : list C)
-  (prf1 : |l1| = |l2|) (prf2 : |l2| = |l3|) on l1 : D ≝
-  match l1 return λx.x = l1 → D with 
-  [ nil ⇒ λ_.init
-  | cons a l1' ⇒ λeq_l1.
-    match l2 return λy.y = l2 → D with
-    [ nil ⇒ λeq_l2.⊥
-    | cons b l2' ⇒ λeq_l2.
-      match l3 return λz.z = l3 → D with
-      [ nil ⇒ λeq_l3.⊥
-      | cons c l3' ⇒ λeq_l3. 
-        f a b c (foldr3 A B C D f init l1' l2' l3' ? ?)
-      ] (refl …)
-    ] (refl …)
-  ] (refl …).
-destruct normalize in prf1; normalize in prf2; destruct // qed.
+destruct normalize in prf;  [destruct|//]
+qed.
 
 definition translate_ne: ∀globals: list ident.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
@@ -614 +611 @@
         let f : rtl_argument → rtl_argument → list (rtl_instruction globals) → list (rtl_instruction globals) ≝
           λs1,s2,acc.
-          OP2 … Xor tmpr s1 s2 ::
-          OP2 … Or destr (Reg destr) (Reg tmpr) ::
+          tmpr  ← s1 .Xor. s2 ::
+          destr ← destr .Or. tmpr ::
           acc in
         let epilogue : list (rtl_instruction globals) ≝
           [ clear_carry … ;
-            OP2 … Sub tmpr (Imm (zero …)) (Reg destr) ;
+            tmpr ← 0 .Sub. destr ;
             (* now carry bit is 1 iff destrs != 0 *)
-            OP2 … Addc destr (Imm (zero …)) (Imm (zero …)) ] in
+            destr ← 0 .Addc. 0 ] in
          translate_cast_unsigned … destrs' @
-         OP2 rtl_params globals Xor destr srcr1 srcr2 ::
+         destr ← srcr1 .Xor. srcr2 ::
          foldr2 ??? f epilogue srcrs1' srcrs2' ?
        ] (refl …)
@@ -637 +634 @@
   match destrs with
   [ nil ⇒ [ ]
-  | cons destr _ ⇒ [OP1 rtl_params globals Cmpl destr destr]
+  | cons destr _ ⇒ [destr ← .Cmpl. destr]
   ].
   
@@ -655 +652 @@
     (* I perform a subtraction, but the only interest is in the carry bit *)
     translate_op ? Sub (make … destr (|destrs|)) srcrs1 srcrs2 ?? @
-    [ OP2 … Addc destr (imm_nat 0) (imm_nat 0) ]
+    [ destr ← 0 .Addc. 0 ]
   ].
 [ <make_length ] assumption qed.
@@ -669 +666 @@
   | cons srcr srcrs' ⇒
     match srcrs' with
-    [ nil ⇒ 〈[ Reg tmp ], [ OP2 … Add tmp srcr (imm_nat 128) ]〉
+    [ nil ⇒ 〈[ Reg tmp ], [ tmp ← srcr .Add. 128 ]〉
     | _ ⇒
       let 〈new_srcrs', op〉 ≝ shift_signed globals tmp srcrs' in