Extract thinnings to a new module.

Also make the interface more abstract, so more efficient representations
can be swapped in with less cost.

1 files changed, 46 insertions, 0 deletions

diff --git a/src/CC/Thinning.idr b/src/CC/Thinning.idr
new file mode 100644
index 0000000..284a230
--- /dev/null
+++ b/src/CC/Thinning.idr
@@ -0,0 +1,46 @@
+module CC.Thinning
+
+-- Definition ------------------------------------------------------------------
+
+export
+data Thins : (src, tgt : SnocList a) -> Type where
+  IsEmpty : [<] `Thins` [<]
+  IsDrop : src `Thins` tgt -> src `Thins` tgt :< x
+  IsKeep : src `Thins` tgt -> src :< x `Thins` tgt :< x
+
+%name Thins thin
+
+-- Operations ------------------------------------------------------------------
+
+export
+empty : [<] `Thins` [<]
+empty = IsEmpty
+
+export
+drop : src `Thins` tgt -> src `Thins` tgt :< x
+drop thin = IsDrop thin
+
+export
+keep : src `Thins` tgt -> src :< x `Thins` tgt :< x
+keep thin = IsKeep thin
+
+export
+id : {ctx : SnocList a} -> ctx `Thins` ctx
+id {ctx = [<]} = empty
+id {ctx = _ :< _} = keep id
+
+-- Views -----------------------------------------------------------------------
+
+public export
+data View : src `Thins` tgt -> Type where
+  Empty : View CC.Thinning.empty
+  Drop : (thin : src `Thins` tgt) -> View (drop thin)
+  Keep : (thin : src `Thins` tgt) -> View (keep thin)
+
+%name View view
+
+public export
+view : (thin : src `Thins` tgt) -> View thin
+view IsEmpty = Empty
+view (IsDrop thin) = Drop thin
+view (IsKeep thin) = Keep thin