Changeset 2730 for extracted/aST.ml


Ignore:
Timestamp:
Feb 25, 2013, 9:54:49 PM (8 years ago)
Author:
sacerdot
Message:

Exported again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/aST.ml

    r2717 r2730  
    418418    (intsize -> signedness -> 'a1) -> 'a1 -> typ -> 'a1 **)
    419419let rec typ_rect_Type4 h_ASTint h_ASTptr = function
    420 | ASTint (x_3480, x_3479) -> h_ASTint x_3480 x_3479
     420| ASTint (x_1295, x_1294) -> h_ASTint x_1295 x_1294
    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_3485, x_3484) -> h_ASTint x_3485 x_3484
     426| ASTint (x_1300, x_1299) -> h_ASTint x_1300 x_1299
    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_3490, x_3489) -> h_ASTint x_3490 x_3489
     432| ASTint (x_1305, x_1304) -> h_ASTint x_1305 x_1304
    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_3495, x_3494) -> h_ASTint x_3495 x_3494
     438| ASTint (x_1310, x_1309) -> h_ASTint x_1310 x_1309
    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_3500, x_3499) -> h_ASTint x_3500 x_3499
     444| ASTint (x_1315, x_1314) -> h_ASTint x_1315 x_1314
    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_3505, x_3504) -> h_ASTint x_3505 x_3504
     450| ASTint (x_1320, x_1319) -> h_ASTint x_1320 x_1319
    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_3540 =
    880   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3540 in
     879let rec signature_rect_Type4 h_mk_signature x_1355 =
     880  let { sig_args = sig_args0; sig_res = sig_res0 } = x_1355 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_3542 =
    886   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3542 in
     885let rec signature_rect_Type5 h_mk_signature x_1357 =
     886  let { sig_args = sig_args0; sig_res = sig_res0 } = x_1357 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_3544 =
    892   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3544 in
     891let rec signature_rect_Type3 h_mk_signature x_1359 =
     892  let { sig_args = sig_args0; sig_res = sig_res0 } = x_1359 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_3546 =
    898   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3546 in
     897let rec signature_rect_Type2 h_mk_signature x_1361 =
     898  let { sig_args = sig_args0; sig_res = sig_res0 } = x_1361 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_3548 =
    904   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3548 in
     903let rec signature_rect_Type1 h_mk_signature x_1363 =
     904  let { sig_args = sig_args0; sig_res = sig_res0 } = x_1363 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_3550 =
    910   let { sig_args = sig_args0; sig_res = sig_res0 } = x_3550 in
     909let rec signature_rect_Type0 h_mk_signature x_1365 =
     910  let { sig_args = sig_args0; sig_res = sig_res0 } = x_1365 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_3578 -> h_Init_int8 x_3578
    987 | Init_int16 x_3579 -> h_Init_int16 x_3579
    988 | Init_int32 x_3580 -> h_Init_int32 x_3580
    989 | Init_space x_3581 -> h_Init_space x_3581
     986| Init_int8 x_1393 -> h_Init_int8 x_1393
     987| Init_int16 x_1394 -> h_Init_int16 x_1394
     988| Init_int32 x_1395 -> h_Init_int32 x_1395
     989| Init_space x_1396 -> h_Init_space x_1396
    990990| Init_null -> h_Init_null
    991 | Init_addrof (x_3583, x_3582) -> h_Init_addrof x_3583 x_3582
     991| Init_addrof (x_1398, x_1397) -> h_Init_addrof x_1398 x_1397
    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_3591 -> h_Init_int8 x_3591
    998 | Init_int16 x_3592 -> h_Init_int16 x_3592
    999 | Init_int32 x_3593 -> h_Init_int32 x_3593
    1000 | Init_space x_3594 -> h_Init_space x_3594
     997| Init_int8 x_1406 -> h_Init_int8 x_1406
     998| Init_int16 x_1407 -> h_Init_int16 x_1407
     999| Init_int32 x_1408 -> h_Init_int32 x_1408
     1000| Init_space x_1409 -> h_Init_space x_1409
    10011001| Init_null -> h_Init_null
    1002 | Init_addrof (x_3596, x_3595) -> h_Init_addrof x_3596 x_3595
     1002| Init_addrof (x_1411, x_1410) -> h_Init_addrof x_1411 x_1410
    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_3604 -> h_Init_int8 x_3604
    1009 | Init_int16 x_3605 -> h_Init_int16 x_3605
    1010 | Init_int32 x_3606 -> h_Init_int32 x_3606
    1011 | Init_space x_3607 -> h_Init_space x_3607
     1008| Init_int8 x_1419 -> h_Init_int8 x_1419
     1009| Init_int16 x_1420 -> h_Init_int16 x_1420
     1010| Init_int32 x_1421 -> h_Init_int32 x_1421
     1011| Init_space x_1422 -> h_Init_space x_1422
    10121012| Init_null -> h_Init_null
    1013 | Init_addrof (x_3609, x_3608) -> h_Init_addrof x_3609 x_3608
     1013| Init_addrof (x_1424, x_1423) -> h_Init_addrof x_1424 x_1423
    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_3617 -> h_Init_int8 x_3617
    1020 | Init_int16 x_3618 -> h_Init_int16 x_3618
    1021 | Init_int32 x_3619 -> h_Init_int32 x_3619
    1022 | Init_space x_3620 -> h_Init_space x_3620
     1019| Init_int8 x_1432 -> h_Init_int8 x_1432
     1020| Init_int16 x_1433 -> h_Init_int16 x_1433
     1021| Init_int32 x_1434 -> h_Init_int32 x_1434
     1022| Init_space x_1435 -> h_Init_space x_1435
    10231023| Init_null -> h_Init_null
    1024 | Init_addrof (x_3622, x_3621) -> h_Init_addrof x_3622 x_3621
     1024| Init_addrof (x_1437, x_1436) -> h_Init_addrof x_1437 x_1436
    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_3630 -> h_Init_int8 x_3630
    1031 | Init_int16 x_3631 -> h_Init_int16 x_3631
    1032 | Init_int32 x_3632 -> h_Init_int32 x_3632
    1033 | Init_space x_3633 -> h_Init_space x_3633
     1030| Init_int8 x_1445 -> h_Init_int8 x_1445
     1031| Init_int16 x_1446 -> h_Init_int16 x_1446
     1032| Init_int32 x_1447 -> h_Init_int32 x_1447
     1033| Init_space x_1448 -> h_Init_space x_1448
    10341034| Init_null -> h_Init_null
    1035 | Init_addrof (x_3635, x_3634) -> h_Init_addrof x_3635 x_3634
     1035| Init_addrof (x_1450, x_1449) -> h_Init_addrof x_1450 x_1449
    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_3643 -> h_Init_int8 x_3643
    1042 | Init_int16 x_3644 -> h_Init_int16 x_3644
    1043 | Init_int32 x_3645 -> h_Init_int32 x_3645
    1044 | Init_space x_3646 -> h_Init_space x_3646
     1041| Init_int8 x_1458 -> h_Init_int8 x_1458
     1042| Init_int16 x_1459 -> h_Init_int16 x_1459
     1043| Init_int32 x_1460 -> h_Init_int32 x_1460
     1044| Init_space x_1461 -> h_Init_space x_1461
    10451045| Init_null -> h_Init_null
    1046 | Init_addrof (x_3648, x_3647) -> h_Init_addrof x_3648 x_3647
     1046| Init_addrof (x_1463, x_1462) -> h_Init_addrof x_1463 x_1462
    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_3735 =
     1113let rec program_rect_Type4 h_mk_program x_1550 =
    11141114  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1115     prog_main0 } = x_3735
     1115    prog_main0 } = x_1550
    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_3737 =
     1122let rec program_rect_Type5 h_mk_program x_1552 =
    11231123  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1124     prog_main0 } = x_3737
     1124    prog_main0 } = x_1552
    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_3739 =
     1131let rec program_rect_Type3 h_mk_program x_1554 =
    11321132  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1133     prog_main0 } = x_3739
     1133    prog_main0 } = x_1554
    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_3741 =
     1140let rec program_rect_Type2 h_mk_program x_1556 =
    11411141  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1142     prog_main0 } = x_3741
     1142    prog_main0 } = x_1556
    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_3743 =
     1149let rec program_rect_Type1 h_mk_program x_1558 =
    11501150  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1151     prog_main0 } = x_3743
     1151    prog_main0 } = x_1558
    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_3745 =
     1158let rec program_rect_Type0 h_mk_program x_1560 =
    11591159  let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main =
    1160     prog_main0 } = x_3745
     1160    prog_main0 } = x_1560
    11611161  in
    11621162  h_mk_program prog_vars0 prog_funct0 prog_main0
     
    14811481(** val external_function_rect_Type4 :
    14821482    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1483 let rec external_function_rect_Type4 h_mk_external_function x_3949 =
    1484   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3949 in
     1483let rec external_function_rect_Type4 h_mk_external_function x_1764 =
     1484  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_1764 in
    14851485  h_mk_external_function ef_id0 ef_sig0
    14861486
    14871487(** val external_function_rect_Type5 :
    14881488    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1489 let rec external_function_rect_Type5 h_mk_external_function x_3951 =
    1490   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3951 in
     1489let rec external_function_rect_Type5 h_mk_external_function x_1766 =
     1490  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_1766 in
    14911491  h_mk_external_function ef_id0 ef_sig0
    14921492
    14931493(** val external_function_rect_Type3 :
    14941494    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1495 let rec external_function_rect_Type3 h_mk_external_function x_3953 =
    1496   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3953 in
     1495let rec external_function_rect_Type3 h_mk_external_function x_1768 =
     1496  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_1768 in
    14971497  h_mk_external_function ef_id0 ef_sig0
    14981498
    14991499(** val external_function_rect_Type2 :
    15001500    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1501 let rec external_function_rect_Type2 h_mk_external_function x_3955 =
    1502   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3955 in
     1501let rec external_function_rect_Type2 h_mk_external_function x_1770 =
     1502  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_1770 in
    15031503  h_mk_external_function ef_id0 ef_sig0
    15041504
    15051505(** val external_function_rect_Type1 :
    15061506    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1507 let rec external_function_rect_Type1 h_mk_external_function x_3957 =
    1508   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3957 in
     1507let rec external_function_rect_Type1 h_mk_external_function x_1772 =
     1508  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_1772 in
    15091509  h_mk_external_function ef_id0 ef_sig0
    15101510
    15111511(** val external_function_rect_Type0 :
    15121512    (ident -> signature -> 'a1) -> external_function -> 'a1 **)
    1513 let rec external_function_rect_Type0 h_mk_external_function x_3959 =
    1514   let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_3959 in
     1513let rec external_function_rect_Type0 h_mk_external_function x_1774 =
     1514  let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_1774 in
    15151515  h_mk_external_function ef_id0 ef_sig0
    15161516
     
    15791579    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15801580let rec fundef_rect_Type4 h_Internal h_External = function
    1581 | Internal x_3979 -> h_Internal x_3979
    1582 | External x_3980 -> h_External x_3980
     1581| Internal x_1794 -> h_Internal x_1794
     1582| External x_1795 -> h_External x_1795
    15831583
    15841584(** val fundef_rect_Type5 :
    15851585    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15861586let rec fundef_rect_Type5 h_Internal h_External = function
    1587 | Internal x_3984 -> h_Internal x_3984
    1588 | External x_3985 -> h_External x_3985
     1587| Internal x_1799 -> h_Internal x_1799
     1588| External x_1800 -> h_External x_1800
    15891589
    15901590(** val fundef_rect_Type3 :
    15911591    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15921592let rec fundef_rect_Type3 h_Internal h_External = function
    1593 | Internal x_3989 -> h_Internal x_3989
    1594 | External x_3990 -> h_External x_3990
     1593| Internal x_1804 -> h_Internal x_1804
     1594| External x_1805 -> h_External x_1805
    15951595
    15961596(** val fundef_rect_Type2 :
    15971597    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    15981598let rec fundef_rect_Type2 h_Internal h_External = function
    1599 | Internal x_3994 -> h_Internal x_3994
    1600 | External x_3995 -> h_External x_3995
     1599| Internal x_1809 -> h_Internal x_1809
     1600| External x_1810 -> h_External x_1810
    16011601
    16021602(** val fundef_rect_Type1 :
    16031603    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16041604let rec fundef_rect_Type1 h_Internal h_External = function
    1605 | Internal x_3999 -> h_Internal x_3999
    1606 | External x_4000 -> h_External x_4000
     1605| Internal x_1814 -> h_Internal x_1814
     1606| External x_1815 -> h_External x_1815
    16071607
    16081608(** val fundef_rect_Type0 :
    16091609    ('a1 -> 'a2) -> (external_function -> 'a2) -> 'a1 fundef -> 'a2 **)
    16101610let rec fundef_rect_Type0 h_Internal h_External = function
    1611 | Internal x_4004 -> h_Internal x_4004
    1612 | External x_4005 -> h_External x_4005
     1611| Internal x_1819 -> h_Internal x_1819
     1612| External x_1820 -> h_External x_1820
    16131613
    16141614(** val fundef_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.