X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fword16.ma;h=f379eb1bf5f7a67c0d6ca0e969ed1bd9e308e8d1;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=80281eeea6d64064dbfa4b208a4834adbd32b3c2;hpb=ced2abc1e3fe84d5bbfa9ccb2ebf46f253279ebe;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma
index 80281eeea..f379eb1bf 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma
@@ -141,6 +141,11 @@ ndefinition compl_w16 ≝
  [ true ⇒ succ_w16 (not_w16 w)
  | false ⇒ not_w16 (pred_w16 w) ].
 
+(* operatore abs *)
+ndefinition abs_w16 ≝
+λw:word16.match getMSB_w16 w with
+ [ true ⇒ compl_w16 w | false ⇒ w ].
+
 (* operatore x in [inf,sup] o in sup],[inf *)
 ndefinition inrange_w16 ≝
 λx,inf,sup:word16.
@@ -148,6 +153,54 @@ ndefinition inrange_w16 ≝
   [ true ⇒ and_bool | false ⇒ or_bool ]
  (le_w16 inf x) (le_w16 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_b8_aux ≝
+λw.nat_it ? rol_w16 w nat4.
+
+ndefinition mulu_b8 ≝
+λb1,b2:byte8.
+ plus_w16_d_d 〈(mulu_ex (cnH ? b1) (cnH ? b2)):〈x0,x0〉〉
+ (plus_w16_d_d (mulu_b8_aux (extu_w16 (mulu_ex (cnH ? b1) (cnL ? b2))))
+  (plus_w16_d_d (mulu_b8_aux (extu_w16 (mulu_ex (cnL ? b1) (cnH ? b2))))
+                (extu_w16 (mulu_ex (cnL ? b1) (cnL ? b2))))).
+
+(* operatore moltiplicazione con segno *)
+(* x * y = sgn(x) * sgn(y) * |x| * |y| *)
+ndefinition muls_b8 ≝
+λb1,b2:byte8.
+(* ++/-- → +, +-/-+ → - *)
+ match (getMSB_b8 b1) ⊙ (getMSB_b8 b2) with
+  (* +- -+ → - *)
+  [ true ⇒ compl_w16
+  (* ++/-- → + *)
+  | false ⇒ λx.x ] (mulu_b8 (abs_b8 b1) (abs_b8 b2)).
+
+(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
+nlet rec div_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (n:nat) on n ≝
+ let w' ≝ plus_w16_d_d divd (compl_w16 divs) in
+  match n with
+  [ O ⇒ match le_w16 divs divd with
+   [ true ⇒ triple … (or_b8 molt q) (cnL ? w') (⊖ (eq_b8 (cnH ? w') 〈x0,x0〉))
+   | false ⇒ triple … q (cnL ? divd) (⊖ (eq_b8 (cnH ? divd) 〈x0,x0〉)) ]
+  | S n' ⇒ match le_w16 divs divd with
+   [ true ⇒ div_b8_aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) n'
+   | false ⇒ div_b8_aux divd (ror_w16 divs) (ror_b8 molt) q n' ]].
+
+ndefinition div_b8 ≝
+λw:word16.λb:byte8.match eq_b8 b 〈x0,x0〉 with
+(* la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato *)
+ [ true ⇒ triple … 〈xF,xF〉 (cnL ? w) true
+ | false ⇒ match eq_w16 w 〈〈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〉 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_b8_aux w (nat_it ? rol_w16 (extu_w16 b) nat7) 〈x8,x0〉 〈x0,x0〉 nat7 ]].
+
 (* word16 ricorsive *)
 ninductive rec_word16 : word16 → Type ≝
   w16_O : rec_word16 〈〈x0,x0〉:〈x0,x0〉〉