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/byte8.ma".
29 nrecord word24 : Type ≝
37 notation "〈x;y;z〉" non associative with precedence 80
38 for @{ 'mk_word24 $x $y $z }.
39 interpretation "mk_word24" 'mk_word24 x y z = (mk_word24 x y z).
43 λw1,w2.(eq_b8 (w24x w1) (w24x w2)) ⊗
44 (eq_b8 (w24h w1) (w24h w2)) ⊗
45 (eq_b8 (w24l w1) (w24l w2)).
50 (lt_b8 (w24x w1) (w24x w2)) ⊕
51 ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((lt_b8 (w24h w1) (w24h w2)) ⊕
52 ((eq_b8 (w24h w1) (w24h w2)) ⊗ (lt_b8 (w24l w1) (w24l w2))))).
57 (lt_b8 (w24x w1) (w24x w2)) ⊕
58 ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((lt_b8 (w24h w1) (w24h w2)) ⊕
59 ((eq_b8 (w24h w1) (w24h w2)) ⊗ (le_b8 (w24l w1) (w24l w2))))).
64 (gt_b8 (w24x w1) (w24x w2)) ⊕
65 ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((gt_b8 (w24h w1) (w24h w2)) ⊕
66 ((eq_b8 (w24h w1) (w24h w2)) ⊗ (gt_b8 (w24l w1) (w24l w2))))).
71 (gt_b8 (w24x w1) (w24x w2)) ⊕
72 ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((gt_b8 (w24h w1) (w24h w2)) ⊕
73 ((eq_b8 (w24h w1) (w24h w2)) ⊗ (ge_b8 (w24l w1) (w24l w2))))).
78 mk_word24 (and_b8 (w24x w1) (w24x w2))
79 (and_b8 (w24h w1) (w24h w2))
80 (and_b8 (w24l w1) (w24l w2)).
85 mk_word24 (or_b8 (w24x w1) (w24x w2))
86 (or_b8 (w24h w1) (w24h w2))
87 (or_b8 (w24l w1) (w24l w2)).
92 mk_word24 (xor_b8 (w24x w1) (w24x w2))
93 (xor_b8 (w24h w1) (w24h w2))
94 (xor_b8 (w24l w1) (w24l w2)).
96 (* operatore rotazione destra con carry *)
98 λw:word24.λc:bool.match rcr_b8 (w24x w) c with
99 [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
100 [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
101 [ pair wl' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
103 (* operatore shift destro *)
104 ndefinition shr_w24 ≝
105 λw:word24.match shr_b8 (w24x w) with
106 [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
107 [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
108 [ pair wl' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
110 (* operatore rotazione destra *)
111 ndefinition ror_w24 ≝
112 λw:word24.match shr_b8 (w24x w) with
113 [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
114 [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
115 [ pair wl' c''' ⇒ match c''' with
116 [ true ⇒ mk_word24 (or_b8 (mk_byte8 x8 x0) wx') wh' wl'
117 | false ⇒ mk_word24 wx' wh' wl' ]]]].
119 (* operatore rotazione destra n-volte *)
120 nlet rec ror_w24_n (w:word24) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
123 | bi_S t' n' ⇒ ror_w24_n (ror_w24 w) t' n' ].
125 (* operatore rotazione sinistra con carry *)
126 ndefinition rcl_w24 ≝
127 λw:word24.λc:bool.match rcl_b8 (w24l w) c with
128 [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
129 [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
130 [ pair wx' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
132 (* operatore shift sinistro *)
133 ndefinition shl_w24 ≝
134 λw:word24.match shl_b8 (w24l w) with
135 [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
136 [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
137 [ pair wx' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
139 (* operatore rotazione sinistra *)
140 ndefinition rol_w24 ≝
141 λw:word24.match shl_b8 (w24l w) with
142 [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
143 [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
144 [ pair wx' c''' ⇒ match c''' with
145 [ true ⇒ mk_word24 wx' wh' (or_b8 (mk_byte8 x0 x1) wl')
146 | false ⇒ mk_word24 wx' wh' wl' ]]]].
148 (* operatore rotazione sinistra n-volte *)
149 nlet rec rol_w24_n (w:word24) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
152 | bi_S t' n' ⇒ rol_w24_n (rol_w24 w) t' n' ].
154 (* operatore not/complemento a 1 *)
155 ndefinition not_w24 ≝
156 λw:word24.mk_word24 (not_b8 (w24x w)) (not_b8 (w24h w)) (not_b8 (w24l w)).
158 (* operatore somma con data+carry → data+carry *)
159 ndefinition plus_w24_dc_dc ≝
160 λw1,w2:word24.λc:bool.
161 match plus_b8_dc_dc (w24l w1) (w24l w2) c with
162 [ pair l c' ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c' with
163 [ pair h c'' ⇒ match plus_b8_dc_dc (w24x w1) (w24x w2) c'' with
164 [ pair x c''' ⇒ pair … 〈x;h;l〉 c''' ]]].
166 (* operatore somma con data+carry → data *)
167 ndefinition plus_w24_dc_d ≝
168 λw1,w2:word24.λc:bool.
169 match plus_b8_dc_dc (w24l w1) (w24l w2) c with
170 [ pair l c' ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c' with
171 [ pair h c'' ⇒ 〈plus_b8_dc_d (w24x w1) (w24x w2) c'';h;l〉 ]].
173 (* operatore somma con data+carry → c *)
174 ndefinition plus_w24_dc_c ≝
175 λw1,w2:word24.λc:bool.
176 plus_b8_dc_c (w24x w1) (w24x w2) (plus_b8_dc_c (w24h w1) (w24h w2) (plus_b8_dc_c (w24l w1) (w24l w2) c)).
178 (* operatore somma con data → data+carry *)
179 ndefinition plus_w24_d_dc ≝
181 match plus_b8_d_dc (w24l w1) (w24l w2) with
182 [ pair l c ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c with
183 [ pair h c' ⇒ match plus_b8_dc_dc (w24x w1) (w24x w2) c' with
184 [ pair x c'' ⇒ pair … 〈x;h;l〉 c'' ]]].
186 (* operatore somma con data → data *)
187 ndefinition plus_w24_d_d ≝
189 match plus_b8_d_dc (w24l w1) (w24l w2) with
190 [ pair l c ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c with
191 [ pair h c' ⇒ 〈plus_b8_dc_d (w24x w1) (w24x w2) c';h;l〉 ]].
193 (* operatore somma con data → c *)
194 ndefinition plus_w24_d_c ≝
196 plus_b8_dc_c (w24x w1) (w24x w2) (plus_b8_dc_c (w24h w1) (w24h w2) (plus_b8_d_c (w24l w1) (w24l w2))).
198 (* operatore Most Significant Bit *)
199 ndefinition MSB_w24 ≝ λw:word24.eq_ex x8 (and_ex x8 (b8h (w24x w))).
201 (* operatore predecessore *)
202 ndefinition pred_w24 ≝
203 λw:word24.match eq_b8 (w24l w) (mk_byte8 x0 x0) with
204 [ true ⇒ match eq_b8 (w24h w) (mk_byte8 x0 x0) with
205 [ true ⇒ mk_word24 (pred_b8 (w24x w)) (pred_b8 (w24h w)) (pred_b8 (w24l w))
206 | false ⇒ mk_word24 (w24x w) (pred_b8 (w24h w)) (pred_b8 (w24l w)) ]
207 | false ⇒ mk_word24 (w24x w) (w24h w) (pred_b8 (w24l w)) ].
209 (* operatore successore *)
210 ndefinition succ_w24 ≝
211 λw:word24.match eq_b8 (w24l w) (mk_byte8 xF xF) with
212 [ true ⇒ match eq_b8 (w24h w) (mk_byte8 xF xF) with
213 [ true ⇒ mk_word24 (succ_b8 (w24x w)) (succ_b8 (w24h w)) (succ_b8 (w24l w))
214 | false ⇒ mk_word24 (w24x w) (succ_b8 (w24h w)) (succ_b8 (w24l w)) ]
215 | false ⇒ mk_word24 (w24x w) (w24h w) (succ_b8 (w24l w)) ].
217 (* operatore neg/complemento a 2 *)
218 ndefinition compl_w24 ≝
219 λw:word24.match MSB_w24 w with
220 [ true ⇒ succ_w24 (not_w24 w)
221 | false ⇒ not_w24 (pred_w24 w) ].
223 (* operatore x in [inf,sup] o in sup],[inf *)
224 ndefinition inrange_w24 ≝
226 match le_w24 inf sup with
227 [ true ⇒ and_bool | false ⇒ or_bool ]
228 (le_w24 inf x) (le_w24 x sup).
230 (* iteratore sulle word *)
231 ndefinition forall_w24 ≝
236 P (mk_word24 bx bh bl )))).