1 files changed, 217 insertions, 0 deletions
diff --git a/src/Inky/Data/SnocList/Thinning.idr b/src/Inky/Data/SnocList/Thinning.idr
new file mode 100644
index 0000000..f766069
--- /dev/null
+++ b/src/Inky/Data/SnocList/Thinning.idr
@@ -0,0 +1,217 @@
+module Inky.Data.SnocList.Thinning
+
+import Data.DPair
+import Data.Nat
+import Inky.Data.SnocList
+import Inky.Data.SnocList.Var
+import Inky.Data.SnocList.Quantifiers
+import Inky.Decidable.Maybe
+
+--------------------------------------------------------------------------------
+-- Thinnings -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+public export
+data Thins : SnocList a -> SnocList a -> Type where
+  Id : sx `Thins` sx
+  Drop : sx `Thins` sy -> sx `Thins` sy :< x
+  Keep : sx `Thins` sy -> sx :< x `Thins` sy :< x
+
+%name Thins f, g, h
+
+-- Basics
+
+public export
+indexPos : (f : sx `Thins` sy) -> (pos : Elem x sx) -> Elem x sy
+indexPos Id pos = pos
+indexPos (Drop f) pos = There (indexPos f pos)
+indexPos (Keep f) Here = Here
+indexPos (Keep f) (There pos) = There (indexPos f pos)
+
+public export
+index : (f : sx `Thins` sy) -> Var sx -> Var sy
+index f i = toVar (indexPos f i.pos)
+
+public export
+(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz
+Id . g = g
+Drop f . g = Drop (f . g)
+Keep f . Id = Keep f
+Keep f . Drop g = Drop (f . g)
+Keep f . Keep g = Keep (f . g)
+
+-- Basic properties
+
+export
+indexPosInjective :
+  (f : sx `Thins` sy) -> {i : Elem x sx} -> {j : Elem y sx} ->
+  (0 _ : elemToNat (indexPos f i) = elemToNat (indexPos f j)) -> i = j
+indexPosInjective Id prf = toNatInjective prf
+indexPosInjective (Drop f) prf = indexPosInjective f (injective prf)
+indexPosInjective (Keep f) {i = Here} {j = Here} prf = Refl
+indexPosInjective (Keep f) {i = There i} {j = There j} prf =
+  thereCong (indexPosInjective f $ injective prf)
+
+export
+indexPosComp :
+  (f : sy `Thins` sz) -> (g : sx `Thins` sy) -> (pos : Elem x sx) ->
+  indexPos (f . g) pos = indexPos f (indexPos g pos)
+indexPosComp Id g pos = Refl
+indexPosComp (Drop f) g pos = cong There (indexPosComp f g pos)
+indexPosComp (Keep f) Id pos = Refl
+indexPosComp (Keep f) (Drop g) pos = cong There (indexPosComp f g pos)
+indexPosComp (Keep f) (Keep g) Here = Refl
+indexPosComp (Keep f) (Keep g) (There pos) = cong There (indexPosComp f g pos)
+
+-- Congruence ------------------------------------------------------------------
+
+export
+infix 6 ~~~
+
+public export
+data (~~~) : sx `Thins` sy -> sx `Thins` sz -> Type where
+  IdId : Id ~~~ Id
+  IdKeep : Id ~~~ f -> Id ~~~ Keep f
+  KeepId : f ~~~ Id -> Keep f ~~~ Id
+  DropDrop : f ~~~ g -> Drop f ~~~ Drop g
+  KeepKeep : f ~~~ g -> Keep f ~~~ Keep g
+
+%name Thinning.(~~~) prf
+
+export
+(.indexPos) : f ~~~ g -> (pos : Elem x sx) -> elemToNat (indexPos f pos) = elemToNat (indexPos g pos)
+(IdId).indexPos pos = Refl
+(IdKeep prf).indexPos Here = Refl
+(IdKeep prf).indexPos (There pos) = cong S $ prf.indexPos pos
+(KeepId prf).indexPos Here = Refl
+(KeepId prf).indexPos (There pos) = cong S $ prf.indexPos pos
+(DropDrop prf).indexPos pos = cong S $ prf.indexPos pos
+(KeepKeep prf).indexPos Here = Refl
+(KeepKeep prf).indexPos (There pos) = cong S $ prf.indexPos pos
+
+export
+(.index) :
+  {0 f, g : sx `Thins` sy} -> f ~~~ g -> (i : Var sx) -> index f i = index g i
+prf.index ((%%) n {pos}) = irrelevantEq $ toVarCong $ toNatInjective $ prf.indexPos pos
+
+-- Useful for Parsers ----------------------------------------------------------
+
+public export
+dropPos : (pos : Elem x ctx) -> dropElem ctx pos `Thins` ctx
+dropPos Here = Drop Id
+dropPos (There pos) = Keep (dropPos pos)
+
+public export
+dropAll : LengthOf sy -> sx `Thins` sx ++ sy
+dropAll Z = Id
+dropAll (S len) = Drop (dropAll len)
+
+public export
+keepAll : LengthOf sz -> sx `Thins` sy -> sx ++ sz `Thins` sy ++ sz
+keepAll Z f = f
+keepAll (S len) f = Keep (keepAll len f)
+
+public export
+append :
+  sx `Thins` sz -> sy `Thins` sw ->
+  {auto len : LengthOf sw} ->
+  sx ++ sy `Thins` sz ++ sw
+append f Id = keepAll len f
+append f (Drop g) {len = S len} = Drop (append f g)
+append f (Keep g) {len = S len} = Keep (append f g)
+
+public export
+assoc : LengthOf sz -> sx ++ (sy ++ sz) `Thins` (sx ++ sy) ++ sz
+assoc Z = Id
+assoc (S len) = Keep (assoc len)
+
+public export
+growLengthOf : sx `Thins` sy -> LengthOf sx -> LengthOf sy
+growLengthOf Id len = len
+growLengthOf (Drop f) len = S (growLengthOf f len)
+growLengthOf (Keep f) (S len) = S (growLengthOf f len)
+
+public export
+thinLengthOf : sx `Thins` sy -> LengthOf sy -> LengthOf sx
+thinLengthOf Id len = len
+thinLengthOf (Drop f) (S len) = thinLengthOf f len
+thinLengthOf (Keep f) (S len) = S (thinLengthOf f len)
+
+public export
+thinAll : sx `Thins` sy -> All p sy -> All p sx
+thinAll Id env = env
+thinAll (Drop f) (env :< px) = thinAll f env
+thinAll (Keep f) (env :< px) = thinAll f env :< px
+
+public export
+splitL :
+  {0 sx, sy, sz : SnocList a} ->
+  LengthOf sz ->
+  sx `Thins` sy ++ sz ->
+  Exists (\sxA => Exists (\sxB => (sx = sxA ++ sxB, sxA `Thins` sy, sxB `Thins` sz)))
+splitL Z f = Evidence sx (Evidence [<] (Refl, f, Id))
+splitL (S len) Id = Evidence sy (Evidence sz (Refl, Id, Id))
+splitL (S len) (Drop f) =
+  let Evidence sxA (Evidence sxB (Refl, g, h)) = splitL len f in
+  Evidence sxA (Evidence sxB (Refl, g, Drop h))
+splitL (S len) (Keep f) =
+  let Evidence sxA (Evidence sxB (Refl, g, h)) = splitL len f in
+  Evidence sxA (Evidence (sxB :< _) (Refl, g, Keep h))
+
+public export
+splitR :
+  {0 sx, sy, sz : SnocList a} ->
+  LengthOf sy ->
+  sx ++ sy `Thins` sz ->
+  Exists (\sxA => Exists (\sxB => (sz = sxA ++ sxB, sx `Thins` sxA, sy `Thins` sxB)))
+splitR Z f = Evidence sz (Evidence [<] (Refl, f, Id))
+splitR (S len) Id = Evidence sx (Evidence sy (Refl, Id, Id))
+splitR (S len) (Drop f) =
+  let Evidence sxA (Evidence sxB (Refl, g, h)) = splitR (S len) f in
+  Evidence sxA (Evidence (sxB :< _) (Refl, g, Drop h))
+splitR (S len) (Keep f) =
+  let Evidence sxA (Evidence sxB (Refl, g, h)) = splitR len f in
+  Evidence sxA (Evidence (sxB :< _) (Refl, g, Keep h))
+
+-- Strengthening ---------------------------------------------------------------
+
+public export
+data Skips : sx `Thins` sy -> Elem y sy -> Type where
+  Here : Drop f `Skips` Here
+  Also : f `Skips` i -> Drop f `Skips` There i
+  There : f `Skips` i -> Keep f `Skips` There i
+
+%name Skips skips
+
+public export
+strengthen :
+  (f : sx `Thins` sy) -> (i : Elem y sy) ->
+  Proof (Elem y sx) (\j => i = indexPos f j) (f `Skips` i)
+strengthen Id i = Just i `Because` Refl
+strengthen (Drop f) Here = Nothing `Because` Here
+strengthen (Drop f) (There i) =
+  map id (\_, prf => cong There prf) Also $
+  strengthen f i
+strengthen (Keep f) Here = Just Here `Because` Refl
+strengthen (Keep f) (There i) =
+  map There (\_, prf => cong There prf) There $
+  strengthen f i
+
+export
+skipsDropPos : (i : Elem x sx) -> dropPos i `Skips` j -> i ~=~ j
+skipsDropPos Here Here = Refl
+skipsDropPos (There i) (There skips) = thereCong (skipsDropPos i skips)
+
+------------------------ -------------------------------------------------------
+-- Renaming Coalgebras ---------------------------------------------------------
+--------------------------------------------------------------------------------
+
+public export
+interface Rename (0 a : Type) (0 t : SnocList a -> Type) where
+  rename :
+    {0 sx, sy : SnocList a} -> sx `Thins` sy ->
+    t sx -> t sy
+  0 renameCong :
+    {0 sx, sy : SnocList a} -> {0 f, g : sx `Thins` sy} -> f ~~~ g ->
+    (x : t sx) -> rename f x = rename g x
+  0 renameId : {0 sx : SnocList a} -> (x : t sx) -> rename Id x = x