module CC.Thinning

-- Definition ------------------------------------------------------------------

export
data Thins : (src, tgt : SnocList a) -> Type where
  IsEmpty : [<] `Thins` [<]
  IsDrop : src `Thins` tgt -> src `Thins` tgt :< x
  IsKeep : src `Thins` tgt -> src :< x `Thins` tgt :< x

%name Thins thin

-- Operations ------------------------------------------------------------------

export
empty : [<] `Thins` [<]
empty = IsEmpty

export
drop : src `Thins` tgt -> src `Thins` tgt :< x
drop thin = IsDrop thin

export
keep : src `Thins` tgt -> src :< x `Thins` tgt :< x
keep thin = IsKeep thin

export
id : {ctx : SnocList a} -> ctx `Thins` ctx
id {ctx = [<]} = empty
id {ctx = _ :< _} = keep id

-- Views -----------------------------------------------------------------------

public export
data View : src `Thins` tgt -> Type where
  Empty : View CC.Thinning.empty
  Drop : (thin : src `Thins` tgt) -> View (drop thin)
  Keep : (thin : src `Thins` tgt) -> View (keep thin)

%name View view

public export
view : (thin : src `Thins` tgt) -> View thin
view IsEmpty = Empty
view (IsDrop thin) = Drop thin
view (IsKeep thin) = Keep thin