bit mask OPE stuff

rename SubView to Sub (Sub to Sub') and port over props
remove stdlib duplication
2022-11-15 15:44:49 +01:00 · 2022-11-06 18:35:42 +01:00 · 2022-11-06 13:03:54 +01:00 · 2022-11-06 12:43:52 +01:00 · 2022-11-06 12:43:52 +01:00 · 2022-11-06 12:43:52 +01:00
16 changed files with 1271 additions and 320 deletions
--- a/flake.lock
+++ b/flake.lock
@ -3,11 +3,11 @@
    "Prettier": {
      "flake": false,
      "locked": {
-        "lastModified": 1639310097,
-        "narHash": "sha256-+eSLEJDuy2ZRkh1h0Y5IF6RUeHEcWhAHpWhwdwW65f0=",
+        "lastModified": 1641402353,
+        "narHash": "sha256-gUE4aoLfXC4FTZWqCj5fAk6PTy/2Z/NihSuspRrDaOk=",
        "owner": "Z-snails",
        "repo": "prettier",
-        "rev": "4a90663b1d586f6d6fce25873aa0f0d7bc633b89",
+        "rev": "0222ada0be5f6abf5528c8513181f2f4ad117b4b",
        "type": "github"
      },
      "original": {
@ -16,14 +16,30 @@
        "type": "github"
      }
    },
+    "algae": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1663891753,
+        "narHash": "sha256-J8tJDJ5xeIMBnTH1Otk/K/ZJJroG8GYUpUMRi0FWuJ8=",
+        "owner": "avidela",
+        "repo": "algebraic-data",
+        "rev": "9b998adc729c4521a3744aa7ba6b1d698d89f588",
+        "type": "gitlab"
+      },
+      "original": {
+        "owner": "avidela",
+        "repo": "algebraic-data",
+        "type": "gitlab"
+      }
+    },
    "collie": {
      "flake": false,
      "locked": {
-        "lastModified": 1631011321,
-        "narHash": "sha256-goYctB+WBoLgsbjA0DlqGjD8i9wr1K0lv0agqpuwflU=",
+        "lastModified": 1642687104,
+        "narHash": "sha256-0GziqzEUDs1tFd5yiu5NECV0nP1aMPe2QxS9oqhmW6I=",
        "owner": "ohad",
        "repo": "collie",
-        "rev": "ed2eda5e04fbd02a7728e915d396e14cc7ec298e",
+        "rev": "46bff04a8d9a1598fec9b19f515541df16dc64ef",
        "type": "github"
      },
      "original": {
@ -35,11 +51,11 @@
    "comonad": {
      "flake": false,
      "locked": {
-        "lastModified": 1638093386,
-        "narHash": "sha256-kxmN6XuszFLK2i76C6LSGHe5XxAURFu9NpzJbi3nodk=",
+        "lastModified": 1654185277,
+        "narHash": "sha256-+/sVUjGBU81VKDbZM/Ot4Xi/AqPSFbHQvj29jkYV5aM=",
        "owner": "stefan-hoeck",
        "repo": "idris2-comonad",
-        "rev": "06d6b551db20f1f940eb24c1dae051c957de97ad",
+        "rev": "35a6e7c2243e73e9c63340e532adaf3197cea3d3",
        "type": "github"
      },
      "original": {
@ -51,11 +67,11 @@
    "dom": {
      "flake": false,
      "locked": {
-        "lastModified": 1639041519,
-        "narHash": "sha256-4ZYc0qaUEVARxhWuH3JgejIeT+GEDNxdS6zIGhBCk34=",
+        "lastModified": 1655723854,
+        "narHash": "sha256-eeKcB+rd0cgp0XRrKKI+Io5nW0Ld45DQu6EOnmCzsR4=",
        "owner": "stefan-hoeck",
        "repo": "idris2-dom",
-        "rev": "01ab52d0ffdb3b47481413a949b8f0c0688c97e4",
+        "rev": "7916d7a744fa3ec39c4d547de659e0740c98407c",
        "type": "github"
      },
      "original": {
@ -67,11 +83,11 @@
    "dot-parse": {
      "flake": false,
      "locked": {
-        "lastModified": 1638264571,
-        "narHash": "sha256-VJQITz+vuQgl5HwR5QdUGwN8SRtGcb2/lJaAVfFbiSk=",
+        "lastModified": 1653991491,
+        "narHash": "sha256-zZjgdCHYK8AoDupWjio21uYI1XeupVyhL+V/kzgi/qw=",
        "owner": "CodingCellist",
        "repo": "idris2-dot-parse",
-        "rev": "48fbda8bf8adbaf9e8ebd6ea740228e4394154d9",
+        "rev": "121a46b72f886b52314c858eddda05fbe56a78ac",
        "type": "github"
      },
      "original": {
@ -83,11 +99,11 @@
    "effect": {
      "flake": false,
      "locked": {
-        "lastModified": 1637477153,
-        "narHash": "sha256-Ta2Vogg/IiSBkfhhD57jjPTEf3S4DOiVRmof38hmwlM=",
+        "lastModified": 1652479904,
+        "narHash": "sha256-52rVYBfly6bRY6l48INum+l5kLIHBvoDpCc1veyofaw=",
        "owner": "russoul",
        "repo": "idris2-effect",
-        "rev": "ea1daf53b2d7e52f9917409f5653adc557f0ee1a",
+        "rev": "b76dce14b79a5f743243a294c3474c6f113f8e3a",
        "type": "github"
      },
      "original": {
@ -99,11 +115,11 @@
    "elab-util": {
      "flake": false,
      "locked": {
-        "lastModified": 1639041013,
-        "narHash": "sha256-K61s/xifFiTDXJTak5NZmZL6757CTYCY+TGywRZMD7M=",
+        "lastModified": 1663162336,
+        "narHash": "sha256-D7p5CRJ02t/6h4ybnwzPZ8JKzuver+zUrw9tjmFelRI=",
        "owner": "stefan-hoeck",
        "repo": "idris2-elab-util",
-        "rev": "7a381c7c5dc3adb7b97c8b8be17e4fb4cc63027d",
+        "rev": "e2b9dc3ac5f75286089e48f34223022f2a12d332",
        "type": "github"
      },
      "original": {
@ -114,11 +130,11 @@
    },
    "flake-utils": {
      "locked": {
-        "lastModified": 1659877975,
-        "narHash": "sha256-zllb8aq3YO3h8B/U0/J1WBgAL8EX5yWf5pMj3G0NAmc=",
+        "lastModified": 1667077288,
+        "narHash": "sha256-bdC8sFNDpT0HK74u9fUkpbf1MEzVYJ+ka7NXCdgBoaA=",
        "owner": "numtide",
        "repo": "flake-utils",
-        "rev": "c0e246b9b83f637f4681389ecabcb2681b4f3af0",
+        "rev": "6ee9ebb6b1ee695d2cacc4faa053a7b9baa76817",
        "type": "github"
      },
      "original": {
@ -130,11 +146,11 @@
    "frex": {
      "flake": false,
      "locked": {
-        "lastModified": 1637410704,
-        "narHash": "sha256-BthU1t++n0ZvS76p0fCHsE33QSoXYxf0hMUSKajDY8w=",
+        "lastModified": 1651873603,
+        "narHash": "sha256-5+SL2WrwfA3P2pIAih7W3+nAPcawbkl0VSFG1JUjRWY=",
        "owner": "frex-project",
        "repo": "idris-frex",
-        "rev": "22c480e879c757a5cebca7bb555ec3d21ae3ac28",
+        "rev": "3c39392d088acda901c83af4d75cb3933b2427f9",
        "type": "github"
      },
      "original": {
@ -146,11 +162,11 @@
    "fvect": {
      "flake": false,
      "locked": {
-        "lastModified": 1633247988,
-        "narHash": "sha256-zElIze03XpcrYL4H5Aj0ZGNplJGbtOx+iWnivJMzHm0=",
+        "lastModified": 1651523510,
+        "narHash": "sha256-h09sQOa2Vn3VQPVRlGi+ze+qShz8M0zoZdGlPbKBHyM=",
        "owner": "mattpolzin",
        "repo": "idris-fvect",
-        "rev": "1c5e3761e0cd83e711a3535ef9051bea45e6db3f",
+        "rev": "d84969fce38ff8a10b9d261458f4d495e6e0f1ca",
        "type": "github"
      },
      "original": {
@ -162,11 +178,11 @@
    "hashable": {
      "flake": false,
      "locked": {
-        "lastModified": 1633965157,
-        "narHash": "sha256-Dggf5K//RCZ7uvtCyeiLNJS6mm+8/n0RFW3zAc7XqPg=",
+        "lastModified": 1663865679,
+        "narHash": "sha256-dHRifrvrjSSVypJiKXrJNdl1pzxrfWKrG0EWKCPxDzo=",
        "owner": "z-snails",
        "repo": "idris2-hashable",
-        "rev": "d6fec8c878057909b67f3d4da334155de4f37907",
+        "rev": "5615bd4627fedcb6122e902ea3d4d18575459ceb",
        "type": "github"
      },
      "original": {
@ -178,11 +194,11 @@
    "hedgehog": {
      "flake": false,
      "locked": {
-        "lastModified": 1639041435,
-        "narHash": "sha256-893cPy7gGSQpVmm9co3QCpWsgjukafZHy8YFk9xts30=",
+        "lastModified": 1655715979,
+        "narHash": "sha256-p0LwUmcxF2whqmku4q0YUYUoDZtutvYni1FbU4HzoWw=",
        "owner": "stefan-hoeck",
        "repo": "idris2-hedgehog",
-        "rev": "a66b1eb0bf84c4a7b743cfb217be69866bc49ad8",
+        "rev": "289c02636ea7a4510320077c81ec72743803a821",
        "type": "github"
      },
      "original": {
@ -194,44 +210,27 @@
    "idrall": {
      "flake": false,
      "locked": {
-        "lastModified": 1636495701,
-        "narHash": "sha256-aOdCRd4XsSxwqVGta1adlZBy8TVTxTwFDnJ1dyMZK8M=",
+        "lastModified": 1661451973,
+        "narHash": "sha256-q3F55PCJpQu6s3vYzz6M9eP/Yp4mBS0wZRhdER+8Wkc=",
        "owner": "alexhumphreys",
        "repo": "idrall",
-        "rev": "13ef174290169d05c9e9abcd77c53412e3e0c944",
+        "rev": "86e43e48e5edfe2bafbccd1544777a6bea5eec59",
        "type": "github"
      },
      "original": {
        "owner": "alexhumphreys",
-        "ref": "13ef174",
        "repo": "idrall",
        "type": "github"
      }
    },
-    "idris-server": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1634507315,
-        "narHash": "sha256-ulo23yLJXsvImoMB/1C6yRRTqmn/Odo+aUaVi+tUhJo=",
-        "owner": "avidela",
-        "repo": "idris-server",
-        "rev": "661a4ecf0fadaa2bd79c8e922c2d4f79b0b7a445",
-        "type": "gitlab"
-      },
-      "original": {
-        "owner": "avidela",
-        "repo": "idris-server",
-        "type": "gitlab"
-      }
-    },
    "idris2": {
      "flake": false,
      "locked": {
-        "lastModified": 1639427352,
-        "narHash": "sha256-C1K2FM1Kio8vi9FTrivdacYCX4cywIsLBeNCsZ6ft4g=",
+        "lastModified": 1667035002,
+        "narHash": "sha256-0jnBxLMj9b9rac19jIgo9RXkGl2Z0zUalfredKIX1NU=",
        "owner": "idris-lang",
        "repo": "idris2",
-        "rev": "36918e618646177b1e0c2fd01f21cc8d04d9da30",
+        "rev": "c2bcc14e00794b19a7fc7ecc600f5a79b849f031",
        "type": "github"
      },
      "original": {
@ -243,6 +242,7 @@
    "idris2-pkgs": {
      "inputs": {
        "Prettier": "Prettier",
+        "algae": "algae",
        "collie": "collie",
        "comonad": "comonad",
        "dom": "dom",
@ -257,7 +257,6 @@
        "hashable": "hashable",
        "hedgehog": "hedgehog",
        "idrall": "idrall",
-        "idris-server": "idris-server",
        "idris2": "idris2",
        "indexed": "indexed",
        "inigo": "inigo",
@ -271,6 +270,7 @@
        "odf": "odf",
        "pretty-show": "pretty-show",
        "python": "python",
+        "recombine": "recombine",
        "rhone": "rhone",
        "rhone-js": "rhone-js",
        "snocvect": "snocvect",
@ -279,15 +279,16 @@
        "xml": "xml"
      },
      "locked": {
-        "lastModified": 1642030375,
-        "narHash": "sha256-J1uXnpPR72mjFjLBuYcvDHStBxVya6/MjBNNwqxGeD0=",
-        "owner": "claymager",
+        "lastModified": 1667146379,
+        "narHash": "sha256-qGDHORfRc8aamv2fdTqTlR1e6vLxctAfy3hXiUzqTcE=",
+        "owner": "lizard-business",
        "repo": "idris2-pkgs",
-        "rev": "ac33a49d4d4bd2b50fddb040cd889733a02c8f09",
+        "rev": "7f318b3f771e92bc306637dc54e9b0848b6ab244",
        "type": "github"
      },
      "original": {
-        "owner": "claymager",
+        "owner": "lizard-business",
+        "ref": "idris0.6.0",
        "repo": "idris2-pkgs",
        "type": "github"
      }
@ -295,11 +296,11 @@
    "indexed": {
      "flake": false,
      "locked": {
-        "lastModified": 1638685238,
-        "narHash": "sha256-FceB7o88yKYzjTfRC6yfhOL6oDPMmCQAsJZu/pjE2uA=",
+        "lastModified": 1659316146,
+        "narHash": "sha256-xySH74mX3i0Xi7EjXpfr/IUWl8kyB5svV34FVuK3uEk=",
        "owner": "mattpolzin",
        "repo": "idris-indexed",
-        "rev": "ff3ba99b0063da6a74c96178e7f3c58a4ac1693e",
+        "rev": "eb1a019dddcf90412fa8ada1e14574b37a3539c3",
        "type": "github"
      },
      "original": {
@ -311,15 +312,16 @@
    "inigo": {
      "flake": false,
      "locked": {
-        "lastModified": 1637596767,
-        "narHash": "sha256-LNx30LO0YWDVSPTxRLWGTFL4f3d5ANG6c60WPdmiYdY=",
-        "owner": "idris-community",
+        "lastModified": 1667143799,
+        "narHash": "sha256-50AGHZ5B2tNaOGjNPt+32khudJxTxkGQ0/Vq4MCwsqE=",
+        "owner": "lizard-business",
        "repo": "Inigo",
-        "rev": "57f5b5c051222d8c630010a0a3cf7d7138910127",
+        "rev": "8bae2a0c02cd88e6e27b98ea10953c86a383033f",
        "type": "github"
      },
      "original": {
-        "owner": "idris-community",
+        "owner": "lizard-business",
+        "ref": "idrall-update",
        "repo": "Inigo",
        "type": "github"
      }
@ -343,11 +345,11 @@
    "json": {
      "flake": false,
      "locked": {
-        "lastModified": 1639041459,
-        "narHash": "sha256-TP/V1jBBP1hFPm/cJ5O2EJiaNoZ19KvBOAI0S9lvAR4=",
+        "lastModified": 1662978011,
+        "narHash": "sha256-G2jKYYZHp1bfM0XrS/f9Er/MGMtMq2VSQetC18VlTLI=",
        "owner": "stefan-hoeck",
        "repo": "idris2-json",
-        "rev": "7c0c028acad0ba0b63b37b92199f37e6ec73864a",
+        "rev": "23b925a6b68ba8bd2d0298fc4b94e5cb78242e80",
        "type": "github"
      },
      "original": {
@ -359,11 +361,11 @@
    "katla": {
      "flake": false,
      "locked": {
-        "lastModified": 1636542431,
-        "narHash": "sha256-X83NA/P3k1iPcBa8g5z8JldEmFEz/jxVeViJX0/FikY=",
+        "lastModified": 1661665759,
+        "narHash": "sha256-A+hLAdt6H5igJwooGSoIXm8Jq+iEQTdoNrQnajtdZ9A=",
        "owner": "idris-community",
        "repo": "katla",
-        "rev": "d841ec243f96b4762074211ee81033e28884c858",
+        "rev": "a7f9f6c5c605dda745c6a9d847e5cf728b011e6b",
        "type": "github"
      },
      "original": {
@ -375,11 +377,11 @@
    "lsp": {
      "flake": false,
      "locked": {
-        "lastModified": 1639486283,
-        "narHash": "sha256-po396FnUu8iqiipwPxqpFZEU4rtpX3jnt3cySwjLsH8=",
+        "lastModified": 1667002591,
+        "narHash": "sha256-pLh5qBKoi1phvoiaCbpgxs38xaXM1VfD5lQI70I5F38=",
        "owner": "idris-community",
        "repo": "idris2-lsp",
-        "rev": "7ebb6caf6bb4b57c5107579aba2b871408e6f183",
+        "rev": "a2603b83124818eedca072269e8883cf8b7a3223",
        "type": "github"
      },
      "original": {
@ -390,27 +392,26 @@
    },
    "nixpkgs": {
      "locked": {
-        "lastModified": 1638239011,
-        "narHash": "sha256-AjhmbT4UBlJWqxY0ea8a6GU2C2HdKUREkG43oRr3TZg=",
+        "lastModified": 1667055375,
+        "narHash": "sha256-xfSTHYxuKRiqF4dcuAFdti1OUvrC2lHpQqCHWUK5/JA=",
        "owner": "NixOS",
        "repo": "nixpkgs",
-        "rev": "a7ecde854aee5c4c7cd6177f54a99d2c1ff28a31",
+        "rev": "7f9be6a505a31f88499c5d20d11f98accf5ae6ba",
        "type": "github"
      },
      "original": {
        "id": "nixpkgs",
-        "ref": "21.11",
        "type": "indirect"
      }
    },
    "odf": {
      "flake": false,
      "locked": {
-        "lastModified": 1638184051,
-        "narHash": "sha256-usSdPx+UqOGImHHdHcrytdzi2LXtIRZuUW0fkD/Wwnk=",
+        "lastModified": 1643726384,
+        "narHash": "sha256-uIqsQXA/Aoat2snaQJaFqjhCs9gYH28UMS5Emc7Ipk0=",
        "owner": "madman-bob",
        "repo": "idris2-odf",
-        "rev": "d2f532437321c8336f1ca786b44b6ebef4117126",
+        "rev": "5eb388c6a19534f9aa1bd24a3b5c42b4ebc1ad44",
        "type": "github"
      },
      "original": {
@ -422,11 +423,11 @@
    "pretty-show": {
      "flake": false,
      "locked": {
-        "lastModified": 1639041411,
-        "narHash": "sha256-BzEe1fpX+lqGEk8b1JZoQT1db5I7s7SZnLCttRVGXdY=",
+        "lastModified": 1660710482,
+        "narHash": "sha256-zctFDeFs4a6n3i/QzD+3263tMzJe9nZJQc69ustdfs0=",
        "owner": "stefan-hoeck",
        "repo": "idris2-pretty-show",
-        "rev": "a4bc6156b9dac43699f87504cbdb8dada5627863",
+        "rev": "f7383c098418e875b6896cd061861a5301bd67c2",
        "type": "github"
      },
      "original": {
@ -438,11 +439,11 @@
    "python": {
      "flake": false,
      "locked": {
-        "lastModified": 1635936936,
-        "narHash": "sha256-c9mcMApN0qgu0AXQVu0V+NXt2poP258wCPkyvtQvv4I=",
+        "lastModified": 1659367107,
+        "narHash": "sha256-KCc/8907hkJXs0GTKF6IIhss9He8qiClL7wZvyF87cM=",
        "owner": "madman-bob",
        "repo": "idris2-python",
-        "rev": "0eab028933c65bebe744e879881416f5136d6943",
+        "rev": "201eb3013600e14484585ba1aeca41936972d957",
        "type": "github"
      },
      "original": {
@ -451,14 +452,30 @@
        "type": "github"
      }
    },
+    "recombine": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1654557256,
+        "narHash": "sha256-EIatN8eunmLIemEnYCzTKO/sVla5N/OPs6nsB+JvHEw=",
+        "owner": "avidela",
+        "repo": "recombine",
+        "rev": "5ef9613d8df64d3886ded6a4052a0c4c8bc89c93",
+        "type": "gitlab"
+      },
+      "original": {
+        "owner": "avidela",
+        "repo": "recombine",
+        "type": "gitlab"
+      }
+    },
    "rhone": {
      "flake": false,
      "locked": {
-        "lastModified": 1639041532,
-        "narHash": "sha256-2g43shlWQIT/1ogesUBUBV9N8YiD3RwaCbbhdKLVp1s=",
+        "lastModified": 1655717433,
+        "narHash": "sha256-ex5Rs6qA8hPD2NAokQtIQWVjsejuWWuruSvs5NmUOeU=",
        "owner": "stefan-hoeck",
        "repo": "idris2-rhone",
-        "rev": "c4d828b0b8efea495d9a5f1e842a9c67cad57724",
+        "rev": "a12fa1c65bbfb072e0a4e76e40cd0097d3c4c2e1",
        "type": "github"
      },
      "original": {
@ -470,11 +487,11 @@
    "rhone-js": {
      "flake": false,
      "locked": {
-        "lastModified": 1639041546,
-        "narHash": "sha256-ddWVsSRbfA6ghmwiRMzDpHBPM+esGdutuqm1qQZgs88=",
+        "lastModified": 1666895711,
+        "narHash": "sha256-DdFrEWZk35VYlNMGAiiERzkDOlkQMAaJTzqjNxJ3EvM=",
        "owner": "stefan-hoeck",
        "repo": "idris2-rhone-js",
-        "rev": "520dd59549f5b14075045314b6805c7492ed636e",
+        "rev": "528b9fd32ea632346764b1e70bebd3f50881330e",
        "type": "github"
      },
      "original": {
@ -494,11 +511,11 @@
    "snocvect": {
      "flake": false,
      "locked": {
-        "lastModified": 1641633224,
-        "narHash": "sha256-6zTU4sDzd/R/dFCTNZaX41H4L3/USGLFghMS0Oc9liY=",
+        "lastModified": 1651518488,
+        "narHash": "sha256-oIFb2yKKxIDHNCdr0ZkHPuV7KeX0m6m9xBwRFPqz7iw=",
        "owner": "mattpolzin",
        "repo": "idris-snocvect",
-        "rev": "ff1e7afba360a62f7e522e9bbb856096a79702c4",
+        "rev": "f6148c3d06c7a9989062a2425f925fc844468215",
        "type": "github"
      },
      "original": {
@ -510,11 +527,11 @@
    "sop": {
      "flake": false,
      "locked": {
-        "lastModified": 1639041379,
-        "narHash": "sha256-PDTf1Wx6EygiWszguvoVPiqIISYFLabI4e0lXHlrjcA=",
+        "lastModified": 1660672216,
+        "narHash": "sha256-HO05C8KLmx9FIQDQ1IpSUZIDxL4oLPJNinbmCXgBZlk=",
        "owner": "stefan-hoeck",
        "repo": "idris2-sop",
-        "rev": "e4354d1883cd73616019457cb9ebf864d99df6a0",
+        "rev": "7b4c1189c8c9df5b34e5b4aec3aecef43dc8aa3c",
        "type": "github"
      },
      "original": {
@ -526,11 +543,11 @@
    "tailrec": {
      "flake": false,
      "locked": {
-        "lastModified": 1637146655,
-        "narHash": "sha256-0yi7MQIrISPvAwkgDC1M5PHDEeVyIaISF0HjKDaT0Rw=",
+        "lastModified": 1654185733,
+        "narHash": "sha256-ONcY1MFWtctuVM8RtIl6ikIOgqfdeV+ECJiNf1FfytM=",
        "owner": "stefan-hoeck",
        "repo": "idris2-tailrec",
-        "rev": "dd0bc6381b3a2e69aa37f9a8c1b165d4b1516ad7",
+        "rev": "ae27e2ed09ef3d880801899cfc26f470f5b71332",
        "type": "github"
      },
      "original": {
--- a/flake.nix
+++ b/flake.nix
@ -1,15 +1,12 @@
 { description = "quox: quantitative extensional type theory";

  inputs = {
-    nixpkgs.url = "nixpkgs/21.11";
-
-    flake-utils = {
-      url = "github:numtide/flake-utils";
-      inputs.nixpkgs.follows = "nixpkgs";
-    };
+    nixpkgs.url = "nixpkgs";
+    flake-utils.url = "github:numtide/flake-utils";

    idris2-pkgs = {
-      url = "github:claymager/idris2-pkgs";
+      url = "github:lizard-business/idris2-pkgs?ref=idris0.6.0"; # [fixme]
+      # url = "github:claymager/idris2-pkgs";
      inputs.nixpkgs.follows = "nixpkgs";
      inputs.flake-utils.follows = "flake-utils";
    };
--- a/lib/Quox/NatExtra.idr
+++ b/lib/Quox/NatExtra.idr
@ -1,7 +1,9 @@
 module Quox.NatExtra

 import public Data.Nat
-import Data.Nat.Division
+import public Data.Nat.Properties
+import public Data.Nat.Division
+import Data.DPair
 import Data.SnocList
 import Data.Vect

@ -55,3 +57,112 @@ parameters {base : Nat} {auto 0 _ : base `GTE` 2} (chars : Vect base Char)
 export
 showHex : Nat -> String
 showHex = showAtBase $ fromList $ unpack "0123456789ABCDEF"
+
+
+n2i = natToInteger
+i2n = fromInteger {ty = Nat}
+
+private partial %inline
+divNatViaInteger : (m, n : Nat) -> Nat
+divNatViaInteger m n = i2n $ n2i m `div` n2i n
+%transform "divNat" divNat = divNatViaInteger
+
+private %inline
+divNatViaIntegerNZ : (m, n : Nat) -> (0 _ : NonZero n) -> Nat
+divNatViaIntegerNZ m n _ = assert_total divNatViaInteger m n
+%transform "divNatNZ" divNatNZ = divNatViaIntegerNZ
+
+private partial %inline
+modNatViaInteger : (m, n : Nat) -> Nat
+modNatViaInteger m n = i2n $ n2i m `mod` n2i n
+%transform "modNat" modNat = modNatViaInteger
+
+private %inline
+modNatViaIntegerNZ : (m, n : Nat) -> (0 _ : NonZero n) -> Nat
+modNatViaIntegerNZ m n _ = assert_total modNatViaInteger m n
+%transform "modNatNZ" modNatNZ = modNatViaIntegerNZ
+
+
+public export
+data ViewLsb : Nat -> Type where
+  Lsb0 : (n : Nat) -> (0 eq : n' =    2 * n)  -> ViewLsb n'
+  Lsb1 : (n : Nat) -> (0 eq : n' = S (2 * n)) -> ViewLsb n'
+%name ViewLsb p, q
+
+public export data IsLsb0 : ViewLsb n -> Type where ItIsLsb0 : IsLsb0 (Lsb0 n eq)
+public export data IsLsb1 : ViewLsb n -> Type where ItIsLsb1 : IsLsb1 (Lsb1 n eq)
+
+export
+0 lsbMutex : n = (2 * a) -> n = S (2 * b) -> Void
+lsbMutex ev od {n = 0} impossible
+lsbMutex ev od {n = 1} {a = S a} {b = 0} =
+  let ev = injective ev in
+  let s  = sym $ plusSuccRightSucc a (a + 0) in
+  absurd $ trans ev s
+lsbMutex ev od {n = S (S n)} {a = S a} {b = S b} =
+  let ev = injective $
+           trans (injective ev) (sym $ plusSuccRightSucc a (a + 0)) in
+  let od = trans (injective $ injective od)
+                 (sym $ plusSuccRightSucc b (b + 0)) in
+  lsbMutex ev od
+
+public export %hint
+doubleIsLsb0 : (p : ViewLsb (2 * n)) -> IsLsb0 p
+doubleIsLsb0 (Lsb0 k eq) = ItIsLsb0
+doubleIsLsb0 (Lsb1 k eq) = void $ absurd $ lsbMutex Refl eq
+
+public export %hint
+sDoubleIsLsb1 : (p : ViewLsb (S (2 * n))) -> IsLsb1 p
+sDoubleIsLsb1 (Lsb1 k eq) = ItIsLsb1
+sDoubleIsLsb1 (Lsb0 k eq) = void $ absurd $ lsbMutex Refl (sym eq)
+
+
+export
+fromLsb0 : (p : ViewLsb n) -> (0 _ : IsLsb0 p) =>
+           Subset Nat (\n' => n = 2 * n')
+fromLsb0 (Lsb0 n' eq) @{ItIsLsb0} = Element n' eq
+
+export
+fromLsb1 : (p : ViewLsb n) -> (0 _ : IsLsb1 p) =>
+           Subset Nat (\n' => n = S (2 * n'))
+fromLsb1 (Lsb1 n' eq) @{ItIsLsb1} = Element n' eq
+
+
+private
+viewLsb' : (m, d : Nat) -> (0 _ : m `LT` 2) -> ViewLsb (m + 2 * d)
+viewLsb' 0 d p = Lsb0 d Refl
+viewLsb' 1 d p = Lsb1 d Refl
+viewLsb' (S (S _)) _ (LTESucc p) = void $ absurd p
+
+export
+viewLsb : (n : Nat) -> ViewLsb n
+viewLsb n =
+  let 0 nz : NonZero 2 = %search in
+  rewrite DivisionTheorem n 2 nz nz in
+  rewrite multCommutative (divNatNZ n 2 nz) 2 in
+  viewLsb' (modNatNZ n 2 nz) (divNatNZ n 2 nz) (boundModNatNZ n 2 nz)
+
+export
+0 doubleInj : {m, n : Nat} -> 2 * m = 2 * n -> m = n
+doubleInj eq =
+  multRightCancel m n 2 %search $
+    trans (multCommutative m 2) $ trans eq (multCommutative 2 n)
+
+export
+0 sDoubleInj : {m, n : Nat} -> S (2 * m) = S (2 * n) -> m = n
+sDoubleInj eq = doubleInj $ injective eq
+
+
+export
+0 lsbOdd : (n : Nat) -> (eq ** viewLsb (S (2 * n)) = Lsb1 n eq)
+lsbOdd n with (viewLsb (S (2 * n)))
+  _ | Lsb0 _  eq = void $ absurd $ lsbMutex Refl (sym eq)
+  _ | Lsb1 n' eq with (sDoubleInj eq)
+    lsbOdd n | (Lsb1 n eq) | Refl = (eq ** Refl)
+
+export
+0 lsbEven : (n : Nat) -> (eq ** viewLsb (2 * n) = Lsb0 n eq)
+lsbEven n with (viewLsb (2 * n))
+  _ | Lsb1 _  eq = void $ absurd $ lsbMutex Refl eq
+  _ | Lsb0 n' eq with (doubleInj eq)
+    lsbEven n | Lsb0 n eq | Refl = (eq ** Refl)
--- a/lib/Quox/OPE.idr
+++ b/lib/Quox/OPE.idr
@ -2,195 +2,9 @@
 ||| a smaller scope and part of a larger one.
 module Quox.OPE

-import Quox.NatExtra
-
-import Data.Nat
-
-%default total
-
-
-public export
-data OPE : Nat -> Nat -> Type where
-  Id   : OPE n n
-  Drop : OPE m n -> OPE m     (S n)
-  Keep : OPE m n -> OPE (S m) (S n)
-%name OPE p, q
-
-public export %inline Injective Drop where injective Refl = Refl
-public export %inline Injective Keep where injective Refl = Refl
-
-public export
-opeZero : {n : Nat} -> OPE 0 n
-opeZero {n = 0}   = Id
-opeZero {n = S n} = Drop opeZero
-
-public export
-(.) : OPE m n -> OPE n p -> OPE m p
-p      . Id     = p
-Id     . q      = q
-p      . Drop q = Drop $ p . q
-Drop p . Keep q = Drop $ p . q
-Keep p . Keep q = Keep $ p . q
-
-public export
-toLTE : {m : Nat} -> OPE m n -> m `LTE` n
-toLTE Id       = reflexive
-toLTE (Drop p) = lteSuccRight $ toLTE p
-toLTE (Keep p) = LTESucc      $ toLTE p
-
-
-public export
-dropInner' : LTE' m n -> OPE m n
-dropInner' LTERefl      = Id
-dropInner' (LTESuccR p) = Drop $ dropInner' $ force p
-
-public export
-dropInner : {n : Nat} -> LTE m n -> OPE m n
-dropInner = dropInner' . fromLte
-
-public export
-dropInnerN : (m : Nat) -> OPE n (m + n)
-dropInnerN 0     = Id
-dropInnerN (S m) = Drop $ dropInnerN m
-
-
-public export
-interface Tighten t where
-  tighten : Alternative f => OPE m n -> t n -> f (t m)
-
-parameters {auto _ : Tighten t} {auto _ : Alternative f}
-  export
-  tightenInner : {n : Nat} -> m `LTE` n -> t n -> f (t m)
-  tightenInner = tighten . dropInner
-
-  export
-  tightenN : (m : Nat) -> t (m + n) -> f (t n)
-  tightenN m = tighten $ dropInnerN m
-
-  export
-  tighten1 : t (S n) -> f (t n)
-  tighten1 = tightenN 1
-
-
-
-- [todo] can this be done with fancy nats too?
-- with bitmasks sure but that might not be worth the effort
-- [the next day] it probably isn't
-
-- public export
-- data OPE' : Nat -> Nat -> Type where
--   None : OPE' 0 0
--   Drop : OPE' m n -> OPE' m (S n)
--   Keep : OPE' m n -> OPE' (S m) (S n)
-- %name OPE' q
-
-
-- public export %inline
-- drop' : Integer -> Integer
-- drop' n = n * 2
-
-- public export %inline
-- keep' : Integer -> Integer
-- keep' n = 1 + 2 * n
-
-- public export
-- data IsOPE : Integer -> (OPE' m n) -> Type where
--   IsNone : 0 `IsOPE` None
--   IsDrop : (0 _ : m `IsOPE` q) -> drop' m `IsOPE` Drop q
--   IsKeep : (0 _ : m `IsOPE` q) -> keep' m `IsOPE` Keep q
-- %name IsOPE p
-
-
-- public export
-- record OPE m n where
--   constructor MkOPE
--   value  : Integer
--   0 spec : OPE' m n
--   0 prf  : value `IsOPE` spec
--   0 pos  : So (value >= 0)
-
-
-- private
-- 0 idrisPleaseLearnAboutIntegers : {x, y : Integer} -> x = y
-- idrisPleaseLearnAboutIntegers {x, y} = believe_me $ Refl {x}
-
-- private
-- 0 natIntPlus : (m, n : Nat) ->
--                natToInteger (m + n) = natToInteger m + natToInteger n
-- natIntPlus m n = idrisPleaseLearnAboutIntegers
-
-- private
-- 0 shiftTwice : (x : Integer) -> (m, n : Nat) ->
--                x `shiftL` (m + n) = (x `shiftL` m) `shiftL` n
-- shiftTwice x m n = idrisPleaseLearnAboutIntegers
-
-- private
-- 0 shift1 : (x : Integer) -> (x `shiftL` 1) = 2 * x
-- shift1 x = idrisPleaseLearnAboutIntegers
-
-- private
-- 0 intPlusComm : (x, y : Integer) -> (x + y) = (y + x)
-- intPlusComm x y = idrisPleaseLearnAboutIntegers
-
-- private
-- 0 intTimes2Minus1 : (x : Integer) -> 2 * x - 1 = 2 * (x - 1) + 1
-- intTimes2Minus1 x = idrisPleaseLearnAboutIntegers
-
-- private
-- 0 intPosShift : So (x > 0) -> So (x `shiftL` i > 0)
-- intPosShift p = believe_me Oh
-
-- private
-- 0 intNonnegDec : {x : Integer} -> So (x > 0) -> So (x - 1 >= 0)
-- intNonnegDec p = believe_me Oh
-
-
-- private
-- 0 shiftSucc : (x : Integer) -> (n : Nat) ->
--               x `shiftL` S n = 2 * (x `shiftL` n)
-- shiftSucc x n = Calc $
--   |~  x `shiftL` S n
--   ~~  x `shiftL` (n + 1)
--         ...(cong (x `shiftL`) $ sym $ plusCommutative {})
--   ~~  (x `shiftL` n) `shiftL` 1
--         ...(shiftTwice {})
--   ~~  2 * (x `shiftL` n)
--         ...(shift1 {})
-
-
-- private
-- opeIdVal : (n : Nat) -> Integer
-- opeIdVal n = (1 `shiftL` n) - 1
-
-- private
-- 0 opeIdValSpec : (n : Nat) -> Integer
-- opeIdValSpec 0     = 0
-- opeIdValSpec (S n) = keep' $ opeIdValSpec n
-
-- private
-- 0 opeIdValOk :  (n : Nat) -> opeIdVal n = opeIdValSpec n
-- opeIdValOk 0     = Refl
-- opeIdValOk (S n) = Calc $
--   |~  (1 `shiftL` S n) - 1
--   ~~  2 * (1 `shiftL` n) - 1      ...(cong (\x => x - 1) $ shiftSucc {})
--   ~~  2 * (1 `shiftL` n - 1) + 1  ...(intTimes2Minus1 {})
--   ~~  1 + 2 * (1 `shiftL` n - 1)  ...(intPlusComm {})
--   ~~  1 + 2 * opeIdValSpec n      ...(cong (\x => 1 + 2 * x) $ opeIdValOk {})
-
-- private
-- 0 opeIdSpec : (n : Nat) -> OPE' n n
-- opeIdSpec 0     = None
-- opeIdSpec (S n) = Keep $ opeIdSpec n
-
-- private
-- 0 opeIdProof' : (n : Nat) -> opeIdValSpec n `IsOPE` opeIdSpec n
-- opeIdProof' 0     = IsNone
-- opeIdProof' (S n) = IsKeep (opeIdProof' n)
-
-- private
-- 0 opeIdProof : (n : Nat) -> opeIdVal n `IsOPE` opeIdSpec n
-- opeIdProof n = rewrite opeIdValOk n in opeIdProof' n
-
-- export
-- opeId : {n : Nat} -> OPE n n
-- opeId {n} = MkOPE {prf = opeIdProof n, pos = intNonnegDec $ intPosShift Oh, _}
+import public Quox.OPE.Basics
+import public Quox.OPE.Length
+import public Quox.OPE.Sub
+import public Quox.OPE.Split
+import public Quox.OPE.Comp
+import public Quox.OPE.Cover
--- a/lib/Quox/OPE/Basics.idr
+++ b/lib/Quox/OPE/Basics.idr
@ -0,0 +1,11 @@
+module Quox.OPE.Basics
+
+%default total
+
+public export
+Scope : Type -> Type
+Scope = SnocList
+
+public export
+Scoped : Type -> Type
+Scoped a = Scope a -> Type
--- a/lib/Quox/OPE/Comp.idr
+++ b/lib/Quox/OPE/Comp.idr
@ -0,0 +1,153 @@
+module Quox.OPE.Comp
+
+import Quox.OPE.Basics
+import Quox.OPE.Length
+import Quox.OPE.Sub
+import Data.DPair
+
+import Control.Function
+import Data.Nat
+
+%default total
+
+
+public export
+data Comp' : ys `Sub'` zs -> xs `Sub'` ys -> xs `Sub'` zs -> Type where
+  CEE : Comp' End End End
+  CKK : Comp' p q pq -> Comp' (Keep p) (Keep q) (Keep pq)
+  CKD : Comp' p q pq -> Comp' (Keep p) (Drop q) (Drop pq)
+  CD0 : Comp' p q pq -> Comp' (Drop p) q        (Drop pq)
+
+public export
+record Comp {a : Type} {xs, ys, zs : Scope a}
+            (p : ys `Sub` zs) (q : xs `Sub` ys) (pq : xs `Sub` zs) where
+  constructor MkComp
+  0 comp : Comp' p.lte q.lte pq.lte
+
+
+export
+compPrf' : (p : ys `Sub'` zs) -> (q : xs `Sub'` ys) -> Comp' p q (p . q)
+compPrf' End      End      = CEE
+compPrf' (Keep p) (Keep q) = CKK $ compPrf' p q
+compPrf' (Keep p) (Drop q) = CKD $ compPrf' p q
+compPrf' (Drop p) q        = CD0 $ compPrf' p q
+
+export
+0 compOk' : Comp' p q r -> r = (p . q)
+compOk' CEE     = Refl
+compOk' (CKK z) = cong Keep $ compOk' z
+compOk' (CKD z) = cong Drop $ compOk' z
+compOk' (CD0 z) = cong Drop $ compOk' z
+
+
+export %inline
+compPrf : (0 sy : Length ys) => (0 sz : Length zs) =>
+       (p : ys `Sub` zs) -> (q : xs `Sub` ys) ->
+       Comp p q ((p . q) @{sy} @{sz})
+compPrf p q = MkComp $
+  replace {p = Comp' p.lte q.lte} (sym $ compLte p q) $
+    compPrf' p.lte q.lte
+
+
+export
+compZero' : (sx : Length xs) => (sy : Length ys) =>
+            (p : xs `Sub'` ys) -> Comp' p (zero' @{sx}) (zero' @{sy})
+compZero' {sx = Z,   sy = Z}   End      = CEE
+compZero' {sx = S _, sy = S _} (Keep p) = CKD (compZero' p)
+compZero'           {sy = S _} (Drop p) = CD0 (compZero' p)
+
+export %inline
+compZero : (sx : Length xs) => (sy : Length ys) =>
+           (p : xs `Sub` ys) -> Comp p (zero @{sx}) (zero @{sy})
+compZero p = MkComp $
+  rewrite zeroLte {sx} in
+  rewrite zeroLte {sx = sy} in
+  compZero' {}
+
+export
+compIdLeft' : (sy : Length ys) =>
+              (p : xs `Sub'` ys) -> Comp' (refl' @{sy}) p p
+compIdLeft' {sy = Z}   End      = CEE
+compIdLeft' {sy = S _} (Keep p) = CKK (compIdLeft' p)
+compIdLeft' {sy = S _} (Drop p) = CKD (compIdLeft' p)
+
+export %inline
+compIdLeft : (sy : Length ys) =>
+             (p : xs `Sub` ys) -> Comp (refl @{sy}) p p
+compIdLeft {sy} p = MkComp $
+  rewrite reflLte {sx = sy} in compIdLeft' {}
+
+export
+compIdRight' : (sx : Length xs) =>
+               (p : xs `Sub'` ys) -> Comp' p (refl' @{sx}) p
+compIdRight' {sx = Z}   End      = CEE
+compIdRight' {sx = S _} (Keep p) = CKK (compIdRight' p)
+compIdRight'            (Drop p) = CD0 (compIdRight' p)
+
+export %inline
+compIdRight : (sx : Length xs) =>
+              (p : xs `Sub` ys) -> Comp p (refl @{sx}) p
+compIdRight {sx} p = MkComp $ rewrite reflLte {sx} in compIdRight' {}
+
+export
+0 compAssoc' : (p : ys `Sub'` zs) -> (q : xs `Sub'` ys) -> (r : ws `Sub'` xs) ->
+               p . (q . r) = (p . q) . r
+compAssoc' End      End      End      = Refl
+compAssoc' (Keep p) (Keep q) (Keep r) = cong Keep $ compAssoc' p q r
+compAssoc' (Keep p) (Keep q) (Drop r) = cong Drop $ compAssoc' p q r
+compAssoc' (Keep p) (Drop q) r        = cong Drop $ compAssoc' p q r
+compAssoc' (Drop p) q        r        = cong Drop $ compAssoc' p q r
+compAssoc' End (Drop _) _ impossible
+
+export %inline
+0 compAssoc : (sx : Length xs) => (sy : Length ys) => (sz : Length zs) =>
+              (p : ys `Sub` zs) -> (q : xs `Sub` ys) -> (r : ws `Sub` xs) ->
+              comp @{sy} @{sz} p (comp @{sx} @{sy} q r) =
+                comp @{sx} @{sz} (comp @{sy} @{sz} p q) r
+compAssoc p q r = lteEq $
+  trans (transLte {}) $
+  trans (cong (p.lte .) (transLte {})) $
+  sym $
+  trans (transLte {}) $
+  trans (cong (. r.lte) (transLte {})) $
+  sym $ compAssoc' {}
+
+public export
+0 Subscope : Scope a -> Type
+Subscope ys = Exists (`Sub` ys)
+
+public export
+record SubMap' {a : Type} {xs, ys, zs : Scope a}
+               (p : xs `Sub'` zs) (q : ys `Sub'` zs) where
+  constructor SM'
+  thin : xs `Sub'` ys
+  0 comp : Comp' q thin p
+
+public export
+record SubMap {a : Type} {xs, ys, zs : Scope a}
+              (p : xs `Sub` zs) (q : ys `Sub` zs) where
+  constructor SM
+  thin : xs `Sub` ys
+  0 comp : Comp q thin p
+
+export
+0 submap' : SubMap p q -> SubMap' p.lte q.lte
+submap' (SM thin comp) = SM' {thin = thin.lte, comp = comp.comp}
+
+parameters (p : xs `Sub'` ys)
+  export
+  subId' : SubMap' p p
+  subId' = SM' refl' (compIdRight' p)
+
+  export
+  subZero' : SubMap' Sub.zero' p
+  subZero' = SM' zero' (compZero' p)
+
+parameters {auto sx : Length xs} (p : xs `Sub` ys)
+  export
+  subId : SubMap p p
+  subId = SM refl (compIdRight p)
+
+  export
+  subZero : SubMap Sub.zero p
+  subZero = SM zero (compZero p)
--- a/lib/Quox/OPE/Cover.idr
+++ b/lib/Quox/OPE/Cover.idr
@ -0,0 +1,90 @@
+module Quox.OPE.Cover
+
+import Quox.OPE.Basics
+import Quox.OPE.Length
+import Quox.OPE.Sub
+
+%default total
+
+
+public export
+data Cover'_ : (overlap : Bool) -> xs `Sub'` zs -> ys `Sub'` zs -> Type where
+  CE : Cover'_ ov End End
+  CL : Cover'_ ov p q -> Cover'_ ov   (Keep p) (Drop q)
+  CR : Cover'_ ov p q -> Cover'_ ov   (Drop p) (Keep q)
+  C2 : Cover'_ ov p q -> Cover'_ True (Keep p) (Keep q)
+
+parameters (p : xs `Sub'` zs) (q : ys `Sub'` zs)
+  public export
+  0 Cover' : Type
+  Cover' = Cover'_ True p q
+
+  public export
+  0 Partition' : Type
+  Partition' = Cover'_ False p q
+
+
+public export
+record Cover_ {a : Type} {xs, ys, zs : Scope a} (overlap : Bool)
+              (p : xs `Sub` zs) (q : ys `Sub` zs) where
+  constructor MkCover
+  0 cover : Cover'_ overlap p.lte q.lte
+
+parameters (p : xs `Sub` zs) (q : ys `Sub` zs)
+  public export
+  0 Cover : Type
+  Cover = Cover_ True p q
+
+  public export
+  0 Partition : Type
+  Partition = Cover_ False p q
+
+
+private %inline
+covCast' : {0 p, p' : xs `Sub'` zs} -> {0 q, q' : ys `Sub'` zs} ->
+           (0 pe : p = p') -> (0 qe : q = q') ->
+           Cover'_ overlap p' q' -> Cover'_ overlap p q
+covCast' pe qe c = replace {p = id} (sym $ cong2 (Cover'_ overlap) pe qe) c
+
+
+parameters {0 overlap : Bool} {0 p : xs `Sub` zs} {0 q : ys `Sub` zs}
+  export %inline
+  left : Cover_ overlap p q -> Cover_ overlap (keep p) (drop q)
+  left (MkCover cover) = MkCover $ covCast' (keepLte p) (dropLte q) $ CL cover
+
+  export %inline
+  right : Cover_ overlap p q -> Cover_ overlap (drop p) (keep q)
+  right (MkCover cover) = MkCover $ covCast' (dropLte p) (keepLte q) $ CR cover
+
+  export %inline
+  both : Cover_ overlap p q -> Cover (keep p) (keep q)
+  both (MkCover cover) = MkCover $ covCast' (keepLte p) (keepLte q) $ C2 cover
+
+
+export
+allLeft' : (sx : Length xs) => Partition' (refl' @{sx}) (zero' @{sx})
+allLeft' {sx = Z}   = CE
+allLeft' {sx = S s} = CL allLeft'
+
+export
+allRight' : (sx : Length xs) => Partition' (zero' @{sx}) (refl' @{sx})
+allRight' {sx = Z}   = CE
+allRight' {sx = S s} = CR allRight'
+
+export
+both' : (sx : Length xs) => Cover' (refl' @{sx}) (refl' @{sx})
+both' {sx = Z}   = CE
+both' {sx = S s} = C2 both'
+
+
+export %inline
+allLeft : (sx : Length xs) => Partition (refl @{sx}) (zero @{sx})
+allLeft = MkCover $ rewrite reflLte {sx} in rewrite zeroLte {sx} in allLeft'
+
+export %inline
+allRight : (sx : Length xs) => Partition (zero @{sx}) (refl @{sx})
+allRight = MkCover $ rewrite reflLte {sx} in rewrite zeroLte {sx} in allRight'
+
+export %inline
+allBoth : (sx : Length xs) => Cover (refl @{sx}) (refl @{sx})
+allBoth = MkCover $ rewrite reflLte {sx} in both'
--- a/lib/Quox/OPE/Length.idr
+++ b/lib/Quox/OPE/Length.idr
@ -0,0 +1,39 @@
+module Quox.OPE.Length
+
+import Quox.OPE.Basics
+
+%default total
+
+
+public export
+data Length : Scope a -> Type where
+  Z : Length [<]
+  S : (s : Length xs) -> Length (xs :< x)
+%name Length s
+%builtin Natural Length
+
+public export
+(.nat) : Length xs -> Nat
+(Z).nat   = Z
+(S s).nat = S s.nat
+%transform "Length.nat" Length.(.nat) xs = believe_me xs
+
+export
+0 ok : (s : Length xs) -> s.nat = length xs
+ok Z     = Refl
+ok (S s) = cong S $ ok s
+
+public export %hint
+toLength : (xs : Scope a) -> Length xs
+toLength [<]       = Z
+toLength (sx :< x) = S (toLength sx)
+
+public export %hint
+lengthApp : Length xs -> Length ys -> Length (xs ++ ys)
+lengthApp sx Z      = sx
+lengthApp sx (S sy) = S (lengthApp sx sy)
+
+public export
+0 lengthIrrel : (sx1, sx2 : Length xs) -> sx1 = sx2
+lengthIrrel Z       Z       = Refl
+lengthIrrel (S sx1) (S sx2) = cong S $ lengthIrrel sx1 sx2
--- a/lib/Quox/OPE/Split.idr
+++ b/lib/Quox/OPE/Split.idr
@ -0,0 +1,37 @@
+module Quox.OPE.Split
+
+import Quox.OPE.Basics
+import Quox.OPE.Length
+import Quox.OPE.Sub
+
+%default total
+
+
+public export
+record Split {a : Type} (xs, ys, zs : Scope a) (p : xs `Sub` ys ++ zs) where
+  constructor MkSplit
+  {0 leftSub, rightSub : Scope a}
+  leftThin : leftSub `Sub` ys
+  rightThin : rightSub `Sub` zs
+  0 eqScope : xs = leftSub ++ rightSub
+  0 eqThin : p ~=~ leftThin ++ rightThin
+
+export
+split : Length ys =>
+        (zs : Scope a) -> (p : xs `Sub` ys ++ zs) -> Split xs ys zs p
+split [<] p = MkSplit p zero Refl (endRight p)
+split (zs :< z) p @{ys} with (p.view @{S (lengthApp ys %search)})
+  split (zs :< z) (SubM (S (2 * n)) (Keep p) v0) | (KEEP v Refl) =
+    case split zs (sub v) of
+      MkSplit l r Refl t =>
+        MkSplit l (keep r) Refl $
+          rewrite viewIrrel v0 (KEEP v Refl) in
+          trans (cong keep {a = sub v} t) $
+          sym $ keepAppRight l r
+  split (zs :< z) (SubM (2 * n) (Drop p) v0) | (DROP v Refl) =
+    case split zs (sub v) of
+      MkSplit l r Refl t =>
+        MkSplit l (drop r) Refl $
+          rewrite viewIrrel v0 (DROP v Refl) in
+          trans (cong drop {a = sub v} t) $
+          sym $ dropAppRight l r
--- a/lib/Quox/OPE/Sub.idr
+++ b/lib/Quox/OPE/Sub.idr
@ -0,0 +1,572 @@
+module Quox.OPE.Sub
+
+import Quox.OPE.Basics
+import Quox.OPE.Length
+import Quox.NatExtra
+import Data.DPair
+import Data.SnocList.Elem
+import Data.SnocList.Quantifiers
+
+%default total
+
+infix 0 `Sub'`, `Sub`
+
+public export
+data Sub' : Scope a -> Scope a -> Type where
+  End  : [<] `Sub'` [<]
+  Keep : xs `Sub'` ys -> xs :< z `Sub'` ys :< z
+  Drop : xs `Sub'` ys -> xs      `Sub'` ys :< z
+%name Sub' p, q
+
+export
+keepInjective : Keep p = Keep q -> p = q
+keepInjective Refl = Refl
+
+export
+dropInjective : Drop p = Drop q -> p = q
+dropInjective Refl = Refl
+
+-- these need to be `public export` so that
+-- `id`, `zero`, and maybe others can reduce
+public export %hint
+lengthLeft : xs `Sub'` ys -> Length xs
+lengthLeft End      = Z
+lengthLeft (Keep p) = S (lengthLeft p)
+lengthLeft (Drop p) = lengthLeft p
+
+public export %hint
+lengthRight : xs `Sub'` ys -> Length ys
+lengthRight End      = Z
+lengthRight (Keep p) = S (lengthRight p)
+lengthRight (Drop p) = S (lengthRight p)
+
+
+export %inline
+dropLast' : (xs :< x) `Sub'` ys -> xs `Sub'` ys
+dropLast' (Keep p) = Drop p
+dropLast' (Drop p) = Drop $ dropLast' p
+
+export
+Uninhabited (xs :< x `Sub'` [<]) where uninhabited _ impossible
+
+export
+Uninhabited (xs :< x `Sub'` xs) where
+  uninhabited (Keep p) = uninhabited p
+  uninhabited (Drop p) = uninhabited $ dropLast' p
+
+
+export
+0 lteLen : xs `Sub'` ys -> length xs `LTE` length ys
+lteLen End      = LTEZero
+lteLen (Keep p) = LTESucc $ lteLen p
+lteLen (Drop p) = lteSuccRight $ lteLen p
+
+export
+0 lteNilRight : xs `Sub'` [<] -> xs = [<]
+lteNilRight End = Refl
+
+
+
+public export
+refl' : Length xs => xs `Sub'` xs
+refl' @{Z}   = End
+refl' @{S s} = Keep refl'
+
+public export
+zero' : Length xs => [<] `Sub'` xs
+zero' @{Z}   = End
+zero' @{S s} = Drop zero'
+
+public export
+single' : Length xs => x `Elem` xs -> [< x] `Sub'` xs
+single' @{S _} Here      = Keep zero'
+single' @{S _} (There p) = Drop $ single' p
+
+
+namespace Sub
+  public export
+  (.) : ys `Sub'` zs -> xs `Sub'` ys -> xs `Sub'` zs
+  End      . End      = End
+  (Keep p) . (Keep q) = Keep $ p . q
+  (Keep p) . (Drop q) = Drop $ p . q
+  (Drop p) . q        = Drop $ p . q
+
+public export
+comp' : ys `Sub'` zs -> xs `Sub'` ys -> xs `Sub'` zs
+comp' = (.)
+
+public export %inline
+trans' : xs `Sub'` ys -> ys `Sub'` zs -> xs `Sub'` zs
+trans' = flip (.)
+
+public export
+app' : xs1 `Sub'` ys1 -> xs2 `Sub'` ys2 -> (xs1 ++ xs2) `Sub'` (ys1 ++ ys2)
+app' p End      = p
+app' p (Keep q) = Keep $ app' p q
+app' p (Drop q) = Drop $ app' p q
+
+
+||| if `p` holds for all elements of the main list,
+||| it holds for all elements of the sublist
+public export
+subAll' : xs `Sub'` ys -> All p ys -> All p xs
+subAll' End      [<]       = [<]
+subAll' (Keep q) (ps :< x) = subAll' q ps :< x
+subAll' (Drop q) (ps :< x) = subAll' q ps
+
+||| if `p` holds for one element of the sublist,
+||| it holds for one element of the main list
+public export
+subAny' : xs `Sub'` ys -> Any p xs -> Any p ys
+subAny' (Keep q) (Here  x) = Here x
+subAny' (Keep q) (There x) = There (subAny' q x)
+subAny' (Drop q) x         = There (subAny' q x)
+
+
+public export
+data SubView : (lte : xs `Sub'` ys) -> (mask : Nat) -> Type where
+  [search lte]
+  END  : (0 eq : n = 0) -> SubView End n
+  KEEP : {n : Nat} -> {0 p : xs `Sub'` ys} ->
+         (0 v : SubView p n) -> (0 eq : n' = S (2 * n)) ->
+         SubView (Keep {z} p) n'
+  DROP : {n : Nat} -> {0 p : xs `Sub'` ys} ->
+         (0 v : SubView p n) -> (0 eq : n' = 2 * n) ->
+         SubView (Drop {z} p) n'
+%name SubView v
+
+public export
+record Sub {a : Type} (xs, ys : Scope a) where
+  constructor SubM
+  mask : Nat
+  0 lte : xs `Sub'` ys
+  0 view0 : SubView lte mask
+%name Sub sub
+
+public export %inline
+sub : {mask : Nat} -> {0 lte : xs `Sub'` ys} -> (0 view0 : SubView lte mask) ->
+      xs `Sub` ys
+sub v = SubM _ _ v
+
+
+private
+0 uip : (p, q : a = b) -> p = q
+uip Refl Refl = Refl
+
+export
+0 viewIrrel : Length ys =>
+              {m : Nat} -> {lte : xs `Sub'` ys} ->
+              (v1, v2 : SubView lte m) -> v1 === v2
+viewIrrel (END eq1) (END eq2) = rewrite uip eq1 eq2 in Refl
+viewIrrel (KEEP v1 eq1) (KEEP v2 eq2) with (sDoubleInj $ trans (sym eq1) eq2)
+  _ | Refl = rewrite viewIrrel v1 v2 in rewrite uip eq1 eq2 in Refl
+viewIrrel (DROP v1 eq1) (DROP v2 eq2) with (doubleInj $ trans (sym eq1) eq2)
+  _ | Refl = rewrite viewIrrel v1 v2 in rewrite uip eq1 eq2 in Refl
+
+export
+0 viewLteEq : {p, q : xs `Sub'` ys} -> SubView p m -> SubView q m -> p = q
+viewLteEq (END _) (END _) = Refl
+viewLteEq (KEEP {n = m} pv pe) (KEEP {n} qv qe) =
+  let eq = sDoubleInj {m, n} $ trans (sym pe) qe in
+  rewrite viewLteEq pv (rewrite eq in qv) in Refl
+viewLteEq (KEEP pv pe) (DROP qv qe) = absurd $ lsbMutex qe pe
+viewLteEq (DROP pv pe) (KEEP qv qe) = absurd $ lsbMutex pe qe
+viewLteEq (DROP {n = m} pv pe) (DROP {n} qv qe) =
+  let eq = doubleInj {m, n} $ trans (sym pe) qe in
+  rewrite viewLteEq pv (rewrite eq in qv) in Refl
+
+private
+0 lteEq' : (p : xs `Sub'` ys) ->
+           (v1 : SubView p m1) -> (v2 : SubView p m2) ->
+           SubM m1 p v1 = SubM m2 p v2
+lteEq' End (END Refl) (END Refl) = Refl
+lteEq' {m1 = S (2 * n)} {m2 = S (2 * n)} (Keep p) (KEEP v1 Refl) (KEEP v2 Refl) =
+  cong (\v => SubM (S (2 * n)) (Keep p) (KEEP v Refl)) $
+    case lteEq' p v1 v2 of Refl => Refl
+lteEq' {m1 = 2 * n} {m2 = 2 * n} (Drop p) (DROP v1 Refl) (DROP v2 Refl) =
+  cong (\v => SubM (2 * n) (Drop p) (DROP v Refl)) $
+    case lteEq' p v1 v2 of Refl => Refl
+lteEq' {m1 = _} {m2 = S _} _ _ (END _) impossible
+lteEq' {m1 = Z} {m2 = _} _ (KEEP _ _) _ impossible
+lteEq' {m1 = _} {m2 = Z} _ _ (KEEP _ _) impossible
+
+export
+0 lteEq : {p, q : xs `Sub` ys} -> p.lte = q.lte -> p = q
+lteEq {p = SubM pm pl pv} {q = SubM qm ql qv} eq =
+  rewrite eq in lteEq' ql (rewrite sym eq in pv) qv
+
+
+public export %inline
+end : [<] `Sub` [<]
+end = SubM 0 End (END Refl)
+
+public export %inline
+keep : xs `Sub` ys -> xs :< z `Sub` ys :< z
+keep (SubM mask lte view0) = SubM (S (2 * mask)) (Keep lte) (KEEP view0 Refl)
+
+public export %inline
+drop : xs `Sub` ys -> xs `Sub` ys :< z
+drop (SubM mask lte view0) = SubM (2 * mask) (Drop lte) (DROP view0 Refl)
+
+
+export
+0 keepLte : (p : xs `Sub` ys) -> (keep p).lte = Keep p.lte
+keepLte (SubM mask lte view0) = Refl
+
+export
+0 dropLte : (p : xs `Sub` ys) -> (drop p).lte = Drop p.lte
+dropLte (SubM mask lte view0) = Refl
+
+
+public export
+data Eqv : {xs, ys : Scope a} -> (p, q : xs `Sub` ys) -> Type where
+  EQV : {0 p, q : xs `Sub` ys} -> p.mask = q.mask -> p `Eqv` q
+%name Eqv eqv
+
+export
+Reflexive (xs `Sub` ys) Eqv where
+  reflexive = EQV Refl
+
+export
+Symmetric (xs `Sub` ys) Eqv where
+  symmetric (EQV eq) = EQV $ sym eq
+
+export
+Transitive (xs `Sub` ys) Eqv where
+  transitive (EQV eq1) (EQV eq2) = EQV $ trans eq1 eq2
+
+export
+0 eqvToEq : {p, q : xs `Sub` ys} -> p `Eqv` q -> p = q
+eqvToEq {p = SubM _ _ pv} {q = SubM _ _ qv} (EQV Refl) with (viewLteEq pv qv)
+  _ | Refl = rewrite viewIrrel pv qv in Refl
+
+export
+0 eqToEqv : {p, q : xs `Sub` ys} -> p = q -> p `Eqv` q
+eqToEqv Refl = reflexive
+
+
+export
+getMask : SubView lte mask -> Subset Nat (Equal mask)
+getMask (END Refl)  = Element 0 Refl
+getMask (KEEP v eq) = Element _ eq
+getMask (DROP v eq) = Element _ eq
+
+
+private
+splitExEq : {0 f, g : a -> b} ->
+            (0 p : (x : a ** f x = g x)) -> Exists (\x => f x = g x)
+splitExEq p = Evidence p.fst (irr p.snd)
+  where irr : forall a, b. (0 eq : a = b) -> a = b
+        irr Refl = Refl
+
+private
+0 lteNil2End : (p : [<] `Sub'` [<]) -> p = End
+lteNil2End End = Refl
+
+private
+0 ltemEnd : SubView p n -> p = End -> n = 0
+ltemEnd (END eq) Refl = eq
+
+private
+0 ltemEvenDrop : {p : xs `Sub'` (ys :< y)} ->
+                 n = 2 * n' -> SubView p n -> (q ** p = Drop q)
+ltemEvenDrop eq (KEEP _ eq') = absurd $ lsbMutex eq eq'
+ltemEvenDrop eq (DROP {})    = (_ ** Refl)
+
+private
+0 fromDROP : {lte : xs `Sub'` ys :< z} -> n = 2 * n' -> lte = Drop lte' ->
+             SubView lte n -> SubView lte' n'
+fromDROP eq Refl (DROP {n} p Refl) =
+  let eq = doubleInj eq {m = n, n = n'} in
+  rewrite sym eq in p
+
+private
+0 ltemOddKeep : {p : (xs :< x) `Sub'` (ys :< x)} -> {n' : Nat} ->
+                n = S (2 * n') -> SubView p n -> (q ** p = Keep q)
+ltemOddKeep eq (KEEP {})    = (_ ** Refl)
+ltemOddKeep eq (DROP _ eq') = absurd $ lsbMutex eq' eq
+ltemOddKeep eq (END _) impossible
+
+private
+0 ltemOddLeft : {0 n, n' : Nat} -> {lte : xs `Sub'` ys :< z} ->
+                n = S (2 * n') -> SubView lte n ->
+                (xs' ** xs = xs' :< z)
+ltemOddLeft eq {lte = Keep p} _ = (_ ** Refl)
+ltemOddLeft eq {lte = Drop p} (DROP n' eq') = void $ lsbMutex eq' eq
+
+private
+0 fromKEEP : {lte : xs :< z `Sub'` ys :< z} ->
+             n = S (2 * n') -> lte = Keep lte' ->
+             SubView lte n -> SubView lte' n'
+fromKEEP eq Refl (KEEP {n} p Refl) =
+  let eq = sDoubleInj eq {m = n, n = n'} in
+  rewrite sym eq in p
+
+
+export
+view : Length ys => (m : Sub xs ys) -> SubView m.lte m.mask
+view @{Z} (SubM mask lte view0) with 0 (lteNilRight lte)
+  _ | Refl =
+    rewrite lteNil2End lte in
+    rewrite ltemEnd view0 (lteNil2End lte) in
+    END Refl
+view @{S sy} (SubM mask lte view0) {ys = ys :< z} with (viewLsb mask)
+  _ | Lsb0 n eqn with (splitExEq $ ltemEvenDrop eqn view0)
+    _ | Evidence lte' eql =
+      rewrite eqn in rewrite eql in
+      DROP (fromDROP eqn eql view0) Refl
+  _ | Lsb1 n eqn with (splitExEq $ ltemOddLeft eqn view0)
+    _ | Evidence xs' Refl =
+      let Evidence q eqq = splitExEq $ ltemOddKeep eqn view0 in
+      rewrite eqn in rewrite eqq in
+      KEEP (fromKEEP eqn eqq view0) Refl
+
+public export %inline
+(.view) : Length ys => (m : Sub xs ys) -> SubView m.lte m.mask
+(.view) = view
+
+public export %inline
+review : Length ys => {m : Nat} -> {0 lte : xs `Sub'` ys} ->
+         (0 _ : SubView lte m) -> SubView lte m
+review v = view $ sub v
+
+
+
+export
+ltemLen : (sy : Length ys) => xs `Sub` ys -> length xs `LTE` sy.nat
+ltemLen (SubM mask lte view0) {sy} with (review view0)
+  ltemLen (SubM _ _ _)            | END eq    = LTEZero
+  ltemLen (SubM _ _ _) {sy = S _} | KEEP v eq = LTESucc $ ltemLen $ sub v
+  ltemLen (SubM _ _ _) {sy = S _} | DROP v eq = lteSuccRight $ ltemLen $ sub v
+
+export
+ltemNilRight : xs `Sub` [<] -> xs = [<]
+ltemNilRight m = irrelevantEq $ lteNilRight m.lte
+
+
+export %inline
+dropLast : Length ys => (xs :< x) `Sub` ys -> xs `Sub` ys
+dropLast (SubM _ _ view0) @{sy} with (review view0)
+  dropLast (SubM _ _ _)        | KEEP v _ = drop $ sub v
+  dropLast (SubM _ _ _) @{S _} | DROP v _ = drop $ dropLast $ sub v
+
+
+export
+Uninhabited (xs :< x `Sub` [<]) where
+  uninhabited sub = void $ uninhabited sub.lte
+
+export
+Length xs => Uninhabited (xs :< x `Sub` xs) where
+  uninhabited (SubM _ _ view0) @{sx} with (review view0)
+    uninhabited (SubM _ _ _) @{S _} | KEEP v _ = uninhabited $ sub v
+    uninhabited (SubM _ _ _) @{S _} | DROP v _ = uninhabited $ dropLast $ sub v
+
+
+export
+refl : Length xs => xs `Sub` xs
+refl @{Z}   = end
+refl @{S s} = keep refl
+
+export
+0 reflLte : {sx : Length xs} -> (refl @{sx}).lte = refl' @{sx}
+reflLte {sx = Z}   = Refl
+reflLte {sx = S s} = trans (keepLte _) $ cong Keep reflLte
+
+public export %inline
+Reflexive (Scope a) Sub where reflexive = refl
+
+mutual
+  private
+  antisym_ : Length xs => Length ys =>
+             {0 p : xs `Sub'` ys} -> {0 q : ys `Sub'` xs} ->
+             SubView p m1 -> SubView q m2 -> xs = ys
+  antisym_ (END _)  (END _) = Refl
+  antisym_ (KEEP v1 _) (KEEP v2 _ {z}) @{S sx} @{S sy} =
+    cong (:< z) $ antisym (SubM _ _ v1) (SubM _ _ v2)
+  antisym_ (KEEP {}) (DROP {}) {p = Keep p} {q = Drop q} =
+    void $ succNotLTEpred $ lteLen q `transitive` lteLen p
+  antisym_ (DROP {}) (KEEP {}) {p = Drop p} {q = Keep q} =
+    void $ succNotLTEpred $ lteLen p `transitive` lteLen q
+  antisym_ (DROP {}) (DROP {}) {p = Drop p} {q = Drop q} =
+    void $ succNotLTEpred $ lteLen p `transitive` lteSuccLeft (lteLen q)
+
+  export
+  antisym : Length xs => Length ys => xs `Sub` ys -> ys `Sub` xs -> xs = ys
+  antisym v1 v2 = antisym_ v1.view v2.view
+
+public export %inline
+Antisymmetric (Scope a) Sub where
+  antisymmetric p q = antisym p q
+
+
+mutual
+  private
+  trans_ : Length ys => Length zs =>
+           {0 p : xs `Sub'` ys} -> {0 q : ys `Sub'` zs} ->
+           SubView p m1 -> SubView q m2 -> xs `Sub` zs
+  trans_ (END _) (END _) = end
+  trans_ (KEEP v1 _) (KEEP v2 _) @{S sy} @{S sz} = keep $ sub v1 `trans` sub v2
+  trans_ (DROP v1 _) (KEEP v2 _) @{S sy} @{S sz} = drop $ sub v1 `trans` sub v2
+  trans_ v1 (DROP v2 _) @{sy} @{S sz} =
+    let Element m1' eq = getMask v1 in
+    drop $ SubM m1' _ (rewrite sym eq in v1) `trans` sub v2
+
+  export
+  trans : Length ys => Length zs => xs `Sub` ys -> ys `Sub` zs -> xs `Sub` zs
+  trans p q = trans_ p.view q.view
+
+public export %inline
+(.) : Length ys => Length zs => ys `Sub` zs -> xs `Sub` ys -> xs `Sub` zs
+(.) = flip trans
+
+public export %inline
+comp : Length ys => Length zs => ys `Sub` zs -> xs `Sub` ys -> xs `Sub` zs
+comp = (.)
+
+public export %inline
+Transitive (Scope a) Sub where
+  transitive p q = q . p
+
+
+public export
+zero : Length xs => [<] `Sub` xs
+zero @{Z}   = end
+zero @{S s} = drop zero
+
+export
+0 zeroLte : {sx : Length xs} -> (zero @{sx}).lte = zero' @{sx}
+zeroLte {sx = Z}   = Refl
+zeroLte {sx = S s} = trans (dropLte zero) $ cong Drop zeroLte
+
+public export
+single : Length xs => x `Elem` xs -> [< x] `Sub` xs
+single @{S sx} Here      = keep zero
+single @{S sx} (There p) = drop $ single p
+
+export
+0 singleLte : {sx : Length xs} -> (p : x `Elem` xs) ->
+              (single p @{sx}).lte = single' p @{sx}
+singleLte {sx = S s} Here      = trans (keepLte zero) $ cong Keep zeroLte
+singleLte {sx = S s} (There p) = trans (dropLte _) $ cong Drop $ singleLte p
+
+
+mutual
+  private
+  app0 : Length ys2 =>
+         (l : xs1 `Sub` ys1) ->
+         {rm : Nat} -> {0 rl : xs2 `Sub'` ys2} -> (rv : SubView rl rm) ->
+         (xs1 ++ xs2) `Sub` (ys1 ++ ys2)
+  app0 l (END eq)              = l
+  app0 l (KEEP v Refl) @{S sy} = keep $ l ++ sub v
+  app0 l (DROP v Refl) @{S sy} = drop $ l ++ sub v
+
+  export
+  app : Length ys2 =>
+        xs1 `Sub` ys1 -> xs2 `Sub` ys2 -> (xs1 ++ xs2) `Sub` (ys1 ++ ys2)
+  app l r = app0 l r.view
+
+  public export %inline
+  (++) : Length ys2 =>
+         xs1 `Sub` ys1 -> xs2 `Sub` ys2 -> (xs1 ++ xs2) `Sub` (ys1 ++ ys2)
+  (++) = app
+
+export
+0 appLte : {sy : Length ys2} ->
+           (l : xs1 `Sub` ys1) -> (r : xs2 `Sub` ys2) ->
+           (app l r @{sy}).lte = app' l.lte r.lte
+appLte l r@(SubM 0 End (END Refl)) =
+  cong (\v => (app0 l v).lte) (viewIrrel (view end) (END Refl))
+appLte l r@(SubM (S (2 * n)) (Keep p) (KEEP v Refl)) {sy = S sy} =
+  trans (cong (\v => (app0 l v @{S sy}).lte) (viewIrrel _ (KEEP v Refl))) $
+  trans (keepLte _) $
+  cong Keep $ appLte l (sub v)
+appLte l r@(SubM 0 (Drop p) (DROP {n = 0} v Refl)) {sy = S sy} =
+  trans (cong (\v => (app0 l v @{S sy}).lte) (viewIrrel _ (DROP v Refl))) $
+  trans (dropLte _) $
+  cong Drop $ appLte l (sub v)
+appLte l r@(SubM (2 * S n) (Drop p) (DROP {n = S n} v Refl)) {sy = S sy} =
+  trans (cong (\v => (app0 l v @{S sy}).lte) (viewIrrel _ (DROP v Refl))) $
+  trans (dropLte _) $
+  cong Drop $ appLte l (sub v)
+appLte {xs2 = _ :< _, ys2 = [<]} _ (SubM _ _ _) impossible
+
+export
+0 keepAppRight : {sy : Length ys2} ->
+                 (l : xs1 `Sub` ys1) -> (r : xs2 `Sub` ys2) ->
+                 (l ++ keep r) @{S sy} = keep ((l ++ r) @{sy})
+keepAppRight l (SubM mask _ _) = rewrite (lsbOdd mask).snd in Refl
+
+export
+0 dropAppRight : (l : xs1 `Sub` ys1) -> (r : xs2 `Sub` ys2) ->
+                 (l ++ drop r) @{S sy} = drop ((l ++ r) @{sy})
+dropAppRight l r = lteEq $
+  trans (appLte l (drop r)) $
+  trans (cong (app' l.lte) (dropLte r)) $
+  trans (cong Drop (sym (appLte l r))) $
+  sym $ dropLte (l ++ r)
+
+
+export
+0 endRight : {xs, ys : Scope a} -> (sub : xs `Sub` ys) -> sub = (sub ++ Sub.end)
+endRight sub = Refl
+
+
+private
+0 transDrop_ : {p : xs `Sub'` ys} -> {q : ys `Sub'` zs} ->
+               (pv : SubView p m1) -> (qv : SubView q m2) ->
+               trans_ pv (DROP qv qe) @{sy} @{S sz} =
+                 drop (trans_ pv qv @{sy} @{sz})
+transDrop_ {sy = Z} {sz = sz} (END Refl) qv =
+  cong (\v => drop $ trans_ {m2, q} (END Refl) v) $ viewIrrel {}
+transDrop_ {sy = S sy} {sz = sz} (KEEP pv Refl) qv {p = Keep p} =
+  cong2 (\x, y => drop (trans_ @{S sy} x y)) (viewIrrel {}) (viewIrrel {})
+transDrop_ {sy = S sy} {sz = S sz} (DROP pv Refl) qv =
+  cong2 (\x, y => drop (trans_ @{S sy} @{S sz} x y))
+    (viewIrrel {}) (viewIrrel {})
+transDrop_ {ys = _ :< _, zs = [<]} _ _ impossible
+
+private
+0 transLte_ : {p : xs `Sub'` ys} -> {q : ys `Sub'` zs} ->
+              (pv : SubView p m1) -> (qv : SubView q m2) ->
+              (trans_ pv qv @{sy} @{sz}).lte = trans' p q
+transLte_ (END _) (END _) = Refl
+transLte_ (KEEP pv pe) (KEEP qv qe) {sy = S _} {sz = S _} =
+  trans (keepLte _) $ cong Keep $ transLte_ {}
+transLte_ (DROP pv pe) (KEEP qv qe) {sy = S _} {sz = S _} =
+  trans (dropLte _) $ cong Drop $ transLte_ {}
+transLte_ pv (DROP qv qe) {sz = S _} =
+  trans (cong lte $ transDrop_ pv qv) $
+  trans (dropLte _) $ cong Drop $ transLte_ pv qv
+transLte_ {ys = _ :< _, zs = [<]} _ _ impossible
+
+export
+0 transLte : {sy : Length ys} -> {sz : Length zs} ->
+             (p : xs `Sub` ys) -> (q : ys `Sub` zs) ->
+             (trans p q @{sy} @{sz}).lte = trans' p.lte q.lte
+transLte p q = transLte_ p.view q.view
+
+public export
+0 compLte : {sy : Length ys} -> {sz : Length zs} ->
+            (q : ys `Sub` zs) -> (p : xs `Sub` ys) ->
+            ((q . p) @{sy} @{sz}).lte = q.lte . p.lte 
+compLte q p = transLte p q
+
+
+||| if `p` holds for all elements of the main list,
+||| it holds for all elements of the sublist
+export
+subAll : Length ys => xs `Sub` ys -> All prop ys -> All prop xs
+subAll (SubM _ _ v) ps @{sy} with (review v)
+  subAll (SubM _ _ _) [<]               | END    _ = [<]
+  subAll (SubM _ _ _) (ps :< p) @{S sy} | KEEP v _ = subAll (sub v) ps :< p
+  subAll (SubM _ _ _) (ps :< p) @{S sy} | DROP v _ = subAll (sub v) ps
+
+
+||| if `p` holds for one element of the sublist,
+||| it holds for one element of the main list
+export
+subAny : Length ys => xs `Sub` ys -> Any prop xs -> Any prop ys
+subAny (SubM _ _ v) p @{sy} with (review v)
+  subAny (SubM _ _ _) (Here  p)         | KEEP v _ = Here p
+  subAny (SubM _ _ _) (There p) @{S sy} | KEEP v _ = There $ subAny (sub v) p
+  subAny (SubM _ _ _) p         @{S sy} | DROP v _ = There $ subAny (sub v) p
--- a/lib/Quox/Pretty.idr
+++ b/lib/Quox/Pretty.idr
@ -69,7 +69,6 @@ hlF' = map . hl'
 export %inline
 parens : Doc HL -> Doc HL
 parens doc = hl Delim "(" <+> doc <+> hl Delim ")"
-%hide Symbols.parens

 export %inline
 parensIf : Bool -> Doc HL -> Doc HL
--- a/lib/Quox/Scope.idr
+++ b/lib/Quox/Scope.idr
@ -0,0 +1,94 @@
+module Quox.Scope
+
+import public Quox.OPE
+
+
+public export
+record Sub {a : Type} (t : Scoped a) (xs : Scope a) where
+  constructor Su
+  {0 support : Scope a}
+  term : t support
+  thin : support `LTE` xs
+
+public export
+CoverS : Sub s xs -> Sub t xs -> Type
+CoverS ss tt = Cover ss.thin tt.thin
+
+export %inline
+inj : Length xs => t xs -> Sub t xs
+inj x = Su x id
+
+export %inline
+flat : Sub (Sub t) xs -> Sub t xs
+flat (Su (Su x q) p) = Su x (p . q)
+
+export %inline
+thinSub : xs `LTE` ys -> Sub t xs -> Sub t ys
+thinSub p x = flat $ Su x p
+
+export %inline
+map : (forall x. s x -> t x) -> Sub s x -> Sub t x
+map f = {term $= f}
+
+public export
+data Unit : Scoped a where
+  Nil : Unit [<]
+
+export %inline
+unit : Length xs => Sub Unit xs
+unit = Su [] zero
+
+public export
+record Coprod {a : Type} {xs, ys, zs : Scope a}
+              (p : xs `LTE` zs) (q : ys `LTE` zs) where
+  constructor Cop
+  {0 scope : Scope a}
+  {thin : scope `LTE` zs}
+  {thinP : xs `LTE` scope}
+  {thinQ : ys `LTE` scope}
+  compP : Comp thin thinP p
+  compQ : Comp thin thinQ q
+  0 cover : Cover thinP thinQ
+
+export
+coprod : (p : xs `LTE` zs) -> (q : ys `LTE` zs) -> Coprod p q
+coprod End      End      = %search
+coprod (Keep p) (Keep q) = let Cop {} = coprod p q in %search
+coprod (Keep p) (Drop q) = let Cop {} = coprod p q in %search
+coprod (Drop p) (Keep q) = let Cop {} = coprod p q in %search
+coprod (Drop p) (Drop q) =
+  -- idk why this one is harder to solve
+  let Cop compP compQ cover = coprod p q in
+  Cop (CD0 compP) (CD0 compQ) cover
+
+public export
+record Pair {a : Type} (s, t : Scoped a) (zs : Scope a) where
+  constructor MkPair
+  fst : Sub s zs
+  snd : Sub t zs
+  0 cover : CoverS fst snd
+
+export
+pair : Sub s xs -> Sub t xs -> Sub (Pair s t) xs
+pair (Su x p) (Su y q) =
+  let c = coprod p q in
+  Su (MkPair (Su x c.thinP) (Su y c.thinQ) c.cover) c.thin
+
+
+public export
+data Var : a -> Scope a -> Type where
+  Only : Var x [< x]
+
+export %inline
+var : (0 x : a) -> [< x] `LTE` xs => Sub (Var x) xs
+var x @{p} = Su Only p
+
+
+infix 0 \\\, \\
+public export
+data Bind : (t : Scoped a) -> (new, old : Scope a) -> Type where
+  (\\\) : new' `LTE` new -> t (old ++ new') -> Bind t new old
+
+(\\) : (new : Scope a) -> Sub t (old ++ new) -> Sub (Bind t new) old
+vs \\ Su term p with (split vs p)
+  vs \\ Su term (l ++ r) | MkSplit l r Refl Refl = Su (r \\\ term) l
--- a/lib/Quox/Syntax/Shift.idr
+++ b/lib/Quox/Syntax/Shift.idr
@ -110,7 +110,14 @@ export
 ssDownEqv SZ      = EqSS EqSZ
 ssDownEqv (SS by) = EqSS $ ssDownEqv by

-%transform "Shift.ssDown" ssDown by = believe_me (SS by)
+private %inline
+ssDownViaNat : Shift (S from) to -> Shift from to
+ssDownViaNat by =
+  rewrite shiftDiff by in
+  rewrite sym $ plusSuccRightSucc by.nat from in
+  fromNat $ S by.nat
+
+%transform "Shift.ssDown" ssDown = ssDownViaNat


 public export
@ -118,12 +125,12 @@ shift : Shift from to -> Var from -> Var to
 shift SZ      i = i
 shift (SS by) i = VS $ shift by i

-private
+private %inline
 shiftViaNat' : (by : Shift from to) -> (i : Var from) ->
               (0 p : by.nat + i.nat `LT` to) -> Var to
 shiftViaNat' by i p = V $ by.nat + i.nat

-private
+private %inline
 shiftViaNat : Shift from to -> Var from -> Var to
 shiftViaNat by i = shiftViaNat' by i $ shiftVarLT by i

@ -156,12 +163,12 @@ compNatProof by bz =
  0 (>>>) : a = b -> b = c -> a = c
  x >>> y = trans x y

-private
+private %inline
 compViaNat' : (by : Shift from mid) -> (bz : Shift mid to) ->
              Shift from (by.nat + bz.nat + from)
 compViaNat' by bz = fromNat $ by.nat + bz.nat

-private
+private %inline
 compViaNat : (by : Shift from mid) -> (bz : Shift mid to) -> Shift from to
 compViaNat by bz = rewrite compNatProof by bz in compViaNat' by bz

@ -200,12 +207,13 @@ public export
 interface CanShift f where
  (//) : f from -> Shift from to -> f to

-export CanShift Var where i // by = shift by i
+export %inline
+CanShift Var where i // by = shift by i

 namespace CanShift
-  public export
+  public export %inline
  [Map] (Functor f, CanShift tm) => CanShift (f . tm) where
    x // by = map (// by) x

-  public export
+  public export %inline
  [Const] CanShift (\_ => a) where x // _ = x
--- a/lib/Quox/Syntax/Term/Reduce.idr
+++ b/lib/Quox/Syntax/Term/Reduce.idr
@ -116,6 +116,7 @@ pushSubstsE' : Elim d n -> Elim d n
 pushSubstsE' e = (pushSubstsE e).fst


+{- [todo] remove these probably?
 mutual
  -- tightening a term/elim also causes substitutions to be pushed through.
  -- this is because otherwise a variable in an unused part of the subst
@ -156,6 +157,7 @@ mutual
  Tighten (ScopeTerm d) where
    tighten p (TUsed   body) = TUsed   <$> tighten (Keep p) body
    tighten p (TUnused body) = TUnused <$> tighten p body
+-}


 public export %inline
--- a/lib/Quox/Syntax/Var.idr
+++ b/lib/Quox/Syntax/Var.idr
@ -2,7 +2,6 @@ module Quox.Syntax.Var

 import Quox.Name
 import Quox.Pretty
-import Quox.OPE

 import Data.Nat
 import Data.List
@ -264,6 +263,7 @@ decEqFromBool i j =

 public export %inline DecEq (Var n) where decEq = varDecEq

+{- [todo] remove this probably?
 export
 Tighten Var where
  tighten Id       i      = pure i
@ -271,3 +271,4 @@ Tighten Var where
  tighten (Drop q) (VS i) = tighten q i
  tighten (Keep q) VZ     = pure VZ
  tighten (Keep q) (VS i) = VS <$> tighten q i
+-}
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@ -11,6 +11,12 @@ modules =
  Quox.NatExtra,
  Quox.Unicode,
  Quox.OPE,
+  Quox.OPE.Basics,
+  Quox.OPE.Length,
+  Quox.OPE.Sub,
+  Quox.OPE.Split,
+  Quox.OPE.Comp,
+  Quox.OPE.Cover,
  Quox.Pretty,
  Quox.Syntax,
  Quox.Syntax.Dim,
Author	SHA1	Message	Date
rhiannon morris	5e11433c9f	bit mask OPE stuff	2022-11-15 15:44:49 +01:00
rhiannon morris	42acbfc4ac	rename SubView to Sub (Sub to Sub') and port over props	2022-11-06 18:35:42 +01:00
rhiannon morris	8582862914	remove stdlib duplication	2022-11-06 13:03:54 +01:00
rhiannon morris	5c3f2510fe	split OPE stuff into modules	2022-11-06 12:43:52 +01:00
rhiannon morris	4b64399891	bitmask representation of lte	2022-11-06 12:43:52 +01:00
rhiannon morris	53bbcbf8c7	OPE & scope stuff	2022-11-06 12:43:52 +01:00
rhiannon morris	23c008b57a	%inline	2022-11-06 12:43:52 +01:00
rhiannon morris	e7272333cb	remove a believe_me	2022-11-06 12:43:52 +01:00
rhiannon morris	e1a9d99514	idris 0.6.0 [with temporary flake fork]	2022-11-06 12:43:52 +01:00
rhiannon morris	014de47a4c	flake fix	2022-11-06 12:43:52 +01:00
rhiannon morris	c8187c0801	OPE & scope stuff	2022-10-10 17:30:46 +02:00