freescale porting

[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
index e89e64f3d81babb84715b4de1a9623f685c579c8..7523ec9189175370410acbea3ec24f7cfdbec99c 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma
@@ -80,27 +80,27 @@ ndefinition xor_w16 ≝
 ndefinition rcr_w16 ≝
 λw:word16.λc:bool.match rcr_b8 (w16h w) c with
  [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
-  [ pair wl' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]]. 
+  [ pair wl' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]].
 
 (* operatore shift destro *)
 ndefinition shr_w16 ≝
-λw:word16.match rcr_b8 (w16h w) false with
+λw:word16.match shr_b8 (w16h w) with
  [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
   [ pair wl' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]].
 
 (* operatore rotazione destra *)
 ndefinition ror_w16 ≝
-λw:word16.match rcr_b8 (w16h w) false with
+λw:word16.match shr_b8 (w16h w) with
  [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
   [ pair wl' c'' ⇒ match c'' with
    [ true ⇒ mk_word16 (or_b8 (mk_byte8 x8 x0) wh') wl'
    | false ⇒ mk_word16 wh' wl' ]]].
 
 (* operatore rotazione destra n-volte *)
-nlet rec ror_w16_n (w:word16) (n:nat) on n ≝
- match n with
-  [ O ⇒ w
-  | S n' ⇒ ror_w16_n (ror_w16 w) n' ].
+nlet rec ror_w16_n (w:word16) (e:exadecim) (re:rec_exadecim e) on re ≝
+ match re with
+  [ ex_O ⇒ w
+  | ex_S e' n' ⇒ ror_w16_n (ror_w16 w) e' n' ].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_w16 ≝
@@ -110,23 +110,23 @@ ndefinition rcl_w16 ≝
 
 (* operatore shift sinistro *)
 ndefinition shl_w16 ≝
-λw:word16.match rcl_b8 (w16l w) false with
+λw:word16.match shl_b8 (w16l w) with
  [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
   [ pair wh' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]].
 
 (* operatore rotazione sinistra *)
 ndefinition rol_w16 ≝
-λw:word16.match rcl_b8 (w16l w) false with
+λw:word16.match shl_b8 (w16l w) with
  [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
   [ pair wh' c'' ⇒ match c'' with
    [ true ⇒ mk_word16 wh' (or_b8 (mk_byte8 x0 x1) wl')
    | false ⇒ mk_word16 wh' wl' ]]].
 
 (* operatore rotazione sinistra n-volte *)
-nlet rec rol_w16_n (w:word16) (n:nat) on n ≝
- match n with
-  [ O ⇒ w
-  | S n' ⇒ rol_w16_n (rol_w16 w) n' ].
+nlet rec rol_w16_n (w:word16) (e:exadecim) (re:rec_exadecim e) on re ≝
+ match re with
+  [ ex_O ⇒ w
+  | ex_S e' n' ⇒ rol_w16_n (rol_w16 w) e' n' ].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_w16 ≝
@@ -136,14 +136,14 @@ ndefinition not_w16 ≝
 ndefinition plus_w16_dc_dc ≝
 λw1,w2:word16.λc:bool.
  match plus_b8_dc_dc (w16l w1) (w16l w2) c with
-  [ pair l c ⇒ match plus_b8_dc_dc (w16h w1) (w16h w2) c with
-   [ pair h c' ⇒ pair … 〈h:l〉 c' ]].
+  [ pair l c' ⇒ match plus_b8_dc_dc (w16h w1) (w16h w2) c' with
+   [ pair h c'' ⇒ pair … 〈h:l〉 c'' ]].
 
 (* operatore somma con data+carry → data *)
 ndefinition plus_w16_dc_d ≝
 λw1,w2:word16.λc:bool.
  match plus_b8_dc_dc (w16l w1) (w16l w2) c with
-  [ pair l c ⇒ 〈plus_b8_dc_d (w16h w1) (w16h w2) c:l〉 ].
+  [ pair l c' ⇒ 〈plus_b8_dc_d (w16h w1) (w16h w2) c':l〉 ].
 
 (* operatore somma con data+carry → c *)
 ndefinition plus_w16_dc_c ≝
@@ -207,17 +207,17 @@ ndefinition mul_b8 ≝
 ]]]]]].
 
 (* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
-nlet rec div_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (c:nat) on c ≝
+nlet rec div_w16_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (o:oct) (ro:rec_oct o) on ro ≝
  let w' ≝ plus_w16_d_d divd (compl_w16 divs) in
-  match c with
-  [ O ⇒ match le_w16 divs divd with
+  match ro with
+  [ oc_O ⇒ match le_w16 divs divd with
    [ true ⇒ triple … (or_b8 molt q) (w16l w') (⊖ (eq_b8 (w16h w') 〈x0,x0〉))
    | false ⇒ triple … q (w16l divd) (⊖ (eq_b8 (w16h divd) 〈x0,x0〉)) ]
-  | S c' ⇒ match le_w16 divs divd with
-   [ true ⇒ div_b8_aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) c'
-   | false ⇒ div_b8_aux divd (ror_w16 divs) (ror_b8 molt) q c' ]].
+  | oc_S o' ro' ⇒ match le_w16 divs divd with
+   [ true ⇒ div_w16_b8_aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) o' ro'
+   | false ⇒ div_w16_b8_aux divd (ror_w16 divs) (ror_b8 molt) q o' ro' ]].
 
-ndefinition div_b8 ≝
+ndefinition div_w16_b8 ≝
 λw:word16.λb:byte8.match eq_b8 b 〈x0,x0〉 with
 (* 
    la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
@@ -231,7 +231,7 @@ ndefinition div_b8 ≝
 (* 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 (rol_w16_n 〈〈x0,x0〉:b〉 nat7) 〈x8,x0〉 〈x0,x0〉 nat7 ]].
+  | false ⇒ div_w16_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 ? (ex_to_recex x7)) 〈x8,x0〉 〈x0,x0〉 ? (oct_to_recoct o7) ]].
 
 (* operatore x in [inf,sup] o in sup],[inf *)
 ndefinition inrange_w16 ≝