source: extracted/aST.mli @ 2746

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