12 files changed, 44 insertions, 732 deletions
diff --git a/src/Inky/Data/Assoc.idr b/src/Inky/Data/Assoc.idr
deleted file mode 100644
index 0818ba3..0000000
--- a/src/Inky/Data/Assoc.idr
+++ /dev/null
@@ -1,38 +0,0 @@
-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 a : Type) (n : String) where
-    constructor (:-)
-    0 name : String
-    {auto 0 prf : n = name}
-    value : a
-
-  public export
-  map : (a -> b) -> Assoc0 a n -> Assoc0 b n
-  map f (n :- x) = n :- f x
-
-namespace Contexts
-  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
deleted file mode 100644
index 4c5f6cf..0000000
--- a/src/Inky/Data/Context.idr
+++ /dev/null
@@ -1,34 +0,0 @@
-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 : {sx : SnocList String} -> All (Assoc0 a) sx -> Context a
-fromAll [<] = [<]
-fromAll {sx = sx :< n} (ctx :< (_ :- x)) = fromAll ctx :< (n :- x)
-
-export
-fromAllNames : {sx : SnocList String} -> (ctx : All (Assoc0 a) sx) -> (fromAll ctx).names = sx
-fromAllNames [<] = Refl
-fromAllNames {sx = sx :< n} (ctx :< (k :- x)) = cong (:< n) $ fromAllNames ctx
diff --git a/src/Inky/Data/Context/Var.idr b/src/Inky/Data/Context/Var.idr
deleted file mode 100644
index 4741580..0000000
--- a/src/Inky/Data/Context/Var.idr
+++ /dev/null
@@ -1,117 +0,0 @@
-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
index d9acb7d..390745a 100644
--- a/src/Inky/Data/Fun.idr
+++ b/src/Inky/Data/Fun.idr
@@ -1,7 +1,7 @@
 module Inky.Data.Fun
 
-import public Inky.Data.SnocList.Quantifiers
-import Inky.Data.SnocList
+import public Flap.Data.SnocList.Quantifiers
+import Flap.Data.SnocList
 
 public export
 Fun : SnocList Type -> Type -> Type
diff --git a/src/Inky/Data/List.idr b/src/Inky/Data/List.idr
deleted file mode 100644
index 24cb9c0..0000000
--- a/src/Inky/Data/List.idr
+++ /dev/null
@@ -1,13 +0,0 @@
-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 42f18da..8362770 100644
--- a/src/Inky/Data/Row.idr
+++ b/src/Inky/Data/Row.idr
@@ -1,11 +1,12 @@
 module Inky.Data.Row
 
 import public Data.So
-import public Inky.Data.Context
-import public Inky.Data.SnocList.Quantifiers
+import public Flap.Data.Context
+import public Flap.Data.SnocList.Quantifiers
 
-import Inky.Data.SnocList.Elem
-import Inky.Decidable
+import Data.Singleton
+import Flap.Data.SnocList.Elem
+import Flap.Decidable
 
 public export
 FreshIn : String -> SnocList String -> Type
@@ -154,6 +155,33 @@ lookupUnique :
   the (x ** Elem (n :- x) row.context) (x ** i) = (y ** j)
 lookupUnique row i j = doLookupUnique row.context row.fresh i j
 
+notHere :
+  {0 ctx : Context a} ->
+  (i : Elem (n :- x) (ctx :< (l :- y))) ->
+  Not (n = l) -> (j : Elem (n :- x) ctx ** i = There j)
+notHere Here neq = void $ neq Refl
+notHere (There i) _ = (i ** Refl)
+
+doLookupRecompute :
+  (ctx : Context a) -> (0 fresh : AllFresh ctx.names) ->
+  {n : String} -> (0 i : Elem (n :- x) ctx) -> Singleton i
+doLookupRecompute [<] [<] i = void $ absurd i
+doLookupRecompute (ctx :< (l :- x)) (fresh :< freshIn) i with (decEq n l)
+  doLookupRecompute (ctx :< (l :- x)) (fresh :< freshIn) i | True `Because` Refl =
+    replace {p = \x => Singleton x.snd}
+      (doLookupUnique (ctx :< (l :- x)) (fresh :< freshIn) Here i)
+      (Val Here)
+  _ | False `Because` contra =
+    let 0 jeq = notHere i contra in
+    rewrite snd jeq in
+    [| There $ doLookupRecompute ctx fresh (fst jeq) |]
+
+export
+lookupRecompute :
+  (row : Row a) -> {n : String} ->
+  (0 i : Elem (n :- x) row.context) -> Singleton i
+lookupRecompute row i = doLookupRecompute row.context row.fresh i
+
 -- Removal ---------------------------------------------------------------------
 
 dropElemFreshIn :
diff --git a/src/Inky/Data/SnocList.idr b/src/Inky/Data/SnocList.idr
deleted file mode 100644
index 494e8cc..0000000
--- a/src/Inky/Data/SnocList.idr
+++ /dev/null
@@ -1,43 +0,0 @@
-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
deleted file mode 100644
index c1e69f6..0000000
--- a/src/Inky/Data/SnocList/Elem.idr
+++ /dev/null
@@ -1,116 +0,0 @@
-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.List
-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
-
-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
-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
deleted file mode 100644
index 886c4e4..0000000
--- a/src/Inky/Data/SnocList/Quantifiers.idr
+++ /dev/null
@@ -1,44 +0,0 @@
-module Inky.Data.SnocList.Quantifiers
-
-import public Data.SnocList.Quantifiers
-
-import Data.List.Quantifiers
-import Inky.Data.SnocList
-import Inky.Data.SnocList.Elem
-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) -> LazyEither (p x) (q x)) ->
-  (sx : SnocList a) -> LazyEither (All p sx) (Any q 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
-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
deleted file mode 100644
index 60666d2..0000000
--- a/src/Inky/Data/SnocList/Thinning.idr
+++ /dev/null
@@ -1,228 +0,0 @@
-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
-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
-(<><) : 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)
-
-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
deleted file mode 100644
index cc7c088..0000000
--- a/src/Inky/Data/SnocList/Var.idr
+++ /dev/null
@@ -1,90 +0,0 @@
-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
index 6ee0d50..eaf5e7b 100644
--- a/src/Inky/Data/Thinned.idr
+++ b/src/Inky/Data/Thinned.idr
@@ -1,6 +1,6 @@
 module Inky.Data.Thinned
 
-import public Inky.Data.SnocList.Thinning
+import public Flap.Data.SnocList.Thinning
 
 public export
 record Thinned (0 p : SnocList a -> Type) (ctx : SnocList a) where
@@ -11,8 +11,15 @@ record Thinned (0 p : SnocList a -> Type) (ctx : SnocList a) where
 
 public export
 rename : (ctx1 `Thins` ctx2) -> Thinned p ctx1 -> Thinned p ctx2
-rename f (value `Over` thins) = value `Over` (f . thins)
+rename f v = v.value `Over` (f . v.thins)
 
 public export
 (.extract) : Rename a p => Thinned p ctx -> p ctx
-(value `Over` thins).extract = rename thins value
+v.extract = rename v.thins v.value
+
+export
+0 extractHomo :
+  Rename a p =>
+  (f : ctx1 `Thins` ctx2) -> (x : Thinned p ctx1) ->
+  rename f x.extract = (rename f x).extract
+extractHomo f x = renameHomo f x.thins x.value