Merge pull request #2 from mio-19/mio · liamoc.net/holbert-ng@5a6da2f

+7

index.html

··· 222 222 .term-bound { 223 223 color: var(--bound-col); 224 224 } 225 + .term-app { 226 + font-family: "Computer Modern Sans"; 227 + color: var(--constructor-col); 228 + } 229 + .term-app-telescope { 230 + vertical-align: sub; 231 + } 225 232 .term-constructor { 226 233 font-family: "Computer Modern Sans"; 227 234 color: var(--constructor-col);

+344 -4

package-lock.json

··· 14 14 "rescript": "^11.1.4" 15 15 }, 16 16 "devDependencies": { 17 + "@dusty-phillips/rescript-zora": "^5.0.1", 17 18 "@eslint/js": "^9.25.0", 18 19 "@rescript/core": "^1.6.1", 19 20 "@rescript/std": "^11.1.4", ··· 24 25 "eslint-plugin-react-hooks": "^5.2.0", 25 26 "eslint-plugin-react-refresh": "^0.4.19", 26 27 "globals": "^16.0.0", 28 + "onchange": "^7.1.0", 29 + "pta": "^1.3.0", 27 30 "typescript": "~5.8.3", 28 31 "typescript-eslint": "^8.30.1", 29 32 "vite": "^6.3.5" 30 33 } 34 + }, 35 + "node_modules/@blakeembrey/deque": { 36 + "version": "1.0.5", 37 + "resolved": "https://registry.npmjs.org/@blakeembrey/deque/-/deque-1.0.5.tgz", 38 + "integrity": "sha512-6xnwtvp9DY1EINIKdTfvfeAtCYw4OqBZJhtiqkT3ivjnEfa25VQ3TsKvaFfKm8MyGIEfE95qLe+bNEt3nB0Ylg==", 39 + "dev": true, 40 + "license": "Apache-2.0" 41 + }, 42 + "node_modules/@blakeembrey/template": { 43 + "version": "1.2.0", 44 + "resolved": "https://registry.npmjs.org/@blakeembrey/template/-/template-1.2.0.tgz", 45 + "integrity": "sha512-w/63nURdkRPpg3AXbNr7lPv6HgOuVDyefTumiXsbXxtIwcuk5EXayWR5OpSwDjsQPgaYsfUSedMduaNOjAYY8A==", 46 + "dev": true, 47 + "license": "Apache-2.0" 48 + }, 49 + "node_modules/@dusty-phillips/rescript-zora": { 50 + "version": "5.0.1", 51 + "resolved": "https://registry.npmjs.org/@dusty-phillips/rescript-zora/-/rescript-zora-5.0.1.tgz", 52 + "integrity": "sha512-OQPkqPWpdJ9kFIfySf289ZM08GNbo2G//dty5+zMp9F6L33axB8VLnna4mlMsuKmutiY8bIPgFpvstdKWx99UA==", 53 + "dev": true, 54 + "license": "MIT", 55 + "dependencies": { 56 + "pta": "^1.2.0", 57 + "zora": "^5.2.0" 58 + } 59 + }, 60 + "node_modules/@dusty-phillips/rescript-zora/node_modules/zora": { 61 + "version": "5.2.0", 62 + "resolved": "https://registry.npmjs.org/zora/-/zora-5.2.0.tgz", 63 + "integrity": "sha512-FSZOvfJVfMWhk/poictNsDBCXq/Z+2Zu2peWs6d8OhWWb9nY++czw95D47hdw06L/kfjasLevwrbUtnXyWLAJw==", 64 + "dev": true, 65 + "license": "MIT" 31 66 }, 32 67 "node_modules/@esbuild/aix-ppc64": { 33 68 "version": "0.25.5", ··· 595 630 } 596 631 }, 597 632 "node_modules/@eslint/plugin-kit": { 598 - "version": "0.3.1", 599 - "resolved": "https://registry.npmjs.org/@eslint/plugin-kit/-/plugin-kit-0.3.1.tgz", 600 - "integrity": "sha512-0J+zgWxHN+xXONWIyPWKFMgVuJoZuGiIFu8yxk7RJjxkzpGmyja5wRFqZIVtjDVOQpV+Rw0iOAjYPE2eQyjr0w==", 633 + "version": "0.3.4", 634 + "resolved": "https://registry.npmjs.org/@eslint/plugin-kit/-/plugin-kit-0.3.4.tgz", 635 + "integrity": "sha512-Ul5l+lHEcw3L5+k8POx6r74mxEYKG5kOb6Xpy2gCRW6zweT6TEhAf8vhxGgjhqrd/VO/Dirhsb+1hNpD1ue9hw==", 601 636 "dev": true, 602 637 "license": "Apache-2.0", 603 638 "dependencies": { 604 - "@eslint/core": "^0.14.0", 639 + "@eslint/core": "^0.15.1", 605 640 "levn": "^0.4.1" 606 641 }, 607 642 "engines": { 608 643 "node": "^18.18.0 || ^20.9.0 || >=21.1.0" 609 644 } 610 645 }, 646 + "node_modules/@eslint/plugin-kit/node_modules/@eslint/core": { 647 + "version": "0.15.1", 648 + "resolved": "https://registry.npmjs.org/@eslint/core/-/core-0.15.1.tgz", 649 + "integrity": "sha512-bkOp+iumZCCbt1K1CmWf0R9pM5yKpDv+ZXtvSyQpudrI9kuFLp+bM2WOPXImuD/ceQuaa8f5pj93Y7zyECIGNA==", 650 + "dev": true, 651 + "license": "Apache-2.0", 652 + "dependencies": { 653 + "@types/json-schema": "^7.0.15" 654 + }, 655 + "engines": { 656 + "node": "^18.18.0 || ^20.9.0 || >=21.1.0" 657 + } 658 + }, 611 659 "node_modules/@humanfs/core": { 612 660 "version": "0.19.1", 613 661 "resolved": "https://registry.npmjs.org/@humanfs/core/-/core-0.19.1.tgz", ··· 1025 1073 "os": [ 1026 1074 "win32" 1027 1075 ] 1076 + }, 1077 + "node_modules/@sindresorhus/merge-streams": { 1078 + "version": "2.3.0", 1079 + "resolved": "https://registry.npmjs.org/@sindresorhus/merge-streams/-/merge-streams-2.3.0.tgz", 1080 + "integrity": "sha512-LtoMMhxAlorcGhmFYI+LhPgbPZCkgP6ra1YL604EeF6U98pLlQ3iWIGMdWSC+vWmPBWBNgmDBAhnAobLROJmwg==", 1081 + "dev": true, 1082 + "license": "MIT", 1083 + "engines": { 1084 + "node": ">=18" 1085 + }, 1086 + "funding": { 1087 + "url": "https://github.com/sponsors/sindresorhus" 1088 + } 1028 1089 }, 1029 1090 "node_modules/@swc/core": { 1030 1091 "version": "1.12.0", ··· 1613 1674 "url": "https://github.com/chalk/ansi-styles?sponsor=1" 1614 1675 } 1615 1676 }, 1677 + "node_modules/anymatch": { 1678 + "version": "3.1.3", 1679 + "resolved": "https://registry.npmjs.org/anymatch/-/anymatch-3.1.3.tgz", 1680 + "integrity": "sha512-KMReFUr0B4t+D+OBkjR3KYqvocp2XaSzO55UcB6mgQMd3KbcE+mWTyvVV7D/zsdEbNnV6acZUutkiHQXvTr1Rw==", 1681 + "dev": true, 1682 + "license": "ISC", 1683 + "dependencies": { 1684 + "normalize-path": "^3.0.0", 1685 + "picomatch": "^2.0.4" 1686 + }, 1687 + "engines": { 1688 + "node": ">= 8" 1689 + } 1690 + }, 1691 + "node_modules/arg": { 1692 + "version": "4.1.3", 1693 + "resolved": "https://registry.npmjs.org/arg/-/arg-4.1.3.tgz", 1694 + "integrity": "sha512-58S9QDqG0Xx27YwPSt9fJxivjYl432YCwfDMfZ+71RAqUrZef7LrKQZ3LHLOwCS4FLNBplP533Zx895SeOCHvA==", 1695 + "dev": true, 1696 + "license": "MIT" 1697 + }, 1616 1698 "node_modules/argparse": { 1617 1699 "version": "2.0.1", 1618 1700 "resolved": "https://registry.npmjs.org/argparse/-/argparse-2.0.1.tgz", ··· 1626 1708 "integrity": "sha512-3oSeUO0TMV67hN1AmbXsK4yaqU7tjiHlbxRDZOpH0KW9+CeX4bRAaX0Anxt0tx2MrpRpWwQaPwIlISEJhYU5Pw==", 1627 1709 "dev": true, 1628 1710 "license": "MIT" 1711 + }, 1712 + "node_modules/binary-extensions": { 1713 + "version": "2.3.0", 1714 + "resolved": "https://registry.npmjs.org/binary-extensions/-/binary-extensions-2.3.0.tgz", 1715 + "integrity": "sha512-Ceh+7ox5qe7LJuLHoY0feh3pHuUDHAcRUeyL2VYghZwfpkNIy/+8Ocg0a3UuSoYzavmylwuLWQOf3hl0jjMMIw==", 1716 + "dev": true, 1717 + "license": "MIT", 1718 + "engines": { 1719 + "node": ">=8" 1720 + }, 1721 + "funding": { 1722 + "url": "https://github.com/sponsors/sindresorhus" 1723 + } 1629 1724 }, 1630 1725 "node_modules/brace-expansion": { 1631 1726 "version": "1.1.12", ··· 1678 1773 "url": "https://github.com/chalk/chalk?sponsor=1" 1679 1774 } 1680 1775 }, 1776 + "node_modules/chokidar": { 1777 + "version": "3.6.0", 1778 + "resolved": "https://registry.npmjs.org/chokidar/-/chokidar-3.6.0.tgz", 1779 + "integrity": "sha512-7VT13fmjotKpGipCW9JEQAusEPE+Ei8nl6/g4FBAmIm0GOOLMua9NDDo/DWp0ZAxCr3cPq5ZpBqmPAQgDda2Pw==", 1780 + "dev": true, 1781 + "license": "MIT", 1782 + "dependencies": { 1783 + "anymatch": "~3.1.2", 1784 + "braces": "~3.0.2", 1785 + "glob-parent": "~5.1.2", 1786 + "is-binary-path": "~2.1.0", 1787 + "is-glob": "~4.0.1", 1788 + "normalize-path": "~3.0.0", 1789 + "readdirp": "~3.6.0" 1790 + }, 1791 + "engines": { 1792 + "node": ">= 8.10.0" 1793 + }, 1794 + "funding": { 1795 + "url": "https://paulmillr.com/funding/" 1796 + }, 1797 + "optionalDependencies": { 1798 + "fsevents": "~2.3.2" 1799 + } 1800 + }, 1801 + "node_modules/chokidar/node_modules/glob-parent": { 1802 + "version": "5.1.2", 1803 + "resolved": "https://registry.npmjs.org/glob-parent/-/glob-parent-5.1.2.tgz", 1804 + "integrity": "sha512-AOIgSQCepiJYwP3ARnGx+5VnTu2HBYdzbGP45eLw1vr3zB3vZLeyed1sC9hnbcOc9/SrMyM5RPQrkGz4aS9Zow==", 1805 + "dev": true, 1806 + "license": "ISC", 1807 + "dependencies": { 1808 + "is-glob": "^4.0.1" 1809 + }, 1810 + "engines": { 1811 + "node": ">= 6" 1812 + } 1813 + }, 1681 1814 "node_modules/color-convert": { 1682 1815 "version": "2.0.1", 1683 1816 "resolved": "https://registry.npmjs.org/color-convert/-/color-convert-2.0.1.tgz", ··· 1695 1828 "version": "1.1.4", 1696 1829 "resolved": "https://registry.npmjs.org/color-name/-/color-name-1.1.4.tgz", 1697 1830 "integrity": "sha512-dOy+3AuW3a2wNbZHIuMZpTcgjGuLU/uBL/ubcZF9OXbDo8ff4O8yVp5Bf0efS8uEoYo5q4Fx7dY9OgQGXgAsQA==", 1831 + "dev": true, 1832 + "license": "MIT" 1833 + }, 1834 + "node_modules/colorette": { 1835 + "version": "2.0.20", 1836 + "resolved": "https://registry.npmjs.org/colorette/-/colorette-2.0.20.tgz", 1837 + "integrity": "sha512-IfEDxwoWIjkeXL1eXcDiow4UbKjhLdq6/EuSVR9GMN7KVH3r9gQ83e73hsz1Nd1T3ijd5xv1wcWRYO+D6kCI2w==", 1698 1838 "dev": true, 1699 1839 "license": "MIT" 1700 1840 }, ··· 1751 1891 "integrity": "sha512-oIPzksmTg4/MriiaYGO+okXDT7ztn/w3Eptv/+gSIdMdKsJo0u4CfYNFJPy+4SKMuCqGw2wxnA+URMg3t8a/bQ==", 1752 1892 "dev": true, 1753 1893 "license": "MIT" 1894 + }, 1895 + "node_modules/diff": { 1896 + "version": "5.2.0", 1897 + "resolved": "https://registry.npmjs.org/diff/-/diff-5.2.0.tgz", 1898 + "integrity": "sha512-uIFDxqpRZGZ6ThOk84hEfqWoHx2devRFvpTZcTHur85vImfaxUbTW9Ryh4CpCuDnToOP1CEtXKIgytHBPVff5A==", 1899 + "dev": true, 1900 + "license": "BSD-3-Clause", 1901 + "engines": { 1902 + "node": ">=0.3.1" 1903 + } 1754 1904 }, 1755 1905 "node_modules/esbuild": { 1756 1906 "version": "0.25.5", ··· 2150 2300 "url": "https://github.com/sponsors/sindresorhus" 2151 2301 } 2152 2302 }, 2303 + "node_modules/globby": { 2304 + "version": "14.1.0", 2305 + "resolved": "https://registry.npmjs.org/globby/-/globby-14.1.0.tgz", 2306 + "integrity": "sha512-0Ia46fDOaT7k4og1PDW4YbodWWr3scS2vAr2lTbsplOt2WkKp0vQbkI9wKis/T5LV/dqPjO3bpS/z6GTJB82LA==", 2307 + "dev": true, 2308 + "license": "MIT", 2309 + "dependencies": { 2310 + "@sindresorhus/merge-streams": "^2.1.0", 2311 + "fast-glob": "^3.3.3", 2312 + "ignore": "^7.0.3", 2313 + "path-type": "^6.0.0", 2314 + "slash": "^5.1.0", 2315 + "unicorn-magic": "^0.3.0" 2316 + }, 2317 + "engines": { 2318 + "node": ">=18" 2319 + }, 2320 + "funding": { 2321 + "url": "https://github.com/sponsors/sindresorhus" 2322 + } 2323 + }, 2324 + "node_modules/globby/node_modules/ignore": { 2325 + "version": "7.0.5", 2326 + "resolved": "https://registry.npmjs.org/ignore/-/ignore-7.0.5.tgz", 2327 + "integrity": "sha512-Hs59xBNfUIunMFgWAbGX5cq6893IbWg4KnrjbYwX3tx0ztorVgTDA6B2sxf8ejHJ4wz8BqGUMYlnzNBer5NvGg==", 2328 + "dev": true, 2329 + "license": "MIT", 2330 + "engines": { 2331 + "node": ">= 4" 2332 + } 2333 + }, 2153 2334 "node_modules/graphemer": { 2154 2335 "version": "1.4.0", 2155 2336 "resolved": "https://registry.npmjs.org/graphemer/-/graphemer-1.4.0.tgz", ··· 2202 2383 "license": "MIT", 2203 2384 "engines": { 2204 2385 "node": ">=0.8.19" 2386 + } 2387 + }, 2388 + "node_modules/is-binary-path": { 2389 + "version": "2.1.0", 2390 + "resolved": "https://registry.npmjs.org/is-binary-path/-/is-binary-path-2.1.0.tgz", 2391 + "integrity": "sha512-ZMERYes6pDydyuGidse7OsHxtbI7WVeUEozgR/g7rd0xUimYNlvZRE/K2MgZTjWy725IfelLeVcEM97mmtRGXw==", 2392 + "dev": true, 2393 + "license": "MIT", 2394 + "dependencies": { 2395 + "binary-extensions": "^2.0.0" 2396 + }, 2397 + "engines": { 2398 + "node": ">=8" 2205 2399 } 2206 2400 }, 2207 2401 "node_modules/is-extglob": { ··· 2395 2589 "dev": true, 2396 2590 "license": "MIT" 2397 2591 }, 2592 + "node_modules/normalize-path": { 2593 + "version": "3.0.0", 2594 + "resolved": "https://registry.npmjs.org/normalize-path/-/normalize-path-3.0.0.tgz", 2595 + "integrity": "sha512-6eZs5Ls3WtCisHWp9S2GUy8dqkpGi4BVSz3GaqiE6ezub0512ESztXUwUB6C6IKbQkY2Pnb/mD4WYojCRwcwLA==", 2596 + "dev": true, 2597 + "license": "MIT", 2598 + "engines": { 2599 + "node": ">=0.10.0" 2600 + } 2601 + }, 2602 + "node_modules/onchange": { 2603 + "version": "7.1.0", 2604 + "resolved": "https://registry.npmjs.org/onchange/-/onchange-7.1.0.tgz", 2605 + "integrity": "sha512-ZJcqsPiWUAUpvmnJri5TPBooqJOPmC0ttN65juhN15Q8xA+Nbg3BaxBHXQ45EistKKlKElb0edmbPWnKSBkvMg==", 2606 + "dev": true, 2607 + "license": "MIT", 2608 + "dependencies": { 2609 + "@blakeembrey/deque": "^1.0.5", 2610 + "@blakeembrey/template": "^1.0.0", 2611 + "arg": "^4.1.3", 2612 + "chokidar": "^3.3.1", 2613 + "cross-spawn": "^7.0.1", 2614 + "ignore": "^5.1.4", 2615 + "tree-kill": "^1.2.2" 2616 + }, 2617 + "bin": { 2618 + "onchange": "dist/bin.js" 2619 + } 2620 + }, 2398 2621 "node_modules/optionator": { 2399 2622 "version": "0.9.4", 2400 2623 "resolved": "https://registry.npmjs.org/optionator/-/optionator-0.9.4.tgz", ··· 2478 2701 "node": ">=8" 2479 2702 } 2480 2703 }, 2704 + "node_modules/path-type": { 2705 + "version": "6.0.0", 2706 + "resolved": "https://registry.npmjs.org/path-type/-/path-type-6.0.0.tgz", 2707 + "integrity": "sha512-Vj7sf++t5pBD637NSfkxpHSMfWaeig5+DKWLhcqIYx6mWQz5hdJTGDVMQiJcw1ZYkhs7AazKDGpRVji1LJCZUQ==", 2708 + "dev": true, 2709 + "license": "MIT", 2710 + "engines": { 2711 + "node": ">=18" 2712 + }, 2713 + "funding": { 2714 + "url": "https://github.com/sponsors/sindresorhus" 2715 + } 2716 + }, 2481 2717 "node_modules/picocolors": { 2482 2718 "version": "1.1.1", 2483 2719 "resolved": "https://registry.npmjs.org/picocolors/-/picocolors-1.1.1.tgz", ··· 2537 2773 "node": ">= 0.8.0" 2538 2774 } 2539 2775 }, 2776 + "node_modules/pta": { 2777 + "version": "1.3.0", 2778 + "resolved": "https://registry.npmjs.org/pta/-/pta-1.3.0.tgz", 2779 + "integrity": "sha512-afFDASgSVTaxqxMPvbFq2O36baoJ72Nwh42MWRyLO52YZsmtgpkzIkm2hgCIrz0Gvks6lu5Syxd+SXJ1EDFDpA==", 2780 + "dev": true, 2781 + "license": "MIT", 2782 + "dependencies": { 2783 + "arg": "^5.0.2", 2784 + "globby": "^14.0.0", 2785 + "zora-reporters": "*" 2786 + }, 2787 + "bin": { 2788 + "pta": "src/bin.js" 2789 + }, 2790 + "peerDependencies": { 2791 + "zora": "^6" 2792 + } 2793 + }, 2794 + "node_modules/pta/node_modules/arg": { 2795 + "version": "5.0.2", 2796 + "resolved": "https://registry.npmjs.org/arg/-/arg-5.0.2.tgz", 2797 + "integrity": "sha512-PYjyFOLKQ9y57JvQ6QLo8dAgNqswh8M1RMJYdQduT6xbWSgK36P/Z/v+p888pM69jMMfS8Xd8F6I1kQ/I9HUGg==", 2798 + "dev": true, 2799 + "license": "MIT" 2800 + }, 2540 2801 "node_modules/punycode": { 2541 2802 "version": "2.3.1", 2542 2803 "resolved": "https://registry.npmjs.org/punycode/-/punycode-2.3.1.tgz", ··· 2587 2848 }, 2588 2849 "peerDependencies": { 2589 2850 "react": "^19.1.0" 2851 + } 2852 + }, 2853 + "node_modules/readdirp": { 2854 + "version": "3.6.0", 2855 + "resolved": "https://registry.npmjs.org/readdirp/-/readdirp-3.6.0.tgz", 2856 + "integrity": "sha512-hOS089on8RduqdbhvQ5Z37A0ESjsqz6qnRcffsMU3495FuTdqSm+7bhJ29JvIOsBDEEnan5DPu9t3To9VRlMzA==", 2857 + "dev": true, 2858 + "license": "MIT", 2859 + "dependencies": { 2860 + "picomatch": "^2.2.1" 2861 + }, 2862 + "engines": { 2863 + "node": ">=8.10.0" 2590 2864 } 2591 2865 }, 2592 2866 "node_modules/rescript": { ··· 2738 3012 "node": ">=8" 2739 3013 } 2740 3014 }, 3015 + "node_modules/slash": { 3016 + "version": "5.1.0", 3017 + "resolved": "https://registry.npmjs.org/slash/-/slash-5.1.0.tgz", 3018 + "integrity": "sha512-ZA6oR3T/pEyuqwMgAKT0/hAv8oAXckzbkmR0UkUosQ+Mc4RxGoJkRmwHgHufaenlyAgE1Mxgpdcrf75y6XcnDg==", 3019 + "dev": true, 3020 + "license": "MIT", 3021 + "engines": { 3022 + "node": ">=14.16" 3023 + }, 3024 + "funding": { 3025 + "url": "https://github.com/sponsors/sindresorhus" 3026 + } 3027 + }, 2741 3028 "node_modules/source-map-js": { 2742 3029 "version": "1.2.1", 2743 3030 "resolved": "https://registry.npmjs.org/source-map-js/-/source-map-js-1.2.1.tgz", ··· 2830 3117 }, 2831 3118 "engines": { 2832 3119 "node": ">=8.0" 3120 + } 3121 + }, 3122 + "node_modules/tree-kill": { 3123 + "version": "1.2.2", 3124 + "resolved": "https://registry.npmjs.org/tree-kill/-/tree-kill-1.2.2.tgz", 3125 + "integrity": "sha512-L0Orpi8qGpRG//Nd+H90vFB+3iHnue1zSSGmNOOCh1GLJ7rUKVwV2HvijphGQS2UmhUZewS9VgvxYIdgr+fG1A==", 3126 + "dev": true, 3127 + "license": "MIT", 3128 + "bin": { 3129 + "tree-kill": "cli.js" 2833 3130 } 2834 3131 }, 2835 3132 "node_modules/ts-api-utils": { ··· 2895 3192 "typescript": ">=4.8.4 <5.9.0" 2896 3193 } 2897 3194 }, 3195 + "node_modules/unicorn-magic": { 3196 + "version": "0.3.0", 3197 + "resolved": "https://registry.npmjs.org/unicorn-magic/-/unicorn-magic-0.3.0.tgz", 3198 + "integrity": "sha512-+QBBXBCvifc56fsbuxZQ6Sic3wqqc3WWaqxs58gvJrcOuN83HGTCwz3oS5phzU9LthRNE9VrJCFCLUgHeeFnfA==", 3199 + "dev": true, 3200 + "license": "MIT", 3201 + "engines": { 3202 + "node": ">=18" 3203 + }, 3204 + "funding": { 3205 + "url": "https://github.com/sponsors/sindresorhus" 3206 + } 3207 + }, 2898 3208 "node_modules/uri-js": { 2899 3209 "version": "4.4.1", 2900 3210 "resolved": "https://registry.npmjs.org/uri-js/-/uri-js-4.4.1.tgz", ··· 3046 3356 "funding": { 3047 3357 "url": "https://github.com/sponsors/sindresorhus" 3048 3358 } 3359 + }, 3360 + "node_modules/zora": { 3361 + "version": "6.0.0", 3362 + "resolved": "https://registry.npmjs.org/zora/-/zora-6.0.0.tgz", 3363 + "integrity": "sha512-uDOZ5VwwURiU9B+5BY5z/ByM9WWC1A5SJpEBg0HL9Qy2zsKnzfizsa+ABWZFJ8onGN1MU2evzAGAuAxybjoYEQ==", 3364 + "dev": true, 3365 + "license": "MIT", 3366 + "peer": true 3367 + }, 3368 + "node_modules/zora-reporters": { 3369 + "version": "2.0.0", 3370 + "resolved": "https://registry.npmjs.org/zora-reporters/-/zora-reporters-2.0.0.tgz", 3371 + "integrity": "sha512-A0Pod5kIlKGGbQDc7tBefMH/vgoQnu2CHdSFp/gZ7ZYlpK86GrwD3BTcPFLmGDxe8igeOnvT0cnPv2pi2qsjIQ==", 3372 + "dev": true, 3373 + "license": "MIT", 3374 + "dependencies": { 3375 + "arg": "^5.0.2", 3376 + "colorette": "^2.0.20", 3377 + "diff": "^5.1.0" 3378 + }, 3379 + "bin": { 3380 + "zr": "src/bin.js" 3381 + } 3382 + }, 3383 + "node_modules/zora-reporters/node_modules/arg": { 3384 + "version": "5.0.2", 3385 + "resolved": "https://registry.npmjs.org/arg/-/arg-5.0.2.tgz", 3386 + "integrity": "sha512-PYjyFOLKQ9y57JvQ6QLo8dAgNqswh8M1RMJYdQduT6xbWSgK36P/Z/v+p888pM69jMMfS8Xd8F6I1kQ/I9HUGg==", 3387 + "dev": true, 3388 + "license": "MIT" 3049 3389 } 3050 3390 } 3051 3391 }

