X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fbyte8.ma;h=61da004eef2fccb354220d88a491b10ef2d0fa74;hb=b886a562ccbfc3f63b8f64a135bcf70e4b189999;hp=698736af6b0fbd4a4445078df8d7f6a8664ace02;hpb=a62de71cf6821c955bd41fa691c52ea62173f25d;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
index 698736af6..61da004ee 100755
--- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -43,20 +43,27 @@ ndefinition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1
 
 (* operatore < *)
 ndefinition lt_b8 ≝
-λb1,b2:byte8.match lt_ex (b8h b1) (b8h b2) with
- [ true ⇒ true
- | false ⇒ match gt_ex (b8h b1) (b8h b2) with
-  [ true ⇒ false
-  | false ⇒ lt_ex (b8l b1) (b8l b2) ]].
+λb1,b2:byte8.
+ (lt_ex (b8h b1) (b8h b2)) ⊕
+ ((eq_ex (b8h b1) (b8h b2)) ⊗ (lt_ex (b8l b1) (b8l b2))).
 
 (* operatore ≤ *)
-ndefinition le_b8 ≝ λb1,b2:byte8.(eq_b8 b1 b2) ⊕ (lt_b8 b1 b2). 
+ndefinition le_b8 ≝
+λb1,b2:byte8.
+ (lt_ex (b8h b1) (b8h b2)) ⊕
+ ((eq_ex (b8h b1) (b8h b2)) ⊗ (le_ex (b8l b1) (b8l b2))).
 
 (* operatore > *)
-ndefinition gt_b8 ≝ λb1,b2:byte8.⊖ (le_b8 b1 b2).
+ndefinition gt_b8 ≝
+λb1,b2:byte8.
+ (gt_ex (b8h b1) (b8h b2)) ⊕
+ ((eq_ex (b8h b1) (b8h b2)) ⊗ (gt_ex (b8l b1) (b8l b2))).
 
 (* operatore ≥ *)
-ndefinition ge_b8 ≝ λb1,b2:byte8.⊖ (lt_b8 b1 b2).
+ndefinition ge_b8 ≝
+λb1,b2:byte8.
+ (gt_ex (b8h b1) (b8h b2)) ⊕
+ ((eq_ex (b8h b1) (b8h b2)) ⊗ (ge_ex (b8l b1) (b8l b2))).
 
 (* operatore and *)
 ndefinition and_b8 ≝
@@ -78,23 +85,23 @@ ndefinition rcr_b8 ≝
 
 (* operatore shift destro *)
 ndefinition shr_b8 ≝
