Changeset 2717 for extracted/aST.ml
 Timestamp:
 Feb 23, 2013, 1:16:55 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/aST.ml
r2649 r2717 10 10 11 11 open Types 12 13 open Exp 12 14 13 15 open Arithmetic … … 416 418 (intsize > signedness > 'a1) > 'a1 > typ > 'a1 **) 417 419 let rec typ_rect_Type4 h_ASTint h_ASTptr = function 418  ASTint (x_ 1373, x_1372) > h_ASTint x_1373 x_1372420  ASTint (x_3480, x_3479) > h_ASTint x_3480 x_3479 419 421  ASTptr > h_ASTptr 420 422 … … 422 424 (intsize > signedness > 'a1) > 'a1 > typ > 'a1 **) 423 425 let rec typ_rect_Type5 h_ASTint h_ASTptr = function 424  ASTint (x_ 1378, x_1377) > h_ASTint x_1378 x_1377426  ASTint (x_3485, x_3484) > h_ASTint x_3485 x_3484 425 427  ASTptr > h_ASTptr 426 428 … … 428 430 (intsize > signedness > 'a1) > 'a1 > typ > 'a1 **) 429 431 let rec typ_rect_Type3 h_ASTint h_ASTptr = function 430  ASTint (x_ 1383, x_1382) > h_ASTint x_1383 x_1382432  ASTint (x_3490, x_3489) > h_ASTint x_3490 x_3489 431 433  ASTptr > h_ASTptr 432 434 … … 434 436 (intsize > signedness > 'a1) > 'a1 > typ > 'a1 **) 435 437 let rec typ_rect_Type2 h_ASTint h_ASTptr = function 436  ASTint (x_ 1388, x_1387) > h_ASTint x_1388 x_1387438  ASTint (x_3495, x_3494) > h_ASTint x_3495 x_3494 437 439  ASTptr > h_ASTptr 438 440 … … 440 442 (intsize > signedness > 'a1) > 'a1 > typ > 'a1 **) 441 443 let rec typ_rect_Type1 h_ASTint h_ASTptr = function 442  ASTint (x_ 1393, x_1392) > h_ASTint x_1393 x_1392444  ASTint (x_3500, x_3499) > h_ASTint x_3500 x_3499 443 445  ASTptr > h_ASTptr 444 446 … … 446 448 (intsize > signedness > 'a1) > 'a1 > typ > 'a1 **) 447 449 let rec typ_rect_Type0 h_ASTint h_ASTptr = function 448  ASTint (x_ 1398, x_1397) > h_ASTint x_1398 x_1397450  ASTint (x_3505, x_3504) > h_ASTint x_3505 x_3504 449 451  ASTptr > h_ASTptr 450 452 … … 875 877 (** val signature_rect_Type4 : 876 878 (typ List.list > typ Types.option > 'a1) > signature > 'a1 **) 877 let rec signature_rect_Type4 h_mk_signature x_ 1433=878 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 1433in879 let rec signature_rect_Type4 h_mk_signature x_3540 = 880 let { sig_args = sig_args0; sig_res = sig_res0 } = x_3540 in 879 881 h_mk_signature sig_args0 sig_res0 880 882 881 883 (** val signature_rect_Type5 : 882 884 (typ List.list > typ Types.option > 'a1) > signature > 'a1 **) 883 let rec signature_rect_Type5 h_mk_signature x_ 1435=884 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 1435in885 let rec signature_rect_Type5 h_mk_signature x_3542 = 886 let { sig_args = sig_args0; sig_res = sig_res0 } = x_3542 in 885 887 h_mk_signature sig_args0 sig_res0 886 888 887 889 (** val signature_rect_Type3 : 888 890 (typ List.list > typ Types.option > 'a1) > signature > 'a1 **) 889 let rec signature_rect_Type3 h_mk_signature x_ 1437=890 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 1437in891 let rec signature_rect_Type3 h_mk_signature x_3544 = 892 let { sig_args = sig_args0; sig_res = sig_res0 } = x_3544 in 891 893 h_mk_signature sig_args0 sig_res0 892 894 893 895 (** val signature_rect_Type2 : 894 896 (typ List.list > typ Types.option > 'a1) > signature > 'a1 **) 895 let rec signature_rect_Type2 h_mk_signature x_ 1439=896 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 1439in897 let rec signature_rect_Type2 h_mk_signature x_3546 = 898 let { sig_args = sig_args0; sig_res = sig_res0 } = x_3546 in 897 899 h_mk_signature sig_args0 sig_res0 898 900 899 901 (** val signature_rect_Type1 : 900 902 (typ List.list > typ Types.option > 'a1) > signature > 'a1 **) 901 let rec signature_rect_Type1 h_mk_signature x_ 1441=902 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 1441in903 let rec signature_rect_Type1 h_mk_signature x_3548 = 904 let { sig_args = sig_args0; sig_res = sig_res0 } = x_3548 in 903 905 h_mk_signature sig_args0 sig_res0 904 906 905 907 (** val signature_rect_Type0 : 906 908 (typ List.list > typ Types.option > 'a1) > signature > 'a1 **) 907 let rec signature_rect_Type0 h_mk_signature x_ 1443=908 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 1443in909 let rec signature_rect_Type0 h_mk_signature x_3550 = 910 let { sig_args = sig_args0; sig_res = sig_res0 } = x_3550 in 909 911 h_mk_signature sig_args0 sig_res0 910 912 … … 982 984 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 **) 983 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 984  Init_int8 x_ 1471 > h_Init_int8 x_1471985  Init_int16 x_ 1472 > h_Init_int16 x_1472986  Init_int32 x_ 1473 > h_Init_int32 x_1473987  Init_space x_ 1474 > h_Init_space x_1474986  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 988 990  Init_null > h_Init_null 989  Init_addrof (x_ 1476, x_1475) > h_Init_addrof x_1476 x_1475991  Init_addrof (x_3583, x_3582) > h_Init_addrof x_3583 x_3582 990 992 991 993 (** val init_data_rect_Type5 : … … 993 995 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 **) 994 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 995  Init_int8 x_ 1484 > h_Init_int8 x_1484996  Init_int16 x_ 1485 > h_Init_int16 x_1485997  Init_int32 x_ 1486 > h_Init_int32 x_1486998  Init_space x_ 1487 > h_Init_space x_1487997  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 999 1001  Init_null > h_Init_null 1000  Init_addrof (x_ 1489, x_1488) > h_Init_addrof x_1489 x_14881002  Init_addrof (x_3596, x_3595) > h_Init_addrof x_3596 x_3595 1001 1003 1002 1004 (** val init_data_rect_Type3 : … … 1004 1006 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 **) 1005 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 1006  Init_int8 x_ 1497 > h_Init_int8 x_14971007  Init_int16 x_ 1498 > h_Init_int16 x_14981008  Init_int32 x_ 1499 > h_Init_int32 x_14991009  Init_space x_ 1500 > h_Init_space x_15001008  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 1010 1012  Init_null > h_Init_null 1011  Init_addrof (x_ 1502, x_1501) > h_Init_addrof x_1502 x_15011013  Init_addrof (x_3609, x_3608) > h_Init_addrof x_3609 x_3608 1012 1014 1013 1015 (** val init_data_rect_Type2 : … … 1015 1017 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 **) 1016 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 1017  Init_int8 x_ 1510 > h_Init_int8 x_15101018  Init_int16 x_ 1511 > h_Init_int16 x_15111019  Init_int32 x_ 1512 > h_Init_int32 x_15121020  Init_space x_ 1513 > h_Init_space x_15131019  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 1021 1023  Init_null > h_Init_null 1022  Init_addrof (x_ 1515, x_1514) > h_Init_addrof x_1515 x_15141024  Init_addrof (x_3622, x_3621) > h_Init_addrof x_3622 x_3621 1023 1025 1024 1026 (** val init_data_rect_Type1 : … … 1026 1028 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 **) 1027 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 1028  Init_int8 x_ 1523 > h_Init_int8 x_15231029  Init_int16 x_ 1524 > h_Init_int16 x_15241030  Init_int32 x_ 1525 > h_Init_int32 x_15251031  Init_space x_ 1526 > h_Init_space x_15261030  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 1032 1034  Init_null > h_Init_null 1033  Init_addrof (x_ 1528, x_1527) > h_Init_addrof x_1528 x_15271035  Init_addrof (x_3635, x_3634) > h_Init_addrof x_3635 x_3634 1034 1036 1035 1037 (** val init_data_rect_Type0 : … … 1037 1039 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 **) 1038 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 1039  Init_int8 x_ 1536 > h_Init_int8 x_15361040  Init_int16 x_ 1537 > h_Init_int16 x_15371041  Init_int32 x_ 1538 > h_Init_int32 x_15381042  Init_space x_ 1539 > h_Init_space x_15391041  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 1043 1045  Init_null > h_Init_null 1044  Init_addrof (x_ 1541, x_1540) > h_Init_addrof x_1541 x_15401046  Init_addrof (x_3648, x_3647) > h_Init_addrof x_3648 x_3647 1045 1047 1046 1048 (** val init_data_inv_rect_Type4 : … … 1109 1111 (((ident, region) Types.prod, 'a2) Types.prod List.list > (ident, 'a1) 1110 1112 Types.prod List.list > ident > 'a3) > ('a1, 'a2) program > 'a3 **) 1111 let rec program_rect_Type4 h_mk_program x_ 1628=1113 let rec program_rect_Type4 h_mk_program x_3735 = 1112 1114 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1113 prog_main0 } = x_ 16281115 prog_main0 } = x_3735 1114 1116 in 1115 1117 h_mk_program prog_vars0 prog_funct0 prog_main0 … … 1118 1120 (((ident, region) Types.prod, 'a2) Types.prod List.list > (ident, 'a1) 1119 1121 Types.prod List.list > ident > 'a3) > ('a1, 'a2) program > 'a3 **) 1120 let rec program_rect_Type5 h_mk_program x_ 1630=1122 let rec program_rect_Type5 h_mk_program x_3737 = 1121 1123 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1122 prog_main0 } = x_ 16301124 prog_main0 } = x_3737 1123 1125 in 1124 1126 h_mk_program prog_vars0 prog_funct0 prog_main0 … … 1127 1129 (((ident, region) Types.prod, 'a2) Types.prod List.list > (ident, 'a1) 1128 1130 Types.prod List.list > ident > 'a3) > ('a1, 'a2) program > 'a3 **) 1129 let rec program_rect_Type3 h_mk_program x_ 1632=1131 let rec program_rect_Type3 h_mk_program x_3739 = 1130 1132 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1131 prog_main0 } = x_ 16321133 prog_main0 } = x_3739 1132 1134 in 1133 1135 h_mk_program prog_vars0 prog_funct0 prog_main0 … … 1136 1138 (((ident, region) Types.prod, 'a2) Types.prod List.list > (ident, 'a1) 1137 1139 Types.prod List.list > ident > 'a3) > ('a1, 'a2) program > 'a3 **) 1138 let rec program_rect_Type2 h_mk_program x_ 1634=1140 let rec program_rect_Type2 h_mk_program x_3741 = 1139 1141 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1140 prog_main0 } = x_ 16341142 prog_main0 } = x_3741 1141 1143 in 1142 1144 h_mk_program prog_vars0 prog_funct0 prog_main0 … … 1145 1147 (((ident, region) Types.prod, 'a2) Types.prod List.list > (ident, 'a1) 1146 1148 Types.prod List.list > ident > 'a3) > ('a1, 'a2) program > 'a3 **) 1147 let rec program_rect_Type1 h_mk_program x_ 1636=1149 let rec program_rect_Type1 h_mk_program x_3743 = 1148 1150 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1149 prog_main0 } = x_ 16361151 prog_main0 } = x_3743 1150 1152 in 1151 1153 h_mk_program prog_vars0 prog_funct0 prog_main0 … … 1154 1156 (((ident, region) Types.prod, 'a2) Types.prod List.list > (ident, 'a1) 1155 1157 Types.prod List.list > ident > 'a3) > ('a1, 'a2) program > 'a3 **) 1156 let rec program_rect_Type0 h_mk_program x_ 1638=1158 let rec program_rect_Type0 h_mk_program x_3745 = 1157 1159 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1158 prog_main0 } = x_ 16381160 prog_main0 } = x_3745 1159 1161 in 1160 1162 h_mk_program prog_vars0 prog_funct0 prog_main0 … … 1479 1481 (** val external_function_rect_Type4 : 1480 1482 (ident > signature > 'a1) > external_function > 'a1 **) 1481 let rec external_function_rect_Type4 h_mk_external_function x_ 1842=1482 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 1842in1483 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 1483 1485 h_mk_external_function ef_id0 ef_sig0 1484 1486 1485 1487 (** val external_function_rect_Type5 : 1486 1488 (ident > signature > 'a1) > external_function > 'a1 **) 1487 let rec external_function_rect_Type5 h_mk_external_function x_ 1844=1488 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 1844in1489 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 1489 1491 h_mk_external_function ef_id0 ef_sig0 1490 1492 1491 1493 (** val external_function_rect_Type3 : 1492 1494 (ident > signature > 'a1) > external_function > 'a1 **) 1493 let rec external_function_rect_Type3 h_mk_external_function x_ 1846=1494 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 1846in1495 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 1495 1497 h_mk_external_function ef_id0 ef_sig0 1496 1498 1497 1499 (** val external_function_rect_Type2 : 1498 1500 (ident > signature > 'a1) > external_function > 'a1 **) 1499 let rec external_function_rect_Type2 h_mk_external_function x_ 1848=1500 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 1848in1501 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 1501 1503 h_mk_external_function ef_id0 ef_sig0 1502 1504 1503 1505 (** val external_function_rect_Type1 : 1504 1506 (ident > signature > 'a1) > external_function > 'a1 **) 1505 let rec external_function_rect_Type1 h_mk_external_function x_ 1850=1506 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 1850in1507 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 1507 1509 h_mk_external_function ef_id0 ef_sig0 1508 1510 1509 1511 (** val external_function_rect_Type0 : 1510 1512 (ident > signature > 'a1) > external_function > 'a1 **) 1511 let rec external_function_rect_Type0 h_mk_external_function x_ 1852=1512 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 1852in1513 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 1513 1515 h_mk_external_function ef_id0 ef_sig0 1514 1516 … … 1577 1579 ('a1 > 'a2) > (external_function > 'a2) > 'a1 fundef > 'a2 **) 1578 1580 let rec fundef_rect_Type4 h_Internal h_External = function 1579  Internal x_ 1872 > h_Internal x_18721580  External x_ 1873 > h_External x_18731581  Internal x_3979 > h_Internal x_3979 1582  External x_3980 > h_External x_3980 1581 1583 1582 1584 (** val fundef_rect_Type5 : 1583 1585 ('a1 > 'a2) > (external_function > 'a2) > 'a1 fundef > 'a2 **) 1584 1586 let rec fundef_rect_Type5 h_Internal h_External = function 1585  Internal x_ 1877 > h_Internal x_18771586  External x_ 1878 > h_External x_18781587  Internal x_3984 > h_Internal x_3984 1588  External x_3985 > h_External x_3985 1587 1589 1588 1590 (** val fundef_rect_Type3 : 1589 1591 ('a1 > 'a2) > (external_function > 'a2) > 'a1 fundef > 'a2 **) 1590 1592 let rec fundef_rect_Type3 h_Internal h_External = function 1591  Internal x_ 1882 > h_Internal x_18821592  External x_ 1883 > h_External x_18831593  Internal x_3989 > h_Internal x_3989 1594  External x_3990 > h_External x_3990 1593 1595 1594 1596 (** val fundef_rect_Type2 : 1595 1597 ('a1 > 'a2) > (external_function > 'a2) > 'a1 fundef > 'a2 **) 1596 1598 let rec fundef_rect_Type2 h_Internal h_External = function 1597  Internal x_ 1887 > h_Internal x_18871598  External x_ 1888 > h_External x_18881599  Internal x_3994 > h_Internal x_3994 1600  External x_3995 > h_External x_3995 1599 1601 1600 1602 (** val fundef_rect_Type1 : 1601 1603 ('a1 > 'a2) > (external_function > 'a2) > 'a1 fundef > 'a2 **) 1602 1604 let rec fundef_rect_Type1 h_Internal h_External = function 1603  Internal x_ 1892 > h_Internal x_18921604  External x_ 1893 > h_External x_18931605  Internal x_3999 > h_Internal x_3999 1606  External x_4000 > h_External x_4000 1605 1607 1606 1608 (** val fundef_rect_Type0 : 1607 1609 ('a1 > 'a2) > (external_function > 'a2) > 'a1 fundef > 'a2 **) 1608 1610 let rec fundef_rect_Type0 h_Internal h_External = function 1609  Internal x_ 1897 > h_Internal x_18971610  External x_ 1898 > h_External x_18981611  Internal x_4004 > h_Internal x_4004 1612  External x_4005 > h_External x_4005 1611 1613 1612 1614 (** val fundef_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.