source: extracted/aST.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

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