Define Thinnings.

1 files changed, 49 insertions, 0 deletions

diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr
new file mode 100644
index 0000000..425d4ad
--- /dev/null
+++ b/src/Core/Thinning.idr
@@ -0,0 +1,49 @@
+module Core.Thinning
+
+import Core.Context
+
+-- Definition ------------------------------------------------------------------
+
+data Thinner : Context -> Context -> Type where
+  IsBase : (0 n : Name) -> Thinner sx (sx :< n)
+  IsDrop : Thinner sx sy -> (0 n : Name) -> Thinner sx (sy :< n)
+  IsKeep : Thinner sx sy -> (0 n : Name) -> Thinner (sx :< n) (sy :< n)
+
+export
+data Thins : Context -> Context -> Type where
+  IsId : sx `Thins` sx
+  IsThinner : Thinner sx sy -> sx `Thins` sy
+
+%name Thinner thinner
+%name Thins thin
+
+-- Constructors ----------------------------------------------------------------
+
+export
+id : (0 sx : Context) -> sx `Thins` sx
+id sx = IsId
+
+export
+drop : sx `Thins` sy -> (0 n : Name) -> sx `Thins` sy :< n
+drop IsId n = IsThinner (IsBase n)
+drop (IsThinner thinner) n = IsThinner (IsDrop thinner n)
+
+export
+keep : sx `Thins` sy -> (0 n : Name) -> sx :< n `Thins` sy :< n
+keep IsId n = IsId
+keep (IsThinner thinner) n = IsThinner (IsKeep thinner n)
+
+-- Views -----------------------------------------------------------------------
+
+public export
+data View : sx `Thins` sy -> Type where
+  Id : (0 sx : Context) -> View (id sx)
+  Drop : (thin : sx `Thins` sy) -> (0 n : Name) -> View (drop thin n)
+  Keep : (thin : sx `Thins` sy) -> (0 n : Name) -> View (keep thin n)
+
+export
+view : (thin : sx `Thins` sy) -> View thin
+view IsId = Id sx
+view (IsThinner (IsBase n)) = Drop IsId n
+view (IsThinner (IsDrop thinner n)) = Drop (IsThinner thinner) n
+view (IsThinner (IsKeep thinner n)) = Keep (IsThinner thinner) n