From 0225730f5461e693386031a8f06085d2354d6537 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 25 Mar 2023 16:15:51 +0000
Subject: Extract thinnings to a new module.

Also make the interface more abstract, so more efficient representations
can be swapped in with less cost.
---
 src/CC/Thinning.idr | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 src/CC/Thinning.idr

(limited to 'src/CC/Thinning.idr')

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
-- 
cgit v1.2.3