source: driver/extracted/aST.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
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 Util
22
23open FoldStuff
24
25open BitVector
26
27open Jmeq
28
29open Russell
30
31open List
32
33open Setoids
34
35open Monad
36
37open Option
38
39open Extranat
40
41open Bool
42
43open Relations
44
45open Nat
46
47open Integers
48
49open Proper
50
51open PositiveMap
52
53open Deqsets
54
55open ErrorMessages
56
57open PreIdentifiers
58
59open Errors
60
61open Extralib
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 repr : 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
534val matching_inv_rect_Type4 :
535  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
536
537val matching_inv_rect_Type3 :
538  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
539
540val matching_inv_rect_Type2 :
541  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
542
543val matching_inv_rect_Type1 :
544  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
545
546val matching_inv_rect_Type0 :
547  matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
548
549val matching_jmdiscr : matching -> matching -> __
550
551val mfe_cast_fn_type :
552  matching -> ident List.list -> ident List.list -> __ -> __
553
554val match_program_rect_Type4 :
555  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
556  -> 'a1
557
558val match_program_rect_Type5 :
559  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
560  -> 'a1
561
562val match_program_rect_Type3 :
563  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
564  -> 'a1
565
566val match_program_rect_Type2 :
567  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
568  -> 'a1
569
570val match_program_rect_Type1 :
571  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
572  -> 'a1
573
574val match_program_rect_Type0 :
575  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> 'a1)
576  -> 'a1
577
578val match_program_inv_rect_Type4 :
579  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
580  -> 'a1) -> 'a1
581
582val match_program_inv_rect_Type3 :
583  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
584  -> 'a1) -> 'a1
585
586val match_program_inv_rect_Type2 :
587  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
588  -> 'a1) -> 'a1
589
590val match_program_inv_rect_Type1 :
591  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
592  -> 'a1) -> 'a1
593
594val match_program_inv_rect_Type0 :
595  matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
596  -> 'a1) -> 'a1
597
598val match_program_discr :
599  matching -> (__, __) program -> (__, __) program -> __
600
601val match_program_jmdiscr :
602  matching -> (__, __) program -> (__, __) program -> __
603
604type external_function = { ef_id : ident; ef_sig : signature }
605
606val external_function_rect_Type4 :
607  (ident -> signature -> 'a1) -> external_function -> 'a1
608
609val external_function_rect_Type5 :
610  (ident -> signature -> 'a1) -> external_function -> 'a1
611
612val external_function_rect_Type3 :
613  (ident -> signature -> 'a1) -> external_function -> 'a1
614
615val external_function_rect_Type2 :
616  (ident -> signature -> 'a1) -> external_function -> 'a1
617
618val external_function_rect_Type1 :
619  (ident -> signature -> 'a1) -> external_function -> 'a1
620
621val external_function_rect_Type0 :
622  (ident -> signature -> 'a1) -> external_function -> 'a1
623
624val ef_id : external_function -> ident
625
626val ef_sig : external_function -> signature
627
628val external_function_inv_rect_Type4 :
629  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
630
631val external_function_inv_rect_Type3 :
632  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
633
634val external_function_inv_rect_Type2 :
635  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
636
637val external_function_inv_rect_Type1 :
638  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
639
640val external_function_inv_rect_Type0 :
641  external_function -> (ident -> signature -> __ -> 'a1) -> 'a1
642
643val external_function_discr : external_function -> external_function -> __
644
645val external_function_jmdiscr : external_function -> external_function -> __
646
647type externalFunction = external_function
648
649val external_function_tag : external_function -> ident
650
651val external_function_sig : external_function -> signature
652
653type 'f fundef =
654| Internal of 'f
655| External of external_function
656
657val fundef_rect_Type4 :
658  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
659
660val fundef_rect_Type5 :
661  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
662
663val fundef_rect_Type3 :
664  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
665
666val fundef_rect_Type2 :
667  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
668
669val fundef_rect_Type1 :
670  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
671
672val fundef_rect_Type0 :
673  ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2
674
675val fundef_inv_rect_Type4 :
676  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
677
678val fundef_inv_rect_Type3 :
679  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
680
681val fundef_inv_rect_Type2 :
682  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
683
684val fundef_inv_rect_Type1 :
685  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
686
687val fundef_inv_rect_Type0 :
688  'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) -> 'a2
689
690val fundef_discr : 'a1 fundef -> 'a1 fundef -> __
691
692val fundef_jmdiscr : 'a1 fundef -> 'a1 fundef -> __
693
694val transf_fundef : ('a1 -> 'a2) -> 'a1 fundef -> 'a2 fundef
695
696val transf_partial_fundef :
697  ('a1 -> 'a2 Errors.res) -> 'a1 fundef -> 'a2 fundef Errors.res
698
Note: See TracBrowser for help on using the repository browser.