Changeset 3043 for extracted/aST.ml
 Timestamp:
 Mar 29, 2013, 6:38:26 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/aST.ml
r2997 r3043 418 418 (intsize > signedness > 'a1) > 'a1 > typ > 'a1 **) 419 419 let rec typ_rect_Type4 h_ASTint h_ASTptr = function 420  ASTint (x_ 411, x_410) > h_ASTint x_411 x_410420  ASTint (x_3662, x_3661) > h_ASTint x_3662 x_3661 421 421  ASTptr > h_ASTptr 422 422 … … 424 424 (intsize > signedness > 'a1) > 'a1 > typ > 'a1 **) 425 425 let rec typ_rect_Type5 h_ASTint h_ASTptr = function 426  ASTint (x_ 416, x_415) > h_ASTint x_416 x_415426  ASTint (x_3667, x_3666) > h_ASTint x_3667 x_3666 427 427  ASTptr > h_ASTptr 428 428 … … 430 430 (intsize > signedness > 'a1) > 'a1 > typ > 'a1 **) 431 431 let rec typ_rect_Type3 h_ASTint h_ASTptr = function 432  ASTint (x_ 421, x_420) > h_ASTint x_421 x_420432  ASTint (x_3672, x_3671) > h_ASTint x_3672 x_3671 433 433  ASTptr > h_ASTptr 434 434 … … 436 436 (intsize > signedness > 'a1) > 'a1 > typ > 'a1 **) 437 437 let rec typ_rect_Type2 h_ASTint h_ASTptr = function 438  ASTint (x_ 426, x_425) > h_ASTint x_426 x_425438  ASTint (x_3677, x_3676) > h_ASTint x_3677 x_3676 439 439  ASTptr > h_ASTptr 440 440 … … 442 442 (intsize > signedness > 'a1) > 'a1 > typ > 'a1 **) 443 443 let rec typ_rect_Type1 h_ASTint h_ASTptr = function 444  ASTint (x_ 431, x_430) > h_ASTint x_431 x_430444  ASTint (x_3682, x_3681) > h_ASTint x_3682 x_3681 445 445  ASTptr > h_ASTptr 446 446 … … 448 448 (intsize > signedness > 'a1) > 'a1 > typ > 'a1 **) 449 449 let rec typ_rect_Type0 h_ASTint h_ASTptr = function 450  ASTint (x_ 436, x_435) > h_ASTint x_436 x_435450  ASTint (x_3687, x_3686) > h_ASTint x_3687 x_3686 451 451  ASTptr > h_ASTptr 452 452 … … 877 877 (** val signature_rect_Type4 : 878 878 (typ List.list > typ Types.option > 'a1) > signature > 'a1 **) 879 let rec signature_rect_Type4 h_mk_signature x_ 471=880 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 471in879 let rec signature_rect_Type4 h_mk_signature x_3722 = 880 let { sig_args = sig_args0; sig_res = sig_res0 } = x_3722 in 881 881 h_mk_signature sig_args0 sig_res0 882 882 883 883 (** val signature_rect_Type5 : 884 884 (typ List.list > typ Types.option > 'a1) > signature > 'a1 **) 885 let rec signature_rect_Type5 h_mk_signature x_ 473=886 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 473in885 let rec signature_rect_Type5 h_mk_signature x_3724 = 886 let { sig_args = sig_args0; sig_res = sig_res0 } = x_3724 in 887 887 h_mk_signature sig_args0 sig_res0 888 888 889 889 (** val signature_rect_Type3 : 890 890 (typ List.list > typ Types.option > 'a1) > signature > 'a1 **) 891 let rec signature_rect_Type3 h_mk_signature x_ 475=892 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 475in891 let rec signature_rect_Type3 h_mk_signature x_3726 = 892 let { sig_args = sig_args0; sig_res = sig_res0 } = x_3726 in 893 893 h_mk_signature sig_args0 sig_res0 894 894 895 895 (** val signature_rect_Type2 : 896 896 (typ List.list > typ Types.option > 'a1) > signature > 'a1 **) 897 let rec signature_rect_Type2 h_mk_signature x_ 477=898 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 477in897 let rec signature_rect_Type2 h_mk_signature x_3728 = 898 let { sig_args = sig_args0; sig_res = sig_res0 } = x_3728 in 899 899 h_mk_signature sig_args0 sig_res0 900 900 901 901 (** val signature_rect_Type1 : 902 902 (typ List.list > typ Types.option > 'a1) > signature > 'a1 **) 903 let rec signature_rect_Type1 h_mk_signature x_ 479=904 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 479in903 let rec signature_rect_Type1 h_mk_signature x_3730 = 904 let { sig_args = sig_args0; sig_res = sig_res0 } = x_3730 in 905 905 h_mk_signature sig_args0 sig_res0 906 906 907 907 (** val signature_rect_Type0 : 908 908 (typ List.list > typ Types.option > 'a1) > signature > 'a1 **) 909 let rec signature_rect_Type0 h_mk_signature x_ 481=910 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 481in909 let rec signature_rect_Type0 h_mk_signature x_3732 = 910 let { sig_args = sig_args0; sig_res = sig_res0 } = x_3732 in 911 911 h_mk_signature sig_args0 sig_res0 912 912 … … 984 984 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 **) 985 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_ 509 > h_Init_int8 x_509987  Init_int16 x_ 510 > h_Init_int16 x_510988  Init_int32 x_ 511 > h_Init_int32 x_511989  Init_space x_ 512 > h_Init_space x_512986  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 990  Init_null > h_Init_null 991  Init_addrof (x_ 514, x_513) > h_Init_addrof x_514 x_513991  Init_addrof (x_3765, x_3764) > h_Init_addrof x_3765 x_3764 992 992 993 993 (** val init_data_rect_Type5 : … … 995 995 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 **) 996 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_ 522 > h_Init_int8 x_522998  Init_int16 x_ 523 > h_Init_int16 x_523999  Init_int32 x_ 524 > h_Init_int32 x_5241000  Init_space x_ 525 > h_Init_space x_525997  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 1001  Init_null > h_Init_null 1002  Init_addrof (x_ 527, x_526) > h_Init_addrof x_527 x_5261002  Init_addrof (x_3778, x_3777) > h_Init_addrof x_3778 x_3777 1003 1003 1004 1004 (** val init_data_rect_Type3 : … … 1006 1006 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 **) 1007 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_ 535 > h_Init_int8 x_5351009  Init_int16 x_ 536 > h_Init_int16 x_5361010  Init_int32 x_ 537 > h_Init_int32 x_5371011  Init_space x_ 538 > h_Init_space x_5381008  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 1012  Init_null > h_Init_null 1013  Init_addrof (x_ 540, x_539) > h_Init_addrof x_540 x_5391013  Init_addrof (x_3791, x_3790) > h_Init_addrof x_3791 x_3790 1014 1014 1015 1015 (** val init_data_rect_Type2 : … … 1017 1017 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 **) 1018 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_ 548 > h_Init_int8 x_5481020  Init_int16 x_ 549 > h_Init_int16 x_5491021  Init_int32 x_ 550 > h_Init_int32 x_5501022  Init_space x_ 551 > h_Init_space x_5511019  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 1023  Init_null > h_Init_null 1024  Init_addrof (x_ 553, x_552) > h_Init_addrof x_553 x_5521024  Init_addrof (x_3804, x_3803) > h_Init_addrof x_3804 x_3803 1025 1025 1026 1026 (** val init_data_rect_Type1 : … … 1028 1028 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 **) 1029 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_ 561 > h_Init_int8 x_5611031  Init_int16 x_ 562 > h_Init_int16 x_5621032  Init_int32 x_ 563 > h_Init_int32 x_5631033  Init_space x_ 564 > h_Init_space x_5641030  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 1034  Init_null > h_Init_null 1035  Init_addrof (x_ 566, x_565) > h_Init_addrof x_566 x_5651035  Init_addrof (x_3817, x_3816) > h_Init_addrof x_3817 x_3816 1036 1036 1037 1037 (** val init_data_rect_Type0 : … … 1039 1039 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 **) 1040 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_ 574 > h_Init_int8 x_5741042  Init_int16 x_ 575 > h_Init_int16 x_5751043  Init_int32 x_ 576 > h_Init_int32 x_5761044  Init_space x_ 577 > h_Init_space x_5771041  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 1045  Init_null > h_Init_null 1046  Init_addrof (x_ 579, x_578) > h_Init_addrof x_579 x_5781046  Init_addrof (x_3830, x_3829) > h_Init_addrof x_3830 x_3829 1047 1047 1048 1048 (** val init_data_inv_rect_Type4 : … … 1111 1111 (((ident, region) Types.prod, 'a2) Types.prod List.list > (ident, 'a1) 1112 1112 Types.prod List.list > ident > 'a3) > ('a1, 'a2) program > 'a3 **) 1113 let rec program_rect_Type4 h_mk_program x_ 666=1113 let rec program_rect_Type4 h_mk_program x_3917 = 1114 1114 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1115 prog_main0 } = x_ 6661115 prog_main0 } = x_3917 1116 1116 in 1117 1117 h_mk_program prog_vars0 prog_funct0 prog_main0 … … 1120 1120 (((ident, region) Types.prod, 'a2) Types.prod List.list > (ident, 'a1) 1121 1121 Types.prod List.list > ident > 'a3) > ('a1, 'a2) program > 'a3 **) 1122 let rec program_rect_Type5 h_mk_program x_ 668=1122 let rec program_rect_Type5 h_mk_program x_3919 = 1123 1123 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1124 prog_main0 } = x_ 6681124 prog_main0 } = x_3919 1125 1125 in 1126 1126 h_mk_program prog_vars0 prog_funct0 prog_main0 … … 1129 1129 (((ident, region) Types.prod, 'a2) Types.prod List.list > (ident, 'a1) 1130 1130 Types.prod List.list > ident > 'a3) > ('a1, 'a2) program > 'a3 **) 1131 let rec program_rect_Type3 h_mk_program x_ 670=1131 let rec program_rect_Type3 h_mk_program x_3921 = 1132 1132 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1133 prog_main0 } = x_ 6701133 prog_main0 } = x_3921 1134 1134 in 1135 1135 h_mk_program prog_vars0 prog_funct0 prog_main0 … … 1138 1138 (((ident, region) Types.prod, 'a2) Types.prod List.list > (ident, 'a1) 1139 1139 Types.prod List.list > ident > 'a3) > ('a1, 'a2) program > 'a3 **) 1140 let rec program_rect_Type2 h_mk_program x_ 672=1140 let rec program_rect_Type2 h_mk_program x_3923 = 1141 1141 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1142 prog_main0 } = x_ 6721142 prog_main0 } = x_3923 1143 1143 in 1144 1144 h_mk_program prog_vars0 prog_funct0 prog_main0 … … 1147 1147 (((ident, region) Types.prod, 'a2) Types.prod List.list > (ident, 'a1) 1148 1148 Types.prod List.list > ident > 'a3) > ('a1, 'a2) program > 'a3 **) 1149 let rec program_rect_Type1 h_mk_program x_ 674=1149 let rec program_rect_Type1 h_mk_program x_3925 = 1150 1150 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1151 prog_main0 } = x_ 6741151 prog_main0 } = x_3925 1152 1152 in 1153 1153 h_mk_program prog_vars0 prog_funct0 prog_main0 … … 1156 1156 (((ident, region) Types.prod, 'a2) Types.prod List.list > (ident, 'a1) 1157 1157 Types.prod List.list > ident > 'a3) > ('a1, 'a2) program > 'a3 **) 1158 let rec program_rect_Type0 h_mk_program x_ 676=1158 let rec program_rect_Type0 h_mk_program x_3927 = 1159 1159 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1160 prog_main0 } = x_ 6761160 prog_main0 } = x_3927 1161 1161 in 1162 1162 h_mk_program prog_vars0 prog_funct0 prog_main0 … … 1477 1477 (** val external_function_rect_Type4 : 1478 1478 (ident > signature > 'a1) > external_function > 'a1 **) 1479 let rec external_function_rect_Type4 h_mk_external_function x_ 880=1480 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 880in1479 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 1481 h_mk_external_function ef_id0 ef_sig0 1482 1482 1483 1483 (** val external_function_rect_Type5 : 1484 1484 (ident > signature > 'a1) > external_function > 'a1 **) 1485 let rec external_function_rect_Type5 h_mk_external_function x_ 882=1486 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 882in1485 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 1487 h_mk_external_function ef_id0 ef_sig0 1488 1488 1489 1489 (** val external_function_rect_Type3 : 1490 1490 (ident > signature > 'a1) > external_function > 'a1 **) 1491 let rec external_function_rect_Type3 h_mk_external_function x_ 884=1492 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 884in1491 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 1493 h_mk_external_function ef_id0 ef_sig0 1494 1494 1495 1495 (** val external_function_rect_Type2 : 1496 1496 (ident > signature > 'a1) > external_function > 'a1 **) 1497 let rec external_function_rect_Type2 h_mk_external_function x_ 886=1498 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 886in1497 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 1499 h_mk_external_function ef_id0 ef_sig0 1500 1500 1501 1501 (** val external_function_rect_Type1 : 1502 1502 (ident > signature > 'a1) > external_function > 'a1 **) 1503 let rec external_function_rect_Type1 h_mk_external_function x_ 888=1504 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 888in1503 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 1505 h_mk_external_function ef_id0 ef_sig0 1506 1506 1507 1507 (** val external_function_rect_Type0 : 1508 1508 (ident > signature > 'a1) > external_function > 'a1 **) 1509 let rec external_function_rect_Type0 h_mk_external_function x_ 890=1510 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 890in1509 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 1511 h_mk_external_function ef_id0 ef_sig0 1512 1512 … … 1575 1575 ('a1 > 'a2) > (external_function > 'a2) > 'a1 fundef > 'a2 **) 1576 1576 let rec fundef_rect_Type4 h_Internal h_External = function 1577  Internal x_ 910 > h_Internal x_9101578  External x_ 911 > h_External x_9111577  Internal x_4161 > h_Internal x_4161 1578  External x_4162 > h_External x_4162 1579 1579 1580 1580 (** val fundef_rect_Type5 : 1581 1581 ('a1 > 'a2) > (external_function > 'a2) > 'a1 fundef > 'a2 **) 1582 1582 let rec fundef_rect_Type5 h_Internal h_External = function 1583  Internal x_ 915 > h_Internal x_9151584  External x_ 916 > h_External x_9161583  Internal x_4166 > h_Internal x_4166 1584  External x_4167 > h_External x_4167 1585 1585 1586 1586 (** val fundef_rect_Type3 : 1587 1587 ('a1 > 'a2) > (external_function > 'a2) > 'a1 fundef > 'a2 **) 1588 1588 let rec fundef_rect_Type3 h_Internal h_External = function 1589  Internal x_ 920 > h_Internal x_9201590  External x_ 921 > h_External x_9211589  Internal x_4171 > h_Internal x_4171 1590  External x_4172 > h_External x_4172 1591 1591 1592 1592 (** val fundef_rect_Type2 : 1593 1593 ('a1 > 'a2) > (external_function > 'a2) > 'a1 fundef > 'a2 **) 1594 1594 let rec fundef_rect_Type2 h_Internal h_External = function 1595  Internal x_ 925 > h_Internal x_9251596  External x_ 926 > h_External x_9261595  Internal x_4176 > h_Internal x_4176 1596  External x_4177 > h_External x_4177 1597 1597 1598 1598 (** val fundef_rect_Type1 : 1599 1599 ('a1 > 'a2) > (external_function > 'a2) > 'a1 fundef > 'a2 **) 1600 1600 let rec fundef_rect_Type1 h_Internal h_External = function 1601  Internal x_ 930 > h_Internal x_9301602  External x_ 931 > h_External x_9311601  Internal x_4181 > h_Internal x_4181 1602  External x_4182 > h_External x_4182 1603 1603 1604 1604 (** val fundef_rect_Type0 : 1605 1605 ('a1 > 'a2) > (external_function > 'a2) > 'a1 fundef > 'a2 **) 1606 1606 let rec fundef_rect_Type0 h_Internal h_External = function 1607  Internal x_ 935 > h_Internal x_9351608  External x_ 936 > h_External x_9361607  Internal x_4186 > h_Internal x_4186 1608  External x_4187 > h_External x_4187 1609 1609 1610 1610 (** val fundef_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.