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 (* iteratore sulle dword *)
37 ndefinition forall_w32 ≝ forall_cn ? forall_w16.
40 ndefinition eq_w32 ≝ eq2_cn ? eq_w16.
43 ndefinition lt_w32 ≝ ltgt_cn ? eq_w16 lt_w16.
46 ndefinition le_w32 ≝ lege_cn ? eq_w16 lt_w16 le_w16.
49 ndefinition gt_w32 ≝ ltgt_cn ? eq_w16 gt_w16.
52 ndefinition ge_w32 ≝ lege_cn ? eq_w16 gt_w16 ge_w16.
55 ndefinition and_w32 ≝ fop2_cn ? and_w16.
58 ndefinition or_w32 ≝ fop2_cn ? or_w16.
61 ndefinition xor_w32 ≝ fop2_cn ? xor_w16.
63 (* operatore Most Significant Bit *)
64 ndefinition getMSB_w32 ≝ getOPH_cn ? getMSB_w16.
65 ndefinition setMSB_w32 ≝ setOPH_cn ? setMSB_w16.
67 (* operatore Least Significant Bit *)
68 ndefinition getLSB_w32 ≝ getOPL_cn ? getLSB_w16.
69 ndefinition setLSB_w32 ≝ setOPL_cn ? setLSB_w16.
71 (* operatore rotazione destra con carry *)
72 ndefinition rcr_w32 ≝ opcr_cn ? rcr_w16.
74 (* operatore shift destro *)
75 ndefinition shr_w32 ≝ opcr_cn ? rcr_w16 false.
77 (* operatore rotazione destra *)
79 λw.match shr_w32 w with
80 [ pair c w' ⇒ match c with
81 [ true ⇒ setMSB_w32 w' | false ⇒ w' ]].
83 (* operatore rotazione sinistra con carry *)
84 ndefinition rcl_w32 ≝ opcl_cn ? rcl_w16.
86 (* operatore shift sinistro *)
87 ndefinition shl_w32 ≝ opcl_cn ? rcl_w16 false.
89 (* operatore rotazione sinistra *)
91 λw.match shl_w32 w with
92 [ pair c w' ⇒ match c with
93 [ true ⇒ setLSB_w32 w' | false ⇒ w' ]].
95 (* operatore not/complemento a 1 *)
96 ndefinition not_w32 ≝ fop_cn ? not_w16.
98 (* operatore somma con data+carry → data+carry *)
99 ndefinition plus_w32_dc_dc ≝ opcl2_cn ? plus_w16_dc_dc.
101 (* operatore somma con data+carry → data *)
102 ndefinition plus_w32_dc_d ≝ λc,w1,w2.snd … (plus_w32_dc_dc c w1 w2).
104 (* operatore somma con data+carry → c *)
105 ndefinition plus_w32_dc_c ≝ λc,w1,w2.fst … (plus_w32_dc_dc c w1 w2).
107 (* operatore somma con data → data+carry *)
108 ndefinition plus_w32_d_dc ≝ opcl2_cn ? plus_w16_dc_dc false.
110 (* operatore somma con data → data *)
111 ndefinition plus_w32_d_d ≝ λw1,w2.snd … (plus_w32_d_dc w1 w2).
113 (* operatore somma con data → c *)
114 ndefinition plus_w32_d_c ≝ λw1,w2.fst … (plus_w32_d_dc w1 w2).
116 (* operatore predecessore *)
117 ndefinition pred_w32 ≝ predsucc_cn ? (eq_w16 〈〈x0,x0〉:〈x0,x0〉〉) pred_w16.
119 (* operatore successore *)
120 ndefinition succ_w32 ≝ predsucc_cn ? (eq_w16 〈〈xF,xF〉:〈xF,xF〉〉) succ_w16.
122 (* operatore neg/complemento a 2 *)
123 ndefinition compl_w32 ≝
124 λw:word32.match getMSB_w32 w with
125 [ true ⇒ succ_w32 (not_w32 w)
126 | false ⇒ not_w32 (pred_w32 w) ].
128 (* operatore x in [inf,sup] o in sup],[inf *)
129 ndefinition inrange_w32 ≝
131 match le_w32 inf sup with
132 [ true ⇒ and_bool | false ⇒ or_bool ]
133 (le_w32 inf x) (le_w32 x sup).