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=e7264f953fcf2cd2bef9057d83add08996d2ce75;hp=4c6d8101b2fbc978375fcaff46f4ff314a96549e;hpb=6ee4fa0ba5f4b6601b62afd482d4f30bd2de2f91;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 4c6d8101b..e9b99efc3 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma
@@ -28,6 +28,7 @@ include "num/word16.ma".
 
 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.
 
 (* \langle \rangle *)
 notation "〈x.y〉" non associative with precedence 80
@@ -63,10 +64,28 @@ 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〉〉〉 ]).
 
 (* operatore rotazione destra con carry *)
 ndefinition rcr_w32 ≝ opcr_cn ? rcr_w16.
@@ -125,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;
+