source: extracted/byteValues.mli @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 12.8 KB
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open ErrorMessages
10
11open PreIdentifiers
12
13open Errors
14
15open Extralib
16
17open Setoids
18
19open Monad
20
21open Option
22
23open Lists
24
25open Identifiers
26
27open Integers
28
29open AST
30
31open Division
32
33open Exp
34
35open Arithmetic
36
37open Extranat
38
39open Vector
40
41open Div_and_mod
42
43open Jmeq
44
45open Russell
46
47open List
48
49open Util
50
51open FoldStuff
52
53open BitVector
54
55open Types
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Positive
72
73open Z
74
75open BitVectorZ
76
77open Pointers
78
79open Hide
80
81type cpointer = Pointers.pointer Types.sig0
82
83type xpointer = Pointers.pointer Types.sig0
84
85type program_counter = { pc_block : Pointers.block Types.sig0;
86                         pc_offset : Positive.pos }
87
88val program_counter_rect_Type4 :
89  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
90  'a1
91
92val program_counter_rect_Type5 :
93  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
94  'a1
95
96val program_counter_rect_Type3 :
97  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
98  'a1
99
100val program_counter_rect_Type2 :
101  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
102  'a1
103
104val program_counter_rect_Type1 :
105  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
106  'a1
107
108val program_counter_rect_Type0 :
109  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
110  'a1
111
112val pc_block : program_counter -> Pointers.block Types.sig0
113
114val pc_offset : program_counter -> Positive.pos
115
116val program_counter_inv_rect_Type4 :
117  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
118  -> 'a1
119
120val program_counter_inv_rect_Type3 :
121  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
122  -> 'a1
123
124val program_counter_inv_rect_Type2 :
125  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
126  -> 'a1
127
128val program_counter_inv_rect_Type1 :
129  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
130  -> 'a1
131
132val program_counter_inv_rect_Type0 :
133  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
134  -> 'a1
135
136val program_counter_discr : program_counter -> program_counter -> __
137
138val program_counter_jmdiscr : program_counter -> program_counter -> __
139
140val eq_program_counter : program_counter -> program_counter -> Bool.bool
141
142val bitvector_from_pos : Nat.nat -> Positive.pos -> BitVector.bitVector
143
144val pos_from_bitvector : Nat.nat -> BitVector.bitVector -> Positive.pos
145
146val cpointer_of_pc : program_counter -> cpointer Types.option
147
148type part =
149  Nat.nat
150  (* singleton inductive, whose constructor was mk_part *)
151
152val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
153
154val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
155
156val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
157
158val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
159
160val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
161
162val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
163
164val part_no : part -> Nat.nat
165
166val part_inv_rect_Type4 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
167
168val part_inv_rect_Type3 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
169
170val part_inv_rect_Type2 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
171
172val part_inv_rect_Type1 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
173
174val part_inv_rect_Type0 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
175
176val part_discr : part -> part -> __
177
178val part_jmdiscr : part -> part -> __
179
180val dpi1__o__part_no__o__inject :
181  (part, 'a1) Types.dPair -> Nat.nat Types.sig0
182
183val dpi1__o__part_no__o__Z_of_nat : (part, 'a1) Types.dPair -> Z.z
184
185val eject__o__part_no__o__inject : part Types.sig0 -> Nat.nat Types.sig0
186
187val eject__o__part_no__o__Z_of_nat : part Types.sig0 -> Z.z
188
189val part_no__o__Z_of_nat : part -> Z.z
190
191val part_no__o__inject : part -> Nat.nat Types.sig0
192
193val dpi1__o__part_no : (part, 'a1) Types.dPair -> Nat.nat
194
195val eject__o__part_no : part Types.sig0 -> Nat.nat
196
197val part_from_sig : Nat.nat Types.sig0 -> part
198
199val dpi1__o__part_no__o__inject__o__sig_to_part__o__inject :
200  (part, 'a1) Types.dPair -> part Types.sig0
201
202val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
203  (part, 'a1) Types.dPair -> Nat.nat Types.sig0
204
205val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
206  (part, 'a1) Types.dPair -> Z.z
207
208val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no :
209  (part, 'a1) Types.dPair -> Nat.nat
210
211val eject__o__part_no__o__inject__o__sig_to_part__o__inject :
212  part Types.sig0 -> part Types.sig0
213
214val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
215  part Types.sig0 -> Nat.nat Types.sig0
216
217val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
218  part Types.sig0 -> Z.z
219
220val eject__o__part_no__o__inject__o__sig_to_part__o__part_no :
221  part Types.sig0 -> Nat.nat
222
223val inject__o__sig_to_part__o__inject : Nat.nat -> part Types.sig0
224
225val inject__o__sig_to_part__o__part_no__o__inject :
226  Nat.nat -> Nat.nat Types.sig0
227
228val inject__o__sig_to_part__o__part_no__o__Z_of_nat : Nat.nat -> Z.z
229
230val inject__o__sig_to_part__o__part_no : Nat.nat -> Nat.nat
231
232val part_no__o__inject__o__sig_to_part__o__inject : part -> part Types.sig0
233
234val part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
235  part -> Nat.nat Types.sig0
236
237val part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat : part -> Z.z
238
239val part_no__o__inject__o__sig_to_part__o__part_no : part -> Nat.nat
240
241val dpi1__o__sig_to_part__o__inject :
242  (Nat.nat Types.sig0, 'a1) Types.dPair -> part Types.sig0
243
244val dpi1__o__sig_to_part__o__part_no__o__inject :
245  (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat Types.sig0
246
247val dpi1__o__sig_to_part__o__part_no__o__Z_of_nat :
248  (Nat.nat Types.sig0, 'a1) Types.dPair -> Z.z
249
250val dpi1__o__sig_to_part__o__part_no :
251  (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat
252
253val eject__o__sig_to_part__o__inject :
254  Nat.nat Types.sig0 Types.sig0 -> part Types.sig0
255
256val eject__o__sig_to_part__o__part_no__o__inject :
257  Nat.nat Types.sig0 Types.sig0 -> Nat.nat Types.sig0
258
259val eject__o__sig_to_part__o__part_no__o__Z_of_nat :
260  Nat.nat Types.sig0 Types.sig0 -> Z.z
261
262val eject__o__sig_to_part__o__part_no :
263  Nat.nat Types.sig0 Types.sig0 -> Nat.nat
264
265val sig_to_part__o__part_no : Nat.nat Types.sig0 -> Nat.nat
266
267val sig_to_part__o__part_no__o__Z_of_nat : Nat.nat Types.sig0 -> Z.z
268
269val sig_to_part__o__part_no__o__inject :
270  Nat.nat Types.sig0 -> Nat.nat Types.sig0
271
272val sig_to_part__o__inject : Nat.nat Types.sig0 -> part Types.sig0
273
274val dpi1__o__part_no__o__inject__o__sig_to_part :
275  (part, 'a1) Types.dPair -> part
276
277val eject__o__part_no__o__inject__o__sig_to_part : part Types.sig0 -> part
278
279val inject__o__sig_to_part : Nat.nat -> part
280
281val part_no__o__inject__o__sig_to_part : part -> part
282
283val dpi1__o__sig_to_part : (Nat.nat Types.sig0, 'a1) Types.dPair -> part
284
285val eject__o__sig_to_part : Nat.nat Types.sig0 Types.sig0 -> part
286
287type beval =
288| BVundef
289| BVnonzero
290| BVXor of Pointers.pointer Types.option * Pointers.pointer Types.option
291   * part
292| BVByte of BitVector.byte
293| BVnull of part
294| BVptr of Pointers.pointer * part
295| BVpc of program_counter * part
296
297val beval_rect_Type4 :
298  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
299  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
300  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
301  beval -> 'a1
302
303val beval_rect_Type5 :
304  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
305  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
306  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
307  beval -> 'a1
308
309val beval_rect_Type3 :
310  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
311  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
312  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
313  beval -> 'a1
314
315val beval_rect_Type2 :
316  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
317  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
318  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
319  beval -> 'a1
320
321val beval_rect_Type1 :
322  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
323  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
324  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
325  beval -> 'a1
326
327val beval_rect_Type0 :
328  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
329  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
330  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
331  beval -> 'a1
332
333val beval_inv_rect_Type4 :
334  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
335  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
336  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
337  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
338
339val beval_inv_rect_Type3 :
340  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
341  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
342  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
343  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
344
345val beval_inv_rect_Type2 :
346  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
347  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
348  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
349  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
350
351val beval_inv_rect_Type1 :
352  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
353  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
354  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
355  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
356
357val beval_inv_rect_Type0 :
358  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
359  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
360  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
361  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
362
363val beval_discr : beval -> beval -> __
364
365val beval_jmdiscr : beval -> beval -> __
366
367val eq_bv_suffix :
368  Nat.nat -> Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
369  -> Bool.bool
370
371val pointer_of_bevals : beval List.list -> Pointers.pointer Errors.res
372
373val pc_of_bevals : beval List.list -> program_counter Errors.res
374
375val bevals_of_pointer : Pointers.pointer -> beval List.list
376
377val bevals_of_pc : program_counter -> beval List.list
378
379val list_to_pair : 'a1 List.list -> ('a1, 'a1) Types.prod
380
381val beval_pair_of_pointer : Pointers.pointer -> (beval, beval) Types.prod
382
383val beval_pair_of_pc : program_counter -> (beval, beval) Types.prod
384
385val bool_of_beval : beval -> Bool.bool Errors.res
386
387val byte_of_val :
388  ErrorMessages.errorMessage -> beval -> BitVector.byte Errors.res
389
390val word_of_list_beval : beval List.list -> Integers.int Errors.res
391
392type bebit =
393| BBbit of Bool.bool
394| BBundef
395| BBptrcarry of Bool.bool * Pointers.pointer * part * BitVector.bitVector
396
397val bebit_rect_Type4 :
398  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
399  BitVector.bitVector -> 'a1) -> bebit -> 'a1
400
401val bebit_rect_Type5 :
402  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
403  BitVector.bitVector -> 'a1) -> bebit -> 'a1
404
405val bebit_rect_Type3 :
406  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
407  BitVector.bitVector -> 'a1) -> bebit -> 'a1
408
409val bebit_rect_Type2 :
410  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
411  BitVector.bitVector -> 'a1) -> bebit -> 'a1
412
413val bebit_rect_Type1 :
414  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
415  BitVector.bitVector -> 'a1) -> bebit -> 'a1
416
417val bebit_rect_Type0 :
418  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
419  BitVector.bitVector -> 'a1) -> bebit -> 'a1
420
421val bebit_inv_rect_Type4 :
422  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
423  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
424
425val bebit_inv_rect_Type3 :
426  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
427  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
428
429val bebit_inv_rect_Type2 :
430  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
431  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
432
433val bebit_inv_rect_Type1 :
434  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
435  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
436
437val bebit_inv_rect_Type0 :
438  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
439  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
440
441val bebit_discr : bebit -> bebit -> __
442
443val bebit_jmdiscr : bebit -> bebit -> __
444
445val bit_of_val :
446  ErrorMessages.errorMessage -> bebit -> BitVector.bit Errors.res
447
Note: See TracBrowser for help on using the repository browser.