Make everything relevant.

Too few proofs were relevant. Now they are.

1 files changed, 110 insertions, 0 deletions

diff --git a/src/Inky/Data/SnocList/Elem.idr b/src/Inky/Data/SnocList/Elem.idr
new file mode 100644
index 0000000..465e92c
--- /dev/null
+++ b/src/Inky/Data/SnocList/Elem.idr
@@ -0,0 +1,110 @@
+module Inky.Data.SnocList.Elem
+
+import public Data.SnocList.Elem
+
+import Data.DPair
+import Data.Nat
+import Data.Singleton
+import Inky.Decidable
+import Inky.Decidable.Maybe
+import Inky.Data.Assoc
+import Inky.Data.SnocList
+
+export
+Uninhabited (Here {sx, x} ~=~ There {sx = sy, x = z, y} i) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (There {sx = sy, x = z, y} i ~=~ Here {sx, x}) where
+  uninhabited Refl impossible
+
+export
+thereCong :
+  {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j ->
+  There {y = z} i = There {y = z} j
+thereCong Refl = Refl
+
+export
+toNatCong : {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j -> elemToNat i = elemToNat j
+toNatCong Refl = Refl
+
+export
+thereInjective :
+  {0 i : Elem x sx} -> {0 j : Elem y sx} -> There {y = z} i = There {y = z} j ->
+  i = j
+thereInjective Refl = Refl
+
+export
+toNatInjective : {i : Elem x sx} -> {j : Elem y sx} -> (0 _ : elemToNat i = elemToNat j) -> i = j
+toNatInjective {i = Here} {j = Here} prf = Refl
+toNatInjective {i = There i} {j = There j} prf with (toNatInjective {i} {j} $ injective prf)
+  toNatInjective {i = There i} {j = There .(i)} prf | Refl = Refl
+
+-- Decidable Equality -----------------------------------------------------------
+
+public export
+reflectEq : (i : Elem x sx) -> (j : Elem y sx) -> (i = j) `When` (elemToNat i == elemToNat j)
+reflectEq Here Here = Refl
+reflectEq Here (There j) = absurd
+reflectEq (There i) Here = absurd
+reflectEq (There i) (There j) = mapWhen thereCong thereInjective $ reflectEq i j
+
+public export
+decEq : (i : Elem x sx) -> (j : Elem y sx) -> Dec' (i = j)
+decEq i j = (elemToNat i == elemToNat j) `Because` reflectEq i j
+
+-- Weakening -------------------------------------------------------------------
+
+public export
+wknL : Elem x sx -> LengthOf sy -> Elem x (sx ++ sy)
+wknL pos Z = pos
+wknL pos (S len) = There (wknL pos len)
+
+public export
+wknR : Elem x sx -> Elem x (sy ++ sx)
+wknR Here = Here
+wknR (There pos) = There (wknR pos)
+
+public export
+split : LengthOf sy -> Elem x (sx ++ sy) -> Either (Elem x sx) (Elem x sy)
+split Z pos = Left pos
+split (S len) Here = Right Here
+split (S len) (There pos) = mapSnd There $ split len pos
+
+-- Lookup ----------------------------------------------------------------------
+
+export
+nameOf : {sx : SnocList a} -> Elem x sx -> Singleton x
+nameOf Here = Val x
+nameOf (There pos) = nameOf pos
+
+-- Search ----------------------------------------------------------------------
+
+export
+lookup : DecEq' a => (x : a) -> (sx : SnocList a) -> Maybe (Elem x sx)
+lookup x [<] = Nothing
+lookup x (sx :< y) =
+  case decEq x y of
+    True `Because` Refl => Just Here
+    False `Because` _ => There <$> lookup x sx
+
+public export
+decLookup : (n : String) -> (sx : SnocList (Assoc a)) -> DecWhen a (\x => Elem (n :- x) sx)
+decLookup n [<] = Nothing `Because` (\_ => absurd)
+decLookup n (sx :< (k :- x)) =
+  map (maybe x id) leftToRight rightToLeft $
+  first (decEq n k) (decLookup n sx)
+  where
+  leftToRight :
+    forall n. (m : Maybe a) ->
+    maybe (n = k) (\y => Elem (n :- y) sx) m ->
+    Elem (n :- maybe x Basics.id m) (sx :< (k :- x))
+  leftToRight Nothing Refl = Here
+  leftToRight (Just _) prf = There prf
+
+  rightToLeft :
+    forall n.
+    (Not (n = k), (y : a) -> Not (Elem (n :- y) sx)) ->
+    (y : a) -> Not (Elem (n :- y) (sx :< (k :- x)))
+  rightToLeft (neq, contra) _ Here = neq Refl
+  rightToLeft (neq, contra) y (There i) = contra y i