source: extracted/aST.ml @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 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: 57.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
73(** val symbolTag : String.string **)
74let symbolTag = "symbolTag"
75  (* failwith "AXIOM TO BE REALIZED" *)
76
77type ident = PreIdentifiers.identifier
78
79(** val ident_eq : ident -> ident -> (__, __) Types.sum **)
80let ident_eq =
81  Identifiers.identifier_eq symbolTag
82
83(** val ident_of_nat : Nat.nat -> ident **)
84let ident_of_nat =
85  Identifiers.identifier_of_nat symbolTag
86
87type region =
88| XData
89| Code
90
91(** val region_rect_Type4 : 'a1 -> 'a1 -> region -> 'a1 **)
92let rec region_rect_Type4 h_XData h_Code = function
93| XData -> h_XData
94| Code -> h_Code
95
96(** val region_rect_Type5 : 'a1 -> 'a1 -> region -> 'a1 **)
97let rec region_rect_Type5 h_XData h_Code = function
98| XData -> h_XData
99| Code -> h_Code
100
101(** val region_rect_Type3 : 'a1 -> 'a1 -> region -> 'a1 **)
102let rec region_rect_Type3 h_XData h_Code = function
103| XData -> h_XData
104| Code -> h_Code
105
106(** val region_rect_Type2 : 'a1 -> 'a1 -> region -> 'a1 **)
107let rec region_rect_Type2 h_XData h_Code = function
108| XData -> h_XData
109| Code -> h_Code
110
111(** val region_rect_Type1 : 'a1 -> 'a1 -> region -> 'a1 **)
112let rec region_rect_Type1 h_XData h_Code = function
113| XData -> h_XData
114| Code -> h_Code
115
116(** val region_rect_Type0 : 'a1 -> 'a1 -> region -> 'a1 **)
117let rec region_rect_Type0 h_XData h_Code = function
118| XData -> h_XData
119| Code -> h_Code
120
121(** val region_inv_rect_Type4 :
122    region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
123let region_inv_rect_Type4 hterm h1 h2 =
124  let hcut = region_rect_Type4 h1 h2 hterm in hcut __
125
126(** val region_inv_rect_Type3 :
127    region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
128let region_inv_rect_Type3 hterm h1 h2 =
129  let hcut = region_rect_Type3 h1 h2 hterm in hcut __
130
131(** val region_inv_rect_Type2 :
132    region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
133let region_inv_rect_Type2 hterm h1 h2 =
134  let hcut = region_rect_Type2 h1 h2 hterm in hcut __
135
136(** val region_inv_rect_Type1 :
137    region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
138let region_inv_rect_Type1 hterm h1 h2 =
139  let hcut = region_rect_Type1 h1 h2 hterm in hcut __
140
141(** val region_inv_rect_Type0 :
142    region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
143let region_inv_rect_Type0 hterm h1 h2 =
144  let hcut = region_rect_Type0 h1 h2 hterm in hcut __
145
146(** val region_discr : region -> region -> __ **)
147let region_discr x y =
148  Logic.eq_rect_Type2 x
149    (match x with
150     | XData -> Obj.magic (fun _ dH -> dH)
151     | Code -> Obj.magic (fun _ dH -> dH)) y
152
153(** val region_jmdiscr : region -> region -> __ **)
154let region_jmdiscr x y =
155  Logic.eq_rect_Type2 x
156    (match x with
157     | XData -> Obj.magic (fun _ dH -> dH)
158     | Code -> Obj.magic (fun _ dH -> dH)) y
159
160(** val eq_region : region -> region -> Bool.bool **)
161let eq_region r5 r6 =
162  match r5 with
163  | XData ->
164    (match r6 with
165     | XData -> Bool.True
166     | Code -> Bool.False)
167  | Code ->
168    (match r6 with
169     | XData -> Bool.False
170     | Code -> Bool.True)
171
172(** val eq_region_elim :
173    region -> region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
174let eq_region_elim r5 r6 =
175  match r5 with
176  | XData ->
177    (match r6 with
178     | XData -> (fun ptrue pfalse -> ptrue __)
179     | Code -> (fun ptrue pfalse -> pfalse __))
180  | Code ->
181    (match r6 with
182     | XData -> (fun ptrue pfalse -> pfalse __)
183     | Code -> (fun ptrue pfalse -> ptrue __))
184
185(** val eq_region_dec : region -> region -> (__, __) Types.sum **)
186let eq_region_dec r5 r6 =
187  eq_region_elim r5 r6 (fun _ -> Types.Inl __) (fun _ -> Types.Inr __)
188
189(** val size_pointer : Nat.nat **)
190let size_pointer =
191  Nat.S (Nat.S Nat.O)
192
193type signedness =
194| Signed
195| Unsigned
196
197(** val signedness_rect_Type4 : 'a1 -> 'a1 -> signedness -> 'a1 **)
198let rec signedness_rect_Type4 h_Signed h_Unsigned = function
199| Signed -> h_Signed
200| Unsigned -> h_Unsigned
201
202(** val signedness_rect_Type5 : 'a1 -> 'a1 -> signedness -> 'a1 **)
203let rec signedness_rect_Type5 h_Signed h_Unsigned = function
204| Signed -> h_Signed
205| Unsigned -> h_Unsigned
206
207(** val signedness_rect_Type3 : 'a1 -> 'a1 -> signedness -> 'a1 **)
208let rec signedness_rect_Type3 h_Signed h_Unsigned = function
209| Signed -> h_Signed
210| Unsigned -> h_Unsigned
211
212(** val signedness_rect_Type2 : 'a1 -> 'a1 -> signedness -> 'a1 **)
213let rec signedness_rect_Type2 h_Signed h_Unsigned = function
214| Signed -> h_Signed
215| Unsigned -> h_Unsigned
216
217(** val signedness_rect_Type1 : 'a1 -> 'a1 -> signedness -> 'a1 **)
218let rec signedness_rect_Type1 h_Signed h_Unsigned = function
219| Signed -> h_Signed
220| Unsigned -> h_Unsigned
221
222(** val signedness_rect_Type0 : 'a1 -> 'a1 -> signedness -> 'a1 **)
223let rec signedness_rect_Type0 h_Signed h_Unsigned = function
224| Signed -> h_Signed
225| Unsigned -> h_Unsigned
226
227(** val signedness_inv_rect_Type4 :
228    signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
229let signedness_inv_rect_Type4 hterm h1 h2 =
230  let hcut = signedness_rect_Type4 h1 h2 hterm in hcut __
231
232(** val signedness_inv_rect_Type3 :
233    signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
234let signedness_inv_rect_Type3 hterm h1 h2 =
235  let hcut = signedness_rect_Type3 h1 h2 hterm in hcut __
236
237(** val signedness_inv_rect_Type2 :
238    signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
239let signedness_inv_rect_Type2 hterm h1 h2 =
240  let hcut = signedness_rect_Type2 h1 h2 hterm in hcut __
241
242(** val signedness_inv_rect_Type1 :
243    signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
244let signedness_inv_rect_Type1 hterm h1 h2 =
245  let hcut = signedness_rect_Type1 h1 h2 hterm in hcut __
246
247(** val signedness_inv_rect_Type0 :
248    signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
249let signedness_inv_rect_Type0 hterm h1 h2 =
250  let hcut = signedness_rect_Type0 h1 h2 hterm in hcut __
251
252(** val signedness_discr : signedness -> signedness -> __ **)
253let signedness_discr x y =
254  Logic.eq_rect_Type2 x
255    (match x with
256     | Signed -> Obj.magic (fun _ dH -> dH)
257     | Unsigned -> Obj.magic (fun _ dH -> dH)) y
258
259(** val signedness_jmdiscr : signedness -> signedness -> __ **)
260let signedness_jmdiscr x y =
261  Logic.eq_rect_Type2 x
262    (match x with
263     | Signed -> Obj.magic (fun _ dH -> dH)
264     | Unsigned -> Obj.magic (fun _ dH -> dH)) y
265
266type intsize =
267| I8
268| I16
269| I32
270
271(** val intsize_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
272let rec intsize_rect_Type4 h_I8 h_I16 h_I32 = function
273| I8 -> h_I8
274| I16 -> h_I16
275| I32 -> h_I32
276
277(** val intsize_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
278let rec intsize_rect_Type5 h_I8 h_I16 h_I32 = function
279| I8 -> h_I8
280| I16 -> h_I16
281| I32 -> h_I32
282
283(** val intsize_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
284let rec intsize_rect_Type3 h_I8 h_I16 h_I32 = function
285| I8 -> h_I8
286| I16 -> h_I16
287| I32 -> h_I32
288
289(** val intsize_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
290let rec intsize_rect_Type2 h_I8 h_I16 h_I32 = function
291| I8 -> h_I8
292| I16 -> h_I16
293| I32 -> h_I32
294
295(** val intsize_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
296let rec intsize_rect_Type1 h_I8 h_I16 h_I32 = function
297| I8 -> h_I8
298| I16 -> h_I16
299| I32 -> h_I32
300
301(** val intsize_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
302let rec intsize_rect_Type0 h_I8 h_I16 h_I32 = function
303| I8 -> h_I8
304| I16 -> h_I16
305| I32 -> h_I32
306
307(** val intsize_inv_rect_Type4 :
308    intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
309let intsize_inv_rect_Type4 hterm h1 h2 h3 =
310  let hcut = intsize_rect_Type4 h1 h2 h3 hterm in hcut __
311
312(** val intsize_inv_rect_Type3 :
313    intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
314let intsize_inv_rect_Type3 hterm h1 h2 h3 =
315  let hcut = intsize_rect_Type3 h1 h2 h3 hterm in hcut __
316
317(** val intsize_inv_rect_Type2 :
318    intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
319let intsize_inv_rect_Type2 hterm h1 h2 h3 =
320  let hcut = intsize_rect_Type2 h1 h2 h3 hterm in hcut __
321
322(** val intsize_inv_rect_Type1 :
323    intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
324let intsize_inv_rect_Type1 hterm h1 h2 h3 =
325  let hcut = intsize_rect_Type1 h1 h2 h3 hterm in hcut __
326
327(** val intsize_inv_rect_Type0 :
328    intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
329let intsize_inv_rect_Type0 hterm h1 h2 h3 =
330  let hcut = intsize_rect_Type0 h1 h2 h3 hterm in hcut __
331
332(** val intsize_discr : intsize -> intsize -> __ **)
333let intsize_discr x y =
334  Logic.eq_rect_Type2 x
335    (match x with
336     | I8 -> Obj.magic (fun _ dH -> dH)
337     | I16 -> Obj.magic (fun _ dH -> dH)
338     | I32 -> Obj.magic (fun _ dH -> dH)) y
339
340(** val intsize_jmdiscr : intsize -> intsize -> __ **)
341let intsize_jmdiscr x y =
342  Logic.eq_rect_Type2 x
343    (match x with
344     | I8 -> Obj.magic (fun _ dH -> dH)
345     | I16 -> Obj.magic (fun _ dH -> dH)
346     | I32 -> Obj.magic (fun _ dH -> dH)) y
347
348type floatsize =
349| F32
350| F64
351
352(** val floatsize_rect_Type4 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
353let rec floatsize_rect_Type4 h_F32 h_F64 = function
354| F32 -> h_F32
355| F64 -> h_F64
356
357(** val floatsize_rect_Type5 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
358let rec floatsize_rect_Type5 h_F32 h_F64 = function
359| F32 -> h_F32
360| F64 -> h_F64
361
362(** val floatsize_rect_Type3 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
363let rec floatsize_rect_Type3 h_F32 h_F64 = function
364| F32 -> h_F32
365| F64 -> h_F64
366
367(** val floatsize_rect_Type2 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
368let rec floatsize_rect_Type2 h_F32 h_F64 = function
369| F32 -> h_F32
370| F64 -> h_F64
371
372(** val floatsize_rect_Type1 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
373let rec floatsize_rect_Type1 h_F32 h_F64 = function
374| F32 -> h_F32
375| F64 -> h_F64
376
377(** val floatsize_rect_Type0 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
378let rec floatsize_rect_Type0 h_F32 h_F64 = function
379| F32 -> h_F32
380| F64 -> h_F64
381
382(** val floatsize_inv_rect_Type4 :
383    floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
384let floatsize_inv_rect_Type4 hterm h1 h2 =
385  let hcut = floatsize_rect_Type4 h1 h2 hterm in hcut __
386
387(** val floatsize_inv_rect_Type3 :
388    floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
389let floatsize_inv_rect_Type3 hterm h1 h2 =
390  let hcut = floatsize_rect_Type3 h1 h2 hterm in hcut __
391
392(** val floatsize_inv_rect_Type2 :
393    floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
394let floatsize_inv_rect_Type2 hterm h1 h2 =
395  let hcut = floatsize_rect_Type2 h1 h2 hterm in hcut __
396
397(** val floatsize_inv_rect_Type1 :
398    floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
399let floatsize_inv_rect_Type1 hterm h1 h2 =
400  let hcut = floatsize_rect_Type1 h1 h2 hterm in hcut __
401
402(** val floatsize_inv_rect_Type0 :
403    floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
404let floatsize_inv_rect_Type0 hterm h1 h2 =
405  let hcut = floatsize_rect_Type0 h1 h2 hterm in hcut __
406
407(** val floatsize_discr : floatsize -> floatsize -> __ **)
408let floatsize_discr x y =
409  Logic.eq_rect_Type2 x
410    (match x with
411     | F32 -> Obj.magic (fun _ dH -> dH)
412     | F64 -> Obj.magic (fun _ dH -> dH)) y
413
414(** val floatsize_jmdiscr : floatsize -> floatsize -> __ **)
415let floatsize_jmdiscr x y =
416  Logic.eq_rect_Type2 x
417    (match x with
418     | F32 -> Obj.magic (fun _ dH -> dH)
419     | F64 -> Obj.magic (fun _ dH -> dH)) y
420
421type typ =
422| ASTint of intsize * signedness
423| ASTptr
424
425(** val typ_rect_Type4 :
426    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
427let rec typ_rect_Type4 h_ASTint h_ASTptr = function
428| ASTint (x_2531, x_2530) -> h_ASTint x_2531 x_2530
429| ASTptr -> h_ASTptr
430
431(** val typ_rect_Type5 :
432    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
433let rec typ_rect_Type5 h_ASTint h_ASTptr = function
434| ASTint (x_2536, x_2535) -> h_ASTint x_2536 x_2535
435| ASTptr -> h_ASTptr
436
437(** val typ_rect_Type3 :
438    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
439let rec typ_rect_Type3 h_ASTint h_ASTptr = function
440| ASTint (x_2541, x_2540) -> h_ASTint x_2541 x_2540
441| ASTptr -> h_ASTptr
442
443(** val typ_rect_Type2 :
444    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
445let rec typ_rect_Type2 h_ASTint h_ASTptr = function
446| ASTint (x_2546, x_2545) -> h_ASTint x_2546 x_2545
447| ASTptr -> h_ASTptr
448
449(** val typ_rect_Type1 :
450    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
451let rec typ_rect_Type1 h_ASTint h_ASTptr = function
452| ASTint (x_2551, x_2550) -> h_ASTint x_2551 x_2550
453| ASTptr -> h_ASTptr
454
455(** val typ_rect_Type0 :
456    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
457let rec typ_rect_Type0 h_ASTint h_ASTptr = function
458| ASTint (x_2556, x_2555) -> h_ASTint x_2556 x_2555
459| ASTptr -> h_ASTptr
460
461(** val typ_inv_rect_Type4 :
462    typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
463let typ_inv_rect_Type4 hterm h1 h2 =
464  let hcut = typ_rect_Type4 h1 h2 hterm in hcut __
465
466(** val typ_inv_rect_Type3 :
467    typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
468let typ_inv_rect_Type3 hterm h1 h2 =
469  let hcut = typ_rect_Type3 h1 h2 hterm in hcut __
470
471(** val typ_inv_rect_Type2 :
472    typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
473let typ_inv_rect_Type2 hterm h1 h2 =
474  let hcut = typ_rect_Type2 h1 h2 hterm in hcut __
475
476(** val typ_inv_rect_Type1 :
477    typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
478let typ_inv_rect_Type1 hterm h1 h2 =
479  let hcut = typ_rect_Type1 h1 h2 hterm in hcut __
480
481(** val typ_inv_rect_Type0 :
482    typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
483let typ_inv_rect_Type0 hterm h1 h2 =
484  let hcut = typ_rect_Type0 h1 h2 hterm in hcut __
485
486(** val typ_discr : typ -> typ -> __ **)
487let typ_discr x y =
488  Logic.eq_rect_Type2 x
489    (match x with
490     | ASTint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
491     | ASTptr -> Obj.magic (fun _ dH -> dH)) y
492
493(** val typ_jmdiscr : typ -> typ -> __ **)
494let typ_jmdiscr x y =
495  Logic.eq_rect_Type2 x
496    (match x with
497     | ASTint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
498     | ASTptr -> Obj.magic (fun _ dH -> dH)) y
499
500type sigType = typ
501
502(** val sigType_Int : typ **)
503let sigType_Int =
504  ASTint (I32, Unsigned)
505
506(** val sigType_Ptr : typ **)
507let sigType_Ptr =
508  ASTptr
509
510(** val pred_size_intsize : intsize -> Nat.nat **)
511let pred_size_intsize = function
512| I8 -> Nat.O
513| I16 -> Nat.S Nat.O
514| I32 -> Nat.S (Nat.S (Nat.S Nat.O))
515
516(** val size_intsize : intsize -> Nat.nat **)
517let size_intsize sz =
518  Nat.S (pred_size_intsize sz)
519
520(** val bitsize_of_intsize : intsize -> Nat.nat **)
521let bitsize_of_intsize sz =
522  Nat.times (size_intsize sz) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
523    (Nat.S (Nat.S Nat.O))))))))
524
525(** val eq_intsize : intsize -> intsize -> Bool.bool **)
526let eq_intsize sz1 sz2 =
527  match sz1 with
528  | I8 ->
529    (match sz2 with
530     | I8 -> Bool.True
531     | I16 -> Bool.False
532     | I32 -> Bool.False)
533  | I16 ->
534    (match sz2 with
535     | I8 -> Bool.False
536     | I16 -> Bool.True
537     | I32 -> Bool.False)
538  | I32 ->
539    (match sz2 with
540     | I8 -> Bool.False
541     | I16 -> Bool.False
542     | I32 -> Bool.True)
543
544(** val eq_intsize_elim :
545    intsize -> intsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
546let eq_intsize_elim clearme sz2 x x0 =
547  (match clearme with
548   | I8 ->
549     (fun clearme0 ->
550       match clearme0 with
551       | I8 -> (fun _ hne heq -> heq __)
552       | I16 -> (fun _ hne heq -> hne __)
553       | I32 -> (fun _ hne heq -> hne __))
554   | I16 ->
555     (fun clearme0 ->
556       match clearme0 with
557       | I8 -> (fun _ hne heq -> hne __)
558       | I16 -> (fun _ hne heq -> heq __)
559       | I32 -> (fun _ hne heq -> hne __))
560   | I32 ->
561     (fun clearme0 ->
562       match clearme0 with
563       | I8 -> (fun _ hne heq -> hne __)
564       | I16 -> (fun _ hne heq -> hne __)
565       | I32 -> (fun _ hne heq -> heq __))) sz2 __ x x0
566
567(** val signedness_check : signedness -> signedness -> 'a1 -> 'a1 -> 'a1 **)
568let signedness_check sg1 sg2 =
569  match sg1 with
570  | Signed ->
571    (fun x ->
572      match sg2 with
573      | Signed -> (fun d -> x)
574      | Unsigned -> (fun d -> d))
575  | Unsigned ->
576    (fun x ->
577      match sg2 with
578      | Signed -> (fun d -> d)
579      | Unsigned -> (fun d -> x))
580
581(** val inttyp_eq_elim' :
582    intsize -> intsize -> signedness -> signedness -> 'a1 -> 'a1 -> 'a1 **)
583let rec inttyp_eq_elim' sz1 sz2 sg1 sg2 =
584  match sz1 with
585  | I8 ->
586    (fun x ->
587      match sz2 with
588      | I8 -> signedness_check sg1 sg2 x
589      | I16 -> (fun d -> d)
590      | I32 -> (fun d -> d))
591  | I16 ->
592    (fun x ->
593      match sz2 with
594      | I8 -> (fun d -> d)
595      | I16 -> signedness_check sg1 sg2 x
596      | I32 -> (fun d -> d))
597  | I32 ->
598    (fun x ->
599      match sz2 with
600      | I8 -> (fun d -> d)
601      | I16 -> (fun d -> d)
602      | I32 -> signedness_check sg1 sg2 x)
603
604(** val intsize_eq_elim' : intsize -> intsize -> 'a1 -> 'a1 -> 'a1 **)
605let rec intsize_eq_elim' sz1 sz2 =
606  match sz1 with
607  | I8 ->
608    (fun x ->
609      match sz2 with
610      | I8 -> (fun d -> x)
611      | I16 -> (fun d -> d)
612      | I32 -> (fun d -> d))
613  | I16 ->
614    (fun x ->
615      match sz2 with
616      | I8 -> (fun d -> d)
617      | I16 -> (fun d -> x)
618      | I32 -> (fun d -> d))
619  | I32 ->
620    (fun x ->
621      match sz2 with
622      | I8 -> (fun d -> d)
623      | I16 -> (fun d -> d)
624      | I32 -> (fun d -> x))
625
626(** val intsize_eq_elim :
627    intsize -> intsize -> 'a2 -> ('a2 -> 'a1) -> 'a1 -> 'a1 **)
628let rec intsize_eq_elim sz1 sz2 =
629  match sz1 with
630  | I8 ->
631    (fun x ->
632      match sz2 with
633      | I8 -> (fun f d -> f x)
634      | I16 -> (fun f d -> d)
635      | I32 -> (fun f d -> d))
636  | I16 ->
637    (fun x ->
638      match sz2 with
639      | I8 -> (fun f d -> d)
640      | I16 -> (fun f d -> f x)
641      | I32 -> (fun f d -> d))
642  | I32 ->
643    (fun x ->
644      match sz2 with
645      | I8 -> (fun f d -> d)
646      | I16 -> (fun f d -> d)
647      | I32 -> (fun f d -> f x))
648
649(** val intsize_eq_elim_elim :
650    intsize -> intsize -> 'a2 -> ('a2 -> 'a1) -> 'a1 -> (__ -> 'a3) -> (__ ->
651    __) -> 'a3 **)
652let intsize_eq_elim_elim clearme sz2 p f d x x0 =
653  (match clearme with
654   | I8 ->
655     (fun clearme0 ->
656       match clearme0 with
657       | I8 -> (fun _ p0 f0 d0 _ hne heq -> Obj.magic heq __)
658       | I16 -> (fun _ p0 f0 d0 _ hne heq -> hne __)
659       | I32 -> (fun _ p0 f0 d0 _ hne heq -> hne __))
660   | I16 ->
661     (fun clearme0 ->
662       match clearme0 with
663       | I8 -> (fun _ p0 f0 d0 _ hne heq -> hne __)
664       | I16 -> (fun _ p0 f0 d0 _ hne heq -> Obj.magic heq __)
665       | I32 -> (fun _ p0 f0 d0 _ hne heq -> hne __))
666   | I32 ->
667     (fun clearme0 ->
668       match clearme0 with
669       | I8 -> (fun _ p0 f0 d0 _ hne heq -> hne __)
670       | I16 -> (fun _ p0 f0 d0 _ hne heq -> hne __)
671       | I32 -> (fun _ p0 f0 d0 _ hne heq -> Obj.magic heq __))) sz2 __ p f d
672    __ x x0
673
674type bvint = BitVector.bitVector
675
676(** val repr0 : intsize -> Nat.nat -> bvint **)
677let repr0 sz x =
678  Arithmetic.bitvector_of_nat (bitsize_of_intsize sz) x
679
680(** val size_floatsize : floatsize -> Nat.nat **)
681let size_floatsize sz =
682  Nat.S
683    (match sz with
684     | F32 -> Nat.S (Nat.S (Nat.S Nat.O))
685     | F64 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
686
687(** val floatsize_eq_elim : floatsize -> floatsize -> 'a1 -> 'a1 -> 'a1 **)
688let rec floatsize_eq_elim sz1 sz2 =
689  match sz1 with
690  | F32 ->
691    (fun x ->
692      match sz2 with
693      | F32 -> (fun d -> x)
694      | F64 -> (fun d -> d))
695  | F64 ->
696    (fun x ->
697      match sz2 with
698      | F32 -> (fun d -> d)
699      | F64 -> (fun d -> x))
700
701(** val typesize : typ -> Nat.nat **)
702let typesize = function
703| ASTint (sz, x) -> size_intsize sz
704| ASTptr -> size_pointer
705
706(** val typ_eq : typ -> typ -> (__, __) Types.sum **)
707let typ_eq = function
708| ASTint (clearme0, x) ->
709  (match clearme0 with
710   | I8 ->
711     (fun clearme1 ->
712       match clearme1 with
713       | Signed ->
714         (fun clearme2 ->
715           match clearme2 with
716           | ASTint (clearme3, x0) ->
717             (match clearme3 with
718              | I8 ->
719                (fun clearme4 ->
720                  match clearme4 with
721                  | Signed -> Types.Inl __
722                  | Unsigned -> Types.Inr __)
723              | I16 ->
724                (fun clearme4 ->
725                  match clearme4 with
726                  | Signed -> Types.Inr __
727                  | Unsigned -> Types.Inr __)
728              | I32 ->
729                (fun clearme4 ->
730                  match clearme4 with
731                  | Signed -> Types.Inr __
732                  | Unsigned -> Types.Inr __)) x0
733           | ASTptr -> Types.Inr __)
734       | Unsigned ->
735         (fun clearme2 ->
736           match clearme2 with
737           | ASTint (clearme3, x0) ->
738             (match clearme3 with
739              | I8 ->
740                (fun clearme4 ->
741                  match clearme4 with
742                  | Signed -> Types.Inr __
743                  | Unsigned -> Types.Inl __)
744              | I16 ->
745                (fun clearme4 ->
746                  match clearme4 with
747                  | Signed -> Types.Inr __
748                  | Unsigned -> Types.Inr __)
749              | I32 ->
750                (fun clearme4 ->
751                  match clearme4 with
752                  | Signed -> Types.Inr __
753                  | Unsigned -> Types.Inr __)) x0
754           | ASTptr -> Types.Inr __))
755   | I16 ->
756     (fun clearme1 ->
757       match clearme1 with
758       | Signed ->
759         (fun clearme2 ->
760           match clearme2 with
761           | ASTint (clearme3, x0) ->
762             (match clearme3 with
763              | I8 ->
764                (fun clearme4 ->
765                  match clearme4 with
766                  | Signed -> Types.Inr __
767                  | Unsigned -> Types.Inr __)
768              | I16 ->
769                (fun clearme4 ->
770                  match clearme4 with
771                  | Signed -> Types.Inl __
772                  | Unsigned -> Types.Inr __)
773              | I32 ->
774                (fun clearme4 ->
775                  match clearme4 with
776                  | Signed -> Types.Inr __
777                  | Unsigned -> Types.Inr __)) x0
778           | ASTptr -> Types.Inr __)
779       | Unsigned ->
780         (fun clearme2 ->
781           match clearme2 with
782           | ASTint (clearme3, x0) ->
783             (match clearme3 with
784              | I8 ->
785                (fun clearme4 ->
786                  match clearme4 with
787                  | Signed -> Types.Inr __
788                  | Unsigned -> Types.Inr __)
789              | I16 ->
790                (fun clearme4 ->
791                  match clearme4 with
792                  | Signed -> Types.Inr __
793                  | Unsigned -> Types.Inl __)
794              | I32 ->
795                (fun clearme4 ->
796                  match clearme4 with
797                  | Signed -> Types.Inr __
798                  | Unsigned -> Types.Inr __)) x0
799           | ASTptr -> Types.Inr __))
800   | I32 ->
801     (fun clearme1 ->
802       match clearme1 with
803       | Signed ->
804         (fun clearme2 ->
805           match clearme2 with
806           | ASTint (clearme3, x0) ->
807             (match clearme3 with
808              | I8 ->
809                (fun clearme4 ->
810                  match clearme4 with
811                  | Signed -> Types.Inr __
812                  | Unsigned -> Types.Inr __)
813              | I16 ->
814                (fun clearme4 ->
815                  match clearme4 with
816                  | Signed -> Types.Inr __
817                  | Unsigned -> Types.Inr __)
818              | I32 ->
819                (fun clearme4 ->
820                  match clearme4 with
821                  | Signed -> Types.Inl __
822                  | Unsigned -> Types.Inr __)) x0
823           | ASTptr -> Types.Inr __)
824       | Unsigned ->
825         (fun clearme2 ->
826           match clearme2 with
827           | ASTint (clearme3, x0) ->
828             (match clearme3 with
829              | I8 ->
830                (fun clearme4 ->
831                  match clearme4 with
832                  | Signed -> Types.Inr __
833                  | Unsigned -> Types.Inr __)
834              | I16 ->
835                (fun clearme4 ->
836                  match clearme4 with
837                  | Signed -> Types.Inr __
838                  | Unsigned -> Types.Inr __)
839              | I32 ->
840                (fun clearme4 ->
841                  match clearme4 with
842                  | Signed -> Types.Inr __
843                  | Unsigned -> Types.Inl __)) x0
844           | ASTptr -> Types.Inr __))) x
845| ASTptr ->
846  (fun clearme0 ->
847    match clearme0 with
848    | ASTint (clearme1, x) ->
849      (match clearme1 with
850       | I8 ->
851         (fun clearme2 ->
852           match clearme2 with
853           | Signed -> Types.Inr __
854           | Unsigned -> Types.Inr __)
855       | I16 ->
856         (fun clearme2 ->
857           match clearme2 with
858           | Signed -> Types.Inr __
859           | Unsigned -> Types.Inr __)
860       | I32 ->
861         (fun clearme2 ->
862           match clearme2 with
863           | Signed -> Types.Inr __
864           | Unsigned -> Types.Inr __)) x
865    | ASTptr -> Types.Inl __)
866
867(** val opt_typ_eq :
868    typ Types.option -> typ Types.option -> (__, __) Types.sum **)
869let opt_typ_eq t1 t2 =
870  match t1 with
871  | Types.None ->
872    (match t2 with
873     | Types.None -> Types.Inl __
874     | Types.Some ty -> Types.Inr __)
875  | Types.Some x ->
876    (match t2 with
877     | Types.None -> (fun ty -> Types.Inr __)
878     | Types.Some ty1 ->
879       (fun ty2 ->
880         Types.sum_rect_Type0 (fun _ -> Types.Inl __) (fun _ -> Types.Inr __)
881           (typ_eq ty1 ty2))) x
882
883type signature = { sig_args : typ List.list; sig_res : typ Types.option }
884
885(** val signature_rect_Type4 :
886    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
887let rec signature_rect_Type4 h_mk_signature x_2591 =
888  let { sig_args = sig_args0; sig_res = sig_res0 } = x_2591 in
889  h_mk_signature sig_args0 sig_res0
890
891(** val signature_rect_Type5 :
892    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
893let rec signature_rect_Type5 h_mk_signature x_2593 =
894  let { sig_args = sig_args0; sig_res = sig_res0 } = x_2593 in
895  h_mk_signature sig_args0 sig_res0
896
897(** val signature_rect_Type3 :
898    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
899let rec signature_rect_Type3 h_mk_signature x_2595 =
900  let { sig_args = sig_args0; sig_res = sig_res0 } = x_2595 in
901  h_mk_signature sig_args0 sig_res0
902
903(** val signature_rect_Type2 :
904    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
905let rec signature_rect_Type2 h_mk_signature x_2597 =
906  let { sig_args = sig_args0; sig_res = sig_res0 } = x_2597 in
907  h_mk_signature sig_args0 sig_res0
908
909(** val signature_rect_Type1 :
910    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
911let rec signature_rect_Type1 h_mk_signature x_2599 =
912  let { sig_args = sig_args0; sig_res = sig_res0 } = x_2599 in
913  h_mk_signature sig_args0 sig_res0
914
915(** val signature_rect_Type0 :
916    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
917let rec signature_rect_Type0 h_mk_signature x_2601 =
918  let { sig_args = sig_args0; sig_res = sig_res0 } = x_2601 in
919  h_mk_signature sig_args0 sig_res0
920
921(** val sig_args : signature -> typ List.list **)
922let rec sig_args xxx =
923  xxx.sig_args
924
925(** val sig_res : signature -> typ Types.option **)
926let rec sig_res xxx =
927  xxx.sig_res
928
929(** val signature_inv_rect_Type4 :
930    signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
931let signature_inv_rect_Type4 hterm h1 =
932  let hcut = signature_rect_Type4 h1 hterm in hcut __
933
934(** val signature_inv_rect_Type3 :
935    signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
936let signature_inv_rect_Type3 hterm h1 =
937  let hcut = signature_rect_Type3 h1 hterm in hcut __
938
939(** val signature_inv_rect_Type2 :
940    signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
941let signature_inv_rect_Type2 hterm h1 =
942  let hcut = signature_rect_Type2 h1 hterm in hcut __
943
944(** val signature_inv_rect_Type1 :
945    signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
946let signature_inv_rect_Type1 hterm h1 =
947  let hcut = signature_rect_Type1 h1 hterm in hcut __
948
949(** val signature_inv_rect_Type0 :
950    signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
951let signature_inv_rect_Type0 hterm h1 =
952  let hcut = signature_rect_Type0 h1 hterm in hcut __
953
954(** val signature_discr : signature -> signature -> __ **)
955let signature_discr x y =
956  Logic.eq_rect_Type2 x
957    (let { sig_args = a0; sig_res = a1 } = x in
958    Obj.magic (fun _ dH -> dH __ __)) y
959
960(** val signature_jmdiscr : signature -> signature -> __ **)
961let signature_jmdiscr x y =
962  Logic.eq_rect_Type2 x
963    (let { sig_args = a0; sig_res = a1 } = x in
964    Obj.magic (fun _ dH -> dH __ __)) y
965
966type signature0 = signature
967
968(** val signature_args : signature -> typ List.list **)
969let signature_args =
970  sig_args
971
972(** val signature_return : signature -> typ Types.option **)
973let signature_return =
974  sig_res
975
976(** val proj_sig_res : signature -> typ **)
977let proj_sig_res s =
978  match s.sig_res with
979  | Types.None -> ASTint (I32, Unsigned)
980  | Types.Some t -> t
981
982type init_data =
983| Init_int8 of bvint
984| Init_int16 of bvint
985| Init_int32 of bvint
986| Init_float32 of Floats.float
987| Init_float64 of Floats.float
988| Init_space of Nat.nat
989| Init_null
990| Init_addrof of ident * Nat.nat
991
992(** val init_data_rect_Type4 :
993    (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float ->
994    'a1) -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident ->
995    Nat.nat -> 'a1) -> init_data -> 'a1 **)
996let rec init_data_rect_Type4 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_float32 h_Init_float64 h_Init_space h_Init_null h_Init_addrof = function
997| Init_int8 x_2633 -> h_Init_int8 x_2633
998| Init_int16 x_2634 -> h_Init_int16 x_2634
999| Init_int32 x_2635 -> h_Init_int32 x_2635
1000| Init_float32 x_2636 -> h_Init_float32 x_2636
1001| Init_float64 x_2637 -> h_Init_float64 x_2637
1002| Init_space x_2638 -> h_Init_space x_2638
1003| Init_null -> h_Init_null
1004| Init_addrof (x_2640, x_2639) -> h_Init_addrof x_2640 x_2639
1005
1006(** val init_data_rect_Type5 :
1007    (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float ->
1008    'a1) -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident ->
1009    Nat.nat -> 'a1) -> init_data -> 'a1 **)
1010let rec init_data_rect_Type5 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_float32 h_Init_float64 h_Init_space h_Init_null h_Init_addrof = function
1011| Init_int8 x_2650 -> h_Init_int8 x_2650
1012| Init_int16 x_2651 -> h_Init_int16 x_2651
1013| Init_int32 x_2652 -> h_Init_int32 x_2652
1014| Init_float32 x_2653 -> h_Init_float32 x_2653
1015| Init_float64 x_2654 -> h_Init_float64 x_2654
1016| Init_space x_2655 -> h_Init_space x_2655
1017| Init_null -> h_Init_null
1018| Init_addrof (x_2657, x_2656) -> h_Init_addrof x_2657 x_2656
1019
1020(** val init_data_rect_Type3 :
1021    (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float ->
1022    'a1) -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident ->
1023    Nat.nat -> 'a1) -> init_data -> 'a1 **)
1024let rec init_data_rect_Type3 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_float32 h_Init_float64 h_Init_space h_Init_null h_Init_addrof = function
1025| Init_int8 x_2667 -> h_Init_int8 x_2667
1026| Init_int16 x_2668 -> h_Init_int16 x_2668
1027| Init_int32 x_2669 -> h_Init_int32 x_2669
1028| Init_float32 x_2670 -> h_Init_float32 x_2670
1029| Init_float64 x_2671 -> h_Init_float64 x_2671
1030| Init_space x_2672 -> h_Init_space x_2672
1031| Init_null -> h_Init_null
1032| Init_addrof (x_2674, x_2673) -> h_Init_addrof x_2674 x_2673
1033
1034(** val init_data_rect_Type2 :
1035    (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float ->
1036    'a1) -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident ->
1037    Nat.nat -> 'a1) -> init_data -> 'a1 **)
1038let rec init_data_rect_Type2 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_float32 h_Init_float64 h_Init_space h_Init_null h_Init_addrof = function
1039| Init_int8 x_2684 -> h_Init_int8 x_2684
1040| Init_int16 x_2685 -> h_Init_int16 x_2685
1041| Init_int32 x_2686 -> h_Init_int32 x_2686
1042| Init_float32 x_2687 -> h_Init_float32 x_2687
1043| Init_float64 x_2688 -> h_Init_float64 x_2688
1044| Init_space x_2689 -> h_Init_space x_2689
1045| Init_null -> h_Init_null
1046| Init_addrof (x_2691, x_2690) -> h_Init_addrof x_2691 x_2690
1047
1048(** val init_data_rect_Type1 :
1049    (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float ->
1050    'a1) -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident ->
1051    Nat.nat -> 'a1) -> init_data -> 'a1 **)
1052let rec init_data_rect_Type1 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_float32 h_Init_float64 h_Init_space h_Init_null h_Init_addrof = function
1053| Init_int8 x_2701 -> h_Init_int8 x_2701
1054| Init_int16 x_2702 -> h_Init_int16 x_2702
1055| Init_int32 x_2703 -> h_Init_int32 x_2703
1056| Init_float32 x_2704 -> h_Init_float32 x_2704
1057| Init_float64 x_2705 -> h_Init_float64 x_2705
1058| Init_space x_2706 -> h_Init_space x_2706
1059| Init_null -> h_Init_null
1060| Init_addrof (x_2708, x_2707) -> h_Init_addrof x_2708 x_2707
1061
1062(** val init_data_rect_Type0 :
1063    (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float ->
1064    'a1) -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident ->
1065    Nat.nat -> 'a1) -> init_data -> 'a1 **)
1066let rec init_data_rect_Type0 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_float32 h_Init_float64 h_Init_space h_Init_null h_Init_addrof = function
1067| Init_int8 x_2718 -> h_Init_int8 x_2718
1068| Init_int16 x_2719 -> h_Init_int16 x_2719
1069| Init_int32 x_2720 -> h_Init_int32 x_2720
1070| Init_float32 x_2721 -> h_Init_float32 x_2721
1071| Init_float64 x_2722 -> h_Init_float64 x_2722
1072| Init_space x_2723 -> h_Init_space x_2723
1073| Init_null -> h_Init_null
1074| Init_addrof (x_2725, x_2724) -> h_Init_addrof x_2725 x_2724
1075
1076(** val init_data_inv_rect_Type4 :
1077    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
1078    -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
1079    (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1)
1080    -> 'a1 **)
1081let init_data_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1082  let hcut = init_data_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1083
1084(** val init_data_inv_rect_Type3 :
1085    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
1086    -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
1087    (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1)
1088    -> 'a1 **)
1089let init_data_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1090  let hcut = init_data_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1091
1092(** val init_data_inv_rect_Type2 :
1093    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
1094    -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
1095    (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1)
1096    -> 'a1 **)
1097let init_data_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1098  let hcut = init_data_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1099
1100(** val init_data_inv_rect_Type1 :
1101    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
1102    -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
1103    (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1)
1104    -> 'a1 **)
1105let init_data_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1106  let hcut = init_data_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1107
1108(** val init_data_inv_rect_Type0 :
1109    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
1110    -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
1111    (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1)
1112    -> 'a1 **)
1113let init_data_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1114  let hcut = init_data_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1115
1116(** val init_data_discr : init_data -> init_data -> __ **)
1117let init_data_discr x y =
1118  Logic.eq_rect_Type2 x
1119    (match x with
1120     | Init_int8 a0 -> Obj.magic (fun _ dH -> dH __)
1121     | Init_int16 a0 -> Obj.magic (fun _ dH -> dH __)
1122     | Init_int32 a0 -> Obj.magic (fun _ dH -> dH __)
1123     | Init_float32 a0 -> Obj.magic (fun _ dH -> dH __)
1124     | Init_float64 a0 -> Obj.magic (fun _ dH -> dH __)
1125     | Init_space a0 -> Obj.magic (fun _ dH -> dH __)
1126     | Init_null -> Obj.magic (fun _ dH -> dH)
1127     | Init_addrof (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1128
1129(** val init_data_jmdiscr : init_data -> init_data -> __ **)
1130let init_data_jmdiscr x y =
1131  Logic.eq_rect_Type2 x
1132    (match x with
1133     | Init_int8 a0 -> Obj.magic (fun _ dH -> dH __)
1134     | Init_int16 a0 -> Obj.magic (fun _ dH -> dH __)
1135     | Init_int32 a0 -> Obj.magic (fun _ dH -> dH __)
1136     | Init_float32 a0 -> Obj.magic (fun _ dH -> dH __)
1137     | Init_float64 a0 -> Obj.magic (fun _ dH -> dH __)
1138     | Init_space a0 -> Obj.magic (fun _ dH -> dH __)
1139     | Init_null -> Obj.magic (fun _ dH -> dH)
1140     | Init_addrof (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1141
1142type ('f, 'v) program = { prog_vars : ((ident, region) Types.prod, 'v)
1143                                      Types.prod List.list;
1144                          prog_funct : (ident, 'f) Types.prod List.list;
1145                          prog_main : ident }
1146
1147(** val program_rect_Type4 :
1148    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
1149    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
1150let rec program_rect_Type4 h_mk_program x_2838 =
1151  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1152    prog_main0 } = x_2838
1153  in
1154  h_mk_program prog_vars0 prog_funct0 prog_main0
1155
1156(** val program_rect_Type5 :
1157    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
1158    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
1159let rec program_rect_Type5 h_mk_program x_2840 =
1160  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1161    prog_main0 } = x_2840
1162  in
1163  h_mk_program prog_vars0 prog_funct0 prog_main0
1164
1165(** val program_rect_Type3 :
1166    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
1167    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
1168let rec program_rect_Type3 h_mk_program x_2842 =
1169  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1170    prog_main0 } = x_2842
1171  in
1172  h_mk_program prog_vars0 prog_funct0 prog_main0
1173
1174(** val program_rect_Type2 :
1175    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
1176    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
1177let rec program_rect_Type2 h_mk_program x_2844 =
1178  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1179    prog_main0 } = x_2844
1180  in
1181  h_mk_program prog_vars0 prog_funct0 prog_main0
1182
1183(** val program_rect_Type1 :
1184    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
1185    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
1186let rec program_rect_Type1 h_mk_program x_2846 =
1187  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1188    prog_main0 } = x_2846
1189  in
1190  h_mk_program prog_vars0 prog_funct0 prog_main0
1191
1192(** val program_rect_Type0 :
1193    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
1194    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
1195let rec program_rect_Type0 h_mk_program x_2848 =
1196  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1197    prog_main0 } = x_2848
1198  in
1199  h_mk_program prog_vars0 prog_funct0 prog_main0
1200
1201(** val prog_vars :
1202    ('a1, 'a2) program -> ((ident, region) Types.prod, 'a2) Types.prod
1203    List.list **)
1204let rec prog_vars xxx =
1205  xxx.prog_vars
1206
1207(** val prog_funct :
1208    ('a1, 'a2) program -> (ident, 'a1) Types.prod List.list **)
1209let rec prog_funct xxx =
1210  xxx.prog_funct
1211
1212(** val prog_main : ('a1, 'a2) program -> ident **)
1213let rec prog_main xxx =
1214  xxx.prog_main
1215
1216(** val program_inv_rect_Type4 :
1217    ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
1218    List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
1219    'a3 **)
1220let program_inv_rect_Type4 hterm h1 =
1221  let hcut = program_rect_Type4 h1 hterm in hcut __
1222
1223(** val program_inv_rect_Type3 :
1224    ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
1225    List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
1226    'a3 **)
1227let program_inv_rect_Type3 hterm h1 =
1228  let hcut = program_rect_Type3 h1 hterm in hcut __
1229
1230(** val program_inv_rect_Type2 :
1231    ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
1232    List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
1233    'a3 **)
1234let program_inv_rect_Type2 hterm h1 =
1235  let hcut = program_rect_Type2 h1 hterm in hcut __
1236
1237(** val program_inv_rect_Type1 :
1238    ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
1239    List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
1240    'a3 **)
1241let program_inv_rect_Type1 hterm h1 =
1242  let hcut = program_rect_Type1 h1 hterm in hcut __
1243
1244(** val program_inv_rect_Type0 :
1245    ('a1, 'a2) program -> (((ident, region) Types.prod, 'a2) Types.prod
1246    List.list -> (ident, 'a1) Types.prod List.list -> ident -> __ -> 'a3) ->
1247    'a3 **)
1248let program_inv_rect_Type0 hterm h1 =
1249  let hcut = program_rect_Type0 h1 hterm in hcut __
1250
1251(** val program_discr : ('a1, 'a2) program -> ('a1, 'a2) program -> __ **)
1252let program_discr x y =
1253  Logic.eq_rect_Type2 x
1254    (let { prog_vars = a0; prog_funct = a10; prog_main = a20 } = x in
1255    Obj.magic (fun _ dH -> dH __ __ __)) y
1256
1257(** val program_jmdiscr : ('a1, 'a2) program -> ('a1, 'a2) program -> __ **)
1258let program_jmdiscr x y =
1259  Logic.eq_rect_Type2 x
1260    (let { prog_vars = a0; prog_funct = a10; prog_main = a20 } = x in
1261    Obj.magic (fun _ dH -> dH __ __ __)) y
1262
1263(** val prog_funct_names : ('a1, 'a2) program -> ident List.list **)
1264let prog_funct_names p =
1265  List.map Types.fst p.prog_funct
1266
1267(** val prog_var_names : ('a1, 'a2) program -> ident List.list **)
1268let prog_var_names p =
1269  List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars
1270
1271(** val transf_program :
1272    ('a1 -> 'a2) -> (ident, 'a1) Types.prod List.list -> (ident, 'a2)
1273    Types.prod List.list **)
1274let transf_program transf l =
1275  List.map (fun id_fn -> { Types.fst = id_fn.Types.fst; Types.snd =
1276    (transf id_fn.Types.snd) }) l
1277
1278(** val transform_program :
1279    ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2) -> ('a2, 'a3)
1280    program **)
1281let transform_program p transf =
1282  { prog_vars = p.prog_vars; prog_funct =
1283    (transf_program
1284      (transf (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars))
1285      p.prog_funct); prog_main = p.prog_main }
1286
1287(** val transf_program_gen :
1288    String.string -> Identifiers.universe -> (Identifiers.universe -> 'a1 ->
1289    ('a2, Identifiers.universe) Types.prod) -> (ident, 'a1) Types.prod
1290    List.list -> ((ident, 'a2) Types.prod List.list, Identifiers.universe)
1291    Types.prod **)
1292let transf_program_gen tag gen transf l =
1293  List.foldr (fun id_fn bs_gen ->
1294    let { Types.fst = fn'; Types.snd = gen' } =
1295      transf bs_gen.Types.snd id_fn.Types.snd
1296    in
1297    { Types.fst = (List.Cons ({ Types.fst = id_fn.Types.fst; Types.snd =
1298    fn' }, bs_gen.Types.fst)); Types.snd = gen' }) { Types.fst = List.Nil;
1299    Types.snd = gen } l
1300
1301(** val transform_program_gen :
1302    String.string -> Identifiers.universe -> ('a1, 'a3) program -> (ident
1303    List.list -> Identifiers.universe -> 'a1 -> ('a2, Identifiers.universe)
1304    Types.prod) -> (('a2, 'a3) program, Identifiers.universe) Types.prod **)
1305let transform_program_gen tag gen p trans =
1306  let fsg =
1307    transf_program_gen tag gen
1308      (trans (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars))
1309      p.prog_funct
1310  in
1311  { Types.fst = { prog_vars = p.prog_vars; prog_funct = fsg.Types.fst;
1312  prog_main = p.prog_main }; Types.snd = fsg.Types.snd }
1313
1314(** val map_partial :
1315    ('a2 -> 'a3 Errors.res) -> ('a1, 'a2) Types.prod List.list -> ('a1, 'a3)
1316    Types.prod List.list Errors.res **)
1317let map_partial f =
1318  Obj.magic
1319    (Monad.m_list_map (Monad.max_def Errors.res0) (fun ab ->
1320      let { Types.fst = a; Types.snd = b } = ab in
1321      Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f b) (fun c ->
1322        Obj.magic (Errors.OK { Types.fst = a; Types.snd = c }))))
1323
1324(** val transform_partial_program :
1325    ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2 Errors.res) -> ('a2,
1326    'a3) program Errors.res **)
1327let transform_partial_program p transf_partial =
1328  Obj.magic
1329    (Monad.m_bind0 (Monad.max_def Errors.res0)
1330      (Obj.magic
1331        (map_partial
1332          (transf_partial
1333            (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars))
1334          p.prog_funct)) (fun fl ->
1335      Obj.magic (Errors.OK { prog_vars = p.prog_vars; prog_funct = fl;
1336        prog_main = p.prog_main })))
1337
1338(** val transform_partial_program2 :
1339    ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2 Errors.res) -> ('a3
1340    -> 'a4 Errors.res) -> ('a2, 'a4) program Errors.res **)
1341let transform_partial_program2 p transf_partial_function transf_partial_variable =
1342  Obj.magic
1343    (Monad.m_bind0 (Monad.max_def Errors.res0)
1344      (Obj.magic
1345        (map_partial
1346          (transf_partial_function
1347            (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars))
1348          p.prog_funct)) (fun fl ->
1349      (match map_partial transf_partial_variable p.prog_vars with
1350       | Errors.OK vl ->
1351         (fun _ ->
1352           Obj.magic (Errors.OK { prog_vars = vl; prog_funct =
1353             (Logic.eq_rect_Type0
1354               (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars) fl
1355               (List.map (fun x -> x.Types.fst.Types.fst) vl)); prog_main =
1356             p.prog_main }))
1357       | Errors.Error err -> (fun _ -> Obj.magic (Errors.Error err))) __))
1358
1359type matching =
1360| Mk_matching
1361
1362(** val matching_rect_Type4 :
1363    (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1364let rec matching_rect_Type4 h_mk_matching = function
1365| Mk_matching -> h_mk_matching __ __ __ __ __ __
1366
1367(** val matching_rect_Type5 :
1368    (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1369let rec matching_rect_Type5 h_mk_matching = function
1370| Mk_matching -> h_mk_matching __ __ __ __ __ __
1371
1372(** val matching_rect_Type3 :
1373    (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1374let rec matching_rect_Type3 h_mk_matching = function
1375| Mk_matching -> h_mk_matching __ __ __ __ __ __
1376
1377(** val matching_rect_Type2 :
1378    (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1379let rec matching_rect_Type2 h_mk_matching = function
1380| Mk_matching -> h_mk_matching __ __ __ __ __ __
1381
1382(** val matching_rect_Type1 :
1383    (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1384let rec matching_rect_Type1 h_mk_matching = function
1385| Mk_matching -> h_mk_matching __ __ __ __ __ __
1386
1387(** val matching_rect_Type0 :
1388    (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1389let rec matching_rect_Type0 h_mk_matching = function
1390| Mk_matching -> h_mk_matching __ __ __ __ __ __
1391
1392type m_A = __
1393
1394type m_B = __
1395
1396type m_V = __
1397
1398type m_W = __
1399
1400type match_fundef = __
1401
1402type match_varinfo = __
1403
1404(** val matching_inv_rect_Type4 :
1405    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1406let matching_inv_rect_Type4 hterm h1 =
1407  let hcut = matching_rect_Type4 h1 hterm in hcut __
1408
1409(** val matching_inv_rect_Type3 :
1410    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1411let matching_inv_rect_Type3 hterm h1 =
1412  let hcut = matching_rect_Type3 h1 hterm in hcut __
1413
1414(** val matching_inv_rect_Type2 :
1415    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1416let matching_inv_rect_Type2 hterm h1 =
1417  let hcut = matching_rect_Type2 h1 hterm in hcut __
1418
1419(** val matching_inv_rect_Type1 :
1420    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1421let matching_inv_rect_Type1 hterm h1 =
1422  let hcut = matching_rect_Type1 h1 hterm in hcut __
1423
1424(** val matching_inv_rect_Type0 :
1425    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1426let matching_inv_rect_Type0 hterm h1 =
1427  let hcut = matching_rect_Type0 h1 hterm in hcut __
1428
1429(** val matching_jmdiscr : matching -> matching -> __ **)
1430let matching_jmdiscr x y =
1431  Logic.eq_rect_Type2 x
1432    (let Mk_matching = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1433
1434(** val mfe_cast_fn_type :
1435    matching -> ident List.list -> ident List.list -> __ -> __ **)
1436let mfe_cast_fn_type m vs vs' =
1437  Extralib.eq_rect_Type0_r1 vs (fun m0 -> m0) vs'
1438
1439(** val match_program_rect_Type4 :
1440    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1441    'a1) -> 'a1 **)
1442let rec match_program_rect_Type4 m p3 p4 h_mk_match_program =
1443  h_mk_match_program __ __ __
1444
1445(** val match_program_rect_Type5 :
1446    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1447    'a1) -> 'a1 **)
1448let rec match_program_rect_Type5 m p3 p4 h_mk_match_program =
1449  h_mk_match_program __ __ __
1450
1451(** val match_program_rect_Type3 :
1452    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1453    'a1) -> 'a1 **)
1454let rec match_program_rect_Type3 m p3 p4 h_mk_match_program =
1455  h_mk_match_program __ __ __
1456
1457(** val match_program_rect_Type2 :
1458    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1459    'a1) -> 'a1 **)
1460let rec match_program_rect_Type2 m p3 p4 h_mk_match_program =
1461  h_mk_match_program __ __ __
1462
1463(** val match_program_rect_Type1 :
1464    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1465    'a1) -> 'a1 **)
1466let rec match_program_rect_Type1 m p3 p4 h_mk_match_program =
1467  h_mk_match_program __ __ __
1468
1469(** val match_program_rect_Type0 :
1470    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1471    'a1) -> 'a1 **)
1472let rec match_program_rect_Type0 m p3 p4 h_mk_match_program =
1473  h_mk_match_program __ __ __
1474
1475(** val match_program_inv_rect_Type4 :
1476    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1477    -> 'a1) -> 'a1 **)
1478let match_program_inv_rect_Type4 x1 x2 x3 h1 =
1479  let hcut = match_program_rect_Type4 x1 x2 x3 h1 in hcut __
1480
1481(** val match_program_inv_rect_Type3 :
1482    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1483    -> 'a1) -> 'a1 **)
1484let match_program_inv_rect_Type3 x1 x2 x3 h1 =
1485  let hcut = match_program_rect_Type3 x1 x2 x3 h1 in hcut __
1486
1487(** val match_program_inv_rect_Type2 :
1488    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1489    -> 'a1) -> 'a1 **)
1490let match_program_inv_rect_Type2 x1 x2 x3 h1 =
1491  let hcut = match_program_rect_Type2 x1 x2 x3 h1 in hcut __
1492
1493(** val match_program_inv_rect_Type1 :
1494    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1495    -> 'a1) -> 'a1 **)
1496let match_program_inv_rect_Type1 x1 x2 x3 h1 =
1497  let hcut = match_program_rect_Type1 x1 x2 x3 h1 in hcut __
1498
1499(** val match_program_inv_rect_Type0 :
1500    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1501    -> 'a1) -> 'a1 **)
1502let match_program_inv_rect_Type0 x1 x2 x3 h1 =
1503  let hcut = match_program_rect_Type0 x1 x2 x3 h1 in hcut __
1504
1505(** val match_program_discr :
1506    matching -> (__, __) program -> (__, __) program -> __ **)
1507let match_program_discr a1 a2 a3 =
1508  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1509
1510(** val match_program_jmdiscr :
1511    matching -> (__, __) program -> (__, __) program -> __ **)
1512let match_program_jmdiscr a1 a2 a3 =
1513  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1514
1515type external_function = { ef_id : ident; ef_sig : signature }
1516
1517(** val external_function_rect_Type4 :
1518    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1519let rec external_function_rect_Type4 h_mk_external_function x_3052 =
1520  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3052 in
1521  h_mk_external_function ef_id0 ef_sig0
1522
1523(** val external_function_rect_Type5 :
1524    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1525let rec external_function_rect_Type5 h_mk_external_function x_3054 =
1526  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3054 in
1527  h_mk_external_function ef_id0 ef_sig0
1528
1529(** val external_function_rect_Type3 :
1530    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1531let rec external_function_rect_Type3 h_mk_external_function x_3056 =
1532  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3056 in
1533  h_mk_external_function ef_id0 ef_sig0
1534
1535(** val external_function_rect_Type2 :
1536    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1537let rec external_function_rect_Type2 h_mk_external_function x_3058 =
1538  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3058 in
1539  h_mk_external_function ef_id0 ef_sig0
1540
1541(** val external_function_rect_Type1 :
1542    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1543let rec external_function_rect_Type1 h_mk_external_function x_3060 =
1544  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3060 in
1545  h_mk_external_function ef_id0 ef_sig0
1546
1547(** val external_function_rect_Type0 :
1548    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1549let rec external_function_rect_Type0 h_mk_external_function x_3062 =
1550  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3062 in
1551  h_mk_external_function ef_id0 ef_sig0
1552
1553(** val ef_id : external_function -> ident **)
1554let rec ef_id xxx =
1555  xxx.ef_id
1556
1557(** val ef_sig : external_function -> signature **)
1558let rec ef_sig xxx =
1559  xxx.ef_sig
1560
1561(** val external_function_inv_rect_Type4 :
1562    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1563let external_function_inv_rect_Type4 hterm h1 =
1564  let hcut = external_function_rect_Type4 h1 hterm in hcut __
1565
1566(** val external_function_inv_rect_Type3 :
1567    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1568let external_function_inv_rect_Type3 hterm h1 =
1569  let hcut = external_function_rect_Type3 h1 hterm in hcut __
1570
1571(** val external_function_inv_rect_Type2 :
1572    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1573let external_function_inv_rect_Type2 hterm h1 =
1574  let hcut = external_function_rect_Type2 h1 hterm in hcut __
1575
1576(** val external_function_inv_rect_Type1 :
1577    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1578let external_function_inv_rect_Type1 hterm h1 =
1579  let hcut = external_function_rect_Type1 h1 hterm in hcut __
1580
1581(** val external_function_inv_rect_Type0 :
1582    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1583let external_function_inv_rect_Type0 hterm h1 =
1584  let hcut = external_function_rect_Type0 h1 hterm in hcut __
1585
1586(** val external_function_discr :
1587    external_function -> external_function -> __ **)
1588let external_function_discr x y =
1589  Logic.eq_rect_Type2 x
1590    (let { ef_id = a0; ef_sig = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
1591    y
1592
1593(** val external_function_jmdiscr :
1594    external_function -> external_function -> __ **)
1595let external_function_jmdiscr x y =
1596  Logic.eq_rect_Type2 x
1597    (let { ef_id = a0; ef_sig = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
1598    y
1599
1600type externalFunction = external_function
1601
1602(** val external_function_tag : external_function -> ident **)
1603let external_function_tag =
1604  ef_id
1605
1606(** val external_function_sig : external_function -> signature **)
1607let external_function_sig =
1608  ef_sig
1609
1610type 'f fundef =
1611| Internal of 'f
1612| External of external_function
1613
1614(** val fundef_rect_Type4 :
1615    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1616let rec fundef_rect_Type4 h_Internal h_External = function
1617| Internal x_3082 -> h_Internal x_3082
1618| External x_3083 -> h_External x_3083
1619
1620(** val fundef_rect_Type5 :
1621    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1622let rec fundef_rect_Type5 h_Internal h_External = function
1623| Internal x_3087 -> h_Internal x_3087
1624| External x_3088 -> h_External x_3088
1625
1626(** val fundef_rect_Type3 :
1627    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1628let rec fundef_rect_Type3 h_Internal h_External = function
1629| Internal x_3092 -> h_Internal x_3092
1630| External x_3093 -> h_External x_3093
1631
1632(** val fundef_rect_Type2 :
1633    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1634let rec fundef_rect_Type2 h_Internal h_External = function
1635| Internal x_3097 -> h_Internal x_3097
1636| External x_3098 -> h_External x_3098
1637
1638(** val fundef_rect_Type1 :
1639    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1640let rec fundef_rect_Type1 h_Internal h_External = function
1641| Internal x_3102 -> h_Internal x_3102
1642| External x_3103 -> h_External x_3103
1643
1644(** val fundef_rect_Type0 :
1645    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1646let rec fundef_rect_Type0 h_Internal h_External = function
1647| Internal x_3107 -> h_Internal x_3107
1648| External x_3108 -> h_External x_3108
1649
1650(** val fundef_inv_rect_Type4 :
1651    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1652    'a2 **)
1653let fundef_inv_rect_Type4 hterm h1 h2 =
1654  let hcut = fundef_rect_Type4 h1 h2 hterm in hcut __
1655
1656(** val fundef_inv_rect_Type3 :
1657    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1658    'a2 **)
1659let fundef_inv_rect_Type3 hterm h1 h2 =
1660  let hcut = fundef_rect_Type3 h1 h2 hterm in hcut __
1661
1662(** val fundef_inv_rect_Type2 :
1663    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1664    'a2 **)
1665let fundef_inv_rect_Type2 hterm h1 h2 =
1666  let hcut = fundef_rect_Type2 h1 h2 hterm in hcut __
1667
1668(** val fundef_inv_rect_Type1 :
1669    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1670    'a2 **)
1671let fundef_inv_rect_Type1 hterm h1 h2 =
1672  let hcut = fundef_rect_Type1 h1 h2 hterm in hcut __
1673
1674(** val fundef_inv_rect_Type0 :
1675    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1676    'a2 **)
1677let fundef_inv_rect_Type0 hterm h1 h2 =
1678  let hcut = fundef_rect_Type0 h1 h2 hterm in hcut __
1679
1680(** val fundef_discr : 'a1 fundef -> 'a1 fundef -> __ **)
1681let fundef_discr x y =
1682  Logic.eq_rect_Type2 x
1683    (match x with
1684     | Internal a0 -> Obj.magic (fun _ dH -> dH __)
1685     | External a0 -> Obj.magic (fun _ dH -> dH __)) y
1686
1687(** val fundef_jmdiscr : 'a1 fundef -> 'a1 fundef -> __ **)
1688let fundef_jmdiscr x y =
1689  Logic.eq_rect_Type2 x
1690    (match x with
1691     | Internal a0 -> Obj.magic (fun _ dH -> dH __)
1692     | External a0 -> Obj.magic (fun _ dH -> dH __)) y
1693
1694(** val transf_fundef : ('a1 -> 'a2) -> 'a1 fundef -> 'a2 fundef **)
1695let transf_fundef transf = function
1696| Internal f -> Internal (transf f)
1697| External ef -> External ef
1698
1699(** val transf_partial_fundef :
1700    ('a1 -> 'a2 Errors.res) -> 'a1 fundef -> 'a2 fundef Errors.res **)
1701let transf_partial_fundef transf_partial = function
1702| Internal f ->
1703  Obj.magic
1704    (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic transf_partial f)
1705      (fun f' -> Obj.magic (Errors.OK (Internal f'))))
1706| External ef -> Errors.OK (External ef)
1707
1708type member1 = __
1709
Note: See TracBrowser for help on using the repository browser.