4 files changed, 463 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
diff --git a/src/Inky/Data/SnocList/Quantifiers.idr b/src/Inky/Data/SnocList/Quantifiers.idr
new file mode 100644
index 0000000..73c6551
--- /dev/null
+++ b/src/Inky/Data/SnocList/Quantifiers.idr
@@ -0,0 +1,46 @@
+module Inky.Data.SnocList.Quantifiers
+
+import public Data.SnocList.Quantifiers
+
+import Data.List.Quantifiers
+import Inky.Data.Irrelevant
+import Inky.Decidable
+
+public export
+(<><) : All p xs -> All p sx -> All p (xs <>< sx)
+sxp <>< [] = sxp
+sxp <>< (px :: pxs) = (sxp :< px) <>< pxs
+
+public export
+head : All p (sx :< x) -> p x
+head (prfs :< px) = px
+
+public export
+tail : All p (sx :< x) -> All p sx
+tail (prfs :< px) = prfs
+
+public export
+HSnocList : SnocList Type -> Type
+HSnocList = All id
+
+public export
+all : ((x : a) -> Dec' (p x)) -> (sx : SnocList a) -> LazyEither (All p sx) (Any (Not . p) sx)
+all f [<] = True `Because` [<]
+all f (sx :< x) =
+  map (\prfs => snd prfs :< fst prfs) (either Here There) $
+  both (f x) (all f sx)
+
+public export
+irrelevant : {0 sx : SnocList a} -> All (Irrelevant . p) sx -> Irrelevant (All p sx)
+irrelevant [<] = Forget [<]
+irrelevant (prfs :< px) = [| irrelevant prfs :< px |]
+
+public export
+relevant : (sx : SnocList a) -> (0 prfs : All p sx) -> All (Irrelevant . p) sx
+relevant [<] _ = [<]
+relevant (sx :< x) prfs = relevant sx (tail prfs) :< Forget (head prfs)
+
+public export
+data Pairwise : (a -> a -> Type) -> SnocList a -> Type where
+  Lin : Pairwise r [<]
+  (:<) : Pairwise r sx -> All (flip r x) sx -> Pairwise r (sx :< x)
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
diff --git a/src/Inky/Data/SnocList/Var.idr b/src/Inky/Data/SnocList/Var.idr
new file mode 100644
index 0000000..cc7c088
--- /dev/null
+++ b/src/Inky/Data/SnocList/Var.idr
@@ -0,0 +1,90 @@
+module Inky.Data.SnocList.Var
+
+import public Inky.Data.SnocList.Elem
+
+import Data.Singleton
+import Inky.Data.SnocList
+import Inky.Decidable
+
+export
+prefix 2 %%
+
+public export
+record Var (sx : SnocList a) where
+  constructor (%%)
+  0 name : a
+  {auto pos : Elem name sx}
+
+%name Var i, j, k
+
+public export
+toVar : Elem x sx -> Var sx
+toVar pos = (%%) x {pos}
+
+public export
+ThereVar : Var sx -> Var (sx :< x)
+ThereVar i = toVar (There i.pos)
+
+export
+Show (Var sx) where
+  show i = show (elemToNat i.pos)
+
+-- Basic Properties ---------------------------------------------------------
+
+export
+toVarCong : {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j -> toVar i = toVar j
+toVarCong Refl = Refl
+
+export
+posCong : {0 i, j : Var sx} -> i = j -> i.pos ~=~ j.pos
+posCong Refl = Refl
+
+export
+toVarInjective : {i : Elem x sx} -> {j : Elem y sx} -> (0 _ : toVar i = toVar j) -> i = j
+toVarInjective prf = toNatInjective $ toNatCong $ posCong prf
+
+export
+posInjective : {i : Var sx} -> {j : Var sx} -> (0 _ : i.pos ~=~ j.pos) -> i = j
+posInjective {i = %% x} {j = %% y} prf = irrelevantEq $ toVarCong prf
+
+-- Decidable Equality ----------------------------------------------------------
+
+public export
+DecEq' (Var {a} sx) where
+  does i j = (decEq i.pos j.pos).does
+  reason i j =
+    mapWhen (\prf => irrelevantEq $ posInjective prf) posCong $
+    (decEq i.pos j.pos).reason
+
+-- Weakening -------------------------------------------------------------------
+
+public export
+wknL : (len : LengthOf sy) => Var sx -> Var (sx ++ sy)
+wknL i = toVar $ wknL i.pos len
+
+public export
+wknR : Var sx -> Var (sy ++ sx)
+wknR i = toVar $ wknR i.pos
+
+public export
+split : {auto len : LengthOf sy} -> Var (sx ++ sy) -> Either (Var sx) (Var sy)
+split i = bimap toVar toVar $ split len i.pos
+
+public export
+lift1 :
+  (Var sx -> Var sy) ->
+  Var (sx :< x) -> Var (sy :< y)
+lift1 f ((%%) x {pos = Here}) = %% y
+lift1 f ((%%) name {pos = There i}) = ThereVar (f $ %% name)
+
+-- Names -----------------------------------------------------------------------
+
+export
+nameOf : {sx : SnocList a} -> (i : Var sx) -> Singleton i.name
+nameOf i = nameOf i.pos
+
+-- Search ----------------------------------------------------------------------
+
+export
+lookup : DecEq' a => (x : a) -> (sx : SnocList a) -> Maybe (Var sx)
+lookup x sx = toVar <$> lookup x sx