From fe1f03b7cd7cfeb9992a968b5a5cbebe8fbe9b7d Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Fri, 14 Apr 2023 17:42:31 +0100 Subject: Define Thinnings. --- src/Core/Thinning.idr | 55 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 src/Core/Thinning.idr (limited to 'src') 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) -- cgit v1.2.3