freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / num / word32.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma
index 091d0f73ca31fbfb2074da2fa65d8e413eb67f56..a5a74faa8803279db711d45b9f6b34763a3c9644 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -42,20 +42,27 @@ ndefinition eq_w32 ≝ λdw1,dw2.(eq_w16 (w32h dw1) (w32h dw2)) ⊗ (eq_w16 (w32
 
 (* operatore < *)
 ndefinition lt_w32 ≝
-λdw1,dw2:word32.match lt_w16 (w32h dw1) (w32h dw2) with
- [ true ⇒ true
- | false ⇒ match gt_w16 (w32h dw1) (w32h dw2) with
-  [ true ⇒ false
-  | false ⇒ lt_w16 (w32l dw1) (w32l dw2) ]].
+λdw1,dw2:word32.
+ (lt_w16 (w32h dw1) (w32h dw2)) ⊕
+ ((eq_w16 (w32h dw1) (w32h dw2)) ⊗ (lt_w16 (w32l dw1) (w32l dw2))).
 
 (* operatore ≤ *)
-ndefinition le_w32 ≝ λdw1,dw2:word32.(eq_w32 dw1 dw2) ⊕ (lt_w32 dw1 dw2).
+ndefinition le_w32 ≝
+λdw1,dw2:word32.
+ (lt_w16 (w32h dw1) (w32h dw2)) ⊕
+ ((eq_w16 (w32h dw1) (w32h dw2)) ⊗ (le_w16 (w32l dw1) (w32l dw2))).
 
 (* operatore > *)
-ndefinition gt_w32 ≝ λdw1,dw2:word32.⊖ (le_w32 dw1 dw2).
+ndefinition gt_w32 ≝
+λdw1,dw2:word32.
+ (gt_w16 (w32h dw1) (w32h dw2)) ⊕
+ ((eq_w16 (w32h dw1) (w32h dw2)) ⊗ (gt_w16 (w32l dw1) (w32l dw2))).
 
 (* operatore ≥ *)
-ndefinition ge_w32 ≝ λdw1,dw2:word32.⊖ (lt_w32 dw1 dw2).
+ndefinition ge_w32 ≝
+λdw1,dw2:word32.
+ (gt_w16 (w32h dw1) (w32h dw2)) ⊕
+ ((eq_w16 (w32h dw1) (w32h dw2)) ⊗ (ge_w16 (w32l dw1) (w32l dw2))).
 
 (* operatore and *)
 ndefinition and_w32 ≝
@@ -90,10 +97,10 @@ ndefinition ror_w32 ≝
    | false ⇒ mk_word32 wh' wl' ]]].
 
 (* operatore rotazione destra n-volte *)
-nlet rec ror_w32_n (dw:word32) (n:bitrigesim) (r:rec_bitrigesim n) on r ≝
- match r with
-  [ bi_O ⇒ dw
-  | bi_S t n' ⇒ ror_w32_n (ror_w32 dw) t n' ].
+nlet rec ror_w32_n (dw:word32) (n:nat) on n ≝
+ match n with
+  [ O ⇒ dw
+  | S n' ⇒ ror_w32_n (ror_w32 dw) n' ].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_w32 ≝
@@ -116,10 +123,10 @@ ndefinition rol_w32 ≝
    | false ⇒ mk_word32 wh' wl' ]]].
 
 (* operatore rotazione sinistra n-volte *)
-nlet rec rol_w32_n (dw:word32) (n:bitrigesim) (r:rec_bitrigesim n) on r ≝
- match r with
-  [ bi_O ⇒ dw
-  | bi_S t n' ⇒ rol_w32_n (rol_w32 dw) t n' ].
+nlet rec rol_w32_n (dw:word32) (n:nat) on n ≝
+ match n with
+  [ O ⇒ dw
+  | S n' ⇒ rol_w32_n (rol_w32 dw) n' ].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_w32 ≝
@@ -200,15 +207,15 @@ ndefinition mul_w16 ≝
 ]]]]]].
 
 (* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
-nlet rec div_w16_aux (divd:word32) (divs:word32) (molt:word16) (q:word16) (c:exadecim) (rc:rec_exadecim c) on rc ≝
+nlet rec div_w16_aux (divd:word32) (divs:word32) (molt:word16) (q:word16) (c:nat) on c ≝
   let w' ≝ plus_w32_d_d divd (compl_w32 divs) in
-   match rc with
-   [ ex_O ⇒ match le_w32 divs divd with
+   match c with
+   [ O ⇒ match le_w32 divs divd with
     [ true ⇒ triple … (or_w16 molt q) (w32l w') (⊖ (eq_w16 (w32h w') 〈〈x0,x0〉:〈x0,x0〉〉))
     | false ⇒ triple … q (w32l divd) (⊖ (eq_w16 (w32h divd) 〈〈x0,x0〉:〈x0,x0〉〉)) ]
-   | ex_S t c' ⇒ match le_w32 divs divd with
-    [ true ⇒ div_w16_aux w' (ror_w32 divs) (ror_w16 molt) (or_w16 molt q) t c'
-    | false ⇒ div_w16_aux divd (ror_w32 divs) (ror_w16 molt) q t c' ]].
+   | S c' ⇒ match le_w32 divs divd with
+    [ true ⇒ div_w16_aux w' (ror_w32 divs) (ror_w16 molt) (or_w16 molt q) c'
+    | false ⇒ div_w16_aux divd (ror_w32 divs) (ror_w16 molt) q c' ]].
 
 ndefinition div_w16 ≝
 λw:word32.λb:word16.match eq_w16 b 〈〈x0,x0〉:〈x0,x0〉〉 with
@@ -224,11 +231,11 @@ ndefinition div_w16 ≝
 (* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
 (* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
 (*    puo' essere sottratto al dividendo *) 
-  | false ⇒ div_w16_aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 ? (bit_to_recbit t0F)) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 ? (ex_to_recex xF) ]].
+  | false ⇒ div_w16_aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 nat15) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 nat15 ]].
 
 (* operatore x in [inf,sup] *)
 ndefinition inrange_w32 ≝
-λx,inf,sup:word32.(le_w32 inf sup) ⊗ (ge_w32 x inf) ⊗ (le_w32 x sup).
+λx,inf,sup:word32.(le_w32 inf x) ⊗ (le_w32 x sup).
 
 (* iteratore sulle word *)
 ndefinition forall_w32 ≝