X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fword32.ma;h=a5a74faa8803279db711d45b9f6b34763a3c9644;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=e9b99efc39bf1a73b4f5df9ffd04e9ad42754084;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma
index e9b99efc3..a5a74faa8 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Sviluppo: 2008-2010                                                  *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -26,158 +26,220 @@ include "num/word16.ma".
 (* DWORD *)
 (* ***** *)
 
-ndefinition word32 ≝ comp_num word16.
-ndefinition mk_word32 ≝ λw1,w2.mk_comp_num word16 w1 w2.
-ndefinition ext_word32 ≝ λw2.mk_comp_num word16 〈〈x0,x0〉:〈x0,x0〉〉 w2.
+nrecord word32 : Type ≝
+ {
+ w32h: word16;
+ w32l: word16
+ }.
 
 (* \langle \rangle *)
 notation "〈x.y〉" non associative with precedence 80
- for @{ mk_comp_num word16 $x $y }.
-
-(* iteratore sulle dword *)
-ndefinition forall_w32 ≝ forall_cn ? forall_w16.
+ for @{ 'mk_word32 $x $y }.
+interpretation "mk_word32" 'mk_word32 x y = (mk_word32 x y).
 
 (* operatore = *)
-ndefinition eq_w32 ≝ eq2_cn ? eq_w16.
+ndefinition eq_w32 ≝ λdw1,dw2.(eq_w16 (w32h dw1) (w32h dw2)) ⊗ (eq_w16 (w32l dw1) (w32l dw2)).
 
 (* operatore < *)
-ndefinition lt_w32 ≝ ltgt_cn ? eq_w16 lt_w16.
+ndefinition lt_w32 ≝
+λ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 ≝ lege_cn ? eq_w16 lt_w16 le_w16.
+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 ≝ ltgt_cn ? eq_w16 gt_w16.
+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 ≝ lege_cn ? eq_w16 gt_w16 ge_w16.
+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 ≝ fop2_cn ? and_w16.
+ndefinition and_w32 ≝
+λdw1,dw2:word32.mk_word32 (and_w16 (w32h dw1) (w32h dw2)) (and_w16 (w32l dw1) (w32l dw2)).
 
 (* operatore or *)
-ndefinition or_w32 ≝ fop2_cn ? or_w16.
+ndefinition or_w32 ≝
+λdw1,dw2:word32.mk_word32 (or_w16 (w32h dw1) (w32h dw2)) (or_w16 (w32l dw1) (w32l dw2)).
 
 (* operatore xor *)
-ndefinition xor_w32 ≝ fop2_cn ? xor_w16.
-
-(* operatore Most Significant Bit *)
-ndefinition getMSB_w32 ≝ getOPH_cn ? getMSB_w16.
-ndefinition setMSB_w32 ≝ setOPH_cn ? setMSB_w16.
-ndefinition clrMSB_w32 ≝ setOPH_cn ? clrMSB_w16.
-
-(* operatore Least Significant Bit *)
-ndefinition getLSB_w32 ≝ getOPL_cn ? getLSB_w16.
-ndefinition setLSB_w32 ≝ setOPL_cn ? setLSB_w16.
-ndefinition clrLSB_w32 ≝ setOPL_cn ? clrLSB_w16.
-
-(* operatore estensione unsigned *)
-ndefinition extu_w32 ≝ λw2.〈〈〈x0,x0〉:〈x0,x0〉〉.w2〉.
-ndefinition extu2_w32 ≝ λb2.〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:b2〉〉.
-ndefinition extu3_w32 ≝ λe2.〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,e2〉〉〉.
-
-(* operatore estensione signed *)
-ndefinition exts_w32 ≝
-λw2.〈(match getMSB_w16 w2 with
-      [ true ⇒ 〈〈xF,xF〉:〈xF,xF〉〉 | false ⇒ 〈〈x0,x0〉:〈x0,x0〉〉 ]).w2〉.
-ndefinition exts2_w32 ≝
-λb2.(match getMSB_b8 b2 with
-      [ true ⇒ 〈〈〈xF,xF〉:〈xF,xF〉〉.〈〈xF,xF〉:b2〉〉 | false ⇒ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:b2〉〉 ]).
-ndefinition exts3_w32 ≝
-λe2.(match getMSB_ex e2 with
-      [ true ⇒ 〈〈〈xF,xF〉:〈xF,xF〉〉.〈〈xF,xF〉:〈xF,e2〉〉〉 | false ⇒ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,e2〉〉〉 ]).
+ndefinition xor_w32 ≝
+λdw1,dw2:word32.mk_word32 (xor_w16 (w32h dw1) (w32h dw2)) (xor_w16 (w32l dw1) (w32l dw2)).
 
 (* operatore rotazione destra con carry *)
-ndefinition rcr_w32 ≝ opcr_cn ? rcr_w16.
+ndefinition rcr_w32 ≝
+λdw:word32.λc:bool.match rcr_w16 (w32h dw) c with
+ [ pair wh' c' ⇒ match rcr_w16 (w32l dw) c' with
+  [ pair wl' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]]. 
 
 (* operatore shift destro *)
-ndefinition shr_w32 ≝ opcr_cn ? rcr_w16 false.
+ndefinition shr_w32 ≝
+λdw:word32.match rcr_w16 (w32h dw) false with
+ [ pair wh' c' ⇒ match rcr_w16 (w32l dw) c' with
+  [ pair wl' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]].
 
 (* operatore rotazione destra *)
 ndefinition ror_w32 ≝
-λw.match shr_w32 w with
- [ pair c w' ⇒ match c with
-  [ true ⇒ setMSB_w32 w' | false ⇒ w' ]].
+λdw:word32.match rcr_w16 (w32h dw) false with
+ [ pair wh' c' ⇒ match rcr_w16 (w32l dw) c' with
+  [ pair wl' c'' ⇒ match c'' with
+   [ true ⇒ mk_word32 (or_w16 (mk_word16 (mk_byte8 x8 x0) (mk_byte8 x0 x0)) wh') wl'
+   | false ⇒ mk_word32 wh' wl' ]]].
+
+(* operatore rotazione destra n-volte *)
+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 ≝ opcl_cn ? rcl_w16.
+ndefinition rcl_w32 ≝
+λdw:word32.λc:bool.match rcl_w16 (w32l dw) c with
+ [ pair wl' c' ⇒ match rcl_w16 (w32h dw) c' with
+  [ pair wh' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]]. 
 
 (* operatore shift sinistro *)
-ndefinition shl_w32 ≝ opcl_cn ? rcl_w16 false.
+ndefinition shl_w32 ≝
+λdw:word32.match rcl_w16 (w32l dw) false with
+ [ pair wl' c' ⇒ match rcl_w16 (w32h dw) c' with
+  [ pair wh' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]].
 
 (* operatore rotazione sinistra *)
 ndefinition rol_w32 ≝
-λw.match shl_w32 w with
- [ pair c w' ⇒ match c with
-  [ true ⇒ setLSB_w32 w' | false ⇒ w' ]].
+λdw:word32.match rcl_w16 (w32l dw) false with
+ [ pair wl' c' ⇒ match rcl_w16 (w32h dw) c' with
+  [ pair wh' c'' ⇒ match c'' with
+   [ true ⇒ mk_word32 wh' (or_w16 (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x1)) wl')
+   | false ⇒ mk_word32 wh' wl' ]]].
+
+(* operatore rotazione sinistra n-volte *)
+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 ≝ fop_cn ? not_w16.
+ndefinition not_w32 ≝
+λdw:word32.mk_word32 (not_w16 (w32h dw)) (not_w16 (w32l dw)).
 
 (* operatore somma con data+carry → data+carry *)
-ndefinition plus_w32_dc_dc ≝ opcl2_cn ? plus_w16_dc_dc.
+ndefinition plus_w32_dc_dc ≝
+λdw1,dw2:word32.λc:bool.
+ match plus_w16_dc_dc (w32l dw1) (w32l dw2) c with
+  [ pair l c ⇒ match plus_w16_dc_dc (w32h dw1) (w32h dw2) c with
+   [ pair h c' ⇒ pair … 〈h.l〉 c' ]].
 
 (* operatore somma con data+carry → data *)
-ndefinition plus_w32_dc_d ≝ λc,w1,w2.snd … (plus_w32_dc_dc c w1 w2).
+ndefinition plus_w32_dc_d ≝
+λdw1,dw2:word32.λc:bool.
+ match plus_w16_dc_dc (w32l dw1) (w32l dw2) c with
+  [ pair l c ⇒ 〈plus_w16_dc_d (w32h dw1) (w32h dw2) c.l〉 ].
 
 (* operatore somma con data+carry → c *)
-ndefinition plus_w32_dc_c ≝ λc,w1,w2.fst … (plus_w32_dc_dc c w1 w2).
+ndefinition plus_w32_dc_c ≝
+λdw1,dw2:word32.λc:bool.
+ plus_w16_dc_c (w32h dw1) (w32h dw2) (plus_w16_dc_c (w32l dw1) (w32l dw2) c).
 
 (* operatore somma con data → data+carry *)
-ndefinition plus_w32_d_dc ≝ opcl2_cn ? plus_w16_dc_dc false.
+ndefinition plus_w32_d_dc ≝
+λdw1,dw2:word32.
+ match plus_w16_d_dc (w32l dw1) (w32l dw2) with
+  [ pair l c ⇒ match plus_w16_dc_dc (w32h dw1) (w32h dw2) c with
+   [ pair h c' ⇒ pair … 〈h.l〉 c' ]].
 
 (* operatore somma con data → data *)
-ndefinition plus_w32_d_d ≝ λw1,w2.snd … (plus_w32_d_dc w1 w2).
+ndefinition plus_w32_d_d ≝
+λdw1,dw2:word32.
+ match plus_w16_d_dc (w32l dw1) (w32l dw2) with
+  [ pair l c ⇒ 〈plus_w16_dc_d (w32h dw1) (w32h dw2) c.l〉 ].
 
 (* operatore somma con data → c *)
-ndefinition plus_w32_d_c ≝ λw1,w2.fst … (plus_w32_d_dc w1 w2).
+ndefinition plus_w32_d_c ≝
+λdw1,dw2:word32.
+ plus_w16_dc_c (w32h dw1) (w32h dw2) (plus_w16_d_c (w32l dw1) (w32l dw2)).
+
+(* operatore Most Significant Bit *)
+ndefinition MSB_w32 ≝ λdw:word32.eq_ex x8 (and_ex x8 (b8h (w16h (w32h dw)))).
 
 (* operatore predecessore *)
-ndefinition pred_w32 ≝ predsucc_cn ? (eq_w16 〈〈x0,x0〉:〈x0,x0〉〉) pred_w16.
+ndefinition pred_w32 ≝
+λdw:word32.match eq_w16 (w32l dw) (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) with
+ [ true ⇒ mk_word32 (pred_w16 (w32h dw)) (pred_w16 (w32l dw))
+ | false ⇒ mk_word32 (w32h dw) (pred_w16 (w32l dw)) ].
 
 (* operatore successore *)
-ndefinition succ_w32 ≝ predsucc_cn ? (eq_w16 〈〈xF,xF〉:〈xF,xF〉〉) succ_w16.
+ndefinition succ_w32 ≝
+λdw:word32.match eq_w16 (w32l dw) (mk_word16 (mk_byte8 xF xF) (mk_byte8 xF xF)) with
+ [ true ⇒ mk_word32 (succ_w16 (w32h dw)) (succ_w16 (w32l dw))
+ | false ⇒ mk_word32 (w32h dw) (succ_w16 (w32l dw)) ].
 
 (* operatore neg/complemento a 2 *)
 ndefinition compl_w32 ≝
-λw:word32.match getMSB_w32 w with
- [ true ⇒ succ_w32 (not_w32 w)
- | false ⇒ not_w32 (pred_w32 w) ].
-
-(* operatore abs *)
-ndefinition abs_w32 ≝
-λw:word32.match getMSB_w32 w with
- [ true ⇒ compl_w32 w | false ⇒ w ].
-
-(* operatore x in [inf,sup] o in sup],[inf *)
+λdw:word32.match MSB_w32 dw with
+ [ true ⇒ succ_w32 (not_w32 dw)
+ | false ⇒ not_w32 (pred_w32 dw) ].
+
+(* 
+   operatore moltiplicazione senza segno: b*b=[0x00000000,0xFFFE0001]
+   ... in pratica (〈a:b〉*〈c:d〉) = (a*c)<<16+(a*d)<<8+(b*c)<<8+(b*d)
+*)
+ndefinition mul_w16 ≝
+λw1,w2:word16.match w1 with
+[ mk_word16 b1h b1l ⇒ match w2 with
+[ mk_word16 b2h b2l ⇒ match mul_b8 b1l b2l with
+[ mk_word16 t1_h t1_l ⇒ match mul_b8 b1h b2l with
+[ mk_word16 t2_h t2_l ⇒ match mul_b8 b2h b1l with
+[ mk_word16 t3_h t3_l ⇒ match mul_b8 b1h b2h with
+[ mk_word16 t4_h t4_l ⇒
+ plus_w32_d_d
+  (plus_w32_d_d
+   (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈t1_h:t1_l〉〉
+]]]]]].
+
+(* 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:nat) on c ≝
+  let w' ≝ plus_w32_d_d divd (compl_w32 divs) in
+   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〉〉)) ]
+   | 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
+(* 
+   la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
+*)
+ [ true ⇒ triple … 〈〈xF,xF〉:〈xF,xF〉〉 (w32l w) true
+ | false ⇒ match eq_w32 w 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉 with
+(* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *)
+  [ true ⇒ triple … 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 false
+(* 1) e' una divisione sensata che produrra' overflow/risultato *)
+(* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *)
+(* 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〉 nat15) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 nat15 ]].
+
+(* operatore x in [inf,sup] *)
 ndefinition inrange_w32 ≝
-λx,inf,sup:word32.
- match le_w32 inf sup with
-  [ true ⇒ and_bool | false ⇒ or_bool ]
- (le_w32 inf x) (le_w32 x sup).
-
-(* operatore moltiplicazione senza segno *)
-(* 〈a1,a2〉 * 〈b1,b2〉 = (a1*b1) x0 x0 + x0 (a1*b2) x0 + x0 (a2*b1) x0 + x0 x0 (a2*b2) *)
-ndefinition mulu_w16_aux ≝
-λw.nat_it ? rol_w32 w nat8.
-
-ndefinition mulu_w16 ≝
-λw1,w2:word16.
- plus_w32_d_d 〈(mulu_b8 (cnH ? w1) (cnH ? w2)).〈〈x0,x0〉:〈x0,x0〉〉〉
- (plus_w32_d_d (mulu_w16_aux (extu_w32 (mulu_b8 (cnH ? w1) (cnL ? w2))))
-  (plus_w32_d_d (mulu_w16_aux (extu_w32 (mulu_b8 (cnL ? w1) (cnH ? w2))))
-                (extu_w32 (mulu_b8 (cnL ? w1) (cnL ? w2))))).
-
-(* operatore moltiplicazione con segno *)
-(* x * y = sgn(x) * sgn(y) * |x| * |y| *)
-ndefinition muls_w16 ≝
-λw1,w2:word16.
-(* ++/-- → +, +-/-+ → - *)
- match (getMSB_w16 w1) ⊙ (getMSB_w16 w2) with
-  (* +- -+ → - *)
-  [ true ⇒ compl_w32
-  (* ++/-- → + *)
-  | false ⇒ λx.x ] (mulu_w16 (abs_w16 w1) (abs_w16 w2)).
-
-nlemma pippo : ∃b.b=(muls_w16 〈〈xC,x3〉:〈x0,x4〉〉 〈〈x7,xE〉:〈xF,x9〉〉). nnormalize;
-
+λx,inf,sup:word32.(le_w32 inf x) ⊗ (le_w32 x sup).
+
+(* iteratore sulle word *)
+ndefinition forall_w32 ≝
+ λP.
+  forall_w16 (λbh.
+  forall_w16 (λbl.
+   P (mk_word32 bh bl ))).