source: extracted/byteValues.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: 10.0 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
199type beval =
200| BVundef
201| BVnonzero
202| BVXor of Pointers.pointer Types.option * Pointers.pointer Types.option
203   * part
204| BVByte of BitVector.byte
205| BVnull of part
206| BVptr of Pointers.pointer * part
207| BVpc of program_counter * part
208
209val beval_rect_Type4 :
210  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
211  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
212  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
213  beval -> 'a1
214
215val beval_rect_Type5 :
216  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
217  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
218  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
219  beval -> 'a1
220
221val beval_rect_Type3 :
222  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
223  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
224  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
225  beval -> 'a1
226
227val beval_rect_Type2 :
228  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
229  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
230  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
231  beval -> 'a1
232
233val beval_rect_Type1 :
234  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
235  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
236  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
237  beval -> 'a1
238
239val beval_rect_Type0 :
240  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
241  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
242  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
243  beval -> 'a1
244
245val beval_inv_rect_Type4 :
246  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
247  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
248  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
249  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
250
251val beval_inv_rect_Type3 :
252  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
253  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
254  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
255  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
256
257val beval_inv_rect_Type2 :
258  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
259  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
260  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
261  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
262
263val beval_inv_rect_Type1 :
264  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
265  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
266  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
267  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
268
269val beval_inv_rect_Type0 :
270  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
271  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
272  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
273  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
274
275val beval_discr : beval -> beval -> __
276
277val beval_jmdiscr : beval -> beval -> __
278
279val eq_bv_suffix :
280  Nat.nat -> Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
281  -> Bool.bool
282
283val pointer_of_bevals : beval List.list -> Pointers.pointer Errors.res
284
285val pc_of_bevals : beval List.list -> program_counter Errors.res
286
287val bevals_of_pointer : Pointers.pointer -> beval List.list
288
289val bevals_of_pc : program_counter -> beval List.list
290
291val list_to_pair : 'a1 List.list -> ('a1, 'a1) Types.prod
292
293val beval_pair_of_pointer : Pointers.pointer -> (beval, beval) Types.prod
294
295val beval_pair_of_pc : program_counter -> (beval, beval) Types.prod
296
297val bool_of_beval : beval -> Bool.bool Errors.res
298
299val byte_of_val :
300  ErrorMessages.errorMessage -> beval -> BitVector.byte Errors.res
301
302val word_of_list_beval : beval List.list -> Integers.int Errors.res
303
304type bebit =
305| BBbit of Bool.bool
306| BBundef
307| BBptrcarry of Bool.bool * Pointers.pointer * part * BitVector.bitVector
308
309val bebit_rect_Type4 :
310  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
311  BitVector.bitVector -> 'a1) -> bebit -> 'a1
312
313val bebit_rect_Type5 :
314  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
315  BitVector.bitVector -> 'a1) -> bebit -> 'a1
316
317val bebit_rect_Type3 :
318  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
319  BitVector.bitVector -> 'a1) -> bebit -> 'a1
320
321val bebit_rect_Type2 :
322  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
323  BitVector.bitVector -> 'a1) -> bebit -> 'a1
324
325val bebit_rect_Type1 :
326  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
327  BitVector.bitVector -> 'a1) -> bebit -> 'a1
328
329val bebit_rect_Type0 :
330  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
331  BitVector.bitVector -> 'a1) -> bebit -> 'a1
332
333val bebit_inv_rect_Type4 :
334  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
335  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
336
337val bebit_inv_rect_Type3 :
338  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
339  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
340
341val bebit_inv_rect_Type2 :
342  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
343  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
344
345val bebit_inv_rect_Type1 :
346  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
347  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
348
349val bebit_inv_rect_Type0 :
350  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
351  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
352
353val bebit_discr : bebit -> bebit -> __
354
355val bebit_jmdiscr : bebit -> bebit -> __
356
357val bit_of_val :
358  ErrorMessages.errorMessage -> bebit -> BitVector.bit Errors.res
359
Note: See TracBrowser for help on using the repository browser.