From 5c3f2510fe0e6d6cde617a869146d3cf40a45846 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 6 Nov 2022 12:39:33 +0100
Subject: [PATCH] split OPE stuff into modules

---
 lib/Quox/OPE.idr        | 371 +---------------------------------------
 lib/Quox/OPE/Basics.idr |  22 +++
 lib/Quox/OPE/Comp.idr   |  83 +++++++++
 lib/Quox/OPE/Cover.idr  |  24 +++
 lib/Quox/OPE/Length.idr |  24 +++
 lib/Quox/OPE/Split.idr  |  27 +++
 lib/Quox/OPE/Sub.idr    | 254 +++++++++++++++++++++++++++
 lib/Quox/Syntax/Var.idr |   1 -
 lib/quox-lib.ipkg       |   6 +
 9 files changed, 446 insertions(+), 366 deletions(-)
 create mode 100644 lib/Quox/OPE/Basics.idr
 create mode 100644 lib/Quox/OPE/Comp.idr
 create mode 100644 lib/Quox/OPE/Cover.idr
 create mode 100644 lib/Quox/OPE/Length.idr
 create mode 100644 lib/Quox/OPE/Split.idr
 create mode 100644 lib/Quox/OPE/Sub.idr

diff --git a/lib/Quox/OPE.idr b/lib/Quox/OPE.idr
index e09f9af..319638d 100644
--- a/lib/Quox/OPE.idr
+++ b/lib/Quox/OPE.idr
@@ -2,368 +2,9 @@
 ||| a smaller scope and part of a larger one.
 module Quox.OPE
 
