source: extracted/arithmetic.mli @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 7 years ago

...

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