Define Thinnings.

1 files changed, 55 insertions, 0 deletions

diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr
new file mode 100644
index 0000000..0067ac4
--- /dev/null
+++ b/src/Core/Thinning.idr
@@ -0,0 +1,55 @@
+module Core.Thinning
+
+-- Definition ------------------------------------------------------------------
+
+data Thinner : Nat -> Nat -> Type where
+  IsBase : Thinner n (S n)
+  IsDrop : Thinner m n -> Thinner m (S n)
+  IsKeep : Thinner m n -> Thinner (S m) (S n)
+
+export
+data Thins : Nat -> Nat -> Type where
+  IsId : n `Thins` n
+  IsThinner : Thinner m n -> m `Thins` n
+
+%name Thinner thin
+%name Thins thin
+
+-- Constructors ----------------------------------------------------------------
+
+export
+id : (0 n : Nat) -> n `Thins` n
+id n = IsId
+
+export
+drop : m `Thins` n -> m `Thins` S n
+drop IsId = IsThinner IsBase
+drop (IsThinner thin) = IsThinner (IsDrop thin)
+
+export
+keep : m `Thins` n -> S m `Thins` S n
+keep IsId = IsId
+keep (IsThinner thin) = IsThinner (IsKeep thin)
+
+-- Non-Identity ----------------------------------------------------------------
+
+export
+data IsNotId : m `Thins` n -> Type where
+  ItIsThinner : IsNotId (IsThinner thin)
+
+%name IsNotId prf
+
+-- Views -----------------------------------------------------------------------
+
+public export
+data View : m `Thins` n -> Type where
+  Id : (0 n : Nat) -> View (id n)
+  Drop : (thin : m `Thins` n) -> View (drop thin)
+  Keep : (thin : m `Thins` n) -> {auto 0 prf : IsNotId thin} -> View (keep thin)
+
+export
+view : (thin : m `Thins` n) -> View thin
+view IsId = Id m
+view (IsThinner IsBase) = Drop (id _)
+view (IsThinner (IsDrop thin)) = Drop (IsThinner thin)
+view (IsThinner (IsKeep thin)) = Keep (IsThinner thin)