source: driver/extracted/arithmetic.mli @ 3106

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