Changeset 2649 for extracted/aST.ml


Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/aST.ml

    r2601 r2649  
    1313open Arithmetic
    1414
    15 open Char
    16 
    17 open String
    18 
    1915open Vector
    2016
     
    4339open Integers
    4440
    45 open Coqlib
    46 
    47 open Floats
    48 
    4941open Proper
    5042
     
    5345open Deqsets
    5446
     47open ErrorMessages
     48
    5549open PreIdentifiers
    5650
     
    7064
    7165open Identifiers
    72 
    73 (** val symbolTag : String.string **)
    74 let symbolTag = "symbolTag"
    75   (* failwith "AXIOM TO BE REALIZED" *)
    7666
    7767type ident = PreIdentifiers.identifier
     
    7969(** val ident_eq : ident -> ident -> (__, __) Types.sum **)
    8070let ident_eq =
    81   Identifiers.identifier_eq symbolTag
     71  Identifiers.identifier_eq PreIdentifiers.SymbolTag
    8272
    8373(** val ident_of_nat : Nat.nat -> ident **)
    8474let ident_of_nat =
    85   Identifiers.identifier_of_nat symbolTag
     75  Identifiers.identifier_of_nat PreIdentifiers.SymbolTag
    8676
    8777type region =
     
    426416    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    427417let rec typ_rect_Type4 h_ASTint h_ASTptr = function
    428 | ASTint (x_2531, x_2530) -> h_ASTint x_2531 x_2530
     418| ASTint (x_1373, x_1372) -> h_ASTint x_1373 x_1372
    429419| ASTptr -> h_ASTptr
    430420
     
    432422    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    433423let rec typ_rect_Type5 h_ASTint h_ASTptr = function
    434 | ASTint (x_2536, x_2535) -> h_ASTint x_2536 x_2535
     424| ASTint (x_1378, x_1377) -> h_ASTint x_1378 x_1377
    435425| ASTptr -> h_ASTptr
    436426
     
    438428    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    439429let rec typ_rect_Type3 h_ASTint h_ASTptr = function
    440 | ASTint (x_2541, x_2540) -> h_ASTint x_2541 x_2540
     430| ASTint (x_1383, x_1382) -> h_ASTint x_1383 x_1382
    441431| ASTptr -> h_ASTptr
    442432
     
    444434    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    445435let rec typ_rect_Type2 h_ASTint h_ASTptr = function
    446 | ASTint (x_2546, x_2545) -> h_ASTint x_2546 x_2545
     436| ASTint (x_1388, x_1387) -> h_ASTint x_1388 x_1387
    447437| ASTptr -> h_ASTptr
    448438
     
    450440    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    451441let rec typ_rect_Type1 h_ASTint h_ASTptr = function
    452 | ASTint (x_2551, x_2550) -> h_ASTint x_2551 x_2550
     442| ASTint (x_1393, x_1392) -> h_ASTint x_1393 x_1392
    453443| ASTptr -> h_ASTptr
    454444
     
    456446    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    457447let rec typ_rect_Type0 h_ASTint h_ASTptr = function
    458 | ASTint (x_2556, x_2555) -> h_ASTint x_2556 x_2555
     448| ASTint (x_1398, x_1397) -> h_ASTint x_1398 x_1397
    459449| ASTptr -> h_ASTptr
    460450
     
    885875(** val signature_rect_Type4 :
    886876    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    887 let rec signature_rect_Type4 h_mk_signature x_2591 =
    888   let { sig_args = sig_args0; sig_res = sig_res0 } = x_2591 in
     877let rec signature_rect_Type4 h_mk_signature x_1433 =
     878  let { sig_args = sig_args0; sig_res = sig_res0 } = x_1433 in
    889879  h_mk_signature sig_args0 sig_res0
    890880
    891881(** val signature_rect_Type5 :
    892882    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    893 let rec signature_rect_Type5 h_mk_signature x_2593 =
    894   let { sig_args = sig_args0; sig_res = sig_res0 } = x_2593 in
     883let rec signature_rect_Type5 h_mk_signature x_1435 =
     884  let { sig_args = sig_args0; sig_res = sig_res0 } = x_1435 in
    895885  h_mk_signature sig_args0 sig_res0
    896886
    897887(** val signature_rect_Type3 :
    898888    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    899 let rec signature_rect_Type3 h_mk_signature x_2595 =
    900   let { sig_args = sig_args0; sig_res = sig_res0 } = x_2595 in
     889let rec signature_rect_Type3 h_mk_signature x_1437 =
     890  let { sig_args = sig_args0; sig_res = sig_res0 } = x_1437 in
    901891  h_mk_signature sig_args0 sig_res0
    902892
    903893(** val signature_rect_Type2 :
    904894    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    905 let rec signature_rect_Type2 h_mk_signature x_2597 =
    906   let { sig_args = sig_args0; sig_res = sig_res0 } = x_2597 in
     895let rec signature_rect_Type2 h_mk_signature x_1439 =
     896  let { sig_args = sig_args0; sig_res = sig_res0 } = x_1439 in
    907897  h_mk_signature sig_args0 sig_res0
    908898
    909899(** val signature_rect_Type1 :
    910900    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    911 let rec signature_rect_Type1 h_mk_signature x_2599 =
    912   let { sig_args = sig_args0; sig_res = sig_res0 } = x_2599 in
     901let rec signature_rect_Type1 h_mk_signature x_1441 =
     902  let { sig_args = sig_args0; sig_res = sig_res0 } = x_1441 in
    913903  h_mk_signature sig_args0 sig_res0
    914904
    915905(** val signature_rect_Type0 :
    916906    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    917 let rec signature_rect_Type0 h_mk_signature x_2601 =
    918   let { sig_args = sig_args0; sig_res = sig_res0 } = x_2601 in
     907let rec signature_rect_Type0 h_mk_signature x_1443 =
     908  let { sig_args = sig_args0; sig_res = sig_res0 } = x_1443 in
    919909  h_mk_signature sig_args0 sig_res0
    920910
     
    984974| Init_int16 of bvint
    985975| Init_int32 of bvint
    986 | Init_float32 of Floats.float
    987 | Init_float64 of Floats.float
    988976| Init_space of Nat.nat
    989977| Init_null
     
    991979
    992980(** val init_data_rect_Type4 :
    993     (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float ->
    994     'a1) -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident ->
    995     Nat.nat -> 'a1) -> init_data -> 'a1 **)
    996 let rec init_data_rect_Type4 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_float32 h_Init_float64 h_Init_space h_Init_null h_Init_addrof = function
    997 | Init_int8 x_2633 -> h_Init_int8 x_2633
    998 | Init_int16 x_2634 -> h_Init_int16 x_2634
    999 | Init_int32 x_2635 -> h_Init_int32 x_2635
    1000 | Init_float32 x_2636 -> h_Init_float32 x_2636
    1001 | Init_float64 x_2637 -> h_Init_float64 x_2637
    1002 | Init_space x_2638 -> h_Init_space x_2638
     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
    1003988| Init_null -> h_Init_null
    1004 | Init_addrof (x_2640, x_2639) -> h_Init_addrof x_2640 x_2639
     989| Init_addrof (x_1476, x_1475) -> h_Init_addrof x_1476 x_1475
    1005990
    1006991(** val init_data_rect_Type5 :
    1007     (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float ->
    1008     'a1) -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident ->
    1009     Nat.nat -> 'a1) -> init_data -> 'a1 **)
    1010 let rec init_data_rect_Type5 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_float32 h_Init_float64 h_Init_space h_Init_null h_Init_addrof = function
    1011 | Init_int8 x_2650 -> h_Init_int8 x_2650
    1012 | Init_int16 x_2651 -> h_Init_int16 x_2651
    1013 | Init_int32 x_2652 -> h_Init_int32 x_2652
    1014 | Init_float32 x_2653 -> h_Init_float32 x_2653
    1015 | Init_float64 x_2654 -> h_Init_float64 x_2654
    1016 | Init_space x_2655 -> h_Init_space x_2655
     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
    1017999| Init_null -> h_Init_null
    1018 | Init_addrof (x_2657, x_2656) -> h_Init_addrof x_2657 x_2656
     1000| Init_addrof (x_1489, x_1488) -> h_Init_addrof x_1489 x_1488
    10191001
    10201002(** val init_data_rect_Type3 :
    1021     (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float ->
    1022     'a1) -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident ->
    1023     Nat.nat -> 'a1) -> init_data -> 'a1 **)
    1024 let rec init_data_rect_Type3 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_float32 h_Init_float64 h_Init_space h_Init_null h_Init_addrof = function
    1025 | Init_int8 x_2667 -> h_Init_int8 x_2667
    1026 | Init_int16 x_2668 -> h_Init_int16 x_2668
    1027 | Init_int32 x_2669 -> h_Init_int32 x_2669
    1028 | Init_float32 x_2670 -> h_Init_float32 x_2670
    1029 | Init_float64 x_2671 -> h_Init_float64 x_2671
    1030 | Init_space x_2672 -> h_Init_space x_2672
     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
    10311010| Init_null -> h_Init_null
    1032 | Init_addrof (x_2674, x_2673) -> h_Init_addrof x_2674 x_2673
     1011| Init_addrof (x_1502, x_1501) -> h_Init_addrof x_1502 x_1501
    10331012
    10341013(** val init_data_rect_Type2 :
    1035     (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float ->
    1036     'a1) -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident ->
    1037     Nat.nat -> 'a1) -> init_data -> 'a1 **)
    1038 let rec init_data_rect_Type2 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_float32 h_Init_float64 h_Init_space h_Init_null h_Init_addrof = function
    1039 | Init_int8 x_2684 -> h_Init_int8 x_2684
    1040 | Init_int16 x_2685 -> h_Init_int16 x_2685
    1041 | Init_int32 x_2686 -> h_Init_int32 x_2686
    1042 | Init_float32 x_2687 -> h_Init_float32 x_2687
    1043 | Init_float64 x_2688 -> h_Init_float64 x_2688
    1044 | Init_space x_2689 -> h_Init_space x_2689
     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
    10451021| Init_null -> h_Init_null
    1046 | Init_addrof (x_2691, x_2690) -> h_Init_addrof x_2691 x_2690
     1022| Init_addrof (x_1515, x_1514) -> h_Init_addrof x_1515 x_1514
    10471023
    10481024(** val init_data_rect_Type1 :
    1049     (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float ->
    1050     'a1) -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident ->
    1051     Nat.nat -> 'a1) -> init_data -> 'a1 **)
    1052 let rec init_data_rect_Type1 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_float32 h_Init_float64 h_Init_space h_Init_null h_Init_addrof = function
    1053 | Init_int8 x_2701 -> h_Init_int8 x_2701
    1054 | Init_int16 x_2702 -> h_Init_int16 x_2702
    1055 | Init_int32 x_2703 -> h_Init_int32 x_2703
    1056 | Init_float32 x_2704 -> h_Init_float32 x_2704
    1057 | Init_float64 x_2705 -> h_Init_float64 x_2705
    1058 | Init_space x_2706 -> h_Init_space x_2706
     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
    10591032| Init_null -> h_Init_null
    1060 | Init_addrof (x_2708, x_2707) -> h_Init_addrof x_2708 x_2707
     1033| Init_addrof (x_1528, x_1527) -> h_Init_addrof x_1528 x_1527
    10611034
    10621035(** val init_data_rect_Type0 :
    1063     (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float ->
    1064     'a1) -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident ->
    1065     Nat.nat -> 'a1) -> init_data -> 'a1 **)
    1066 let rec init_data_rect_Type0 h_Init_int8 h_Init_int16 h_Init_int32 h_Init_float32 h_Init_float64 h_Init_space h_Init_null h_Init_addrof = function
    1067 | Init_int8 x_2718 -> h_Init_int8 x_2718
    1068 | Init_int16 x_2719 -> h_Init_int16 x_2719
    1069 | Init_int32 x_2720 -> h_Init_int32 x_2720
    1070 | Init_float32 x_2721 -> h_Init_float32 x_2721
    1071 | Init_float64 x_2722 -> h_Init_float64 x_2722
    1072 | Init_space x_2723 -> h_Init_space x_2723
     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
    10731043| Init_null -> h_Init_null
    1074 | Init_addrof (x_2725, x_2724) -> h_Init_addrof x_2725 x_2724
     1044| Init_addrof (x_1541, x_1540) -> h_Init_addrof x_1541 x_1540
    10751045
    10761046(** val init_data_inv_rect_Type4 :
    10771047    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    1078     -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
    1079     (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1)
    1080     -> 'a1 **)
    1081 let init_data_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    1082   let hcut = init_data_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
     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 __
    10831052
    10841053(** val init_data_inv_rect_Type3 :
    10851054    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    1086     -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
    1087     (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1)
    1088     -> 'a1 **)
    1089 let init_data_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    1090   let hcut = init_data_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
     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 __
    10911059
    10921060(** val init_data_inv_rect_Type2 :
    10931061    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    1094     -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
    1095     (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1)
    1096     -> 'a1 **)
    1097 let init_data_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    1098   let hcut = init_data_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
     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 __
    10991066
    11001067(** val init_data_inv_rect_Type1 :
    11011068    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    1102     -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
    1103     (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1)
    1104     -> 'a1 **)
    1105 let init_data_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    1106   let hcut = init_data_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
     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 __
    11071073
    11081074(** val init_data_inv_rect_Type0 :
    11091075    init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    1110     -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
    1111     (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1)
    1112     -> 'a1 **)
    1113 let init_data_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
    1114   let hcut = init_data_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
     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 __
    11151080
    11161081(** val init_data_discr : init_data -> init_data -> __ **)
     
    11211086     | Init_int16 a0 -> Obj.magic (fun _ dH -> dH __)
    11221087     | Init_int32 a0 -> Obj.magic (fun _ dH -> dH __)
    1123      | Init_float32 a0 -> Obj.magic (fun _ dH -> dH __)
    1124      | Init_float64 a0 -> Obj.magic (fun _ dH -> dH __)
    11251088     | Init_space a0 -> Obj.magic (fun _ dH -> dH __)
    11261089     | Init_null -> Obj.magic (fun _ dH -> dH)
     
    11341097     | Init_int16 a0 -> Obj.magic (fun _ dH -> dH __)
    11351098     | Init_int32 a0 -> Obj.magic (fun _ dH -> dH __)
    1136      | Init_float32 a0 -> Obj.magic (fun _ dH -> dH __)
    1137      | Init_float64 a0 -> Obj.magic (fun _ dH -> dH __)
    11381099     | Init_space a0 -> Obj.magic (fun _ dH -> dH __)
    11391100     | Init_null -> Obj.magic (fun _ dH -> dH)
     
    11481109    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11491110    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1150 let rec program_rect_Type4 h_mk_program x_2838 =
     1111let rec program_rect_Type4 h_mk_program x_1628 =
    11511112  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1152     prog_main0 } = x_2838
     1113    prog_main0 } = x_1628
    11531114  in
    11541115  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11571118    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11581119    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1159 let rec program_rect_Type5 h_mk_program x_2840 =
     1120let rec program_rect_Type5 h_mk_program x_1630 =
    11601121  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1161     prog_main0 } = x_2840
     1122    prog_main0 } = x_1630
    11621123  in
    11631124  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11661127    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11671128    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1168 let rec program_rect_Type3 h_mk_program x_2842 =
     1129let rec program_rect_Type3 h_mk_program x_1632 =
    11691130  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1170     prog_main0 } = x_2842
     1131    prog_main0 } = x_1632
    11711132  in
    11721133  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11751136    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11761137    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1177 let rec program_rect_Type2 h_mk_program x_2844 =
     1138let rec program_rect_Type2 h_mk_program x_1634 =
    11781139  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1179     prog_main0 } = x_2844
     1140    prog_main0 } = x_1634
    11801141  in
    11811142  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11841145    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11851146    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1186 let rec program_rect_Type1 h_mk_program x_2846 =
     1147let rec program_rect_Type1 h_mk_program x_1636 =
    11871148  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1188     prog_main0 } = x_2846
     1149    prog_main0 } = x_1636
    11891150  in
    11901151  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11931154    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11941155    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1195 let rec program_rect_Type0 h_mk_program x_2848 =
     1156let rec program_rect_Type0 h_mk_program x_1638 =
    11961157  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1197     prog_main0 } = x_2848
     1158    prog_main0 } = x_1638
    11981159  in
    11991160  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    12861247
    12871248(** val transf_program_gen :
    1288     String.string -> Identifiers.universe -> (Identifiers.universe -> 'a1 ->
    1289     ('a2, Identifiers.universe) Types.prod) -> (ident, 'a1) Types.prod
    1290     List.list -> ((ident, 'a2) Types.prod List.list, Identifiers.universe)
    1291     Types.prod **)
     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 **)
    12921253let transf_program_gen tag gen transf l =
    12931254  List.foldr (fun id_fn bs_gen ->
     
    13001261
    13011262(** val transform_program_gen :
    1302     String.string -> Identifiers.universe -> ('a1, 'a3) program -> (ident
    1303     List.list -> Identifiers.universe -> 'a1 -> ('a2, Identifiers.universe)
    1304     Types.prod) -> (('a2, 'a3) program, Identifiers.universe) Types.prod **)
     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 **)
    13051267let transform_program_gen tag gen p trans =
    13061268  let fsg =
     
    15171479(** val external_function_rect_Type4 :
    15181480    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1519 let rec external_function_rect_Type4 h_mk_external_function x_3052 =
    1520   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3052 in
     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
    15211483  h_mk_external_function ef_id0 ef_sig0
    15221484
    15231485(** val external_function_rect_Type5 :
    15241486    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1525 let rec external_function_rect_Type5 h_mk_external_function x_3054 =
    1526   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3054 in
     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
    15271489  h_mk_external_function ef_id0 ef_sig0
    15281490
    15291491(** val external_function_rect_Type3 :
    15301492    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1531 let rec external_function_rect_Type3 h_mk_external_function x_3056 =
    1532   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3056 in
     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
    15331495  h_mk_external_function ef_id0 ef_sig0
    15341496
    15351497(** val external_function_rect_Type2 :
    15361498    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1537 let rec external_function_rect_Type2 h_mk_external_function x_3058 =
    1538   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3058 in
     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
    15391501  h_mk_external_function ef_id0 ef_sig0
    15401502
    15411503(** val external_function_rect_Type1 :
    15421504    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1543 let rec external_function_rect_Type1 h_mk_external_function x_3060 =
    1544   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3060 in
     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
    15451507  h_mk_external_function ef_id0 ef_sig0
    15461508
    15471509(** val external_function_rect_Type0 :
    15481510    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1549 let rec external_function_rect_Type0 h_mk_external_function x_3062 =
    1550   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3062 in
     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
    15511513  h_mk_external_function ef_id0 ef_sig0
    15521514
     
    16151577    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16161578let rec fundef_rect_Type4 h_Internal h_External = function
    1617 | Internal x_3082 -> h_Internal x_3082
    1618 | External x_3083 -> h_External x_3083
     1579| Internal x_1872 -> h_Internal x_1872
     1580| External x_1873 -> h_External x_1873
    16191581
    16201582(** val fundef_rect_Type5 :
    16211583    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16221584let rec fundef_rect_Type5 h_Internal h_External = function
    1623 | Internal x_3087 -> h_Internal x_3087
    1624 | External x_3088 -> h_External x_3088
     1585| Internal x_1877 -> h_Internal x_1877
     1586| External x_1878 -> h_External x_1878
    16251587
    16261588(** val fundef_rect_Type3 :
    16271589    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16281590let rec fundef_rect_Type3 h_Internal h_External = function
    1629 | Internal x_3092 -> h_Internal x_3092
    1630 | External x_3093 -> h_External x_3093
     1591| Internal x_1882 -> h_Internal x_1882
     1592| External x_1883 -> h_External x_1883
    16311593
    16321594(** val fundef_rect_Type2 :
    16331595    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16341596let rec fundef_rect_Type2 h_Internal h_External = function
    1635 | Internal x_3097 -> h_Internal x_3097
    1636 | External x_3098 -> h_External x_3098
     1597| Internal x_1887 -> h_Internal x_1887
     1598| External x_1888 -> h_External x_1888
    16371599
    16381600(** val fundef_rect_Type1 :
    16391601    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16401602let rec fundef_rect_Type1 h_Internal h_External = function
    1641 | Internal x_3102 -> h_Internal x_3102
    1642 | External x_3103 -> h_External x_3103
     1603| Internal x_1892 -> h_Internal x_1892
     1604| External x_1893 -> h_External x_1893
    16431605
    16441606(** val fundef_rect_Type0 :
    16451607    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16461608let rec fundef_rect_Type0 h_Internal h_External = function
    1647 | Internal x_3107 -> h_Internal x_3107
    1648 | External x_3108 -> h_External x_3108
     1609| Internal x_1897 -> h_Internal x_1897
     1610| External x_1898 -> h_External x_1898
    16491611
    16501612(** val fundef_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.