X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fword32.ma;h=8eb5d52e540888cdae1dce4a68dff1458e744996;hb=17c6ac2888a1f30aee059f5cf6b8872bb4f3ab61;hp=e9ede855628ef3c4433c99f1a1b586a089413830;hpb=64bdbee95e40a5be3bb6c5c2866869103730a4d0;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/word32.ma b/helm/software/matita/contribs/ng_assembly/freescale/word32.ma
index e9ede8556..8eb5d52e5 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/word32.ma
@@ -13,9 +13,10 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -31,21 +32,6 @@ nrecord word32 : Type ≝
  w32l: word16
  }.
 
-ndefinition word32_ind : ΠP:word32 → Prop.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝
-λP:word32 → Prop.λf:Πw:word16.Πw1:word16.P (mk_word32 w w1).λdw:word32.
- match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ].
-
-ndefinition word32_rec : ΠP:word32 → Set.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝
-λP:word32 → Set.λf:Πw:word16.Πw1:word16.P (mk_word32 w w1).λdw:word32.
- match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ].
-
-ndefinition word32_rect : ΠP:word32 → Type.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝
-λP:word32 → Type.λf:Πw:word16.Πw1:word16.P (mk_word32 w w1).λdw:word32.
- match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ].
-
-ndefinition w32h ≝ λdw:word32.match dw with [ mk_word32 x _ ⇒ x ].
-ndefinition w32l ≝ λdw:word32.match dw with [ mk_word32 _ x ⇒ x ].
-
 (* \langle \rangle *)
 notation "〈x.y〉" non associative with precedence 80
  for @{ 'mk_word32 $x $y }.
@@ -87,13 +73,13 @@ ndefinition xor_w32 ≝
 ndefinition rcr_w32 ≝
 λdw:word32.λc:bool.match rcr_w16 (w32h dw) c with
  [ pair wh' c' ⇒ match rcr_w16 (w32l dw) c' with
-  [ pair wl' c'' ⇒ pair ?? (mk_word32 wh' wl') c'' ]]. 
+  [ pair wl' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]]. 
 
 (* operatore shift destro *)
 ndefinition shr_w32 ≝
 λdw:word32.match rcr_w16 (w32h dw) false with
  [ pair wh' c' ⇒ match rcr_w16 (w32l dw) c' with
-  [ pair wl' c'' ⇒ pair ?? (mk_word32 wh' wl') c'' ]].
+  [ pair wl' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]].
 
 (* operatore rotazione destra *)
 ndefinition ror_w32 ≝
@@ -104,22 +90,22 @@ ndefinition ror_w32 ≝
    | false ⇒ mk_word32 wh' wl' ]]].
 
 (* operatore rotazione destra n-volte *)
-nlet rec ror_w32_n (dw:word32) (n:nat) on n ≝
- match n with
-  [ O ⇒ dw
-  | S n' ⇒ ror_w32_n (ror_w32 dw) n' ].
+nlet rec ror_w32_n (dw:word32) (n:bitrigesim) (r:rec_bitrigesim n) on r ≝
+ match r with
+  [ bi_O ⇒ dw
+  | bi_S t n' ⇒ ror_w32_n (ror_w32 dw) t n' ].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_w32 ≝
 λdw:word32.λc:bool.match rcl_w16 (w32l dw) c with
  [ pair wl' c' ⇒ match rcl_w16 (w32h dw) c' with
-  [ pair wh' c'' ⇒ pair ?? (mk_word32 wh' wl') c'' ]]. 
+  [ pair wh' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]]. 
 
 (* operatore shift sinistro *)
 ndefinition shl_w32 ≝
 λdw:word32.match rcl_w16 (w32l dw) false with
  [ pair wl' c' ⇒ match rcl_w16 (w32h dw) c' with
-  [ pair wh' c'' ⇒ pair ?? (mk_word32 wh' wl') c'' ]].
+  [ pair wh' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]].
 
 (* operatore rotazione sinistra *)
 ndefinition rol_w32 ≝
@@ -130,10 +116,10 @@ ndefinition rol_w32 ≝
    | false ⇒ mk_word32 wh' wl' ]]].
 
 (* operatore rotazione sinistra n-volte *)
-nlet rec rol_w32_n (dw:word32) (n:nat) on n ≝
- match n with
-  [ O ⇒ dw
-  | S n' ⇒ rol_w32_n (rol_w32 dw) n' ].
+nlet rec rol_w32_n (dw:word32) (n:bitrigesim) (r:rec_bitrigesim n) on r ≝
+ match r with
+  [ bi_O ⇒ dw
+  | bi_S t n' ⇒ rol_w32_n (rol_w32 dw) t n' ].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_w32 ≝
@@ -144,7 +130,7 @@ ndefinition plus_w32_dc_dc ≝
 λdw1,dw2:word32.λc:bool.
  match plus_w16_dc_dc (w32l dw1) (w32l dw2) c with
   [ pair l c ⇒ match plus_w16_dc_dc (w32h dw1) (w32h dw2) c with
-   [ pair h c' ⇒ pair ?? 〈h.l〉 c' ]].
+   [ pair h c' ⇒ pair … 〈h.l〉 c' ]].
 
 (* operatore somma con data+carry → data *)
 ndefinition plus_w32_dc_d ≝
@@ -162,7 +148,7 @@ ndefinition plus_w32_d_dc ≝
 λdw1,dw2:word32.
  match plus_w16_d_dc (w32l dw1) (w32l dw2) with
   [ pair l c ⇒ match plus_w16_dc_dc (w32h dw1) (w32h dw2) c with
-   [ pair h c' ⇒ pair ?? 〈h.l〉 c' ]].
+   [ pair h c' ⇒ pair … 〈h.l〉 c' ]].
 
 (* operatore somma con data → data *)
 ndefinition plus_w32_d_d ≝
@@ -178,9 +164,6 @@ ndefinition plus_w32_d_c ≝
 (* operatore Most Significant Bit *)
 ndefinition MSB_w32 ≝ λdw:word32.eq_ex x8 (and_ex x8 (b8h (w16h (w32h dw)))).
 
-(* word → naturali *)
-ndefinition nat_of_word32 ≝ λdw:word32. (256 * 256 * (nat_of_word16 (w32h dw))) + (nat_of_word16 (w32l dw)).
-
 (* operatore predecessore *)
 ndefinition pred_w32 ≝
 λdw:word32.match eq_w16 (w32l dw) (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) with
@@ -217,39 +200,39 @@ ndefinition mul_w16 ≝
 ]]]]]].
 
 (* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
-nlet rec div_w16_aux (divd:word32) (divs:word32) (molt:word16) (q:word16) (c:nat) on c ≝
+nlet rec div_w16_aux (divd:word32) (divs:word32) (molt:word16) (q:word16) (c:exadecim) (rc:rec_exadecim c) on rc ≝
   let w' ≝ plus_w32_d_d divd (compl_w32 divs) in
-   match c with
-   [ O ⇒ match le_w32 divs divd with
-    [ true ⇒ triple ??? (or_w16 molt q) (w32l w') (⊖ (eq_w16 (w32h w') 〈〈x0,x0〉:〈x0,x0〉〉))
-    | false ⇒ triple ??? q (w32l divd) (⊖ (eq_w16 (w32h divd) 〈〈x0,x0〉:〈x0,x0〉〉)) ]
-   | S c' ⇒ match le_w32 divs divd with
-    [ true ⇒ div_w16_aux w' (ror_w32 divs) (ror_w16 molt) (or_w16 molt q) c'
-    | false ⇒ div_w16_aux divd (ror_w32 divs) (ror_w16 molt) q c' ]].
+   match rc with
+   [ ex_O ⇒ match le_w32 divs divd with
+    [ true ⇒ triple … (or_w16 molt q) (w32l w') (⊖ (eq_w16 (w32h w') 〈〈x0,x0〉:〈x0,x0〉〉))
+    | false ⇒ triple … q (w32l divd) (⊖ (eq_w16 (w32h divd) 〈〈x0,x0〉:〈x0,x0〉〉)) ]
+   | ex_S t c' ⇒ match le_w32 divs divd with
+    [ true ⇒ div_w16_aux w' (ror_w32 divs) (ror_w16 molt) (or_w16 molt q) t c'
+    | false ⇒ div_w16_aux divd (ror_w32 divs) (ror_w16 molt) q t c' ]].
 
 ndefinition div_w16 ≝
 λw:word32.λb:word16.match eq_w16 b 〈〈x0,x0〉:〈x0,x0〉〉 with
 (* 
    la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
 *)
- [ true ⇒ triple ??? 〈〈xF,xF〉:〈xF,xF〉〉 (w32l w) true
+ [ true ⇒ triple … 〈〈xF,xF〉:〈xF,xF〉〉 (w32l w) true
  | false ⇒ match eq_w32 w 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈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〉〉 〈〈x0,x0〉:〈x0,x0〉〉 false
+  [ true ⇒ triple … 〈〈x0,x0〉:〈x0,x0〉〉 〈〈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_w16_aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 15) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 15 ]].
+  | false ⇒ div_w16_aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 ? (bit_to_recbit t0F)) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 ? (ex_to_recex xF) ]].
 
 (* operatore x in [inf,sup] *)
-ndefinition in_range ≝
+ndefinition inrange_w32 ≝
 λx,inf,sup:word32.(le_w32 inf sup) ⊗ (ge_w32 x inf) ⊗ (le_w32 x sup).
 
 (* iteratore sulle word *)
-ndefinition forall_word32 ≝
+ndefinition forall_w32 ≝
  λP.
-  forall_word16 (λbh.
-  forall_word16 (λbl.
+  forall_w16 (λbh.
+  forall_w16 (λbl.
    P (mk_word32 bh bl ))).