From c8187c0801891e5e333a8affc63bdbc204ae59c3 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 10 Oct 2022 17:30:46 +0200
Subject: [PATCH] OPE & scope stuff

---
 lib/Quox/NatExtra.idr |  44 +++++
 lib/Quox/OPE.idr      | 401 ++++++++++++++++++++++++------------------
 lib/Quox/Scope.idr    |  94 ++++++++++
 3 files changed, 370 insertions(+), 169 deletions(-)
 create mode 100644 lib/Quox/Scope.idr

diff --git a/lib/Quox/NatExtra.idr b/lib/Quox/NatExtra.idr
index 42f627e..8da43b8 100644
--- a/lib/Quox/NatExtra.idr
+++ b/lib/Quox/NatExtra.idr
@@ -55,3 +55,47 @@ 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 "divNat" 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 "modNat" modNatNZ = modNatViaIntegerNZ
+
+
+public export
+data ViewLsb : Nat -> Type where
+  Lsb0 : (n : Nat) -> ViewLsb (2 * n)
+  Lsb1 : (n : Nat) -> ViewLsb (S (2 * n))
+
+private
+viewLsb' : (m, d : Nat) -> (0 _ : m `LT` 2) -> ViewLsb (m + 2 * d)
+viewLsb' 0 d p = Lsb0 d
+viewLsb' 1 d p = Lsb1 d
+viewLsb' (S (S _)) _ (LTESucc p) = void $ absurd p
+
+export
+viewLsb : (n : Nat) -> ViewLsb n
+viewLsb n =
+  let nz = the (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)
diff --git a/lib/Quox/OPE.idr b/lib/Quox/OPE.idr
index 0f50df0..4a245b7 100644
--- a/lib/Quox/OPE.idr
+++ b/lib/Quox/OPE.idr
@@ -3,194 +3,257 @@
 module Quox.OPE
 
 import Quox.NatExtra
-
-import Data.Nat
+import public Data.DPair
+import public Data.SnocList
+import public Data.SnocList.Elem
 
 %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
+LTE_n = Nat.LTE
+%hide Nat.LTE
 
 
 public export
-dropInner' : LTE' m n -> OPE m n
-dropInner' LTERefl      = Id
-dropInner' (LTESuccR p) = Drop $ dropInner' $ force p
+Scope : Type -> Type
+Scope = SnocList
 
 public export
-dropInner : {n : Nat} -> LTE m n -> OPE m n
-dropInner = dropInner' . fromLte
+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
 
-public export
-dropInnerN : (m : Nat) -> OPE n (m + n)
-dropInnerN 0     = Id
-dropInnerN (S m) = Drop $ dropInnerN m
+-- [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
+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
+lteNilRight : xs `LTE` [<] -> xs = [<]
+lteNilRight End = Refl
 
 
 public export
-interface Tighten t where
-  tighten : Alternative f => OPE m n -> t n -> f (t m)
+data Length : Scope a -> Type where
+  Z : Length [<]
+  S : (s : Length xs) -> Length (xs :< x)
+%name Length s
+%builtin Natural Length
 
-parameters {auto _ : Tighten t} {auto _ : Alternative f}
+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
+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)
+
+
+private
+0 compExample :
+  Comp {zs = [< a, b, c, d, e]}
+    (Keep $ Drop $ Keep $ Drop $ Keep End)
+    (Keep $ Drop $ Keep End)
+    (Keep $ Drop $ Drop $ Drop $ Keep End)
+compExample = %search
+
+
+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 xs = Exists (`LTE` xs)
+
+public export
+SubMap : {xs, ys : Scope a} -> xs `LTE` zs -> ys `LTE` zs -> Type
+SubMap p q = DPair (xs `LTE` ys) (\r => Comp q r p)
+
+parameters (p : xs `LTE` ys)
   export
-  tightenInner : {n : Nat} -> m `LTE` n -> t n -> f (t m)
-  tightenInner = tighten . dropInner
+  subId : SubMap p p
+  subId = (id ** compIdRight p)
 
   export
-  tightenN : (m : Nat) -> t (m + n) -> f (t n)
-  tightenN m = tighten $ dropInnerN m
+  subZero : SubMap OPE.zero p
+  subZero = (zero ** compZero p)
 
-  export
-  tighten1 : t (S n) -> f (t n)
-  tighten1 = tightenN 1
+
+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
 
 
 
--- [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 LTEMaskView : xs `LTE` ys -> Nat -> Type where
+  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)
 
--- 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
+record LTEMask {a : Type} (xs, ys : Scope a) where
+  constructor LTEM
+  mask : Nat
+  0 lte : xs `LTE` ys
+  0 view0 : LTEMaskView lte mask
 
-
--- 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, _}
+export
+view : (sx : Length xs) => (sy : Length ys) =>
+       (m : LTEMask xs ys) -> LTEMaskView m.lte m.mask
diff --git a/lib/Quox/Scope.idr b/lib/Quox/Scope.idr
new file mode 100644
index 0000000..5ff1e11
--- /dev/null
+++ 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