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

; ACL2 Version 3.1  A Computational Logic for Applicative Common Lisp
; Copyright (C) 2006 University of Texas at Austin
; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
; (C) 1997 Computational Logic, Inc. See the documentation topic NOTE20.
; This program is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.
; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; GNU General Public License for more details.
; You should have received a copy of the GNU General Public License
; along with this program; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
; Written by: Matt Kaufmann and J Strother Moore
; email: Kaufmann@cs.utexas.edu and Moore@cs.utexas.edu
; Department of Computer Sciences
; University of Texas at Austin
; Austin, TX 787121188 U.S.A.
(inpackage "ACL2")
; Our toplevel function for generating variables attempts to feed
; genvar roots that generate names suggestive of the term being
; replaced by the variable. We now develop the code for generating
; these roots. It involves a recursive descent through a term. At
; the bottom, we see variable symbols, e.g., ABC123, and we wish to
; generate the root '("ABC" . 124).
(defun stripfinaldigits1 (lst)
; See stripfinaldigits.
(cond ((null lst) (mv "" 0))
((member (car lst) '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9))
(mvlet (str n)
(stripfinaldigits1 (cdr lst))
(mv str (+ (let ((c (car lst)))
(case c
(#\0 0)
(#\1 1)
(#\2 2)
(#\3 3)
(#\4 4)
(#\5 5)
(#\6 6)
(#\7 7)
(#\8 8)
(otherwise 9)))
(* 10 n)))))
(t (mv (coerce (reverse lst) 'string) 0))))
(defun stripfinaldigits (str)
; Given a string, such as "ABC123", we strip off the final digits in it,
; and compute the number they represent. We return two things,
; the string and the number, e.g., "ABC" and 123.
(stripfinaldigits1 (reverse (coerce str 'list))))
; For nonvariable, nonquote terms we try first the idea of
; generating a name based on the type of the term. The following
; constant associates with selected type sets the names of some
; variables that we find pleasing and suggestive of the type. When we
; generalize a term we look at its type and if it is a subtype of one
; of those listed we prefer to use the variables given. The first
; variable in each family is additionally used as the root for a
; gensym, should it come to that. This list can be extended
; arbitarily without affecting soundness, as long as (a) the car of
; each pair below is a type set and (b) the cdr is a truelist of
; symbols. Arbitrary overlaps between the types and between the
; symbols are permitted.
;; RAG  I changed rational to real and complexrational to complex in
;; the list below, since the new types are supersets of the old types,
;; so it should be harmless.
(defconst *varfamiliesbytype*
(list (cons *tsinteger* '(I J K L M N))
(cons #+:nonstandardanalysis
*tsreal*
#:nonstandardanalysis
*tsrational*
'(R S I J K L M N))
(cons #+:nonstandardanalysis
*tscomplex*
#:nonstandardanalysis
*tscomplexrational*
'(Z R S I J K L M N))
(cons *tscons* '(L LST))
(cons *tsboolean* '(P Q R))
(cons *tssymbol* '(A B C D E))
(cons *tsstring* '(S STR))
(cons *tscharacter* '(C CH))))
; The following function is used to find the family of vars, given the
; type set of a term:
(defun assoctssubsetp (ts alist)
; Like assoc except we compare with tssubsetp.
(cond ((null alist) nil)
((tssubsetp ts (caar alist)) (car alist))
(t (assoctssubsetp ts (cdr alist)))))
; And here is how we look for an acceptable variable.
(defun firstnonmembereq (lst1 lst2)
; Return the first member of lst1 that is not a membereq of lst2.
(cond ((null lst1) nil)
((membereq (car lst1) lst2)
(firstnonmembereq (cdr lst1) lst2))
(t (car lst1))))
; If the above techniques don't lead to a choice we generate a string
; from the term by abbreviating the first symbol in the term. Here is
; how we abbreviate:
(defun abbreviatehyphenatedstring1 (str i maximum prevc)
; We return a list of characters that, when coerced to a string,
; abbreviates string str from position i to (but not including) maximum.
; Currently, it returns the first character after each block of "hyphens"
; and the last character. Thus, "PITONTEMPSTK" is abbreviated
; "PTSK".
; If prevchar is T it means we output the character we last saw.
; If prevchar is NIL it means the character we last saw was a "hyphen".
; Otherwise, prevchar is the previous character. "Hyphen" here means
; any one of several commonly used "word separators" in symbols.
; This function can be changed arbitrarily as long as it returns a
; list of characters.
(cond
((< i maximum)
(let ((c (char str i)))
(cond
((member c '(#\ #\_ #\. #\/ #\+))
(abbreviatehyphenatedstring1 str (1+ i) maximum nil))
((null prevc)
(cons c (abbreviatehyphenatedstring1 str (1+ i) maximum t)))
(t (abbreviatehyphenatedstring1 str (1+ i) maximum c)))))
((characterp prevc) (list prevc))
(t nil)))
(defun abbreviatehyphenatedstring (str)
; The function scans a string and collects the first and last character
; and every character immediately after a block of "hyphens" as defined
; above.
(let ((lst (abbreviatehyphenatedstring1 str 0 (length str) nil)))
(coerce
(cond ((or (null lst)
(member (car lst) *suspiciouslyfirstnumericchars*))
(cons #\V lst))
(t lst))
'string)))
; Just as stripfinaldigits produces the genvar root for a variable,
; the following function produces the genvar root for a nonvariable term.
(defun generatevariableroot1 (term avoidlst typealist ens wrld)
; Term is a nonvariable, nonquote term. This function returns two
; results, str and n, such that (str . n) is a "root" for genvar.
; In fact, it tries to return a root that when fed to genvar will
; create a variable symbol that is suggestive of term and which does
; not occur in avoidlst. But the function is correct as long as it
; returns any root, which could be any string.
(mvlet
(ts ttree)
(typeset term t nil typealist nil ens wrld nil nil nil)
; Note: We don't really know that the guards have been checked and we
; don't split on the 'assumptions we have forced. But our only use of
; type set here is heuristic. This also explains why we just use the
; global enabled structure and ignore the ttree.
(declare (ignore ttree))
(let* ((family (cdr (assoctssubsetp ts *varfamiliesbytype*)))
(var (firstnonmembereq family avoidlst)))
(cond (var
; If the type set of term is one of those for which we have a var family
; and some member of that family does not occur in avoidlst, then we will
; use the symbolname of var as the root from which to generate a
; variable symbol for term. This will almost certainly result in the
; generation of the symbol var by genvar. The only condition under which
; this won't happen is if var is an illegal variable symbol, in which case
; genvar will suffix it with some sufficiently large natural.
(mv (symbolname var) nil))
(family
; If we have a family for this type of term but all the members are
; to be avoided, we'll genvar from the first member of the family and
; we might as well start suffixing immediately (from 0) because we
; know the unsuffixed var is in avoidlst.
(mv (symbolname (car family)) 0))
(t
; Otherwise, we will genvar from an abbreviated version of the "first
; symbol" in term.
(mv (abbreviatehyphenatedstring
(symbolname
(cond ((variablep term) 'z) ; never happens
((fquotep term) 'z) ; never happens
((flambdaapplicationp term) 'z)
(t (ffnsymb term)))))
nil))))))
; And here we put them together with one last convention. The
; root for (CAR ...) is just the root for ..., except we force
; there to be a suffix. Thus, the root for (CAR X4) is going to be
; ("X" . 5).
(defun generatevariableroot (term avoidlst typealist ens wrld)
(cond
((variablep term)
(mvlet (str n)
(stripfinaldigits (symbolname term))
(mv str (1+ n))))
((fquotep term) (mv "CONST" 0))
((eq (ffnsymb term) 'car)
(mvlet (str n)
(generatevariableroot (fargn term 1) avoidlst typealist ens
wrld)
(mv str (or n 0))))
((eq (ffnsymb term) 'cdr)
(mvlet (str n)
(generatevariableroot (fargn term 1) avoidlst typealist ens
wrld)
(mv str (or n 0))))
(t (generatevariableroot1 term avoidlst typealist ens wrld))))
(defun generatevariable (term avoidlst typealist ens wrld)
; We generate a legal variable symbol that does not occur in avoidlst. We use
; term, typealist, ens, and wrld in a heuristic way to suggest a preferred
; name for the symbol. Generally speaking, the symbol we generate will be used
; to replace term in some conjecture, so we try to generate a symbol that we
; think "suggests" term.
(mvlet (str n)
(generatevariableroot term avoidlst typealist ens wrld)
(genvar (findpkgwitness term) str n avoidlst)))
(defun generatevariablelst (termlst avoidlst typealist ens wrld)
; And here we generate a list of variable names sequentially, one for
; each term in termlst.
(cond ((null termlst) nil)
(t
(let ((var (generatevariable (car termlst) avoidlst
typealist ens wrld)))
(cons var (generatevariablelst (cdr termlst)
(cons var avoidlst)
typealist ens wrld))))))
; That completes the code for generating new variable names.
; An elimrule, as declared below, denotes a theorem of the form
; (implies hyps (equal lhs rhs)), where rhs is a variable symbol and
; lhs involves the terms destructorterms, each of which is of the
; form (dfn v1 ... vn), where the vi are distinct variables and {v1
; ... vn} are all the variables in the formula. We call rhs the
; "crucial variable". It is the one we will "puff up" to eliminate
; the destructor terms. For example, in (CONSP X) > (CONS (CAR X)
; (CDR X)) = X, X is the crucial variable and puffing it up to (CONS A
; B) we can eliminate (CAR X) and (CDR X). We store an elimrule
; under the function symbol, dfn, of each destructor term. The rule
; we store for (dfn v1 ... vn) has that term as the car of destructor
; terms and has crucialposition j where (nth j '(v1 ... vn)) = rhs.
; (Thus, the crucialposition is the position in the args at which the
; crucial variable occurs and for these purposes we enumerate the args
; from 0 (as by nth) rather than from 1 (as by fargn).)
(defrec elimrule
(((nume . crucialposition) . (destructorterm . destructorterms))
(hyps . equiv)
(lhs . rhs)
. rune) nil)
(defun occursnowhereelse (var args c i)
; Index the elements of args starting at i. Scan all args except the
; one with index c and return nil if var occurs in one of them and t
; otherwise.
(cond ((null args) t)
((int= c i)
(occursnowhereelse var (cdr args) c (1+ i)))
((dumboccur var (car args)) nil)
(t (occursnowhereelse var (cdr args) c (1+ i)))))
(defun firstnomination (term votes nominations)
; See nominatedestructorcandidate for an explanation.
(cons (cons term (cons term votes))
nominations))
(defun secondnomination (term votes nominations)
; See nominatedestructorcandidate for an explanation.
(cond ((null nominations) nil)
((equal term (car (car nominations)))
(cons (cons term
(unionequal votes (cdr (car nominations))))
(cdr nominations)))
(t (cons (car nominations)
(secondnomination term votes (cdr nominations))))))
(defun somehypprobablynilp (hyps typealist ens wrld)
; The name of this function is meant to limit its use to heuristics.
; In fact, if this function says some hyp is probably nil then in fact
; some hyp is known to be nil under the given typealist, wrld and
; some forced 'assumptions.
; Since the function actually ignores 'assumptions generated, its use
; must be limited to heuristic situations. When it says "yes, some
; hyp is probably nil" we choose not to pursue the establishment of
; those hyps.
(cond
((null hyps) nil)
(t (mvlet
(knownp nilp ttree)
(knownwhethernil
(car hyps) typealist ens (oktoforceens ens) wrld nil)
(declare (ignore ttree))
(cond ((and knownp nilp) t)
(t (somehypprobablynilp (cdr hyps) typealist ens wrld)))))))
(mutualrecursion
(defun sublisexpr (alist term)
; Alist is of the form ((a1 . b1) ... (ak . bk)) where the ai and bi are
; all terms. We substitute bi for each occurrence of ai in term.
; Thus, if the ai are distinct variables, this function is equivalent to
; sublisvar. We do not look for ai's properly inside of quoted objects.
; Thus,
; (sublisexpr '(('3 . x)) '(f '3)) = '(f x)
; but
; (sublisexpr '(('3 . x)) '(f '(3 . 4))) = '(f '(3 . 4)).
(let ((temp (assocequal term alist)))
(cond (temp (cdr temp))
((variablep term) term)
((fquotep term) term)
(t (consterm (ffnsymb term)
(sublisexprlst alist (fargs term)))))))
(defun sublisexprlst (alist lst)
(cond ((null lst) nil)
(t (cons (sublisexpr alist (car lst))
(sublisexprlst alist (cdr lst))))))
)
(defun nominatedestructorcandidate
(term eliminables typealist clause ens wrld votes nominations)
; This function recognizes candidates for destructor elimination. It
; is assumed that term is a nonvariable, nonquotep term. To be a
; candidate the term must not be a lambda application and the function
; symbol of the term must have an enabled destructor elimination rule.
; Furthermore, the crucial argument position of the term must be
; occupied by a variable symbol that is a member of the eliminables,
; that occurs only in equivhittable positions within the clause,
; and that occurs nowhere else in the arguments of the term, or else
; the crucial argument position must be occupied by a term that itself
; is recursively a candidate. (Note that if the crucial argument is
; an eliminable term then when we eliminate it we will introduce a
; suitable distinct var into the crucial argument of this term and
; hence it will be eliminable.) Finally, the instantiated hypotheses
; of the destructor elimination rule must not be known nil under the
; typealist.
; Votes and nominations are accumulators. Votes is a list of terms
; that contain term and will be candidates if term is eliminated.
; Nominations are explained below.
; If term is a candidate we either "nominate" it, by adding a
; "nomination" for term to the running accumulator nominations, or
; else we "second" a prior nomination for it. A nomination of a term
; is a list of the form (dterm . votes) where dterm is the innermost
; eliminable candidate in term and votes is a list of all the terms
; that will be eliminable if dterm is eliminated. To "second" a
; nomination is simply to add yourself as a vote.
; For example, if X is eliminable then (CAR (CAR (CAR X))) is a
; candidate. If nominations is initially nil then at the conclusion
; of this function it will be
; (((CAR X) (CAR X) (CAR (CAR X)) (CAR (CAR (CAR X))))).
; We always return a nominations list.
(cond
((flambdaapplicationp term) nominations)
(t (let ((rule (getprop (ffnsymb term) 'eliminatedestructorsrule
nil 'currentacl2world wrld)))
(cond
((or (null rule)
(not (enablednumep (access elimrule rule :nume) ens)))
nominations)
(t (let ((crucialarg (nth (access elimrule rule :crucialposition)
(fargs term))))
(cond
((variablep crucialarg)
; Next we wish to determine that every occurrence of the crucial
; argument  outside of the destructor nests themselves  is equiv
; hittable. For example, for carcdrelim, where we have A as the
; crucial arg (meaning term, above, is (CAR A) or (CDR A)), we wish to
; determine that every A in the clause is equalhittable, except those
; A's occurring inside the (CAR A) and (CDR A) destructors. Suppose
; the clause is p(A,(CAR A),(CDR A)). The logical explanation of what
; elim does is to replace the A's not in the destructor nests by (CONS
; (CAR A) (CDR A)) and then generalize (CAR A) to HD and (CDR A) to
; TL. This will produce p((CONS HD TL), HD, TL). Observe that we do
; not actually hit the A's inside the CAR and CDR. So we do not
; require that they be equivhittable. (This situation actually
; arises in the elim rule for sets, where equiv tests equality on the
; canonicalizations. In this setting, equiv is not a congruence for
; the destructors.) So the question then is how do we detect that all
; the ``naked'' A's are equivhittable? We ``ought'' to generalize
; away the instantiated destructor terms and then ask whether all the
; A's are equivhittable. But we do not want to pay the price of
; generating n distinct new variable symbols. So we just replace
; every destructor term by NIL. This creates a ``pseudoclause;'' the
; ``terms'' in it are not really legal  NIL is not a variable
; symbol. We only use this pseudoclause to answer the question of
; whether the crucial variable, which certainly isn't NIL, is
; equivhittable in every occurrence.
(let* ((alist (pairlis$
(fargs
(access elimrule rule :destructorterm))
(fargs term)))
(instdestructors
(sublisvarlst
alist
(cons (access elimrule rule :destructorterm)
(access elimrule rule :destructorterms))))
(pseudoclause (sublisexprlst
(pairlis$ instdestructors nil)
clause)))
(cond
((not (everyoccurrenceequivhittablepinclausep
(access elimrule rule :equiv)
crucialarg
pseudoclause ens wrld))
nominations)
((assocequal term nominations)
(secondnomination term votes nominations))
((member crucialarg eliminables)
(cond
((occursnowhereelse crucialarg
(fargs term)
(access elimrule rule
:crucialposition)
0)
(let* ((insthyps
(sublisvarlst alist
(access elimrule rule :hyps))))
(cond
((somehypprobablynilp insthyps
typealist ens wrld)
nominations)
(t (firstnomination term votes nominations)))))
(t nominations)))
(t nominations))))
(t (nominatedestructorcandidate crucialarg
eliminables
typealist
clause
ens
wrld
(cons term votes)
nominations))))))))))
(mutualrecursion
(defun nominatedestructorcandidates
(term eliminables typealist clause ens wrld nominations)
; We explore term and accumulate onto nominations all the nominations.
(cond ((variablep term) nominations)
((fquotep term) nominations)
(t (nominatedestructorcandidateslst
(fargs term)
eliminables
typealist
clause
ens
wrld
(nominatedestructorcandidate term
eliminables
typealist
clause
ens
wrld
nil
nominations)))))
(defun nominatedestructorcandidateslst
(terms eliminables typealist clause ens wrld nominations)
(cond ((null terms) nominations)
(t (nominatedestructorcandidateslst
(cdr terms)
eliminables
typealist
clause
ens
wrld
(nominatedestructorcandidates (car terms)
eliminables
typealist
clause
ens
wrld
nominations)))))
)
; We next turn to the problem of choosing which candidate we will eliminate.
; We want to eliminate the most complicated one. We measure them with
; maxlevelno, which is also used by the defuns principle to store the
; levelno of each fn. Maxlevelno was originally defined here, but it is
; mutually recursive with getlevelno, a function we call earlier in the ACL2
; sources, in sortapproved1rating1.
(defun sumlevelnos (lst wrld)
; Lst is a list of nonvariable, nonquotep terms. We sum the
; levelno of the function symbols of the terms. For the level no of
; a lambda expression we use the max level no of its body, just as
; would be done if a nonrecursive function with the same body were
; being applied.
(cond ((null lst) 0)
(t (+ (if (flambdaapplicationp (car lst))
(maxlevelno (lambdabody (ffnsymb (car lst))) wrld)
(or (getprop (ffnsymb (car lst)) 'levelno
nil 'currentacl2world wrld)
0))
(sumlevelnos (cdr lst) wrld)))))
(defun pickhighestsumlevelnos (nominations wrld dterm maxscore)
; Nominations is a list of pairs of the form (dterm . votes), where
; votes is a list of terms. The "score" of a dterm is the
; sumlevelnos of its votes. We scan nominations and return a dterm
; with maximal score, assuming that dterm and maxscore are the
; winning dterm and its score seen so far.
(cond
((null nominations) dterm)
(t (let ((score (sumlevelnos (cdr (car nominations)) wrld)))
(cond
((> score maxscore)
(pickhighestsumlevelnos (cdr nominations) wrld
(caar nominations) score))
(t
(pickhighestsumlevelnos (cdr nominations) wrld
dterm maxscore)))))))
(defun selectinstantiatedelimrule (clause typealist eliminables ens wrld)
; Clause is a clause to which we wish to apply destructor elimination.
; Typealist is the typealist obtained by assuming all literals of cl nil.
; Eliminables is the list of legal "crucial variables" which can be
; "puffed up" to do an elim. For example, to eliminate (CAR X), X
; must be puffed up to (CONS A B). X is the crucial variable in (CAR
; X). Upon entry to the destructor elimination process we consider
; all the variables eliminable (except the ones historically
; introduced by elim). But once we get going within the elim process,
; the only eliminable variables are the ones we introduce ourselves
; (because they won't be eliminable by subsequent processes since they
; were introduced by elim).
; If there is at least one nomination for an elim, we choose the one
; with maximal score and return an instantiated version of the
; elimrule corresponding to it. Otherwise we return nil.
(let ((nominations
(nominatedestructorcandidateslst clause
eliminables
typealist
clause
ens
wrld
nil)))
(cond
((null nominations) nil)
(t
(let* ((dterm (pickhighestsumlevelnos nominations wrld nil 1))
(rule (getprop (ffnsymb dterm) 'eliminatedestructorsrule
nil 'currentacl2world wrld))
(alist (pairlis$ (fargs (access elimrule rule :destructorterm))
(fargs dterm))))
(change elimrule rule
:hyps (sublisvarlst alist (access elimrule rule :hyps))
:lhs (sublisvar alist (access elimrule rule :lhs))
:rhs (sublisvar alist (access elimrule rule :rhs))
:destructorterm
(sublisvar alist (access elimrule rule :destructorterm))
:destructorterms
(sublisvarlst
alist
(access elimrule rule :destructorterms))))))))
; We now take a break from elim and develop the code for the
; generalization that elim uses. We want to be able to replace terms
; by variables (sublisexpr, above), we want to be able to restrict
; the new variables by noting typesets of the terms replaced, and we
; want to be able to use generalization rules provided in the data
; base.
; We now develop the function that converts a typeset into a term.
(defrec typesetinverterrule ((nume . ts) terms . rune) nil)
; A typesetinverterrule states that x has typeset ts iff the conjunction of
; terms{X/x} is true. Thus, for example, if :ts is *tsinteger* then :terms is
; '((INTEGERP X)).
; WARNING: See the warning in converttypesettoterm if you are ever
; tempted to generalize typesetinverterrules to allow hypotheses that
; may be FORCEd or CASESPLITd!
; A typeset, s, is a disjunction of the individual bits in it. Thus, to
; create a term whose truth is equivalent to the claim that X has typeset s it
; is sufficient to find any typesetinverterrule whose :ts is a subset of s
; and then disjoin the :term of that rule to the result of recursively creating
; the term recognizing s minus :ts. This assumes one has a rule for each
; single type bit.
; The following is the initial setting of the world global variable
; 'typesetinverterrules. WARNING: EACH TERM IN :TERMS MUST BE IN TRANSLATED
; FORM. The list is ordered in an important way: the larger typesets are at
; the front. This ordering is exploited by converttypesettotermlst which
; operates by finding the largest recognized type set group and knocks it out
; of the type set.
;; RAG  I added a rule for realp, nonzero real, nonnegative real,
;; nonpositive real, positive real, negative real, irrational,
;; negative irrational, positive irrational, and complex.
(defconst *initialtypesetinverterrules*
(list (make typesetinverterrule ;;; 11 (14) bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts (tscomplement *tscons*)
:terms '((atom x)))
(make typesetinverterrule ;;; 6 (9) bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsacl2number*
:terms '((acl2numberp x)))
#+:nonstandardanalysis
(make typesetinverterrule ;;; _ (7) bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsreal*
:terms '((realp x)))
(make typesetinverterrule ;;; 5 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsrational*
:terms '((rationalp x)))
(make typesetinverterrule ;;; 5 (8) bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts (tsintersection *tsacl2number* (tscomplement *tszero*))
:terms '((acl2numberp x) (not (equal x '0))))
#+:nonstandardanalysis
(make typesetinverterrule ;;; _ (6) bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts (tsintersection *tsreal* (tscomplement *tszero*))
:terms '((realp x) (not (equal x '0))))
(make typesetinverterrule ;;; 4 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts (tsintersection *tsrational* (tscomplement *tszero*))
:terms '((rationalp x) (not (equal x '0))))
#+:nonstandardanalysis
(make typesetinverterrule ;;; _ (4) bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts (tsunion *tspositivereal* *tszero*)
:terms '((realp x) (not (< x '0))))
(make typesetinverterrule ;;; 3 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts (tsunion *tspositiverational* *tszero*)
:terms '((rationalp x) (not (< x '0))))
#+:nonstandardanalysis
(make typesetinverterrule ;;; _ (4) bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts (tsunion *tsnegativereal* *tszero*)
:terms '((realp x) (not (< '0 x))))
(make typesetinverterrule ;;; 3 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts (tsunion *tsnegativerational* *tszero*)
:terms '((rationalp x) (not (< '0 x))))
(make typesetinverterrule ;;; 3 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsinteger*
:terms'((integerp x)))
(make typesetinverterrule ;;; 2 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts (tsintersection *tsinteger* (tscomplement *tszero*))
:terms '((integerp x) (not (equal x '0))))
#+:nonstandardanalysis
(make typesetinverterrule ;;; _ (3) bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tspositivereal*
:terms'((realp x) (< '0 x)))
(make typesetinverterrule ;;; 2 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tspositiverational*
:terms'((rationalp x) (< '0 x)))
#+:nonstandardanalysis
(make typesetinverterrule ;;; _ (3) bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsnegativereal*
:terms'((realp x) (< x '0)))
(make typesetinverterrule ;;; 2 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsnegativerational*
:terms'((rationalp x) (< x '0)))
(make typesetinverterrule ;;; 2 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts (tsunion *tspositiveinteger* *tszero*)
:terms '((integerp x) (not (< x '0))))
(make typesetinverterrule ;;; 2 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts (tsunion *tsnegativeinteger* *tszero*)
:terms '((integerp x) (not (< '0 x))))
#+:nonstandardanalysis
(make typesetinverterrule ;;; _ (2) bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsnonratio*
:terms'((realp x) (not (rationalp x))))
(make typesetinverterrule ;;; 2 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsratio*
:terms'((rationalp x) (not (integerp x))))
#+:nonstandardanalysis
(make typesetinverterrule ;;; _ (1) bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsnegativenonratio*
:terms'((realp x) (not (rationalp x)) (< x '0)))
(make typesetinverterrule ;;; 1 bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsnegativeratio*
:terms'((rationalp x) (not (integerp x)) (< x '0)))
(make typesetinverterrule ;;; 1 bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsnegativeinteger*
:terms'((integerp x) (< x '0)))
#+:nonstandardanalysis
(make typesetinverterrule ;;; _ (1) bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tspositivenonratio*
:terms'((realp x) (not (rationalp x)) (< '0 x)))
(make typesetinverterrule ;;; 1 bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tspositiveratio*
:terms'((rationalp x) (not (integerp x)) (< '0 x)))
(make typesetinverterrule ;;; 1 bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tspositiveinteger*
:terms'((integerp x) (< '0 x)))
#+:nonstandardanalysis
(make typesetinverterrule ;;; _ (2) bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tscomplex*
:terms'((complexp x)))
(make typesetinverterrule ;;; 1 bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tscomplexrational*
:terms'((complexrationalp x)))
#+:nonstandardanalysis
(make typesetinverterrule ;;; _ (1) bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tscomplexnonrational*
:terms'((complexp x) (not (complexrationalp x))))
(make typesetinverterrule ;;; 1 bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tszero*
:terms'((equal x '0)))
(make typesetinverterrule ;;; 3 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tssymbol*
:terms'((symbolp x)))
(make typesetinverterrule ;;;2 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsboolean*
:terms'((if (equal x 't) 't (equal x 'nil))))
(make typesetinverterrule ;;; 2 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tscons*
:terms'((consp x)))
(make typesetinverterrule ;;; 2 bits
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tstruelist*
:terms'((truelistp x)))
(make typesetinverterrule ;;; 1 bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsimpropercons*
:terms'((consp x) (not (truelistp x))))
(make typesetinverterrule ;;; 1 bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tspropercons*
:terms'((consp x) (truelistp x)))
(make typesetinverterrule ;;; 1 bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsnontnonnilsymbol*
:terms '((symbolp x) (not (equal x 't)) (not (equal x 'nil))))
(make typesetinverterrule ;;; 1 bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tst*
:terms'((equal x 't)))
(make typesetinverterrule ;;; 1 bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsnil*
:terms'((equal x 'nil)))
(make typesetinverterrule ;;; 1 bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tsstring*
:terms'((stringp x)))
(make typesetinverterrule ;;; 1 bit
:nume nil
:rune *fakeruneforanonymousenabledrule*
:ts *tscharacter*
:terms'((characterp x)))))
(defun converttypesettotermlst (ts rules ens lst ttree)
; We map over the list of typesetinverter rules and each time we find an
; enabled rule whose :ts is a subset of ts, we accumulate its conjoined :terms
; and its :rune, and knock off those bits of ts. We return (mv lst ttree),
; where lst is a list of terms in the variable X whose disjunction is
; equivalent to ts.
(cond
((null rules) (mv (reverse lst) ttree))
((and (enablednumep (access typesetinverterrule (car rules) :nume) ens)
(ts= (access typesetinverterrule (car rules) :ts)
(tsintersection
(access typesetinverterrule (car rules) :ts)
ts)))
(converttypesettotermlst
(tsintersection
ts
(tscomplement (access typesetinverterrule (car rules) :ts)))
(cdr rules)
ens
(addtosetequal
(conjoin (access typesetinverterrule (car rules) :terms))
lst)
(pushlemma (access typesetinverterrule (car rules) :rune)
ttree)))
(t (converttypesettotermlst ts (cdr rules) ens lst ttree))))
(defun converttypesettoterm (x ts ens w ttree)
; Given a term x and a type set ts we generate a term that expresses the
; assertion that "x has type set ts". E.g., if x is the term (FN X Y) and ts
; is *tsrational* then our output will be (RATIONALP (FN X Y)). We return (mv
; term ttree), where term is the term and ttree contains the 'lemmas used. We
; do not use disabled typesetinverters.
; Note: It would be a major change to make this function force assumptions.
; If the returned ttree contains 'assumption tags then the primary use of
; this function, namely the expression of typealists in clausal form so that
; assumptions can be attacked as clauses, becomes problematic. Don't glibbly
; generalize typesetinverter rules to force assumptions.
(cond ((ts= ts *tsunknown*) (mv *t* ttree))
((and (ts= ts *tst*)
(tsbooleanp x ens w))
(mv x ttree))
((tscomplementp ts)
(mvlet (lst ttree)
(converttypesettotermlst
(tscomplement ts)
(globalval 'typesetinverterrules w)
ens nil ttree)
(mv (substvar x 'x
(conjoin (dumbnegatelitlst lst)))
ttree)))
(t (mvlet (lst ttree)
(converttypesettotermlst
ts
(globalval 'typesetinverterrules w)
ens nil ttree)
(mv (substvar x 'x (disjoin lst)) ttree)))))
(defun typerestrictionsegment (cl terms vars typealist ens wrld)
; Cl is a clause. Terms is a list of terms and is in 1:1
; correspondence with vars, which is a list of vars. Typealist is
; the result of assuming false every literal of cl. This function
; returns three results. The first is a list of literals that can be
; disjoined to cl without altering the validity of cl. The second is
; a subset of vars. The third is an extension of ttree. Technically
; speaking, this function may return any list of terms with the
; property that every term in it is false (under the assumptions in
; typealist) and any subset of vars, provided the ttree returned is
; an extension of ttree and justifies the falsity of the terms
; returned. The final ttree must be 'assumptionfree and is if the
; initial ttree is also.
; As for motivation, we are about to generalize cl by replacing each
; term in terms by the corresponding var in vars. It is sound, of
; course, to restrict the new variable to have whatever properties the
; corresponding term has. This function is responsible for selecting
; the restrictions we want to place on each variable, based on
; typeset reasoning alone. Thus, if t is known to have properties h1
; & ... & hk, then we can include (not h1), ..., (not hk) in our first
; answer to restrict the variable introduced for t. We will include
; the corresponding var in our second answer to indicate that we have
; a type restriction on that variable.
; We do not want our type restrictions to cause the new clause to
; explode into cases. Therefore, we adopt the following heuristic.
; We convert the type set of each term t into a term (hyp t) known to
; be true of t. We negate (hyp t) and clausify the result. If that
; produces a single clause (segment) then that segment is added to our
; answer. Otherwise, we add no restriction. There are probably
; better ways to do this than to call the fullblown
; converttypesettoterm and clausify. But this is simple, elegant,
; and lets us take advantage of improvements to those two utilities.
(cond
((null terms) (mv nil nil nil))
(t
(mvlet
(ts ttree1)
(typeset (car terms) nil nil typealist nil ens wrld nil
nil nil)
(mvlet
(term ttree1)
(converttypesettoterm (car terms) ts ens wrld ttree1)
(let ((clauses (clausify (dumbnegatelit term) nil t wrld)))
(mvlet
(lits restrictedvars ttree)
(typerestrictionsegment cl
(cdr terms)
(cdr vars)
typealist ens wrld)
(cond ((null clauses)
; If the negation of the type restriction term clausifies to the empty set
; of clauses, then the term is nil. Since we get to assume it, we're done.
; But this can only happen if the typeset of the term is empty. We don't think
; this will happen, but we test for it nonetheless, and toss a nil hypothesis
; into our answer literals if it happens.
(mv (addtosetequal *nil* lits)
(cons (car vars) restrictedvars)
(constagtrees ttree1 ttree)))
((and (null (cdr clauses))
(not (null (car clauses))))
; If there is only one clause and it is not the empty clause, we'll
; assume everything in it. (If the clausify above produced '(NIL)
; then the type restriction was just *t* and we ignore it.) It is
; possible that the literals we are about to assume are already in cl.
; If so, we are not fooled into thinking we've restricted the new var.
(cond
((subsetpequal (car clauses) cl)
(mv lits restrictedvars ttree))
(t (mv (disjoinclauses (car clauses) lits)
(cons (car vars) restrictedvars)
(constagtrees ttree1 ttree)))))
(t
; There may be useful type information we could extract, but we don't.
; It is always sound to exit here, giving ourselves no additional
; assumptions.
(mv lits restrictedvars ttree))))))))))
(mutualrecursion
(defun subtermonewayunify (pat term)
; This function searches pat for a nonvariable nonquote subterm s such that
; (onewayunify s term) returns t and a unifysubst. If it finds one, it
; returns t and the unifysubst. Otherwise, it returns two nils.
(cond ((variablep pat) (mv nil nil))
((fquotep pat) (mv nil nil))
(t (mvlet (ans alist)
(onewayunify pat term)
(cond (ans (mv ans alist))
(t (subtermonewayunifylst (fargs pat) term)))))))
(defun subtermonewayunifylst (patlst term)
(cond
((null patlst) (mv nil nil))
(t (mvlet (ans alist)
(subtermonewayunify (car patlst) term)
(cond (ans (mv ans alist))
(t (subtermonewayunifylst (cdr patlst) term)))))))
)
(defrec generalizerule (nume formula . rune) nil)
(defun applygeneralizerule (genrule term ens)
; Genrule is a generalization rule, and hence has a name and a
; formula component. Term is a term which we are intending to
; generalize by replacing it with a new variable. We return two
; results. The first is either t or nil indicating whether genrule
; provides a useful restriction on the generalization of term. If the
; first result is nil, so is the second. Otherwise, the second result
; is an instantiation of the formula of genrule in which term appears.
; Our heuristic for deciding whether to use genrule is: (a) the rule
; must be enabled, (b) term must unify with a nonvariable subterm of
; the formula of the rule, (c) the unifying substitution must leave no
; free vars in that formula, and (d) the function symbol of term must
; not occur in the instantiation of the formula except in the
; occurrences of term itself.
(cond
((not (enablednumep (access generalizerule genrule :nume) ens))
(mv nil nil))
(t (mvlet
(ans unifysubst)
(subtermonewayunify (access generalizerule genrule :formula)
term)
(cond
((null ans)
(mv nil nil))
((freevarsp (access generalizerule genrule :formula)
unifysubst)
(mv nil nil))
(t (let ((instformula (sublisvar unifysubst
(access generalizerule
genrule
:formula))))
(cond ((ffnnamep (ffnsymb term)
(substexpr 'x term instformula))
(mv nil nil))
(t (mv t instformula))))))))))
(defun generalizerulesegment1 (generalizerules term ens)
; Given a list of :GENERALIZE rules and a term we return two results:
; the list of instantiated negated formulas of those applicable rules
; and the runes of all applicable rules. The former list is suitable
; for splicing into a clause to add the formulas as hypotheses.
(cond
((null generalizerules) (mv nil nil))
(t (mvlet (ans formula)
(applygeneralizerule (car generalizerules) term ens)
(mvlet (formulas runes)
(generalizerulesegment1 (cdr generalizerules)
term ens)
(cond (ans (mv (addliteral (dumbnegatelit formula)
formulas nil)
(cons (access generalizerule
(car generalizerules)
:rune)
runes)))
(t (mv formulas runes))))))))
(defun generalizerulesegment (terms vars ens wrld)
; Given a list of terms and a list of vars in 1:1 correspondence, we
; return two results. The first is a clause segment containing the
; instantiated negated formulas derived from every applicable
; :GENERALIZE rule for each term in terms. This segment can be spliced
; into a clause to restrict the range of a generalization of terms.
; The second answer is an alist pairing some of the vars in vars to
; the runes of all :GENERALIZE rules in wrld that are applicable to the
; corresponding term in terms. The second answer is of interest only
; to output routines.
(cond
((null terms) (mv nil nil))
(t (mvlet (segment1 runes1)
(generalizerulesegment1 (globalval 'generalizerules wrld)
(car terms) ens)
(mvlet (segment2 alist)
(generalizerulesegment (cdr terms) (cdr vars) ens wrld)
(cond
((null runes1) (mv segment2 alist))
(t (mv (disjoinclauses segment1 segment2)
(cons (cons (car vars) runes1) alist)))))))))
(defun generalize1 (cl typealist terms vars ens wrld)
; Cl is a clause. Typealist is a typealist obtained by assuming all
; literals of cl false. Terms and vars are lists of terms and
; variables, respectively, in 1:1 correspondence. We assume no var in
; vars occurs in cl. We generalize cl by substituting vars for the
; corresponding terms. We restrict the variables by using typeset
; information about the terms and by using :GENERALIZE rules in wrld.
; We return four results. The first is the new clause. The second
; is a list of the variables for which we added type restrictions.
; The third is an alist pairing some variables with the runes of
; generalization rules used to restrict them. The fourth is a ttree
; justifying our work; it is 'assumptionfree.
(mvlet (trseg restrictedvars ttree)
(typerestrictionsegment cl terms vars typealist ens wrld)
(mvlet (grseg alist)
(generalizerulesegment terms vars ens wrld)
(mv (sublisexprlst (pairlis$ terms vars)
(disjoinclauses trseg
(disjoinclauses grseg
cl)))
restrictedvars
alist
ttree))))
; This completes our brief flirtation with generalization. We now
; have enough machinery to finish coding destructor elimination.
; However, it might be noted that generalize1 is the main subroutine
; of the generalizeclause waterfall processor.
(defun applyinstantiatedelimrule (rule cl typealist avoidvars ens wrld)
; This function takes an instantiated elimrule, rule, and applies it
; to a clause cl. Avoidvars is a list of variable names to avoid
; when we generate new ones. See eliminatedestructorsclause for
; an explanation of that.
; An instantiated :ELIM rule has hyps, lhs, rhs, and destructorterms,
; all instantiated so that the car of the destructor terms occurs
; somewhere in the clause. To apply such an instantiated :ELIM rule to
; a clause we assume the hyps (adding their negations to cl), we
; generalize away the destructor terms occurring in the clause and in
; the lhs of the rule, and then we substitute that generalized lhs for
; the rhs into the generalized cl to obtain the final clause. The
; generalization step above may involve adding additional hypotheses
; to the clause and using generalization rules in wrld.
; We return four things. The first is contradictionp, a flag which
; indicates whether the instantiated hyps are all true under the
; typealist. The second is the clause described above, which implies
; cl when the hyps of the rule are known to be true, the third is the
; set of elim variables we have just introduced into it, and the
; fourth is a list describing this application of the rune of the
; rule, as explained below.
; The list returned as the fourth value will become an element in the
; 'elimsequence list in the ttree of the history entry for this
; elimination process. The "elimsequence element" we return has the
; form:
; (rune rhs lhs alist restrictedvars vartorunesalist ttree)
; and means "use rune to replace rhs by lhs, generalizing as specified
; by alist (which maps destructors to variables), restricting the
; restrictedvars variables by type (as justified by ttree) and
; restricting the vartorunesalist variables by the named generalize
; rules." The ttree is 'assumptionfree.
(let* ((rune (access elimrule rule :rune))
(hyps (access elimrule rule :hyps))
(lhs (access elimrule rule :lhs))
(rhs (access elimrule rule :rhs))
(dests (access elimrule rule :destructorterms))
(negatedhyps (dumbnegatelitlst hyps)))
(mvlet
(contradictionp typealist0 ttree0)
(typealistclause negatedhyps nil nil typealist ens wrld
nil nil)
; Before Version_2.9.3, we just punted when contradictionp is true
; here, and this led to infinite loops reported by Sol Swords and then
; (shortly thereafter) Doug Harper, who both sent examples. Our
; initial fix was to punt without going into the infinite loop, but
; then we implemented the current scheme in which we simply perform
; the elimination without generating clauses for the impossible
; "pathological" cases corresponding to falsity of each of the
; instantiated :elim rule's hypotheses. Both fixes avoid the infinite
; loop in both examples, but the present fix actually proves the
; latter example (shown here) without induction:
; (includebook "ihs/@logops" :dir :system)
; (thm (implies (integerp (* 1/2 n)) (equal (mod n 2) 0)))
(let* ((clwithhyps (if contradictionp
cl
(disjoinclauses negatedhyps cl)))
(typealist (if contradictionp
typealist
typealist0))
(elimvars (generatevariablelst dests
(allvars1lst clwithhyps
avoidvars)
typealist ens wrld)))
(mvlet (generalizedclwithhyps
restrictedvars
vartorunesalist
ttree)
(generalize1 clwithhyps typealist dests elimvars ens wrld)
(let* ((alist (pairlis$ dests elimvars))
(generalizedlhs (sublisexpr alist lhs))
(finalcl
(substvarlst generalizedlhs
rhs
generalizedclwithhyps))
(actualelimvars
(intersectioneq elimvars
(allvars1lst finalcl nil))))
(mv contradictionp
finalcl
actualelimvars
(list rune rhs generalizedlhs alist
restrictedvars
vartorunesalist
(constagtrees ttree0 ttree)))))))))
(defun eliminatedestructorsclause1
(cl eliminables avoidvars ens wrld topflg)
; Cl is a clause we are trying to prove. Eliminables is the set of
; variables on which we will permit a destructor elimination.
; Avoidvars is a list of variable names we are to avoid when
; generating new names. In addition, we avoid the variables in cl.
; We look for an eliminable destructor, select the highest scoring one
; and get its instantiated rule, split on the hyps of that rule to
; produce a "pathological" case of cl for each hyp and apply the rule
; to cl to produce the "normal" elim case. Then we iterate until
; there is nothing more to eliminate.
; The handling of the eliminables needs explanation however. At the
; toplevel (when topflg is t) eliminables is the set of all
; variables occurring in cl except those historically introduced by
; destructor elimination. It is with respect to that set that we
; select our first elimination rule. Thereafter (when topflg is nil)
; the set of eliminables is always just the set of variables we have
; introduced into the clauses. We permit these variables to be
; eliminated by this elim and this elim only. For example, the
; toplevel entry might permit elimination of (CAR X) and of (CAR Y).
; Suppose we choose X, introducing A and B. Then on the second
; iteration, we'll allow eliminations of A and B, but not of Y.
; We return three things. The first is a set of clauses to prove
; instead of cl. The second is the set of variable names introduced
; by this destructor elimination step. The third is an "elimsequence
; list" that documents this step. If the list is nil, it means we did
; nothing. Otherwise it is a list, in order, of the "elimsequence
; elements" described in applyinstantiatedelimrule above. This list
; should become the 'elimsequence entry in the ttree for this elim
; process.
; Historical Remark on Nqthm.
; This code is spiritually very similar to that of Nqthm. However, it
; is much more elegant and easy to understand. Nqthm managed the
; "iteration" with a "todo" list which grew and then shrank. In
; addition, while we select the best rule on each round from scratch,
; Nqthm kept an ordered list of candidates (which it culled
; appropriately when eliminations removed some of them from the clause
; or when the crucial variables were no longer among eliminables).
; Finally, and most obscurely, Nqthm used an incrutable test on the
; "process history" (related to our elimsequence) and a subtle
; invariant about the candidates to switch from our topflg t mode to
; topflg nil mode. We have spent about a week coding destructor
; elimination in ACL2 and we have thrown away more code that we have
; kept as we at first transcribed and then repeatedly refined the
; Nqthm code. We are much happier with the current code than Nqthm's
; and believe it will be much easier to modify in the future. Oh, one
; last remark: Nqthm's destructor elimination code had almost no
; comments and everything was done in a single big function with lots
; of ITERATEs. It is no wonder it was so hard to decode.
; Our first step is to get the typealist of cl. It is used in two
; different ways: to identify contradictory hypotheses of candidate
; :ELIM lemmas and to generate names for new variables.
(mvlet
(contradictionp typealist ttree)
(typealistclause cl nil t nil ens wrld
nil nil)
(declare (ignore ttree))
(cond
(contradictionp
; This is unusual. We don't really expect to find a contradiction
; here. We'll return an answer indicating that we didn't do anything.
; We ignore the possibly nonnil ttree here, which is valid given that
; we are returning the same goal clause rather than actually relying
; on the contradiction. We thus ignore ttree everywhere because it is
; nil when contradictionp is nil.
(mv (list cl) nil nil))
(t
(let ((rule (selectinstantiatedelimrule cl typealist eliminables
ens wrld)))
(cond ((null rule) (mv (list cl) nil nil))
(t (mvlet (contradictionp newclause elimvars1 ele)
(applyinstantiatedelimrule rule cl typealist
avoidvars ens wrld)
(let ((clauses1 (if contradictionp
nil
(splitonassumptions
(access elimrule rule :hyps)
cl nil))))
; Clauses1 is a set of clauses obtained by splitting on the
; instantiated hyps of the rule. It contains n clauses, each obtained
; by adding one member of insthyps to cl. (If any of these new
; clauses is a tautology, it will be deleted, thus there may not be as
; many clauses as there are insthyps.) Because these n clauses are
; all "pathological" wrt the destructor term, e.g., we're assuming
; (not (consp x)) in a clause involving (car x), we do no further
; elimination down those paths. Note the special case where
; contradictionp is true, meaning that we have ascertained that the
; pathological cases are all impossible.
(cond
((equal newclause *trueclause*)
(mv clauses1 elimvars1 (list ele)))
(t
(mvlet (clauses2 elimvars2 elimseq)
(eliminatedestructorsclause1
newclause
(if topflg
elimvars1
(unioneq elimvars1
(remove1eq
(access elimrule rule :rhs)
eliminables)))
avoidvars
ens
wrld
nil)
(mv (conjoinclausesets clauses1 clauses2)
(unioneq elimvars1 elimvars2)
(cons ele elimseq))))))))))))))
(defun ownedvars (process mineflg history)
; This function takes a process name, e.g., 'eliminatedestructors
; clause, a flag which must be either nil or t, and a clause history.
; If the flag is t, it returns all of the variables introduced into
; the history by the given process. If the flag is nil, it returns
; all of the variables introduced into the history by any other
; process. Note: the variables returned may not even occur in the
; clause whose history we scan.
; For example, if the only two processes that introduce variables are
; destructor elimination and generalization, then when given
; 'eliminatedestructorsclause and mineflg nil this function will
; return all the variables introduced by 'generalizeclause.
; In order to work properly, a process that introduces variables must
; so record it by adding a tagged object to the ttree of the process.
; The tag should be 'variables and the object should be a list of the
; variables introduced at that step. There should be at most one
; occurrence of that tag in the ttree.
; Why are we interested in this concept? Destructor elimination is
; controlled by a heuristic meant to prevent indefinite elim loops
; involving simplification. For example, suppose you eliminate (CDR
; X0) by introducing (CONS A X1) for X0, and then open a recursive
; function so as to produce (CDR X1). It is easy to cause a loop if
; you then eliminate (CDR X1) by replacing X1 it with (CONS B X2),
; etc. To prevent this, we do not allow destructor elimination to
; work on a variable that was introduced by destructor elimination
; (except within the activation of the elim process that introduces
; that variable).
; That raises the question of telling how a variable was introduced
; into a clause. In ACL2 we adopt the convention described above and
; follow the rule that no process shall introduce a variable into a
; clause that has been introduced by a different process in the
; history of that clause. Thus, if X1 is introduced by elim into the
; history, then X1 cannot also be introduced by generalization, even
; if X1 is new for the clause when generalization occurs. By
; following this rule we know that if a variable is in a clause and
; that variable was introduced into the history of the clause by elim
; then that variable was introduced into the clause by elim. If
; generalize could "reuse" a variable that was already "owned" by
; elim in the history, then we could not accurately determine by
; syntactic means the elim variables in the clause.
; Historical Remark on Nqthm:
; Nqthm solved this problem by allocating a fixed set of variable names
; to elim and a disjoint set to generalize. At the top of the waterfall it
; removed from those two fixed sets the variables that occurred in the
; input clause. Thereafter, if a variable was found to be in the (locally)
; fixed sets, it was known to be introduced by the given process. The
; limitation to a fixed set caused the famous setdifn error message
; when the set was exhausted:
; FATAL ERROR: SETDIFFN called with inappropriate arguments.
; In the neverreleased xnqthm  the "book version" of Nqthm that was
; in preparation when we began work on ACL2  we generated a more
; informative error message and increased the size of the fixed sets
; from 18 to over 600. But that meant copying a list of length 600 at
; the top of the waterfall. But the real impetus to the current
; scheme was the irritation over there being a fixed set and the
; attraction of being able to generate mnemonic names from terms. (It
; remains to be seen whether we like the current algorithms. E.g., is
; AENI really a good name for (EXPLODENONNEGATIVEINTEGER N 10 A)?
; In any case, now we are free to experiment with name generation.)
(cond ((null history) nil)
((eq mineflg
(eq (access historyentry (car history) :processor)
process))
(unioneq (cdr (taggedobject 'variables
(access historyentry (car history)
:ttree)))
(ownedvars process mineflg (cdr history))))
(t (ownedvars process mineflg (cdr history)))))
(defun eliminatedestructorsclause (clause hist pspv wrld state)
; This is the waterfall processor that eliminates destructors.
; Like all waterfall processors it returns four values: 'hit or 'miss,
; and, if 'hit, a set of clauses, a ttree, and a possibly modified pspv.
(declare (ignore state))
(mvlet
(clauses elimvars elimseq)
(eliminatedestructorsclause1 clause
(setdifferenceeq
(allvars1lst clause nil)
(ownedvars 'eliminatedestructorsclause t
hist))
(ownedvars 'eliminatedestructorsclause nil
hist)
(access rewriteconstant
(access provespecvar
pspv
:rewriteconstant)
:currentenabledstructure)
wrld
t)
(cond (elimseq (mv 'hit clauses
(addtotagtree 'variables elimvars
(addtotagtree 'elimsequence
elimseq
nil))
pspv))
(t (mv 'miss nil nil nil)))))
; We now develop the code to describe the destructor elimination done,
; starting with printing clauses prettily.
(defun prettyifyclause1 (cl wrld)
(cond ((null (cdr cl)) nil)
(t (cons (untranslate (dumbnegatelit (car cl)) t wrld)
(prettyifyclause1 (cdr cl) wrld)))))
(defun prettyifyclause2 (cl wrld)
(cond ((null cl) nil)
((null (cdr cl)) (untranslate (car cl) t wrld))
((null (cddr cl)) (list 'implies
(untranslate (dumbnegatelit (car cl)) t wrld)
(untranslate (cadr cl) t wrld)))
(t (list 'implies
(cons 'and (prettyifyclause1 cl wrld))
(untranslate (car (last cl)) t wrld)))))
; Rockwell Addition: Prettyifyclause now has a new arg to control
; whether we abstract away common subexprs. This will show up many
; times in a comparewindows.
(defun prettyifyclause (cl let*abstractionp wrld)
(if let*abstractionp
(mvlet (vars terms)
(maximalmultiples (cons 'list cl) let*abstractionp)
(cond
((null vars)
(prettyifyclause2 cl wrld))
(t `(let* ,(listlis vars
(untranslatelst (allbutlast terms)
nil wrld))
,(prettyifyclause2 (cdr (car (last terms))) wrld)))))
(prettyifyclause2 cl wrld)))
(defun prettyifyclauselst (clauses let*abstractionp wrld)
(cond ((null clauses) nil)
(t (cons (prettyifyclause (car clauses) let*abstractionp wrld)
(prettyifyclauselst (cdr clauses) let*abstractionp
wrld)))))
(defun prettyifyclauseset (clauses let*abstractionp wrld)
(cond ((null clauses) t)
((null (cdr clauses))
(prettyifyclause (car clauses) let*abstractionp wrld))
(t (cons 'and (prettyifyclauselst clauses let*abstractionp wrld)))))
(defun tilde*elimphrase/alist1 (alist wrld)
(cond ((null alist) nil)
(t (cons (msg "~p0 by ~x1"
(untranslate (caar alist) nil wrld)
(cdar alist))
(tilde*elimphrase/alist1 (cdr alist) wrld)))))
(defun tilde*elimphrase/alist (alist wrld)
; Alist is never nil, except in the unusual case that
; applyinstantiatedelimrule detected a tautology where we claim
; none could occur. If that happens we print the phrase "generalizing
; nothing". This is documented simply because it is strange to put
; anything in the 0 case below.
(list* "" " and ~@*" ", ~@*" ", ~@*"
(tilde*elimphrase/alist1 alist wrld)
nil))
(defun tilde*elimphrase3 (vartorunesalist)
(cond ((null vartorunesalist) nil)
(t (cons (msg "noting the condition imposed on ~x0 by the ~
generalization rule~#1~[~/s~] ~&1"
(caar vartorunesalist)
(stripbasesymbols (cdar vartorunesalist)))
(tilde*elimphrase3 (cdr vartorunesalist))))))
(defun tilde*elimphrase2 (alist restrictedvars vartorunesalist ttree wrld)
(list* "" "~@*" "~@* and " "~@*, "
(append
(list (msg "~*0"
(tilde*elimphrase/alist alist wrld)))
(cond
(restrictedvars
(let ((simpphrase (tilde*simpphrase ttree)))
(cond ((null (cdr restrictedvars))
(list (msg "restrict the type of the new ~
variable ~&0 to be that of the term ~
it replaces~#1~[~/, as established ~
by ~*2~]"
restrictedvars
(if (nth 4 simpphrase) 1 0)
simpphrase)))
(t (list (msg "restrict the types of the new ~
variables ~&0 to be those of the ~
terms they replace~#1~[~/, as ~
established by ~*2~]"
restrictedvars
(if (nth 4 simpphrase) 1 0)
simpphrase))))))
(t nil))
(tilde*elimphrase3 vartorunesalist))
nil))
(defun tilde*elimphrase1 (lst i alreadyused wrld)
(cond
((null lst) nil)
(t (cons
(cons "(~xi) ~#f~[Use~/Finally, use~] ~#a~[~x0~/~x0, again,~] to ~
replace ~x1 by ~p2~*3. "
(list (cons #\i i)
(cons #\f (if (and (null (cdr lst))
(> i 2))
1
0))
(cons #\a (if (memberequal (nth 0 (car lst)) alreadyused)
(if (memberequal (nth 0 (car lst))
(cdr (memberequal
(nth 0 (car lst))
alreadyused)))
0
1)
0))
(cons #\0 (basesymbol (nth 0 (car lst))))
(cons #\1 (nth 1 (car lst)))
(cons #\2 (untranslate (nth 2 (car lst)) nil wrld))
(cons #\3 (tilde*elimphrase2 (nth 3 (car lst))
(nth 4 (car lst))
(nth 5 (car lst))
(nth 6 (car lst))
wrld))))
(tilde*elimphrase1 (cdr lst)
(1+ i)
(cons (nth 0 (car lst))
alreadyused)
wrld)))))
(defun tilde*elimphrase (lst wrld)
; Lst is the 'elimsequence list of the ttree of the elim process,
; i.e., it is the third result of eliminatedestructorsclause1 above,
; the third result of applyinstantiatedelimrule, i.e., a list of
; elements of the form
; (rune rhs lhs alist restrictedvars vartorunesalist ttree).
; We generate an object suitable for giving to the tilde* fmt directive
; that will cause each element of the list to print out a phrase
; describing that step.
(list* ""
"~@*"
"~@*"
"~@*"
(tilde*elimphrase1 lst 1 nil wrld)
nil))
(defun tilde*untranslatelstphrase (lst flg wrld)
(list* "" "~p*" "~p* and " "~p*, "
(untranslatelst lst flg wrld)
nil))
(defun eliminatedestructorsclausemsg1 (signal clauses ttree pspv state)
; The arguments to this function are the standard ones for an output
; function in the waterfall. See the discussion of the waterfall.
(declare (ignore signal pspv))
(let ((lst (cdr (taggedobject 'elimsequence ttree)))
(n (length clauses))
(wrld (w state)))
(cond
((null (cdr lst))
(fms "The destructor term~#p~[~/s~] ~*0 can be eliminated by ~
using ~x1 to replace ~p2 by ~p3~*4. ~#5~[All the ~
clauses produced are tautological.~/This produces the following goal.~/~
This produces the following ~n6 goals.~]~"
(list (cons #\p (nth 3 (car lst)))
(cons #\0 (tilde*untranslatelstphrase
(stripcars (nth 3 (car lst))) nil wrld))
(cons #\1 (basesymbol (nth 0 (car lst))))
(cons #\2 (nth 1 (car lst)))
(cons #\3 (untranslate (nth 2 (car lst)) nil wrld))
(cons #\4 (tilde*elimphrase2 (nth 3 (car lst))
(nth 4 (car lst))
(nth 5 (car lst))
(nth 6 (car lst))
wrld))
(cons #\5 (zerooneormore n))
(cons #\6 n))
(proofsco state)
state
(termevisctuple nil state)))
(t
(fms "The destructor term~#p~[~/s~] ~*0 can be eliminated. Furthermore, ~
~#p~[that term is~/those terms are~] at the root of a ~
chain of ~n1 rounds of destructor elimination. ~*2 ~
These steps produce ~#3~[no nontautological goals~/the ~
following goal~/the following ~n4 goals~].~"
(list (cons #\p (nth 3 (car lst)))
(cons #\0 (tilde*untranslatelstphrase
(stripcars (nth 3 (car lst)))
nil wrld))
(cons #\1 (length lst))
(cons #\2 (tilde*elimphrase lst wrld))
(cons #\3 (zerooneormore n))
(cons #\4 n))
(proofsco state)
state
(termevisctuple nil state))))))
; We now develop the crossfertilization process.
(mutualrecursion
(defun almostquotep1 (term)
(cond ((variablep term) t)
((fquotep term) t)
((flambdaapplicationp term)
(and (almostquotep1 (lambdabody term))
(almostquotep1listp (fargs term))))
((eq (ffnsymb term) 'cons)
(and (almostquotep1 (fargn term 1))
(almostquotep1 (fargn term 2))))
(t nil)))
(defun almostquotep1listp (terms)
(cond ((null terms) t)
(t (and (almostquotep1 (car terms))
(almostquotep1listp (cdr terms))))))
)
(defun almostquotep (term)
; A term is "almost a quotep" if it is a nonvariablep term that
; consists only of variables, explicit values, and applications of
; cons. Lambdaapplications are permitted provided they have
; almostquotep bodies and args.
; Further work: See equalxconsxyp.
(and (nvariablep term)
(almostquotep1 term)))
(defun destructorappliedtovarsp (term ens wrld)
; We determine whether term is of the form (destr v1 ... vn)
; where destr has an enabled 'eliminatedestructorsrule
; and all the vi are variables.
(cond ((variablep term) nil)
((fquotep term) nil)
((flambdaapplicationp term) nil)
(t (and (allvariablep (fargs term))
(let ((rule (getprop (ffnsymb term)
'eliminatedestructorsrule
nil 'currentacl2world wrld)))
(and rule
(enablednumep (access elimrule rule :nume)
ens)))))))
(defun dumboccurlstexcept (term lst lit)
; Like dumboccurlst except that it does not look into the first
; element of lst that is equal to lit. If you think of lst as a
; clause and lit as a literal, we ask whether term occurs in some
; literal of clause other than lit. In Nqthm we looked for an eq
; occurrence of lit, which we can't do here. But if there are two
; occurrences of lit in lst, then normally in Nqthm they would not
; be eq and hence we'd look in one of them. Thus, here we look in
; all the literals of lst after we've seen lit. This is probably
; unnecessarily complicated.
(cond ((null lst) nil)
((equal lit (car lst))
(dumboccurlst term (cdr lst)))
(t (or (dumboccur term (car lst))
(dumboccurlstexcept term (cdr lst) lit)))))
(defun fertilizefeasible (lit cl hist term ens wrld)
; Lit is a literal of the form (not (equiv term val)) (or the commuted
; form). We determine if it is feasible to substitute val for term in
; clause cl. By that we mean that term is neither a near constant nor
; a destructor, term does occur elsewhere in the clause, every
; occurrence of term is equivhittable, and we haven't already
; fertilized with this literal.
(and (not (almostquotep term))
(not (destructorappliedtovarsp term ens wrld))
(dumboccurlstexcept term cl lit)
(everyoccurrenceequivhittablepinclausep (ffnsymb (fargn lit 1))
term cl ens wrld)
(not (alreadyusedbyfertilizeclausep lit hist t))))
(mutualrecursion
(defun fertilizecomplexity (term wrld)
; The fertilizecomplexity of (fn a1 ... an) is the level number of fn
; plus the maximum fertilize complexity of ai.
(cond ((variablep term) 0)
((fquotep term) 0)
(t (+ (getlevelno (ffnsymb term) wrld)
(maximizefertilizecomplexity (fargs term) wrld)))))
(defun maximizefertilizecomplexity (terms wrld)
(cond ((null terms) 0)
(t (max (fertilizecomplexity (car terms) wrld)
(maximizefertilizecomplexity (cdr terms) wrld)))))
)
(defun firstfertilizelit (lst cl hist ens wrld)
; We find the first literal lst of the form (not (equiv lhs1 rhs1))
; such that a fertilization of one side for the other into cl is
; feasible. We return six values. The first is either nil, meaning
; no such lit was found, or a direction of 'leftforright or
; 'rightforleft. The second is the literal found. The last three are
; the equiv, lhs, and rhs of the literal, and the length of the tail of
; cl after lit.
(cond
((null lst) (mv nil nil nil nil nil nil))
(t (let ((lit (car lst)))
(casematch
lit
(('not (equiv lhs rhs))
(cond
((equivalencerelationp equiv wrld)
(cond
((fertilizefeasible lit cl hist lhs ens wrld)
(cond
((fertilizefeasible lit cl hist rhs ens wrld)
(cond ((< (fertilizecomplexity lhs wrld)
(fertilizecomplexity rhs wrld))
(mv 'leftforright lit equiv lhs rhs (len (cdr lst))))
(t (mv 'rightforleft lit equiv lhs rhs
(len (cdr lst))))))
(t (mv 'rightforleft lit equiv lhs rhs (len (cdr lst))))))
((fertilizefeasible lit cl hist rhs ens wrld)
(mv 'leftforright lit equiv lhs rhs (len (cdr lst))))
(t (firstfertilizelit (cdr lst) cl hist ens wrld))))
(t (firstfertilizelit (cdr lst) cl hist ens wrld))))
(& (firstfertilizelit (cdr lst) cl hist ens wrld)))))))
(defun crossfertilizep/c (equiv cl direction lhs1 rhs1)
; See condition (c) of crossfertilizep.
(cond ((null cl) nil)
((and (nvariablep (car cl))
(not (fquotep (car cl)))
(equal (ffnsymb (car cl)) equiv)
(if (eq direction 'leftforright)
(dumboccur rhs1 (fargn (car cl) 2))
(dumboccur lhs1 (fargn (car cl) 1))))
t)
(t (crossfertilizep/c equiv (cdr cl) direction lhs1 rhs1))))
(defun crossfertilizep/d (equiv cl direction lhs1 rhs1)
; See condition (d) of crossfertilizep.
(cond ((null cl) nil)
((and (nvariablep (car cl))
(not (fquotep (car cl)))
(equal (ffnsymb (car cl)) equiv)
(if (eq direction 'leftforright)
(dumboccur rhs1 (fargn (car cl) 1))
(dumboccur lhs1 (fargn (car cl) 2))))
t)
(t (crossfertilizep/d equiv (cdr cl) direction lhs1 rhs1))))
(defun crossfertilizep (equiv cl pspv direction lhs1 rhs1)
; We have found a literal, (not (equiv lhs1 rhs1)), of cl such that a
; fertilization is feasible in the indicated direction. We want to
; know whether this will be a crossfertilization or not. Suppose,
; without loss of generality, that the direction is 'leftforright,
; i.e., we are going to substitute lhs1 for rhs1. A cross
; fertilization is performed only if (a) neither lhs1 nor rhs1 is an
; explicit value, (b) we are under an induction (thus our interest in
; pspv), (c) there is some equiv literal, (equiv lhs2 rhs2), in the
; clause such that rhs1 occurs in rhs2 (thus we'll hit rhs2) and (d)
; there is some equiv literal such that rhs1 occurs in lhs2 (thus,
; cross fertilization will actually prevent us from hitting something
; massive substitution would hit). Note that since we know the
; fertilization is feasible, every occurrence of the target is in an
; equivhittable slot. Thus, we can use equivalenceinsensitive occur
; checks rather than being prissy.
(and (not (quotep lhs1))
(not (quotep rhs1))
(assoceq 'beingprovedbyinduction
(access provespecvar pspv :pool))
(crossfertilizep/c equiv cl direction lhs1 rhs1)
(crossfertilizep/d equiv cl direction lhs1 rhs1)))
(defun deletefromttree1 (tag val ttree changedpseen)
; This function returns (mv changedp newttree), where if changedp is nil then
; newttree equals ttree. Tag is a symbol. If changedp is nil then newttree
; is equal (in fact eq) to ttree.
(cond ((null ttree) (mv changedpseen nil))
((and (eq tag (caar ttree))
(equal (cdar ttree) val))
(deletefromttree1 tag val (cdr ttree) t))
((symbolp (caar ttree))
(mvlet (changedp cdrttree)
(deletefromttree1 tag val (cdr ttree) changedpseen)
(if changedp
(mv t (cons (car ttree) cdrttree))
(mv nil ttree))))
(t (mvlet (changedp1 ttree1)
(deletefromttree1 tag val (car ttree) changedpseen)
(mvlet (changedp2 ttree2)
(deletefromttree1 tag val (cdr ttree) changedp1)
(if changedp2
(mv t (constagtrees ttree1 ttree2))
(mv nil ttree)))))))
(defun deletefromttree (tag val ttree)
(mvlet (changedp newttree)
(deletefromttree1 tag val ttree nil)
(declare (ignore changedp))
newttree))
(defun fertilizeclause1 (cl lit1 equiv lhs1 rhs1
direction
crossfertflg
deletelitflg
ens
wrld
state
ttree)
; Cl is a clause we are fertilizing with lit1, which is one of its
; literals and which is of the form (not (equiv lhs1 rhs1)). Direction is
; 'leftforright or 'rightforleft, indicating which way we're to
; substitute. Crossfertflg is t if we are to hit only (equiv lhs2
; rhs2) and do it in a crossfertilize sort of way (left for right
; into right or right for left into left); otherwise we substitute for
; all occurrences. Deletelitflg is t if we are to delete the first
; occurrence of lit when we see it. We return two things: the new
; clause and a ttree indicating the congruences used.
(cond
((null cl) (mv nil ttree))
(t
(let* ((lit2 (car cl))
(lit2islit1p (equal lit2 lit1)))
; First, we substitute into lit2 as appropriate. We obtain newlit2
; and a ttree. We ignore the hitp result always returned by
; substequivexpr.
; What do we mean by "as appropriate"? We consider three cases on
; lit2, the literal into which we are substituting: lit2 is (equiv lhs
; rhs), lit2 is (not (equiv lhs rhs)), or otherwise. We also consider
; whether we are cross fertilizing or just substituting for all
; occurrences. Here is a table that explains our actions below.
; lit2 (equiv lhs rhs) (not (equiv lhs rhs)) other
; xfert xfert subst no action
; subst subst subst subst
; The only surprising part of this table is that in the case of
; crossfertilizing into (not (equiv lhs rhs)), i.e., into another
; equiv hypothesis, we do a fullfledged substitution rather than a
; crossfertilization. I do not give an example of why we do this.
; However, it is exactly what Nqthm does (in the only comparable case,
; namely, when equiv is EQUAL).
(mvlet
(hitp newlit2 ttree)
(cond
(lit2islit1p (mv nil lit2 ttree))
((or (not crossfertflg)
(casematch lit2
(('not (equivsym & &)) (equal equivsym equiv))
(& nil)))
(cond ((eq direction 'leftforright)
(substequivexpr equiv lhs1 rhs1
*geneqviff*
lit2 ens wrld state ttree))
(t (substequivexpr equiv rhs1 lhs1
*geneqviff*
lit2 ens wrld state ttree))))
(t
; Caution: There was once a bug below. We are cross fertilizing.
; Suppose we see (equiv lhs2 rhs2) and want to substitute lhs1 for
; rhs1 in rhs2. What geneqv do we maintain? The bug, which was
; completely nonsensical, was that we maintained *geneqviff*, just as
; above. But in fact we must maintain whatever geneqv maintains
; *geneqviff* in the second arg of equiv. Geneqvlst returns a list
; of geneqvs, one for each argument position of equiv. We select the
; one in the argument position corresponding to the side we are
; changing. Actually, the two geneqvs for an equivalence relation
; ought to be the identical, but it would be confusing to exploit
; that.
; In the days when this bug was present there was another problem! We
; only substituted into (equal lhs2 rhs2)! (That is, the casematch
; below was on ('equal lhs2 rhs2) rather than (equivsym lhs2 rhs2).)
; So here is an example of a screwy substitution we might have done:
; Suppose (equiv a b) is a hypothesis and (equal (f a) (f b)) is a
; conclusion and that we are to do a crossfertilization of a for b.
; We ought not to substitute into equal except maintaining equality.
; But we actually would substitute into (f b) maintaining iff! Now
; suppose we knew that (equiv x y) > (iff (f x) (f y)). Then we
; could derive (equal (f a) (f a)), which would be t and unsound. The
; preconditions for this screwy situation are exhibited by:
#
(defun squash (x)
(cond ((null x) nil)
((integerp x) 1)
(t t)))
(defun equiv (x y)
(equal (squash x) (squash y)))
(defequiv equiv)
(defun f (x) x)
(defcong equiv iff (f x) 1)
#
; In particular, (implies (equiv a b) (equal (f a) (f b))) is not a
; theorem (a=1 and b=2 are counterexamples), but this function, if
; called with that input clause, ((not (equiv a b)) (equal (f a) (f
; b))), and the obvious lit1, etc., would return (equal (f a) (f a)),
; which is T. (Here we are substituting left for right, a for b.) So
; there was a soundness bug in the old version of this function.
; But it turns out that this bug could never be exploited. The bug
; can be provoked only if we are doing crossfertilization. And
; crossfertilization is only done if the fertilization is "feasible".
; That means that every occurrence of b in the clause is equiv
; hittable, as per everyoccurrenceequivhittablepinclausep. In
; our example, the b in (f b) is not equiv hittable. Indeed, if every
; occurrence of b is equiv hittable then no matter what braindamaged
; geneqv we use below, the result will be sound! A braindamaged
; geneqv might prevent us from hitting some, but any hit it allowed is
; ok.
; This bug was first noticed by Bill McCune (September, 1998), who
; reported an example in which the system io indicated that a was
; substituted for b but in fact no substitution occurred. No
; substitution occurred because we didn't have the congruence theorem
; shown above  not a surprising lack considering the random nature
; of the problem. At first I was worried about soundness but then saw
; the argument above.
(casematch
lit2
((equivsym lhs2 rhs2)
(cond ((not (equal equivsym equiv)) (mv nil lit2 ttree))
((eq direction 'leftforright)
(mvlet (hitp newrhs2 ttree)
(substequivexpr equiv lhs1 rhs1
(cadr (geneqvlst equiv
*geneqviff*
ens wrld))
rhs2 ens wrld state ttree)
(declare (ignore hitp))
(mv nil
(mconsterm* equiv lhs2 newrhs2)
ttree)))
(t
(mvlet (hitp newlhs2 ttree)
(substequivexpr equiv rhs1 lhs1
(car (geneqvlst equiv
*geneqviff*
ens wrld))
lhs2 ens wrld state ttree)
(declare (ignore hitp))
(mv nil
(mconsterm* equiv newlhs2 rhs2)
ttree)))))
(& (mv nil lit2 ttree)))))
(declare (ignore hitp))
; Second, we recursively fertilize appropriately into the rest of the clause.
(mvlet (newtail ttree)
(fertilizeclause1 (cdr cl) lit1 equiv lhs1 rhs1
direction
crossfertflg
(if lit2islit1p
nil
deletelitflg)
ens wrld state ttree)
; Finally, we combine the two, deleting the lit if required.
(cond
(lit2islit1p
(cond (deletelitflg (mv newtail ttree))
(t (mvlet (notflg atm)
(stripnot lit2)
(prog2$
(or notflg
(er hard 'fertilizeclause1
"We had thought that we only ~
fertilize with negated literals, ~
unlike ~x0!"
newlit2))
(prog2$
(or (equal lit2 newlit2) ; should be eq
(er hard 'fertilizeclause1
"Internal error in ~
fertilizeclause1!~Old lit2: ~
~x0.~New lit2: ~x1"
lit2 newlit2))
(mv (cons (mconsterm* 'not
(mconsterm* 'hide
atm))
newtail)
ttree)))))))
(t (mv (cons newlit2 newtail) ttree)))))))))
(defun fertilizeclause (clid cl hist pspv wrld state)
; A standard clause processor of the waterfall.
; We return 4 values. The first is a signal that is either 'hit, or
; 'miss. When the signal is 'miss, the other 3 values are irrelevant.
; When the signal is 'hit, the second result is the list of new
; clauses, the third is a ttree that will become that component of the
; historyentry for this fertilization, and the fourth is an
; unmodified pspv. (We return the fourth thing to adhere to the
; convention used by all clause processors in the waterfall (q.v.).)
; The ttree we return has seven tagged objects in it plus a bunch
; of 'lemmas indicating the :CONGRUENCE rules used.
; 'literal  the literal from cl we used, guaranteed to be of
; the form (not (equiv lhs rhs)).
; 'clauseid  the current clauseid
; 'hypphrase  a tilde@ phrase that describes literal in cl.
; 'equiv  the equivalence relation
; 'bullet  the term we substituted
; 'target  the term we substituted for
; 'crossfertflg  whether we did a cross fertilization
; 'deletelitflg  whether we deleted literal from the
; clause.
(mvlet (direction lit equiv lhs rhs lentail)
(firstfertilizelit cl cl hist
(access rewriteconstant
(access provespecvar
pspv
:rewriteconstant)
:currentenabledstructure)
wrld)
(cond
((null direction) (mv 'miss nil nil nil))
(t (let ((crossfertflg
(crossfertilizep equiv cl pspv direction lhs rhs))
(deletelitflg
(and
(not (quotep lhs))
(not (quotep rhs))
(assoceq 'beingprovedbyinduction
(access provespecvar
pspv
:pool)))))
(mvlet (newcl ttree)
(fertilizeclause1 cl lit equiv lhs rhs
direction
crossfertflg
deletelitflg
(access rewriteconstant
(access provespecvar
pspv
:rewriteconstant)
:currentenabledstructure)
wrld
state
nil)
(mv 'hit
(list newcl)
(addtotagtree
'literal lit
(addtotagtree
'hypphrase (tilde@hypphrase lentail cl)
(addtotagtree
'crossfertflg crossfertflg
(addtotagtree
'equiv equiv
(addtotagtree
'bullet (if (eq direction 'leftforright)
lhs
rhs)
(addtotagtree
'target (if (eq direction 'leftforright)
rhs
lhs)
(addtotagtree
'clauseid clid
(addtotagtree
'deletelitflg deletelitflg
(if deletelitflg
ttree
(pushlemma (fnrunenume 'hide nil nil
wrld)
ttree))))))))))
pspv)))))))
(defun fertilizeclausemsg1 (signal clauses ttree pspv state)
; The arguments to this function are the standard ones for an output
; function in the waterfall. See the discussion of the waterfall.
(declare (ignore signal pspv clauses))
(let* ((hypphrase (cdr (taggedobject 'hypphrase ttree)))
(wrld (w state))
(ttree
; We can get away with eliminating the :definition of hide from the ttree
; because fertilizeclause1 only pushes lemmas by way of substequivexpr,
; which are either about geneqvs (from geneqvrefinementp) or are executable
; counterparts (from sconsterm). If we do not delete the definition of hide
; from ttree here, we get a bogus "validity of this substitution relies upon
; the :definition HIDE" message.
(deletefromttree 'lemma (fnrunenume 'hide nil nil wrld) ttree)))
(fms "We now use ~@0 by ~#1~[substituting~/crossfertilizing~] ~p2 for ~p3 ~
and ~#4~[hiding~/throwing away~] the ~@5.~#6~[~/ The validity of ~
this substitution relies upon ~*7.~] This produces~"
(list
(cons #\0 hypphrase)
(cons #\1 (if (cdr (taggedobject 'crossfertflg ttree))
1
0))
(cons #\2 (untranslate (cdr (taggedobject 'bullet ttree)) nil wrld))
(cons #\3 (untranslate (cdr (taggedobject 'target ttree)) nil wrld))
(cons #\4 (if (cdr (taggedobject 'deletelitflg ttree))
1
0))
(cons #\5 (if (and (consp hypphrase)
(null (cdr hypphrase)))
"conclusion"
"hypothesis"))
(cons #\6 (if (null (cdr (taggedobject 'lemma ttree)))
0
1))
(cons #\7 (tilde*simpphrase ttree)))
(proofsco state)
state
(termevisctuple nil state))))
; And now we do generalization...
(defun collectablefnp (fn ens wrld)
; A common collectable term is a nonquoted term that is an
; application of a collectablefnp. Most functions are common
; collectable. The ones that are not are cons, open lambdas, and the
; (enabled) destructors of wrld.
(cond ((flambdap fn) nil)
((eq fn 'cons) nil)
(t (let ((rule (getprop fn 'eliminatedestructorsrule nil
'currentacl2world wrld)))
(cond ((and rule
(enablednumep (access elimrule rule :nume) ens))
nil)
(t t))))))
(mutualrecursion
(defun smallestcommonsubterms1 (term1 term2 ens wrld ans)
; This is the workhorse of smallestcommonsubterms, but the arguments are
; arranged so that we know that term1 is the smaller. We add to ans
; every subterm x of term1 that (a) occurs in term2, (b) is
; collectable, and (c) has no collectable subterms in common with
; term2.
; We return two values. The first is the modified ans. The second is
; t or nil according to whether term1 occurs in term2 but neither it
; nor any of its subterms is collectable. This latter condition is
; said to be the ``potential'' of term1 participating in a collection
; vicariously. What does that mean? Suppose a1, ..., an, all have
; potential. Then none of them are collected (because they aren't
; collectable) but each occurs in term2. Thus, a term such as (fn a1
; ... an) might actually be collected because it may occur in term2
; (all of its args do, at least), it may be collectable, and none of
; its subterms are. So those ai have the potential to participate
; vicariously in a collection.
(cond ((or (variablep term1)
(fquotep term1))
; Since term1 is not collectable, we don't add it to ans. But we return
; t as our second value if term1 occurs in term2, i.e., term1 has
; potential.
(mv ans (occur term1 term2)))
(t (mvlet
(ans allpotentials)
(smallestcommonsubterms1lst (fargs term1) term2 ens wrld ans)
(cond ((null allpotentials)
; Ok, some arg did not have potential. Either it did not occur or it
; was collected. In either case, term1 should not be collected and
; furthermore, has no potential for participating later.
(mv ans nil))
((not (occur term1 term2))
; Every arg of term1 had potential but term1 doesn't occur in
; term2. That means we don't collect it and it hasn't got
; potential.
(mv ans nil))
((collectablefnp (ffnsymb term1) ens wrld)
; So term1 occurs, none of its subterms were collected, and term1
; is collectable. So we collect it, but it no longer has potential
; (because it got collected).
(mv (addtosetequal term1 ans)
nil))
(t
; Term1 occurs, none of its subterms were collected, and term1
; was not collected. So it has potential to participate vicariously.
(mv ans t)))))))
(defun smallestcommonsubterms1lst (terms term2 ens wrld ans)
; We accumulate onto ans every subterm of every element of terms
; that (a) occurs in term2, (b) is collectable, and (c) has no
; collectable subterms in common with term2. We return the modified
; ans and the flag indicating whether all of the terms have potential.
(cond
((null terms) (mv ans t))
(t (mvlet
(ans carpotential)
(smallestcommonsubterms1 (car terms) term2 ens wrld ans)
(mvlet
(ans cdrpotential)
(smallestcommonsubterms1lst (cdr terms) term2 ens wrld ans)
(mv ans
(and carpotential
cdrpotential)))))))
)
(defun smallestcommonsubterms (term1 term2 ens wrld ans)
; We accumulate onto ans and return the list of every subterm x of
; term1 that is also a subterm of term2, provided x is ``collectable''
; and no subterm of x is collectable. A term is a collectable if it
; is an application of a collectablefnp and is not an explicit value.
; Our aim is to collect the ``innermost'' or ``smallest'' collectable
; subterms.
(mvlet (ans potential)
(cond ((> (conscount term1) (conscount term2))
(smallestcommonsubterms1 term2 term1 ens wrld ans))
(t (smallestcommonsubterms1 term1 term2 ens wrld ans)))
(declare (ignore potential))
ans))
(defun generalizingrelationp (term wrld)
; Term occurs as a literal of a clause. We want to know whether
; we should generalize common subterms occurring in its arguments.
; Right now the answer is geared to the special case that term is
; a binary relation  or at least that only two of the arguments
; encourage generalizations. We return three results. The first
; is t or nil indicating whether the other two are important.
; The other two are the two terms we should explore for common
; subterms.
; For example, for (equal lhs rhs), (not (equal lhs rhs)), (< lhs
; rhs), and (not (< lhs rhs)), we return t, lhs, and rhs. We also
; generalize across any known equivalence relation, but this code has
; built into the assumption that all such relations have arity at
; least 2 and just returns the first two args. For (member x y), we
; return three nils.
(mvlet (negflg atm)
(stripnot term)
(declare (ignore negflg))
(cond ((or (variablep atm)
(fquotep atm)
(flambdaapplicationp atm))
(mv nil nil nil))
((or (eq (ffnsymb atm) 'equal)
(eq (ffnsymb atm) '<)
(equivalencerelationp (ffnsymb atm) wrld))
(mv t (fargn atm 1) (fargn atm 2)))
(t (mv nil nil nil)))))
(defun generalizabletermsacrossrelations (cl ens wrld ans)
; We scan clause cl for each literal that is a generalizingrelationp,
; e.g., (equal lhs rhs), and collect into ans all the smallest common
; subterms that occur in each lhs and rhs. We return the final ans.
(cond ((null cl) ans)
(t (mvlet (genp lhs rhs)
(generalizingrelationp (car cl) wrld)
(generalizabletermsacrossrelations
(cdr cl) ens wrld
(if genp
(smallestcommonsubterms lhs rhs ens wrld ans)
ans))))))
(defun generalizabletermsacrossliterals1 (lit1 cl ens wrld ans)
(cond ((null cl) ans)
(t (generalizabletermsacrossliterals1
lit1 (cdr cl) ens wrld
(smallestcommonsubterms lit1 (car cl) ens wrld ans)))))
(defun generalizabletermsacrossliterals (cl ens wrld ans)
; We consider each pair of literals, lit1 and lit2, in cl and
; collect into ans the smallest common subterms that occur in
; both lit1 and lit2. We return the final ans.
(cond ((null cl) ans)
(t (generalizabletermsacrossliterals
(cdr cl) ens wrld
(generalizabletermsacrossliterals1 (car cl) (cdr cl)
ens wrld ans)))))
(defun generalizableterms (cl ens wrld)
; We return the list of all the subterms of cl that we will generalize.
; We look for common subterms across equalities and inequalities, and
; for common subterms between the literals of cl.
(generalizabletermsacrossliterals
cl ens wrld
(generalizabletermsacrossrelations
cl ens wrld nil)))
(defun generalizeclause (cl hist pspv wrld state)
; A standard clause processor of the waterfall.
; We return 4 values. The first is a signal that is either 'hit, or
; 'miss. When the signal is 'miss, the other 3 values are irrelevant.
; When the signal is 'hit, the second result is the list of new
; clauses, the third is a ttree that will become that component of the
; historyentry for this generalization, and the fourth is an
; unmodified pspv. (We return the fourth thing to adhere to the
; convention used by all clause processors in the waterfall (q.v.).)
; The ttree we return is 'assumptionfree.
(declare (ignore state))
(cond
((not (assoceq 'beingprovedbyinduction
(access provespecvar pspv :pool)))
(mv 'miss nil nil nil))
(t (let* ((ens (access rewriteconstant
(access provespecvar
pspv
:rewriteconstant)
:currentenabledstructure))
(terms (generalizableterms cl ens wrld)))
(cond
((null terms)
(mv 'miss nil nil nil))
(t
(mvlet
(contradictionp typealist ttree)
(typealistclause cl nil t nil ens wrld
nil nil)
(declare (ignore ttree))
(cond
(contradictionp
; We compute the typealist of the clause to allow us to generate nice
; variable names and to restrict the coming generalization. We know
; that a contradiction cannot arise, because this clause survived
; simplification. However, we will return an accurate answer just to
; be rugged. We'll report that we couldn't do anything! That's
; really funny. We just proved our goal and we're saying we can't do
; anything. But if we made this fn sometimes return the empty set of
; clauses we'd want to fix the io handler for it and we'd have to
; respect the 'assumptions in the ttree and we don't. Do we? As
; usual, we ignore the ttree in this case, and hence we ignore it
; totally since it is known to be nil when contradictionp is nil.
(mv 'miss nil nil nil))
(t
(let ((genvars
(generatevariablelst terms
(allvars1lst cl
(ownedvars
'generalizeclause
nil
hist))
typealist ens wrld)))
(mvlet (generalizedcl restrictedvars vartorunesalist ttree)
(generalize1 cl typealist terms genvars ens wrld)
(mv 'hit
(list generalizedcl)
(addtotagtree
'variables genvars
(addtotagtree
'terms terms
(addtotagtree
'restrictedvars restrictedvars
(addtotagtree
'vartorunesalist vartorunesalist
(addtotagtree
'tsttree ttree
nil)))))
pspv))))))))))))
(defun tilde*genphrase/alist1 (alist wrld)
(cond ((null alist) nil)
(t (cons (msg "~p0 by ~x1"
(untranslate (caar alist) nil wrld)
(cdar alist))
(tilde*genphrase/alist1 (cdr alist) wrld)))))
(defun tilde*genphrase/alist (alist wrld)
; Alist is never nil
(list* "" "~@*" "~@* and " "~@*, "
(tilde*genphrase/alist1 alist wrld)
nil))
(defun tilde*genphrase (alist restrictedvars vartorunesalist ttree wrld)
(list* "" "~@*" "~@* and " "~@*, "
(append
(list (msg "~*0"
(tilde*genphrase/alist alist wrld)))
(cond
(restrictedvars
(let* ((runes (taggedobjects 'lemma ttree nil))
(primitivetypereasoningp
(memberequal *fakerunefortypeset* runes))
(symbols
(stripbasesymbols
(remove1equal *fakerunefortypeset* runes))))
(cond ((membereq nil symbols)
(er hard 'tilde*genphrase
"A fake rune other than ~
*fakerunefortypeset* was found in the ~
tsttree generated by generalizeclause. ~
The list of runes in the ttree is ~x0."
runes))
((null (cdr restrictedvars))
(list (msg "restricting the type of the new ~
variable ~&0 to be that of the term ~
it replaces~#1~[~/, as established ~
by primitive type reasoning~/, as ~
established by ~&2~/, as established ~
by primitive type reasoning and ~&2~]"
restrictedvars
(cond ((and symbols
primitivetypereasoningp)
3)
(symbols 2)
(primitivetypereasoningp 1)
(t 0))
symbols)))
(t (list (msg "restricting the types of the new ~
variables ~&0 to be those of the ~
terms they replace~#1~[~/, as ~
established by primitive type ~
reasoning~/, as established by ~
~&2~/, as established by primitive ~
type reasoning and ~&2~]"
restrictedvars
(cond ((and symbols
primitivetypereasoningp)
3)
(symbols 2)
(primitivetypereasoningp 1)
(t 0))
symbols))))))
(t nil))
(tilde*elimphrase3 vartorunesalist))
nil))
(defun generalizeclausemsg1 (signal clauses ttree pspv state)
; The arguments to this function are the standard ones for an output
; function in the waterfall. See the discussion of the waterfall.
(declare (ignore signal pspv clauses))
(fms "We generalize this conjecture, replacing ~*0. This produces~"
(list
(cons #\0
(tilde*genphrase
(pairlis$ (cdr (taggedobject 'terms ttree))
(cdr (taggedobject 'variables ttree)))
(cdr (taggedobject 'restrictedvars ttree))
(cdr (taggedobject 'vartorunesalist ttree))
(cdr (taggedobject 'tsttree ttree))
(w state))))
(proofsco state)
state
(termevisctuple nil state)))
; The elimination of irrelevance is defined in the same file as induct
; because elim uses m&m.
