source: extracted/byteValues.mli @ 2649

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

...

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 Arithmetic
34
35open Extranat
36
37open Vector
38
39open Div_and_mod
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Util
48
49open FoldStuff
50
51open BitVector
52
53open Types
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Positive
70
71open Z
72
73open BitVectorZ
74
75open Pointers
76
77open Hide
78
79type cpointer = Pointers.pointer Types.sig0
80
81type xpointer = Pointers.pointer Types.sig0
82
83type program_counter = { pc_block : Pointers.block Types.sig0;
84                         pc_offset : Positive.pos }
85
86val program_counter_rect_Type4 :
87  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
88  'a1
89
90val program_counter_rect_Type5 :
91  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
92  'a1
93
94val program_counter_rect_Type3 :
95  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
96  'a1
97
98val program_counter_rect_Type2 :
99  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
100  'a1
101
102val program_counter_rect_Type1 :
103  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
104  'a1
105
106val program_counter_rect_Type0 :
107  (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
108  'a1
109
110val pc_block : program_counter -> Pointers.block Types.sig0
111
112val pc_offset : program_counter -> Positive.pos
113
114val program_counter_inv_rect_Type4 :
115  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
116  -> 'a1
117
118val program_counter_inv_rect_Type3 :
119  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
120  -> 'a1
121
122val program_counter_inv_rect_Type2 :
123  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
124  -> 'a1
125
126val program_counter_inv_rect_Type1 :
127  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
128  -> 'a1
129
130val program_counter_inv_rect_Type0 :
131  program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ -> 'a1)
132  -> 'a1
133
134val program_counter_discr : program_counter -> program_counter -> __
135
136val program_counter_jmdiscr : program_counter -> program_counter -> __
137
138val eq_program_counter : program_counter -> program_counter -> Bool.bool
139
140val bitvector_from_pos : Nat.nat -> Positive.pos -> BitVector.bitVector
141
142val pos_from_bitvector : Nat.nat -> BitVector.bitVector -> Positive.pos
143
144val cpointer_of_pc : program_counter -> cpointer Types.option
145
146type part =
147  Nat.nat
148  (* singleton inductive, whose constructor was mk_part *)
149
150val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
151
152val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
153
154val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
155
156val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
157
158val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
159
160val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1
161
162val part_no : part -> Nat.nat
163
164val part_inv_rect_Type4 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
165
166val part_inv_rect_Type3 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
167
168val part_inv_rect_Type2 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
169
170val part_inv_rect_Type1 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
171
172val part_inv_rect_Type0 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1
173
174val part_discr : part -> part -> __
175
176val part_jmdiscr : part -> part -> __
177
178val dpi1__o__part_no__o__inject :
179  (part, 'a1) Types.dPair -> Nat.nat Types.sig0
180
181val dpi1__o__part_no__o__Z_of_nat : (part, 'a1) Types.dPair -> Z.z
182
183val eject__o__part_no__o__inject : part Types.sig0 -> Nat.nat Types.sig0
184
185val eject__o__part_no__o__Z_of_nat : part Types.sig0 -> Z.z
186
187val part_no__o__Z_of_nat : part -> Z.z
188
189val part_no__o__inject : part -> Nat.nat Types.sig0
190
191val dpi1__o__part_no : (part, 'a1) Types.dPair -> Nat.nat
192
193val eject__o__part_no : part Types.sig0 -> Nat.nat
194
195val part_from_sig : Nat.nat Types.sig0 -> part
196
197type beval =
198| BVundef
199| BVnonzero
200| BVXor of Pointers.pointer Types.option * Pointers.pointer Types.option
201   * part
202| BVByte of BitVector.byte
203| BVnull of part
204| BVptr of Pointers.pointer * part
205| BVpc of program_counter * part
206
207val beval_rect_Type4 :
208  'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
209  Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1) ->
210  (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1) ->
211  beval -> 'a1
212
213val beval_rect_Type5 :
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_Type3 :
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_Type2 :
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_Type1 :
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_Type0 :
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_inv_rect_Type4 :
244  beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
245  Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
246  __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
247  'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1
248
249val beval_inv_rect_Type3 :
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_Type2 :
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_Type1 :
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_Type0 :
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_discr : beval -> beval -> __
274
275val beval_jmdiscr : beval -> beval -> __
276
277val eq_bv_suffix :
278  Nat.nat -> Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
279  -> Bool.bool
280
281val pointer_of_bevals : beval List.list -> Pointers.pointer Errors.res
282
283val pc_of_bevals : beval List.list -> program_counter Errors.res
284
285val bevals_of_pointer : Pointers.pointer -> beval List.list
286
287val bevals_of_pc : program_counter -> beval List.list
288
289val list_to_pair : 'a1 List.list -> ('a1, 'a1) Types.prod
290
291val beval_pair_of_pointer : Pointers.pointer -> (beval, beval) Types.prod
292
293val beval_pair_of_pc : program_counter -> (beval, beval) Types.prod
294
295val bool_of_beval : beval -> Bool.bool Errors.res
296
297val byte_of_val :
298  ErrorMessages.errorMessage -> beval -> BitVector.byte Errors.res
299
300val word_of_list_beval : beval List.list -> Integers.int Errors.res
301
302type bebit =
303| BBbit of Bool.bool
304| BBundef
305| BBptrcarry of Bool.bool * Pointers.pointer * part * BitVector.bitVector
306
307val bebit_rect_Type4 :
308  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
309  BitVector.bitVector -> 'a1) -> bebit -> 'a1
310
311val bebit_rect_Type5 :
312  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
313  BitVector.bitVector -> 'a1) -> bebit -> 'a1
314
315val bebit_rect_Type3 :
316  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
317  BitVector.bitVector -> 'a1) -> bebit -> 'a1
318
319val bebit_rect_Type2 :
320  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
321  BitVector.bitVector -> 'a1) -> bebit -> 'a1
322
323val bebit_rect_Type1 :
324  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
325  BitVector.bitVector -> 'a1) -> bebit -> 'a1
326
327val bebit_rect_Type0 :
328  (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
329  BitVector.bitVector -> 'a1) -> bebit -> 'a1
330
331val bebit_inv_rect_Type4 :
332  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
333  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
334
335val bebit_inv_rect_Type3 :
336  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
337  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
338
339val bebit_inv_rect_Type2 :
340  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
341  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
342
343val bebit_inv_rect_Type1 :
344  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
345  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
346
347val bebit_inv_rect_Type0 :
348  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
349  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
350
351val bebit_discr : bebit -> bebit -> __
352
353val bebit_jmdiscr : bebit -> bebit -> __
354
355val bit_of_val :
356  ErrorMessages.errorMessage -> bebit -> BitVector.bit Errors.res
357
Note: See TracBrowser for help on using the repository browser.