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)