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).
41 (* iteratore sulle word *)
42 ndefinition forall_w24 ≝
47 P (mk_word24 bx bh bl )))).
51 λw1,w2.(eq_b8 (w24x w1) (w24x w2)) ⊗
52 (eq_b8 (w24h w1) (w24h w2)) ⊗
53 (eq_b8 (w24l w1) (w24l w2)).
58 (lt_b8 (w24x w1) (w24x w2)) ⊕
59 ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((lt_b8 (w24h w1) (w24h w2)) ⊕
60 ((eq_b8 (w24h w1) (w24h w2)) ⊗ (lt_b8 (w24l w1) (w24l w2))))).
65 (lt_b8 (w24x w1) (w24x w2)) ⊕
66 ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((lt_b8 (w24h w1) (w24h w2)) ⊕
67 ((eq_b8 (w24h w1) (w24h w2)) ⊗ (le_b8 (w24l w1) (w24l w2))))).
72 (gt_b8 (w24x w1) (w24x w2)) ⊕
73 ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((gt_b8 (w24h w1) (w24h w2)) ⊕
74 ((eq_b8 (w24h w1) (w24h w2)) ⊗ (gt_b8 (w24l w1) (w24l w2))))).
79 (gt_b8 (w24x w1) (w24x w2)) ⊕
80 ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((gt_b8 (w24h w1) (w24h w2)) ⊕
81 ((eq_b8 (w24h w1) (w24h w2)) ⊗ (ge_b8 (w24l w1) (w24l w2))))).
86 mk_word24 (and_b8 (w24x w1) (w24x w2))
87 (and_b8 (w24h w1) (w24h w2))
88 (and_b8 (w24l w1) (w24l w2)).
93 mk_word24 (or_b8 (w24x w1) (w24x w2))
94 (or_b8 (w24h w1) (w24h w2))
95 (or_b8 (w24l w1) (w24l w2)).
100 mk_word24 (xor_b8 (w24x w1) (w24x w2))
101 (xor_b8 (w24h w1) (w24h w2))
102 (xor_b8 (w24l w1) (w24l w2)).
104 (* operatore Most Significant Bit *)
105 ndefinition getMSB_w24 ≝ λw:word24.getMSB_b8 (w24x w).
106 ndefinition setMSB_w24 ≝ λw:word24.mk_word24 (setMSB_b8 (w24x w)) (w24h w) (w24l w).
108 (* operatore Least Significant Bit *)
109 ndefinition getLSB_w24 ≝ λw:word24.getLSB_b8 (w24l w).
110 ndefinition setLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (setLSB_b8 (w24l w)).
112 (* operatore rotazione destra con carry *)
113 ndefinition rcr_w24 ≝
114 λc:bool.λw:word24.match rcr_b8 c (w24x w) with
115 [ pair c' wx' ⇒ match rcr_b8 c' (w24h w) with
116 [ pair c'' wh' ⇒ match rcr_b8 c'' (w24l w) with
117 [ pair c''' wl' ⇒ pair … c''' (mk_word24 wx' wh' wl') ]]].
119 (* operatore shift destro *)
120 ndefinition shr_w24 ≝ rcr_w24 false.
122 (* operatore rotazione destra *)
123 ndefinition ror_w24 ≝
124 λw.match shr_w24 w with
125 [ pair c w' ⇒ match c with
126 [ true ⇒ setMSB_w24 w' | false ⇒ w' ]].
128 (* operatore rotazione sinistra con carry *)
129 ndefinition rcl_w24 ≝
130 λc:bool.λw:word24.match rcl_b8 c (w24l w) with
131 [ pair c' wl' ⇒ match rcl_b8 c' (w24h w) with
132 [ pair c'' wh' ⇒ match rcl_b8 c'' (w24x w) with
133 [ pair c''' wx' ⇒ pair … c''' (mk_word24 wx' wh' wl') ]]].
135 (* operatore shift sinistro *)
136 ndefinition shl_w24 ≝ rcl_w24 false.
138 (* operatore rotazione sinistra *)
139 ndefinition rol_w24 ≝
140 λw.match shl_w24 w with
141 [ pair c w' ⇒ match c with
142 [ true ⇒ setLSB_w24 w' | false ⇒ w' ]].
144 (* operatore not/complemento a 1 *)
145 ndefinition not_w24 ≝
146 λw:word24.mk_word24 (not_b8 (w24x w)) (not_b8 (w24h w)) (not_b8 (w24l w)).
148 (* operatore somma con data+carry → data+carry *)
149 ndefinition plus_w24_dc_dc ≝
150 λc:bool.λw1,w2:word24.
151 match plus_b8_dc_dc c (w24l w1) (w24l w2) with
152 [ pair c' l ⇒ match plus_b8_dc_dc c' (w24h w1) (w24h w2) with
153 [ pair c'' h ⇒ match plus_b8_dc_dc c'' (w24x w1) (w24x w2) with
154 [ pair c''' x ⇒ pair … c''' 〈x;h;l〉 ]]].
156 (* operatore somma con data+carry → data *)
157 ndefinition plus_w24_dc_d ≝ λc,w1,w2.snd … (plus_w24_dc_dc c w1 w2).
159 (* operatore somma con data+carry → c *)
160 ndefinition plus_w24_dc_c ≝ λc,w1,w2.fst … (plus_w24_dc_dc c w1 w2).
162 (* operatore somma con data → data+carry *)
163 ndefinition plus_w24_d_dc ≝ plus_w24_dc_dc false.
165 (* operatore somma con data → data *)
166 ndefinition plus_w24_d_d ≝ λw1,w2.snd … (plus_w24_d_dc w1 w2).
168 (* operatore somma con data → c *)
169 ndefinition plus_w24_d_c ≝ λw1,w2.fst … (plus_w24_d_dc w1 w2).
171 (* operatore predecessore *)
172 ndefinition pred_w24 ≝
173 λw:word24.match eq_b8 (w24l w) 〈x0,x0〉 with
174 [ true ⇒ match eq_b8 (w24h w) 〈x0,x0〉 with
175 [ true ⇒ mk_word24 (pred_b8 (w24x w)) (pred_b8 (w24h w)) (pred_b8 (w24l w))
176 | false ⇒ mk_word24 (w24x w) (pred_b8 (w24h w)) (pred_b8 (w24l w)) ]
177 | false ⇒ mk_word24 (w24x w) (w24h w) (pred_b8 (w24l w)) ].
179 (* operatore successore *)
180 ndefinition succ_w24 ≝
181 λw:word24.match eq_b8 (w24l w) 〈xF,xF〉 with
182 [ true ⇒ match eq_b8 (w24h w) 〈xF,xF〉 with
183 [ true ⇒ mk_word24 (succ_b8 (w24x w)) (succ_b8 (w24h w)) (succ_b8 (w24l w))
184 | false ⇒ mk_word24 (w24x w) (succ_b8 (w24h w)) (succ_b8 (w24l w)) ]
185 | false ⇒ mk_word24 (w24x w) (w24h w) (succ_b8 (w24l w)) ].
187 (* operatore neg/complemento a 2 *)
188 ndefinition compl_w24 ≝
189 λw:word24.match getMSB_w24 w with
190 [ true ⇒ succ_w24 (not_w24 w)
191 | false ⇒ not_w24 (pred_w24 w) ].
193 (* operatore x in [inf,sup] o in sup],[inf *)
194 ndefinition inrange_w24 ≝
196 match le_w24 inf sup with
197 [ true ⇒ and_bool | false ⇒ or_bool ]
198 (le_w24 inf x) (le_w24 x sup).