Fully expand thinnings.

This makes adding CoDebruijn syntax simpler. If carrying the lengths of
contexts around is too inefficient, I can always switch back to
truncated thinnings.

1 files changed, 196 insertions, 105 deletions

diff --git a/src/Thinning.idr b/src/Thinning.idr
index a9b724d..f9e76b5 100644
--- a/src/Thinning.idr
+++ b/src/Thinning.idr
@@ -2,125 +2,239 @@ module Thinning
 
 import Data.SnocList.Elem
 
+%prefix_record_projections off
+
 -- Definition ------------------------------------------------------------------
 
 public export
-data Thins : SnocList a -> SnocList a -> Type
-public export
-data NotId : Thins sx sy -> Type
-
-data Thins where
-  Id : sx `Thins` sx
+data Thins : SnocList a -> SnocList a -> Type where
+  Empty : [<] `Thins` [<]
   Drop : sx `Thins` sy -> sx `Thins` sy :< z
   Keep :
     (thin : sx `Thins` sy) ->
-    {auto 0 prf : NotId thin} ->
     sx :< z `Thins` sy :< z
 
-data NotId where
-  DropNotId : NotId (Drop thin)
-  KeepNotId : (0 prf : NotId thin) -> NotId (Keep thin)
-
 %name Thins thin
 
--- Smart Constructors ----------------------------------------------------------
+-- Utility ---------------------------------------------------------------------
 
 public export
-keep : sx `Thins` sy -> sx :< z `Thins` sy :< z
-keep Id = Id
-keep (Drop thin) = Keep (Drop thin)
-keep (Keep thin) = Keep (Keep thin)
+data Len : SnocList a -> Type where
+  Z : Len [<]
+  S : Len sx -> Len (sx :< x)
+
+%name Len k, m, n
+
+%hint
+export
+length : (sx : SnocList a) -> Len sx
+length [<] = Z
+length (sx :< x) = S (length sx)
+
+%hint
+export
+lenSrc : sx `Thins` sy -> Len sx
+lenSrc Empty = Z
+lenSrc (Drop thin) = lenSrc thin
+lenSrc (Keep thin) = S (lenSrc thin)
+
+%hint
+export
+lenTgt : sx `Thins` sy -> Len sy
+lenTgt Empty = Z
+lenTgt (Drop thin) = S (lenTgt thin)
+lenTgt (Keep thin) = S (lenTgt thin)
+
+%hint
+export
+lenPred : Len (sx :< x) -> Len sx
+lenPred (S k) = k
+
+export
+Cast (Len sx) Nat where
+  cast Z = 0
+  cast (S k) = S (cast k)
+
+-- Smart Constructors ----------------------------------------------------------
+
+export
+empty : (len : Len sx) => [<] `Thins` sx
+empty {len = Z} = Empty
+empty {len = S k} = Drop empty
 
 public export
-empty : (sx : SnocList a) -> [<] `Thins` sx
-empty [<] = Id
-empty (sx :< x) = Drop (empty sx)
+id : (len : Len sx) => sx `Thins` sx
+id {len = Z} = Empty
+id {len = S k} = Keep id
+
+export
+point : Len sx => Elem ty sx -> [<ty] `Thins` sx
+point Here = Keep empty
+point (There i) = Drop (point i)
 
 -- Operations ------------------------------------------------------------------
 
 public export
 index : sx `Thins` sy -> Elem z sx -> Elem z sy
