]> matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/blob - extracted/arithmetic.mli
Control and copyright added.
[pkg-cerco/acc-trusted.git] / extracted / arithmetic.mli
1 open Preamble
2
3 open Setoids
4
5 open Monad
6
7 open Option
8
9 open Extranat
10
11 open Vector
12
13 open Div_and_mod
14
15 open Jmeq
16
17 open Russell
18
19 open Types
20
21 open List
22
23 open Util
24
25 open FoldStuff
26
27 open Bool
28
29 open Hints_declaration
30
31 open Core_notation
32
33 open Pts
34
35 open Logic
36
37 open Relations
38
39 open Nat
40
41 open BitVector
42
43 open Exp
44
45 val addr16_of_addr11 : BitVector.word -> BitVector.word11 -> BitVector.word
46
47 val nat_of_bool : Bool.bool -> Nat.nat
48
49 val carry_of : Bool.bool -> Bool.bool -> Bool.bool -> Bool.bool
50
51 val add_with_carries :
52   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
53   (BitVector.bitVector, BitVector.bitVector) Types.prod
54
55 val borrow_of : Bool.bool -> Bool.bool -> Bool.bool -> Bool.bool
56
57 val sub_with_borrows :
58   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
59   (BitVector.bitVector, BitVector.bitVector) Types.prod
60
61 val add_n_with_carry :
62   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
63   (BitVector.bitVector, BitVector.bitVector) Types.prod
64
65 val sub_n_with_carry :
66   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
67   (BitVector.bitVector, BitVector.bitVector) Types.prod
68
69 val add_8_with_carry :
70   BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
71   (BitVector.bitVector, BitVector.bitVector) Types.prod
72
73 val add_16_with_carry :
74   BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
75   (BitVector.bitVector, BitVector.bitVector) Types.prod
76
77 val sub_7_with_carry :
78   BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
79   (BitVector.bitVector, BitVector.bitVector) Types.prod
80
81 val sub_8_with_carry :
82   BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
83   (BitVector.bitVector, BitVector.bitVector) Types.prod
84
85 val sub_16_with_carry :
86   BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
87   (BitVector.bitVector, BitVector.bitVector) Types.prod
88
89 val increment : Nat.nat -> BitVector.bitVector -> BitVector.bitVector
90
91 val decrement : Nat.nat -> BitVector.bitVector -> BitVector.bitVector
92
93 val bitvector_of_nat_aux :
94   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
95
96 val bitvector_of_nat : Nat.nat -> Nat.nat -> BitVector.bitVector
97
98 val nat_of_bitvector_aux :
99   Nat.nat -> Nat.nat -> BitVector.bitVector -> Nat.nat
100
101 val nat_of_bitvector : Nat.nat -> BitVector.bitVector -> Nat.nat
102
103 val two_complement_negation :
104   Nat.nat -> BitVector.bitVector -> BitVector.bitVector
105
106 val addition_n :
107   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
108   BitVector.bitVector
109
110 val subtraction :
111   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
112   BitVector.bitVector
113
114 val mult_aux :
115   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
116   BitVector.bitVector -> BitVector.bitVector
117
118 val multiplication :
119   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
120   BitVector.bitVector
121
122 val short_multiplication :
123   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
124   BitVector.bitVector
125
126 type fbs_diff =
127 | Fbs_diff' of Nat.nat * Nat.nat
128
129 val fbs_diff_rect_Type4 :
130   (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1
131
132 val fbs_diff_rect_Type5 :
133   (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1
134
135 val fbs_diff_rect_Type3 :
136   (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1
137
138 val fbs_diff_rect_Type2 :
139   (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1
140
141 val fbs_diff_rect_Type1 :
142   (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1
143
144 val fbs_diff_rect_Type0 :
145   (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1
146
147 val fbs_diff_inv_rect_Type4 :
148   Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1
149
150 val fbs_diff_inv_rect_Type3 :
151   Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1
152
153 val fbs_diff_inv_rect_Type2 :
154   Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1
155
156 val fbs_diff_inv_rect_Type1 :
157   Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1
158
159 val fbs_diff_inv_rect_Type0 :
160   Nat.nat -> fbs_diff -> (Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> 'a1
161
162 val fbs_diff_discr : Nat.nat -> fbs_diff -> fbs_diff -> __
163
164 val fbs_diff_jmdiscr : Nat.nat -> fbs_diff -> fbs_diff -> __
165
166 val first_bit_set : Nat.nat -> BitVector.bitVector -> fbs_diff Types.option
167
168 val divmod_u_aux :
169   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
170   (BitVector.bitVector, BitVector.bitVector) Types.prod
171
172 val divmod_u :
173   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
174   (BitVector.bitVector, BitVector.bitVector) Types.prod Types.option
175
176 val division_u :
177   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
178   BitVector.bitVector Types.option
179
180 val division_s :
181   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
182   BitVector.bitVector Types.option
183
184 val modulus_u :
185   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
186   BitVector.bitVector Types.option
187
188 val modulus_s :
189   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
190   BitVector.bitVector Types.option
191
192 val lt_u :
193   Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool
194
195 val gt_u :
196   Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool
197
198 val lte_u :
199   Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool
200
201 val gte_u :
202   Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool
203
204 val lt_s : Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool
205
206 val gt_s : Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool
207
208 val lte_s :
209   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool
210
211 val gte_s :
212   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool
213
214 type ternary =
215 | Zero_carry
216 | One_carry
217 | Two_carry
218
219 val ternary_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1
220
221 val ternary_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1
222
223 val ternary_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1
224
225 val ternary_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1
226
227 val ternary_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1
228
229 val ternary_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> ternary -> 'a1
230
231 val ternary_inv_rect_Type4 :
232   ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
233
234 val ternary_inv_rect_Type3 :
235   ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
236
237 val ternary_inv_rect_Type2 :
238   ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
239
240 val ternary_inv_rect_Type1 :
241   ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
242
243 val ternary_inv_rect_Type0 :
244   ternary -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
245
246 val ternary_discr : ternary -> ternary -> __
247
248 val ternary_jmdiscr : ternary -> ternary -> __
249
250 val carry_0 : ternary -> (Bool.bool, ternary) Types.prod
251
252 val carry_1 : ternary -> (Bool.bool, ternary) Types.prod
253
254 val carry_2 : ternary -> (Bool.bool, ternary) Types.prod
255
256 val carry_3 : ternary -> (Bool.bool, ternary) Types.prod
257
258 val ternary_carry_of :
259   Bool.bool -> Bool.bool -> Bool.bool -> ternary -> (Bool.bool, ternary)
260   Types.prod
261
262 val canonical_add :
263   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
264   BitVector.bitVector -> ternary -> (BitVector.bitVector, ternary) Types.prod
265
266 val carries_to_ternary : Bool.bool -> Bool.bool -> ternary
267
268 val max_u :
269   Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool
270   Vector.vector
271
272 val min_u :
273   Nat.nat -> Bool.bool Vector.vector -> Bool.bool Vector.vector -> Bool.bool
274   Vector.vector
275
276 val max_s :
277   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
278   BitVector.bitVector
279
280 val min_s :
281   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
282   BitVector.bitVector
283
284 val bitvector_of_bool : Nat.nat -> Bool.bool -> BitVector.bitVector
285
286 val full_add :
287   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> BitVector.bit ->
288   (BitVector.bit, BitVector.bitVector) Types.prod
289
290 val half_add :
291   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (BitVector.bit,
292   BitVector.bitVector) Types.prod
293
294 val add :
295   Nat.nat -> BitVector.bitVector -> BitVector.bitVector ->
296   BitVector.bitVector
297
298 val sign_extension : BitVector.byte -> BitVector.word
299
300 val sign_bit : Nat.nat -> BitVector.bitVector -> Bool.bool
301
302 val sign_extend :
303   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
304
305 val zero_ext :
306   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
307
308 val sign_ext :
309   Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
310