]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/num/word24.ma
mod change (-x)
[helm.git] / matita / matita / contribs / ng_assembly / num / word24.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "num/byte8.ma".
24
25 (* ********* *)
26 (* BYTE+WORD *)
27 (* ********* *)
28
29 nrecord word24 : Type ≝
30  {
31  w24x: byte8;
32  w24h: byte8;
33  w24l: byte8
34  }.
35
36 (* \langle \rangle *)
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).
40
41 (* iteratore sulle word *)
42 ndefinition forall_w24 ≝
43  λP.
44   forall_b8 (λbx.
45   forall_b8 (λbh.
46   forall_b8 (λbl.
47    P (mk_word24 bx bh bl )))).
48
49 (* operatore = *)
50 ndefinition eq_w24 ≝
51 λw1,w2.(eq_b8 (w24x w1) (w24x w2)) ⊗
52        (eq_b8 (w24h w1) (w24h w2)) ⊗
53        (eq_b8 (w24l w1) (w24l w2)).
54
55 (* operatore < *)
56 ndefinition lt_w24 ≝
57 λw1,w2:word24.
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))))).
61
62 (* operatore ≤ *)
63 ndefinition le_w24 ≝
64 λw1,w2:word24.
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))))).
68
69 (* operatore > *)
70 ndefinition gt_w24 ≝
71 λw1,w2:word24.
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))))).
75
76 (* operatore ≥ *)
77 ndefinition ge_w24 ≝
78 λw1,w2:word24.
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))))).
82
83 (* operatore and *)
84 ndefinition and_w24 ≝
85 λw1,w2:word24.
86  mk_word24 (and_b8 (w24x w1) (w24x w2))
87            (and_b8 (w24h w1) (w24h w2))
88            (and_b8 (w24l w1) (w24l w2)).
89
90 (* operatore or *)
91 ndefinition or_w24 ≝
92 λw1,w2:word24.
93  mk_word24 (or_b8 (w24x w1) (w24x w2))
94            (or_b8 (w24h w1) (w24h w2))
95            (or_b8 (w24l w1) (w24l w2)).
96
97 (* operatore xor *)
98 ndefinition xor_w24 ≝
99 λw1,w2:word24.
100  mk_word24 (xor_b8 (w24x w1) (w24x w2))
101            (xor_b8 (w24h w1) (w24h w2))
102            (xor_b8 (w24l w1) (w24l w2)).
103
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).
107 ndefinition clrMSB_w24 ≝ λw:word24.mk_word24 (clrMSB_b8 (w24x w)) (w24h w) (w24l w).
108
109 (* operatore Least Significant Bit *)
110 ndefinition getLSB_w24 ≝ λw:word24.getLSB_b8 (w24l w).
111 ndefinition setLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (setLSB_b8 (w24l w)).
112 ndefinition clrLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (clrLSB_b8 (w24l w)).
113
114 (* operatore rotazione destra con carry *)
115 ndefinition rcr_w24 ≝
116 λc:bool.λw:word24.match rcr_b8 c (w24x w) with
117  [ pair c' wx' ⇒ match rcr_b8 c' (w24h w) with
118   [ pair c'' wh' ⇒ match rcr_b8 c'' (w24l w) with
119    [ pair c''' wl' ⇒ pair … c''' (mk_word24 wx' wh' wl') ]]]. 
120
121 (* operatore shift destro *)
122 ndefinition shr_w24 ≝ rcr_w24 false.
123
124 (* operatore rotazione destra *)
125 ndefinition ror_w24 ≝
126 λw.match shr_w24 w with
127  [ pair c w' ⇒ match c with
128   [ true ⇒ setMSB_w24 w' | false ⇒ w' ]].
129
130 (* operatore rotazione sinistra con carry *)
131 ndefinition rcl_w24 ≝
132 λc:bool.λw:word24.match rcl_b8 c (w24l w) with
133  [ pair c' wl' ⇒ match rcl_b8 c' (w24h w) with
134   [ pair c'' wh' ⇒ match rcl_b8 c'' (w24x w) with
135    [ pair c''' wx' ⇒ pair … c''' (mk_word24 wx' wh' wl') ]]].
136
137 (* operatore shift sinistro *)
138 ndefinition shl_w24 ≝ rcl_w24 false.
139
140 (* operatore rotazione sinistra *)
141 ndefinition rol_w24 ≝
142 λw.match shl_w24 w with
143  [ pair c w' ⇒ match c with
144   [ true ⇒ setLSB_w24 w' | false ⇒ w' ]].
145
146 (* operatore not/complemento a 1 *)
147 ndefinition not_w24 ≝
148 λw:word24.mk_word24 (not_b8 (w24x w)) (not_b8 (w24h w)) (not_b8 (w24l w)).
149
150 (* operatore somma con data+carry → data+carry *)
151 ndefinition plus_w24_dc_dc ≝
152 λc:bool.λw1,w2:word24.
153  match plus_b8_dc_dc c (w24l w1) (w24l w2) with
154   [ pair c' l ⇒ match plus_b8_dc_dc c' (w24h w1) (w24h w2) with
155    [ pair c'' h ⇒ match plus_b8_dc_dc c'' (w24x w1) (w24x w2) with
156     [ pair c''' x ⇒ pair … c''' 〈x;h;l〉 ]]].
157
158 (* operatore somma con data+carry → data *)
159 ndefinition plus_w24_dc_d ≝ λc,w1,w2.snd … (plus_w24_dc_dc c w1 w2).
160
161 (* operatore somma con data+carry → c *)
162 ndefinition plus_w24_dc_c ≝ λc,w1,w2.fst … (plus_w24_dc_dc c w1 w2).
163
164 (* operatore somma con data → data+carry *)
165 ndefinition plus_w24_d_dc ≝ plus_w24_dc_dc false.
166
167 (* operatore somma con data → data *)
168 ndefinition plus_w24_d_d ≝ λw1,w2.snd … (plus_w24_d_dc w1 w2).
169
170 (* operatore somma con data → c *)
171 ndefinition plus_w24_d_c ≝ λw1,w2.fst … (plus_w24_d_dc w1 w2).
172
173 (* operatore predecessore *)
174 ndefinition pred_w24 ≝
175 λw:word24.match eq_b8 (w24l w) 〈x0,x0〉 with
176  [ true ⇒ match eq_b8 (w24h w) 〈x0,x0〉 with
177   [ true ⇒ mk_word24 (pred_b8 (w24x w)) (pred_b8 (w24h w)) (pred_b8 (w24l w))
178   | false ⇒ mk_word24 (w24x w) (pred_b8 (w24h w)) (pred_b8 (w24l w)) ]
179  | false ⇒ mk_word24 (w24x w) (w24h w) (pred_b8 (w24l w)) ].
180
181 (* operatore successore *)
182 ndefinition succ_w24 ≝
183 λw:word24.match eq_b8 (w24l w) 〈xF,xF〉 with
184  [ true ⇒ match eq_b8 (w24h w) 〈xF,xF〉 with
185   [ true ⇒ mk_word24 (succ_b8 (w24x w)) (succ_b8 (w24h w)) (succ_b8 (w24l w))
186   | false ⇒ mk_word24 (w24x w) (succ_b8 (w24h w)) (succ_b8 (w24l w)) ]
187  | false ⇒ mk_word24 (w24x w) (w24h w) (succ_b8 (w24l w)) ].
188
189 (* operatore neg/complemento a 2 *)
190 ndefinition compl_w24 ≝
191 λw:word24.match getMSB_w24 w with
192  [ true ⇒ succ_w24 (not_w24 w)
193  | false ⇒ not_w24 (pred_w24 w) ].
194
195 (* operatore abs *)
196 ndefinition abs_w24 ≝
197 λw:word24.match getMSB_w24 w with
198  [ true ⇒ compl_w24 w | false ⇒ w ].
199
200 (* operatore x in [inf,sup] o in sup],[inf *)
201 ndefinition inrange_w24 ≝
202 λx,inf,sup:word24.
203  match le_w24 inf sup with
204   [ true ⇒ and_bool | false ⇒ or_bool ]
205  (le_w24 inf x) (le_w24 x sup).