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

export
data IsNotId : sx `Thins` sy -> Type where
  ItIsThinner : IsNotId (IsThinner thinner)

-- 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) ->
    (0 prf : IsNotId thin) -> -- For uniqueness
    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 ItIsThinner