source: extracted/arithmetic.mli @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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