mod change (-x)

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma
old mode 100755 (executable)
new mode 100644 (file)
index a6c12ec..f379eb1
--- a/helm/software/matita/contribs/ng_assembly/num/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma
@@ -65,10 +65,12 @@ ndefinition xor_w16 ≝ fop2_cn ? xor_b8.
 (* operatore Most Significant Bit *)
 ndefinition getMSB_w16 ≝ getOPH_cn ? getMSB_b8.
 ndefinition setMSB_w16 ≝ setOPH_cn ? setMSB_b8.
+ndefinition clrMSB_w16 ≝ setOPH_cn ? clrMSB_b8.
 
 (* operatore Least Significant Bit *)
 ndefinition getLSB_w16 ≝ getOPL_cn ? getLSB_b8.
 ndefinition setLSB_w16 ≝ setOPL_cn ? setLSB_b8.
+ndefinition clrLSB_w16 ≝ setOPL_cn ? clrLSB_b8.
 
 (* operatore estensione unsigned *)
 ndefinition extu_w16 ≝ λb2.〈〈x0,x0〉:b2〉.
@@ -139,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.
@@ -146,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〉〉