X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fword32.ma;h=e9b99efc39bf1a73b4f5df9ffd04e9ad42754084;hb=433d9c9612c1557e03a549e004c796c1137d4b4a;hp=7be3a53c5fd90a6b58982bbe51e886dc7585f569;hpb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;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 7be3a53c5..e9b99efc3 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma
@@ -64,10 +64,12 @@ 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〉.
@@ -142,9 +144,40 @@ ndefinition compl_w32 ≝
  [ 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 *)
 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;
+