-import Quox.NatExtra
-import public Data.DPair
-import public Data.SnocList
-import public Data.SnocList.Elem
-
-%default total
-
-LTE_n = Nat.LTE
-%hide Nat.LTE
-
-
-public export
-Scope : Type -> Type
-Scope = SnocList
-
-public export
-data LTE : Scope a -> Scope a -> Type where
-  End  : [<] `LTE` [<]
-  Keep : xs `LTE` ys -> xs :< z `LTE` ys :< z
-  Drop : xs `LTE` ys -> xs      `LTE` ys :< z
-%name LTE p, q
-
--- [todo] bitmask representation???
-
-
-export
-dropLast : (xs :< x) `LTE` ys -> xs `LTE` ys
-dropLast (Keep p) = Drop p
-dropLast (Drop p) = Drop $ dropLast p
-
-export
-Uninhabited (xs :< x `LTE` [<]) where uninhabited _ impossible
-
-export
-Uninhabited (xs :< x `LTE` xs) where
-  uninhabited (Keep p) = uninhabited p
-  uninhabited (Drop p) = uninhabited $ dropLast p
-
-
-export
-0 lteLen : xs `LTE` ys -> length xs `LTE_n` length ys
-lteLen End      = LTEZero
-lteLen (Keep p) = LTESucc $ lteLen p
-lteLen (Drop p) = lteSuccRight $ lteLen p
-
-export
-0 lteNilRight : xs `LTE` [<] -> xs = [<]
-lteNilRight End = Refl
-
-export
-0 lteNilLeftDrop : (p : [<] `LTE` (xs :< x)) -> Exists (\q => p = Drop q)
-lteNilLeftDrop (Drop q) = Evidence q Refl
-
-export
-0 lteNil2End : (p : [<] `LTE` [<]) -> p = End
-lteNil2End End = Refl
-
-
-public export
-data Length : Scope a -> Type where
-  Z : Length [<]
-  S : (s : Length xs) -> Length (xs :< x)
-%name Length s
-%builtin Natural Length
-
-namespace 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 lengthOk : (s : Length xs) -> s.nat = length xs
-  lengthOk Z     = Refl
-  lengthOk (S s) = cong S $ lengthOk s
-
-export %hint
-lengthLeft : xs `LTE` ys -> Length xs
-lengthLeft End      = Z
-lengthLeft (Keep p) = S (lengthLeft p)
-lengthLeft (Drop p) = lengthLeft p
-
-export %hint
-lengthRight : xs `LTE` ys -> Length ys
-lengthRight End      = Z
-lengthRight (Keep p) = S (lengthRight p)
-lengthRight (Drop p) = S (lengthRight p)
-
-
-export
-id : Length xs => xs `LTE` xs
-id @{Z}   = End
-id @{S s} = Keep id
-
-export
-zero : Length xs => [<] `LTE` xs
-zero @{Z}   = End
-zero @{S s} = Drop zero
-
-export
-single : Length xs => x `Elem` xs -> [< x] `LTE` xs
-single @{S _} Here      = Keep zero
-single @{S _} (There p) = Drop $ single p
-
-
-export
-(.) : ys `LTE` zs -> xs `LTE` ys -> xs `LTE` zs
-End    . End    = End
-Keep p . Keep q = Keep (p . q)
-Keep p . Drop q = Drop (p . q)
-Drop p . q      = Drop (p . q)
-
-export
-(++) : xs1 `LTE` ys1 -> xs2 `LTE` ys2 -> (xs1 ++ xs2) `LTE` (ys1 ++ ys2)
-p ++ End    = p
-p ++ Keep q = Keep (p ++ q)
-p ++ Drop q = Drop (p ++ q)
-
-
-
-public export
-data LTEMaskView : (lte : xs `LTE` ys) -> (mask : Nat) -> Type where
-  [search lte]
-  END  : LTEMaskView End 0
-  KEEP : (0 _ : LTEMaskView p n) -> LTEMaskView (Keep p) (S (2 * n))
-  DROP : (0 _ : LTEMaskView p n) -> LTEMaskView (Drop p)    (2 * n)
-%name LTEMaskView p, q
-
-record LTEMask {a : Type} (xs, ys : Scope a) where
-  constructor LTEM
-  mask : Nat
-  0 lte : xs `LTE` ys
-  0 view0 : LTEMaskView lte mask
-%name LTEMask m
-
-namespace View
-  private
-  0 lteMaskEnd' : LTEMaskView p n -> p = End -> n = 0
-  lteMaskEnd' END Refl = Refl
-
-  private
-  0 lteMaskDrop' : LTEMaskView p n -> p = Drop q -> (n' ** n = 2 * n')
-  lteMaskDrop' (DROP p {n = n'}) Refl = (n' ** Refl)
-
-  private
-  0 lteMaskEven' : {p : xs `LTE` (ys :< y)} ->
-                   n = 2 * n' -> LTEMaskView p n -> (q ** p = Drop q)
-  lteMaskEven' eq (KEEP q) = absurd $ lsbMutex' eq Refl
-  lteMaskEven' eq (DROP q) = (_ ** Refl)
-
-  private
-  lteMaskEven : {0 p : xs `LTE` (ys :< y)} ->
-                (0 _ : LTEMaskView p (2 * n)) -> Exists (\q => p = Drop q)
-  lteMaskEven q =
-    let 0 res = lteMaskEven' Refl q in
-    Evidence res.fst (irrelevantEq res.snd)
-
-  private
-  0 fromDROP' : {lte : xs `LTE` ys} -> n = 2 * n' ->
-                LTEMaskView (Drop lte) n -> LTEMaskView lte n'
-  fromDROP' eq (DROP {n} p) =
-    let eq = doubleInj eq {m = n, n = n'} in
-    rewrite sym eq in p
-
-  private
-  0 fromDROP : LTEMaskView (Drop lte) (2 * n) -> LTEMaskView lte n
-  fromDROP = fromDROP' Refl
-
-  private
-  0 lteMaskOdd' : {p : (xs :< x) `LTE` (ys :< x)} -> {n' : Nat} ->
-                  n = S (2 * n') -> LTEMaskView p n -> (q ** p = Keep q)
-  lteMaskOdd' eq (KEEP q) = (_ ** Refl)
-  lteMaskOdd' eq (DROP q) = absurd $ lsbMutex' Refl eq
-  lteMaskOdd' _  END      impossible
-
-  private
-  lteMaskOdd : (0 _ : LTEMaskView p (S (2 * n))) -> Exists (\q => p = Keep q)
-  lteMaskOdd q =
-    let 0 res = lteMaskOdd' Refl q in
-    Evidence res.fst (irrelevantEq res.snd)
-
-  private
-  0 lteMaskOddHead' : {p : (xs :< x) `LTE` (ys :< y)} -> {n' : Nat} ->
-                      n = S (2 * n') -> LTEMaskView p n -> x = y
-  lteMaskOddHead' eq (KEEP q) = Refl
-  lteMaskOddHead' eq (DROP q) = absurd $ lsbMutex' Refl eq
-  lteMaskOddHead' eq END      impossible
-
-  private
-  lteMaskOddHead : {0 p : (xs :< x) `LTE` (ys :< y)} ->
-                   (0 _ : LTEMaskView p (S (2 * n))) -> x = y
-  lteMaskOddHead q = irrelevantEq $ lteMaskOddHead' Refl q
-
-  private
-  0 fromKEEP' : {lte : xs `LTE` ys} -> n = S (2 * n') ->
-                LTEMaskView (Keep lte) n -> LTEMaskView lte n'
-  fromKEEP' eq (KEEP {n} p) =
-    let eq = doubleInj (injective eq) {m = n, n = n'} in
-    rewrite sym eq in p
-
-  private
-  0 fromKEEP : LTEMaskView (Keep lte) (S (2 * n)) -> LTEMaskView lte n
-  fromKEEP = fromKEEP' Refl
-
-  export
-  view : (sx : Length xs) => (sy : Length ys) =>
-         (m : LTEMask xs ys) -> LTEMaskView m.lte m.mask
-  view @{Z} @{Z} (LTEM {lte, view0, _}) =
-    rewrite lteNil2End lte in
-    rewrite lteMaskEnd' view0 (lteNil2End lte) in
-    END
-  view @{S _} @{Z} (LTEM {lte, _}) = void $ absurd lte
-  view @{Z} @{S sy} (LTEM mask lte view0) =
-    rewrite (lteNilLeftDrop lte).snd in
-    rewrite (lteMaskDrop' view0 (lteNilLeftDrop lte).snd).snd in
-    DROP $ let DROP p = view0 in p
-  view @{S sx} @{S sy} (LTEM mask lte view0) with (viewLsb mask)
-    view @{S sx} @{S sy} (LTEM (2 * n) lte view0)
-        | Evidence Even (Lsb0 n) with (lteMaskEven view0)
-      view @{S sx} @{S sy} (LTEM (2 * m) (Drop lte) view0)
-          | Evidence Even (Lsb0 m) | Evidence lte Refl =
-              DROP $ fromDROP view0
-    view @{S sx} @{S sy} (LTEM (S (2 * n)) lte view0)
-        | Evidence Odd (Lsb1 n) with (lteMaskOddHead view0)
-      view @{S sx} @{S sy} (LTEM (S (2 * n)) lte view0)
-          | Evidence Odd (Lsb1 n) | Refl with (lteMaskOdd view0)
-        view @{S sx} @{S sy} (LTEM (S (2 * n)) (Keep lte) view0)
-            | Evidence Odd (Lsb1 n) | Refl | Evidence lte Refl =
-                KEEP $ fromKEEP view0
-
-
-
-public export
-record Split {a : Type} (xs, ys, zs : Scope a) (p : xs `LTE` ys ++ zs) where
-  constructor MkSplit
-  {0 leftSub, rightSub : Scope a}
-  leftThin : leftSub `LTE` ys
-  rightThin : rightSub `LTE` zs
-  0 eqScope : xs = leftSub ++ rightSub
-  0 eqThin : p ~=~ leftThin ++ rightThin
-
-export
-split : (zs : Scope a) -> (p : xs `LTE` ys ++ zs) -> Split xs ys zs p
-split [<] p = MkSplit p zero Refl Refl
-split (zs :< z) (Keep p) with (split zs p)
-  split (zs :< z) (Keep (l ++ r)) | MkSplit l r Refl Refl =
-    MkSplit l (Keep r) Refl Refl
-split (zs :< z) (Drop p) {xs} with (split zs p)
-  split (zs :< z) (Drop (l ++ r)) {xs = _} | MkSplit l r Refl Refl =
-    MkSplit l (Drop r) Refl Refl
-
-
-public export
-data Comp : ys `LTE` zs -> xs `LTE` ys -> xs `LTE` 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)
-
-export
-comp : (p : ys `LTE` zs) -> (q : xs `LTE` ys) -> Comp p q (p . q)
-comp End      End      = CEE
-comp (Keep p) (Keep q) = CKK (comp p q)
-comp (Keep p) (Drop q) = CKD (comp p q)
-comp (Drop p) q        = CD0 (comp 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
-compZero : (sx : Length xs) => (sy : Length ys) =>
-           (p : xs `LTE` ys) -> Comp p (OPE.zero @{sx}) (OPE.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
-compIdLeft : (sy : Length ys) =>
-             (p : xs `LTE` ys) -> Comp (OPE.id @{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
-compIdRight : (sx : Length xs) =>
-              (p : xs `LTE` ys) -> Comp p (OPE.id @{sx}) p
-compIdRight {sx = Z}   End      = CEE
-compIdRight {sx = S _} (Keep p) = CKK (compIdRight p)
-compIdRight            (Drop p) = CD0 (compIdRight p)
-
-
-export
-0 compAssoc : (p : ys `LTE` zs) -> (q : xs `LTE` ys) -> (r : ws `LTE` 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
-
-
-public export
-Scoped : Type -> Type
-Scoped a = Scope a -> Type
-
-public export
-Subscope : Scope a -> Type
-Subscope ys = Exists (`LTE` ys)
-
-public export
-record SubMap {a : Type} {xs, ys, zs : Scope a}
-              (p : xs `LTE` zs) (q : ys `LTE` zs) where
-  constructor SM
-  thin : xs `LTE` ys
-  0 comp : Comp q thin p
-
-parameters (p : xs `LTE` ys)
-  export
-  subId : SubMap p p
-  subId = SM id (compIdRight p)
-
-  export
-  subZero : SubMap OPE.zero p
-  subZero = SM zero (compZero p)
-
-
-public export
-data All : (a -> Type) -> Scoped a where
-  Lin  : All p [<]
-  (:<) : All p xs -> p x -> All p (xs :< x)
-%name OPE.All ps, qs
-
-export
-mapAll : (forall x. p x -> q x) -> All p xs -> All q xs
-mapAll f [<]      = [<]
-mapAll f (x :< y) = mapAll f x :< f y
-
-export
-subAll : xs `LTE` 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
-
-
-public export
-data Cover_ : (overlap : Bool) -> xs `LTE` zs -> ys `LTE` 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)
-
-public export
-Cover : xs `LTE` zs -> ys `LTE` zs -> Type
-Cover = Cover_ True
-
-public export
-Partition : xs `LTE` zs -> ys `LTE` zs -> Type
-Partition = Cover_ False
-
+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
diff --git a/lib/Quox/OPE/Basics.idr b/lib/Quox/OPE/Basics.idr
new file mode 100644
index 0000000..d4d92fc
--- /dev/null
+++ b/lib/Quox/OPE/Basics.idr
@@ -0,0 +1,22 @@
+module Quox.OPE.Basics
+
+%default total
+
+public export
+Scope : Type -> Type
+Scope = SnocList
+
+public export
+Scoped : Type -> Type
+Scoped a = Scope a -> Type
+
+public export
+data All : (a -> Type) -> Scoped a where
+  Lin  : All p [<]
+  (:<) : All p xs -> p x -> All p (xs :< x)
+%name OPE.Basics.All ps, qs
+
+public export
+mapAll : (forall x. p x -> q x) -> All p xs -> All q xs
+mapAll f [<]      = [<]
+mapAll f (x :< y) = mapAll f x :< f y
diff --git a/lib/Quox/OPE/Comp.idr b/lib/Quox/OPE/Comp.idr
new file mode 100644
index 0000000..c2e8a74
--- /dev/null
+++ b/lib/Quox/OPE/Comp.idr
@@ -0,0 +1,83 @@
+module Quox.OPE.Comp
+
+import Quox.OPE.Basics
+import Quox.OPE.Length
+import Quox.OPE.Sub
+import Data.DPair
+
+%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)
+
+export
+comp : (p : ys `Sub` zs) -> (q : xs `Sub` ys) -> Comp p q (p . q)
+comp End      End      = CEE
+comp (Keep p) (Keep q) = CKK (comp p q)
+comp (Keep p) (Drop q) = CKD (comp p q)
+comp (Drop p) q        = CD0 (comp 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
+compZero : (sx : Length xs) => (sy : Length ys) =>
+           (p : xs `Sub` ys) -> Comp p (Sub.zero @{sx}) (Sub.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
+compIdLeft : (sy : Length ys) =>
+             (p : xs `Sub` ys) -> Comp (Sub.id @{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
+compIdRight : (sx : Length xs) =>
+              (p : xs `Sub` ys) -> Comp p (Sub.id @{sx}) p
+compIdRight {sx = Z}   End      = CEE
+compIdRight {sx = S _} (Keep p) = CKK (compIdRight p)
+compIdRight            (Drop p) = CD0 (compIdRight p)
+
+
+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
+
+
+public export
+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
+
+parameters (p : xs `Sub` ys)
+  export
+  subId : SubMap p p
+  subId = SM id (compIdRight p)
+
+  export
+  subZero : SubMap Sub.zero p
+  subZero = SM zero (compZero p)
diff --git a/lib/Quox/OPE/Cover.idr b/lib/Quox/OPE/Cover.idr
new file mode 100644
index 0000000..63e5acb
--- /dev/null
+++ b/lib/Quox/OPE/Cover.idr
@@ -0,0 +1,24 @@
+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)
+
+public export
+Cover : xs `Sub` zs -> ys `Sub` zs -> Type
+Cover = Cover_ True
+
+public export
+Partition : xs `Sub` zs -> ys `Sub` zs -> Type
+Partition = Cover_ False
+
diff --git a/lib/Quox/OPE/Length.idr b/lib/Quox/OPE/Length.idr
new file mode 100644
index 0000000..c280327
--- /dev/null
+++ b/lib/Quox/OPE/Length.idr
@@ -0,0 +1,24 @@
+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
diff --git a/lib/Quox/OPE/Split.idr b/lib/Quox/OPE/Split.idr
new file mode 100644
index 0000000..ea8215e
--- /dev/null
+++ b/lib/Quox/OPE/Split.idr
@@ -0,0 +1,27 @@
+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 : (zs : Scope a) -> (p : xs `Sub` ys ++ zs) -> Split xs ys zs p
+split [<] p = MkSplit p zero Refl Refl
+split (zs :< z) (Keep p) with (split zs p)
+  split (zs :< z) (Keep (l ++ r)) | MkSplit l r Refl Refl =
+    MkSplit l (Keep r) Refl Refl
+split (zs :< z) (Drop p) {xs} with (split zs p)
+  split (zs :< z) (Drop (l ++ r)) {xs = _} | MkSplit l r Refl Refl =
+    MkSplit l (Drop r) Refl Refl
diff --git a/lib/Quox/OPE/Sub.idr b/lib/Quox/OPE/Sub.idr
new file mode 100644
index 0000000..de7e2b2
--- /dev/null
+++ b/lib/Quox/OPE/Sub.idr
@@ -0,0 +1,254 @@
+module Quox.OPE.Sub
+
+import Quox.OPE.Basics
+import Quox.OPE.Length
+import Quox.NatExtra
+import Data.DPair
+import Data.SnocList.Elem
+
+%default total
+
+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
+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
+id : Length xs => xs `Sub` xs
+id @{Z}   = End
+id @{S s} = Keep id
+
+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
+
+
+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
+(++) : xs1 `Sub` ys1 -> xs2 `Sub` ys2 -> (xs1 ++ xs2) `Sub` (ys1 ++ ys2)
+p ++ End    = p
+p ++ Keep q = Keep (p ++ q)
+p ++ Drop q = Drop (p ++ q)
+
+export
+0 appZeroRight : (p : xs `Sub` ys) -> p ++ zero @{len} {xs = [<]} = p
+appZeroRight {len = Z} p = Refl
+
+
+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
+
+
+
+public export
+data SubMaskView : (lte : xs `Sub` ys) -> (mask : Nat) -> Type where
+  [search lte]
+  END  : SubMaskView End 0
+  KEEP : {n : Nat} -> {0 p : xs `Sub` ys} ->
+         (0 v : SubMaskView p n) -> SubMaskView (Keep {z} p) (S (2 * n))
+  DROP : {n : Nat} -> {0 p : xs `Sub` ys} ->
+         (0 v : SubMaskView p n) -> SubMaskView (Drop {z} p)    (2 * n)
+%name SubMaskView v
+
+public export
+record SubMask {a : Type} (xs, ys : Scope a) where
+  constructor SubM
+  mask : Nat
+  0 lte : xs `Sub` ys
+  0 view0 : SubMaskView lte mask
+%name SubMask m
+
+private
+0 ltemNilLeftZero' : SubMaskView {xs = [<]} lte mask -> mask = 0
+ltemNilLeftZero' END      = Refl
+ltemNilLeftZero' (DROP v) = cong (2 *) $ ltemNilLeftZero' v
+
+export
+ltemNilLeftZero : (0 _ : SubMaskView {xs = [<]} lte mask) -> mask = 0
+ltemNilLeftZero v = irrelevantEq $ ltemNilLeftZero' v
+
+
+private
+0 lteNilLeftDrop0 : (p : [<] `Sub` (xs :< x)) -> (q ** p = Drop q)
+lteNilLeftDrop0 (Drop q) = (q ** Refl)
+
+private
+lteNilLeftDrop : (0 p : [<] `Sub` (xs :< x)) -> Exists (\q => p = Drop q)
+lteNilLeftDrop q =
+  let 0 res = lteNilLeftDrop0 q in
+  Evidence res.fst (irrelevantEq res.snd)
+
+private
+0 lteNil2End : (p : [<] `Sub` [<]) -> p = End
+lteNil2End End = Refl
+
+private
+0 ltemEnd' : SubMaskView p n -> p = End -> n = 0
+ltemEnd' END Refl = Refl
+
+private
+0 ltemEven' : {p : xs `Sub` (ys :< y)} ->
+              n = 2 * n' -> SubMaskView p n -> (q ** p = Drop q)
+ltemEven' eq (KEEP q) = absurd $ lsbMutex' eq Refl
+ltemEven' eq (DROP q) = (_ ** Refl)
+
+private
+ltemEven : {0 p : xs `Sub` (ys :< y)} ->
+           (0 _ : SubMaskView p (2 * n)) -> Exists (\q => p = Drop q)
+ltemEven q =
+  let 0 res = ltemEven' Refl q in
+  Evidence res.fst (irrelevantEq res.snd)
+
+private
+0 fromDROP' : {lte : xs `Sub` ys} -> n = 2 * n' ->
+              SubMaskView (Drop lte) n -> SubMaskView lte n'
+fromDROP' eq (DROP {n} p) =
+  let eq = doubleInj eq {m = n, n = n'} in
+  rewrite sym eq in p
+
+private
+0 ltemOdd' : {p : (xs :< x) `Sub` (ys :< x)} -> {n' : Nat} ->
+                n = S (2 * n') -> SubMaskView p n -> (q ** p = Keep q)
+ltemOdd' eq (KEEP q) = (_ ** Refl)
+ltemOdd' eq (DROP q) = absurd $ lsbMutex' Refl eq
+ltemOdd' eq END      impossible
+
+private
+ltemOdd : (0 _ : SubMaskView p (S (2 * n))) -> Exists (\q => p = Keep q)
+ltemOdd q =
+  let 0 res = ltemOdd' Refl q in
+  Evidence res.fst (irrelevantEq res.snd)
+
+private
+0 ltemOddHead' : {p : (xs :< x) `Sub` (ys :< y)} -> {n' : Nat} ->
+                    n = S (2 * n') -> SubMaskView p n -> x = y
+ltemOddHead' eq (KEEP q) = Refl
+ltemOddHead' eq (DROP q) = absurd $ lsbMutex' Refl eq
+ltemOddHead' eq END      impossible
+
+private
+ltemOddHead : {0 p : (xs :< x) `Sub` (ys :< y)} ->
+              (0 _ : SubMaskView p (S (2 * n))) -> x = y
+ltemOddHead q = irrelevantEq $ ltemOddHead' Refl q
+
+private
+0 fromKEEP' : {lte : xs `Sub` ys} -> n = S (2 * n') ->
+              SubMaskView (Keep lte) n -> SubMaskView lte n'
+fromKEEP' eq (KEEP {n} p) =
+  let eq = doubleInj (injective eq) {m = n, n = n'} in
+  rewrite sym eq in p
+
+export
+view : Length xs => Length ys =>
+       (m : SubMask xs ys) -> SubMaskView m.lte m.mask
+view @{Z} @{Z} (SubM {lte, view0, _}) =
+  rewrite lteNil2End lte in
+  rewrite ltemEnd' view0 (lteNil2End lte) in
+  END
+view @{S _} @{Z} (SubM {lte, _}) = void $ absurd lte
+view @{Z} @{S sy} (SubM mask lte view0) with (ltemNilLeftZero view0)
+  view @{Z} @{S sy} (SubM 0 lte view0)
+      | Refl with (lteNilLeftDrop lte)
+    view @{Z} @{S sy} (SubM 0 (Drop lte) view0)
+        | Refl | Evidence lte Refl =
+            DROP {n = 0} $ let DROP {n = 0} p = view0 in p
+view @{S sx} @{S sy} (SubM mask lte view0) with (viewLsb mask)
+  view @{S sx} @{S sy} (SubM (2 * n) lte view0)
+      | Evidence Even (Lsb0 n) with (ltemEven view0)
+    view @{S sx} @{S sy} (SubM (2 * m) (Drop lte) view0)
+        | Evidence Even (Lsb0 m) | Evidence lte Refl =
+            DROP $ fromDROP' Refl view0
+  view @{S sx} @{S sy} (SubM (S (2 * n)) lte view0)
+      | Evidence Odd (Lsb1 n) with (ltemOddHead view0)
+    view @{S sx} @{S sy} (SubM (S (2 * n)) lte view0)
+        | Evidence Odd (Lsb1 n) | Refl with (ltemOdd view0)
+      view @{S sx} @{S sy} (SubM (S (2 * n)) (Keep lte) view0)
+          | Evidence Odd (Lsb1 n) | Refl | Evidence lte Refl =
+              KEEP $ fromKEEP' Refl view0
+
+export
+(.view) : Length xs => Length ys =>
+          (m : SubMask xs ys) -> SubMaskView m.lte m.mask
+(.view) = view
+
+
+export
+ltemLen : Length xs => Length ys =>
+          xs `SubMask` ys -> length xs `LTE` length ys
+ltemLen @{sx} @{sy} lte@(SubM m l _) with (lte.view)
+  ltemLen @{sx} @{sy} lte@(SubM 0 End _) | END = LTEZero
+  ltemLen @{S sx} @{S sy} lte@(SubM (S (2 * n)) (Keep p) _) | (KEEP q) =
+    LTESucc $ ltemLen $ SubM n p q
+  ltemLen @{sx} @{S sy} lte@(SubM (2 * n) (Drop p) _) | (DROP q) =
+    lteSuccRight $ ltemLen $ SubM n p q
+
+export
+ltemNilRight : xs `SubMask` [<] -> xs = [<]
+ltemNilRight m = irrelevantEq $ lteNilRight m.lte
diff --git a/lib/Quox/Syntax/Var.idr b/lib/Quox/Syntax/Var.idr
index 4840350..ea872a9 100644
--- 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
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index f37371f..3175265 100644
--- 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,