5 files changed, 74 insertions, 14 deletions
diff --git a/src/Inky/Data/List.idr b/src/Inky/Data/List.idr
new file mode 100644
index 0000000..24cb9c0
--- /dev/null
+++ b/src/Inky/Data/List.idr
@@ -0,0 +1,13 @@
+module Inky.Data.List
+
+public export
+data LengthOf : List a -> Type where
+  Z : LengthOf []
+  S : LengthOf xs -> LengthOf (x :: xs)
+
+%name LengthOf len
+
+public export
+lengthOf : (xs : List a) -> LengthOf xs
+lengthOf [] = Z
+lengthOf (x :: xs) = S (lengthOf xs)
diff --git a/src/Inky/Data/Row.idr b/src/Inky/Data/Row.idr
index ba0c5f6..05e1fd0 100644
--- a/src/Inky/Data/Row.idr
+++ b/src/Inky/Data/Row.idr
@@ -28,20 +28,6 @@ public export
 (.names) : Row a -> SnocList String
 row.names = row.context.names
 
--- Interfaces ------------------------------------------------------------------
-
-public export
-Functor Row where
-  map f row = MkRow (map (map f) row.context) (rewrite mapNames f row.context in row.fresh)
-
-public export
-Foldable Row where
-  foldr f x row = foldr (\x, y => f x.value y) x row.context
-  foldl f x row = foldl (\x, y => f x y.value) x row.context
-  null row = null row.context
-  foldlM f x row = foldlM (\x, y => f x y.value) x row.context
-  foldMap f row = foldMap (f . value) row.context
-
 -- Equality --------------------------------------------------------------------
 
 export
@@ -81,10 +67,47 @@ public export
   Row a
 row :< x = MkRow (row.context :< x) (row.fresh :< fresh)
 
+export
+snocCong :
+  {0 x, y : Assoc a} ->
+  row1 = row2 -> x = y ->
+  {0 fresh1 : x.name `FreshIn` row1.names} ->
+  {0 fresh2 : y.name `FreshIn` row2.names} ->
+  (:<) row1 x @{fresh1} = (:<) row2 y @{fresh2}
+snocCong eq1 eq2 = rowCong $ cong2 (\x, y => x.context :< y) eq1 eq2
+
 public export
 fromAll : (row : Row a) -> All (const b) row.names -> Row b
 fromAll row sx = MkRow (fromAll row.context sx) (rewrite fromAllNames row.context sx in row.fresh)
 
+-- Interfaces ------------------------------------------------------------------
+
+public export
+mapRow : (a -> b) -> (ctx : Context a) -> (0 fresh : AllFresh ctx.names) -> Row b
+export
+mapRowNames :
+  (0 f : a -> b) -> (ctx : Context a) -> (0 fresh : AllFresh ctx.names) ->
+  (mapRow f ctx fresh).names = ctx.names
+
+mapRow f [<] [<] = [<]
+mapRow f (ctx :< (l :- x)) (prfs :< prf) =
+  (:<) (mapRow f ctx prfs) (l :- f x) @{rewrite mapRowNames f ctx prfs in prf}
+
+mapRowNames f [<] [<] = Refl
+mapRowNames f (ctx :< (l :- x)) (prfs :< prf) = cong (:< l) $ mapRowNames f ctx prfs
+
+public export
+Functor Row where
+  map f row = mapRow f row.context row.fresh
+
+public export
+Foldable Row where
+  foldr f x row = foldr (\x, y => f x.value y) x row.context
+  foldl f x row = foldl (\x, y => f x y.value) x row.context
+  null row = null row.context
+  foldlM f x row = foldlM (\x, y => f x y.value) x row.context
+  foldMap f row = foldMap (f . value) row.context
+
 -- Operations ------------------------------------------------------------------
 
 export
diff --git a/src/Inky/Data/SnocList/Elem.idr b/src/Inky/Data/SnocList/Elem.idr
index 465e92c..c1e69f6 100644
--- a/src/Inky/Data/SnocList/Elem.idr
+++ b/src/Inky/Data/SnocList/Elem.idr
@@ -8,6 +8,7 @@ import Data.Singleton
 import Inky.Decidable
 import Inky.Decidable.Maybe
 import Inky.Data.Assoc
+import Inky.Data.List
 import Inky.Data.SnocList
 
 export
@@ -71,6 +72,11 @@ split Z pos = Left pos
 split (S len) Here = Right Here
 split (S len) (There pos) = mapSnd There $ split len pos
 
+public export
+wknL' : Elem x sx -> LengthOf xs -> Elem x (sx <>< xs)
+wknL' i Z = i
+wknL' i (S len) = wknL' (There i) len
+
 -- Lookup ----------------------------------------------------------------------
 
 export
diff --git a/src/Inky/Data/SnocList/Quantifiers.idr b/src/Inky/Data/SnocList/Quantifiers.idr
index 73c6551..ac6287b 100644
--- a/src/Inky/Data/SnocList/Quantifiers.idr
+++ b/src/Inky/Data/SnocList/Quantifiers.idr
@@ -4,6 +4,8 @@ import public Data.SnocList.Quantifiers
 
 import Data.List.Quantifiers
 import Inky.Data.Irrelevant
+import Inky.Data.SnocList
+import Inky.Data.SnocList.Elem
 import Inky.Decidable
 
 public export
@@ -41,6 +43,11 @@ relevant [<] _ = [<]
 relevant (sx :< x) prfs = relevant sx (tail prfs) :< Forget (head prfs)
 
 public export
+tabulate : LengthOf sx -> (forall x. Elem x sx -> p x) -> All p sx
+tabulate Z f = [<]
+tabulate (S len) f = tabulate len (f . There) :< f Here
+
+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
index f766069..60666d2 100644
--- a/src/Inky/Data/SnocList/Thinning.idr
+++ b/src/Inky/Data/SnocList/Thinning.idr
@@ -2,6 +2,7 @@ module Inky.Data.SnocList.Thinning
 
 import Data.DPair
 import Data.Nat
+import Inky.Data.List
 import Inky.Data.SnocList
 import Inky.Data.SnocList.Var
 import Inky.Data.SnocList.Quantifiers
@@ -97,6 +98,16 @@ prf.index ((%%) n {pos}) = irrelevantEq $ toVarCong $ toNatInjective $ prf.index
 -- Useful for Parsers ----------------------------------------------------------
 
 public export
+(<><) : ctx1 `Thins` ctx2 -> LengthOf bound -> ctx1 <>< bound `Thins` ctx2 <>< bound
+f <>< Z = f
+f <>< S len = Keep f <>< len
+
+public export
+dropFish : ctx1 `Thins` ctx2 -> LengthOf bound -> ctx1 `Thins` ctx2 <>< bound
+dropFish f Z = f
+dropFish f (S len) = dropFish (Drop f) len
+
+public export
 dropPos : (pos : Elem x ctx) -> dropElem ctx pos `Thins` ctx
 dropPos Here = Drop Id
 dropPos (There pos) = Keep (dropPos pos)