-index Id i = i
 index (Drop thin) i = There (index thin i)
 index (Keep thin) Here = Here
 index (Keep thin) (There i) = There (index thin i)
 
 public export
 (.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz
-compNotId :
-  {0 thin2 : sy `Thins` sz} ->
-  {0 thin1 : sx `Thins` sy} ->
-  NotId thin2 -> NotId thin1 ->
-  NotId (thin2 . thin1)
-
-Id . thin1 = thin1
-(Drop thin2) . thin1 = Drop (thin2 . thin1)
-(Keep thin2) . Id = Keep thin2
-(Keep thin2) . (Drop thin1) = Drop (thin2 . thin1)
-(Keep {prf = prf2} thin2) . (Keep {prf = prf1} thin1) =
-  Keep {prf = compNotId prf2 prf1} (thin2 . thin1)
-
-compNotId DropNotId p = DropNotId
-compNotId (KeepNotId prf) DropNotId = DropNotId
-compNotId (KeepNotId prf) (KeepNotId prf') = KeepNotId (compNotId prf prf')
+Empty . thin1 = thin1
+Drop thin2 . thin1 = Drop (thin2 . thin1)
+Keep thin2 . Drop thin1 = Drop (thin2 . thin1)
+Keep thin2 . Keep thin1 = Keep (thin2 . thin1)
 
--- Properties ------------------------------------------------------------------
+export
+(++) : sx `Thins` sy -> sz `Thins` sw -> sx ++ sz `Thins` sy ++ sw
+thin2 ++ Empty = thin2
+thin2 ++ (Drop thin1) = Drop (thin2 ++ thin1)
+thin2 ++ (Keep thin1) = Keep (thin2 ++ thin1)
+
+-- Commuting Triangles and Coverings -------------------------------------------
+
+data Triangle : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz -> Type where
+  EmptyAny : Triangle Empty thin1 thin1
+  DropAny : Triangle thin2 thin1 thin -> Triangle (Drop thin2) thin1 (Drop thin)
+  KeepDrop : Triangle thin2 thin1 thin -> Triangle (Keep thin2) (Drop thin1) (Drop thin)
+  KeepKeep : Triangle thin2 thin1 thin -> Triangle (Keep thin2) (Keep thin1) (Keep thin)
+
+data Overlap = Covers | Partitions
+
+namespace Covering
+  public export
+  data Covering : Overlap -> sx `Thins` sz -> sy `Thins` sz -> Type where
+    EmptyEmpty : Covering ov Empty Empty
+    DropKeep : Covering ov thin1 thin2 -> Covering ov (Drop thin1) (Keep thin2)
+    KeepDrop : Covering ov thin1 thin2 -> Covering ov (Keep thin1) (Drop thin2)
+    KeepKeep : Covering Covers thin1 thin2 -> Covering Covers (Keep thin1) (Keep thin2)
+
+record Coproduct {sx, sy, sz : SnocList a} (thin1 : sx `Thins` sz) (thin2 : sy `Thins` sz) where
+  constructor MkCoprod
+  {0 sw : SnocList a}
+  {thin1' : sx `Thins` sw}
+  {thin2' : sy `Thins` sw}
+  {thin : sw `Thins` sz}
+  0 left : Triangle thin thin1' thin1
+  0 right : Triangle thin thin2' thin2
+  0 cover : Covering Covers thin1' thin2'
+
+coprod : (thin1 : sx `Thins` sz) -> (thin2 : sy `Thins` sz) -> Coproduct thin1 thin2
+coprod Empty Empty = MkCoprod EmptyAny EmptyAny EmptyEmpty
+coprod (Drop thin1) (Drop thin2) =
+  { left $= DropAny, right $= DropAny } (coprod thin1 thin2)
+coprod (Drop thin1) (Keep thin2) =
+  { left $= KeepDrop, right $= KeepKeep, cover $= DropKeep } (coprod thin1 thin2)
+coprod (Keep thin1) (Drop thin2) =
+  { left $= KeepKeep, right $= KeepDrop, cover $= KeepDrop } (coprod thin1 thin2)
+coprod (Keep thin1) (Keep thin2) =
+  { left $= KeepKeep, right $= KeepKeep, cover $= KeepKeep } (coprod thin1 thin2)
+
+-- Splitting off Contexts ------------------------------------------------------
+
+data Split : (global, local : SnocList a) -> (thin : sx `Thins` global ++ local) -> Type where
+  MkSplit :
+    (thin2 : sx `Thins` global) ->
+    (thin1 : used `Thins` local) ->
+    Split global local (thin2 ++ thin1)
+
+split : Len local -> (thin : sx `Thins` global ++ local) -> Split global local thin
+split Z thin = MkSplit thin Empty
+split (S k) (Drop thin) with (split k thin)
+  split (S k) (Drop .(thin2 ++ thin1)) | MkSplit thin2 thin1 = MkSplit thin2 (Drop thin1)
+split (S k) (Keep thin) with (split k thin)
+  split (S k) (Keep .(thin2 ++ thin1)) | MkSplit thin2 thin1 = MkSplit thin2 (Keep thin1)
+
+-- Thinned Things --------------------------------------------------------------
 
--- NotId
+public export
+record Thinned (T : SnocList a -> Type) (sx : SnocList a) where
+  constructor Over
+  {0 support : SnocList a}
+  value : T support
+  thin : support `Thins` sx
 
-NotIdUnique : (p, q : NotId thin) -> p = q
-NotIdUnique DropNotId DropNotId = Refl
-NotIdUnique (KeepNotId prf) (KeepNotId prf) = Refl
+public export
+record OverlapPair (overlap : Overlap) (T, U : SnocList a -> Type) (sx : SnocList a) where
+  constructor MakePair
+  left : Thinned T sx
+  right : Thinned U sx
+  0 cover : Covering overlap left.thin right.thin
 
--- index
+public export
+Pair : (T, U : SnocList a -> Type) -> SnocList a -> Type
+Pair = OverlapPair Covers
 
 export
-indexKeepHere : (thin : sx `Thins` sy) -> index (keep thin) Here = Here
-indexKeepHere Id = Refl
-indexKeepHere (Drop thin) = Refl
-indexKeepHere (Keep thin) = Refl
+MkPair : Thinned t sx -> Thinned u sx -> Thinned (OverlapPair Covers t u) sx
+MkPair (t `Over` thin1) (u `Over` thin2) =
+  let cp = coprod thin1 thin2 in
+  MakePair (t `Over` cp.thin1') (u `Over` cp.thin2') cp.cover `Over` cp.thin
+
+public export
+record Binds (local : SnocList a) (T : SnocList a -> Type) (sx : SnocList a) where
+  constructor MakeBound
+  {0 used : SnocList a}
+  value : T (sx ++ used)
+  thin : used `Thins` local
 
 export
-indexKeepThere :
-  (thin : sx `Thins` sy) ->
-  (i : Elem x sx) ->
-  index (keep thin) (There i) = There (index thin i)
-indexKeepThere Id i = Refl
-indexKeepThere (Drop thin) i = Refl
-indexKeepThere (Keep thin) i = Refl
+MkBound : Len local -> Thinned t (sx ++ local) -> Thinned (Binds local t) sx
+MkBound k (value `Over` thin) with (split k thin)
+  MkBound k (value `Over` .(thin2 ++ thin1)) | MkSplit thin2 thin1 =
+    MakeBound value thin1 `Over` thin2
+
+export
+map : (forall ctx. t ctx -> u ctx) -> Thinned t ctx -> Thinned u ctx
+map f (value `Over` thin) = f value `Over` thin
+
+%hint
+export
+thinnedLen : Thinned t sx -> Len sx
+thinnedLen (value `Over` thin) = lenTgt thin
+
+-- Properties ------------------------------------------------------------------
+
+export
+lenUnique : (k, m : Len sx) -> k = m
+lenUnique Z Z = Refl
+lenUnique (S k) (S m) = cong S (lenUnique k m)
+
+export
+identityLeft : (len : Len sy) => (thin : sx `Thins` sy) -> id @{len} . thin = thin
+identityLeft {len = Z} thin = Refl
+identityLeft {len = S k} (Drop thin) = cong Drop (identityLeft thin)
+identityLeft {len = S k} (Keep thin) = cong Keep (identityLeft thin)
+
+export
+identityRight : (len : Len sx) => (thin : sx `Thins` sy) -> thin . id @{len} = thin
+identityRight {len = Z} Empty = Refl
+identityRight (Drop thin) = cong Drop (identityRight thin)
+identityRight {len = S k} (Keep thin) = cong Keep (identityRight thin)
 
--- (.)
+export
+identitySquared : (len : Len sx) -> id @{len} . id @{len} = id @{len}
+identitySquared Z = Refl
+identitySquared (S k) = cong Keep (identitySquared k)
 
 export
 assoc :
-  (thin3 : ctx'' `Thins` ctx''') ->
-  (thin2 : ctx' `Thins` ctx'') ->
-  (thin1 : ctx `Thins` ctx') ->
+  (thin3 : sz `Thins` sw) ->
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
   thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1
-assoc Id thin2 thin1 = Refl
+assoc Empty thin2 thin1 = Refl
 assoc (Drop thin3) thin2 thin1 = cong Drop (assoc thin3 thin2 thin1)
-assoc (Keep thin3) Id thin1 = Refl
 assoc (Keep thin3) (Drop thin2) thin1 = cong Drop (assoc thin3 thin2 thin1)
-assoc (Keep thin3) (Keep thin2) Id = Refl
 assoc (Keep thin3) (Keep thin2) (Drop thin1) = cong Drop (assoc thin3 thin2 thin1)
-assoc (Keep {prf = prf3} thin3) (Keep {prf = prf2} thin2) (Keep {prf = prf1} thin1) =
-  let
-    eq : (thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1)
-    eq = assoc thin3 thin2 thin1
-    0 prf :
-      (compNotId prf3 (compNotId prf2 prf1) =
-       (rewrite eq in compNotId (compNotId prf3 prf2) prf1))
-    prf = NotIdUnique _ _
-  in
-  rewrite eq in
-  rewrite prf in
-  Refl
-
-export
-identityRight : (thin : sx `Thins` sy) -> thin . Id = thin
-identityRight Id = Refl
-identityRight (Drop thin) = cong Drop (identityRight thin)
-identityRight (Keep thin) = Refl
+assoc (Keep thin3) (Keep thin2) (Keep thin1) = cong Keep (assoc thin3 thin2 thin1)
+
+export
+indexId : (len : Len sx) => (i : Elem x sx) -> index (id @{len}) i = i
+indexId {len = S k} Here = Refl
+indexId {len = S k} (There i) = cong There (indexId i)
 
 export
 indexHomo :
@@ -128,31 +242,8 @@ indexHomo :
   (thin1 : sx `Thins` sy) ->
   (i : Elem x sx) ->
   index thin2 (index thin1 i) = index (thin2 . thin1) i
-indexHomo Id thin1 i = Refl
-indexHomo (Drop thin2) thin1 i = cong There $ indexHomo thin2 thin1 i
-indexHomo (Keep thin2) Id i = Refl
-indexHomo (Keep thin2) (Drop thin1) i = cong There $ indexHomo thin2 thin1 i
+indexHomo Empty Empty i impossible
+indexHomo (Drop thin2) thin1 i = cong There (indexHomo thin2 thin1 i)
+indexHomo (Keep thin2) (Drop thin1) i = cong There (indexHomo thin2 thin1 i)
 indexHomo (Keep thin2) (Keep thin1) Here = Refl
-indexHomo (Keep thin2) (Keep thin1) (There i) = cong There $ indexHomo thin2 thin1 i
-
-export
-keepHomo :
-  (thin2 : sy `Thins` sz) ->
-  (thin1 : sx `Thins` sy) ->
-  keep thin2 . keep thin1 = keep (thin2 . thin1)
-keepHomo Id thin1 = Refl
-keepHomo (Drop thin2) Id = rewrite identityRight thin2 in Refl
-keepHomo (Drop thin2) (Drop thin1) = Refl
-keepHomo (Drop thin2) (Keep thin1) = Refl
-keepHomo (Keep thin2) Id = Refl
-keepHomo (Keep thin2) (Drop thin) = Refl
-keepHomo (Keep thin2) (Keep thin) = Refl
-
-export
-keepDrop :
-  (thin2 : sy `Thins` sz) ->
-  (thin1 : sx `Thins` sy) ->
-  keep thin2 . Drop thin1 = Drop (thin2 . thin1)
-keepDrop Id thin1 = Refl
-keepDrop (Drop thin2) thin1 = Refl
-keepDrop (Keep thin2) thin1 = Refl
+indexHomo (Keep thin2) (Keep thin1) (There i) = cong There (indexHomo thin2 thin1 i)