+1 -1

package.json

··· 12 12 "res:clean": "rescript clean", 13 13 "res:dev": "rescript -w", 14 14 "res:format": "rescript format -all", 15 - "test": "pta 'tests/*.mjs'", 15 + "test": "npm run res:build && pta 'tests/*.mjs'", 16 16 "test-watch": "onchange --initial '{tests,src}/*.mjs' -- pta 'tests/*.mjs'" 17 17 }, 18 18 "dependencies": {

+2 -1

src/AxiomSet.res

··· 22 22 let ret = ref(Error("impossible")) 23 23 while go.contents { 24 24 switch Rule.parseTopLevel(cur.contents, ~scope=[]) { 25 - | Ok((t, n), rest) => if n->String.trim == "" { 25 + | Ok((t, n), rest) => 26 + if n->String.trim == "" { 26 27 go := false 27 28 ret := Error("Rule given with no name") 28 29 } else {

+674

src/HOTerm.res

··· 1 + open Util 2 + module IntCmp = Belt.Id.MakeComparable({ 3 + type t = int 4 + let cmp = Pervasives.compare 5 + }) 6 + 7 + type rec t = 8 + | Symbol({name: string}) 9 + | Var({idx: int}) 10 + | Schematic({schematic: int}) 11 + | Lam({name: string, body: t}) 12 + | App({func: t, arg: t}) 13 + // Unallowed is used internally in unify, where Nipkow 1993 uses Var(-infinity) 14 + | Unallowed 15 + type meta = string 16 + type schematic = int 17 + type subst = Belt.Map.Int.t<t> 18 + let substHas = (subst: subst, schematic: schematic) => subst->Belt.Map.Int.has(schematic) 19 + let substGet = (subst: subst, schematic: schematic) => subst->Belt.Map.Int.get(schematic) 20 + let mapSubst = (m: subst, f: t => t): subst => { 21 + m->Belt.Map.Int.map(f) 22 + } 23 + let rec equivalent = (a: t, b: t) => { 24 + switch (a, b) { 25 + | (Symbol({name: na}), Symbol({name: nb})) => na == nb 26 + | (Var({idx: ia}), Var({idx: ib})) => ia == ib 27 + | (Schematic({schematic: sa}), Schematic({schematic: sb})) => sa == sb 28 + | (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => equivalent(ba, bb) 29 + | (App({func: fa, arg: aa}), App({func: fb, arg: ab})) => equivalent(fa, fb) && equivalent(aa, ab) 30 + | (_, _) => false 31 + } 32 + } 33 + type gen = ref<int> 34 + let seen = (g: gen, s: int) => { 35 + if s >= g.contents { 36 + g := s + 1 37 + } 38 + } 39 + let fresh = (g: gen, ~replacing as _=?) => { 40 + let v = g.contents 41 + g := g.contents + 1 42 + v 43 + } 44 + let rec schematicsIn = (subst: subst, it: t): Belt.Set.t<schematic, IntCmp.identity> => 45 + switch it { 46 + | Schematic({schematic, _}) if subst->substHas(schematic) => 47 + let found = subst->substGet(schematic)->Option.getExn 48 + schematicsIn(subst, found) 49 + | Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic) 50 + | Lam({body}) => schematicsIn(subst, body) 51 + | App({func, arg}) => Belt.Set.union(schematicsIn(subst, func), schematicsIn(subst, arg)) 52 + | Unallowed | Symbol(_) | Var(_) => Belt.Set.make(~id=module(IntCmp)) 53 + } 54 + let occ = (schematic: schematic, subst: subst, t: t): bool => { 55 + let set = schematicsIn(subst, t) 56 + set->Belt.Set.has(schematic) 57 + } 58 + let rec freeVarsIn = (subst: subst, it: t): Belt.Set.t<int, IntCmp.identity> => 59 + switch it { 60 + | Schematic({schematic, _}) if subst->substHas(schematic) => 61 + let found = subst->substGet(schematic)->Option.getExn 62 + freeVarsIn(subst, found) 63 + | Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx) 64 + | Lam({name: _, body}) => 65 + freeVarsIn(subst, body) 66 + ->Belt.Set.toArray 67 + ->Array.filterMap(v => 68 + if v >= 1 { 69 + Some(v - 1) 70 + } else { 71 + None 72 + } 73 + ) 74 + ->Belt.Set.fromArray(~id=module(IntCmp)) 75 + | App({func, arg}) => Belt.Set.union(freeVarsIn(subst, func), freeVarsIn(subst, arg)) 76 + | Unallowed | Symbol(_) | Schematic(_) => Belt.Set.make(~id=module(IntCmp)) 77 + } 78 + let freeVarsContains = (term: t, subst: subst, idx: int): bool => { 79 + let set = freeVarsIn(subst, term) 80 + set->Belt.Set.has(idx) 81 + } 82 + // f might map an index to a new one or to a term. when mapping to a term the real index without shifting is passed 83 + let rec mapbind0 = (term: t, f: int => result<int, int => t>, ~from: int=0): t => 84 + switch term { 85 + | Symbol(_) => term 86 + | Var({idx}) => 87 + if idx >= from { 88 + switch f(idx - from) { 89 + | Ok(newIdx) => 90 + let new = newIdx + from 91 + if new < 0 { 92 + raise(Err("mapbind: negative index")) 93 + } 94 + Var({ 95 + idx: new, 96 + }) 97 + | Error(t) => t(from) 98 + } 99 + } else { 100 + term 101 + } 102 + | Schematic({schematic}) => 103 + Schematic({ 104 + schematic: schematic, 105 + }) 106 + | Lam({name, body}) => 107 + Lam({ 108 + name, 109 + body: mapbind0(body, f, ~from=from + 1), 110 + }) 111 + | App({func, arg}) => 112 + App({ 113 + func: mapbind0(func, f, ~from), 114 + arg: mapbind0(arg, f, ~from), 115 + }) 116 + | Unallowed => Unallowed 117 + } 118 + let mapbind = (term: t, f: int => int, ~from: int=0): t => mapbind0(term, idx => Ok(f(idx)), ~from) 119 + let upshift = (term: t, amount: int, ~from: int=0) => mapbind(term, idx => idx + amount, ~from) 120 + let downshift = (term: t, amount: int, ~from: int=1) => { 121 + if amount > from { 122 + raise(Err("downshift amount must be less than from")) 123 + } 124 + mapbind(term, idx => idx - amount, ~from) 125 + } 126 + let emptySubst: subst = Belt.Map.Int.empty 127 + let substAdd = (subst: subst, schematic: schematic, term: t) => { 128 + assert(schematic >= 0) 129 + assert(subst->Belt.Map.Int.has(schematic) == false) 130 + subst->Belt.Map.Int.set(schematic, term) 131 + } 132 + let rec substitute = (term: t, subst: subst) => 133 + switch term { 134 + | Schematic({schematic, _}) => 135 + switch Belt.Map.Int.get(subst, schematic) { 136 + | None => term 137 + | Some(found) => found 138 + } 139 + | Lam({name, body}) => 140 + Lam({ 141 + name, 142 + // upshift is not needed for pattern unification, but it is safer to have upshift here 143 + body: substitute(body, subst->Belt.Map.Int.map(t => upshift(t, 1))), 144 + }) 145 + | App({func, arg}) => 146 + App({ 147 + func: substitute(func, subst), 148 + arg: substitute(arg, subst), 149 + }) 150 + | Var(_) | Unallowed | Symbol(_) => term 151 + } 152 + // TODO: check how will this interact with meta variables (schematics) and check if it is needed to have a subst parameter - it should not be needed for subst produced by pattern unification 153 + let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) => 154 + switch term { 155 + | Symbol(_) => term 156 + | Var({idx: var}) => 157 + if var < from { 158 + term 159 + } else if var - from < Array.length(substs) && var - from >= 0 { 160 + Option.getExn(substs[var - from]) 161 + } else { 162 + Var({idx: var - Array.length(substs)}) 163 + } 164 + | Schematic({schematic}) => 165 + Schematic({ 166 + schematic: schematic, 167 + }) 168 + | Lam({name, body}) => 169 + Lam({ 170 + name, 171 + body: substDeBruijn(body, substs->Array.map(term => upshift(term, 1)), ~from=from + 1), 172 + }) 173 + | App({func, arg}) => 174 + App({ 175 + func: substDeBruijn(func, substs, ~from), 176 + arg: substDeBruijn(arg, substs, ~from), 177 + }) 178 + | Unallowed => Unallowed 179 + } 180 + // beta reduced and eta reduced 181 + let rec reduceFull = (term: t, subst: subst): t => { 182 + switch term { 183 + | Schematic({schematic}) if subst->substHas(schematic) => 184 + let found = subst->substGet(schematic)->Option.getExn 185 + reduceFull(found, subst) 186 + | Lam({body: App({func, arg: Var({idx: 0})})}) if !(func->freeVarsContains(subst, 0)) => 187 + reduceFull(downshift(func, 1), subst) 188 + | App({func, arg}) => 189 + switch reduceFull(func, subst) { 190 + | Lam({body}) => reduceFull(substDeBruijn(body, [arg]), subst) 191 + | func => App({func, arg: reduceFull(arg, subst)}) 192 + } 193 + | Lam({name, body}) => 194 + Lam({ 195 + name, 196 + body: reduceFull(body, subst), 197 + }) 198 + | Symbol(_) | Var(_) | Schematic(_) => term 199 + 200 + | Unallowed => Unallowed 201 + } 202 + } 203 + let reduceSubst = (subst: subst): subst => { 204 + subst->Belt.Map.Int.map(x => reduceFull(x, subst)) 205 + } 206 + let rec lams = (amount: int, term: t): t => { 207 + assert(amount >= 0) 208 + if amount <= 0 { 209 + term 210 + } else { 211 + Lam({ 212 + name: "x", 213 + body: lams(amount - 1, term), 214 + }) 215 + } 216 + } 217 + let rec idx = (is: array<t>, j: int): option<int> => { 218 + if is->Array.length == 0 { 219 + None 220 + } else { 221 + let head = is[0]->Option.getExn 222 + let tail = is->Array.sliceToEnd(~start=1) 223 + if equivalent(head, Var({idx: j})) { 224 + Some(tail->Array.length) 225 + } else { 226 + idx(tail, j) 227 + } 228 + } 229 + } 230 + let idx1 = (is: array<t>, j: int): t => { 231 + switch idx(is, j) { 232 + | None => Unallowed 233 + | Some(idx) => Var({idx: idx}) 234 + } 235 + } 236 + let idx2 = (is: array<t>, j: int): result<int, int => t> => { 237 + switch idx(is, j) { 238 + | None => Error(_ => Unallowed) 239 + | Some(idx) => Ok(idx) 240 + } 241 + } 242 + let rec app = (term: t, args: array<t>): t => { 243 + if args->Array.length == 0 { 244 + term 245 + } else { 246 + let head = args[0]->Option.getExn 247 + let rest = args->Array.sliceToEnd(~start=1) 248 + app(App({func: term, arg: head}), rest) 249 + } 250 + } 251 + exception UnifyFail(string) 252 + let isvar = (term: t): bool => 253 + switch term { 254 + | Var(_) => true 255 + | _ => false 256 + } 257 + let rec red = (term: t, is: array<t>, js: array<t>): t => { 258 + switch term { 259 + | Lam({name, body}) if is->Array.length > 0 && isvar(is[0]->Option.getExn) => { 260 + let head = is[0]->Option.getExn 261 + let rest = is->Array.sliceToEnd(~start=1) 262 + red(body, rest, Array.concat([head], js)) 263 + } 264 + | _ => 265 + app( 266 + term->mapbind(k => 267 + switch js[k]->Option.getExn { 268 + | Var({idx}) => idx 269 + | _ => raise(UnifyFail("expected variable in red")) 270 + } 271 + ), 272 + is, 273 + ) 274 + } 275 + } 276 + // app with beta reduction 277 + let rec app1 = (term: t, args: array<t>): t => 278 + if args->Array.length == 0 { 279 + term 280 + } else { 281 + let head = args[0]->Option.getExn 282 + let rest = args->Array.sliceToEnd(~start=1) 283 + switch term { 284 + | Lam({body}) => app1(substDeBruijn(body, [head]), rest) 285 + | _ => app1(App({func: term, arg: head}), rest) 286 + } 287 + } 288 + let lam = (is: array<t>, g: t, js: array<int>): t => { 289 + lams(is->Array.length, app(g, js->Array.map(j => idx1(is, j)))) 290 + } 291 + let rec strip = (term: t): (t, array<t>) => { 292 + switch term { 293 + | App({func, arg}) => 294 + let (peeledFunc, peeledArgs) = strip(func) 295 + (peeledFunc, Array.concat(peeledArgs, [arg])) 296 + | _ => (term, []) 297 + } 298 + } 299 + let rec devar = (subst: subst, term: t): t => { 300 + let (func, args) = strip(term) 301 + switch func { 302 + | Schematic({schematic}) if substHas(subst, schematic) => 303 + devar(subst, red(substGet(subst, schematic)->Option.getExn, args, [])) 304 + | _ => term 305 + } 306 + } 307 + let rec proj = (subst: subst, term: t, ~gen: option<gen>): subst => { 308 + switch strip(devar(subst, term)) { 309 + | (Lam({name, body}), args) if args->Array.length == 0 => proj(subst, body, ~gen) 310 + | (Unallowed, args) => raise(UnifyFail("unallowed")) 311 + | (Symbol(_) | Var(_), args) => Array.reduce(args, subst, (acc, a) => proj(acc, a, ~gen)) 312 + | (Schematic({schematic}), args) => { 313 + assert(!substHas(subst, schematic)) 314 + if gen->Option.isNone { 315 + raise(UnifyFail("no gen provided")) 316 + } 317 + let h = Schematic({schematic: fresh(Option.getExn(gen))}) 318 + subst->substAdd( 319 + schematic, 320 + lams( 321 + args->Array.length, 322 + app( 323 + h, 324 + Belt.Array.init(args->Array.length, j => { 325 + switch args[j]->Option.getExn { 326 + | Var({idx}) => Some(Var({idx: args->Belt.Array.length - j - 1})) 327 + | _ => None 328 + } 329 + })->Array.keepSome, 330 + ), 331 + ), 332 + ) 333 + } 334 + | _ => raise(UnifyFail("not a symbol, var or schematic")) 335 + } 336 + } 337 + let flexflex = ( 338 + sa: schematic, 339 + xs: array<t>, 340 + sb: schematic, 341 + ys: array<t>, 342 + subst: subst, 343 + ~gen: option<gen>, 344 + ): subst => { 345 + if sa == sb { 346 + if xs->Array.length != ys->Array.length { 347 + raise(UnifyFail("flexible schematics have different number of arguments")) 348 + } 349 + if gen->Option.isNone { 350 + raise(UnifyFail("no gen provided")) 351 + } 352 + let len = xs->Array.length 353 + let h = Schematic({schematic: fresh(Option.getExn(gen))}) 354 + let xs = Belt.Array.init(len, k => { 355 + let a = xs[k]->Option.getExn 356 + let b = ys[k]->Option.getExn 357 + switch (a, b) { 358 + | (Var(_), Var(_)) if equivalent(a, b) => Some(Var({idx: len - k - 1})) 359 + | _ => None 360 + } 361 + })->Array.keepSome 362 + subst->substAdd(sa, lams(len, app(h, xs))) 363 + } else { 364 + let y_vars = Belt.Set.fromArray( 365 + ys->Array.filterMap(y => 366 + switch y { 367 + | Var({idx}) => Some(idx) 368 + | _ => None 369 + } 370 + ), 371 + ~id=module(IntCmp), 372 + ) 373 + let common = xs->Array.filterMap(x => 374 + switch x { 375 + | Var({idx}) if y_vars->Belt.Set.has(idx) => Some(idx) 376 + | _ => None 377 + } 378 + ) 379 + let h = Schematic({schematic: fresh(Option.getExn(gen))}) 380 + subst->substAdd(sa, lam(xs, h, common))->substAdd(sb, lam(ys, h, common)) 381 + } 382 + } 383 + let flexrigid = (sa: schematic, xs: array<t>, b: t, subst: subst, ~gen: option<gen>): subst => { 384 + if occ(sa, subst, b) { 385 + raise(UnifyFail("flexible schematic occurs in rigid term")) 386 + } 387 + let u = b->mapbind0(bind => idx2(xs, bind)) 388 + proj(subst->substAdd(sa, lams(xs->Array.length, u)), u, ~gen) 389 + } 390 + let rec unifyTerm = (a: t, b: t, subst: subst, ~gen: option<gen>): subst => 391 + switch (devar(subst, a), devar(subst, b)) { 392 + | (Symbol({name: na}), Symbol({name: nb})) => 393 + if na == nb { 394 + subst 395 + } else { 396 + raise(UnifyFail("symbols do not match")) 397 + } 398 + | (Var({idx: ia}), Var({idx: ib})) => 399 + if ia == ib { 400 + subst 401 + } else { 402 + raise(UnifyFail("variables do not match")) 403 + } 404 + | (Schematic({schematic: sa}), Schematic({schematic: sb})) if sa == sb => subst 405 + | (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => unifyTerm(ba, bb, subst, ~gen) 406 + | (Lam({name: _, body: ba}), b) => 407 + unifyTerm(ba, App({func: upshift(b, 1), arg: Var({idx: 0})}), subst, ~gen) 408 + | (a, Lam({name: _, body: bb})) => 409 + unifyTerm(App({func: upshift(a, 1), arg: Var({idx: 0})}), bb, subst, ~gen) 410 + | (_, _) => 411 + switch (strip(a), strip(b)) { 412 + | ((Schematic({schematic: sa}), xs), (Schematic({schematic: sb}), ys)) => 413 + flexflex(sa, xs, sb, ys, subst, ~gen) 414 + | ((Schematic({schematic: sa}), xs), _) => flexrigid(sa, xs, b, subst, ~gen) 415 + | (_, (Schematic({schematic: sb}), ys)) => flexrigid(sb, ys, a, subst, ~gen) 416 + | ((a, xs), (b, ys)) => rigidrigid(a, xs, b, ys, subst, ~gen) 417 + | (_, _) => raise(UnifyFail("no rules match")) 418 + } 419 + } 420 + and unifyArray = (xs: array<t>, ys: array<t>, subst: subst, ~gen: option<gen>): subst => { 421 + if xs->Array.length != ys->Array.length { 422 + raise(UnifyFail("arrays have different lengths")) 423 + } 424 + Belt.Array.zip(xs, ys)->Belt.Array.reduce(subst, (acc, (x, y)) => unifyTerm(x, y, acc, ~gen)) 425 + } 426 + and rigidrigid = ( 427 + a: t, 428 + xs: array<t>, 429 + b: t, 430 + ys: array<t>, 431 + subst: subst, 432 + ~gen: option<gen>, 433 + ): subst => { 434 + if !equivalent(a, b) { 435 + raise(UnifyFail("rigid terms do not match")) 436 + } 437 + if xs->Array.length != ys->Array.length { 438 + raise(UnifyFail("rigid terms have different number of arguments")) 439 + } 440 + unifyArray(xs, ys, subst, ~gen) 441 + } 442 + let unify = (a: t, b: t, ~gen=?) => { 443 + try { 444 + [unifyTerm(a, b, emptySubst, ~gen)] 445 + } catch { 446 + | UnifyFail(_) => [] 447 + } 448 + } 449 + let place = (x: int, ~scope: array<string>) => Schematic({ 450 + schematic: x, 451 + }) 452 + let prettyPrintVar = (idx: int, scope: array<string>) => 453 + switch scope[idx] { 454 + | Some(n) if Array.indexOf(scope, n) == idx => n 455 + | _ => "\\"->String.concat(String.make(idx)) 456 + } 457 + let makeGen = () => { 458 + ref(0) 459 + } 460 + let rec stripLam = (it: t): (array<string>, t) => 461 + switch it { 462 + | Lam({name, body}) => 463 + let (names, body) = stripLam(body) 464 + (Array.concat([name], names), body) 465 + | _ => ([], it) 466 + } 467 + let rec prettyPrint = (it: t, ~scope: array<string>) => 468 + switch it { 469 + | Symbol({name}) => name 470 + | Var({idx}) => prettyPrintVar(idx, scope) 471 + | Schematic({schematic}) => "?"->String.concat(String.make(schematic)) 472 + | Lam(_) => 473 + let (names, body) = stripLam(it) 474 + let (func, args) = strip(body) 475 + let bodies = Array.concat([func], args) 476 + let innerScope = Array.concat(Array.toReversed(names), scope) 477 + "(" 478 + ->String.concat(Array.join(names->Array.map(name => String.concat(name, ".")), " ")) 479 + ->String.concat(" ") 480 + ->String.concat(Array.join(bodies->Array.map(e => prettyPrint(e, ~scope=innerScope)), " ")) 481 + ->String.concat(")") 482 + | App(_) => 483 + let (func, args) = strip(it) 484 + "(" 485 + ->String.concat(prettyPrint(func, ~scope)) 486 + ->String.concat(" ") 487 + ->String.concat(Array.join(args->Array.map(e => prettyPrint(e, ~scope)), " ")) 488 + ->String.concat(")") 489 + | Unallowed => "" 490 + } 491 + let symbolRegexpString = "^([^\\s()]+)" 492 + let nameRES = "^([^\\s.\\[\\]()]+)\\." 493 + exception ParseError(string) 494 + type token = LParen | RParen | VarT(int) | SchematicT(int) | AtomT(string) | NameT(string) | EOF 495 + let varRegexpString = "^\\\\([0-9]+)" 496 + let schematicRegexpString = "^\\?([0-9]+)" 497 + let tokenize = (str0: string): (token, string) => { 498 + let str = str0->String.trimStart 499 + if str->String.length == 0 { 500 + (EOF, "") 501 + } else { 502 + let rest = () => str->String.sliceToEnd(~start=1) 503 + switch str->String.charAt(0) { 504 + | "(" => (LParen, rest()) 505 + | ")" => (RParen, rest()) 506 + | "\\" => { 507 + let re = RegExp.fromStringWithFlags(varRegexpString, ~flags="y") 508 + switch re->RegExp.exec(str) { 509 + | None => raise(ParseError("invalid variable")) 510 + | Some(res) => 511 + switch RegExp.Result.matches(res) { 512 + | [n] => ( 513 + VarT(n->Int.fromString->Option.getExn), 514 + String.sliceToEnd(str, ~start=RegExp.lastIndex(re)), 515 + ) 516 + | _ => raise(ParseError("invalid variable")) 517 + } 518 + } 519 + } 520 + | "?" => { 521 + let re = RegExp.fromStringWithFlags(schematicRegexpString, ~flags="y") 522 + switch re->RegExp.exec(str) { 523 + | None => raise(ParseError("invalid schematic")) 524 + | Some(res) => 525 + switch RegExp.Result.matches(res) { 526 + | [n] => ( 527 + SchematicT(n->Int.fromString->Option.getExn), 528 + String.sliceToEnd(str, ~start=RegExp.lastIndex(re)), 529 + ) 530 + | _ => raise(ParseError("invalid schematic")) 531 + } 532 + } 533 + } 534 + | _ => { 535 + let reName = RegExp.fromStringWithFlags(nameRES, ~flags="y") 536 + switch reName->RegExp.exec(str) { 537 + | Some(res) => 538 + switch RegExp.Result.matches(res) { 539 + | [n] => (NameT(n), String.sliceToEnd(str, ~start=RegExp.lastIndex(reName))) 540 + | _ => raise(ParseError("invalid symbol")) 541 + } 542 + | None => 543 + let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y") 544 + switch re->RegExp.exec(str) { 545 + | None => raise(ParseError("invalid symbol")) 546 + | Some(res) => 547 + switch RegExp.Result.matches(res) { 548 + | [n] => (AtomT(n), String.sliceToEnd(str, ~start=RegExp.lastIndex(re))) 549 + | _ => raise(ParseError("invalid symbol")) 550 + } 551 + } 552 + } 553 + } 554 + } 555 + } 556 + } 557 + type rec simple = 558 + | ListS({xs: array<simple>}) 559 + | AtomS({name: string}) 560 + | VarS({idx: int}) 561 + | SchematicS({schematic: int}) 562 + | LambdaS({name: string, body: simple}) 563 + let rec parseSimple = (str: string): (simple, string) => { 564 + let (t0, rest) = tokenize(str) 565 + switch t0 { 566 + | LParen => { 567 + let (t1, rest1) = tokenize(rest) 568 + switch t1 { 569 + | NameT(name) => { 570 + let (result, rest2) = parseSimple("("->String.concat(rest1)) 571 + (LambdaS({name, body: result}), rest2) 572 + } 573 + | RParen => (ListS({xs: []}), rest1) 574 + | _ => { 575 + let (head, rest2) = parseSimple(rest) 576 + let (tail, rest3) = parseSimple("("->String.concat(rest2)) 577 + switch tail { 578 + | ListS({xs}) => (ListS({xs: Array.concat([head], xs)}), rest3) 579 + | _ => raise(Unreachable("bug")) 580 + } 581 + } 582 + } 583 + } 584 + | RParen => raise(ParseError("unexpected right parenthesis")) 585 + | VarT(idx) => (VarS({idx: idx}), rest) 586 + | SchematicT(schematic) => (SchematicS({schematic: schematic}), rest) 587 + | AtomT(name) => (AtomS({name: name}), rest) 588 + | NameT(name) => { 589 + let (result, rest1) = parseSimple(rest) 590 + (LambdaS({name, body: result}), rest1) 591 + } 592 + | EOF => raise(ParseError("unexpected end of file")) 593 + } 594 + } 595 + type env = Map.t<string, int> 596 + let incrEnv = (env: env): env => { 597 + let nu: env = Map.make() 598 + Map.entries(env)->Iterator.forEach(opt => 599 + switch opt { 600 + | None => () 601 + | Some((key, value)) => nu->Map.set(key, value + 1) 602 + } 603 + ) 604 + nu 605 + } 606 + let envFromScope = (scope: array<string>): env => { 607 + let nu: env = Map.make() 608 + scope->Array.forEachWithIndex((name, idx) => { 609 + nu->Map.set(name, idx) 610 + }) 611 + nu 612 + } 613 + let envPushLambda = (env: env, name: string): env => { 614 + let nu = incrEnv(env) 615 + nu->Map.set(name, 0) 616 + nu 617 + } 618 + let rec parseAll = (simple: simple, ~env: env, ~gen=?): t => { 619 + switch simple { 620 + | ListS({xs}) => { 621 + let ts = xs->Array.map(x => parseAll(x, ~env, ~gen?)) 622 + if ts->Array.length == 0 { 623 + raise(ParseError("empty list")) 624 + } else { 625 + ts 626 + ->Array.sliceToEnd(~start=1) 627 + ->Array.reduce(ts[0]->Option.getExn, (acc, x) => App({func: acc, arg: x})) 628 + } 629 + } 630 + | AtomS({name}) => 631 + if env->Map.has(name) { 632 + let idx = env->Map.get(name)->Option.getExn 633 + Var({idx: idx}) 634 + } else { 635 + Symbol({name: name}) 636 + } 637 + | VarS({idx}) => Var({idx: idx}) 638 + | SchematicS({schematic}) => 639 + switch gen { 640 + | Some(g) => { 641 + seen(g, schematic) 642 + Schematic({schematic: schematic}) 643 + } 644 + | None => raise(ParseError("Schematics not allowed here")) 645 + } 646 + | LambdaS({name, body}) => 647 + Lam({ 648 + name, 649 + body: parseAll(body, ~env=envPushLambda(env, name), ~gen?), 650 + }) 651 + } 652 + } 653 + let prettyPrintMeta = (str: string) => { 654 + String.concat(str, ".") 655 + } 656 + let parseMeta = (str: string) => { 657 + let re = RegExp.fromStringWithFlags(nameRES, ~flags="y") 658 + switch re->RegExp.exec(str->String.trim) { 659 + | None => Error("not a meta name") 660 + | Some(res) => 661 + switch RegExp.Result.matches(res) { 662 + | [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re))) 663 + | _ => Error("impossible happened") 664 + } 665 + } 666 + } 667 + let parse = (str: string, ~scope: array<string>, ~gen=?) => { 668 + try { 669 + let (simple, rest) = parseSimple(str) 670 + Ok((parseAll(simple, ~env=envFromScope(scope), ~gen?), rest)) 671 + } catch { 672 + | ParseError(msg) => Error(msg) 673 + } 674 + }

+22

src/HOTerm.resi

··· 1 + type rec t = 2 + | Symbol({name: string}) 3 + | Var({idx: int}) 4 + | Schematic({schematic: int}) 5 + | Lam({name: string, body: t}) 6 + | App({func: t, arg: t}) 7 + // Unallowed is used internally in unify, where Nipkow 1993 uses Var(-infinity) 8 + | Unallowed 9 + 10 + include Signatures.TERM 11 + with type t := t 12 + and type meta = string 13 + and type schematic = int 14 + and type subst = Belt.Map.Int.t<t> 15 + 16 + let emptySubst: subst 17 + let strip: t => (t, array<t>) 18 + // exposed for testing purposes 19 + exception UnifyFail(string) 20 + let substAdd: (subst, schematic, t) => subst 21 + let unifyTerm: (t, t, subst, ~gen: option<gen>) => subst 22 + let reduceSubst: subst => subst

+6

src/HOTermJView.res

··· 1 + module TermView = HOTermView 2 + type props = { 3 + judgment: HOTerm.t, 4 + scope: array<string>, 5 + } 6 + let make = ({judgment, scope}) => HOTermView.make({term: judgment, scope})

+1

src/HOTermJView.resi

··· 1 + include Signatures.JUDGMENT_VIEW with module Term := HOTerm and module Judgment := HOTerm

+68

src/HOTermView.res

··· 1 + type props = {term: HOTerm.t, scope: array<string>} 2 + open Util 3 + type idx_props = {idx: int, scope: array<string>} 4 + let viewVar = (props: idx_props) => 5 + switch props.scope[props.idx] { 6 + | Some(n) if Array.indexOf(props.scope, n) == props.idx => 7 + {React.string(n)} 8 + | _ => 9 + 10 + {React.string("\\")} 11 + {React.int(props.idx)} 12 + 13 + } 14 + 15 + let makeMeta = (str: string) => 16 + 17 + {React.string(str)} 18 + {React.string(".")} 19 + 20 + 21 + let parenthesise = f => 22 + [ 23 + {React.string("(")} , 24 + ...f, 25 + {React.string(")")} , 26 + ] 27 + 28 + let intersperse = a => 29 + a->Array.flatMapWithIndex((e, i) => 30 + if i == 0 { 31 + [e] 32 + } else { 33 + [React.string(" "), e] 34 + } 35 + ) 36 + 37 + @react.componentWithProps 38 + let rec make = ({term, scope}) => 39 + switch term { 40 + | Var({idx}) => viewVar({idx, scope}) 41 + | Symbol({name: s}) => {React.string(s)} 42 + | Schematic({schematic: s}) => 43 + 44 + {React.string("?")} 45 + {React.int(s)} 46 + 47 + | App(_) => 48 + switch HOTerm.strip(term) { 49 + | (func, args) => 50 + 51 + {React.createElement(make, {term: func, scope})} 52 + 53 + {args 54 + ->Array.mapWithIndex((t, i) => React.createElement(make, withKey({term: t, scope}, i))) 55 + ->intersperse 56 + ->parenthesise 57 + ->React.array} 58 + 59 + 60 + } 61 + | Lam({name, body}) => { 62 + let newScope = Array.concat([name], scope) 63 + 64 + {React.string(name)} 65 + {React.createElement(make, {term: body, scope: newScope})} 66 + 67 + } 68 + }

+1

src/HOTermView.resi

··· 1 + include Signatures.TERM_VIEW with module Term := HOTerm

+2 -1

src/Method.res

··· 189 189 let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => { 190 190 //todo add toplevel 191 191 switch Rule.parseInner(input, ~scope, ~gen) { 192 - | Ok((rule, rest)) => switch subparser(rest, ~scope, ~gen) { 192 + | Ok((rule, rest)) => 193 + switch subparser(rest, ~scope, ~gen) { 193 194 | Ok((proof, rest')) => 194 195 switch String.trim(rest')->subparser(~scope, ~gen) { 195 196 | Ok((show, rest'')) => Ok({rule, proof, show}, rest'')

+2 -4

src/Proof.res

··· 82 82 cur := cur.contents->String.trim->String.sliceToEnd(~start=2)->String.trim 83 83 let scope' = Array.concat(fixes, scope) 84 84 switch parseKeyword(cur.contents) { 85 - | Some("?") => Ok(( 86 - {fixes, assumptions, method: None}, 87 - cur.contents->String.sliceToEnd(~start=1), 88 - )) 85 + | Some("?") => 86 + Ok(({fixes, assumptions, method: None}, cur.contents->String.sliceToEnd(~start=1))) 89 87 | Some(keyword) => { 90 88 cur := cur.contents->String.sliceToEnd(~start=String.length(keyword)) 91 89 switch Method.parse(cur.contents, ~keyword, ~scope=scope', ~gen, ~subparser=parse) {

+5 -3

src/Rule.res

··· 6 6 module Make = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { 7 7 type rec t = {vars: array<Term.meta>, premises: array<t>, conclusion: Judgment.t} 8 8 let rec substitute = (rule: t, subst: Term.subst) => { 9 - let subst' = subst->Util.mapMapValues(v => v->Term.upshift(Array.length(rule.vars))) 9 + let subst' = subst->Term.mapSubst(v => v->Term.upshift(Array.length(rule.vars))) 10 10 { 11 11 vars: rule.vars, 12 12 premises: rule.premises->Array.map(premise => premise->substitute(subst')), ··· 46 46 let re = RegExp.fromStringWithFlags(ruleNamePattern, ~flags="y") 47 47 switch re->RegExp.exec(String.trim(str)) { 48 48 | None => Error("expected rule name") 49 - | Some(res) => switch res[0] { 49 + | Some(res) => 50 + switch res[0] { 50 51 | Some(Some(n)) if String.trim(n) != "" => 51 52 Ok(n, String.sliceToEnd(String.trim(str), ~start=RegExp.lastIndex(re))) 52 53 | _ => Error("expected rule name") ··· 57 58 let re = RegExp.fromStringWithFlags(vinculumRES, ~flags="y") 58 59 switch re->RegExp.exec(str) { 59 60 | None => Error("expected vinculum") 60 - | Some(res) => switch res[1] { 61 + | Some(res) => 62 + switch res[1] { 61 63 | Some(Some(n)) if String.trim(n) != "" => 62 64 Ok(n, String.sliceToEnd(str, ~start=RegExp.lastIndex(re))) 63 65 | _ => Ok("", String.sliceToEnd(str, ~start=RegExp.lastIndex(re)))

+12 -3

src/SExp.res

··· 11 11 type meta = string 12 12 type schematic = int 13 13 type subst = Map.t<schematic, t> 14 + let mapSubst = (m: subst, f: t => t): subst => { 15 + let nu = Map.make() 16 + m->Map.forEachWithKey((v, k) => { 17 + nu->Map.set(k, f(v)) 18 + }) 19 + nu 20 + } 14 21 let equivalent = (a: t, b: t) => { 15 22 a == b 16 23 } ··· 89 96 let (x, y) = a[0]->Option.getUnsafe 90 97 switch unifyTerm(x, y) { 91 98 | None => None 92 - | Some(s1) => switch a 99 + | Some(s1) => 100 + switch a 93 101 ->Array.sliceToEnd(~start=1) 94 102 ->Array.map(((t1, t2)) => (substitute(t1, s1), substitute(t2, s1))) 95 103 ->unifyArray { ··· 99 107 } 100 108 } 101 109 } 102 - let unify = (a: t, b: t) => { 110 + let unify = (a: t, b: t, ~gen=?) => { 103 111 switch unifyTerm(a, b) { 104 112 | None => [] 105 113 | Some(s) => [s] ··· 303 311 Array.push(bits, it.contents->getVar->Option.getUnsafe) 304 312 } 305 313 switch it.contents { 306 - | Some(RParen) => switch gen { 314 + | Some(RParen) => 315 + switch gen { 307 316 | Some(g) => { 308 317 seen(g, num) 309 318 Some(Schematic({schematic: num, allowed: bits}))

+2 -1

src/SExpView.res

··· 37 37 @react.componentWithProps 38 38 let rec make = ({term, scope}) => 39 39 switch term { 40 - | Compound({subexps: bits}) => 40 + | Compound({subexps: bits}) => 41 + 41 42 {bits 42 43 ->Array.mapWithIndex((t, i) => React.createElement(make, withKey({term: t, scope}, i))) 43 44 ->intersperse

+5 -4

src/Signatures.res

··· 2 2 type t 3 3 type schematic 4 4 type meta 5 - type subst = Map.t<schematic, t> 5 + type subst 6 + let mapSubst: (subst, t => t) => subst 7 + type gen 6 8 let substitute: (t, subst) => t 7 - let unify: (t, t) => array<subst> 9 + let unify: (t, t, ~gen: gen=?) => array<subst> 8 10 // law: unify(a,b) == [{}] iff equivalent(a,b) 9 11 let equivalent: (t, t) => bool 10 12 let substDeBruijn: (t, array<t>, ~from: int=?) => t 11 13 let upshift: (t, int, ~from: int=?) => t 12 - type gen 13 14 let fresh: (gen, ~replacing: meta=?) => schematic 14 15 let seen: (gen, schematic) => unit 15 16 let place: (schematic, ~scope: array<meta>) => t ··· 25 26 type t 26 27 let substitute: (t, Term.subst) => t 27 28 let equivalent: (t, t) => bool 28 - let unify: (t, t) => array<Term.subst> 29 + let unify: (t, t, ~gen: Term.gen=?) => array<Term.subst> 29 30 let substDeBruijn: (t, array<Term.t>, ~from: int=?) => t 30 31 let upshift: (t, int, ~from: int=?) => t 31 32 let parse: (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t, string), string>

+2 -7

src/Util.res

··· 1 1 let newline = "\n" 2 - let mapMapValues = (m: Map.t<'a, 'b>, f: 'b => 'c) => { 3 - let nu = Map.make() 4 - m->Map.forEachWithKey((v, k) => { 5 - nu->Map.set(k, f(v)) 6 - }) 7 - nu 8 - } 9 2 let withKey: ('props, int) => 'props = %raw(`(props, key) => ({...props, key})`) 10 3 11 4 let arrayWithIndex = (arr: array<React.element>) => { 12 5 React.array(arr->Array.mapWithIndex((m, i) => m )) 13 6 } 7 + exception Unreachable(string) 8 + exception Err(string)

+217

tests/HOTermTest.res

··· 1 + open Zora 2 + open HOTerm 3 + 4 + module Util = TestUtil.MakeTerm(HOTerm) 5 + 6 + let testUnify0 = (t: Zora.t, at: string, bt: string, ~subst=?, ~msg=?, ~reduce=false) => { 7 + let gen = HOTerm.makeGen() 8 + let (a, _) = HOTerm.parse(at, ~scope=[], ~gen)->Result.getExn 9 + let (b, _) = HOTerm.parse(bt, ~scope=[], ~gen)->Result.getExn 10 + try { 11 + let res0 = HOTerm.unifyTerm(a, b, HOTerm.emptySubst, ~gen=Some(gen)) 12 + let res = if reduce { 13 + HOTerm.reduceSubst(res0) 14 + } else { 15 + res0 16 + } 17 + switch subst { 18 + | None => t->ok(true, ~msg=msg->Option.getOr("unification succeeded")) 19 + | Some(subst) => 20 + subst->Belt.Map.Int.forEach((k, v) => { 21 + let expected = subst->Belt.Map.Int.getExn(k) 22 + if res->Belt.Map.Int.has(k) == false { 23 + t->fail( 24 + ~msg=msg->Option.getOr("substitution on " ++ TestUtil.stringifyExn(k) ++ " not found"), 25 + ) 26 + } else { 27 + let actual = res->Belt.Map.Int.getExn(k) 28 + t->equal( 29 + actual, 30 + expected, 31 + ~msg=msg->Option.getOr("substitution on " ++ TestUtil.stringifyExn(k)), 32 + ) 33 + } 34 + }) 35 + } 36 + } catch { 37 + | HOTerm.UnifyFail(failed) => 38 + t->fail( 39 + ~msg="unification failed: " ++ 40 + TestUtil.stringifyExn(a) ++ 41 + " and " ++ 42 + TestUtil.stringifyExn(b) ++ 43 + " with error: " ++ 44 + failed, 45 + ) 46 + } 47 + } 48 + let testUnify = (t: Zora.t, at: string, bt: string, ~subst=?, ~msg=?, ~reduce=true) => { 49 + testUnify0(t, at, bt, ~subst?, ~msg?, ~reduce) 50 + testUnify0(t, bt, at, ~subst?, ~msg?, ~reduce) 51 + } 52 + zoraBlock("parse symbol", t => { 53 + t->block("single char", t => t->Util.testParse("x", Symbol({name: "x"}))) 54 + t->block("multi char", t => t->Util.testParse("xyz", Symbol({name: "xyz"}))) 55 + }) 56 + 57 + zoraBlock("parse var", t => { 58 + t->block("single digit", t => t->Util.testParse("\\1", Var({idx: 1}))) 59 + t->block("multi digit", t => t->Util.testParse("\\234", Var({idx: 234}))) 60 + }) 61 + 62 + zoraBlock("parse schematic", t => { 63 + t->block("empty allowed", t => t->Util.testParse("?1", Schematic({schematic: 1}))) 64 + }) 65 + 66 + zoraBlock("parse application", t => { 67 + t->block("multiple", t => { 68 + t->Util.testParse("(a b)", App({func: Symbol({name: "a"}), arg: Symbol({name: "b"})})) 69 + }) 70 + t->block("multiple more", t => { 71 + t->Util.testParse( 72 + "(a b c)", 73 + App({ 74 + func: App({func: Symbol({name: "a"}), arg: Symbol({name: "b"})}), 75 + arg: Symbol({name: "c"}), 76 + }), 77 + ) 78 + }) 79 + t->block("multiple var", t => { 80 + t->Util.testParse( 81 + "(a \\1 ?1)", 82 + App({ 83 + func: App({func: Symbol({name: "a"}), arg: Var({idx: 1})}), 84 + arg: Schematic({schematic: 1}), 85 + }), 86 + ) 87 + }) 88 + }) 89 + 90 + zoraBlock("parse lambda", t => { 91 + t->block("simple", t => { 92 + t->Util.testParse("(x. x)", Lam({name: "x", body: Var({idx: 0})})) 93 + }) 94 + t->block("with application", t => { 95 + t->Util.testParse( 96 + "(x. x x)", 97 + Lam({name: "x", body: App({func: Var({idx: 0}), arg: Var({idx: 0})})}), 98 + ) 99 + }) 100 + t->block("with application 2args", t => { 101 + t->Util.testParse( 102 + "(x. y. x y)", 103 + Lam({ 104 + name: "x", 105 + body: Lam({name: "y", body: App({func: Var({idx: 1}), arg: Var({idx: 0})})}), 106 + }), 107 + ) 108 + t->Util.testParse("(x. y. x)", Lam({name: "x", body: Lam({name: "y", body: Var({idx: 1})})})) 109 + }) 110 + t->block("omit outer ()", t => { 111 + t->Util.testParse( 112 + "x. (x x)", 113 + Lam({name: "x", body: App({func: Var({idx: 0}), arg: Var({idx: 0})})}), 114 + ) 115 + }) 116 + // TODO: test if remaining strings are returned correctly 117 + }) 118 + 119 + zoraBlock("parse and prettyprint", t => { 120 + t->block("examples", t => { 121 + t->Util.testParsePrettyPrint("\\1", "\\1") 122 + t->Util.testParsePrettyPrint("?1", "?1") 123 + t->Util.testParsePrettyPrint("(x. x)", "(x. x)") 124 + t->Util.testParsePrettyPrint("(x. x. \\0)", "(x. x. x)") 125 + t->Util.testParsePrettyPrint("(x. x. \\1)", "(x. x. \\1)") 126 + t->Util.testParsePrettyPrint("(x. y. z. z)", "(x. y. z. z)") 127 + t->Util.testParsePrettyPrint("(x. y. z. y)", "(x. y. z. y)") 128 + t->Util.testParsePrettyPrint("(x. y. z. x)", "(x. y. z. x)") 129 + t->Util.testParsePrettyPrint("(x. y. z. z y x)", "(x. y. z. z y x)") 130 + }) 131 + }) 132 + 133 + zoraBlock("unify test", t => { 134 + t->block("symbols", t => { 135 + let x = "x" 136 + let y = "y" 137 + t->testUnify(x, x) 138 + t->Util.testNotUnify(y, x) 139 + t->Util.testNotUnify(x, y) 140 + }) 141 + t->block("applications", t => { 142 + let ab = "(a b)" 143 + let cd = "(c d)" 144 + t->testUnify(ab, ab) 145 + t->testUnify(cd, cd) 146 + t->Util.testNotUnify(ab, cd) 147 + t->Util.testNotUnify(cd, ab) 148 + }) 149 + t->block("flex-rigid", t => { 150 + let x = "?0" 151 + let y = "y" 152 + t->testUnify(x, y, ~subst=emptySubst->substAdd(0, Symbol({name: "y"}))) 153 + }) 154 + t->block("flex-rigid2", t => { 155 + let x = "(x. ?0 x)" 156 + let y = "(x. y x)" 157 + // it is y only after eta reduction 158 + t->testUnify( 159 + x, 160 + y, 161 + ~reduce=false, 162 + ~subst=emptySubst->substAdd( 163 + 0, 164 + Lam({name: "x", body: App({func: Symbol({name: "y"}), arg: Var({idx: 0})})}), 165 + ), 166 + ) 167 + t->testUnify(x, y, ~reduce=true, ~subst=emptySubst->substAdd(0, Symbol({name: "y"}))) 168 + }) 169 + t->block("?0 \\0", t => { 170 + let x = "(?0 \\0)" 171 + let y = "\\0" 172 + t->testUnify(x, y, ~subst=emptySubst->substAdd(0, Lam({name: "x", body: Var({idx: 0})}))) 173 + }) 174 + t->block("?0 x y", t => { 175 + let x = "(x. y. ?0 x y)" 176 + let y = "(x. y. y x)" 177 + // ?0 = (x. y. \0 \1) 178 + t->testUnify( 179 + x, 180 + y, 181 + ~reduce=false, 182 + ~subst=emptySubst->substAdd( 183 + 0, 184 + Lam({ 185 + name: "x", 186 + body: Lam({name: "x", body: App({func: Var({idx: 0}), arg: Var({idx: 1})})}), 187 + }), 188 + ), 189 + ) 190 + }) 191 + t->block("occurs-check (flex-rigid)", t => { 192 + let a = "(x. ?0 x)" 193 + let b = "(x. f (?0 x))" 194 + // ?0 occurs in the rigid term on the right → should not unify 195 + t->Util.testNotUnify(a, b) 196 + }) 197 + t->block("no capture", t => { 198 + let a = "(x. ?0)" 199 + let b = "(x. x)" 200 + // Should fail: it cannot capture the bound variable. 201 + t->Util.testNotUnify(a, b) 202 + }) 203 + t->block("eta", t => { 204 + t->testUnify( 205 + "(x. ?0 x)", 206 + "a", 207 + ~reduce=true, 208 + ~subst=emptySubst->substAdd(0, Symbol({name: "a"})), 209 + ) 210 + }) 211 + t->block("divergent", t => { 212 + let divergent = "((x. x x) (x. x x))" 213 + let a = "((x. ?0 x) (x. x x))" 214 + // TODO: should it not unify or not? 215 + t->Util.testNotUnify(a, divergent) 216 + }) 217 + })

+43

tests/TestUtil.res

··· 22 22 | Error(msg) => t->fail(~msg="parse failed: " ++ msg) 23 23 } 24 24 } 25 + let testUnify = (t: Zora.t, at: string, bt: string, ~subst=?, ~msg=?) => { 26 + let gen = Term.makeGen() 27 + let (a, _) = Term.parse(at, ~scope=[], ~gen)->Result.getExn 28 + let (b, _) = Term.parse(bt, ~scope=[], ~gen)->Result.getExn 29 + let res = Term.unify(a, b, ~gen) 30 + if res->Array.length == 0 { 31 + t->fail(~msg="unification failed: " ++ stringifyExn(a) ++ " and " ++ stringifyExn(b)) 32 + } else { 33 + switch subst { 34 + | None => t->ok(true, ~msg=msg->Option.getOr("unification succeeded")) 35 + | Some(subst) => { 36 + t->equal(res->Array.length, 1) 37 + t->equal( 38 + res[0]->Option.getExn, 39 + subst, 40 + ~msg=msg->Option.getOr("unification succeeded with substitution"), 41 + ) 42 + } 43 + } 44 + } 45 + } 46 + let testNotUnify = (t: Zora.t, at: string, bt: string, ~msg=?) => { 47 + let gen = Term.makeGen() 48 + let (a, _) = Term.parse(at, ~scope=[], ~gen)->Result.getExn 49 + let (b, _) = Term.parse(bt, ~scope=[], ~gen)->Result.getExn 50 + let res = Term.unify(a, b) 51 + if res->Array.length != 0 { 52 + t->fail(~msg="unification succeeded: " ++ stringifyExn(a) ++ " and " ++ stringifyExn(b)) 53 + } else { 54 + t->ok(true, ~msg=msg->Option.getOr("unification failed")) 55 + } 56 + } 57 + let testParsePrettyPrint = (t: Zora.t, input, expected, ~scope=[]) => { 58 + let res = Term.parse(input, ~scope=[], ~gen=Term.makeGen()) 59 + 60 + switch res { 61 + | Ok(res) => { 62 + let result = Term.prettyPrint(res->fst, ~scope) 63 + t->equal(result, expected, ~msg="prettyPrint output matches expected") 64 + } 65 + | Error(msg) => t->fail(~msg="parse failed: " ++ msg) 66 + } 67 + } 25 68 }

Configure Feed

Configure Feed