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 }.
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 ≝
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 ≝
λ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 ≝
λ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 ≝
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〉〉)) ]
+ [ 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' ]].
(*
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 *)