source: extracted/aST.mli @ 2649

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

...

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