Make everything relevant.

Too few proofs were relevant. Now they are.

12 files changed, 928 insertions, 0 deletions

diff --git a/src/Inky/Data/Assoc.idr b/src/Inky/Data/Assoc.idr
new file mode 100644
index 0000000..a009515
--- /dev/null
+++ b/src/Inky/Data/Assoc.idr
@@ -0,0 +1,26 @@
+module Inky.Data.Assoc
+
+export
+infix 2 :-
+
+public export
+record Assoc (a : Type) where
+  constructor (:-)
+  name : String
+  value : a
+
+public export
+Functor Assoc where
+  map f x = x.name :- f x.value
+
+namespace Irrelevant
+  public export
+  record Assoc0 (0 p : a -> Type) (x : Assoc a) where
+    constructor (:-)
+    0 name : String
+    {auto 0 prf : x.name = name}
+    value : p x.value
+
+  public export
+  map : (forall x. p x -> q x) -> forall x. Assoc0 p x -> Assoc0 q x
+  map f (n :- px) = n :- f px
diff --git a/src/Inky/Data/Context.idr b/src/Inky/Data/Context.idr
new file mode 100644
index 0000000..0d3df99
--- /dev/null
+++ b/src/Inky/Data/Context.idr
@@ -0,0 +1,36 @@
+module Inky.Data.Context
+
+import public Inky.Data.Assoc
+import public Inky.Data.SnocList
+
+import Inky.Data.SnocList.Quantifiers
+
+-- Contexts --------------------------------------------------------------------
+
+public export
+Context : Type -> Type
+Context a = SnocList (Assoc a)
+
+public export
+(.names) : Context a -> SnocList String
+[<].names = [<]
+(ctx :< nx).names = ctx.names :< nx.name
+
+export
+mapNames : (0 f : a -> b) -> (ctx : Context a) -> (map (map f) ctx).names = ctx.names
+mapNames f [<] = Refl
+mapNames f (ctx :< nx) = cong (:< nx.name) $ mapNames f ctx
+
+-- Construction ----------------------------------------------------------------
+
+public export
+fromAll : (ctx : Context a) -> All (const b) ctx.names -> Context b
+fromAll [<] [<] = [<]
+fromAll (ctx :< (n :- _)) (sx :< x) = fromAll ctx sx :< (n :- x)
+
+export
+fromAllNames :
+  (ctx : Context a) -> (sx : All (const b) ctx.names) ->
+  (fromAll ctx sx).names = ctx.names
+fromAllNames [<] [<] = Refl
+fromAllNames (ctx :< (n :- _)) (sx :< x) = cong (:< n) $ fromAllNames ctx sx
diff --git a/src/Inky/Data/Context/Var.idr b/src/Inky/Data/Context/Var.idr
new file mode 100644
index 0000000..4741580
--- /dev/null
+++ b/src/Inky/Data/Context/Var.idr
@@ -0,0 +1,117 @@
+module Inky.Data.Context.Var
+
+import Data.DPair
+import Data.Singleton
+import Inky.Data.Context
+import Inky.Data.SnocList.Elem
+import Inky.Decidable
+import Inky.Decidable.Maybe
+
+export
+prefix 2 %%, %%%
+
+public export
+record Var (ctx : Context a) (x : a) where
+  constructor (%%)
+  0 name : String
+  {auto pos : Elem (name :- x) ctx}
+
+%name Var i, j, k
+
+public export
+toVar : Elem (n :- x) ctx -> Var ctx x
+toVar pos = (%%) n {pos}
+
+public export
+ThereVar : Var ctx x -> Var (ctx :< ny) x
+ThereVar i = toVar (There i.pos)
+
+export
+Show (Var ctx x) where
+  show i = show (elemToNat i.pos)
+
+-- Basic Properties ---------------------------------------------------------
+
+export
+toVarCong :
+  {0 n, k : String} -> {0 x, y : a} ->
+  {0 i : Elem (n :- x) ctx} -> {0 j : Elem (k :- y) ctx} ->
+  i ~=~ j -> toVar i ~=~ toVar j
+toVarCong Refl = Refl
+
+export
+posCong : {0 i : Var ctx x} -> {0 j : Var ctx y} -> i = j -> i.pos ~=~ j.pos
+posCong Refl = Refl
+
+export
+toVarInjective :
+  {0 n, k : String} -> {0 x, y : a} ->
+  {i : Elem (n :- x) ctx} -> {j : Elem (k :- y) ctx} ->
+  (0 _ : toVar i ~=~ toVar j) -> i ~=~ j
+toVarInjective prf = toNatInjective $ toNatCong $ posCong prf
+
+export
+posInjective : {i : Var ctx x} -> {j : Var ctx y} -> (0 _ : i.pos ~=~ j.pos) -> i ~=~ j
+posInjective {i = %% x} {j = %% y} prf = irrelevantEq $ toVarCong prf
+
+-- Decidable Equality ----------------------------------------------------------
+
+public export
+decEq : (i : Var ctx x) -> (j : Var ctx y) -> Dec' (i ~=~ j)
+decEq i j =
+  mapDec (\prf => irrelevantEq $ posInjective prf) posCong $
+  decEq i.pos j.pos
+
+-- Weakening -------------------------------------------------------------------
+
+public export
+wknL : (len : LengthOf ctx2) => Var ctx1 x -> Var (ctx1 ++ ctx2) x
+wknL i = toVar $ wknL i.pos len
+
+public export
+wknR : Var ctx1 x -> Var (ctx2 ++ ctx1) x
+wknR i = toVar $ wknR i.pos
+
+public export
+split : {auto len : LengthOf ctx2} -> Var (ctx1 ++ ctx2) x -> Either (Var ctx1 x) (Var ctx2 x)
+split i = bimap toVar toVar $ split len i.pos
+
+public export
+lift :
+  {auto len : LengthOf ctx3} ->
+  (forall x. Var ctx1 x -> Var ctx2 x) ->
+  Var (ctx1 ++ ctx3) x -> Var (ctx2 ++ ctx3) x
+lift f = either (wknL {len} . f) wknR . split {len}
+
+-- Names -----------------------------------------------------------------------
+
+export
+nameOf : {ctx : Context a} -> (i : Var ctx x) -> Singleton i.name
+nameOf i = [| (nameOf i.pos).name |]
+
+-- Search ----------------------------------------------------------------------
+
+export
+lookup : (n : String) -> (ctx : Context a) -> Maybe (x ** Var ctx x)
+lookup n ctx =
+  case decLookup n ctx of
+    Just x `Because` pos => Just (x ** toVar pos)
+    Nothing `Because` _ => Nothing
+
+namespace Search
+  public export
+  data VarPos : String -> a -> (ctx : Context a) -> Type where
+    [search ctx]
+    Here : VarPos n x (ctx :< (n :- x))
+    There : VarPos n x ctx -> VarPos n x (ctx :< ky)
+
+  %name VarPos pos
+
+  public export
+  toElem : VarPos n x ctx -> Elem (n :- x) ctx
+  toElem Here = Here
+  toElem (There pos) = There (toElem pos)
+
+  public export
+  (%%%) : (0 n : String) -> {auto pos : VarPos n x ctx} -> Var ctx x
+  (%%%) n {pos} = toVar $ toElem pos
diff --git a/src/Inky/Data/Fun.idr b/src/Inky/Data/Fun.idr
new file mode 100644
index 0000000..d9acb7d
--- /dev/null
+++ b/src/Inky/Data/Fun.idr
@@ -0,0 +1,55 @@
+module Inky.Data.Fun
+
+import public Inky.Data.SnocList.Quantifiers
+import Inky.Data.SnocList
+
+public export
+Fun : SnocList Type -> Type -> Type
+Fun [<] b = b
+Fun (as :< a) b = Fun as (a -> b)
+
+public export
+chain : (len : LengthOf as) -> (b -> c) -> Fun as b -> Fun as c
+chain Z f x = f x
+chain (S len) f g = chain len (f .) g
+
+public export
+DFun : (as : SnocList Type) -> Fun as Type -> Type
+DFun [<] p = p
+DFun (as :< a) p = DFun as (chain (lengthOf as) (\f => (x : a) -> f x) p)
+
+public export
+DIFun : (as : SnocList Type) -> Fun as Type -> Type
+DIFun [<] p = p
+DIFun (as :< a) p = DIFun as (chain (lengthOf as) (\f => {x : a} -> f x) p)
+
+public export
+curry : (len : LengthOf as) -> (HSnocList as -> b) -> Fun as b
+curry Z f = f [<]
+curry (S len) f = curry len (f .: (:<))
+
+public export
+uncurry : Fun as b -> HSnocList as -> b
+uncurry f [<] = f
+uncurry f (sx :< x) = uncurry f sx x
+
+export
+uncurryChain :
+  (0 g : b -> c) -> (0 f : Fun as b) -> (xs : HSnocList as) ->
+  uncurry (chain (lengthOf as) g f) xs = g (uncurry f xs)
+uncurryChain g f [<] = Refl
+uncurryChain g f (sx :< x) = cong (\f => f x) (uncurryChain (g .) f sx)
+
+export
+dcurry : (len : LengthOf as) -> ((xs : HSnocList as) -> uncurry p xs) -> DFun as p
+dcurry Z f = f [<]
+dcurry (S len) f =
+  dcurry len (\sx =>
+    replace {p = id} (sym $ uncurryChain (\f => (x : _) -> f x) p sx)
+      (\x => f (sx :< x)))
+
+export
+duncurry : DFun as p -> (sx : HSnocList as) -> uncurry p sx
+duncurry f [<] = f
+duncurry f (sx :< x) =
+  replace {p = id} (uncurryChain (\f => (x : _) -> f x) p sx) (duncurry f sx) x
diff --git a/src/Inky/Data/Irrelevant.idr b/src/Inky/Data/Irrelevant.idr
new file mode 100644
index 0000000..ca72470
--- /dev/null
+++ b/src/Inky/Data/Irrelevant.idr
@@ -0,0 +1,19 @@
+module Inky.Data.Irrelevant
+
+public export
+record Irrelevant (a : Type) where
+  constructor Forget
+  0 value : a
+
+public export
+Functor Irrelevant where
+  map f x = Forget (f x.value)
+
+public export
+Applicative Irrelevant where
+  pure x = Forget x
+  f <*> x = Forget (f.value x.value)
+
+public export
+Monad Irrelevant where
+  join x = Forget (x.value.value)
diff --git a/src/Inky/Data/Row.idr b/src/Inky/Data/Row.idr
new file mode 100644
index 0000000..ba0c5f6
--- /dev/null
+++ b/src/Inky/Data/Row.idr
@@ -0,0 +1,151 @@
+module Inky.Data.Row
+
+import public Data.So
+import public Inky.Data.Context
+import public Inky.Data.SnocList.Quantifiers
+
+import Inky.Data.SnocList.Elem
+import Inky.Data.Irrelevant
+import Inky.Decidable
+
+public export
+FreshIn : String -> SnocList String -> Type
+FreshIn n = All (\x => So (x /= n))
+
+public export
+AllFresh : SnocList String -> Type
+AllFresh = Pairwise (So .: (/=))
+
+public export
+record Row (a : Type) where
+  constructor MkRow
+  context : Context a
+  0 fresh : AllFresh context.names
+
+%name Row row
+
+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
+soUnique : (prf1, prf2 : So b) -> prf1 = prf2
+soUnique Oh Oh = Refl
+
+export
+freshInUnique : (freshIn1, freshIn2 : x `FreshIn` sx) -> freshIn1 = freshIn2
+freshInUnique [<] [<] = Refl
+freshInUnique (freshIn1 :< prf1) (freshIn2 :< prf2) =
+  cong2 (:<) (freshInUnique freshIn1 freshIn2) (soUnique prf1 prf2)
+
+export
+freshUnique : (fresh1, fresh2 : AllFresh sx) -> fresh1 = fresh2
+freshUnique [<] [<] = Refl
+freshUnique (fresh1 :< freshIn1) (fresh2 :< freshIn2) =
+  cong2 (:<) (freshUnique fresh1 fresh2) (freshInUnique freshIn1 freshIn2)
+
+export
+rowCong :
+  {0 ctx1, ctx2 : Context a} ->
+  {0 fresh1 : AllFresh ctx1.names} ->
+  {0 fresh2 : AllFresh ctx2.names} ->
+  ctx1 = ctx2 -> MkRow ctx1 fresh1 = MkRow ctx2 fresh2
+rowCong Refl = rewrite freshUnique fresh1 fresh2 in Refl
+
+-- Smart Constructors ----------------------------------------------------------
+
+public export
+Lin : Row a
+Lin = MkRow [<] [<]
+
+public export
+(:<) :
+  (row : Row a) -> (x : Assoc a) ->
+  (0 fresh : x.name `FreshIn` row.names) =>
+  Row a
+row :< x = MkRow (row.context :< x) (row.fresh :< fresh)
+
+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)
+
+-- Operations ------------------------------------------------------------------
+
+export
+isFresh :
+  (names : SnocList String) ->
+  (name : String) ->
+  Dec' (Irrelevant $ name `FreshIn` names)
+isFresh names name =
+  map irrelevant (\contra, prfs => anyNegAll contra $ relevant names prfs.value) $
+  all (\x => (decSo $ x /= name).forget) names
+
+export
+extend : Row a -> Assoc a -> Maybe (Row a)
+extend row x with (isFresh row.names x.name)
+  _ | True `Because` Forget prf = Just (row :< x)
+  _ | False `Because` _ = Nothing
+
+-- Search ----------------------------------------------------------------------
+
+noLookupFresh :
+  (ctx : Context a) ->
+  (0 freshIn : n `FreshIn` ctx.names) ->
+  Not (Elem (n :- x) ctx)
+noLookupFresh (sx :< (n :- x)) (freshIn :< prf) Here with ((decEq n n).reason) | ((decEq n n).does)
+  _ | _ | True = void $ absurd prf
+  _ | contra | False = void $ contra Refl
+noLookupFresh (sx :< (k :- _)) (freshIn :< prf) (There i) = noLookupFresh sx freshIn i
+
+doLookupUnique :
+  (ctx : Context a) ->
+  (0 fresh : AllFresh ctx.names) ->
+  (i : Elem (n :- x) ctx) ->
+  (j : Elem (n :- y) ctx) ->
+  the (x ** Elem (n :- x) ctx) (x ** i) = (y ** j)
+doLookupUnique (ctx :< (n :- x)) (fresh :< freshIn) Here Here = Refl
+doLookupUnique (ctx :< (n :- x)) (fresh :< freshIn) Here (There j) = void $ noLookupFresh ctx freshIn j
+doLookupUnique (ctx :< (n :- z)) (fresh :< freshIn) (There i) Here = void $ noLookupFresh ctx freshIn i
+doLookupUnique (ctx :< (k :- z)) (fresh :< freshIn) (There i) (There j) =
+  cong (\(x ** i) => (x ** There i)) $
+  doLookupUnique ctx fresh i j
+
+export
+lookupUnique :
+  (row : Row a) ->
+  (i : Elem (n :- x) row.context) ->
+  (j : Elem (n :- y) row.context) ->
+  the (x ** Elem (n :- x) row.context) (x ** i) = (y ** j)
+lookupUnique row i j = doLookupUnique row.context row.fresh i j
+
+-- Removal ---------------------------------------------------------------------
+
+dropElemFreshIn :
+  (ctx : Context a) -> n `FreshIn` ctx.names -> (i : Elem nx ctx) ->
+  n `FreshIn` (dropElem ctx i).names
+dropElemFreshIn (ctx :< (n :- x)) (freshIn :< prf) Here = freshIn
+dropElemFreshIn (ctx :< (n :- x)) (freshIn :< prf) (There i) = dropElemFreshIn ctx freshIn i :< prf
+
+export
+dropElemFresh :
+  (ctx : Context a) -> AllFresh ctx.names -> (i : Elem nx ctx) ->
+  AllFresh (dropElem ctx i).names
+dropElemFresh (ctx :< (n :- x)) (fresh :< freshIn) Here = fresh
+dropElemFresh (ctx :< (n :- x)) (fresh :< freshIn) (There i) =
+  dropElemFresh ctx fresh i :< dropElemFreshIn ctx freshIn i
diff --git a/src/Inky/Data/SnocList.idr b/src/Inky/Data/SnocList.idr
new file mode 100644
index 0000000..494e8cc
--- /dev/null
+++ b/src/Inky/Data/SnocList.idr
@@ -0,0 +1,43 @@
+module Inky.Data.SnocList
+
+import public Data.SnocList
+import public Data.SnocList.Operations
+
+import Inky.Decidable.Maybe
+
+public export
+data LengthOf : SnocList a -> Type where
+  Z : LengthOf [<]
+  S : LengthOf sx -> LengthOf (sx :< x)
+
+%name LengthOf len
+
+public export
+lengthOfAppend : LengthOf sx -> LengthOf sy -> LengthOf (sx ++ sy)
+lengthOfAppend len1 Z = len1
+lengthOfAppend len1 (S len2) = S (lengthOfAppend len1 len2)
+
+public export
+lengthOf : (sx : SnocList a) -> LengthOf sx
+lengthOf [<] = Z
+lengthOf (sx :< x) = S (lengthOf sx)
+
+export
+lengthUnique : (len1, len2 : LengthOf sx) -> len1 = len2
+lengthUnique Z Z = Refl
+lengthUnique (S len1) (S len2) = cong S $ lengthUnique len1 len2
+
+export
+isSnoc : (sx : SnocList a) -> Proof (SnocList a, a) (\syy => sx = fst syy :< snd syy) (sx = [<])
+isSnoc [<] = Nothing `Because` Refl
+isSnoc (sx :< x) = Just (sx, x) `Because` Refl
+
+public export
+replicate : Nat -> a -> SnocList a
+replicate 0 x = [<]
+replicate (S n) x = replicate n x :< x
+
+public export
+lengthOfReplicate : (n : Nat) -> (0 x : a) -> LengthOf (replicate n x)
+lengthOfReplicate 0 x = Z
+lengthOfReplicate (S k) x = S (lengthOfReplicate k x)
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
diff --git a/src/Inky/Data/Thinned.idr b/src/Inky/Data/Thinned.idr
new file mode 100644
index 0000000..6ee0d50
--- /dev/null
+++ b/src/Inky/Data/Thinned.idr
@@ -0,0 +1,18 @@
+module Inky.Data.Thinned
+
+import public Inky.Data.SnocList.Thinning
+
+public export
+record Thinned (0 p : SnocList a -> Type) (ctx : SnocList a) where
+  constructor Over
+  {0 support : SnocList a}
+  value : p support
+  thins : support `Thins` ctx
+
+public export
+rename : (ctx1 `Thins` ctx2) -> Thinned p ctx1 -> Thinned p ctx2
+rename f (value `Over` thins) = value `Over` (f . thins)
+
+public export
+(.extract) : Rename a p => Thinned p ctx -> p ctx
+(value `Over` thins).extract = rename thins value