| 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) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
+ match rt with
+ [ bi_O ⇒ dw
+ | bi_S t' n' ⇒ ror_w32_n (ror_w32 dw) t' n' ].
(* operatore rotazione sinistra con carry *)
ndefinition rcl_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) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
+ match rt with
+ [ bi_O ⇒ dw
+ | bi_S t' n' ⇒ rol_w32_n (rol_w32 dw) t' n' ].
(* operatore not/complemento a 1 *)
ndefinition not_w32 ≝
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 l c' ⇒ match plus_w16_dc_dc (w32h dw1) (w32h dw2) c' with
+ [ pair h c'' ⇒ pair … 〈h.l〉 c'' ]].
(* operatore somma con data+carry → data *)
ndefinition plus_w32_dc_d ≝
λdw1,dw2:word32.λc:bool.
match plus_w16_dc_dc (w32l dw1) (w32l dw2) c with
- [ pair l c ⇒ 〈plus_w16_dc_d (w32h dw1) (w32h dw2) c.l〉 ].
+ [ pair l c' ⇒ 〈plus_w16_dc_d (w32h dw1) (w32h dw2) c'.l〉 ].
(* operatore somma con data+carry → c *)
ndefinition plus_w32_dc_c ≝
]]]]]].
(* 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_w32_w16_aux (divd:word32) (divs:word32) (molt:word16) (q:word16) (e:exadecim) (re:rec_exadecim e) on re ≝
let w' ≝ plus_w32_d_d divd (compl_w32 divs) in
- match c with
- [ O ⇒ match le_w32 divs divd with
+ match re 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〉〉)) ]
- | 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' ]].
+ | ex_S e' re' ⇒ match le_w32 divs divd with
+ [ true ⇒ div_w32_w16_aux w' (ror_w32 divs) (ror_w16 molt) (or_w16 molt q) e' re'
+ | false ⇒ div_w32_w16_aux divd (ror_w32 divs) (ror_w16 molt) q e' re' ]].
-ndefinition div_w16 ≝
+ndefinition div_w32_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
(* 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〉 nat15) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 nat15 ]].
+ | false ⇒ div_w32_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] o in sup],[inf *)
ndefinition inrange_w32 ≝
(* iteratore sulle word *)
ndefinition forall_w32 ≝
λP.
- forall_w16 (λbh.
- forall_w16 (λbl.
- P (mk_word32 bh bl ))).
+ forall_w16 (λwh.
+ forall_w16 (λwl.
+ P (mk_word32 wh wl ))).