source: extracted/byteValues.mli @ 2933

Last change on this file since 2933 was 2933, checked in by sacerdot, 6 years ago

New extraction, several bug fixed. RTL_semantics fixed by hand, will be fixed
automatically when Paolo commits.

File size: 13.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 Lists
18
19open Identifiers
20
21open Integers
22
23open AST
24
25open Division
26
27open Exp
28
29open Arithmetic
30
31open Setoids
32
33open Monad
34
35open Option
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 add_or_sub =
393| Do_add
394| Do_sub
395
396val add_or_sub_rect_Type4 : 'a1 -> 'a1 -> add_or_sub -> 'a1
397
398val add_or_sub_rect_Type5 : 'a1 -> 'a1 -> add_or_sub -> 'a1
399
400val add_or_sub_rect_Type3 : 'a1 -> 'a1 -> add_or_sub -> 'a1
401
402val add_or_sub_rect_Type2 : 'a1 -> 'a1 -> add_or_sub -> 'a1
403
404val add_or_sub_rect_Type1 : 'a1 -> 'a1 -> add_or_sub -> 'a1
405
406val add_or_sub_rect_Type0 : 'a1 -> 'a1 -> add_or_sub -> 'a1
407
408val add_or_sub_inv_rect_Type4 :
409  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
410
411val add_or_sub_inv_rect_Type3 :
412  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
413
414val add_or_sub_inv_rect_Type2 :
415  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
416
417val add_or_sub_inv_rect_Type1 :
418  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
419
420val add_or_sub_inv_rect_Type0 :
421  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
422
423val add_or_sub_discr : add_or_sub -> add_or_sub -> __
424
425val add_or_sub_jmdiscr : add_or_sub -> add_or_sub -> __
426
427val eq_add_or_sub : add_or_sub -> add_or_sub -> Bool.bool
428
429type bebit =
430| BBbit of Bool.bool
431| BBundef
432| BBptrcarry of add_or_sub * Pointers.pointer * part * BitVector.bitVector
433
434val bebit_rect_Type4 :
435  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
436  BitVector.bitVector -> 'a1) -> bebit -> 'a1
437
438val bebit_rect_Type5 :
439  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
440  BitVector.bitVector -> 'a1) -> bebit -> 'a1
441
442val bebit_rect_Type3 :
443  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
444  BitVector.bitVector -> 'a1) -> bebit -> 'a1
445
446val bebit_rect_Type2 :
447  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
448  BitVector.bitVector -> 'a1) -> bebit -> 'a1
449
450val bebit_rect_Type1 :
451  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
452  BitVector.bitVector -> 'a1) -> bebit -> 'a1
453
454val bebit_rect_Type0 :
455  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
456  BitVector.bitVector -> 'a1) -> bebit -> 'a1
457
458val bebit_inv_rect_Type4 :
459  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
460  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
461
462val bebit_inv_rect_Type3 :
463  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
464  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
465
466val bebit_inv_rect_Type2 :
467  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
468  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
469
470val bebit_inv_rect_Type1 :
471  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
472  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
473
474val bebit_inv_rect_Type0 :
475  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
476  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
477
478val bebit_discr : bebit -> bebit -> __
479
480val bebit_jmdiscr : bebit -> bebit -> __
481
482val bit_of_val :
483  ErrorMessages.errorMessage -> bebit -> BitVector.bit Errors.res
484
Note: See TracBrowser for help on using the repository browser.