/usr/lib/ocaml/compiler-libs/typing/ctype.ml is in ocaml-compiler-libs 3.12.1-2ubuntu2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411 1412 1413 1414 1415 1416 1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 1433 1434 1435 1436 1437 1438 1439 1440 1441 1442 1443 1444 1445 1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456 1457 1458 1459 1460 1461 1462 1463 1464 1465 1466 1467 1468 1469 1470 1471 1472 1473 1474 1475 1476 1477 1478 1479 1480 1481 1482 1483 1484 1485 1486 1487 1488 1489 1490 1491 1492 1493 1494 1495 1496 1497 1498 1499 1500 1501 1502 1503 1504 1505 1506 1507 1508 1509 1510 1511 1512 1513 1514 1515 1516 1517 1518 1519 1520 1521 1522 1523 1524 1525 1526 1527 1528 1529 1530 1531 1532 1533 1534 1535 1536 1537 1538 1539 1540 1541 1542 1543 1544 1545 1546 1547 1548 1549 1550 1551 1552 1553 1554 1555 1556 1557 1558 1559 1560 1561 1562 1563 1564 1565 1566 1567 1568 1569 1570 1571 1572 1573 1574 1575 1576 1577 1578 1579 1580 1581 1582 1583 1584 1585 1586 1587 1588 1589 1590 1591 1592 1593 1594 1595 1596 1597 1598 1599 1600 1601 1602 1603 1604 1605 1606 1607 1608 1609 1610 1611 1612 1613 1614 1615 1616 1617 1618 1619 1620 1621 1622 1623 1624 1625 1626 1627 1628 1629 1630 1631 1632 1633 1634 1635 1636 1637 1638 1639 1640 1641 1642 1643 1644 1645 1646 1647 1648 1649 1650 1651 1652 1653 1654 1655 1656 1657 1658 1659 1660 1661 1662 1663 1664 1665 1666 1667 1668 1669 1670 1671 1672 1673 1674 1675 1676 1677 1678 1679 1680 1681 1682 1683 1684 1685 1686 1687 1688 1689 1690 1691 1692 1693 1694 1695 1696 1697 1698 1699 1700 1701 1702 1703 1704 1705 1706 1707 1708 1709 1710 1711 1712 1713 1714 1715 1716 1717 1718 1719 1720 1721 1722 1723 1724 1725 1726 1727 1728 1729 1730 1731 1732 1733 1734 1735 1736 1737 1738 1739 1740 1741 1742 1743 1744 1745 1746 1747 1748 1749 1750 1751 1752 1753 1754 1755 1756 1757 1758 1759 1760 1761 1762 1763 1764 1765 1766 1767 1768 1769 1770 1771 1772 1773 1774 1775 1776 1777 1778 1779 1780 1781 1782 1783 1784 1785 1786 1787 1788 1789 1790 1791 1792 1793 1794 1795 1796 1797 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808 1809 1810 1811 1812 1813 1814 1815 1816 1817 1818 1819 1820 1821 1822 1823 1824 1825 1826 1827 1828 1829 1830 1831 1832 1833 1834 1835 1836 1837 1838 1839 1840 1841 1842 1843 1844 1845 1846 1847 1848 1849 1850 1851 1852 1853 1854 1855 1856 1857 1858 1859 1860 1861 1862 1863 1864 1865 1866 1867 1868 1869 1870 1871 1872 1873 1874 1875 1876 1877 1878 1879 1880 1881 1882 1883 1884 1885 1886 1887 1888 1889 1890 1891 1892 1893 1894 1895 1896 1897 1898 1899 1900 1901 1902 1903 1904 1905 1906 1907 1908 1909 1910 1911 1912 1913 1914 1915 1916 1917 1918 1919 1920 1921 1922 1923 1924 1925 1926 1927 1928 1929 1930 1931 1932 1933 1934 1935 1936 1937 1938 1939 1940 1941 1942 1943 1944 1945 1946 1947 1948 1949 1950 1951 1952 1953 1954 1955 1956 1957 1958 1959 1960 1961 1962 1963 1964 1965 1966 1967 1968 1969 1970 1971 1972 1973 1974 1975 1976 1977 1978 1979 1980 1981 1982 1983 1984 1985 1986 1987 1988 1989 1990 1991 1992 1993 1994 1995 1996 1997 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018 2019 2020 2021 2022 2023 2024 2025 2026 2027 2028 2029 2030 2031 2032 2033 2034 2035 2036 2037 2038 2039 2040 2041 2042 2043 2044 2045 2046 2047 2048 2049 2050 2051 2052 2053 2054 2055 2056 2057 2058 2059 2060 2061 2062 2063 2064 2065 2066 2067 2068 2069 2070 2071 2072 2073 2074 2075 2076 2077 2078 2079 2080 2081 2082 2083 2084 2085 2086 2087 2088 2089 2090 2091 2092 2093 2094 2095 2096 2097 2098 2099 2100 2101 2102 2103 2104 2105 2106 2107 2108 2109 2110 2111 2112 2113 2114 2115 2116 2117 2118 2119 2120 2121 2122 2123 2124 2125 2126 2127 2128 2129 2130 2131 2132 2133 2134 2135 2136 2137 2138 2139 2140 2141 2142 2143 2144 2145 2146 2147 2148 2149 2150 2151 2152 2153 2154 2155 2156 2157 2158 2159 2160 2161 2162 2163 2164 2165 2166 2167 2168 2169 2170 2171 2172 2173 2174 2175 2176 2177 2178 2179 2180 2181 2182 2183 2184 2185 2186 2187 2188 2189 2190 2191 2192 2193 2194 2195 2196 2197 2198 2199 2200 2201 2202 2203 2204 2205 2206 2207 2208 2209 2210 2211 2212 2213 2214 2215 2216 2217 2218 2219 2220 2221 2222 2223 2224 2225 2226 2227 2228 2229 2230 2231 2232 2233 2234 2235 2236 2237 2238 2239 2240 2241 2242 2243 2244 2245 2246 2247 2248 2249 2250 2251 2252 2253 2254 2255 2256 2257 2258 2259 2260 2261 2262 2263 2264 2265 2266 2267 2268 2269 2270 2271 2272 2273 2274 2275 2276 2277 2278 2279 2280 2281 2282 2283 2284 2285 2286 2287 2288 2289 2290 2291 2292 2293 2294 2295 2296 2297 2298 2299 2300 2301 2302 2303 2304 2305 2306 2307 2308 2309 2310 2311 2312 2313 2314 2315 2316 2317 2318 2319 2320 2321 2322 2323 2324 2325 2326 2327 2328 2329 2330 2331 2332 2333 2334 2335 2336 2337 2338 2339 2340 2341 2342 2343 2344 2345 2346 2347 2348 2349 2350 2351 2352 2353 2354 2355 2356 2357 2358 2359 2360 2361 2362 2363 2364 2365 2366 2367 2368 2369 2370 2371 2372 2373 2374 2375 2376 2377 2378 2379 2380 2381 2382 2383 2384 2385 2386 2387 2388 2389 2390 2391 2392 2393 2394 2395 2396 2397 2398 2399 2400 2401 2402 2403 2404 2405 2406 2407 2408 2409 2410 2411 2412 2413 2414 2415 2416 2417 2418 2419 2420 2421 2422 2423 2424 2425 2426 2427 2428 2429 2430 2431 2432 2433 2434 2435 2436 2437 2438 2439 2440 2441 2442 2443 2444 2445 2446 2447 2448 2449 2450 2451 2452 2453 2454 2455 2456 2457 2458 2459 2460 2461 2462 2463 2464 2465 2466 2467 2468 2469 2470 2471 2472 2473 2474 2475 2476 2477 2478 2479 2480 2481 2482 2483 2484 2485 2486 2487 2488 2489 2490 2491 2492 2493 2494 2495 2496 2497 2498 2499 2500 2501 2502 2503 2504 2505 2506 2507 2508 2509 2510 2511 2512 2513 2514 2515 2516 2517 2518 2519 2520 2521 2522 2523 2524 2525 2526 2527 2528 2529 2530 2531 2532 2533 2534 2535 2536 2537 2538 2539 2540 2541 2542 2543 2544 2545 2546 2547 2548 2549 2550 2551 2552 2553 2554 2555 2556 2557 2558 2559 2560 2561 2562 2563 2564 2565 2566 2567 2568 2569 2570 2571 2572 2573 2574 2575 2576 2577 2578 2579 2580 2581 2582 2583 2584 2585 2586 2587 2588 2589 2590 2591 2592 2593 2594 2595 2596 2597 2598 2599 2600 2601 2602 2603 2604 2605 2606 2607 2608 2609 2610 2611 2612 2613 2614 2615 2616 2617 2618 2619 2620 2621 2622 2623 2624 2625 2626 2627 2628 2629 2630 2631 2632 2633 2634 2635 2636 2637 2638 2639 2640 2641 2642 2643 2644 2645 2646 2647 2648 2649 2650 2651 2652 2653 2654 2655 2656 2657 2658 2659 2660 2661 2662 2663 2664 2665 2666 2667 2668 2669 2670 2671 2672 2673 2674 2675 2676 2677 2678 2679 2680 2681 2682 2683 2684 2685 2686 2687 2688 2689 2690 2691 2692 2693 2694 2695 2696 2697 2698 2699 2700 2701 2702 2703 2704 2705 2706 2707 2708 2709 2710 2711 2712 2713 2714 2715 2716 2717 2718 2719 2720 2721 2722 2723 2724 2725 2726 2727 2728 2729 2730 2731 2732 2733 2734 2735 2736 2737 2738 2739 2740 2741 2742 2743 2744 2745 2746 2747 2748 2749 2750 2751 2752 2753 2754 2755 2756 2757 2758 2759 2760 2761 2762 2763 2764 2765 2766 2767 2768 2769 2770 2771 2772 2773 2774 2775 2776 2777 2778 2779 2780 2781 2782 2783 2784 2785 2786 2787 2788 2789 2790 2791 2792 2793 2794 2795 2796 2797 2798 2799 2800 2801 2802 2803 2804 2805 2806 2807 2808 2809 2810 2811 2812 2813 2814 2815 2816 2817 2818 2819 2820 2821 2822 2823 2824 2825 2826 2827 2828 2829 2830 2831 2832 2833 2834 2835 2836 2837 2838 2839 2840 2841 2842 2843 2844 2845 2846 2847 2848 2849 2850 2851 2852 2853 2854 2855 2856 2857 2858 2859 2860 2861 2862 2863 2864 2865 2866 2867 2868 2869 2870 2871 2872 2873 2874 2875 2876 2877 2878 2879 2880 2881 2882 2883 2884 2885 2886 2887 2888 2889 2890 2891 2892 2893 2894 2895 2896 2897 2898 2899 2900 2901 2902 2903 2904 2905 2906 2907 2908 2909 2910 2911 2912 2913 2914 2915 2916 2917 2918 2919 2920 2921 2922 2923 2924 2925 2926 2927 2928 2929 2930 2931 2932 2933 2934 2935 2936 2937 2938 2939 2940 2941 2942 2943 2944 2945 2946 2947 2948 2949 2950 2951 2952 2953 2954 2955 2956 2957 2958 2959 2960 2961 2962 2963 2964 2965 2966 2967 2968 2969 2970 2971 2972 2973 2974 2975 2976 2977 2978 2979 2980 2981 2982 2983 2984 2985 2986 2987 2988 2989 2990 2991 2992 2993 2994 2995 2996 2997 2998 2999 3000 3001 3002 3003 3004 3005 3006 3007 3008 3009 3010 3011 3012 3013 3014 3015 3016 3017 3018 3019 3020 3021 3022 3023 3024 3025 3026 3027 3028 3029 3030 3031 3032 3033 3034 3035 3036 3037 3038 3039 3040 3041 3042 3043 3044 3045 3046 3047 3048 3049 3050 3051 3052 3053 3054 3055 3056 3057 3058 3059 3060 3061 3062 3063 3064 3065 3066 3067 3068 3069 3070 3071 3072 3073 3074 3075 3076 3077 3078 3079 3080 3081 3082 3083 3084 3085 3086 3087 3088 3089 3090 3091 3092 3093 3094 3095 3096 3097 3098 3099 3100 3101 3102 3103 3104 3105 3106 3107 3108 3109 3110 3111 3112 3113 3114 3115 3116 3117 3118 3119 3120 3121 3122 3123 3124 3125 3126 3127 3128 3129 3130 3131 3132 3133 3134 3135 3136 3137 3138 3139 3140 3141 3142 3143 3144 3145 3146 3147 3148 3149 3150 3151 3152 3153 3154 3155 3156 3157 3158 3159 3160 3161 3162 3163 3164 3165 3166 3167 3168 3169 3170 3171 3172 3173 3174 3175 3176 3177 3178 3179 3180 3181 3182 3183 3184 3185 3186 3187 3188 3189 3190 3191 3192 3193 3194 3195 3196 3197 3198 3199 3200 3201 3202 3203 3204 3205 3206 3207 3208 3209 3210 3211 3212 3213 3214 3215 3216 3217 3218 3219 3220 3221 3222 3223 3224 3225 3226 3227 3228 3229 3230 3231 3232 3233 3234 3235 3236 3237 3238 3239 3240 3241 3242 3243 3244 3245 3246 3247 3248 3249 3250 3251 3252 3253 3254 3255 3256 3257 3258 3259 3260 3261 3262 3263 3264 3265 3266 3267 3268 3269 3270 3271 3272 3273 3274 3275 3276 3277 3278 3279 3280 3281 3282 3283 3284 3285 3286 3287 3288 3289 3290 3291 3292 3293 3294 3295 3296 3297 3298 3299 3300 3301 3302 3303 3304 3305 3306 3307 3308 3309 3310 3311 3312 3313 3314 3315 3316 3317 3318 3319 3320 3321 3322 3323 3324 3325 3326 3327 3328 3329 3330 3331 3332 3333 3334 3335 3336 3337 3338 3339 3340 3341 3342 3343 3344 3345 3346 3347 3348 3349 3350 3351 3352 3353 3354 3355 3356 3357 3358 3359 3360 3361 3362 3363 3364 3365 3366 3367 3368 3369 3370 3371 3372 3373 3374 3375 3376 3377 3378 3379 3380 3381 3382 3383 3384 3385 3386 3387 3388 3389 3390 3391 3392 3393 3394 3395 3396 3397 3398 3399 3400 3401 3402 3403 3404 3405 3406 3407 3408 3409 3410 3411 3412 3413 3414 3415 3416 3417 3418 3419 3420 3421 3422 3423 3424 3425 3426 3427 3428 3429 3430 3431 3432 3433 3434 3435 3436 3437 3438 3439 3440 3441 3442 3443 3444 3445 3446 3447 3448 3449 3450 3451 3452 3453 3454 3455 3456 3457 3458 3459 3460 3461 3462 3463 3464 3465 3466 3467 3468 3469 3470 3471 3472 3473 3474 3475 3476 3477 3478 3479 3480 3481 3482 3483 3484 3485 3486 3487 3488 3489 3490 3491 3492 3493 3494 | (***********************************************************************)
(* *)
(* Objective Caml *)
(* *)
(* Xavier Leroy and Jerome Vouillon, projet Cristal, INRIA Rocquencourt*)
(* *)
(* Copyright 1996 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed *)
(* under the terms of the Q Public License version 1.0. *)
(* *)
(***********************************************************************)
(* $Id: ctype.ml 10702 2010-10-02 08:56:39Z garrigue $ *)
(* Operations on core types *)
open Misc
open Asttypes
open Types
open Btype
(*
Type manipulation after type inference
======================================
If one wants to manipulate a type after type inference (for
instance, during code generation or in the debugger), one must
first make sure that the type levels are correct, using the
function [correct_levels]. Then, this type can be correctely
manipulated by [apply], [expand_head] and [moregeneral].
*)
(*
General notes
=============
- As much sharing as possible should be kept : it makes types
smaller and better abbreviated.
When necessary, some sharing can be lost. Types will still be
printed correctly (+++ TO DO...), and abbreviations defined by a
class do not depend on sharing thanks to constrained
abbreviations. (Of course, even if some sharing is lost, typing
will still be correct.)
- All nodes of a type have a level : that way, one know whether a
node need to be duplicated or not when instantiating a type.
- Levels of a type are decreasing (generic level being considered
as greatest).
- The level of a type constructor is superior to the binding
time of its path.
- Recursive types without limitation should be handled (even if
there is still an occur check). This avoid treating specially the
case for objects, for instance. Furthermore, the occur check
policy can then be easily changed.
*)
(*
A faire
=======
- Revoir affichage des types.
- Etendre la portee d'un alias [... as 'a] a tout le type englobant.
- #-type implementes comme de vraies abreviations.
- Niveaux plus fins pour les identificateurs :
Champ [global] renomme en [level];
Niveau -1 : global
0 : module toplevel
1 : module contenu dans module toplevel
...
En fait, incrementer le niveau a chaque fois que l'on rentre dans
un module.
3 4 6
\ / /
1 2 5
\|/
0
[Subst] doit ecreter les niveaux (pour qu'un variable non
generalisable dans un module de niveau 2 ne se retrouve pas
generalisable lorsque l'on l'utilise au niveau 0).
- Traitement de la trace de l'unification separe de la fonction
[unify].
*)
(**** Errors ****)
exception Unify of (type_expr * type_expr) list
exception Tags of label * label
exception Subtype of
(type_expr * type_expr) list * (type_expr * type_expr) list
exception Cannot_expand
exception Cannot_apply
exception Recursive_abbrev
(**** Type level management ****)
let current_level = ref 0
let nongen_level = ref 0
let global_level = ref 1
let saved_level = ref []
let init_def level = current_level := level; nongen_level := level
let begin_def () =
saved_level := (!current_level, !nongen_level) :: !saved_level;
incr current_level; nongen_level := !current_level
let begin_class_def () =
saved_level := (!current_level, !nongen_level) :: !saved_level;
incr current_level
let raise_nongen_level () =
saved_level := (!current_level, !nongen_level) :: !saved_level;
nongen_level := !current_level
let end_def () =
let (cl, nl) = List.hd !saved_level in
saved_level := List.tl !saved_level;
current_level := cl; nongen_level := nl
let reset_global_level () =
global_level := !current_level + 1
let increase_global_level () =
let gl = !global_level in
global_level := !current_level;
gl
let restore_global_level gl =
global_level := gl
(**** Whether a path points to an object type (with hidden row variable) ****)
let is_object_type path =
let name =
match path with Path.Pident id -> Ident.name id
| Path.Pdot(_, s,_) -> s
| Path.Papply _ -> assert false
in name.[0] = '#'
(**** Abbreviations without parameters ****)
(* Shall reset after generalizing *)
let simple_abbrevs = ref Mnil
let proper_abbrevs path tl abbrev =
if !Clflags.principal || tl <> [] || is_object_type path then abbrev
else simple_abbrevs
(**** Some type creators ****)
(* Re-export generic type creators *)
let newty2 = Btype.newty2
let newty desc = newty2 !current_level desc
let new_global_ty desc = newty2 !global_level desc
let newvar () = newty2 !current_level Tvar
let newvar2 level = newty2 level Tvar
let new_global_var () = newty2 !global_level Tvar
let newobj fields = newty (Tobject (fields, ref None))
let newconstr path tyl = newty (Tconstr (path, tyl, ref Mnil))
let none = newty (Ttuple []) (* Clearly ill-formed type *)
(**** Representative of a type ****)
(* Re-export repr *)
let repr = repr
(**** Type maps ****)
module TypePairs =
Hashtbl.Make (struct
type t = type_expr * type_expr
let equal (t1, t1') (t2, t2') = (t1 == t2) && (t1' == t2')
let hash (t, t') = t.id + 93 * t'.id
end)
(**********************************************)
(* Miscellaneous operations on object types *)
(**********************************************)
(* Note:
We need to maintain some invariants:
* cty_self must be a Tobject
* ...
*)
(**** Object field manipulation. ****)
let dummy_method = "*dummy method*"
let object_fields ty =
match (repr ty).desc with
Tobject (fields, _) -> fields
| _ -> assert false
let flatten_fields ty =
let rec flatten l ty =
let ty = repr ty in
match ty.desc with
Tfield(s, k, ty1, ty2) ->
flatten ((s, k, ty1)::l) ty2
| _ ->
(l, ty)
in
let (l, r) = flatten [] ty in
(Sort.list (fun (n, _, _) (n', _, _) -> n < n') l, r)
let build_fields level =
List.fold_right
(fun (s, k, ty1) ty2 -> newty2 level (Tfield(s, k, ty1, ty2)))
let associate_fields fields1 fields2 =
let rec associate p s s' =
function
(l, []) ->
(List.rev p, (List.rev s) @ l, List.rev s')
| ([], l') ->
(List.rev p, List.rev s, (List.rev s') @ l')
| ((n, k, t)::r, (n', k', t')::r') when n = n' ->
associate ((n, k, t, k', t')::p) s s' (r, r')
| ((n, k, t)::r, ((n', k', t')::_ as l')) when n < n' ->
associate p ((n, k, t)::s) s' (r, l')
| (((n, k, t)::r as l), (n', k', t')::r') (* when n > n' *) ->
associate p s ((n', k', t')::s') (l, r')
in
associate [] [] [] (fields1, fields2)
(**** Check whether an object is open ****)
(* +++ Il faudra penser a eventuellement expanser l'abreviation *)
let rec object_row ty =
let ty = repr ty in
match ty.desc with
Tobject (t, _) -> object_row t
| Tfield(_, _, _, t) -> object_row t
| _ -> ty
let opened_object ty =
match (object_row ty).desc with
| Tvar -> true
| Tunivar -> true
| Tconstr _ -> true
| _ -> false
(**** Close an object ****)
let close_object ty =
let rec close ty =
let ty = repr ty in
match ty.desc with
Tvar ->
link_type ty (newty2 ty.level Tnil)
| Tfield(_, _, _, ty') -> close ty'
| _ -> assert false
in
match (repr ty).desc with
Tobject (ty, _) -> close ty
| _ -> assert false
(**** Row variable of an object type ****)
let row_variable ty =
let rec find ty =
let ty = repr ty in
match ty.desc with
Tfield (_, _, _, ty) -> find ty
| Tvar -> ty
| _ -> assert false
in
match (repr ty).desc with
Tobject (fi, _) -> find fi
| _ -> assert false
(**** Object name manipulation ****)
(* +++ Bientot obsolete *)
let set_object_name id rv params ty =
match (repr ty).desc with
Tobject (fi, nm) ->
set_name nm (Some (Path.Pident id, rv::params))
| _ ->
assert false
let remove_object_name ty =
match (repr ty).desc with
Tobject (_, nm) -> set_name nm None
| Tconstr (_, _, _) -> ()
| _ -> fatal_error "Ctype.remove_object_name"
(**** Hiding of private methods ****)
let hide_private_methods ty =
match (repr ty).desc with
Tobject (fi, nm) ->
nm := None;
let (fl, _) = flatten_fields fi in
List.iter
(function (_, k, _) ->
match field_kind_repr k with
Fvar r -> set_kind r Fabsent
| _ -> ())
fl
| _ ->
assert false
(*******************************)
(* Operations on class types *)
(*******************************)
let rec signature_of_class_type =
function
Tcty_constr (_, _, cty) -> signature_of_class_type cty
| Tcty_signature sign -> sign
| Tcty_fun (_, ty, cty) -> signature_of_class_type cty
let self_type cty =
repr (signature_of_class_type cty).cty_self
let rec class_type_arity =
function
Tcty_constr (_, _, cty) -> class_type_arity cty
| Tcty_signature _ -> 0
| Tcty_fun (_, _, cty) -> 1 + class_type_arity cty
(*******************************************)
(* Miscellaneous operations on row types *)
(*******************************************)
let sort_row_fields = Sort.list (fun (p,_) (q,_) -> p < q)
let rec merge_rf r1 r2 pairs fi1 fi2 =
match fi1, fi2 with
(l1,f1 as p1)::fi1', (l2,f2 as p2)::fi2' ->
if l1 = l2 then merge_rf r1 r2 ((l1,f1,f2)::pairs) fi1' fi2' else
if l1 < l2 then merge_rf (p1::r1) r2 pairs fi1' fi2 else
merge_rf r1 (p2::r2) pairs fi1 fi2'
| [], _ -> (List.rev r1, List.rev_append r2 fi2, pairs)
| _, [] -> (List.rev_append r1 fi1, List.rev r2, pairs)
let merge_row_fields fi1 fi2 =
match fi1, fi2 with
[], _ | _, [] -> (fi1, fi2, [])
| [p1], _ when not (List.mem_assoc (fst p1) fi2) -> (fi1, fi2, [])
| _, [p2] when not (List.mem_assoc (fst p2) fi1) -> (fi1, fi2, [])
| _ -> merge_rf [] [] [] (sort_row_fields fi1) (sort_row_fields fi2)
let rec filter_row_fields erase = function
[] -> []
| (l,f as p)::fi ->
let fi = filter_row_fields erase fi in
match row_field_repr f with
Rabsent -> fi
| Reither(_,_,false,e) when erase -> set_row_field e Rabsent; fi
| _ -> p :: fi
(**************************************)
(* Check genericity of type schemes *)
(**************************************)
exception Non_closed
let rec closed_schema_rec ty =
let ty = repr ty in
if ty.level >= lowest_level then begin
let level = ty.level in
ty.level <- pivot_level - level;
match ty.desc with
Tvar when level <> generic_level ->
raise Non_closed
| Tfield(_, kind, t1, t2) ->
if field_kind_repr kind = Fpresent then
closed_schema_rec t1;
closed_schema_rec t2
| Tvariant row ->
let row = row_repr row in
iter_row closed_schema_rec row;
if not (static_row row) then closed_schema_rec row.row_more
| _ ->
iter_type_expr closed_schema_rec ty
end
(* Return whether all variables of type [ty] are generic. *)
let closed_schema ty =
try
closed_schema_rec ty;
unmark_type ty;
true
with Non_closed ->
unmark_type ty;
false
exception Non_closed of type_expr * bool
let free_variables = ref []
let really_closed = ref None
let rec free_vars_rec real ty =
let ty = repr ty in
if ty.level >= lowest_level then begin
ty.level <- pivot_level - ty.level;
begin match ty.desc, !really_closed with
Tvar, _ ->
free_variables := (ty, real) :: !free_variables
| Tconstr (path, tl, _), Some env ->
begin try
let (_, body) = Env.find_type_expansion path env in
if (repr body).level <> generic_level then
free_variables := (ty, real) :: !free_variables
with Not_found -> ()
end;
List.iter (free_vars_rec true) tl
(* Do not count "virtual" free variables
| Tobject(ty, {contents = Some (_, p)}) ->
free_vars_rec false ty; List.iter (free_vars_rec true) p
*)
| Tobject (ty, _), _ ->
free_vars_rec false ty
| Tfield (_, _, ty1, ty2), _ ->
free_vars_rec true ty1; free_vars_rec false ty2
| Tvariant row, _ ->
let row = row_repr row in
iter_row (free_vars_rec true) row;
if not (static_row row) then free_vars_rec false row.row_more
| _ ->
iter_type_expr (free_vars_rec true) ty
end;
end
let free_vars ?env ty =
free_variables := [];
really_closed := env;
free_vars_rec true ty;
let res = !free_variables in
free_variables := [];
really_closed := None;
res
let free_variables ?env ty =
let tl = List.map fst (free_vars ?env ty) in
unmark_type ty;
tl
let rec closed_type ty =
match free_vars ty with
[] -> ()
| (v, real) :: _ -> raise (Non_closed (v, real))
let closed_parameterized_type params ty =
List.iter mark_type params;
let ok =
try closed_type ty; true with Non_closed _ -> false in
List.iter unmark_type params;
unmark_type ty;
ok
let closed_type_decl decl =
try
List.iter mark_type decl.type_params;
begin match decl.type_kind with
Type_abstract ->
()
| Type_variant v ->
List.iter (fun (_, tyl) -> List.iter closed_type tyl) v
| Type_record(r, rep) ->
List.iter (fun (_, _, ty) -> closed_type ty) r
end;
begin match decl.type_manifest with
None -> ()
| Some ty -> closed_type ty
end;
unmark_type_decl decl;
None
with Non_closed (ty, _) ->
unmark_type_decl decl;
Some ty
type closed_class_failure =
CC_Method of type_expr * bool * string * type_expr
| CC_Value of type_expr * bool * string * type_expr
exception Failure of closed_class_failure
let closed_class params sign =
let ty = object_fields (repr sign.cty_self) in
let (fields, rest) = flatten_fields ty in
List.iter mark_type params;
mark_type rest;
List.iter
(fun (lab, _, ty) -> if lab = dummy_method then mark_type ty)
fields;
try
mark_type_node (repr sign.cty_self);
List.iter
(fun (lab, kind, ty) ->
if field_kind_repr kind = Fpresent then
try closed_type ty with Non_closed (ty0, real) ->
raise (Failure (CC_Method (ty0, real, lab, ty))))
fields;
mark_type_params (repr sign.cty_self);
List.iter unmark_type params;
unmark_class_signature sign;
None
with Failure reason ->
mark_type_params (repr sign.cty_self);
List.iter unmark_type params;
unmark_class_signature sign;
Some reason
(**********************)
(* Type duplication *)
(**********************)
(* Duplicate a type, preserving only type variables *)
let duplicate_type ty =
Subst.type_expr Subst.identity ty
(* Same, for class types *)
let duplicate_class_type ty =
Subst.class_type Subst.identity ty
(*****************************)
(* Type level manipulation *)
(*****************************)
(*
It would be a bit more efficient to remove abbreviation expansions
rather than generalizing them: these expansions will usually not be
used anymore. However, this is not possible in the general case, as
[expand_abbrev] (via [subst]) requires these expansions to be
preserved. Does it worth duplicating this code ?
*)
let rec iter_generalize tyl ty =
let ty = repr ty in
if (ty.level > !current_level) && (ty.level <> generic_level) then begin
set_level ty generic_level;
begin match ty.desc with
Tconstr (_, _, abbrev) ->
iter_abbrev (iter_generalize tyl) !abbrev
| _ -> ()
end;
iter_type_expr (iter_generalize tyl) ty
end else
tyl := ty :: !tyl
let iter_generalize tyl ty =
simple_abbrevs := Mnil;
iter_generalize tyl ty
let generalize ty =
iter_generalize (ref []) ty
(* Efficient repeated generalisation of the same type *)
let iterative_generalization min_level tyl =
let tyl' = ref [] in
List.iter (iter_generalize tyl') tyl;
List.fold_right (fun ty l -> if ty.level <= min_level then l else ty::l)
!tyl' []
(* Generalize the structure and lower the variables *)
let rec generalize_structure var_level ty =
let ty = repr ty in
if ty.level <> generic_level then begin
if ty.desc = Tvar && ty.level > var_level then
set_level ty var_level
else if ty.level > !current_level then begin
set_level ty generic_level;
begin match ty.desc with
Tconstr (_, _, abbrev) -> abbrev := Mnil
| _ -> ()
end;
iter_type_expr (generalize_structure var_level) ty
end
end
let generalize_structure var_level ty =
simple_abbrevs := Mnil;
generalize_structure var_level ty
(* let generalize_expansive ty = generalize_structure !nongen_level ty *)
let generalize_global ty = generalize_structure !global_level ty
let generalize_structure ty = generalize_structure !current_level ty
(* Generalize the spine of a function, if the level >= !current_level *)
let rec generalize_spine ty =
let ty = repr ty in
if ty.level < !current_level || ty.level = generic_level then () else
match ty.desc with
Tarrow (_, _, ty', _) | Tpoly (ty', _) ->
set_level ty generic_level;
generalize_spine ty'
| _ -> ()
let forward_try_expand_once = (* Forward declaration *)
ref (fun env ty -> raise Cannot_expand)
(*
Lower the levels of a type (assume [level] is not
[generic_level]).
*)
(*
The level of a type constructor must be greater than its binding
time. That way, a type constructor cannot escape the scope of its
definition, as would be the case in
let x = ref []
module M = struct type t let _ = (x : t list ref) end
(without this constraint, the type system would actually be unsound.)
*)
let rec update_level env level ty =
let ty = repr ty in
if ty.level > level then begin
begin match ty.desc with
Tconstr(p, tl, abbrev) when level < Path.binding_time p ->
(* Try first to replace an abbreviation by its expansion. *)
begin try
link_type ty (!forward_try_expand_once env ty);
update_level env level ty
with Cannot_expand ->
(* +++ Levels should be restored... *)
raise (Unify [(ty, newvar2 level)])
end
| Tpackage (p, _, _) when level < Path.binding_time p ->
raise (Unify [(ty, newvar2 level)])
| Tobject(_, ({contents=Some(p, tl)} as nm))
when level < Path.binding_time p ->
set_name nm None;
update_level env level ty
| Tvariant row ->
let row = row_repr row in
begin match row.row_name with
| Some (p, tl) when level < Path.binding_time p ->
log_type ty;
ty.desc <- Tvariant {row with row_name = None}
| _ -> ()
end;
set_level ty level;
iter_type_expr (update_level env level) ty
| Tfield(lab, _, _, _) when lab = dummy_method ->
raise (Unify [(ty, newvar2 level)])
| _ ->
set_level ty level;
(* XXX what about abbreviations in Tconstr ? *)
iter_type_expr (update_level env level) ty
end
end
(* Generalize and lower levels of contravariant branches simultaneously *)
let rec generalize_expansive env var_level ty =
let ty = repr ty in
if ty.level <> generic_level then begin
if ty.level > var_level then begin
set_level ty generic_level;
match ty.desc with
Tconstr (path, tyl, abbrev) ->
let variance =
try (Env.find_type path env).type_variance
with Not_found -> List.map (fun _ -> (true,true,true)) tyl in
abbrev := Mnil;
List.iter2
(fun (co,cn,ct) t ->
if ct then update_level env var_level t
else generalize_expansive env var_level t)
variance tyl
| Tpackage (_, _, tyl) ->
List.iter (update_level env var_level) tyl
| Tarrow (_, t1, t2, _) ->
update_level env var_level t1;
generalize_expansive env var_level t2
| _ ->
iter_type_expr (generalize_expansive env var_level) ty
end
end
let generalize_expansive env ty =
simple_abbrevs := Mnil;
try
generalize_expansive env !nongen_level ty
with Unify [_, ty'] ->
raise (Unify [ty, ty'])
(* Correct the levels of type [ty]. *)
let correct_levels ty =
duplicate_type ty
(* Only generalize the type ty0 in ty *)
let limited_generalize ty0 ty =
let ty0 = repr ty0 in
let graph = Hashtbl.create 17 in
let idx = ref lowest_level in
let roots = ref [] in
let rec inverse pty ty =
let ty = repr ty in
if (ty.level > !current_level) || (ty.level = generic_level) then begin
decr idx;
Hashtbl.add graph !idx (ty, ref pty);
if (ty.level = generic_level) || (ty == ty0) then
roots := ty :: !roots;
set_level ty !idx;
iter_type_expr (inverse [ty]) ty
end else if ty.level < lowest_level then begin
let (_, parents) = Hashtbl.find graph ty.level in
parents := pty @ !parents
end
and generalize_parents ty =
let idx = ty.level in
if idx <> generic_level then begin
set_level ty generic_level;
List.iter generalize_parents !(snd (Hashtbl.find graph idx));
(* Special case for rows: must generalize the row variable *)
match ty.desc with
Tvariant row ->
let more = row_more row in
let lv = more.level in
if (lv < lowest_level || lv > !current_level)
&& lv <> generic_level then set_level more generic_level
| _ -> ()
end
in
inverse [] ty;
if ty0.level < lowest_level then
iter_type_expr (inverse []) ty0;
List.iter generalize_parents !roots;
Hashtbl.iter
(fun _ (ty, _) ->
if ty.level <> generic_level then set_level ty !current_level)
graph
(*******************)
(* Instantiation *)
(*******************)
let rec find_repr p1 =
function
Mnil ->
None
| Mcons (Public, p2, ty, _, _) when Path.same p1 p2 ->
Some ty
| Mcons (_, _, _, _, rem) ->
find_repr p1 rem
| Mlink {contents = rem} ->
find_repr p1 rem
(*
Generic nodes are duplicated, while non-generic nodes are left
as-is.
During instantiation, the description of a generic node is first
replaced by a link to a stub ([Tsubst (newvar ())]). Once the
copy is made, it replaces the stub.
After instantiation, the description of generic node, which was
stored by [save_desc], must be put back, using [cleanup_types].
*)
let abbreviations = ref (ref Mnil)
(* Abbreviation memorized. *)
let rec copy ty =
let ty = repr ty in
match ty.desc with
Tsubst ty -> ty
| _ ->
if ty.level <> generic_level then ty else
let desc = ty.desc in
save_desc ty desc;
let t = newvar() in (* Stub *)
ty.desc <- Tsubst t;
t.desc <-
begin match desc with
| Tconstr (p, tl, _) ->
let abbrevs = proper_abbrevs p tl !abbreviations in
begin match find_repr p !abbrevs with
Some ty when repr ty != t -> (* XXX Commentaire... *)
Tlink ty
| _ ->
(*
One must allocate a new reference, so that abbrevia-
tions belonging to different branches of a type are
independent.
Moreover, a reference containing a [Mcons] must be
shared, so that the memorized expansion of an abbrevi-
ation can be released by changing the content of just
one reference.
*)
Tconstr (p, List.map copy tl,
ref (match !(!abbreviations) with
Mcons _ -> Mlink !abbreviations
| abbrev -> abbrev))
end
| Tvariant row0 ->
let row = row_repr row0 in
let more = repr row.row_more in
(* We must substitute in a subtle way *)
(* Tsubst takes a tuple containing the row var and the variant *)
begin match more.desc with
Tsubst {desc = Ttuple [_;ty2]} ->
(* This variant type has been already copied *)
ty.desc <- Tsubst ty2; (* avoid Tlink in the new type *)
Tlink ty2
| _ ->
(* If the row variable is not generic, we must keep it *)
let keep = more.level <> generic_level in
let more' =
match more.desc with
Tsubst ty -> ty
| Tconstr _ ->
if keep then save_desc more more.desc;
copy more
| Tvar | Tunivar ->
save_desc more more.desc;
if keep then more else newty more.desc
| _ -> assert false
in
(* Register new type first for recursion *)
more.desc <- Tsubst(newgenty(Ttuple[more';t]));
(* Return a new copy *)
Tvariant (copy_row copy true row keep more')
end
| Tfield (p, k, ty1, ty2) ->
begin match field_kind_repr k with
Fabsent -> Tlink (copy ty2)
| Fpresent -> copy_type_desc copy desc
| Fvar r ->
dup_kind r;
copy_type_desc copy desc
end
| _ -> copy_type_desc copy desc
end;
t
(**** Variants of instantiations ****)
let instance sch =
let ty = copy sch in
cleanup_types ();
ty
let instance_list schl =
let tyl = List.map copy schl in
cleanup_types ();
tyl
let instance_constructor cstr =
let ty_res = copy cstr.cstr_res in
let ty_args = List.map copy cstr.cstr_args in
cleanup_types ();
(ty_args, ty_res)
let instance_parameterized_type sch_args sch =
let ty_args = List.map copy sch_args in
let ty = copy sch in
cleanup_types ();
(ty_args, ty)
let instance_parameterized_type_2 sch_args sch_lst sch =
let ty_args = List.map copy sch_args in
let ty_lst = List.map copy sch_lst in
let ty = copy sch in
cleanup_types ();
(ty_args, ty_lst, ty)
let instance_declaration decl =
let decl =
{decl with type_params = List.map copy decl.type_params;
type_manifest = may_map copy decl.type_manifest;
type_kind = match decl.type_kind with
| Type_abstract -> Type_abstract
| Type_variant cl ->
Type_variant (List.map (fun (s,tl) -> (s, List.map copy tl)) cl)
| Type_record (fl, rr) ->
Type_record (List.map (fun (s,m,ty) -> (s, m, copy ty)) fl, rr)}
in
cleanup_types ();
decl
let instance_class params cty =
let rec copy_class_type =
function
Tcty_constr (path, tyl, cty) ->
Tcty_constr (path, List.map copy tyl, copy_class_type cty)
| Tcty_signature sign ->
Tcty_signature
{cty_self = copy sign.cty_self;
cty_vars =
Vars.map (function (m, v, ty) -> (m, v, copy ty)) sign.cty_vars;
cty_concr = sign.cty_concr;
cty_inher =
List.map (fun (p,tl) -> (p, List.map copy tl)) sign.cty_inher}
| Tcty_fun (l, ty, cty) ->
Tcty_fun (l, copy ty, copy_class_type cty)
in
let params' = List.map copy params in
let cty' = copy_class_type cty in
cleanup_types ();
(params', cty')
(**** Instanciation for types with free universal variables ****)
module TypeHash = Hashtbl.Make(TypeOps)
module TypeSet = Set.Make(TypeOps)
type inv_type_expr =
{ inv_type : type_expr;
mutable inv_parents : inv_type_expr list }
let rec inv_type hash pty ty =
let ty = repr ty in
try
let inv = TypeHash.find hash ty in
inv.inv_parents <- pty @ inv.inv_parents
with Not_found ->
let inv = { inv_type = ty; inv_parents = pty } in
TypeHash.add hash ty inv;
iter_type_expr (inv_type hash [inv]) ty
let compute_univars ty =
let inverted = TypeHash.create 17 in
inv_type inverted [] ty;
let node_univars = TypeHash.create 17 in
let rec add_univar univ inv =
match inv.inv_type.desc with
Tpoly (ty, tl) when List.memq univ (List.map repr tl) -> ()
| _ ->
try
let univs = TypeHash.find node_univars inv.inv_type in
if not (TypeSet.mem univ !univs) then begin
univs := TypeSet.add univ !univs;
List.iter (add_univar univ) inv.inv_parents
end
with Not_found ->
TypeHash.add node_univars inv.inv_type (ref(TypeSet.singleton univ));
List.iter (add_univar univ) inv.inv_parents
in
TypeHash.iter (fun ty inv -> if ty.desc = Tunivar then add_univar ty inv)
inverted;
fun ty ->
try !(TypeHash.find node_univars ty) with Not_found -> TypeSet.empty
let rec diff_list l1 l2 =
if l1 == l2 then [] else
match l1 with [] -> invalid_arg "Ctype.diff_list"
| a :: l1 -> a :: diff_list l1 l2
let conflicts free bound =
let bound = List.map repr bound in
TypeSet.exists (fun t -> List.memq (repr t) bound) free
let delayed_copy = ref []
(* copying to do later *)
(* Copy without sharing until there are no free univars left *)
(* all free univars must be included in [visited] *)
let rec copy_sep fixed free bound visited ty =
let ty = repr ty in
let univars = free ty in
if TypeSet.is_empty univars then
if ty.level <> generic_level then ty else
let t = newvar () in
delayed_copy :=
lazy (t.desc <- Tlink (copy ty))
:: !delayed_copy;
t
else try
let t, bound_t = List.assq ty visited in
let dl = if ty.desc = Tunivar then [] else diff_list bound bound_t in
if dl <> [] && conflicts univars dl then raise Not_found;
t
with Not_found -> begin
let t = newvar() in (* Stub *)
let visited =
match ty.desc with
Tarrow _ | Ttuple _ | Tvariant _ | Tconstr _ | Tobject _ | Tpackage _ ->
(ty,(t,bound)) :: visited
| _ -> visited in
let copy_rec = copy_sep fixed free bound visited in
t.desc <-
begin match ty.desc with
| Tvariant row0 ->
let row = row_repr row0 in
let more = repr row.row_more in
(* We shall really check the level on the row variable *)
let keep = more.desc = Tvar && more.level <> generic_level in
let more' = copy_rec more in
let fixed' = fixed && (repr more').desc = Tvar in
let row = copy_row copy_rec fixed' row keep more' in
Tvariant row
| Tpoly (t1, tl) ->
let tl = List.map repr tl in
let tl' = List.map (fun t -> newty Tunivar) tl in
let bound = tl @ bound in
let visited =
List.map2 (fun ty t -> ty,(t,bound)) tl tl' @ visited in
Tpoly (copy_sep fixed free bound visited t1, tl')
| _ -> copy_type_desc copy_rec ty.desc
end;
t
end
let instance_poly fixed univars sch =
let vars = List.map (fun _ -> newvar ()) univars in
let pairs = List.map2 (fun u v -> repr u, (v, [])) univars vars in
delayed_copy := [];
let ty = copy_sep fixed (compute_univars sch) [] pairs sch in
List.iter Lazy.force !delayed_copy;
delayed_copy := [];
cleanup_types ();
vars, ty
let instance_label fixed lbl =
let ty_res = copy lbl.lbl_res in
let vars, ty_arg =
match repr lbl.lbl_arg with
{desc = Tpoly (ty, tl)} ->
instance_poly fixed tl ty
| ty ->
[], copy lbl.lbl_arg
in
cleanup_types ();
(vars, ty_arg, ty_res)
(**** Instantiation with parameter substitution ****)
let unify' = (* Forward declaration *)
ref (fun env ty1 ty2 -> raise (Unify []))
let rec subst env level priv abbrev ty params args body =
if List.length params <> List.length args then raise (Unify []);
let old_level = !current_level in
current_level := level;
try
let body0 = newvar () in (* Stub *)
begin match ty with
None -> ()
| Some ({desc = Tconstr (path, tl, _)} as ty) ->
let abbrev = proper_abbrevs path tl abbrev in
memorize_abbrev abbrev priv path ty body0
| _ ->
assert false
end;
abbreviations := abbrev;
let (params', body') = instance_parameterized_type params body in
abbreviations := ref Mnil;
!unify' env body0 body';
List.iter2 (!unify' env) params' args;
current_level := old_level;
body'
with Unify _ as exn ->
current_level := old_level;
raise exn
(*
Only the shape of the type matters, not whether is is generic or
not. [generic_level] might be somewhat slower, but it ensures
invariants on types are enforced (decreasing levels.), and we don't
care about efficiency here.
*)
let apply env params body args =
try
subst env generic_level Public (ref Mnil) None params args body
with
Unify _ -> raise Cannot_apply
(****************************)
(* Abbreviation expansion *)
(****************************)
(*
If the environnement has changed, memorized expansions might not
be correct anymore, and so we flush the cache. This is safe but
quite pessimistic: it would be enough to flush the cache when a
type or module definition is overridden in the environnement.
*)
let previous_env = ref Env.empty
let string_of_kind = function Public -> "public" | Private -> "private"
let check_abbrev_env env =
if env != !previous_env then begin
(* prerr_endline "cleanup expansion cache"; *)
cleanup_abbrev ();
previous_env := env
end
(* Expand an abbreviation. The expansion is memorized. *)
(*
Assume the level is greater than the path binding time of the
expanded abbreviation.
*)
(*
An abbreviation expansion will fail in either of these cases:
1. The type constructor does not correspond to a manifest type.
2. The type constructor is defined in an external file, and this
file is not in the path (missing -I options).
3. The type constructor is not in the "local" environment. This can
happens when a non-generic type variable has been instantiated
afterwards to the not yet defined type constructor. (Actually,
this cannot happen at the moment due to the strong constraints
between type levels and constructor binding time.)
4. The expansion requires the expansion of another abbreviation,
and this other expansion fails.
*)
let expand_abbrev_gen kind find_type_expansion env ty =
check_abbrev_env env;
match ty with
{desc = Tconstr (path, args, abbrev); level = level} ->
let lookup_abbrev = proper_abbrevs path args abbrev in
begin match find_expans kind path !lookup_abbrev with
Some ty ->
(* prerr_endline
("found a "^string_of_kind kind^" expansion for "^Path.name path);*)
if level <> generic_level then
begin try
update_level env level ty
with Unify _ ->
(* XXX This should not happen.
However, levels are not correctly restored after a
typing error *)
()
end;
ty
| None ->
let (params, body) =
try find_type_expansion path env with Not_found ->
raise Cannot_expand
in
(* prerr_endline
("add a "^string_of_kind kind^" expansion for "^Path.name path);*)
let ty' = subst env level kind abbrev (Some ty) params args body in
(* Hack to name the variant type *)
begin match repr ty' with
{desc=Tvariant row} as ty when static_row row ->
ty.desc <- Tvariant { row with row_name = Some (path, args) }
| _ -> ()
end;
ty'
end
| _ ->
assert false
let expand_abbrev = expand_abbrev_gen Public Env.find_type_expansion
let safe_abbrev env ty =
let snap = Btype.snapshot () in
try ignore (expand_abbrev env ty); true
with Cannot_expand | Unify _ ->
Btype.backtrack snap;
false
let try_expand_once env ty =
let ty = repr ty in
match ty.desc with
Tconstr _ -> repr (expand_abbrev env ty)
| _ -> raise Cannot_expand
let _ = forward_try_expand_once := try_expand_once
(* Fully expand the head of a type.
Raise Cannot_expand if the type cannot be expanded.
May raise Unify, if a recursion was hidden in the type. *)
let rec try_expand_head env ty =
let ty' = try_expand_once env ty in
begin try
try_expand_head env ty'
with Cannot_expand ->
ty'
end
(* Expand once the head of a type *)
let expand_head_once env ty =
try expand_abbrev env (repr ty) with Cannot_expand -> assert false
(* Fully expand the head of a type. *)
let expand_head_unif env ty =
try try_expand_head env ty with Cannot_expand -> repr ty
let expand_head env ty =
let snap = Btype.snapshot () in
try try_expand_head env ty
with Cannot_expand | Unify _ -> (* expand_head shall never fail *)
Btype.backtrack snap;
repr ty
(* Implementing function [expand_head_opt], the compiler's own version of
[expand_head] used for type-based optimisations.
[expand_head_opt] uses [Env.find_type_expansion_opt] to access the
manifest type information of private abstract data types which is
normally hidden to the type-checker out of the implementation module of
the private abbreviation. *)
let expand_abbrev_opt = expand_abbrev_gen Private Env.find_type_expansion_opt
let try_expand_once_opt env ty =
let ty = repr ty in
match ty.desc with
Tconstr _ -> repr (expand_abbrev_opt env ty)
| _ -> raise Cannot_expand
let rec try_expand_head_opt env ty =
let ty' = try_expand_once_opt env ty in
begin try
try_expand_head_opt env ty'
with Cannot_expand ->
ty'
end
let expand_head_opt env ty =
let snap = Btype.snapshot () in
try try_expand_head_opt env ty
with Cannot_expand | Unify _ -> (* expand_head shall never fail *)
Btype.backtrack snap;
repr ty
(* Make sure that the type parameters of the type constructor [ty]
respect the type constraints *)
let enforce_constraints env ty =
match ty with
{desc = Tconstr (path, args, abbrev); level = level} ->
let decl = Env.find_type path env in
ignore
(subst env level Public (ref Mnil) None decl.type_params args
(newvar2 level))
| _ ->
assert false
(* Recursively expand the head of a type.
Also expand #-types. *)
let rec full_expand env ty =
let ty = repr (expand_head env ty) in
match ty.desc with
Tobject (fi, {contents = Some (_, v::_)}) when (repr v).desc = Tvar ->
newty2 ty.level (Tobject (fi, ref None))
| _ ->
ty
(*
Check whether the abbreviation expands to a well-defined type.
During the typing of a class, abbreviations for correspondings
types expand to non-generic types.
*)
let generic_abbrev env path =
try
let (_, body) = Env.find_type_expansion path env in
(repr body).level = generic_level
with
Not_found ->
false
(*****************)
(* Occur check *)
(*****************)
exception Occur
(* The marks are already used by [expand_abbrev]... *)
let visited = ref []
let rec non_recursive_abbrev env ty0 ty =
let ty = repr ty in
if ty == repr ty0 then raise Recursive_abbrev;
if not (List.memq ty !visited) then begin
visited := ty :: !visited;
match ty.desc with
Tconstr(p, args, abbrev) ->
begin try
non_recursive_abbrev env ty0 (try_expand_once_opt env ty)
with Cannot_expand ->
if !Clflags.recursive_types then () else
iter_type_expr (non_recursive_abbrev env ty0) ty
end
| Tobject _ | Tvariant _ ->
()
| _ ->
if !Clflags.recursive_types then () else
iter_type_expr (non_recursive_abbrev env ty0) ty
end
let correct_abbrev env path params ty =
check_abbrev_env env;
let ty0 = newgenvar () in
visited := [];
let abbrev = Mcons (Public, path, ty0, ty0, Mnil) in
simple_abbrevs := abbrev;
try
non_recursive_abbrev env ty0
(subst env generic_level Public (ref abbrev) None [] [] ty);
simple_abbrevs := Mnil;
visited := []
with exn ->
simple_abbrevs := Mnil;
visited := [];
raise exn
let rec occur_rec env visited ty0 ty =
if ty == ty0 then raise Occur;
match ty.desc with
Tconstr(p, tl, abbrev) ->
begin try
if List.memq ty visited || !Clflags.recursive_types then raise Occur;
iter_type_expr (occur_rec env (ty::visited) ty0) ty
with Occur -> try
let ty' = try_expand_head env ty in
(* Maybe we could simply make a recursive call here,
but it seems it could make the occur check loop
(see change in rev. 1.58) *)
if ty' == ty0 || List.memq ty' visited then raise Occur;
match ty'.desc with
Tobject _ | Tvariant _ -> ()
| _ ->
if not !Clflags.recursive_types then
iter_type_expr (occur_rec env (ty'::visited) ty0) ty'
with Cannot_expand ->
if not !Clflags.recursive_types then raise Occur
end
| Tobject _ | Tvariant _ ->
()
| _ ->
if not !Clflags.recursive_types then
iter_type_expr (occur_rec env visited ty0) ty
let type_changed = ref false (* trace possible changes to the studied type *)
let merge r b = if b then r := true
let occur env ty0 ty =
let old = !type_changed in
try
while type_changed := false; occur_rec env [] ty0 ty; !type_changed
do () (* prerr_endline "changed" *) done;
merge type_changed old
with exn ->
merge type_changed old;
raise (match exn with Occur -> Unify [] | _ -> exn)
(*****************************)
(* Polymorphic Unification *)
(*****************************)
(* Since we cannot duplicate universal variables, unification must
be done at meta-level, using bindings in univar_pairs *)
let rec unify_univar t1 t2 = function
(cl1, cl2) :: rem ->
let find_univ t cl =
try
let (_, r) = List.find (fun (t',_) -> t == repr t') cl in
Some r
with Not_found -> None
in
begin match find_univ t1 cl1, find_univ t2 cl2 with
Some {contents=Some t'2}, Some _ when t2 == repr t'2 ->
()
| Some({contents=None} as r1), Some({contents=None} as r2) ->
set_univar r1 t2; set_univar r2 t1
| None, None ->
unify_univar t1 t2 rem
| _ ->
raise (Unify [])
end
| [] -> raise (Unify [])
module TypeMap = Map.Make (TypeOps)
(* Test the occurence of free univars in a type *)
(* that's way too expansive. Must do some kind of cacheing *)
let occur_univar env ty =
let visited = ref TypeMap.empty in
let rec occur_rec bound ty =
let ty = repr ty in
if ty.level >= lowest_level &&
if TypeSet.is_empty bound then
(ty.level <- pivot_level - ty.level; true)
else try
let bound' = TypeMap.find ty !visited in
if TypeSet.exists (fun x -> not (TypeSet.mem x bound)) bound' then
(visited := TypeMap.add ty (TypeSet.inter bound bound') !visited;
true)
else false
with Not_found ->
visited := TypeMap.add ty bound !visited;
true
then
match ty.desc with
Tunivar ->
if not (TypeSet.mem ty bound) then raise (Unify [ty, newgenvar()])
| Tpoly (ty, tyl) ->
let bound = List.fold_right TypeSet.add (List.map repr tyl) bound in
occur_rec bound ty
| Tconstr (_, [], _) -> ()
| Tconstr (p, tl, _) ->
begin try
let td = Env.find_type p env in
List.iter2
(fun t (pos,neg,_) -> if pos || neg then occur_rec bound t)
tl td.type_variance
with Not_found ->
List.iter (occur_rec bound) tl
end
| _ -> iter_type_expr (occur_rec bound) ty
in
try
occur_rec TypeSet.empty ty; unmark_type ty
with exn ->
unmark_type ty; raise exn
(* Grouping univars by families according to their binders *)
let add_univars =
List.fold_left (fun s (t,_) -> TypeSet.add (repr t) s)
let get_univar_family univar_pairs univars =
if univars = [] then TypeSet.empty else
let rec insert s = function
cl1, (_::_ as cl2) ->
if List.exists (fun (t1,_) -> TypeSet.mem (repr t1) s) cl1 then
add_univars s cl2
else s
| _ -> s
in
let s = List.fold_right TypeSet.add univars TypeSet.empty in
List.fold_left insert s univar_pairs
(* Whether a family of univars escapes from a type *)
let univars_escape env univar_pairs vl ty =
let family = get_univar_family univar_pairs vl in
let visited = ref TypeSet.empty in
let rec occur t =
let t = repr t in
if TypeSet.mem t !visited then () else begin
visited := TypeSet.add t !visited;
match t.desc with
Tpoly (t, tl) ->
if List.exists (fun t -> TypeSet.mem (repr t) family) tl then ()
else occur t
| Tunivar ->
if TypeSet.mem t family then raise Occur
| Tconstr (_, [], _) -> ()
| Tconstr (p, tl, _) ->
begin try
let td = Env.find_type p env in
List.iter2 (fun t (pos,neg,_) -> if pos || neg then occur t)
tl td.type_variance
with Not_found ->
List.iter occur tl
end
| _ ->
iter_type_expr occur t
end
in
try occur ty; false with Occur -> true
(* Wrapper checking that no variable escapes and updating univar_pairs *)
let enter_poly env univar_pairs t1 tl1 t2 tl2 f =
let old_univars = !univar_pairs in
let known_univars =
List.fold_left (fun s (cl,_) -> add_univars s cl)
TypeSet.empty old_univars
in
let tl1 = List.map repr tl1 and tl2 = List.map repr tl2 in
if List.exists (fun t -> TypeSet.mem t known_univars) tl1 &&
univars_escape env old_univars tl1 (newty(Tpoly(t2,tl2)))
|| List.exists (fun t -> TypeSet.mem t known_univars) tl2 &&
univars_escape env old_univars tl2 (newty(Tpoly(t1,tl1)))
then raise (Unify []);
let cl1 = List.map (fun t -> t, ref None) tl1
and cl2 = List.map (fun t -> t, ref None) tl2 in
univar_pairs := (cl1,cl2) :: (cl2,cl1) :: old_univars;
try let res = f t1 t2 in univar_pairs := old_univars; res
with exn -> univar_pairs := old_univars; raise exn
let univar_pairs = ref []
(*****************)
(* Unification *)
(*****************)
let rec has_cached_expansion p abbrev =
match abbrev with
Mnil -> false
| Mcons(_, p', _, _, rem) -> Path.same p p' || has_cached_expansion p rem
| Mlink rem -> has_cached_expansion p !rem
(**** Transform error trace ****)
(* +++ Move it to some other place ? *)
let expand_trace env trace =
List.fold_right
(fun (t1, t2) rem ->
(repr t1, full_expand env t1)::(repr t2, full_expand env t2)::rem)
trace []
(* build a dummy variant type *)
let mkvariant fields closed =
newgenty
(Tvariant
{row_fields = fields; row_closed = closed; row_more = newvar();
row_bound = (); row_fixed = false; row_name = None })
(* force unification in Reither when one side has as non-conjunctive type *)
let rigid_variants = ref false
(**** Unification ****)
(* Return whether [t0] occurs in [ty]. Objects are also traversed. *)
let deep_occur t0 ty =
let rec occur_rec ty =
let ty = repr ty in
if ty.level >= lowest_level then begin
if ty == t0 then raise Occur;
ty.level <- pivot_level - ty.level;
iter_type_expr occur_rec ty
end
in
try
occur_rec ty; unmark_type ty; false
with Occur ->
unmark_type ty; true
(*
1. When unifying two non-abbreviated types, one type is made a link
to the other. When unifying an abbreviated type with a
non-abbreviated type, the non-abbreviated type is made a link to
the other one. When unifying to abbreviated types, these two
types are kept distincts, but they are made to (temporally)
expand to the same type.
2. Abbreviations with at least one parameter are systematically
expanded. The overhead does not seem to high, and that way
abbreviations where some parameters does not appear in the
expansion, such as ['a t = int], are correctly handled. In
particular, for this example, unifying ['a t] with ['b t] keeps
['a] and ['b] distincts. (Is it really important ?)
3. Unifying an abbreviation ['a t = 'a] with ['a] should not yield
['a t as 'a]. Indeed, the type variable would otherwise be lost.
This problem occurs for abbreviations expanding to a type
variable, but also to many other constrained abbreviations (for
instance, [(< x : 'a > -> unit) t = <x : 'a>]). The solution is
that, if an abbreviation is unified with some subpart of its
parameters, then the parameter actually does not get
abbreviated. It would be possible to check whether some
information is indeed lost, but it probably does not worth it.
*)
let rec unify env t1 t2 =
(* First step: special cases (optimizations) *)
if t1 == t2 then () else
let t1 = repr t1 in
let t2 = repr t2 in
if t1 == t2 then () else
try
type_changed := true;
match (t1.desc, t2.desc) with
(Tvar, Tconstr _) when deep_occur t1 t2 ->
unify2 env t1 t2
| (Tconstr _, Tvar) when deep_occur t2 t1 ->
unify2 env t1 t2
| (Tvar, _) ->
occur env t1 t2; occur_univar env t2;
update_level env t1.level t2;
link_type t1 t2
| (_, Tvar) ->
occur env t2 t1; occur_univar env t1;
update_level env t2.level t1;
link_type t2 t1
| (Tunivar, Tunivar) ->
unify_univar t1 t2 !univar_pairs;
update_level env t1.level t2;
link_type t1 t2
| (Tconstr (p1, [], a1), Tconstr (p2, [], a2))
when Path.same p1 p2
(* This optimization assumes that t1 does not expand to t2
(and conversely), so we fall back to the general case
when any of the types has a cached expansion. *)
&& not (has_cached_expansion p1 !a1
|| has_cached_expansion p2 !a2) ->
update_level env t1.level t2;
link_type t1 t2
| _ ->
unify2 env t1 t2
with Unify trace ->
raise (Unify ((t1, t2)::trace))
and unify2 env t1 t2 =
(* Second step: expansion of abbreviations *)
let rec expand_both t1'' t2'' =
let t1' = expand_head_unif env t1 in
let t2' = expand_head_unif env t2 in
(* Expansion may have changed the representative of the types... *)
if t1' == t1'' && t2' == t2'' then (t1',t2') else
expand_both t1' t2'
in
let t1', t2' = expand_both t1 t2 in
if t1' == t2' then () else
let t1 = repr t1 and t2 = repr t2 in
if (t1 == t1') || (t2 != t2') then
unify3 env t1 t1' t2 t2'
else
try unify3 env t2 t2' t1 t1' with Unify trace ->
raise (Unify (List.map (fun (x, y) -> (y, x)) trace))
and unify3 env t1 t1' t2 t2' =
(* Third step: truly unification *)
(* Assumes either [t1 == t1'] or [t2 != t2'] *)
let d1 = t1'.desc and d2 = t2'.desc in
let create_recursion = (t2 != t2') && (deep_occur t1' t2) in
occur env t1' t2;
update_level env t1'.level t2;
link_type t1' t2;
try
begin match (d1, d2) with
(Tvar, _) ->
occur_univar env t2
| (_, Tvar) ->
let td1 = newgenty d1 in
occur env t2' td1;
occur_univar env td1;
if t1 == t1' then begin
(* The variable must be instantiated... *)
let ty = newty2 t1'.level d1 in
update_level env t2'.level ty;
link_type t2' ty
end else begin
log_type t1';
t1'.desc <- d1;
update_level env t2'.level t1;
link_type t2' t1
end
| (Tarrow (l1, t1, u1, c1), Tarrow (l2, t2, u2, c2)) when l1 = l2
|| !Clflags.classic && not (is_optional l1 || is_optional l2) ->
unify env t1 t2; unify env u1 u2;
begin match commu_repr c1, commu_repr c2 with
Clink r, c2 -> set_commu r c2
| c1, Clink r -> set_commu r c1
| _ -> ()
end
| (Ttuple tl1, Ttuple tl2) ->
unify_list env tl1 tl2
| (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 ->
unify_list env tl1 tl2
| (Tobject (fi1, nm1), Tobject (fi2, _)) ->
unify_fields env fi1 fi2;
(* Type [t2'] may have been instantiated by [unify_fields] *)
(* XXX One should do some kind of unification... *)
begin match (repr t2').desc with
Tobject (_, {contents = Some (_, va::_)})
when let va = repr va in List.mem va.desc [Tvar; Tunivar; Tnil] ->
()
| Tobject (_, nm2) ->
set_name nm2 !nm1
| _ ->
()
end
| (Tvariant row1, Tvariant row2) ->
unify_row env row1 row2
| (Tfield _, Tfield _) -> (* Actually unused *)
unify_fields env t1' t2'
| (Tfield(f,kind,_,rem), Tnil) | (Tnil, Tfield(f,kind,_,rem)) ->
begin match field_kind_repr kind with
Fvar r when f <> dummy_method -> set_kind r Fabsent
| _ -> raise (Unify [])
end
| (Tnil, Tnil) ->
()
| (Tpoly (t1, []), Tpoly (t2, [])) ->
unify env t1 t2
| (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
enter_poly env univar_pairs t1 tl1 t2 tl2 (unify env)
| (Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2)) when Path.same p1 p2 && n1 = n2 ->
unify_list env tl1 tl2
| (_, _) ->
raise (Unify [])
end;
(* XXX Commentaires + changer "create_recursion" *)
if create_recursion then begin
match t2.desc with
Tconstr (p, tl, abbrev) ->
forget_abbrev abbrev p;
let t2'' = expand_head_unif env t2 in
if not (closed_parameterized_type tl t2'') then
link_type (repr t2) (repr t2')
| _ ->
() (* t2 has already been expanded by update_level *)
end
(*
(*
Can only be done afterwards, once the row variable has
(possibly) been instantiated.
*)
if t1 != t1' (* && t2 != t2' *) then begin
match (t1.desc, t2.desc) with
(Tconstr (p, ty::_, _), _)
when ((repr ty).desc <> Tvar)
&& weak_abbrev p
&& not (deep_occur t1 t2) ->
update_level env t1.level t2;
link_type t1 t2
| (_, Tconstr (p, ty::_, _))
when ((repr ty).desc <> Tvar)
&& weak_abbrev p
&& not (deep_occur t2 t1) ->
update_level env t2.level t1;
link_type t2 t1;
link_type t1' t2'
| _ ->
()
end
*)
with Unify trace ->
t1'.desc <- d1;
raise (Unify trace)
and unify_list env tl1 tl2 =
if List.length tl1 <> List.length tl2 then
raise (Unify []);
List.iter2 (unify env) tl1 tl2
and unify_fields env ty1 ty2 = (* Optimization *)
let (fields1, rest1) = flatten_fields ty1
and (fields2, rest2) = flatten_fields ty2 in
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
let l1 = (repr ty1).level and l2 = (repr ty2).level in
let va =
if miss1 = [] then rest2
else if miss2 = [] then rest1
else newty2 (min l1 l2) Tvar
in
let d1 = rest1.desc and d2 = rest2.desc in
try
unify env (build_fields l1 miss1 va) rest2;
unify env rest1 (build_fields l2 miss2 va);
List.iter
(fun (n, k1, t1, k2, t2) ->
unify_kind k1 k2;
try unify env t1 t2 with Unify trace ->
raise (Unify ((newty (Tfield(n, k1, t1, va)),
newty (Tfield(n, k2, t2, va)))::trace)))
pairs
with exn ->
log_type rest1; rest1.desc <- d1;
log_type rest2; rest2.desc <- d2;
raise exn
and unify_kind k1 k2 =
let k1 = field_kind_repr k1 in
let k2 = field_kind_repr k2 in
if k1 == k2 then () else
match k1, k2 with
(Fvar r, (Fvar _ | Fpresent)) -> set_kind r k2
| (Fpresent, Fvar r) -> set_kind r k1
| (Fpresent, Fpresent) -> ()
| _ -> assert false
and unify_pairs env tpl =
List.iter (fun (t1, t2) -> unify env t1 t2) tpl
and unify_row env row1 row2 =
let row1 = row_repr row1 and row2 = row_repr row2 in
let rm1 = row_more row1 and rm2 = row_more row2 in
if rm1 == rm2 then () else
let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in
if r1 <> [] && r2 <> [] then begin
let ht = Hashtbl.create (List.length r1) in
List.iter (fun (l,_) -> Hashtbl.add ht (hash_variant l) l) r1;
List.iter
(fun (l,_) ->
try raise (Tags(l, Hashtbl.find ht (hash_variant l)))
with Not_found -> ())
r2
end;
let more =
if row1.row_fixed then rm1 else
if row2.row_fixed then rm2 else
newgenvar ()
in update_level env (min rm1.level rm2.level) more;
let fixed = row1.row_fixed || row2.row_fixed
and closed = row1.row_closed || row2.row_closed in
let keep switch =
List.for_all
(fun (_,f1,f2) ->
let f1, f2 = switch f1 f2 in
row_field_repr f1 = Rabsent || row_field_repr f2 <> Rabsent)
pairs
in
let empty fields =
List.for_all (fun (_,f) -> row_field_repr f = Rabsent) fields in
(* Check whether we are going to build an empty type *)
if closed && (empty r1 || row2.row_closed) && (empty r2 || row1.row_closed)
&& List.for_all
(fun (_,f1,f2) ->
row_field_repr f1 = Rabsent || row_field_repr f2 = Rabsent)
pairs
then raise (Unify [mkvariant [] true, mkvariant [] true]);
let name =
if row1.row_name <> None && (row1.row_closed || empty r2) &&
(not row2.row_closed || keep (fun f1 f2 -> f1, f2) && empty r1)
then row1.row_name
else if row2.row_name <> None && (row2.row_closed || empty r1) &&
(not row1.row_closed || keep (fun f1 f2 -> f2, f1) && empty r2)
then row2.row_name
else None
in
let row0 = {row_fields = []; row_more = more; row_bound = ();
row_closed = closed; row_fixed = fixed; row_name = name} in
let set_more row rest =
let rest =
if closed then
filter_row_fields row.row_closed rest
else rest in
if rest <> [] && (row.row_closed || row.row_fixed)
|| closed && row.row_fixed && not row.row_closed then begin
let t1 = mkvariant [] true and t2 = mkvariant rest false in
raise (Unify [if row == row1 then (t1,t2) else (t2,t1)])
end;
let rm = row_more row in
if row.row_fixed then
if row0.row_more == rm then () else
if rm.desc = Tvar then link_type rm row0.row_more else
unify env rm row0.row_more
else
let ty = newty2 generic_level (Tvariant {row0 with row_fields = rest}) in
update_level env rm.level ty;
link_type rm ty
in
let md1 = rm1.desc and md2 = rm2.desc in
begin try
set_more row2 r1;
set_more row1 r2;
List.iter
(fun (l,f1,f2) ->
try unify_row_field env row1.row_fixed row2.row_fixed more l f1 f2
with Unify trace ->
raise (Unify ((mkvariant [l,f1] true,
mkvariant [l,f2] true) :: trace)))
pairs;
with exn ->
log_type rm1; rm1.desc <- md1; log_type rm2; rm2.desc <- md2; raise exn
end
and unify_row_field env fixed1 fixed2 more l f1 f2 =
let f1 = row_field_repr f1 and f2 = row_field_repr f2 in
if f1 == f2 then () else
match f1, f2 with
Rpresent(Some t1), Rpresent(Some t2) -> unify env t1 t2
| Rpresent None, Rpresent None -> ()
| Reither(c1, tl1, m1, e1), Reither(c2, tl2, m2, e2) ->
if e1 == e2 then () else
let redo =
(m1 || m2 ||
!rigid_variants && (List.length tl1 = 1 || List.length tl2 = 1)) &&
begin match tl1 @ tl2 with [] -> false
| t1 :: tl ->
if c1 || c2 then raise (Unify []);
List.iter (unify env t1) tl;
!e1 <> None || !e2 <> None
end in
if redo then unify_row_field env fixed1 fixed2 more l f1 f2 else
let tl1 = List.map repr tl1 and tl2 = List.map repr tl2 in
let rec remq tl = function [] -> []
| ty :: tl' ->
if List.memq ty tl then remq tl tl' else ty :: remq tl tl'
in
let tl2' = remq tl2 tl1 and tl1' = remq tl1 tl2 in
(* Is this handling of levels really principal? *)
List.iter (update_level env (repr more).level) (tl1' @ tl2');
let e = ref None in
let f1' = Reither(c1 || c2, tl1', m1 || m2, e)
and f2' = Reither(c1 || c2, tl2', m1 || m2, e) in
set_row_field e1 f1'; set_row_field e2 f2';
| Reither(_, _, false, e1), Rabsent -> set_row_field e1 f2
| Rabsent, Reither(_, _, false, e2) -> set_row_field e2 f1
| Rabsent, Rabsent -> ()
| Reither(false, tl, _, e1), Rpresent(Some t2) when not fixed1 ->
set_row_field e1 f2;
(try List.iter (fun t1 -> unify env t1 t2) tl
with exn -> e1 := None; raise exn)
| Rpresent(Some t1), Reither(false, tl, _, e2) when not fixed2 ->
set_row_field e2 f1;
(try List.iter (unify env t1) tl
with exn -> e2 := None; raise exn)
| Reither(true, [], _, e1), Rpresent None when not fixed1 ->
set_row_field e1 f2
| Rpresent None, Reither(true, [], _, e2) when not fixed2 ->
set_row_field e2 f1
| _ -> raise (Unify [])
let unify env ty1 ty2 =
try
unify env ty1 ty2
with Unify trace ->
raise (Unify (expand_trace env trace))
let unify_var env t1 t2 =
let t1 = repr t1 and t2 = repr t2 in
if t1 == t2 then () else
match t1.desc with
Tvar ->
begin try
occur env t1 t2;
update_level env t1.level t2;
link_type t1 t2
with Unify trace ->
raise (Unify (expand_trace env ((t1,t2)::trace)))
end
| _ ->
unify env t1 t2
let _ = unify' := unify_var
let unify_pairs env ty1 ty2 pairs =
univar_pairs := pairs;
unify env ty1 ty2
let unify env ty1 ty2 =
univar_pairs := [];
unify env ty1 ty2
(**** Special cases of unification ****)
(*
Unify [t] and [l:'a -> 'b]. Return ['a] and ['b].
In label mode, label mismatch is accepted when
(1) the requested label is ""
(2) the original label is not optional
*)
let rec filter_arrow env t l =
let t = expand_head_unif env t in
match t.desc with
Tvar ->
let t1 = newvar () and t2 = newvar () in
let t' = newty (Tarrow (l, t1, t2, Cok)) in
update_level env t.level t';
link_type t t';
(t1, t2)
| Tarrow(l', t1, t2, _)
when l = l' || !Clflags.classic && l = "" && not (is_optional l') ->
(t1, t2)
| _ ->
raise (Unify [])
(* Used by [filter_method]. *)
let rec filter_method_field env name priv ty =
let ty = repr ty in
match ty.desc with
Tvar ->
let level = ty.level in
let ty1 = newvar2 level and ty2 = newvar2 level in
let ty' = newty2 level (Tfield (name,
begin match priv with
Private -> Fvar (ref None)
| Public -> Fpresent
end,
ty1, ty2))
in
link_type ty ty';
ty1
| Tfield(n, kind, ty1, ty2) ->
let kind = field_kind_repr kind in
if (n = name) && (kind <> Fabsent) then begin
if priv = Public then
unify_kind kind Fpresent;
ty1
end else
filter_method_field env name priv ty2
| _ ->
raise (Unify [])
(* Unify [ty] and [< name : 'a; .. >]. Return ['a]. *)
let rec filter_method env name priv ty =
let ty = expand_head_unif env ty in
match ty.desc with
Tvar ->
let ty1 = newvar () in
let ty' = newobj ty1 in
update_level env ty.level ty';
link_type ty ty';
filter_method_field env name priv ty1
| Tobject(f, _) ->
filter_method_field env name priv f
| _ ->
raise (Unify [])
let check_filter_method env name priv ty =
ignore(filter_method env name priv ty)
let filter_self_method env lab priv meths ty =
let ty' = filter_method env lab priv ty in
try
Meths.find lab !meths
with Not_found ->
let pair = (Ident.create lab, ty') in
meths := Meths.add lab pair !meths;
pair
(***********************************)
(* Matching between type schemes *)
(***********************************)
(*
Update the level of [ty]. First check that the levels of generic
variables from the subject are not lowered.
*)
let moregen_occur env level ty =
let rec occur ty =
let ty = repr ty in
if ty.level > level then begin
if ty.desc = Tvar && ty.level >= generic_level - 1 then raise Occur;
ty.level <- pivot_level - ty.level;
match ty.desc with
Tvariant row when static_row row ->
iter_row occur row
| _ ->
iter_type_expr occur ty
end
in
begin try
occur ty; unmark_type ty
with Occur ->
unmark_type ty; raise (Unify [])
end;
(* also check for free univars *)
occur_univar env ty;
update_level env level ty
let may_instantiate inst_nongen t1 =
if inst_nongen then t1.level <> generic_level - 1
else t1.level = generic_level
let rec moregen inst_nongen type_pairs env t1 t2 =
if t1 == t2 then () else
let t1 = repr t1 in
let t2 = repr t2 in
if t1 == t2 then () else
try
match (t1.desc, t2.desc) with
(Tunivar, Tunivar) ->
unify_univar t1 t2 !univar_pairs
| (Tvar, _) when may_instantiate inst_nongen t1 ->
moregen_occur env t1.level t2;
occur env t1 t2;
link_type t1 t2
| (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 ->
()
| _ ->
let t1' = expand_head_unif env t1 in
let t2' = expand_head_unif env t2 in
(* Expansion may have changed the representative of the types... *)
let t1' = repr t1' and t2' = repr t2' in
if t1' == t2' then () else
begin try
TypePairs.find type_pairs (t1', t2')
with Not_found ->
TypePairs.add type_pairs (t1', t2') ();
match (t1'.desc, t2'.desc) with
(Tvar, _) when may_instantiate inst_nongen t1' ->
moregen_occur env t1'.level t2;
link_type t1' t2
| (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _)) when l1 = l2
|| !Clflags.classic && not (is_optional l1 || is_optional l2) ->
moregen inst_nongen type_pairs env t1 t2;
moregen inst_nongen type_pairs env u1 u2
| (Ttuple tl1, Ttuple tl2) ->
moregen_list inst_nongen type_pairs env tl1 tl2
| (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _))
when Path.same p1 p2 ->
moregen_list inst_nongen type_pairs env tl1 tl2
| Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2) when Path.same p1 p2 && n1 = n2 ->
moregen_list inst_nongen type_pairs env tl1 tl2
| (Tvariant row1, Tvariant row2) ->
moregen_row inst_nongen type_pairs env row1 row2
| (Tobject (fi1, nm1), Tobject (fi2, nm2)) ->
moregen_fields inst_nongen type_pairs env fi1 fi2
| (Tfield _, Tfield _) -> (* Actually unused *)
moregen_fields inst_nongen type_pairs env t1' t2'
| (Tnil, Tnil) ->
()
| (Tpoly (t1, []), Tpoly (t2, [])) ->
moregen inst_nongen type_pairs env t1 t2
| (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
enter_poly env univar_pairs t1 tl1 t2 tl2
(moregen inst_nongen type_pairs env)
| (_, _) ->
raise (Unify [])
end
with Unify trace ->
raise (Unify ((t1, t2)::trace))
and moregen_list inst_nongen type_pairs env tl1 tl2 =
if List.length tl1 <> List.length tl2 then
raise (Unify []);
List.iter2 (moregen inst_nongen type_pairs env) tl1 tl2
and moregen_fields inst_nongen type_pairs env ty1 ty2 =
let (fields1, rest1) = flatten_fields ty1
and (fields2, rest2) = flatten_fields ty2 in
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
if miss1 <> [] then raise (Unify []);
moregen inst_nongen type_pairs env rest1
(build_fields (repr ty2).level miss2 rest2);
List.iter
(fun (n, k1, t1, k2, t2) ->
moregen_kind k1 k2;
try moregen inst_nongen type_pairs env t1 t2 with Unify trace ->
raise (Unify ((newty (Tfield(n, k1, t1, rest2)),
newty (Tfield(n, k2, t2, rest2)))::trace)))
pairs
and moregen_kind k1 k2 =
let k1 = field_kind_repr k1 in
let k2 = field_kind_repr k2 in
if k1 == k2 then () else
match k1, k2 with
(Fvar r, (Fvar _ | Fpresent)) -> set_kind r k2
| (Fpresent, Fpresent) -> ()
| _ -> raise (Unify [])
and moregen_row inst_nongen type_pairs env row1 row2 =
let row1 = row_repr row1 and row2 = row_repr row2 in
let rm1 = repr row1.row_more and rm2 = repr row2.row_more in
if rm1 == rm2 then () else
let may_inst = rm1.desc = Tvar && may_instantiate inst_nongen rm1 in
let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in
let r1, r2 =
if row2.row_closed then
filter_row_fields may_inst r1, filter_row_fields false r2
else r1, r2
in
if r1 <> [] || row1.row_closed && (not row2.row_closed || r2 <> [])
then raise (Unify []);
begin match rm1.desc, rm2.desc with
Tunivar, Tunivar ->
unify_univar rm1 rm2 !univar_pairs
| Tunivar, _ | _, Tunivar ->
raise (Unify [])
| _ when static_row row1 -> ()
| _ when may_inst ->
if not (static_row row2) then moregen_occur env rm1.level rm2;
let ext =
if r2 = [] then rm2 else
let row_ext = {row2 with row_fields = r2} in
iter_row (moregen_occur env rm1.level) row_ext;
newty2 rm1.level (Tvariant row_ext)
in
link_type rm1 ext
| Tconstr _, Tconstr _ ->
moregen inst_nongen type_pairs env rm1 rm2
| _ -> raise (Unify [])
end;
List.iter
(fun (l,f1,f2) ->
let f1 = row_field_repr f1 and f2 = row_field_repr f2 in
if f1 == f2 then () else
match f1, f2 with
Rpresent(Some t1), Rpresent(Some t2) ->
moregen inst_nongen type_pairs env t1 t2
| Rpresent None, Rpresent None -> ()
| Reither(false, tl1, _, e1), Rpresent(Some t2) when may_inst ->
set_row_field e1 f2;
List.iter (fun t1 -> moregen inst_nongen type_pairs env t1 t2) tl1
| Reither(c1, tl1, _, e1), Reither(c2, tl2, m2, e2) ->
if e1 != e2 then begin
if c1 && not c2 then raise(Unify []);
set_row_field e1 (Reither (c2, [], m2, e2));
if List.length tl1 = List.length tl2 then
List.iter2 (moregen inst_nongen type_pairs env) tl1 tl2
else match tl2 with
t2 :: _ ->
List.iter (fun t1 -> moregen inst_nongen type_pairs env t1 t2)
tl1
| [] ->
if tl1 <> [] then raise (Unify [])
end
| Reither(true, [], _, e1), Rpresent None when may_inst ->
set_row_field e1 f2
| Reither(_, _, _, e1), Rabsent when may_inst ->
set_row_field e1 f2
| Rabsent, Rabsent -> ()
| _ -> raise (Unify []))
pairs
(* Must empty univar_pairs first *)
let moregen inst_nongen type_pairs env patt subj =
univar_pairs := [];
moregen inst_nongen type_pairs env patt subj
(*
Non-generic variable can be instanciated only if [inst_nongen] is
true. So, [inst_nongen] should be set to false if the subject might
contain non-generic variables (and we do not want them to be
instanciated).
Usually, the subject is given by the user, and the pattern
is unimportant. So, no need to propagate abbreviations.
*)
let moregeneral env inst_nongen pat_sch subj_sch =
let old_level = !current_level in
current_level := generic_level - 1;
(*
Generic variables are first duplicated with [instance]. So,
their levels are lowered to [generic_level - 1]. The subject is
then copied with [duplicate_type]. That way, its levels won't be
changed.
*)
let subj = duplicate_type (instance subj_sch) in
current_level := generic_level;
(* Duplicate generic variables *)
let patt = instance pat_sch in
let res =
try moregen inst_nongen (TypePairs.create 13) env patt subj; true with
Unify _ -> false
in
current_level := old_level;
res
(* Alternative approach: "rigidify" a type scheme,
and check validity after unification *)
(* Simpler, no? *)
let rec rigidify_rec vars ty =
let ty = repr ty in
if ty.level >= lowest_level then begin
ty.level <- pivot_level - ty.level;
match ty.desc with
| Tvar ->
if not (List.memq ty !vars) then vars := ty :: !vars
| Tvariant row ->
let row = row_repr row in
let more = repr row.row_more in
if more.desc = Tvar && not row.row_fixed then begin
let more' = newty2 more.level Tvar in
let row' = {row with row_fixed=true; row_fields=[]; row_more=more'}
in link_type more (newty2 ty.level (Tvariant row'))
end;
iter_row (rigidify_rec vars) row;
(* only consider the row variable if the variant is not static *)
if not (static_row row) then rigidify_rec vars (row_more row)
| _ ->
iter_type_expr (rigidify_rec vars) ty
end
let rigidify ty =
let vars = ref [] in
rigidify_rec vars ty;
unmark_type ty;
!vars
let all_distinct_vars env vars =
let tyl = ref [] in
List.for_all
(fun ty ->
let ty = expand_head env ty in
if List.memq ty !tyl then false else
(tyl := ty :: !tyl; ty.desc = Tvar))
vars
let matches env ty ty' =
let snap = snapshot () in
let vars = rigidify ty in
cleanup_abbrev ();
let ok =
try unify env ty ty'; all_distinct_vars env vars
with Unify _ -> false
in
backtrack snap;
ok
(*********************************************)
(* Equivalence between parameterized types *)
(*********************************************)
let expand_head_rigid env ty =
let old = !rigid_variants in
rigid_variants := true;
let ty' = expand_head_unif env ty in
rigid_variants := old; ty'
let normalize_subst subst =
if List.exists
(function {desc=Tlink _}, _ | _, {desc=Tlink _} -> true | _ -> false)
!subst
then subst := List.map (fun (t1,t2) -> repr t1, repr t2) !subst
let rec eqtype rename type_pairs subst env t1 t2 =
if t1 == t2 then () else
let t1 = repr t1 in
let t2 = repr t2 in
if t1 == t2 then () else
try
match (t1.desc, t2.desc) with
(Tvar, Tvar) when rename ->
begin try
normalize_subst subst;
if List.assq t1 !subst != t2 then raise (Unify [])
with Not_found ->
if List.exists (fun (_, t) -> t == t2) !subst then raise (Unify []);
subst := (t1, t2) :: !subst
end
| (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 ->
()
| _ ->
let t1' = expand_head_rigid env t1 in
let t2' = expand_head_rigid env t2 in
(* Expansion may have changed the representative of the types... *)
let t1' = repr t1' and t2' = repr t2' in
if t1' == t2' then () else
begin try
TypePairs.find type_pairs (t1', t2')
with Not_found ->
TypePairs.add type_pairs (t1', t2') ();
match (t1'.desc, t2'.desc) with
(Tvar, Tvar) when rename ->
begin try
normalize_subst subst;
if List.assq t1' !subst != t2' then raise (Unify [])
with Not_found ->
if List.exists (fun (_, t) -> t == t2') !subst then raise (Unify []);
subst := (t1', t2') :: !subst
end
| (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _)) when l1 = l2
|| !Clflags.classic && not (is_optional l1 || is_optional l2) ->
eqtype rename type_pairs subst env t1 t2;
eqtype rename type_pairs subst env u1 u2;
| (Ttuple tl1, Ttuple tl2) ->
eqtype_list rename type_pairs subst env tl1 tl2
| (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _))
when Path.same p1 p2 ->
eqtype_list rename type_pairs subst env tl1 tl2
| Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2) when Path.same p1 p2 && n1 = n2 ->
eqtype_list rename type_pairs subst env tl1 tl2
| (Tvariant row1, Tvariant row2) ->
eqtype_row rename type_pairs subst env row1 row2
| (Tobject (fi1, nm1), Tobject (fi2, nm2)) ->
eqtype_fields rename type_pairs subst env fi1 fi2
| (Tfield _, Tfield _) -> (* Actually unused *)
eqtype_fields rename type_pairs subst env t1' t2'
| (Tnil, Tnil) ->
()
| (Tpoly (t1, []), Tpoly (t2, [])) ->
eqtype rename type_pairs subst env t1 t2
| (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
enter_poly env univar_pairs t1 tl1 t2 tl2
(eqtype rename type_pairs subst env)
| (Tunivar, Tunivar) ->
unify_univar t1' t2' !univar_pairs
| (_, _) ->
raise (Unify [])
end
with Unify trace ->
raise (Unify ((t1, t2)::trace))
and eqtype_list rename type_pairs subst env tl1 tl2 =
if List.length tl1 <> List.length tl2 then
raise (Unify []);
List.iter2 (eqtype rename type_pairs subst env) tl1 tl2
and eqtype_fields rename type_pairs subst env ty1 ty2 =
let (fields2, rest2) = flatten_fields ty2 in
(* Try expansion, needed when called from Includecore.type_manifest *)
match expand_head_rigid env rest2 with
{desc=Tobject(ty2,_)} -> eqtype_fields rename type_pairs subst env ty1 ty2
| _ ->
let (fields1, rest1) = flatten_fields ty1 in
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
eqtype rename type_pairs subst env rest1 rest2;
if (miss1 <> []) || (miss2 <> []) then raise (Unify []);
List.iter
(function (n, k1, t1, k2, t2) ->
eqtype_kind k1 k2;
try eqtype rename type_pairs subst env t1 t2 with Unify trace ->
raise (Unify ((newty (Tfield(n, k1, t1, rest2)),
newty (Tfield(n, k2, t2, rest2)))::trace)))
pairs
and eqtype_kind k1 k2 =
let k1 = field_kind_repr k1 in
let k2 = field_kind_repr k2 in
match k1, k2 with
(Fvar _, Fvar _)
| (Fpresent, Fpresent) -> ()
| _ -> raise (Unify [])
and eqtype_row rename type_pairs subst env row1 row2 =
(* Try expansion, needed when called from Includecore.type_manifest *)
match expand_head_rigid env (row_more row2) with
{desc=Tvariant row2} -> eqtype_row rename type_pairs subst env row1 row2
| _ ->
let row1 = row_repr row1 and row2 = row_repr row2 in
let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in
if row1.row_closed <> row2.row_closed
|| not row1.row_closed && (r1 <> [] || r2 <> [])
|| filter_row_fields false (r1 @ r2) <> []
then raise (Unify []);
if not (static_row row1) then
eqtype rename type_pairs subst env row1.row_more row2.row_more;
List.iter
(fun (_,f1,f2) ->
match row_field_repr f1, row_field_repr f2 with
Rpresent(Some t1), Rpresent(Some t2) ->
eqtype rename type_pairs subst env t1 t2
| Reither(true, [], _, _), Reither(true, [], _, _) ->
()
| Reither(false, t1::tl1, _, _), Reither(false, t2::tl2, _, _) ->
eqtype rename type_pairs subst env t1 t2;
if List.length tl1 = List.length tl2 then
(* if same length allow different types (meaning?) *)
List.iter2 (eqtype rename type_pairs subst env) tl1 tl2
else begin
(* otherwise everything must be equal *)
List.iter (eqtype rename type_pairs subst env t1) tl2;
List.iter (fun t1 -> eqtype rename type_pairs subst env t1 t2) tl1
end
| Rpresent None, Rpresent None -> ()
| Rabsent, Rabsent -> ()
| _ -> raise (Unify []))
pairs
(* Two modes: with or without renaming of variables *)
let equal env rename tyl1 tyl2 =
try
univar_pairs := [];
eqtype_list rename (TypePairs.create 11) (ref []) env tyl1 tyl2; true
with
Unify _ -> false
(* Must empty univar_pairs first *)
let eqtype rename type_pairs subst env t1 t2 =
univar_pairs := [];
eqtype rename type_pairs subst env t1 t2
(*************************)
(* Class type matching *)
(*************************)
type class_match_failure =
CM_Virtual_class
| CM_Parameter_arity_mismatch of int * int
| CM_Type_parameter_mismatch of (type_expr * type_expr) list
| CM_Class_type_mismatch of class_type * class_type
| CM_Parameter_mismatch of (type_expr * type_expr) list
| CM_Val_type_mismatch of string * (type_expr * type_expr) list
| CM_Meth_type_mismatch of string * (type_expr * type_expr) list
| CM_Non_mutable_value of string
| CM_Non_concrete_value of string
| CM_Missing_value of string
| CM_Missing_method of string
| CM_Hide_public of string
| CM_Hide_virtual of string * string
| CM_Public_method of string
| CM_Private_method of string
| CM_Virtual_method of string
exception Failure of class_match_failure list
let rec moregen_clty trace type_pairs env cty1 cty2 =
try
match cty1, cty2 with
Tcty_constr (_, _, cty1), _ ->
moregen_clty true type_pairs env cty1 cty2
| _, Tcty_constr (_, _, cty2) ->
moregen_clty true type_pairs env cty1 cty2
| Tcty_fun (l1, ty1, cty1'), Tcty_fun (l2, ty2, cty2') when l1 = l2 ->
begin try moregen true type_pairs env ty1 ty2 with Unify trace ->
raise (Failure [CM_Parameter_mismatch (expand_trace env trace)])
end;
moregen_clty false type_pairs env cty1' cty2'
| Tcty_signature sign1, Tcty_signature sign2 ->
let ty1 = object_fields (repr sign1.cty_self) in
let ty2 = object_fields (repr sign2.cty_self) in
let (fields1, rest1) = flatten_fields ty1
and (fields2, rest2) = flatten_fields ty2 in
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
List.iter
(fun (lab, k1, t1, k2, t2) ->
begin try moregen true type_pairs env t1 t2 with Unify trace ->
raise (Failure [CM_Meth_type_mismatch
(lab, expand_trace env trace)])
end)
pairs;
Vars.iter
(fun lab (mut, v, ty) ->
let (mut', v', ty') = Vars.find lab sign1.cty_vars in
try moregen true type_pairs env ty' ty with Unify trace ->
raise (Failure [CM_Val_type_mismatch
(lab, expand_trace env trace)]))
sign2.cty_vars
| _ ->
raise (Failure [])
with
Failure error when trace || error = [] ->
raise (Failure (CM_Class_type_mismatch (cty1, cty2)::error))
let match_class_types ?(trace=true) env pat_sch subj_sch =
let type_pairs = TypePairs.create 53 in
let old_level = !current_level in
current_level := generic_level - 1;
(*
Generic variables are first duplicated with [instance]. So,
their levels are lowered to [generic_level - 1]. The subject is
then copied with [duplicate_type]. That way, its levels won't be
changed.
*)
let (_, subj_inst) = instance_class [] subj_sch in
let subj = duplicate_class_type subj_inst in
current_level := generic_level;
(* Duplicate generic variables *)
let (_, patt) = instance_class [] pat_sch in
let res =
let sign1 = signature_of_class_type patt in
let sign2 = signature_of_class_type subj in
let t1 = repr sign1.cty_self in
let t2 = repr sign2.cty_self in
TypePairs.add type_pairs (t1, t2) ();
let (fields1, rest1) = flatten_fields (object_fields t1)
and (fields2, rest2) = flatten_fields (object_fields t2) in
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
let error =
List.fold_right
(fun (lab, k, _) err ->
let err =
let k = field_kind_repr k in
begin match k with
Fvar r -> set_kind r Fabsent; err
| _ -> CM_Hide_public lab::err
end
in
if Concr.mem lab sign1.cty_concr then err
else CM_Hide_virtual ("method", lab) :: err)
miss1 []
in
let missing_method = List.map (fun (m, _, _) -> m) miss2 in
let error =
(List.map (fun m -> CM_Missing_method m) missing_method) @ error
in
(* Always succeeds *)
moregen true type_pairs env rest1 rest2;
let error =
List.fold_right
(fun (lab, k1, t1, k2, t2) err ->
try moregen_kind k1 k2; err with
Unify _ -> CM_Public_method lab::err)
pairs error
in
let error =
Vars.fold
(fun lab (mut, vr, ty) err ->
try
let (mut', vr', ty') = Vars.find lab sign1.cty_vars in
if mut = Mutable && mut' <> Mutable then
CM_Non_mutable_value lab::err
else if vr = Concrete && vr' <> Concrete then
CM_Non_concrete_value lab::err
else
err
with Not_found ->
CM_Missing_value lab::err)
sign2.cty_vars error
in
let error =
Vars.fold
(fun lab (_,vr,_) err ->
if vr = Virtual && not (Vars.mem lab sign2.cty_vars) then
CM_Hide_virtual ("instance variable", lab) :: err
else err)
sign1.cty_vars error
in
let error =
List.fold_right
(fun e l ->
if List.mem e missing_method then l else CM_Virtual_method e::l)
(Concr.elements (Concr.diff sign2.cty_concr sign1.cty_concr))
error
in
match error with
[] ->
begin try
moregen_clty trace type_pairs env patt subj;
[]
with
Failure r -> r
end
| error ->
CM_Class_type_mismatch (patt, subj)::error
in
current_level := old_level;
res
let rec equal_clty trace type_pairs subst env cty1 cty2 =
try
match cty1, cty2 with
Tcty_constr (_, _, cty1), Tcty_constr (_, _, cty2) ->
equal_clty true type_pairs subst env cty1 cty2
| Tcty_constr (_, _, cty1), _ ->
equal_clty true type_pairs subst env cty1 cty2
| _, Tcty_constr (_, _, cty2) ->
equal_clty true type_pairs subst env cty1 cty2
| Tcty_fun (l1, ty1, cty1'), Tcty_fun (l2, ty2, cty2') when l1 = l2 ->
begin try eqtype true type_pairs subst env ty1 ty2 with Unify trace ->
raise (Failure [CM_Parameter_mismatch (expand_trace env trace)])
end;
equal_clty false type_pairs subst env cty1' cty2'
| Tcty_signature sign1, Tcty_signature sign2 ->
let ty1 = object_fields (repr sign1.cty_self) in
let ty2 = object_fields (repr sign2.cty_self) in
let (fields1, rest1) = flatten_fields ty1
and (fields2, rest2) = flatten_fields ty2 in
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
List.iter
(fun (lab, k1, t1, k2, t2) ->
begin try eqtype true type_pairs subst env t1 t2 with
Unify trace ->
raise (Failure [CM_Meth_type_mismatch
(lab, expand_trace env trace)])
end)
pairs;
Vars.iter
(fun lab (_, _, ty) ->
let (_, _, ty') = Vars.find lab sign1.cty_vars in
try eqtype true type_pairs subst env ty' ty with Unify trace ->
raise (Failure [CM_Val_type_mismatch
(lab, expand_trace env trace)]))
sign2.cty_vars
| _ ->
raise
(Failure (if trace then []
else [CM_Class_type_mismatch (cty1, cty2)]))
with
Failure error when trace ->
raise (Failure (CM_Class_type_mismatch (cty1, cty2)::error))
let match_class_declarations env patt_params patt_type subj_params subj_type =
let type_pairs = TypePairs.create 53 in
let subst = ref [] in
let sign1 = signature_of_class_type patt_type in
let sign2 = signature_of_class_type subj_type in
let t1 = repr sign1.cty_self in
let t2 = repr sign2.cty_self in
TypePairs.add type_pairs (t1, t2) ();
let (fields1, rest1) = flatten_fields (object_fields t1)
and (fields2, rest2) = flatten_fields (object_fields t2) in
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
let error =
List.fold_right
(fun (lab, k, _) err ->
let err =
let k = field_kind_repr k in
begin match k with
Fvar r -> err
| _ -> CM_Hide_public lab::err
end
in
if Concr.mem lab sign1.cty_concr then err
else CM_Hide_virtual ("method", lab) :: err)
miss1 []
in
let missing_method = List.map (fun (m, _, _) -> m) miss2 in
let error =
(List.map (fun m -> CM_Missing_method m) missing_method) @ error
in
(* Always succeeds *)
eqtype true type_pairs subst env rest1 rest2;
let error =
List.fold_right
(fun (lab, k1, t1, k2, t2) err ->
let k1 = field_kind_repr k1 in
let k2 = field_kind_repr k2 in
match k1, k2 with
(Fvar _, Fvar _)
| (Fpresent, Fpresent) -> err
| (Fvar _, Fpresent) -> CM_Private_method lab::err
| (Fpresent, Fvar _) -> CM_Public_method lab::err
| _ -> assert false)
pairs error
in
let error =
Vars.fold
(fun lab (mut, vr, ty) err ->
try
let (mut', vr', ty') = Vars.find lab sign1.cty_vars in
if mut = Mutable && mut' <> Mutable then
CM_Non_mutable_value lab::err
else if vr = Concrete && vr' <> Concrete then
CM_Non_concrete_value lab::err
else
err
with Not_found ->
CM_Missing_value lab::err)
sign2.cty_vars error
in
let error =
Vars.fold
(fun lab (_,vr,_) err ->
if vr = Virtual && not (Vars.mem lab sign2.cty_vars) then
CM_Hide_virtual ("instance variable", lab) :: err
else err)
sign1.cty_vars error
in
let error =
List.fold_right
(fun e l ->
if List.mem e missing_method then l else CM_Virtual_method e::l)
(Concr.elements (Concr.diff sign2.cty_concr sign1.cty_concr))
error
in
match error with
[] ->
begin try
let lp = List.length patt_params in
let ls = List.length subj_params in
if lp <> ls then
raise (Failure [CM_Parameter_arity_mismatch (lp, ls)]);
List.iter2 (fun p s ->
try eqtype true type_pairs subst env p s with Unify trace ->
raise (Failure [CM_Type_parameter_mismatch
(expand_trace env trace)]))
patt_params subj_params;
(* old code: equal_clty false type_pairs subst env patt_type subj_type; *)
equal_clty false type_pairs subst env
(Tcty_signature sign1) (Tcty_signature sign2);
(* Use moregeneral for class parameters, need to recheck everything to
keeps relationships (PR#4824) *)
let clty_params = List.fold_right (fun ty cty -> Tcty_fun ("*",ty,cty)) in
match_class_types ~trace:false env
(clty_params patt_params patt_type) (clty_params subj_params subj_type)
with
Failure r -> r
end
| error ->
error
(***************)
(* Subtyping *)
(***************)
(**** Build a subtype of a given type. ****)
(* build_subtype:
[visited] traces traversed object and variant types
[loops] is a mapping from variables to variables, to reproduce
positive loops in a class type
[posi] true if the current variance is positive
[level] number of expansions/enlargement allowed on this branch *)
let warn = ref false (* whether double coercion might do better *)
let pred_expand n = if n mod 2 = 0 && n > 0 then pred n else n
let pred_enlarge n = if n mod 2 = 1 then pred n else n
type change = Unchanged | Equiv | Changed
let collect l = List.fold_left (fun c1 (_, c2) -> max c1 c2) Unchanged l
let rec filter_visited = function
[] -> []
| {desc=Tobject _|Tvariant _} :: _ as l -> l
| _ :: l -> filter_visited l
let memq_warn t visited =
if List.memq t visited then (warn := true; true) else false
let rec lid_of_path sharp = function
Path.Pident id ->
Longident.Lident (sharp ^ Ident.name id)
| Path.Pdot (p1, s, _) ->
Longident.Ldot (lid_of_path "" p1, sharp ^ s)
| Path.Papply (p1, p2) ->
Longident.Lapply (lid_of_path sharp p1, lid_of_path "" p2)
let find_cltype_for_path env p =
let path, cl_abbr = Env.lookup_type (lid_of_path "#" p) env in
match cl_abbr.type_manifest with
Some ty ->
begin match (repr ty).desc with
Tobject(_,{contents=Some(p',_)}) when Path.same p p' -> cl_abbr, ty
| _ -> raise Not_found
end
| None -> assert false
let has_constr_row' env t =
has_constr_row (expand_abbrev env t)
let rec build_subtype env visited loops posi level t =
let t = repr t in
match t.desc with
Tvar ->
if posi then
try
let t' = List.assq t loops in
warn := true;
(t', Equiv)
with Not_found ->
(t, Unchanged)
else
(t, Unchanged)
| Tarrow(l, t1, t2, _) ->
if memq_warn t visited then (t, Unchanged) else
let visited = t :: visited in
let (t1', c1) = build_subtype env visited loops (not posi) level t1 in
let (t2', c2) = build_subtype env visited loops posi level t2 in
let c = max c1 c2 in
if c > Unchanged then (newty (Tarrow(l, t1', t2', Cok)), c)
else (t, Unchanged)
| Ttuple tlist ->
if memq_warn t visited then (t, Unchanged) else
let visited = t :: visited in
let tlist' =
List.map (build_subtype env visited loops posi level) tlist
in
let c = collect tlist' in
if c > Unchanged then (newty (Ttuple (List.map fst tlist')), c)
else (t, Unchanged)
| Tconstr(p, tl, abbrev)
when level > 0 && generic_abbrev env p && safe_abbrev env t
&& not (has_constr_row' env t) ->
let t' = repr (expand_abbrev env t) in
let level' = pred_expand level in
begin try match t'.desc with
Tobject _ when posi && not (opened_object t') ->
let cl_abbr, body = find_cltype_for_path env p in
let ty =
subst env !current_level Public abbrev None
cl_abbr.type_params tl body in
let ty = repr ty in
let ty1, tl1 =
match ty.desc with
Tobject(ty1,{contents=Some(p',tl1)}) when Path.same p p' ->
ty1, tl1
| _ -> raise Not_found
in
(* Fix PR4505: do not set ty to Tvar when it appears in tl1,
as this occurence might break the occur check.
XXX not clear whether this correct anyway... *)
if List.exists (deep_occur ty) tl1 then raise Not_found;
ty.desc <- Tvar;
let t'' = newvar () in
let loops = (ty, t'') :: loops in
(* May discard [visited] as level is going down *)
let (ty1', c) =
build_subtype env [t'] loops posi (pred_enlarge level') ty1 in
assert (t''.desc = Tvar);
let nm =
if c > Equiv || deep_occur ty ty1' then None else Some(p,tl1) in
t''.desc <- Tobject (ty1', ref nm);
(try unify_var env ty t with Unify _ -> assert false);
(t'', Changed)
| _ -> raise Not_found
with Not_found ->
let (t'',c) = build_subtype env visited loops posi level' t' in
if c > Unchanged then (t'',c)
else (t, Unchanged)
end
| Tconstr(p, tl, abbrev) ->
(* Must check recursion on constructors, since we do not always
expand them *)
if memq_warn t visited then (t, Unchanged) else
let visited = t :: visited in
begin try
let decl = Env.find_type p env in
if level = 0 && generic_abbrev env p && safe_abbrev env t
&& not (has_constr_row' env t)
then warn := true;
let tl' =
List.map2
(fun (co,cn,_) t ->
if cn then
if co then (t, Unchanged)
else build_subtype env visited loops (not posi) level t
else
if co then build_subtype env visited loops posi level t
else (newvar(), Changed))
decl.type_variance tl
in
let c = collect tl' in
if c > Unchanged then (newconstr p (List.map fst tl'), c)
else (t, Unchanged)
with Not_found ->
(t, Unchanged)
end
| Tvariant row ->
let row = row_repr row in
if memq_warn t visited || not (static_row row) then (t, Unchanged) else
let level' = pred_enlarge level in
let visited =
t :: if level' < level then [] else filter_visited visited in
let fields = filter_row_fields false row.row_fields in
let fields =
List.map
(fun (l,f as orig) -> match row_field_repr f with
Rpresent None ->
if posi then
(l, Reither(true, [], false, ref None)), Unchanged
else
orig, Unchanged
| Rpresent(Some t) ->
let (t', c) = build_subtype env visited loops posi level' t in
let f =
if posi && level > 0
then Reither(false, [t'], false, ref None)
else Rpresent(Some t')
in (l, f), c
| _ -> assert false)
fields
in
let c = collect fields in
let row =
{ row_fields = List.map fst fields; row_more = newvar();
row_bound = (); row_closed = posi; row_fixed = false;
row_name = if c > Unchanged then None else row.row_name }
in
(newty (Tvariant row), Changed)
| Tobject (t1, _) ->
if memq_warn t visited || opened_object t1 then (t, Unchanged) else
let level' = pred_enlarge level in
let visited =
t :: if level' < level then [] else filter_visited visited in
let (t1', c) = build_subtype env visited loops posi level' t1 in
if c > Unchanged then (newty (Tobject (t1', ref None)), c)
else (t, Unchanged)
| Tfield(s, _, t1, t2) (* Always present *) ->
let (t1', c1) = build_subtype env visited loops posi level t1 in
let (t2', c2) = build_subtype env visited loops posi level t2 in
let c = max c1 c2 in
if c > Unchanged then (newty (Tfield(s, Fpresent, t1', t2')), c)
else (t, Unchanged)
| Tnil ->
if posi then
let v = newvar () in
(v, Changed)
else begin
warn := true;
(t, Unchanged)
end
| Tsubst _ | Tlink _ ->
assert false
| Tpoly(t1, tl) ->
let (t1', c) = build_subtype env visited loops posi level t1 in
if c > Unchanged then (newty (Tpoly(t1', tl)), c)
else (t, Unchanged)
| Tunivar | Tpackage _ ->
(t, Unchanged)
let enlarge_type env ty =
warn := false;
(* [level = 4] allows 2 expansions involving objects/variants *)
let (ty', _) = build_subtype env [] [] true 4 ty in
(ty', !warn)
(**** Check whether a type is a subtype of another type. ****)
(*
During the traversal, a trace of visited types is maintained. It
is printed in case of error.
Constraints (pairs of types that must be equals) are accumulated
rather than being enforced straight. Indeed, the result would
otherwise depend on the order in which these constraints are
enforced.
A function enforcing these constraints is returned. That way, type
variables can be bound to their actual values before this function
is called (see Typecore).
Only well-defined abbreviations are expanded (hence the tests
[generic_abbrev ...]).
*)
let subtypes = TypePairs.create 17
let subtype_error env trace =
raise (Subtype (expand_trace env (List.rev trace), []))
let private_abbrev env path =
try
let decl = Env.find_type path env in
decl.type_private = Private && decl.type_manifest <> None
with Not_found -> false
let rec subtype_rec env trace t1 t2 cstrs =
let t1 = repr t1 in
let t2 = repr t2 in
if t1 == t2 then cstrs else
begin try
TypePairs.find subtypes (t1, t2);
cstrs
with Not_found ->
TypePairs.add subtypes (t1, t2) ();
match (t1.desc, t2.desc) with
(Tvar, _) | (_, Tvar) ->
(trace, t1, t2, !univar_pairs)::cstrs
| (Tarrow(l1, t1, u1, _), Tarrow(l2, t2, u2, _)) when l1 = l2
|| !Clflags.classic && not (is_optional l1 || is_optional l2) ->
let cstrs = subtype_rec env ((t2, t1)::trace) t2 t1 cstrs in
subtype_rec env ((u1, u2)::trace) u1 u2 cstrs
| (Ttuple tl1, Ttuple tl2) ->
subtype_list env trace tl1 tl2 cstrs
| (Tconstr(p1, [], _), Tconstr(p2, [], _)) when Path.same p1 p2 ->
cstrs
| (Tconstr(p1, tl1, abbrev1), _)
when generic_abbrev env p1 && safe_abbrev env t1 ->
subtype_rec env trace (expand_abbrev env t1) t2 cstrs
| (_, Tconstr(p2, tl2, abbrev2))
when generic_abbrev env p2 && safe_abbrev env t2 ->
subtype_rec env trace t1 (expand_abbrev env t2) cstrs
| (Tconstr(p1, tl1, _), Tconstr(p2, tl2, _)) when Path.same p1 p2 ->
begin try
let decl = Env.find_type p1 env in
List.fold_left2
(fun cstrs (co, cn, _) (t1, t2) ->
if co then
if cn then
(trace, newty2 t1.level (Ttuple[t1]),
newty2 t2.level (Ttuple[t2]), !univar_pairs) :: cstrs
else subtype_rec env ((t1, t2)::trace) t1 t2 cstrs
else
if cn then subtype_rec env ((t2, t1)::trace) t2 t1 cstrs
else cstrs)
cstrs decl.type_variance (List.combine tl1 tl2)
with Not_found ->
(trace, t1, t2, !univar_pairs)::cstrs
end
| (Tconstr(p1, tl1, _), _) when private_abbrev env p1 ->
subtype_rec env trace (expand_abbrev_opt env t1) t2 cstrs
| (Tobject (f1, _), Tobject (f2, _))
when (object_row f1).desc = Tvar && (object_row f2).desc = Tvar ->
(* Same row variable implies same object. *)
(trace, t1, t2, !univar_pairs)::cstrs
| (Tobject (f1, _), Tobject (f2, _)) ->
subtype_fields env trace f1 f2 cstrs
| (Tvariant row1, Tvariant row2) ->
begin try
subtype_row env trace row1 row2 cstrs
with Exit ->
(trace, t1, t2, !univar_pairs)::cstrs
end
| (Tpoly (u1, []), Tpoly (u2, [])) ->
subtype_rec env trace u1 u2 cstrs
| (Tpoly (u1, tl1), Tpoly (u2, [])) ->
let _, u1' = instance_poly false tl1 u1 in
subtype_rec env trace u1' u2 cstrs
| (Tpoly (u1, tl1), Tpoly (u2,tl2)) ->
begin try
enter_poly env univar_pairs u1 tl1 u2 tl2
(fun t1 t2 -> subtype_rec env trace t1 t2 cstrs)
with Unify _ ->
(trace, t1, t2, !univar_pairs)::cstrs
end
| (_, _) ->
(trace, t1, t2, !univar_pairs)::cstrs
end
and subtype_list env trace tl1 tl2 cstrs =
if List.length tl1 <> List.length tl2 then
subtype_error env trace;
List.fold_left2
(fun cstrs t1 t2 -> subtype_rec env ((t1, t2)::trace) t1 t2 cstrs)
cstrs tl1 tl2
and subtype_fields env trace ty1 ty2 cstrs =
(* Assume that either rest1 or rest2 is not Tvar *)
let (fields1, rest1) = flatten_fields ty1 in
let (fields2, rest2) = flatten_fields ty2 in
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
let cstrs =
if rest2.desc = Tnil then cstrs else
if miss1 = [] then
subtype_rec env ((rest1, rest2)::trace) rest1 rest2 cstrs
else
(trace, build_fields (repr ty1).level miss1 rest1, rest2,
!univar_pairs) :: cstrs
in
let cstrs =
if miss2 = [] then cstrs else
(trace, rest1, build_fields (repr ty2).level miss2 (newvar ()),
!univar_pairs) :: cstrs
in
List.fold_left
(fun cstrs (_, k1, t1, k2, t2) ->
(* Theses fields are always present *)
subtype_rec env ((t1, t2)::trace) t1 t2 cstrs)
cstrs pairs
and subtype_row env trace row1 row2 cstrs =
let row1 = row_repr row1 and row2 = row_repr row2 in
let r1, r2, pairs =
merge_row_fields row1.row_fields row2.row_fields in
let more1 = repr row1.row_more
and more2 = repr row2.row_more in
match more1.desc, more2.desc with
Tconstr(p1,_,_), Tconstr(p2,_,_) when Path.same p1 p2 ->
subtype_rec env ((more1,more2)::trace) more1 more2 cstrs
| (Tvar|Tconstr _), (Tvar|Tconstr _)
when row1.row_closed && r1 = [] ->
List.fold_left
(fun cstrs (_,f1,f2) ->
match row_field_repr f1, row_field_repr f2 with
(Rpresent None|Reither(true,_,_,_)), Rpresent None ->
cstrs
| Rpresent(Some t1), Rpresent(Some t2) ->
subtype_rec env ((t1, t2)::trace) t1 t2 cstrs
| Reither(false, t1::_, _, _), Rpresent(Some t2) ->
subtype_rec env ((t1, t2)::trace) t1 t2 cstrs
| Rabsent, _ -> cstrs
| _ -> raise Exit)
cstrs pairs
| Tunivar, Tunivar
when row1.row_closed = row2.row_closed && r1 = [] && r2 = [] ->
let cstrs =
subtype_rec env ((more1,more2)::trace) more1 more2 cstrs in
List.fold_left
(fun cstrs (_,f1,f2) ->
match row_field_repr f1, row_field_repr f2 with
Rpresent None, Rpresent None
| Reither(true,[],_,_), Reither(true,[],_,_)
| Rabsent, Rabsent ->
cstrs
| Rpresent(Some t1), Rpresent(Some t2)
| Reither(false,[t1],_,_), Reither(false,[t2],_,_) ->
subtype_rec env ((t1, t2)::trace) t1 t2 cstrs
| _ -> raise Exit)
cstrs pairs
| _ ->
raise Exit
let subtype env ty1 ty2 =
TypePairs.clear subtypes;
univar_pairs := [];
(* Build constraint set. *)
let cstrs = subtype_rec env [(ty1, ty2)] ty1 ty2 [] in
TypePairs.clear subtypes;
(* Enforce constraints. *)
function () ->
List.iter
(function (trace0, t1, t2, pairs) ->
try unify_pairs env t1 t2 pairs with Unify trace ->
raise (Subtype (expand_trace env (List.rev trace0),
List.tl (List.tl trace))))
(List.rev cstrs)
(*******************)
(* Miscellaneous *)
(*******************)
(* Utility for printing. The resulting type is not used in computation. *)
let rec unalias_object ty =
let ty = repr ty in
match ty.desc with
Tfield (s, k, t1, t2) ->
newty2 ty.level (Tfield (s, k, t1, unalias_object t2))
| Tvar | Tnil ->
newty2 ty.level ty.desc
| Tunivar ->
ty
| Tconstr _ ->
newty2 ty.level Tvar
| _ ->
assert false
let unalias ty =
let ty = repr ty in
match ty.desc with
Tvar | Tunivar ->
ty
| Tvariant row ->
let row = row_repr row in
let more = row.row_more in
newty2 ty.level
(Tvariant {row with row_more = newty2 more.level more.desc})
| Tobject (ty, nm) ->
newty2 ty.level (Tobject (unalias_object ty, nm))
| _ ->
newty2 ty.level ty.desc
(* Return the arity (as for curried functions) of the given type. *)
let rec arity ty =
match (repr ty).desc with
Tarrow(_, t1, t2, _) -> 1 + arity t2
| _ -> 0
(* Check whether an abbreviation expands to itself. *)
let cyclic_abbrev env id ty =
let rec check_cycle seen ty =
let ty = repr ty in
match ty.desc with
Tconstr (p, tl, abbrev) ->
p = Path.Pident id || List.memq ty seen ||
begin try
check_cycle (ty :: seen) (expand_abbrev_opt env ty)
with
Cannot_expand -> false
| Unify _ -> true
end
| _ ->
false
in check_cycle [] ty
(* Normalize a type before printing, saving... *)
(* Cannot use mark_type because deep_occur uses it too *)
let rec normalize_type_rec env visited ty =
let ty = repr ty in
if not (TypeSet.mem ty !visited) then begin
visited := TypeSet.add ty !visited;
begin match ty.desc with
| Tvariant row ->
let row = row_repr row in
let fields = List.map
(fun (l,f0) ->
let f = row_field_repr f0 in l,
match f with Reither(b, ty::(_::_ as tyl), m, e) ->
let tyl' =
List.fold_left
(fun tyl ty ->
if List.exists (fun ty' -> equal env false [ty] [ty']) tyl
then tyl else ty::tyl)
[ty] tyl
in
if f != f0 || List.length tyl' < List.length tyl then
Reither(b, List.rev tyl', m, e)
else f
| _ -> f)
row.row_fields in
let fields =
List.sort (fun (p,_) (q,_) -> compare p q)
(List.filter (fun (_,fi) -> fi <> Rabsent) fields) in
log_type ty;
ty.desc <- Tvariant {row with row_fields = fields}
| Tobject (fi, nm) ->
begin match !nm with
| None -> ()
| Some (n, v :: l) ->
if deep_occur ty (newgenty (Ttuple l)) then
(* The abbreviation may be hiding something, so remove it *)
set_name nm None
else let v' = repr v in
begin match v'.desc with
| Tvar|Tunivar ->
if v' != v then set_name nm (Some (n, v' :: l))
| Tnil ->
log_type ty; ty.desc <- Tconstr (n, l, ref Mnil)
| _ -> set_name nm None
end
| _ ->
fatal_error "Ctype.normalize_type_rec"
end;
let fi = repr fi in
if fi.level < lowest_level then () else
let fields, row = flatten_fields fi in
let fi' = build_fields fi.level fields row in
log_type ty; fi.desc <- fi'.desc
| _ -> ()
end;
iter_type_expr (normalize_type_rec env visited) ty
end
let normalize_type env ty =
normalize_type_rec env (ref TypeSet.empty) ty
(*************************)
(* Remove dependencies *)
(*************************)
(*
Variables are left unchanged. Other type nodes are duplicated, with
levels set to generic level.
We cannot use Tsubst here, because unification may be called by
expand_abbrev.
*)
let nondep_hash = TypeHash.create 47
let nondep_variants = TypeHash.create 17
let clear_hash () =
TypeHash.clear nondep_hash; TypeHash.clear nondep_variants
let rec nondep_type_rec env id ty =
match ty.desc with
Tvar | Tunivar -> ty
| Tlink ty -> nondep_type_rec env id ty
| _ -> try TypeHash.find nondep_hash ty
with Not_found ->
let ty' = newgenvar () in (* Stub *)
TypeHash.add nondep_hash ty ty';
ty'.desc <-
begin match ty.desc with
| Tconstr(p, tl, abbrev) ->
if Path.isfree id p then
begin try
Tlink (nondep_type_rec env id
(expand_abbrev env (newty2 ty.level ty.desc)))
(*
The [Tlink] is important. The expanded type may be a
variable, or may not be completely copied yet
(recursive type), so one cannot just take its
description.
*)
with Cannot_expand | Unify _ ->
raise Not_found
end
else
Tconstr(p, List.map (nondep_type_rec env id) tl, ref Mnil)
| Tpackage(p, _, _) when Path.isfree id p ->
raise Not_found
| Tobject (t1, name) ->
Tobject (nondep_type_rec env id t1,
ref (match !name with
None -> None
| Some (p, tl) ->
if Path.isfree id p then None
else Some (p, List.map (nondep_type_rec env id) tl)))
| Tvariant row ->
let row = row_repr row in
let more = repr row.row_more in
(* We must keep sharing according to the row variable *)
begin try
let ty2 = TypeHash.find nondep_variants more in
(* This variant type has been already copied *)
TypeHash.add nondep_hash ty ty2;
Tlink ty2
with Not_found ->
(* Register new type first for recursion *)
TypeHash.add nondep_variants more ty';
let static = static_row row in
let more' = if static then newgenvar () else more in
(* Return a new copy *)
let row =
copy_row (nondep_type_rec env id) true row true more' in
match row.row_name with
Some (p, tl) when Path.isfree id p ->
Tvariant {row with row_name = None}
| _ -> Tvariant row
end
| _ -> copy_type_desc (nondep_type_rec env id) ty.desc
end;
ty'
let nondep_type env id ty =
try
let ty' = nondep_type_rec env id ty in
clear_hash ();
ty'
with Not_found ->
clear_hash ();
raise Not_found
let unroll_abbrev id tl ty =
let ty = repr ty and path = Path.Pident id in
if (ty.desc = Tvar) || (List.exists (deep_occur ty) tl)
|| is_object_type path then
ty
else
let ty' = newty2 ty.level ty.desc in
link_type ty (newty2 ty.level (Tconstr (path, tl, ref Mnil)));
ty'
(* Preserve sharing inside type declarations. *)
let nondep_type_decl env mid id is_covariant decl =
try
let params = List.map (nondep_type_rec env mid) decl.type_params in
let tk =
try match decl.type_kind with
Type_abstract ->
Type_abstract
| Type_variant cstrs ->
Type_variant
(List.map
(fun (c, tl) -> (c, List.map (nondep_type_rec env mid) tl))
cstrs)
| Type_record(lbls, rep) ->
Type_record
(List.map
(fun (c, mut, t) -> (c, mut, nondep_type_rec env mid t))
lbls,
rep)
with Not_found when is_covariant -> Type_abstract
and tm =
try match decl.type_manifest with
None -> None
| Some ty ->
Some (unroll_abbrev id params (nondep_type_rec env mid ty))
with Not_found when is_covariant ->
None
in
clear_hash ();
let priv =
match tm with
| Some ty when Btype.has_constr_row ty -> Private
| _ -> decl.type_private
in
{ type_params = params;
type_arity = decl.type_arity;
type_kind = tk;
type_manifest = tm;
type_private = priv;
type_variance = decl.type_variance;
}
with Not_found ->
clear_hash ();
raise Not_found
(* Preserve sharing inside class types. *)
let nondep_class_signature env id sign =
{ cty_self = nondep_type_rec env id sign.cty_self;
cty_vars =
Vars.map (function (m, v, t) -> (m, v, nondep_type_rec env id t))
sign.cty_vars;
cty_concr = sign.cty_concr;
cty_inher =
List.map (fun (p,tl) -> (p, List.map (nondep_type_rec env id) tl))
sign.cty_inher }
let rec nondep_class_type env id =
function
Tcty_constr (p, _, cty) when Path.isfree id p ->
nondep_class_type env id cty
| Tcty_constr (p, tyl, cty) ->
Tcty_constr (p, List.map (nondep_type_rec env id) tyl,
nondep_class_type env id cty)
| Tcty_signature sign ->
Tcty_signature (nondep_class_signature env id sign)
| Tcty_fun (l, ty, cty) ->
Tcty_fun (l, nondep_type_rec env id ty, nondep_class_type env id cty)
let nondep_class_declaration env id decl =
assert (not (Path.isfree id decl.cty_path));
let decl =
{ cty_params = List.map (nondep_type_rec env id) decl.cty_params;
cty_variance = decl.cty_variance;
cty_type = nondep_class_type env id decl.cty_type;
cty_path = decl.cty_path;
cty_new =
begin match decl.cty_new with
None -> None
| Some ty -> Some (nondep_type_rec env id ty)
end }
in
clear_hash ();
decl
let nondep_cltype_declaration env id decl =
assert (not (Path.isfree id decl.clty_path));
let decl =
{ clty_params = List.map (nondep_type_rec env id) decl.clty_params;
clty_variance = decl.clty_variance;
clty_type = nondep_class_type env id decl.clty_type;
clty_path = decl.clty_path }
in
clear_hash ();
decl
(* collapse conjonctive types in class parameters *)
let rec collapse_conj env visited ty =
let ty = repr ty in
if List.memq ty visited then () else
let visited = ty :: visited in
match ty.desc with
Tvariant row ->
let row = row_repr row in
List.iter
(fun (l,fi) ->
match row_field_repr fi with
Reither (c, t1::(_::_ as tl), m, e) ->
List.iter (unify env t1) tl;
set_row_field e (Reither (c, [t1], m, ref None))
| _ ->
())
row.row_fields;
iter_row (collapse_conj env visited) row
| _ ->
iter_type_expr (collapse_conj env visited) ty
let collapse_conj_params env params =
List.iter (collapse_conj env []) params
|