source: driver/extracted/aST.ml @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 55.3 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Exp
14
15open Arithmetic
16
17open Vector
18
19open Div_and_mod
20
21open Util
22
23open FoldStuff
24
25open BitVector
26
27open Jmeq
28
29open Russell
30
31open List
32
33open Setoids
34
35open Monad
36
37open Option
38
39open Extranat
40
41open Bool
42
43open Relations
44
45open Nat
46
47open Integers
48
49open Proper
50
51open PositiveMap
52
53open Deqsets
54
55open ErrorMessages
56
57open PreIdentifiers
58
59open Errors
60
61open Extralib
62
63open Lists
64
65open Positive
66
67open Identifiers
68
69type ident = PreIdentifiers.identifier
70
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 r1 r2 =
154  match r1 with
155  | XData ->
156    (match r2 with
157     | XData -> Bool.True
158     | Code -> Bool.False)
159  | Code ->
160    (match r2 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 r1 r2 =
167  match r1 with
168  | XData ->
169    (match r2 with
170     | XData -> (fun ptrue pfalse -> ptrue __)
171     | Code -> (fun ptrue pfalse -> pfalse __))
172  | Code ->
173    (match r2 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 r1 r2 =
179  eq_region_elim r1 r2 (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_3662, x_3661) -> h_ASTint x_3662 x_3661
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_3667, x_3666) -> h_ASTint x_3667 x_3666
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_3672, x_3671) -> h_ASTint x_3672 x_3671
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_3677, x_3676) -> h_ASTint x_3677 x_3676
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_3682, x_3681) -> h_ASTint x_3682 x_3681
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_3687, x_3686) -> h_ASTint x_3687 x_3686
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 repr : intsize -> Nat.nat -> bvint **)
669let repr 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_3722 =
880  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3722 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_3724 =
886  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3724 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_3726 =
892  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3726 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_3728 =
898  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3728 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_3730 =
904  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3730 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_3732 =
910  let { sig_args = sig_args0; sig_res = sig_res0 } = x_3732 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_3760 -> h_Init_int8 x_3760
987| Init_int16 x_3761 -> h_Init_int16 x_3761
988| Init_int32 x_3762 -> h_Init_int32 x_3762
989| Init_space x_3763 -> h_Init_space x_3763
990| Init_null -> h_Init_null
991| Init_addrof (x_3765, x_3764) -> h_Init_addrof x_3765 x_3764
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_3773 -> h_Init_int8 x_3773
998| Init_int16 x_3774 -> h_Init_int16 x_3774
999| Init_int32 x_3775 -> h_Init_int32 x_3775
1000| Init_space x_3776 -> h_Init_space x_3776
1001| Init_null -> h_Init_null
1002| Init_addrof (x_3778, x_3777) -> h_Init_addrof x_3778 x_3777
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_3786 -> h_Init_int8 x_3786
1009| Init_int16 x_3787 -> h_Init_int16 x_3787
1010| Init_int32 x_3788 -> h_Init_int32 x_3788
1011| Init_space x_3789 -> h_Init_space x_3789
1012| Init_null -> h_Init_null
1013| Init_addrof (x_3791, x_3790) -> h_Init_addrof x_3791 x_3790
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_3799 -> h_Init_int8 x_3799
1020| Init_int16 x_3800 -> h_Init_int16 x_3800
1021| Init_int32 x_3801 -> h_Init_int32 x_3801
1022| Init_space x_3802 -> h_Init_space x_3802
1023| Init_null -> h_Init_null
1024| Init_addrof (x_3804, x_3803) -> h_Init_addrof x_3804 x_3803
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_3812 -> h_Init_int8 x_3812
1031| Init_int16 x_3813 -> h_Init_int16 x_3813
1032| Init_int32 x_3814 -> h_Init_int32 x_3814
1033| Init_space x_3815 -> h_Init_space x_3815
1034| Init_null -> h_Init_null
1035| Init_addrof (x_3817, x_3816) -> h_Init_addrof x_3817 x_3816
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_3825 -> h_Init_int8 x_3825
1042| Init_int16 x_3826 -> h_Init_int16 x_3826
1043| Init_int32 x_3827 -> h_Init_int32 x_3827
1044| Init_space x_3828 -> h_Init_space x_3828
1045| Init_null -> h_Init_null
1046| Init_addrof (x_3830, x_3829) -> h_Init_addrof x_3830 x_3829
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_3917 =
1114  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1115    prog_main0 } = x_3917
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_3919 =
1123  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1124    prog_main0 } = x_3919
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_3921 =
1132  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1133    prog_main0 } = x_3921
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_3923 =
1141  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1142    prog_main0 } = x_3923
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_3925 =
1150  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1151    prog_main0 } = x_3925
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_3927 =
1159  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
1160    prog_main0 } = x_3927
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
1364(** val matching_inv_rect_Type4 :
1365    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1366let matching_inv_rect_Type4 hterm h1 =
1367  let hcut = matching_rect_Type4 h1 hterm in hcut __
1368
1369(** val matching_inv_rect_Type3 :
1370    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1371let matching_inv_rect_Type3 hterm h1 =
1372  let hcut = matching_rect_Type3 h1 hterm in hcut __
1373
1374(** val matching_inv_rect_Type2 :
1375    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1376let matching_inv_rect_Type2 hterm h1 =
1377  let hcut = matching_rect_Type2 h1 hterm in hcut __
1378
1379(** val matching_inv_rect_Type1 :
1380    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1381let matching_inv_rect_Type1 hterm h1 =
1382  let hcut = matching_rect_Type1 h1 hterm in hcut __
1383
1384(** val matching_inv_rect_Type0 :
1385    matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1386let matching_inv_rect_Type0 hterm h1 =
1387  let hcut = matching_rect_Type0 h1 hterm in hcut __
1388
1389(** val matching_jmdiscr : matching -> matching -> __ **)
1390let matching_jmdiscr x y =
1391  Logic.eq_rect_Type2 x
1392    (let Mk_matching = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1393
1394(** val mfe_cast_fn_type :
1395    matching -> ident List.list -> ident List.list -> __ -> __ **)
1396let mfe_cast_fn_type m vs vs' =
1397  Extralib.eq_rect_Type0_r vs (fun m0 -> m0) vs'
1398
1399(** val match_program_rect_Type4 :
1400    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1401    'a1) -> 'a1 **)
1402let rec match_program_rect_Type4 m p1 p2 h_mk_match_program =
1403  h_mk_match_program __ __ __
1404
1405(** val match_program_rect_Type5 :
1406    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1407    'a1) -> 'a1 **)
1408let rec match_program_rect_Type5 m p1 p2 h_mk_match_program =
1409  h_mk_match_program __ __ __
1410
1411(** val match_program_rect_Type3 :
1412    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1413    'a1) -> 'a1 **)
1414let rec match_program_rect_Type3 m p1 p2 h_mk_match_program =
1415  h_mk_match_program __ __ __
1416
1417(** val match_program_rect_Type2 :
1418    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1419    'a1) -> 'a1 **)
1420let rec match_program_rect_Type2 m p1 p2 h_mk_match_program =
1421  h_mk_match_program __ __ __
1422
1423(** val match_program_rect_Type1 :
1424    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1425    'a1) -> 'a1 **)
1426let rec match_program_rect_Type1 m p1 p2 h_mk_match_program =
1427  h_mk_match_program __ __ __
1428
1429(** val match_program_rect_Type0 :
1430    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1431    'a1) -> 'a1 **)
1432let rec match_program_rect_Type0 m p1 p2 h_mk_match_program =
1433  h_mk_match_program __ __ __
1434
1435(** val match_program_inv_rect_Type4 :
1436    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1437    -> 'a1) -> 'a1 **)
1438let match_program_inv_rect_Type4 x1 x2 x3 h1 =
1439  let hcut = match_program_rect_Type4 x1 x2 x3 h1 in hcut __
1440
1441(** val match_program_inv_rect_Type3 :
1442    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1443    -> 'a1) -> 'a1 **)
1444let match_program_inv_rect_Type3 x1 x2 x3 h1 =
1445  let hcut = match_program_rect_Type3 x1 x2 x3 h1 in hcut __
1446
1447(** val match_program_inv_rect_Type2 :
1448    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1449    -> 'a1) -> 'a1 **)
1450let match_program_inv_rect_Type2 x1 x2 x3 h1 =
1451  let hcut = match_program_rect_Type2 x1 x2 x3 h1 in hcut __
1452
1453(** val match_program_inv_rect_Type1 :
1454    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1455    -> 'a1) -> 'a1 **)
1456let match_program_inv_rect_Type1 x1 x2 x3 h1 =
1457  let hcut = match_program_rect_Type1 x1 x2 x3 h1 in hcut __
1458
1459(** val match_program_inv_rect_Type0 :
1460    matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1461    -> 'a1) -> 'a1 **)
1462let match_program_inv_rect_Type0 x1 x2 x3 h1 =
1463  let hcut = match_program_rect_Type0 x1 x2 x3 h1 in hcut __
1464
1465(** val match_program_discr :
1466    matching -> (__, __) program -> (__, __) program -> __ **)
1467let match_program_discr a1 a2 a3 =
1468  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1469
1470(** val match_program_jmdiscr :
1471    matching -> (__, __) program -> (__, __) program -> __ **)
1472let match_program_jmdiscr a1 a2 a3 =
1473  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1474
1475type external_function = { ef_id : ident; ef_sig : signature }
1476
1477(** val external_function_rect_Type4 :
1478    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1479let rec external_function_rect_Type4 h_mk_external_function x_4131 =
1480  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4131 in
1481  h_mk_external_function ef_id0 ef_sig0
1482
1483(** val external_function_rect_Type5 :
1484    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1485let rec external_function_rect_Type5 h_mk_external_function x_4133 =
1486  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4133 in
1487  h_mk_external_function ef_id0 ef_sig0
1488
1489(** val external_function_rect_Type3 :
1490    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1491let rec external_function_rect_Type3 h_mk_external_function x_4135 =
1492  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4135 in
1493  h_mk_external_function ef_id0 ef_sig0
1494
1495(** val external_function_rect_Type2 :
1496    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1497let rec external_function_rect_Type2 h_mk_external_function x_4137 =
1498  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4137 in
1499  h_mk_external_function ef_id0 ef_sig0
1500
1501(** val external_function_rect_Type1 :
1502    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1503let rec external_function_rect_Type1 h_mk_external_function x_4139 =
1504  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4139 in
1505  h_mk_external_function ef_id0 ef_sig0
1506
1507(** val external_function_rect_Type0 :
1508    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1509let rec external_function_rect_Type0 h_mk_external_function x_4141 =
1510  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4141 in
1511  h_mk_external_function ef_id0 ef_sig0
1512
1513(** val ef_id : external_function -> ident **)
1514let rec ef_id xxx =
1515  xxx.ef_id
1516
1517(** val ef_sig : external_function -> signature **)
1518let rec ef_sig xxx =
1519  xxx.ef_sig
1520
1521(** val external_function_inv_rect_Type4 :
1522    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1523let external_function_inv_rect_Type4 hterm h1 =
1524  let hcut = external_function_rect_Type4 h1 hterm in hcut __
1525
1526(** val external_function_inv_rect_Type3 :
1527    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1528let external_function_inv_rect_Type3 hterm h1 =
1529  let hcut = external_function_rect_Type3 h1 hterm in hcut __
1530
1531(** val external_function_inv_rect_Type2 :
1532    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1533let external_function_inv_rect_Type2 hterm h1 =
1534  let hcut = external_function_rect_Type2 h1 hterm in hcut __
1535
1536(** val external_function_inv_rect_Type1 :
1537    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1538let external_function_inv_rect_Type1 hterm h1 =
1539  let hcut = external_function_rect_Type1 h1 hterm in hcut __
1540
1541(** val external_function_inv_rect_Type0 :
1542    external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1543let external_function_inv_rect_Type0 hterm h1 =
1544  let hcut = external_function_rect_Type0 h1 hterm in hcut __
1545
1546(** val external_function_discr :
1547    external_function -> external_function -> __ **)
1548let external_function_discr x y =
1549  Logic.eq_rect_Type2 x
1550    (let { ef_id = a0; ef_sig = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
1551    y
1552
1553(** val external_function_jmdiscr :
1554    external_function -> external_function -> __ **)
1555let external_function_jmdiscr x y =
1556  Logic.eq_rect_Type2 x
1557    (let { ef_id = a0; ef_sig = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
1558    y
1559
1560type externalFunction = external_function
1561
1562(** val external_function_tag : external_function -> ident **)
1563let external_function_tag =
1564  ef_id
1565
1566(** val external_function_sig : external_function -> signature **)
1567let external_function_sig =
1568  ef_sig
1569
1570type 'f fundef =
1571| Internal of 'f
1572| External of external_function
1573
1574(** val fundef_rect_Type4 :
1575    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1576let rec fundef_rect_Type4 h_Internal h_External = function
1577| Internal x_4161 -> h_Internal x_4161
1578| External x_4162 -> h_External x_4162
1579
1580(** val fundef_rect_Type5 :
1581    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1582let rec fundef_rect_Type5 h_Internal h_External = function
1583| Internal x_4166 -> h_Internal x_4166
1584| External x_4167 -> h_External x_4167
1585
1586(** val fundef_rect_Type3 :
1587    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1588let rec fundef_rect_Type3 h_Internal h_External = function
1589| Internal x_4171 -> h_Internal x_4171
1590| External x_4172 -> h_External x_4172
1591
1592(** val fundef_rect_Type2 :
1593    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1594let rec fundef_rect_Type2 h_Internal h_External = function
1595| Internal x_4176 -> h_Internal x_4176
1596| External x_4177 -> h_External x_4177
1597
1598(** val fundef_rect_Type1 :
1599    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1600let rec fundef_rect_Type1 h_Internal h_External = function
1601| Internal x_4181 -> h_Internal x_4181
1602| External x_4182 -> h_External x_4182
1603
1604(** val fundef_rect_Type0 :
1605    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1606let rec fundef_rect_Type0 h_Internal h_External = function
1607| Internal x_4186 -> h_Internal x_4186
1608| External x_4187 -> h_External x_4187
1609
1610(** val fundef_inv_rect_Type4 :
1611    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1612    'a2 **)
1613let fundef_inv_rect_Type4 hterm h1 h2 =
1614  let hcut = fundef_rect_Type4 h1 h2 hterm in hcut __
1615
1616(** val fundef_inv_rect_Type3 :
1617    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1618    'a2 **)
1619let fundef_inv_rect_Type3 hterm h1 h2 =
1620  let hcut = fundef_rect_Type3 h1 h2 hterm in hcut __
1621
1622(** val fundef_inv_rect_Type2 :
1623    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1624    'a2 **)
1625let fundef_inv_rect_Type2 hterm h1 h2 =
1626  let hcut = fundef_rect_Type2 h1 h2 hterm in hcut __
1627
1628(** val fundef_inv_rect_Type1 :
1629    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1630    'a2 **)
1631let fundef_inv_rect_Type1 hterm h1 h2 =
1632  let hcut = fundef_rect_Type1 h1 h2 hterm in hcut __
1633
1634(** val fundef_inv_rect_Type0 :
1635    'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1636    'a2 **)
1637let fundef_inv_rect_Type0 hterm h1 h2 =
1638  let hcut = fundef_rect_Type0 h1 h2 hterm in hcut __
1639
1640(** val fundef_discr : 'a1 fundef -> 'a1 fundef -> __ **)
1641let fundef_discr x y =
1642  Logic.eq_rect_Type2 x
1643    (match x with
1644     | Internal a0 -> Obj.magic (fun _ dH -> dH __)
1645     | External a0 -> Obj.magic (fun _ dH -> dH __)) y
1646
1647(** val fundef_jmdiscr : 'a1 fundef -> 'a1 fundef -> __ **)
1648let fundef_jmdiscr x y =
1649  Logic.eq_rect_Type2 x
1650    (match x with
1651     | Internal a0 -> Obj.magic (fun _ dH -> dH __)
1652     | External a0 -> Obj.magic (fun _ dH -> dH __)) y
1653
1654(** val transf_fundef : ('a1 -> 'a2) -> 'a1 fundef -> 'a2 fundef **)
1655let transf_fundef transf = function
1656| Internal f -> Internal (transf f)
1657| External ef -> External ef
1658
1659(** val transf_partial_fundef :
1660    ('a1 -> 'a2 Errors.res) -> 'a1 fundef -> 'a2 fundef Errors.res **)
1661let transf_partial_fundef transf_partial = function
1662| Internal f ->
1663  Obj.magic
1664    (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic transf_partial f)
1665      (fun f' -> Obj.magic (Errors.OK (Internal f'))))
1666| External ef -> Errors.OK (External ef)
1667
Note: See TracBrowser for help on using the repository browser.