1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "num/word16.ma".
29 ndefinition word32 ≝ comp_num word16.
30 ndefinition mk_word32 ≝ λw1,w2.mk_comp_num word16 w1 w2.
33 notation "〈x.y〉" non associative with precedence 80
34 for @{ mk_comp_num word16 $x $y }.
36 ndefinition word32_is_comparable_ext ≝ cn_is_comparable_ext word16_is_comparable_ext.
37 unification hint 0 ≔ ⊢ carr (comp_base word32_is_comparable_ext) ≡ comp_num (comp_num (comp_num exadecim)).
38 unification hint 0 ≔ ⊢ carr (comp_base word32_is_comparable_ext) ≡ comp_num (comp_num byte8).
39 unification hint 0 ≔ ⊢ carr (comp_base word32_is_comparable_ext) ≡ comp_num word16.
40 unification hint 0 ≔ ⊢ carr (comp_base word32_is_comparable_ext) ≡ word32.
42 (* operatore estensione unsigned *)
43 ndefinition extu_w32 ≝ λw2.〈zeroc ?.w2〉.
44 ndefinition extu2_w32 ≝ λb2.〈zeroc ?.〈zeroc ?:b2〉〉.
45 ndefinition extu3_w32 ≝ λe2.〈zeroc ?.〈zeroc ?:〈zeroc ?,e2〉〉〉.
47 (* operatore estensione signed *)
48 ndefinition exts_w32 ≝
49 λw2.〈(match getMSBc ? w2 with
50 [ true ⇒ predc ? (zeroc ?) | false ⇒ zeroc ? ]).w2〉.
51 ndefinition exts2_w32 ≝
52 λb2.(match getMSBc ? b2 with
53 [ true ⇒ 〈predc ? (zeroc ?).〈predc ? (zeroc ?):b2〉〉
54 | false ⇒ 〈zeroc ?.〈zeroc ?:b2〉〉 ]).
55 ndefinition exts3_w32 ≝
56 λe2.(match getMSBc ? e2 with
57 [ true ⇒ 〈predc ? (zeroc ?).〈predc ? (zeroc ?):〈predc ? (zeroc ?),e2〉〉〉
58 | false ⇒ 〈zeroc ?.〈zeroc ?:〈zeroc ?,e2〉〉〉 ]).
60 (* operatore moltiplicazione senza segno *)
61 (* 〈a1,a2〉 * 〈b1,b2〉 = (a1*b1) x0 x0 + x0 (a1*b2) x0 + x0 (a2*b1) x0 + x0 x0 (a2*b2) *)
62 ndefinition mulu_w16_aux ≝
63 λw:word32.nat_it ? (rolc ?) w nat8.
65 ndefinition mulu_w16 ≝
67 plusc_d_d ? 〈(mulu_b8 (cnH ? w1) (cnH ? w2)).zeroc ?〉
68 (plusc_d_d ? (mulu_w16_aux (extu_w32 (mulu_b8 (cnH ? w1) (cnL ? w2))))
69 (plusc_d_d ? (mulu_w16_aux (extu_w32 (mulu_b8 (cnL ? w1) (cnH ? w2))))
70 (extu_w32 (mulu_b8 (cnL ? w1) (cnL ? w2))))).
72 (* operatore moltiplicazione con segno *)
73 (* x * y = sgn(x) * sgn(y) * |x| * |y| *)
74 ndefinition muls_w16 ≝
76 (* ++/-- → +, +-/-+ → - *)
77 match (getMSBc ? w1) ⊙ (getMSBc ? w2) with
81 | false ⇒ λx.x ] (mulu_w16 (absc ? w1) (absc ? w2)).