source: extracted/aST.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: 20.1 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Arithmetic
14
15open Char
16
17open String
18
19open Vector
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open List
28
29open Util
30
31open FoldStuff
32
33open BitVector
34
35open Extranat
36
37open Bool
38
39open Relations
40
41open Nat
42
43open Integers
44
45open Coqlib
46
47open Floats
48
49open Proper
50
51open PositiveMap
52
53open Deqsets
54
55open PreIdentifiers
56
57open Errors
58
59open Extralib
60
61open Setoids
62
63open Monad
64
65open Option
66
67open Lists
68
69open Positive
70
71open Identifiers
72
73val symbolTag : String.string
74
75type ident = PreIdentifiers.identifier
76
77val ident_eq : ident -> ident -> (__, __) Types.sum
78
79val ident_of_nat : Nat.nat -> ident
80
81type region =
82| XData
83| Code
84
85val region_rect_Type4 : 'a1 -> 'a1 -> region -> 'a1
86
87val region_rect_Type5 : 'a1 -> 'a1 -> region -> 'a1
88
89val region_rect_Type3 : 'a1 -> 'a1 -> region -> 'a1
90
91val region_rect_Type2 : 'a1 -> 'a1 -> region -> 'a1
92
93val region_rect_Type1 : 'a1 -> 'a1 -> region -> 'a1
94
95val region_rect_Type0 : 'a1 -> 'a1 -> region -> 'a1
96
97val region_inv_rect_Type4 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
98
99val region_inv_rect_Type3 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
100
101val region_inv_rect_Type2 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
102
103val region_inv_rect_Type1 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
104
105val region_inv_rect_Type0 : region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
106
107val region_discr : region -> region -> __
108
109val region_jmdiscr : region -> region -> __
110
111val eq_region : region -> region -> Bool.bool
112
113val eq_region_elim : region -> region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
114
115val eq_region_dec : region -> region -> (__, __) Types.sum
116
117val size_pointer : Nat.nat
118
119type signedness =
120| Signed
121| Unsigned
122
123val signedness_rect_Type4 : 'a1 -> 'a1 -> signedness -> 'a1
124
125val signedness_rect_Type5 : 'a1 -> 'a1 -> signedness -> 'a1
126
127val signedness_rect_Type3 : 'a1 -> 'a1 -> signedness -> 'a1
128
129val signedness_rect_Type2 : 'a1 -> 'a1 -> signedness -> 'a1
130
131val signedness_rect_Type1 : 'a1 -> 'a1 -> signedness -> 'a1
132
133val signedness_rect_Type0 : 'a1 -> 'a1 -> signedness -> 'a1
134
135val signedness_inv_rect_Type4 :
136  signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
137
138val signedness_inv_rect_Type3 :
139  signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
140
141val signedness_inv_rect_Type2 :
142  signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
143
144val signedness_inv_rect_Type1 :
145  signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
146
147val signedness_inv_rect_Type0 :
148  signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
149
150val signedness_discr : signedness -> signedness -> __
151
152val signedness_jmdiscr : signedness -> signedness -> __
153
154type intsize =
155| I8
156| I16
157| I32
158
159val intsize_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1
160
161val intsize_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1
162
163val intsize_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1
164
165val intsize_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1
166
167val intsize_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1
168
169val intsize_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1
170
171val intsize_inv_rect_Type4 :
172  intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
173
174val intsize_inv_rect_Type3 :
175  intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
176
177val intsize_inv_rect_Type2 :
178  intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
179
180val intsize_inv_rect_Type1 :
181  intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
182
183val intsize_inv_rect_Type0 :
184  intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
185
186val intsize_discr : intsize -> intsize -> __
187
188val intsize_jmdiscr : intsize -> intsize -> __
189
190type floatsize =
191| F32
192| F64
193
194val floatsize_rect_Type4 : 'a1 -> 'a1 -> floatsize -> 'a1
195
196val floatsize_rect_Type5 : 'a1 -> 'a1 -> floatsize -> 'a1
197
198val floatsize_rect_Type3 : 'a1 -> 'a1 -> floatsize -> 'a1
199
200val floatsize_rect_Type2 : 'a1 -> 'a1 -> floatsize -> 'a1
201
202val floatsize_rect_Type1 : 'a1 -> 'a1 -> floatsize -> 'a1
203
204val floatsize_rect_Type0 : 'a1 -> 'a1 -> floatsize -> 'a1
205
206val floatsize_inv_rect_Type4 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
207
208val floatsize_inv_rect_Type3 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
209
210val floatsize_inv_rect_Type2 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
211
212val floatsize_inv_rect_Type1 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
213
214val floatsize_inv_rect_Type0 : floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
215
216val floatsize_discr : floatsize -> floatsize -> __
217
218val floatsize_jmdiscr : floatsize -> floatsize -> __
219
220type typ =
221| ASTint of intsize * signedness
222| ASTptr
223
224val typ_rect_Type4 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1
225
226val typ_rect_Type5 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1
227
228val typ_rect_Type3 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1
229
230val typ_rect_Type2 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1
231
232val typ_rect_Type1 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1
233
234val typ_rect_Type0 : (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1
235
236val typ_inv_rect_Type4 :
237  typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
238
239val typ_inv_rect_Type3 :
240  typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
241
242val typ_inv_rect_Type2 :
243  typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
244
245val typ_inv_rect_Type1 :
246  typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
247
248val typ_inv_rect_Type0 :
249  typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
250
251val typ_discr : typ -> typ -> __
252
253val typ_jmdiscr : typ -> typ -> __
254
255type sigType = typ
256
257val sigType_Int : typ
258
259val sigType_Ptr : typ
260
261val pred_size_intsize : intsize -> Nat.nat
262
263val size_intsize : intsize -> Nat.nat
264
265val bitsize_of_intsize : intsize -> Nat.nat
266
267val eq_intsize : intsize -> intsize -> Bool.bool
268
269val eq_intsize_elim : intsize -> intsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
270
271val signedness_check : signedness -> signedness -> 'a1 -> 'a1 -> 'a1
272
273val inttyp_eq_elim' :
274  intsize -> intsize -> signedness -> signedness -> 'a1 -> 'a1 -> 'a1
275
276val intsize_eq_elim' : intsize -> intsize -> 'a1 -> 'a1 -> 'a1
277
278val intsize_eq_elim : intsize -> intsize -> 'a2 -> ('a2 -> 'a1) -> 'a1 -> 'a1
279
280val intsize_eq_elim_elim :
281  intsize -> intsize -> 'a2 -> ('a2 -> 'a1) -> 'a1 -> (__ -> 'a3) -> (__ ->
282  __) -> 'a3
283
284type bvint = BitVector.bitVector
285
286val repr0 : intsize -> Nat.nat -> bvint
287
288val size_floatsize : floatsize -> Nat.nat
289
290val floatsize_eq_elim : floatsize -> floatsize -> 'a1 -> 'a1 -> 'a1
291
292val typesize : typ -> Nat.nat
293
294val typ_eq : typ -> typ -> (__, __) Types.sum
295
296val opt_typ_eq : typ Types.option -> typ Types.option -> (__, __) Types.sum
297
298type signature = { sig_args : typ List.list; sig_res : typ Types.option }
299
300val signature_rect_Type4 :
301  (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1
302
303val signature_rect_Type5 :
304  (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1
305
306val signature_rect_Type3 :
307  (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1
308
309val signature_rect_Type2 :
310  (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1
311
312val signature_rect_Type1 :
313  (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1
314
315val signature_rect_Type0 :
316  (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1
317
318val sig_args : signature -> typ List.list
319
320val sig_res : signature -> typ Types.option
321
322val signature_inv_rect_Type4 :
323  signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1
324
325val signature_inv_rect_Type3 :
326  signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1
327
328val signature_inv_rect_Type2 :
329  signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1
330
331val signature_inv_rect_Type1 :
332  signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1
333
334val signature_inv_rect_Type0 :
335  signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1
336
337val signature_discr : signature -> signature -> __
338
339val signature_jmdiscr : signature -> signature -> __
340
341type signature0 = signature
342
343val signature_args : signature -> typ List.list
344
345val signature_return : signature -> typ Types.option
346
347val proj_sig_res : signature -> typ
348
349type init_data =
350| Init_int8 of bvint
351| Init_int16 of bvint
352| Init_int32 of bvint
353| Init_float32 of Floats.float
354| Init_float64 of Floats.float
355| Init_space of Nat.nat
356| Init_null
357| Init_addrof of ident * Nat.nat
358
359val init_data_rect_Type4 :
360  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float -> 'a1)
361  -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident -> Nat.nat ->
362  'a1) -> init_data -> 'a1
363
364val init_data_rect_Type5 :
365  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float -> 'a1)
366  -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident -> Nat.nat ->
367  'a1) -> init_data -> 'a1
368
369val init_data_rect_Type3 :
370  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float -> 'a1)
371  -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident -> Nat.nat ->
372  'a1) -> init_data -> 'a1
373
374val init_data_rect_Type2 :
375  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float -> 'a1)
376  -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident -> Nat.nat ->
377  'a1) -> init_data -> 'a1
378
379val init_data_rect_Type1 :
380  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float -> 'a1)
381  -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident -> Nat.nat ->
382  'a1) -> init_data -> 'a1
383
384val init_data_rect_Type0 :
385  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float -> 'a1)
386  -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident -> Nat.nat ->
387  'a1) -> init_data -> 'a1
388
389val init_data_inv_rect_Type4 :
390  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
391  -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
392  (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1) ->
393  'a1
394
395val init_data_inv_rect_Type3 :
396  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
397  -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
398  (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1) ->
399  'a1
400
401val init_data_inv_rect_Type2 :
402  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
403  -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
404  (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1) ->
405  'a1
406
407val init_data_inv_rect_Type1 :
408  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
409  -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
410  (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1) ->
411  'a1
412
413val init_data_inv_rect_Type0 :
414  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
415  -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
416  (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1) ->
417  'a1
418
419val init_data_discr : init_data -> init_data -> __
420
421val init_data_jmdiscr : init_data -> init_data -> __
422
423type ('f, 'v) program = { prog_vars : ((ident, region) Types.prod, 'v)
424                                      Types.prod List.list;
425                          prog_funct : (ident, 'f) Types.prod List.list;
426                          prog_main : ident }
427
428val program_rect_Type4 :
429  (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
430  Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3
431
432val program_rect_Type5 :
433  (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
434  Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3
435
436val program_rect_Type3 :
437  (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
438  Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3
439
440val program_rect_Type2 :
441  (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
442  Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3
443
444val program_rect_Type1 :
445  (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
446  Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3
447
448val program_rect_Type0 :
449  (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
450  Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3
451
452val prog_vars :
453  ('a1, 'a2) program -> ((ident, region) Types.prod, 'a2) Types.prod
454  List.list
455
456val prog_funct : ('a1, 'a2) program -> (ident, 'a1) Types.prod List.list
457
458val prog_main : ('a1, 'a2) program -> ident
459
460val program_inv_rect_Type4 :
461  ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
462  List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
463  'a3
464
465val program_inv_rect_Type3 :
466  ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
467  List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
468  'a3
469
470val program_inv_rect_Type2 :
471  ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
472  List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
473  'a3
474
475val program_inv_rect_Type1 :
476  ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
477  List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
478  'a3
479
480val program_inv_rect_Type0 :
481  ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
482  List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
483  'a3
484
485val program_discr : ('a1, 'a2) program -> ('a1, 'a2) program -> __
486
487val program_jmdiscr : ('a1, 'a2) program -> ('a1, 'a2) program -> __
488
489val prog_funct_names : ('a1, 'a2) program -> ident List.list
490
491val prog_var_names : ('a1, 'a2) program -> ident List.list
492
493val transf_program :
494  ('a1 -> 'a2) -> (ident, 'a1) Types.prod List.list -> (ident, 'a2)
495  Types.prod List.list
496
497val transform_program :
498  ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2) -> ('a2, 'a3) program
499
500val transf_program_gen :
501  String.string -> Identifiers.universe -> (Identifiers.universe -> 'a1 ->
502  ('a2, Identifiers.universe) Types.prod) -> (ident, 'a1) Types.prod
503  List.list -> ((ident, 'a2) Types.prod List.list, Identifiers.universe)
504  Types.prod
505
506val transform_program_gen :
507  String.string -> Identifiers.universe -> ('a1, 'a3) program -> (ident
508  List.list -> Identifiers.universe -> 'a1 -> ('a2, Identifiers.universe)
509  Types.prod) -> (('a2, 'a3) program, Identifiers.universe) Types.prod
510
511val map_partial :
512  ('a2 -> 'a3 Errors.res) -> ('a1, 'a2) Types.prod List.list -> ('a1, 'a3)
513  Types.prod List.list Errors.res
514
515val transform_partial_program :
516  ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2 Errors.res) -> ('a2,
517  'a3) program Errors.res
518
519val transform_partial_program2 :
520  ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2 Errors.res) -> ('a3 ->
521  'a4 Errors.res) -> ('a2, 'a4) program Errors.res
522
523type matching =
524| Mk_matching
525
526val matching_rect_Type4 :
527  (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1
528
529val matching_rect_Type5 :
530  (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1
531
532val matching_rect_Type3 :
533  (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1
534
535val matching_rect_Type2 :
536  (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1
537
538val matching_rect_Type1 :
539  (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1
540
541val matching_rect_Type0 :
542  (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1
543
544type m_A
545
546type m_B
547
548type m_V
549
550type m_W
551
552type match_fundef = __
553
554type match_varinfo = __
555
556val matching_inv_rect_Type4 :
557  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
558
559val matching_inv_rect_Type3 :
560  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
561
562val matching_inv_rect_Type2 :
563  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
564
565val matching_inv_rect_Type1 :
566  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
567
568val matching_inv_rect_Type0 :
569  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
570
571val matching_jmdiscr : matching -> matching -> __
572
573val mfe_cast_fn_type :
574  matching -> ident List.list -> ident List.list -> __ -> __
575
576val match_program_rect_Type4 :
577  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
578  -> 'a1
579
580val match_program_rect_Type5 :
581  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
582  -> 'a1
583
584val match_program_rect_Type3 :
585  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
586  -> 'a1
587
588val match_program_rect_Type2 :
589  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
590  -> 'a1
591
592val match_program_rect_Type1 :
593  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
594  -> 'a1
595
596val match_program_rect_Type0 :
597  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
598  -> 'a1
599
600val match_program_inv_rect_Type4 :
601  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
602  -> 'a1) -> 'a1
603
604val match_program_inv_rect_Type3 :
605  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
606  -> 'a1) -> 'a1
607
608val match_program_inv_rect_Type2 :
609  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
610  -> 'a1) -> 'a1
611
612val match_program_inv_rect_Type1 :
613  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
614  -> 'a1) -> 'a1
615
616val match_program_inv_rect_Type0 :
617  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
618  -> 'a1) -> 'a1
619
620val match_program_discr :
621  matching -> (__, __) program -> (__, __) program -> __
622
623val match_program_jmdiscr :
624  matching -> (__, __) program -> (__, __) program -> __
625
626type external_function = { ef_id : ident; ef_sig : signature }
627
628val external_function_rect_Type4 :
629  (ident -> signature -> 'a1) -> external_function -> 'a1
630
631val external_function_rect_Type5 :
632  (ident -> signature -> 'a1) -> external_function -> 'a1
633
634val external_function_rect_Type3 :
635  (ident -> signature -> 'a1) -> external_function -> 'a1
636
637val external_function_rect_Type2 :
638  (ident -> signature -> 'a1) -> external_function -> 'a1
639
640val external_function_rect_Type1 :
641  (ident -> signature -> 'a1) -> external_function -> 'a1
642
643val external_function_rect_Type0 :
644  (ident -> signature -> 'a1) -> external_function -> 'a1
645
646val ef_id : external_function -> ident
647
648val ef_sig : external_function -> signature
649
650val external_function_inv_rect_Type4 :
651  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
652
653val external_function_inv_rect_Type3 :
654  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
655
656val external_function_inv_rect_Type2 :
657  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
658
659val external_function_inv_rect_Type1 :
660  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
661
662val external_function_inv_rect_Type0 :
663  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
664
665val external_function_discr : external_function -> external_function -> __
666
667val external_function_jmdiscr : external_function -> external_function -> __
668
669type externalFunction = external_function
670
671val external_function_tag : external_function -> ident
672
673val external_function_sig : external_function -> signature
674
675type 'f fundef =
676| Internal of 'f
677| External of external_function
678
679val fundef_rect_Type4 :
680  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
681
682val fundef_rect_Type5 :
683  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
684
685val fundef_rect_Type3 :
686  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
687
688val fundef_rect_Type2 :
689  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
690
691val fundef_rect_Type1 :
692  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
693
694val fundef_rect_Type0 :
695  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
696
697val fundef_inv_rect_Type4 :
698  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
699
700val fundef_inv_rect_Type3 :
701  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
702
703val fundef_inv_rect_Type2 :
704  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
705
706val fundef_inv_rect_Type1 :
707  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
708
709val fundef_inv_rect_Type0 :
710  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
711
712val fundef_discr : 'a1 fundef -> 'a1 fundef -> __
713
714val fundef_jmdiscr : 'a1 fundef -> 'a1 fundef -> __
715
716val transf_fundef : ('a1 -> 'a2) -> 'a1 fundef -> 'a2 fundef
717
718val transf_partial_fundef :
719  ('a1 -> 'a2 Errors.res) -> 'a1 fundef -> 'a2 fundef Errors.res
720
721type member1 = __
722
Note: See TracBrowser for help on using the repository browser.