69 type ident = PreIdentifiers.identifier
71 (** val ident_eq : ident -> ident -> (__, __) Types.sum **)
73 Identifiers.identifier_eq PreIdentifiers.SymbolTag
75 (** val ident_of_nat : Nat.nat -> ident **)
77 Identifiers.identifier_of_nat PreIdentifiers.SymbolTag
83 (** val region_rect_Type4 : 'a1 -> 'a1 -> region -> 'a1 **)
84 let rec region_rect_Type4 h_XData h_Code = function
88 (** val region_rect_Type5 : 'a1 -> 'a1 -> region -> 'a1 **)
89 let rec region_rect_Type5 h_XData h_Code = function
93 (** val region_rect_Type3 : 'a1 -> 'a1 -> region -> 'a1 **)
94 let rec region_rect_Type3 h_XData h_Code = function
98 (** val region_rect_Type2 : 'a1 -> 'a1 -> region -> 'a1 **)
99 let rec region_rect_Type2 h_XData h_Code = function
103 (** val region_rect_Type1 : 'a1 -> 'a1 -> region -> 'a1 **)
104 let rec region_rect_Type1 h_XData h_Code = function
108 (** val region_rect_Type0 : 'a1 -> 'a1 -> region -> 'a1 **)
109 let rec region_rect_Type0 h_XData h_Code = function
113 (** val region_inv_rect_Type4 :
114 region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
115 let region_inv_rect_Type4 hterm h1 h2 =
116 let hcut = region_rect_Type4 h1 h2 hterm in hcut __
118 (** val region_inv_rect_Type3 :
119 region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
120 let region_inv_rect_Type3 hterm h1 h2 =
121 let hcut = region_rect_Type3 h1 h2 hterm in hcut __
123 (** val region_inv_rect_Type2 :
124 region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
125 let region_inv_rect_Type2 hterm h1 h2 =
126 let hcut = region_rect_Type2 h1 h2 hterm in hcut __
128 (** val region_inv_rect_Type1 :
129 region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
130 let region_inv_rect_Type1 hterm h1 h2 =
131 let hcut = region_rect_Type1 h1 h2 hterm in hcut __
133 (** val region_inv_rect_Type0 :
134 region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
135 let region_inv_rect_Type0 hterm h1 h2 =
136 let hcut = region_rect_Type0 h1 h2 hterm in hcut __
138 (** val region_discr : region -> region -> __ **)
139 let region_discr x y =
140 Logic.eq_rect_Type2 x
142 | XData -> Obj.magic (fun _ dH -> dH)
143 | Code -> Obj.magic (fun _ dH -> dH)) y
145 (** val region_jmdiscr : region -> region -> __ **)
146 let region_jmdiscr x y =
147 Logic.eq_rect_Type2 x
149 | XData -> Obj.magic (fun _ dH -> dH)
150 | Code -> Obj.magic (fun _ dH -> dH)) y
152 (** val eq_region : region -> region -> Bool.bool **)
153 let eq_region r1 r2 =
158 | Code -> Bool.False)
161 | XData -> Bool.False
164 (** val eq_region_elim :
165 region -> region -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
166 let eq_region_elim r1 r2 =
170 | XData -> (fun ptrue pfalse -> ptrue __)
171 | Code -> (fun ptrue pfalse -> pfalse __))
174 | XData -> (fun ptrue pfalse -> pfalse __)
175 | Code -> (fun ptrue pfalse -> ptrue __))
177 (** val eq_region_dec : region -> region -> (__, __) Types.sum **)
178 let eq_region_dec r1 r2 =
179 eq_region_elim r1 r2 (fun _ -> Types.Inl __) (fun _ -> Types.Inr __)
181 (** val size_pointer : Nat.nat **)
189 (** val signedness_rect_Type4 : 'a1 -> 'a1 -> signedness -> 'a1 **)
190 let rec signedness_rect_Type4 h_Signed h_Unsigned = function
192 | Unsigned -> h_Unsigned
194 (** val signedness_rect_Type5 : 'a1 -> 'a1 -> signedness -> 'a1 **)
195 let rec signedness_rect_Type5 h_Signed h_Unsigned = function
197 | Unsigned -> h_Unsigned
199 (** val signedness_rect_Type3 : 'a1 -> 'a1 -> signedness -> 'a1 **)
200 let rec signedness_rect_Type3 h_Signed h_Unsigned = function
202 | Unsigned -> h_Unsigned
204 (** val signedness_rect_Type2 : 'a1 -> 'a1 -> signedness -> 'a1 **)
205 let rec signedness_rect_Type2 h_Signed h_Unsigned = function
207 | Unsigned -> h_Unsigned
209 (** val signedness_rect_Type1 : 'a1 -> 'a1 -> signedness -> 'a1 **)
210 let rec signedness_rect_Type1 h_Signed h_Unsigned = function
212 | Unsigned -> h_Unsigned
214 (** val signedness_rect_Type0 : 'a1 -> 'a1 -> signedness -> 'a1 **)
215 let rec signedness_rect_Type0 h_Signed h_Unsigned = function
217 | Unsigned -> h_Unsigned
219 (** val signedness_inv_rect_Type4 :
220 signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
221 let signedness_inv_rect_Type4 hterm h1 h2 =
222 let hcut = signedness_rect_Type4 h1 h2 hterm in hcut __
224 (** val signedness_inv_rect_Type3 :
225 signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
226 let signedness_inv_rect_Type3 hterm h1 h2 =
227 let hcut = signedness_rect_Type3 h1 h2 hterm in hcut __
229 (** val signedness_inv_rect_Type2 :
230 signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
231 let signedness_inv_rect_Type2 hterm h1 h2 =
232 let hcut = signedness_rect_Type2 h1 h2 hterm in hcut __
234 (** val signedness_inv_rect_Type1 :
235 signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
236 let signedness_inv_rect_Type1 hterm h1 h2 =
237 let hcut = signedness_rect_Type1 h1 h2 hterm in hcut __
239 (** val signedness_inv_rect_Type0 :
240 signedness -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
241 let signedness_inv_rect_Type0 hterm h1 h2 =
242 let hcut = signedness_rect_Type0 h1 h2 hterm in hcut __
244 (** val signedness_discr : signedness -> signedness -> __ **)
245 let signedness_discr x y =
246 Logic.eq_rect_Type2 x
248 | Signed -> Obj.magic (fun _ dH -> dH)
249 | Unsigned -> Obj.magic (fun _ dH -> dH)) y
251 (** val signedness_jmdiscr : signedness -> signedness -> __ **)
252 let signedness_jmdiscr x y =
253 Logic.eq_rect_Type2 x
255 | Signed -> Obj.magic (fun _ dH -> dH)
256 | Unsigned -> Obj.magic (fun _ dH -> dH)) y
263 (** val intsize_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
264 let rec intsize_rect_Type4 h_I8 h_I16 h_I32 = function
269 (** val intsize_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
270 let rec intsize_rect_Type5 h_I8 h_I16 h_I32 = function
275 (** val intsize_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
276 let rec intsize_rect_Type3 h_I8 h_I16 h_I32 = function
281 (** val intsize_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
282 let rec intsize_rect_Type2 h_I8 h_I16 h_I32 = function
287 (** val intsize_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
288 let rec intsize_rect_Type1 h_I8 h_I16 h_I32 = function
293 (** val intsize_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> intsize -> 'a1 **)
294 let rec intsize_rect_Type0 h_I8 h_I16 h_I32 = function
299 (** val intsize_inv_rect_Type4 :
300 intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
301 let intsize_inv_rect_Type4 hterm h1 h2 h3 =
302 let hcut = intsize_rect_Type4 h1 h2 h3 hterm in hcut __
304 (** val intsize_inv_rect_Type3 :
305 intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
306 let intsize_inv_rect_Type3 hterm h1 h2 h3 =
307 let hcut = intsize_rect_Type3 h1 h2 h3 hterm in hcut __
309 (** val intsize_inv_rect_Type2 :
310 intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
311 let intsize_inv_rect_Type2 hterm h1 h2 h3 =
312 let hcut = intsize_rect_Type2 h1 h2 h3 hterm in hcut __
314 (** val intsize_inv_rect_Type1 :
315 intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
316 let intsize_inv_rect_Type1 hterm h1 h2 h3 =
317 let hcut = intsize_rect_Type1 h1 h2 h3 hterm in hcut __
319 (** val intsize_inv_rect_Type0 :
320 intsize -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
321 let intsize_inv_rect_Type0 hterm h1 h2 h3 =
322 let hcut = intsize_rect_Type0 h1 h2 h3 hterm in hcut __
324 (** val intsize_discr : intsize -> intsize -> __ **)
325 let intsize_discr x y =
326 Logic.eq_rect_Type2 x
328 | I8 -> Obj.magic (fun _ dH -> dH)
329 | I16 -> Obj.magic (fun _ dH -> dH)
330 | I32 -> Obj.magic (fun _ dH -> dH)) y
332 (** val intsize_jmdiscr : intsize -> intsize -> __ **)
333 let intsize_jmdiscr x y =
334 Logic.eq_rect_Type2 x
336 | I8 -> Obj.magic (fun _ dH -> dH)
337 | I16 -> Obj.magic (fun _ dH -> dH)
338 | I32 -> Obj.magic (fun _ dH -> dH)) y
344 (** val floatsize_rect_Type4 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
345 let rec floatsize_rect_Type4 h_F32 h_F64 = function
349 (** val floatsize_rect_Type5 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
350 let rec floatsize_rect_Type5 h_F32 h_F64 = function
354 (** val floatsize_rect_Type3 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
355 let rec floatsize_rect_Type3 h_F32 h_F64 = function
359 (** val floatsize_rect_Type2 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
360 let rec floatsize_rect_Type2 h_F32 h_F64 = function
364 (** val floatsize_rect_Type1 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
365 let rec floatsize_rect_Type1 h_F32 h_F64 = function
369 (** val floatsize_rect_Type0 : 'a1 -> 'a1 -> floatsize -> 'a1 **)
370 let rec floatsize_rect_Type0 h_F32 h_F64 = function
374 (** val floatsize_inv_rect_Type4 :
375 floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
376 let floatsize_inv_rect_Type4 hterm h1 h2 =
377 let hcut = floatsize_rect_Type4 h1 h2 hterm in hcut __
379 (** val floatsize_inv_rect_Type3 :
380 floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
381 let floatsize_inv_rect_Type3 hterm h1 h2 =
382 let hcut = floatsize_rect_Type3 h1 h2 hterm in hcut __
384 (** val floatsize_inv_rect_Type2 :
385 floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
386 let floatsize_inv_rect_Type2 hterm h1 h2 =
387 let hcut = floatsize_rect_Type2 h1 h2 hterm in hcut __
389 (** val floatsize_inv_rect_Type1 :
390 floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
391 let floatsize_inv_rect_Type1 hterm h1 h2 =
392 let hcut = floatsize_rect_Type1 h1 h2 hterm in hcut __
394 (** val floatsize_inv_rect_Type0 :
395 floatsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
396 let floatsize_inv_rect_Type0 hterm h1 h2 =
397 let hcut = floatsize_rect_Type0 h1 h2 hterm in hcut __
399 (** val floatsize_discr : floatsize -> floatsize -> __ **)
400 let floatsize_discr x y =
401 Logic.eq_rect_Type2 x
403 | F32 -> Obj.magic (fun _ dH -> dH)
404 | F64 -> Obj.magic (fun _ dH -> dH)) y
406 (** val floatsize_jmdiscr : floatsize -> floatsize -> __ **)
407 let floatsize_jmdiscr x y =
408 Logic.eq_rect_Type2 x
410 | F32 -> Obj.magic (fun _ dH -> dH)
411 | F64 -> Obj.magic (fun _ dH -> dH)) y
414 | ASTint of intsize * signedness
417 (** val typ_rect_Type4 :
418 (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
419 let rec typ_rect_Type4 h_ASTint h_ASTptr = function
420 | ASTint (x_3662, x_3661) -> h_ASTint x_3662 x_3661
423 (** val typ_rect_Type5 :
424 (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
425 let rec typ_rect_Type5 h_ASTint h_ASTptr = function
426 | ASTint (x_3667, x_3666) -> h_ASTint x_3667 x_3666
429 (** val typ_rect_Type3 :
430 (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
431 let rec typ_rect_Type3 h_ASTint h_ASTptr = function
432 | ASTint (x_3672, x_3671) -> h_ASTint x_3672 x_3671
435 (** val typ_rect_Type2 :
436 (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
437 let rec typ_rect_Type2 h_ASTint h_ASTptr = function
438 | ASTint (x_3677, x_3676) -> h_ASTint x_3677 x_3676
441 (** val typ_rect_Type1 :
442 (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
443 let rec typ_rect_Type1 h_ASTint h_ASTptr = function
444 | ASTint (x_3682, x_3681) -> h_ASTint x_3682 x_3681
447 (** val typ_rect_Type0 :
448 (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
449 let rec typ_rect_Type0 h_ASTint h_ASTptr = function
450 | ASTint (x_3687, x_3686) -> h_ASTint x_3687 x_3686
453 (** val typ_inv_rect_Type4 :
454 typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
455 let typ_inv_rect_Type4 hterm h1 h2 =
456 let hcut = typ_rect_Type4 h1 h2 hterm in hcut __
458 (** val typ_inv_rect_Type3 :
459 typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
460 let typ_inv_rect_Type3 hterm h1 h2 =
461 let hcut = typ_rect_Type3 h1 h2 hterm in hcut __
463 (** val typ_inv_rect_Type2 :
464 typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
465 let typ_inv_rect_Type2 hterm h1 h2 =
466 let hcut = typ_rect_Type2 h1 h2 hterm in hcut __
468 (** val typ_inv_rect_Type1 :
469 typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
470 let typ_inv_rect_Type1 hterm h1 h2 =
471 let hcut = typ_rect_Type1 h1 h2 hterm in hcut __
473 (** val typ_inv_rect_Type0 :
474 typ -> (intsize -> signedness -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
475 let typ_inv_rect_Type0 hterm h1 h2 =
476 let hcut = typ_rect_Type0 h1 h2 hterm in hcut __
478 (** val typ_discr : typ -> typ -> __ **)
480 Logic.eq_rect_Type2 x
482 | ASTint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
483 | ASTptr -> Obj.magic (fun _ dH -> dH)) y
485 (** val typ_jmdiscr : typ -> typ -> __ **)
486 let typ_jmdiscr x y =
487 Logic.eq_rect_Type2 x
489 | ASTint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
490 | ASTptr -> Obj.magic (fun _ dH -> dH)) y
494 (** val sigType_Int : typ **)
496 ASTint (I32, Unsigned)
498 (** val sigType_Ptr : typ **)
502 (** val pred_size_intsize : intsize -> Nat.nat **)
503 let pred_size_intsize = function
506 | I32 -> Nat.S (Nat.S (Nat.S Nat.O))
508 (** val size_intsize : intsize -> Nat.nat **)
509 let size_intsize sz =
510 Nat.S (pred_size_intsize sz)
512 (** val bitsize_of_intsize : intsize -> Nat.nat **)
513 let 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))))))))
517 (** val eq_intsize : intsize -> intsize -> Bool.bool **)
518 let eq_intsize sz1 sz2 =
536 (** val eq_intsize_elim :
537 intsize -> intsize -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
538 let eq_intsize_elim clearme sz2 x x0 =
543 | I8 -> (fun _ hne heq -> heq __)
544 | I16 -> (fun _ hne heq -> hne __)
545 | I32 -> (fun _ hne heq -> hne __))
549 | I8 -> (fun _ hne heq -> hne __)
550 | I16 -> (fun _ hne heq -> heq __)
551 | I32 -> (fun _ hne heq -> hne __))
555 | I8 -> (fun _ hne heq -> hne __)
556 | I16 -> (fun _ hne heq -> hne __)
557 | I32 -> (fun _ hne heq -> heq __))) sz2 __ x x0
559 (** val signedness_check : signedness -> signedness -> 'a1 -> 'a1 -> 'a1 **)
560 let signedness_check sg1 sg2 =
565 | Signed -> (fun d -> x)
566 | Unsigned -> (fun d -> d))
570 | Signed -> (fun d -> d)
571 | Unsigned -> (fun d -> x))
573 (** val inttyp_eq_elim' :
574 intsize -> intsize -> signedness -> signedness -> 'a1 -> 'a1 -> 'a1 **)
575 let rec inttyp_eq_elim' sz1 sz2 sg1 sg2 =
580 | I8 -> signedness_check sg1 sg2 x
581 | I16 -> (fun d -> d)
582 | I32 -> (fun d -> d))
587 | I16 -> signedness_check sg1 sg2 x
588 | I32 -> (fun d -> d))
593 | I16 -> (fun d -> d)
594 | I32 -> signedness_check sg1 sg2 x)
596 (** val intsize_eq_elim' : intsize -> intsize -> 'a1 -> 'a1 -> 'a1 **)
597 let rec intsize_eq_elim' sz1 sz2 =
603 | I16 -> (fun d -> d)
604 | I32 -> (fun d -> d))
609 | I16 -> (fun d -> x)
610 | I32 -> (fun d -> d))
615 | I16 -> (fun d -> d)
616 | I32 -> (fun d -> x))
618 (** val intsize_eq_elim :
619 intsize -> intsize -> 'a2 -> ('a2 -> 'a1) -> 'a1 -> 'a1 **)
620 let rec intsize_eq_elim sz1 sz2 =
625 | I8 -> (fun f d -> f x)
626 | I16 -> (fun f d -> d)
627 | I32 -> (fun f d -> d))
631 | I8 -> (fun f d -> d)
632 | I16 -> (fun f d -> f x)
633 | I32 -> (fun f d -> d))
637 | I8 -> (fun f d -> d)
638 | I16 -> (fun f d -> d)
639 | I32 -> (fun f d -> f x))
641 (** val intsize_eq_elim_elim :
642 intsize -> intsize -> 'a2 -> ('a2 -> 'a1) -> 'a1 -> (__ -> 'a3) -> (__ ->
644 let intsize_eq_elim_elim clearme sz2 p f d x x0 =
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 __))
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 __))
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
666 type bvint = BitVector.bitVector
668 (** val repr : intsize -> Nat.nat -> bvint **)
670 Arithmetic.bitvector_of_nat (bitsize_of_intsize sz) x
672 (** val size_floatsize : floatsize -> Nat.nat **)
673 let size_floatsize sz =
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)))))))
679 (** val floatsize_eq_elim : floatsize -> floatsize -> 'a1 -> 'a1 -> 'a1 **)
680 let rec floatsize_eq_elim sz1 sz2 =
685 | F32 -> (fun d -> x)
686 | F64 -> (fun d -> d))
690 | F32 -> (fun d -> d)
691 | F64 -> (fun d -> x))
693 (** val typesize : typ -> Nat.nat **)
694 let typesize = function
695 | ASTint (sz, x) -> size_intsize sz
696 | ASTptr -> size_pointer
698 (** val typ_eq : typ -> typ -> (__, __) Types.sum **)
699 let typ_eq = function
700 | ASTint (clearme0, x) ->
708 | ASTint (clearme3, x0) ->
713 | Signed -> Types.Inl __
714 | Unsigned -> Types.Inr __)
718 | Signed -> Types.Inr __
719 | Unsigned -> Types.Inr __)
723 | Signed -> Types.Inr __
724 | Unsigned -> Types.Inr __)) x0
725 | ASTptr -> Types.Inr __)
729 | ASTint (clearme3, x0) ->
734 | Signed -> Types.Inr __
735 | Unsigned -> Types.Inl __)
739 | Signed -> Types.Inr __
740 | Unsigned -> Types.Inr __)
744 | Signed -> Types.Inr __
745 | Unsigned -> Types.Inr __)) x0
746 | ASTptr -> Types.Inr __))
753 | ASTint (clearme3, x0) ->
758 | Signed -> Types.Inr __
759 | Unsigned -> Types.Inr __)
763 | Signed -> Types.Inl __
764 | Unsigned -> Types.Inr __)
768 | Signed -> Types.Inr __
769 | Unsigned -> Types.Inr __)) x0
770 | ASTptr -> Types.Inr __)
774 | ASTint (clearme3, x0) ->
779 | Signed -> Types.Inr __
780 | Unsigned -> Types.Inr __)
784 | Signed -> Types.Inr __
785 | Unsigned -> Types.Inl __)
789 | Signed -> Types.Inr __
790 | Unsigned -> Types.Inr __)) x0
791 | ASTptr -> Types.Inr __))
798 | ASTint (clearme3, x0) ->
803 | Signed -> Types.Inr __
804 | Unsigned -> Types.Inr __)
808 | Signed -> Types.Inr __
809 | Unsigned -> Types.Inr __)
813 | Signed -> Types.Inl __
814 | Unsigned -> Types.Inr __)) x0
815 | ASTptr -> Types.Inr __)
819 | ASTint (clearme3, x0) ->
824 | Signed -> Types.Inr __
825 | Unsigned -> Types.Inr __)
829 | Signed -> Types.Inr __
830 | Unsigned -> Types.Inr __)
834 | Signed -> Types.Inr __
835 | Unsigned -> Types.Inl __)) x0
836 | ASTptr -> Types.Inr __))) x
840 | ASTint (clearme1, x) ->
845 | Signed -> Types.Inr __
846 | Unsigned -> Types.Inr __)
850 | Signed -> Types.Inr __
851 | Unsigned -> Types.Inr __)
855 | Signed -> Types.Inr __
856 | Unsigned -> Types.Inr __)) x
857 | ASTptr -> Types.Inl __)
860 typ Types.option -> typ Types.option -> (__, __) Types.sum **)
861 let opt_typ_eq t1 t2 =
865 | Types.None -> Types.Inl __
866 | Types.Some ty -> Types.Inr __)
869 | Types.None -> (fun ty -> Types.Inr __)
872 Types.sum_rect_Type0 (fun _ -> Types.Inl __) (fun _ -> Types.Inr __)
875 type signature = { sig_args : typ List.list; sig_res : typ Types.option }
877 (** val signature_rect_Type4 :
878 (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
879 let 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
883 (** val signature_rect_Type5 :
884 (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
885 let 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
889 (** val signature_rect_Type3 :
890 (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
891 let 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
895 (** val signature_rect_Type2 :
896 (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
897 let 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
901 (** val signature_rect_Type1 :
902 (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
903 let 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
907 (** val signature_rect_Type0 :
908 (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
909 let 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
913 (** val sig_args : signature -> typ List.list **)
914 let rec sig_args xxx =
917 (** val sig_res : signature -> typ Types.option **)
918 let rec sig_res xxx =
921 (** val signature_inv_rect_Type4 :
922 signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
923 let signature_inv_rect_Type4 hterm h1 =
924 let hcut = signature_rect_Type4 h1 hterm in hcut __
926 (** val signature_inv_rect_Type3 :
927 signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
928 let signature_inv_rect_Type3 hterm h1 =
929 let hcut = signature_rect_Type3 h1 hterm in hcut __
931 (** val signature_inv_rect_Type2 :
932 signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
933 let signature_inv_rect_Type2 hterm h1 =
934 let hcut = signature_rect_Type2 h1 hterm in hcut __
936 (** val signature_inv_rect_Type1 :
937 signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
938 let signature_inv_rect_Type1 hterm h1 =
939 let hcut = signature_rect_Type1 h1 hterm in hcut __
941 (** val signature_inv_rect_Type0 :
942 signature -> (typ List.list -> typ Types.option -> __ -> 'a1) -> 'a1 **)
943 let signature_inv_rect_Type0 hterm h1 =
944 let hcut = signature_rect_Type0 h1 hterm in hcut __
946 (** val signature_discr : signature -> signature -> __ **)
947 let 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
952 (** val signature_jmdiscr : signature -> signature -> __ **)
953 let 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
958 type signature0 = signature
960 (** val signature_args : signature -> typ List.list **)
964 (** val signature_return : signature -> typ Types.option **)
965 let signature_return =
968 (** val proj_sig_res : signature -> typ **)
971 | Types.None -> ASTint (I32, Unsigned)
976 | Init_int16 of bvint
977 | Init_int32 of bvint
978 | Init_space of Nat.nat
980 | Init_addrof of ident * Nat.nat
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 **)
985 let 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
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 **)
996 let 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
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 **)
1007 let 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
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 **)
1018 let 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
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 **)
1029 let 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
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 **)
1040 let 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
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 **)
1052 let 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 __
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 **)
1059 let 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 __
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 **)
1066 let 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 __
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 **)
1073 let 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 __
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 **)
1080 let 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 __
1083 (** val init_data_discr : init_data -> init_data -> __ **)
1084 let init_data_discr x y =
1085 Logic.eq_rect_Type2 x
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
1094 (** val init_data_jmdiscr : init_data -> init_data -> __ **)
1095 let init_data_jmdiscr x y =
1096 Logic.eq_rect_Type2 x
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
1105 type ('f, 'v) program = { prog_vars : ((ident, region) Types.prod, 'v)
1106 Types.prod List.list;
1107 prog_funct : (ident, 'f) Types.prod List.list;
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 **)
1113 let 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
1117 h_mk_program prog_vars0 prog_funct0 prog_main0
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 **)
1122 let 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
1126 h_mk_program prog_vars0 prog_funct0 prog_main0
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 **)
1131 let 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
1135 h_mk_program prog_vars0 prog_funct0 prog_main0
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 **)
1140 let 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
1144 h_mk_program prog_vars0 prog_funct0 prog_main0
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 **)
1149 let 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
1153 h_mk_program prog_vars0 prog_funct0 prog_main0
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 **)
1158 let 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
1162 h_mk_program prog_vars0 prog_funct0 prog_main0
1165 ('a1, 'a2) program -> ((ident, region) Types.prod, 'a2) Types.prod
1167 let rec prog_vars xxx =
1170 (** val prog_funct :
1171 ('a1, 'a2) program -> (ident, 'a1) Types.prod List.list **)
1172 let rec prog_funct xxx =
1175 (** val prog_main : ('a1, 'a2) program -> ident **)
1176 let rec prog_main xxx =
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) ->
1183 let program_inv_rect_Type4 hterm h1 =
1184 let hcut = program_rect_Type4 h1 hterm in hcut __
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) ->
1190 let program_inv_rect_Type3 hterm h1 =
1191 let hcut = program_rect_Type3 h1 hterm in hcut __
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) ->
1197 let program_inv_rect_Type2 hterm h1 =
1198 let hcut = program_rect_Type2 h1 hterm in hcut __
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) ->
1204 let program_inv_rect_Type1 hterm h1 =
1205 let hcut = program_rect_Type1 h1 hterm in hcut __
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) ->
1211 let program_inv_rect_Type0 hterm h1 =
1212 let hcut = program_rect_Type0 h1 hterm in hcut __
1214 (** val program_discr : ('a1, 'a2) program -> ('a1, 'a2) program -> __ **)
1215 let 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
1220 (** val program_jmdiscr : ('a1, 'a2) program -> ('a1, 'a2) program -> __ **)
1221 let 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
1226 (** val prog_funct_names : ('a1, 'a2) program -> ident List.list **)
1227 let prog_funct_names p =
1228 List.map Types.fst p.prog_funct
1230 (** val prog_var_names : ('a1, 'a2) program -> ident List.list **)
1231 let prog_var_names p =
1232 List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars
1234 (** val transf_program :
1235 ('a1 -> 'a2) -> (ident, 'a1) Types.prod List.list -> (ident, 'a2)
1236 Types.prod List.list **)
1237 let 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
1241 (** val transform_program :
1242 ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2) -> ('a2, 'a3)
1244 let transform_program p transf =
1245 { prog_vars = p.prog_vars; prog_funct =
1247 (transf (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars))
1248 p.prog_funct); prog_main = p.prog_main }
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 **)
1255 let 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
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;
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 **)
1269 let transform_program_gen tag gen p trans =
1271 transf_program_gen tag gen
1272 (trans (List.map (fun x -> x.Types.fst.Types.fst) p.prog_vars))
1275 { Types.fst = { prog_vars = p.prog_vars; prog_funct = fsg.Types.fst;
1276 prog_main = p.prog_main }; Types.snd = fsg.Types.snd }
1278 (** val map_partial :
1279 ('a2 -> 'a3 Errors.res) -> ('a1, 'a2) Types.prod List.list -> ('a1, 'a3)
1280 Types.prod List.list Errors.res **)
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 }))))
1288 (** val transform_partial_program :
1289 ('a1, 'a3) program -> (ident List.list -> 'a1 -> 'a2 Errors.res) -> ('a2,
1290 'a3) program Errors.res **)
1291 let transform_partial_program p transf_partial =
1293 (Monad.m_bind0 (Monad.max_def Errors.res0)
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 })))
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 **)
1305 let transform_partial_program2 p transf_partial_function transf_partial_variable =
1307 (Monad.m_bind0 (Monad.max_def Errors.res0)
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
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 =
1321 | Errors.Error err -> (fun _ -> Obj.magic (Errors.Error err))) __))
1326 (** val matching_rect_Type4 :
1327 (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1328 let rec matching_rect_Type4 h_mk_matching = function
1329 | Mk_matching -> h_mk_matching __ __ __ __ __ __
1331 (** val matching_rect_Type5 :
1332 (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1333 let rec matching_rect_Type5 h_mk_matching = function
1334 | Mk_matching -> h_mk_matching __ __ __ __ __ __
1336 (** val matching_rect_Type3 :
1337 (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1338 let rec matching_rect_Type3 h_mk_matching = function
1339 | Mk_matching -> h_mk_matching __ __ __ __ __ __
1341 (** val matching_rect_Type2 :
1342 (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1343 let rec matching_rect_Type2 h_mk_matching = function
1344 | Mk_matching -> h_mk_matching __ __ __ __ __ __
1346 (** val matching_rect_Type1 :
1347 (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1348 let rec matching_rect_Type1 h_mk_matching = function
1349 | Mk_matching -> h_mk_matching __ __ __ __ __ __
1351 (** val matching_rect_Type0 :
1352 (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> matching -> 'a1 **)
1353 let rec matching_rect_Type0 h_mk_matching = function
1354 | Mk_matching -> h_mk_matching __ __ __ __ __ __
1364 (** val matching_inv_rect_Type4 :
1365 matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1366 let matching_inv_rect_Type4 hterm h1 =
1367 let hcut = matching_rect_Type4 h1 hterm in hcut __
1369 (** val matching_inv_rect_Type3 :
1370 matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1371 let matching_inv_rect_Type3 hterm h1 =
1372 let hcut = matching_rect_Type3 h1 hterm in hcut __
1374 (** val matching_inv_rect_Type2 :
1375 matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1376 let matching_inv_rect_Type2 hterm h1 =
1377 let hcut = matching_rect_Type2 h1 hterm in hcut __
1379 (** val matching_inv_rect_Type1 :
1380 matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1381 let matching_inv_rect_Type1 hterm h1 =
1382 let hcut = matching_rect_Type1 h1 hterm in hcut __
1384 (** val matching_inv_rect_Type0 :
1385 matching -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1386 let matching_inv_rect_Type0 hterm h1 =
1387 let hcut = matching_rect_Type0 h1 hterm in hcut __
1389 (** val matching_jmdiscr : matching -> matching -> __ **)
1390 let matching_jmdiscr x y =
1391 Logic.eq_rect_Type2 x
1392 (let Mk_matching = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1394 (** val mfe_cast_fn_type :
1395 matching -> ident List.list -> ident List.list -> __ -> __ **)
1396 let mfe_cast_fn_type m vs vs' =
1397 Extralib.eq_rect_Type0_r vs (fun m0 -> m0) vs'
1399 (** val match_program_rect_Type4 :
1400 matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1402 let rec match_program_rect_Type4 m p1 p2 h_mk_match_program =
1403 h_mk_match_program __ __ __
1405 (** val match_program_rect_Type5 :
1406 matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1408 let rec match_program_rect_Type5 m p1 p2 h_mk_match_program =
1409 h_mk_match_program __ __ __
1411 (** val match_program_rect_Type3 :
1412 matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1414 let rec match_program_rect_Type3 m p1 p2 h_mk_match_program =
1415 h_mk_match_program __ __ __
1417 (** val match_program_rect_Type2 :
1418 matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1420 let rec match_program_rect_Type2 m p1 p2 h_mk_match_program =
1421 h_mk_match_program __ __ __
1423 (** val match_program_rect_Type1 :
1424 matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1426 let rec match_program_rect_Type1 m p1 p2 h_mk_match_program =
1427 h_mk_match_program __ __ __
1429 (** val match_program_rect_Type0 :
1430 matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ ->
1432 let rec match_program_rect_Type0 m p1 p2 h_mk_match_program =
1433 h_mk_match_program __ __ __
1435 (** val match_program_inv_rect_Type4 :
1436 matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1438 let match_program_inv_rect_Type4 x1 x2 x3 h1 =
1439 let hcut = match_program_rect_Type4 x1 x2 x3 h1 in hcut __
1441 (** val match_program_inv_rect_Type3 :
1442 matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1444 let match_program_inv_rect_Type3 x1 x2 x3 h1 =
1445 let hcut = match_program_rect_Type3 x1 x2 x3 h1 in hcut __
1447 (** val match_program_inv_rect_Type2 :
1448 matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1450 let match_program_inv_rect_Type2 x1 x2 x3 h1 =
1451 let hcut = match_program_rect_Type2 x1 x2 x3 h1 in hcut __
1453 (** val match_program_inv_rect_Type1 :
1454 matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1456 let match_program_inv_rect_Type1 x1 x2 x3 h1 =
1457 let hcut = match_program_rect_Type1 x1 x2 x3 h1 in hcut __
1459 (** val match_program_inv_rect_Type0 :
1460 matching -> (__, __) program -> (__, __) program -> (__ -> __ -> __ -> __
1462 let match_program_inv_rect_Type0 x1 x2 x3 h1 =
1463 let hcut = match_program_rect_Type0 x1 x2 x3 h1 in hcut __
1465 (** val match_program_discr :
1466 matching -> (__, __) program -> (__, __) program -> __ **)
1467 let match_program_discr a1 a2 a3 =
1468 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1470 (** val match_program_jmdiscr :
1471 matching -> (__, __) program -> (__, __) program -> __ **)
1472 let match_program_jmdiscr a1 a2 a3 =
1473 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
1475 type external_function = { ef_id : ident; ef_sig : signature }
1477 (** val external_function_rect_Type4 :
1478 (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1479 let 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
1483 (** val external_function_rect_Type5 :
1484 (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1485 let 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
1489 (** val external_function_rect_Type3 :
1490 (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1491 let 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
1495 (** val external_function_rect_Type2 :
1496 (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1497 let 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
1501 (** val external_function_rect_Type1 :
1502 (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1503 let 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
1507 (** val external_function_rect_Type0 :
1508 (ident -> signature -> 'a1) -> external_function -> 'a1 **)
1509 let 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
1513 (** val ef_id : external_function -> ident **)
1517 (** val ef_sig : external_function -> signature **)
1518 let rec ef_sig xxx =
1521 (** val external_function_inv_rect_Type4 :
1522 external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1523 let external_function_inv_rect_Type4 hterm h1 =
1524 let hcut = external_function_rect_Type4 h1 hterm in hcut __
1526 (** val external_function_inv_rect_Type3 :
1527 external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1528 let external_function_inv_rect_Type3 hterm h1 =
1529 let hcut = external_function_rect_Type3 h1 hterm in hcut __
1531 (** val external_function_inv_rect_Type2 :
1532 external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1533 let external_function_inv_rect_Type2 hterm h1 =
1534 let hcut = external_function_rect_Type2 h1 hterm in hcut __
1536 (** val external_function_inv_rect_Type1 :
1537 external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1538 let external_function_inv_rect_Type1 hterm h1 =
1539 let hcut = external_function_rect_Type1 h1 hterm in hcut __
1541 (** val external_function_inv_rect_Type0 :
1542 external_function -> (ident -> signature -> __ -> 'a1) -> 'a1 **)
1543 let external_function_inv_rect_Type0 hterm h1 =
1544 let hcut = external_function_rect_Type0 h1 hterm in hcut __
1546 (** val external_function_discr :
1547 external_function -> external_function -> __ **)
1548 let 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 __ __))
1553 (** val external_function_jmdiscr :
1554 external_function -> external_function -> __ **)
1555 let 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 __ __))
1560 type externalFunction = external_function
1562 (** val external_function_tag : external_function -> ident **)
1563 let external_function_tag =
1566 (** val external_function_sig : external_function -> signature **)
1567 let external_function_sig =
1572 | External of external_function
1574 (** val fundef_rect_Type4 :
1575 ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1576 let 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
1580 (** val fundef_rect_Type5 :
1581 ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1582 let 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
1586 (** val fundef_rect_Type3 :
1587 ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1588 let 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
1592 (** val fundef_rect_Type2 :
1593 ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1594 let 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
1598 (** val fundef_rect_Type1 :
1599 ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1600 let 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
1604 (** val fundef_rect_Type0 :
1605 ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
1606 let 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
1610 (** val fundef_inv_rect_Type4 :
1611 'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1613 let fundef_inv_rect_Type4 hterm h1 h2 =
1614 let hcut = fundef_rect_Type4 h1 h2 hterm in hcut __
1616 (** val fundef_inv_rect_Type3 :
1617 'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1619 let fundef_inv_rect_Type3 hterm h1 h2 =
1620 let hcut = fundef_rect_Type3 h1 h2 hterm in hcut __
1622 (** val fundef_inv_rect_Type2 :
1623 'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1625 let fundef_inv_rect_Type2 hterm h1 h2 =
1626 let hcut = fundef_rect_Type2 h1 h2 hterm in hcut __
1628 (** val fundef_inv_rect_Type1 :
1629 'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1631 let fundef_inv_rect_Type1 hterm h1 h2 =
1632 let hcut = fundef_rect_Type1 h1 h2 hterm in hcut __
1634 (** val fundef_inv_rect_Type0 :
1635 'a1 fundef -> ('a1 -> __ -> 'a2) -> (external_function -> __ -> 'a2) ->
1637 let fundef_inv_rect_Type0 hterm h1 h2 =
1638 let hcut = fundef_rect_Type0 h1 h2 hterm in hcut __
1640 (** val fundef_discr : 'a1 fundef -> 'a1 fundef -> __ **)
1641 let fundef_discr x y =
1642 Logic.eq_rect_Type2 x
1644 | Internal a0 -> Obj.magic (fun _ dH -> dH __)
1645 | External a0 -> Obj.magic (fun _ dH -> dH __)) y
1647 (** val fundef_jmdiscr : 'a1 fundef -> 'a1 fundef -> __ **)
1648 let fundef_jmdiscr x y =
1649 Logic.eq_rect_Type2 x
1651 | Internal a0 -> Obj.magic (fun _ dH -> dH __)
1652 | External a0 -> Obj.magic (fun _ dH -> dH __)) y
1654 (** val transf_fundef : ('a1 -> 'a2) -> 'a1 fundef -> 'a2 fundef **)
1655 let transf_fundef transf = function
1656 | Internal f -> Internal (transf f)
1657 | External ef -> External ef
1659 (** val transf_partial_fundef :
1660 ('a1 -> 'a2 Errors.res) -> 'a1 fundef -> 'a2 fundef Errors.res **)
1661 let transf_partial_fundef transf_partial = function
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)