From 4b643998910fbfaa827026b9e22e3eea030c4fe6 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 5 Nov 2022 22:08:57 +0100
Subject: [PATCH] bitmask representation of lte

---
 lib/Quox/NatExtra.idr |  62 ++++++++++++---
 lib/Quox/OPE.idr      | 176 ++++++++++++++++++++++++++++++++++--------
 2 files changed, 194 insertions(+), 44 deletions(-)

diff --git a/lib/Quox/NatExtra.idr b/lib/Quox/NatExtra.idr
index 8da43b8..343fcf3 100644
--- 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
 
@@ -68,7 +70,7 @@ divNatViaInteger m n = i2n $ n2i m `div` n2i n
 private %inline
 divNatViaIntegerNZ : (m, n : Nat) -> (0 _ : NonZero n) -> Nat
 divNatViaIntegerNZ m n _ = assert_total divNatViaInteger m n
-%transform "divNat" divNatNZ = divNatViaIntegerNZ
+%transform "divNatNZ" divNatNZ = divNatViaIntegerNZ
 
 private partial %inline
 modNatViaInteger : (m, n : Nat) -> Nat
@@ -78,24 +80,62 @@ modNatViaInteger m n = i2n $ n2i m `mod` n2i n
 private %inline
 modNatViaIntegerNZ : (m, n : Nat) -> (0 _ : NonZero n) -> Nat
 modNatViaIntegerNZ m n _ = assert_total modNatViaInteger m n
-%transform "modNat" modNatNZ = modNatViaIntegerNZ
+%transform "modNatNZ" modNatNZ = modNatViaIntegerNZ
 
 
 public export
-data ViewLsb : Nat -> Type where
-  Lsb0 : (n : Nat) -> ViewLsb (2 * n)
-  Lsb1 : (n : Nat) -> ViewLsb (S (2 * n))
+data Parity = Even | Odd
+
+public export
+data ViewLsb : Nat -> Parity -> Type where
+  Lsb0 : (n : Nat) -> ViewLsb    (2 * n)  Even
+  Lsb1 : (n : Nat) -> ViewLsb (S (2 * n)) Odd
+%name ViewLsb p, q
+
+export
+fromLsb0 : ViewLsb n Even -> Subset Nat (\n' => n = 2 * n')
+fromLsb0 (Lsb0 n') = Element n' Refl
+
+export
+fromLsb1 : ViewLsb n Odd -> Subset Nat (\n' => n = S (2 * n'))
+fromLsb1 (Lsb1 n') = Element n' Refl
+
 
 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' : (m, d : Nat) -> (0 _ : m `LT` 2) -> Exists $ ViewLsb (m + 2 * d)
+viewLsb' 0 d p = Evidence Even (Lsb0 d)
+viewLsb' 1 d p = Evidence Odd  (Lsb1 d)
 viewLsb' (S (S _)) _ (LTESucc p) = void $ absurd p
 
 export
-viewLsb : (n : Nat) -> ViewLsb n
+viewLsb : (n : Nat) -> Exists $ ViewLsb n
 viewLsb n =
-  let nz = the (NonZero 2) %search in
+  let 0 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)
+
+
+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
+
+export
+0 lsbMutex : ViewLsb n Even -> ViewLsb n Odd -> Void
+lsbMutex p q = lsbMutex' (fromLsb0 p).snd (fromLsb1 q).snd
+
+export
+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)
diff --git a/lib/Quox/OPE.idr b/lib/Quox/OPE.idr
index 4a245b7..e09f9af 100644
--- a/lib/Quox/OPE.idr
+++ b/lib/Quox/OPE.idr
@@ -42,15 +42,23 @@ Uninhabited (xs :< x `LTE` xs) where
 
 
 export
-lteLen : xs `LTE` ys -> length xs `LTE_n` length ys
+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
-lteNilRight : xs `LTE` [<] -> xs = [<]
+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
@@ -59,6 +67,18 @@ data Length : Scope a -> Type where
 %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
@@ -102,6 +122,119 @@ 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
@@ -165,15 +298,6 @@ 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
@@ -191,20 +315,23 @@ Scoped a = Scope a -> Type
 
 public export
 Subscope : Scope a -> Type
-Subscope xs = Exists (`LTE` xs)
+Subscope ys = Exists (`LTE` ys)
 
 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)
+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 = (id ** compIdRight p)
+  subId = SM id (compIdRight p)
 
   export
   subZero : SubMap OPE.zero p
-  subZero = (zero ** compZero p)
+  subZero = SM zero (compZero p)
 
 
 public export
@@ -240,20 +367,3 @@ public export
 Partition : xs `LTE` zs -> ys `LTE` zs -> Type
 Partition = Cover_ False
 
-
-
-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)
-
-record LTEMask {a : Type} (xs, ys : Scope a) where
-  constructor LTEM
-  mask : Nat
-  0 lte : xs `LTE` ys
-  0 view0 : LTEMaskView lte mask
-
-export
-view : (sx : Length xs) => (sy : Length ys) =>
-       (m : LTEMask xs ys) -> LTEMaskView m.lte m.mask