source: extracted/aST.ml @ 2649

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

...

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