Changeset 2997 for extracted/aST.ml
 Timestamp:
 Mar 28, 2013, 10:27:41 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/aST.ml
r2827 r2997 418 418 (intsize > signedness > 'a1) > 'a1 > typ > 'a1 **) 419 419 let rec typ_rect_Type4 h_ASTint h_ASTptr = function 420  ASTint (x_ 3649, x_3648) > h_ASTint x_3649 x_3648420  ASTint (x_411, x_410) > h_ASTint x_411 x_410 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_ 3654, x_3653) > h_ASTint x_3654 x_3653426  ASTint (x_416, x_415) > h_ASTint x_416 x_415 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_ 3659, x_3658) > h_ASTint x_3659 x_3658432  ASTint (x_421, x_420) > h_ASTint x_421 x_420 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_ 3664, x_3663) > h_ASTint x_3664 x_3663438  ASTint (x_426, x_425) > h_ASTint x_426 x_425 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_ 3669, x_3668) > h_ASTint x_3669 x_3668444  ASTint (x_431, x_430) > h_ASTint x_431 x_430 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_ 3674, x_3673) > h_ASTint x_3674 x_3673450  ASTint (x_436, x_435) > h_ASTint x_436 x_435 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_ 3709=880 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 3709in879 let rec signature_rect_Type4 h_mk_signature x_471 = 880 let { sig_args = sig_args0; sig_res = sig_res0 } = x_471 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_ 3711=886 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 3711in885 let rec signature_rect_Type5 h_mk_signature x_473 = 886 let { sig_args = sig_args0; sig_res = sig_res0 } = x_473 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_ 3713=892 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 3713in891 let rec signature_rect_Type3 h_mk_signature x_475 = 892 let { sig_args = sig_args0; sig_res = sig_res0 } = x_475 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_ 3715=898 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 3715in897 let rec signature_rect_Type2 h_mk_signature x_477 = 898 let { sig_args = sig_args0; sig_res = sig_res0 } = x_477 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_ 3717=904 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 3717in903 let rec signature_rect_Type1 h_mk_signature x_479 = 904 let { sig_args = sig_args0; sig_res = sig_res0 } = x_479 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_ 3719=910 let { sig_args = sig_args0; sig_res = sig_res0 } = x_ 3719in909 let rec signature_rect_Type0 h_mk_signature x_481 = 910 let { sig_args = sig_args0; sig_res = sig_res0 } = x_481 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_ 3747 > h_Init_int8 x_3747987  Init_int16 x_ 3748 > h_Init_int16 x_3748988  Init_int32 x_ 3749 > h_Init_int32 x_3749989  Init_space x_ 3750 > h_Init_space x_3750986  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 990 990  Init_null > h_Init_null 991  Init_addrof (x_ 3752, x_3751) > h_Init_addrof x_3752 x_3751991  Init_addrof (x_514, x_513) > h_Init_addrof x_514 x_513 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_ 3760 > h_Init_int8 x_3760998  Init_int16 x_ 3761 > h_Init_int16 x_3761999  Init_int32 x_ 3762 > h_Init_int32 x_37621000  Init_space x_ 3763 > h_Init_space x_3763997  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 1001 1001  Init_null > h_Init_null 1002  Init_addrof (x_ 3765, x_3764) > h_Init_addrof x_3765 x_37641002  Init_addrof (x_527, x_526) > h_Init_addrof x_527 x_526 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_ 3773 > h_Init_int8 x_37731009  Init_int16 x_ 3774 > h_Init_int16 x_37741010  Init_int32 x_ 3775 > h_Init_int32 x_37751011  Init_space x_ 3776 > h_Init_space x_37761008  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 1012 1012  Init_null > h_Init_null 1013  Init_addrof (x_ 3778, x_3777) > h_Init_addrof x_3778 x_37771013  Init_addrof (x_540, x_539) > h_Init_addrof x_540 x_539 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_ 3786 > h_Init_int8 x_37861020  Init_int16 x_ 3787 > h_Init_int16 x_37871021  Init_int32 x_ 3788 > h_Init_int32 x_37881022  Init_space x_ 3789 > h_Init_space x_37891019  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 1023 1023  Init_null > h_Init_null 1024  Init_addrof (x_ 3791, x_3790) > h_Init_addrof x_3791 x_37901024  Init_addrof (x_553, x_552) > h_Init_addrof x_553 x_552 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_ 3799 > h_Init_int8 x_37991031  Init_int16 x_ 3800 > h_Init_int16 x_38001032  Init_int32 x_ 3801 > h_Init_int32 x_38011033  Init_space x_ 3802 > h_Init_space x_38021030  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 1034 1034  Init_null > h_Init_null 1035  Init_addrof (x_ 3804, x_3803) > h_Init_addrof x_3804 x_38031035  Init_addrof (x_566, x_565) > h_Init_addrof x_566 x_565 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_ 3812 > h_Init_int8 x_38121042  Init_int16 x_ 3813 > h_Init_int16 x_38131043  Init_int32 x_ 3814 > h_Init_int32 x_38141044  Init_space x_ 3815 > h_Init_space x_38151041  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 1045 1045  Init_null > h_Init_null 1046  Init_addrof (x_ 3817, x_3816) > h_Init_addrof x_3817 x_38161046  Init_addrof (x_579, x_578) > h_Init_addrof x_579 x_578 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_ 3904=1113 let rec program_rect_Type4 h_mk_program x_666 = 1114 1114 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1115 prog_main0 } = x_ 39041115 prog_main0 } = x_666 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_ 3906=1122 let rec program_rect_Type5 h_mk_program x_668 = 1123 1123 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1124 prog_main0 } = x_ 39061124 prog_main0 } = x_668 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_ 3908=1131 let rec program_rect_Type3 h_mk_program x_670 = 1132 1132 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1133 prog_main0 } = x_ 39081133 prog_main0 } = x_670 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_ 3910=1140 let rec program_rect_Type2 h_mk_program x_672 = 1141 1141 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1142 prog_main0 } = x_ 39101142 prog_main0 } = x_672 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_ 3912=1149 let rec program_rect_Type1 h_mk_program x_674 = 1150 1150 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1151 prog_main0 } = x_ 39121151 prog_main0 } = x_674 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_ 3914=1158 let rec program_rect_Type0 h_mk_program x_676 = 1159 1159 let { prog_vars = prog_vars0; prog_funct = prog_funct0; prog_main = 1160 prog_main0 } = x_ 39141160 prog_main0 } = x_676 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_ 4118=1480 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 4118in1479 let rec external_function_rect_Type4 h_mk_external_function x_880 = 1480 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_880 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_ 4120=1486 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 4120in1485 let rec external_function_rect_Type5 h_mk_external_function x_882 = 1486 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_882 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_ 4122=1492 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 4122in1491 let rec external_function_rect_Type3 h_mk_external_function x_884 = 1492 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_884 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_ 4124=1498 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 4124in1497 let rec external_function_rect_Type2 h_mk_external_function x_886 = 1498 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_886 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_ 4126=1504 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 4126in1503 let rec external_function_rect_Type1 h_mk_external_function x_888 = 1504 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_888 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_ 4128=1510 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_ 4128in1509 let rec external_function_rect_Type0 h_mk_external_function x_890 = 1510 let { ef_id = ef_id0; ef_sig = ef_sig0 } = x_890 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_ 4148 > h_Internal x_41481578  External x_ 4149 > h_External x_41491577  Internal x_910 > h_Internal x_910 1578  External x_911 > h_External x_911 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_ 4153 > h_Internal x_41531584  External x_ 4154 > h_External x_41541583  Internal x_915 > h_Internal x_915 1584  External x_916 > h_External x_916 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_ 4158 > h_Internal x_41581590  External x_ 4159 > h_External x_41591589  Internal x_920 > h_Internal x_920 1590  External x_921 > h_External x_921 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_ 4163 > h_Internal x_41631596  External x_ 4164 > h_External x_41641595  Internal x_925 > h_Internal x_925 1596  External x_926 > h_External x_926 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_ 4168 > h_Internal x_41681602  External x_ 4169 > h_External x_41691601  Internal x_930 > h_Internal x_930 1602  External x_931 > h_External x_931 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_ 4173 > h_Internal x_41731608  External x_ 4174 > h_External x_41741607  Internal x_935 > h_Internal x_935 1608  External x_936 > h_External x_936 1609 1609 1610 1610 (** val fundef_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.