Changeset 2997 for extracted/aST.ml


Ignore:
Timestamp:
Mar 28, 2013, 10:27:41 AM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/aST.ml

    r2827 r2997  
    418418    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    419419let rec typ_rect_Type4 h_ASTint h_ASTptr = function
    420 | ASTint (x_3649, x_3648) -> h_ASTint x_3649 x_3648
     420| ASTint (x_411, x_410) -> h_ASTint x_411 x_410
    421421| ASTptr -> h_ASTptr
    422422
     
    424424    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    425425let rec typ_rect_Type5 h_ASTint h_ASTptr = function
    426 | ASTint (x_3654, x_3653) -> h_ASTint x_3654 x_3653
     426| ASTint (x_416, x_415) -> h_ASTint x_416 x_415
    427427| ASTptr -> h_ASTptr
    428428
     
    430430    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    431431let rec typ_rect_Type3 h_ASTint h_ASTptr = function
    432 | ASTint (x_3659, x_3658) -> h_ASTint x_3659 x_3658
     432| ASTint (x_421, x_420) -> h_ASTint x_421 x_420
    433433| ASTptr -> h_ASTptr
    434434
     
    436436    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    437437let rec typ_rect_Type2 h_ASTint h_ASTptr = function
    438 | ASTint (x_3664, x_3663) -> h_ASTint x_3664 x_3663
     438| ASTint (x_426, x_425) -> h_ASTint x_426 x_425
    439439| ASTptr -> h_ASTptr
    440440
     
    442442    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    443443let rec typ_rect_Type1 h_ASTint h_ASTptr = function
    444 | ASTint (x_3669, x_3668) -> h_ASTint x_3669 x_3668
     444| ASTint (x_431, x_430) -> h_ASTint x_431 x_430
    445445| ASTptr -> h_ASTptr
    446446
     
    448448    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    449449let rec typ_rect_Type0 h_ASTint h_ASTptr = function
    450 | ASTint (x_3674, x_3673) -> h_ASTint x_3674 x_3673
     450| ASTint (x_436, x_435) -> h_ASTint x_436 x_435
    451451| ASTptr -> h_ASTptr
    452452
     
    877877(** val signature_rect_Type4 :
    878878    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    879 let rec signature_rect_Type4 h_mk_signature x_3709 =
    880   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3709 in
     879let rec signature_rect_Type4 h_mk_signature x_471 =
     880  let { sig_args = sig_args0; sig_res = sig_res0 } = x_471 in
    881881  h_mk_signature sig_args0 sig_res0
    882882
    883883(** val signature_rect_Type5 :
    884884    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    885 let rec signature_rect_Type5 h_mk_signature x_3711 =
    886   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3711 in
     885let rec signature_rect_Type5 h_mk_signature x_473 =
     886  let { sig_args = sig_args0; sig_res = sig_res0 } = x_473 in
    887887  h_mk_signature sig_args0 sig_res0
    888888
    889889(** val signature_rect_Type3 :
    890890    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    891 let rec signature_rect_Type3 h_mk_signature x_3713 =
    892   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3713 in
     891let rec signature_rect_Type3 h_mk_signature x_475 =
     892  let { sig_args = sig_args0; sig_res = sig_res0 } = x_475 in
    893893  h_mk_signature sig_args0 sig_res0
    894894
    895895(** val signature_rect_Type2 :
    896896    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    897 let rec signature_rect_Type2 h_mk_signature x_3715 =
    898   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3715 in
     897let rec signature_rect_Type2 h_mk_signature x_477 =
     898  let { sig_args = sig_args0; sig_res = sig_res0 } = x_477 in
    899899  h_mk_signature sig_args0 sig_res0
    900900
    901901(** val signature_rect_Type1 :
    902902    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    903 let rec signature_rect_Type1 h_mk_signature x_3717 =
    904   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3717 in
     903let rec signature_rect_Type1 h_mk_signature x_479 =
     904  let { sig_args = sig_args0; sig_res = sig_res0 } = x_479 in
    905905  h_mk_signature sig_args0 sig_res0
    906906
    907907(** val signature_rect_Type0 :
    908908    (typ List.list -> typ Types.option -> 'a1) -> signature -> 'a1 **)
    909 let rec signature_rect_Type0 h_mk_signature x_3719 =
    910   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3719 in
     909let rec signature_rect_Type0 h_mk_signature x_481 =
     910  let { sig_args = sig_args0; sig_res = sig_res0 } = x_481 in
    911911  h_mk_signature sig_args0 sig_res0
    912912
     
    984984    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    985985let 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_3747 -> h_Init_int8 x_3747
    987 | Init_int16 x_3748 -> h_Init_int16 x_3748
    988 | Init_int32 x_3749 -> h_Init_int32 x_3749
    989 | Init_space x_3750 -> h_Init_space x_3750
     986| Init_int8 x_509 -> h_Init_int8 x_509
     987| Init_int16 x_510 -> h_Init_int16 x_510
     988| Init_int32 x_511 -> h_Init_int32 x_511
     989| Init_space x_512 -> h_Init_space x_512
    990990| Init_null -> h_Init_null
    991 | Init_addrof (x_3752, x_3751) -> h_Init_addrof x_3752 x_3751
     991| Init_addrof (x_514, x_513) -> h_Init_addrof x_514 x_513
    992992
    993993(** val init_data_rect_Type5 :
     
    995995    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    996996let 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_3760 -> h_Init_int8 x_3760
    998 | Init_int16 x_3761 -> h_Init_int16 x_3761
    999 | Init_int32 x_3762 -> h_Init_int32 x_3762
    1000 | Init_space x_3763 -> h_Init_space x_3763
     997| Init_int8 x_522 -> h_Init_int8 x_522
     998| Init_int16 x_523 -> h_Init_int16 x_523
     999| Init_int32 x_524 -> h_Init_int32 x_524
     1000| Init_space x_525 -> h_Init_space x_525
    10011001| Init_null -> h_Init_null
    1002 | Init_addrof (x_3765, x_3764) -> h_Init_addrof x_3765 x_3764
     1002| Init_addrof (x_527, x_526) -> h_Init_addrof x_527 x_526
    10031003
    10041004(** val init_data_rect_Type3 :
     
    10061006    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10071007let 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_3773 -> h_Init_int8 x_3773
    1009 | Init_int16 x_3774 -> h_Init_int16 x_3774
    1010 | Init_int32 x_3775 -> h_Init_int32 x_3775
    1011 | Init_space x_3776 -> h_Init_space x_3776
     1008| Init_int8 x_535 -> h_Init_int8 x_535
     1009| Init_int16 x_536 -> h_Init_int16 x_536
     1010| Init_int32 x_537 -> h_Init_int32 x_537
     1011| Init_space x_538 -> h_Init_space x_538
    10121012| Init_null -> h_Init_null
    1013 | Init_addrof (x_3778, x_3777) -> h_Init_addrof x_3778 x_3777
     1013| Init_addrof (x_540, x_539) -> h_Init_addrof x_540 x_539
    10141014
    10151015(** val init_data_rect_Type2 :
     
    10171017    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10181018let 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_3786 -> h_Init_int8 x_3786
    1020 | Init_int16 x_3787 -> h_Init_int16 x_3787
    1021 | Init_int32 x_3788 -> h_Init_int32 x_3788
    1022 | Init_space x_3789 -> h_Init_space x_3789
     1019| Init_int8 x_548 -> h_Init_int8 x_548
     1020| Init_int16 x_549 -> h_Init_int16 x_549
     1021| Init_int32 x_550 -> h_Init_int32 x_550
     1022| Init_space x_551 -> h_Init_space x_551
    10231023| Init_null -> h_Init_null
    1024 | Init_addrof (x_3791, x_3790) -> h_Init_addrof x_3791 x_3790
     1024| Init_addrof (x_553, x_552) -> h_Init_addrof x_553 x_552
    10251025
    10261026(** val init_data_rect_Type1 :
     
    10281028    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10291029let 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_3799 -> h_Init_int8 x_3799
    1031 | Init_int16 x_3800 -> h_Init_int16 x_3800
    1032 | Init_int32 x_3801 -> h_Init_int32 x_3801
    1033 | Init_space x_3802 -> h_Init_space x_3802
     1030| Init_int8 x_561 -> h_Init_int8 x_561
     1031| Init_int16 x_562 -> h_Init_int16 x_562
     1032| Init_int32 x_563 -> h_Init_int32 x_563
     1033| Init_space x_564 -> h_Init_space x_564
    10341034| Init_null -> h_Init_null
    1035 | Init_addrof (x_3804, x_3803) -> h_Init_addrof x_3804 x_3803
     1035| Init_addrof (x_566, x_565) -> h_Init_addrof x_566 x_565
    10361036
    10371037(** val init_data_rect_Type0 :
     
    10391039    'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1 **)
    10401040let 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_3812 -> h_Init_int8 x_3812
    1042 | Init_int16 x_3813 -> h_Init_int16 x_3813
    1043 | Init_int32 x_3814 -> h_Init_int32 x_3814
    1044 | Init_space x_3815 -> h_Init_space x_3815
     1041| Init_int8 x_574 -> h_Init_int8 x_574
     1042| Init_int16 x_575 -> h_Init_int16 x_575
     1043| Init_int32 x_576 -> h_Init_int32 x_576
     1044| Init_space x_577 -> h_Init_space x_577
    10451045| Init_null -> h_Init_null
    1046 | Init_addrof (x_3817, x_3816) -> h_Init_addrof x_3817 x_3816
     1046| Init_addrof (x_579, x_578) -> h_Init_addrof x_579 x_578
    10471047
    10481048(** val init_data_inv_rect_Type4 :
     
    11111111    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11121112    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1113 let rec program_rect_Type4 h_mk_program x_3904 =
     1113let rec program_rect_Type4 h_mk_program x_666 =
    11141114  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1115     prog_main0 } = x_3904
     1115    prog_main0 } = x_666
    11161116  in
    11171117  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11201120    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11211121    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1122 let rec program_rect_Type5 h_mk_program x_3906 =
     1122let rec program_rect_Type5 h_mk_program x_668 =
    11231123  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1124     prog_main0 } = x_3906
     1124    prog_main0 } = x_668
    11251125  in
    11261126  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11291129    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11301130    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1131 let rec program_rect_Type3 h_mk_program x_3908 =
     1131let rec program_rect_Type3 h_mk_program x_670 =
    11321132  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1133     prog_main0 } = x_3908
     1133    prog_main0 } = x_670
    11341134  in
    11351135  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11381138    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11391139    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1140 let rec program_rect_Type2 h_mk_program x_3910 =
     1140let rec program_rect_Type2 h_mk_program x_672 =
    11411141  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1142     prog_main0 } = x_3910
     1142    prog_main0 } = x_672
    11431143  in
    11441144  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11471147    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11481148    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1149 let rec program_rect_Type1 h_mk_program x_3912 =
     1149let rec program_rect_Type1 h_mk_program x_674 =
    11501150  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1151     prog_main0 } = x_3912
     1151    prog_main0 } = x_674
    11521152  in
    11531153  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    11561156    (((ident, region) Types.prod, 'a2) Types.prod List.list -> (ident, 'a1)
    11571157    Types.prod List.list -> ident -> 'a3) -> ('a1, 'a2) program -> 'a3 **)
    1158 let rec program_rect_Type0 h_mk_program x_3914 =
     1158let rec program_rect_Type0 h_mk_program x_676 =
    11591159  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1160     prog_main0 } = x_3914
     1160    prog_main0 } = x_676
    11611161  in
    11621162  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    14771477(** val external_function_rect_Type4 :
    14781478    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1479 let rec external_function_rect_Type4 h_mk_external_function x_4118 =
    1480   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4118 in
     1479let rec external_function_rect_Type4 h_mk_external_function x_880 =
     1480  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_880 in
    14811481  h_mk_external_function ef_id0 ef_sig0
    14821482
    14831483(** val external_function_rect_Type5 :
    14841484    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1485 let rec external_function_rect_Type5 h_mk_external_function x_4120 =
    1486   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4120 in
     1485let rec external_function_rect_Type5 h_mk_external_function x_882 =
     1486  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_882 in
    14871487  h_mk_external_function ef_id0 ef_sig0
    14881488
    14891489(** val external_function_rect_Type3 :
    14901490    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1491 let rec external_function_rect_Type3 h_mk_external_function x_4122 =
    1492   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4122 in
     1491let rec external_function_rect_Type3 h_mk_external_function x_884 =
     1492  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_884 in
    14931493  h_mk_external_function ef_id0 ef_sig0
    14941494
    14951495(** val external_function_rect_Type2 :
    14961496    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1497 let rec external_function_rect_Type2 h_mk_external_function x_4124 =
    1498   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4124 in
     1497let rec external_function_rect_Type2 h_mk_external_function x_886 =
     1498  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_886 in
    14991499  h_mk_external_function ef_id0 ef_sig0
    15001500
    15011501(** val external_function_rect_Type1 :
    15021502    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1503 let rec external_function_rect_Type1 h_mk_external_function x_4126 =
    1504   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4126 in
     1503let rec external_function_rect_Type1 h_mk_external_function x_888 =
     1504  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_888 in
    15051505  h_mk_external_function ef_id0 ef_sig0
    15061506
    15071507(** val external_function_rect_Type0 :
    15081508    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1509 let rec external_function_rect_Type0 h_mk_external_function x_4128 =
    1510   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_4128 in
     1509let rec external_function_rect_Type0 h_mk_external_function x_890 =
     1510  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_890 in
    15111511  h_mk_external_function ef_id0 ef_sig0
    15121512
     
    15751575    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15761576let rec fundef_rect_Type4 h_Internal h_External = function
    1577 | Internal x_4148 -> h_Internal x_4148
    1578 | External x_4149 -> h_External x_4149
     1577| Internal x_910 -> h_Internal x_910
     1578| External x_911 -> h_External x_911
    15791579
    15801580(** val fundef_rect_Type5 :
    15811581    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15821582let rec fundef_rect_Type5 h_Internal h_External = function
    1583 | Internal x_4153 -> h_Internal x_4153
    1584 | External x_4154 -> h_External x_4154
     1583| Internal x_915 -> h_Internal x_915
     1584| External x_916 -> h_External x_916
    15851585
    15861586(** val fundef_rect_Type3 :
    15871587    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15881588let rec fundef_rect_Type3 h_Internal h_External = function
    1589 | Internal x_4158 -> h_Internal x_4158
    1590 | External x_4159 -> h_External x_4159
     1589| Internal x_920 -> h_Internal x_920
     1590| External x_921 -> h_External x_921
    15911591
    15921592(** val fundef_rect_Type2 :
    15931593    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15941594let rec fundef_rect_Type2 h_Internal h_External = function
    1595 | Internal x_4163 -> h_Internal x_4163
    1596 | External x_4164 -> h_External x_4164
     1595| Internal x_925 -> h_Internal x_925
     1596| External x_926 -> h_External x_926
    15971597
    15981598(** val fundef_rect_Type1 :
    15991599    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16001600let rec fundef_rect_Type1 h_Internal h_External = function
    1601 | Internal x_4168 -> h_Internal x_4168
    1602 | External x_4169 -> h_External x_4169
     1601| Internal x_930 -> h_Internal x_930
     1602| External x_931 -> h_External x_931
    16031603
    16041604(** val fundef_rect_Type0 :
    16051605    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16061606let rec fundef_rect_Type0 h_Internal h_External = function
    1607 | Internal x_4173 -> h_Internal x_4173
    1608 | External x_4174 -> h_External x_4174
     1607| Internal x_935 -> h_Internal x_935
     1608| External x_936 -> h_External x_936
    16091609
    16101610(** val fundef_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.