X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fword24.ma;h=4aabde7710cf2124ca4eb7be29a96344acff3a4c;hb=a4cd6a8a1d6a008518c12daca794b9e811c1dee5;hp=70e407c3708fec1d5594e21ec0f98fda21b0ef87;hpb=b886a562ccbfc3f63b8f64a135bcf70e4b189999;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/word24.ma b/helm/software/matita/contribs/ng_assembly/num/word24.ma
index 70e407c37..4aabde771 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word24.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word24.ma
@@ -38,6 +38,14 @@ notation "〈x;y;z〉" non associative with precedence 80
  for @{ 'mk_word24 $x $y $z }.
 interpretation "mk_word24" 'mk_word24 x y z = (mk_word24 x y z).
 
+(* iteratore sulle word *)
+ndefinition forall_w24 ≝
+ λP.
+  forall_b8 (λbx.
+  forall_b8 (λbh.
+  forall_b8 (λbl.
+   P (mk_word24 bx bh bl )))).
+
 (* operatore = *)
 ndefinition eq_w24 ≝
 λw1,w2.(eq_b8 (w24x w1) (w24x w2)) ⊗
@@ -93,63 +101,47 @@ ndefinition xor_w24 ≝
            (xor_b8 (w24h w1) (w24h w2))
            (xor_b8 (w24l w1) (w24l w2)).
 
+(* operatore Most Significant Bit *)
+ndefinition getMSB_w24 ≝ λw:word24.getMSB_b8 (w24x w).
+ndefinition setMSB_w24 ≝ λw:word24.mk_word24 (setMSB_b8 (w24x w)) (w24h w) (w24l w).
+ndefinition clrMSB_w24 ≝ λw:word24.mk_word24 (clrMSB_b8 (w24x w)) (w24h w) (w24l w).
+
+(* operatore Least Significant Bit *)
+ndefinition getLSB_w24 ≝ λw:word24.getLSB_b8 (w24l w).
+ndefinition setLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (setLSB_b8 (w24l w)).
+ndefinition clrLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (clrLSB_b8 (w24l w)).
+
 (* operatore rotazione destra con carry *)
 ndefinition rcr_w24 ≝
-λw:word24.λc:bool.match rcr_b8 (w24x w) c with
- [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
-  [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
-   [ pair wl' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]]. 
+λc:bool.λw:word24.match rcr_b8 c (w24x w) with
+ [ pair c' wx' ⇒ match rcr_b8 c' (w24h w) with
+  [ pair c'' wh' ⇒ match rcr_b8 c'' (w24l w) with
+   [ pair c''' wl' ⇒ pair … c''' (mk_word24 wx' wh' wl') ]]]. 
 
 (* operatore shift destro *)
-ndefinition shr_w24 ≝
-λw:word24.match shr_b8 (w24x w) with
- [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
-  [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
-   [ pair wl' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
+ndefinition shr_w24 ≝ rcr_w24 false.
 
 (* operatore rotazione destra *)
 ndefinition ror_w24 ≝
-λw:word24.match shr_b8 (w24x w) with
- [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
-  [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
-   [ pair wl' c''' ⇒ match c''' with
-    [ true ⇒ mk_word24 (or_b8 (mk_byte8 x8 x0) wx') wh' wl'
-    | false ⇒ mk_word24 wx' wh' wl' ]]]].
-
-(* operatore rotazione destra n-volte *)
-nlet rec ror_w24_n (w:word24) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
- match rt with
-  [ bi_O ⇒ w
-  | bi_S t' n' ⇒ ror_w24_n (ror_w24 w) t' n' ].
+λw.match shr_w24 w with
+ [ pair c w' ⇒ match c with
+  [ true ⇒ setMSB_w24 w' | false ⇒ w' ]].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_w24 ≝
-λw:word24.λc:bool.match rcl_b8 (w24l w) c with
- [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
-  [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
-   [ pair wx' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
+λc:bool.λw:word24.match rcl_b8 c (w24l w) with
+ [ pair c' wl' ⇒ match rcl_b8 c' (w24h w) with
+  [ pair c'' wh' ⇒ match rcl_b8 c'' (w24x w) with
+   [ pair c''' wx' ⇒ pair … c''' (mk_word24 wx' wh' wl') ]]].
 
 (* operatore shift sinistro *)
-ndefinition shl_w24 ≝
-λw:word24.match shl_b8 (w24l w) with
- [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
-  [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
-   [ pair wx' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
+ndefinition shl_w24 ≝ rcl_w24 false.
 
 (* operatore rotazione sinistra *)
 ndefinition rol_w24 ≝
-λw:word24.match shl_b8 (w24l w) with
- [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
-  [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
-   [ pair wx' c''' ⇒ match c''' with
-    [ true ⇒ mk_word24 wx' wh' (or_b8 (mk_byte8 x0 x1) wl')
-    | false ⇒ mk_word24 wx' wh' wl' ]]]].
-
-(* operatore rotazione sinistra n-volte *)
-nlet rec rol_w24_n (w:word24) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
- match rt with
-  [ bi_O ⇒ w
-  | bi_S t' n' ⇒ rol_w24_n (rol_w24 w) t' n' ].
+λw.match shl_w24 w with
+ [ pair c w' ⇒ match c with
+  [ true ⇒ setLSB_w24 w' | false ⇒ w' ]].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_w24 ≝
@@ -157,80 +149,57 @@ ndefinition not_w24 ≝
 
 (* operatore somma con data+carry → data+carry *)
 ndefinition plus_w24_dc_dc ≝
-λw1,w2:word24.λc:bool.
- match plus_b8_dc_dc (w24l w1) (w24l w2) c with
-  [ pair l c' ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c' with
-   [ pair h c'' ⇒ match plus_b8_dc_dc (w24x w1) (w24x w2) c'' with
-    [ pair x c''' ⇒ pair … 〈x;h;l〉 c''' ]]].
+λc:bool.λw1,w2:word24.
+ match plus_b8_dc_dc c (w24l w1) (w24l w2) with
+  [ pair c' l ⇒ match plus_b8_dc_dc c' (w24h w1) (w24h w2) with
+   [ pair c'' h ⇒ match plus_b8_dc_dc c'' (w24x w1) (w24x w2) with
+    [ pair c''' x ⇒ pair … c''' 〈x;h;l〉 ]]].
 
 (* operatore somma con data+carry → data *)
-ndefinition plus_w24_dc_d ≝
-λw1,w2:word24.λc:bool.
- match plus_b8_dc_dc (w24l w1) (w24l w2) c with
-  [ pair l c' ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c' with
-   [ pair h c'' ⇒ 〈plus_b8_dc_d (w24x w1) (w24x w2) c'';h;l〉 ]].
+ndefinition plus_w24_dc_d ≝ λc,w1,w2.snd … (plus_w24_dc_dc c w1 w2).
 
 (* operatore somma con data+carry → c *)
-ndefinition plus_w24_dc_c ≝
-λw1,w2:word24.λc:bool.
- plus_b8_dc_c (w24x w1) (w24x w2) (plus_b8_dc_c (w24h w1) (w24h w2) (plus_b8_dc_c (w24l w1) (w24l w2) c)).
+ndefinition plus_w24_dc_c ≝ λc,w1,w2.fst … (plus_w24_dc_dc c w1 w2).
 
 (* operatore somma con data → data+carry *)
-ndefinition plus_w24_d_dc ≝
-λw1,w2:word24.
- match plus_b8_d_dc (w24l w1) (w24l w2) with
-  [ pair l c ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c with
-   [ pair h c' ⇒ match plus_b8_dc_dc (w24x w1) (w24x w2) c' with
-    [ pair x c'' ⇒ pair … 〈x;h;l〉 c'' ]]].
+ndefinition plus_w24_d_dc ≝ plus_w24_dc_dc false.
 
 (* operatore somma con data → data *)
-ndefinition plus_w24_d_d ≝
-λw1,w2:word24.
- match plus_b8_d_dc (w24l w1) (w24l w2) with
-  [ pair l c ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c with
-   [ pair h c' ⇒ 〈plus_b8_dc_d (w24x w1) (w24x w2) c';h;l〉 ]].
+ndefinition plus_w24_d_d ≝ λw1,w2.snd … (plus_w24_d_dc w1 w2).
 
 (* operatore somma con data → c *)
-ndefinition plus_w24_d_c ≝
-λw1,w2:word24.
- plus_b8_dc_c (w24x w1) (w24x w2) (plus_b8_dc_c (w24h w1) (w24h w2) (plus_b8_d_c (w24l w1) (w24l w2))).
-
-(* operatore Most Significant Bit *)
-ndefinition MSB_w24 ≝ λw:word24.eq_ex x8 (and_ex x8 (b8h (w24x w))).
+ndefinition plus_w24_d_c ≝ λw1,w2.fst … (plus_w24_d_dc w1 w2).
 
 (* operatore predecessore *)
 ndefinition pred_w24 ≝
-λw:word24.match eq_b8 (w24l w) (mk_byte8 x0 x0) with
- [ true ⇒ match eq_b8 (w24h w) (mk_byte8 x0 x0) with
+λw:word24.match eq_b8 (w24l w) 〈x0,x0〉 with
+ [ true ⇒ match eq_b8 (w24h w) 〈x0,x0〉 with
   [ true ⇒ mk_word24 (pred_b8 (w24x w)) (pred_b8 (w24h w)) (pred_b8 (w24l w))
   | false ⇒ mk_word24 (w24x w) (pred_b8 (w24h w)) (pred_b8 (w24l w)) ]
  | false ⇒ mk_word24 (w24x w) (w24h w) (pred_b8 (w24l w)) ].
 
 (* operatore successore *)
 ndefinition succ_w24 ≝
-λw:word24.match eq_b8 (w24l w) (mk_byte8 xF xF) with
- [ true ⇒ match eq_b8 (w24h w) (mk_byte8 xF xF) with
+λw:word24.match eq_b8 (w24l w) 〈xF,xF〉 with
+ [ true ⇒ match eq_b8 (w24h w) 〈xF,xF〉 with
   [ true ⇒ mk_word24 (succ_b8 (w24x w)) (succ_b8 (w24h w)) (succ_b8 (w24l w))
   | false ⇒ mk_word24 (w24x w) (succ_b8 (w24h w)) (succ_b8 (w24l w)) ]
  | false ⇒ mk_word24 (w24x w) (w24h w) (succ_b8 (w24l w)) ].
 
 (* operatore neg/complemento a 2 *)
 ndefinition compl_w24 ≝
-λw:word24.match MSB_w24 w with
+λw:word24.match getMSB_w24 w with
  [ true ⇒ succ_w24 (not_w24 w)
  | false ⇒ not_w24 (pred_w24 w) ].
 
+(* operatore abs *)
+ndefinition abs_w24 ≝
+λw:word24.match getMSB_w24 w with
+ [ true ⇒ compl_w24 w | false ⇒ w ].
+
 (* operatore x in [inf,sup] o in sup],[inf *)
 ndefinition inrange_w24 ≝
 λx,inf,sup:word24.
  match le_w24 inf sup with
   [ true ⇒ and_bool | false ⇒ or_bool ]
  (le_w24 inf x) (le_w24 x sup).
-
-(* iteratore sulle word *)
-ndefinition forall_w24 ≝
- λP.
-  forall_b8 (λbx.
-  forall_b8 (λbh.
-  forall_b8 (λbl.
-   P (mk_word24 bx bh bl )))).