source: extracted/byteValues.mli @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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