-λb:byte8.match rcr_ex (b8h b) false with
+λb:byte8.match shr_ex (b8h b) with
  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
   [ pair bl' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
 
 (* operatore rotazione destra *)
 ndefinition ror_b8 ≝
-λb:byte8.match rcr_ex (b8h b) false with
+λb:byte8.match shr_ex (b8h b) with
  [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
   [ pair bl' c'' ⇒ match c'' with
    [ true ⇒ mk_byte8 (or_ex x8 bh') bl'
    | false ⇒ mk_byte8 bh' bl' ]]].
 
 (* operatore rotazione destra n-volte *)
-nlet rec ror_b8_n (b:byte8) (n:nat) on n ≝
- match n with
-  [ O ⇒ b
-  | S n' ⇒ ror_b8_n (ror_b8 b) n' ].
+nlet rec ror_b8_n (b:byte8) (o:oct) (ro:rec_oct o) on ro ≝
+ match ro with
+  [ oc_O ⇒ b
+  | oc_S o' n' ⇒ ror_b8_n (ror_b8 b) o' n' ].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_b8 ≝
@@ -104,23 +111,23 @@ ndefinition rcl_b8 ≝
 
 (* operatore shift sinistro *)
 ndefinition shl_b8 ≝
-λb:byte8.match rcl_ex (b8l b) false with
+λb:byte8.match shl_ex (b8l b) with
  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
   [ pair bh' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
 
 (* operatore rotazione sinistra *)
 ndefinition rol_b8 ≝
-λb:byte8.match rcl_ex (b8l b) false with
+λb:byte8.match shl_ex (b8l b) with
  [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
   [ pair bh' c'' ⇒ match c'' with
    [ true ⇒ mk_byte8 bh' (or_ex x1 bl')
    | false ⇒ mk_byte8 bh' bl' ]]].
 
 (* operatore rotazione sinistra n-volte *)
-nlet rec rol_b8_n (b:byte8) (n:nat) on n ≝
- match n with
-  [ O ⇒ b
-  | S n' ⇒ rol_b8_n (rol_b8 b) n' ].
+nlet rec rol_b8_n (b:byte8) (o:oct) (ro:rec_oct o) on ro ≝
+ match ro with
+  [ oc_O ⇒ b
+  | oc_S o' n' ⇒ rol_b8_n (rol_b8 b) o' n' ].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_b8 ≝
@@ -130,14 +137,14 @@ ndefinition not_b8 ≝
 ndefinition plus_b8_dc_dc ≝
 λb1,b2:byte8.λc:bool.
  match plus_ex_dc_dc (b8l b1) (b8l b2) c with
-  [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
-   [ pair h c' ⇒ pair … 〈h,l〉 c' ]].
+  [ pair l c' ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c' with
+   [ pair h c'' ⇒ pair … 〈h,l〉 c'' ]].
 
 (* operatore somma con data+carry → data *)
 ndefinition plus_b8_dc_d ≝
 λb1,b2:byte8.λc:bool.
  match plus_ex_dc_dc (b8l b1) (b8l b2) c with
-  [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
+  [ pair l c' ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c',l〉 ].
 
 (* operatore somma con data+carry → c *)
 ndefinition plus_b8_dc_c ≝
@@ -299,6 +306,40 @@ ndefinition daa_b8 ≝
    pair … X'' true
   ].
 
+(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
+nlet rec div_b8_ex_aux (divd:byte8) (divs:byte8) (molt:exadecim) (q:exadecim) (qu:quatern) (rqu:rec_quatern qu) on rqu ≝
+ let w' ≝ plus_b8_d_d divd (compl_b8 divs) in
+  match rqu with
+  [ qu_O ⇒ match le_b8 divs divd with
+   [ true ⇒ triple … (or_ex molt q) (b8l w') (⊖ (eq_ex (b8h w') x0))
+   | false ⇒ triple … q (b8l divd) (⊖ (eq_ex (b8h divd) x0)) ]
+  | qu_S qu' rqu' ⇒ match le_b8 divs divd with
+   [ true ⇒ div_b8_ex_aux w' (ror_b8 divs) (ror_ex molt) (or_ex molt q) qu' rqu'
+   | false ⇒ div_b8_ex_aux divd (ror_b8 divs) (ror_ex molt) q qu' rqu' ]].
+
+ndefinition div_b8_ex ≝
+λb:byte8.λe:exadecim.match eq_ex e x0 with
+(* 
+   la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
+*)
+ [ true ⇒ triple … xF (b8l b) true
+ | false ⇒ match eq_b8 b 〈x0,x0〉 with
+(* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *)
+  [ true ⇒ triple … 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_ex_aux b (rol_b8_n 〈x0,e〉 ? (oct_to_recoct o3)) x8 x0 ? (qu_to_recqu q3) ]].
+
+(* operatore x in [inf,sup] o in sup],[inf *)
+ndefinition inrange_b8 ≝
+λx,inf,sup:byte8.
+ match le_b8 inf sup with
+  [ true ⇒ and_bool | false ⇒ or_bool ]
+ (le_b8 inf x) (le_b8 x sup).
+
 (* iteratore sui byte *)
 ndefinition forall_b8 ≝
  λP.