module Core.Thinning

import Data.Fin

-- 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)

-- Composition -----------------------------------------------------------------

comp : Thinner m n -> Thinner k m -> Thinner k n
comp IsBase thin2 = IsDrop thin2
comp (IsDrop thin1) thin2 = IsDrop (comp thin1 thin2)
comp (IsKeep thin1) IsBase = IsDrop thin1
comp (IsKeep thin1) (IsDrop thin2) = IsDrop (comp thin1 thin2)
comp (IsKeep thin1) (IsKeep thin2) = IsKeep (comp thin1 thin2)

export
(.) : m `Thins` n -> k `Thins` m -> k `Thins` n
IsId . thin2 = thin2
IsThinner thin1 . IsId = IsThinner thin1
IsThinner thin1 . IsThinner thin2 = IsThinner (comp thin1 thin2)

-- Specific Cases

export
compRightId : (thin : m `Thins` n) -> thin . id m = thin
compRightId IsId = Refl
compRightId (IsThinner thin) = Refl

export
compKeep :
  (thin1 : m `Thins` n) ->
  (thin2 : k `Thins` m) ->
  keep thin1 . keep thin2 = keep (thin1 . thin2)
compKeep IsId thin2 = Refl
compKeep (IsThinner thin1) IsId = Refl
compKeep (IsThinner thin1) (IsThinner thin2) = Refl

-- Weakening -------------------------------------------------------------------

wkn' : Fin m -> Thinner m n -> Fin n
wkn' i IsBase = FS i
wkn' i (IsDrop thin) = FS (wkn' i thin)
wkn' FZ (IsKeep thin) = FZ
wkn' (FS i) (IsKeep thin) = FS (wkn' i thin)

export
wkn : Fin m -> m `Thins` n -> Fin n
wkn i IsId = i
wkn i (IsThinner thin) = wkn' i thin

-- Properties

wkn'Homo :
  (i : Fin k) ->
  (thin2 : Thinner m n) ->
  (thin1 : Thinner k m) ->
  wkn' (wkn' i thin1) thin2 = wkn' i (comp thin2 thin1)
wkn'Homo i IsBase thin1 = Refl
wkn'Homo i (IsDrop thin2) thin1 = cong FS (wkn'Homo i thin2 thin1)
wkn'Homo i (IsKeep thin2) IsBase = Refl
wkn'Homo i (IsKeep thin2) (IsDrop thin1) = cong FS (wkn'Homo i thin2 thin1)
wkn'Homo FZ (IsKeep thin2) (IsKeep thin1) = Refl
wkn'Homo (FS i) (IsKeep thin2) (IsKeep thin1) = cong FS (wkn'Homo i thin2 thin1)

export
wknHomo :
  (i : Fin k) ->
  (thin1 : k `Thins` m) ->
  (thin2 : m `Thins` n) ->
  wkn (wkn i thin1) thin2 = wkn i (thin2 . thin1)
wknHomo i IsId thin2 = sym $ cong (wkn i) $ compRightId thin2
wknHomo i (IsThinner thin1) IsId = Refl
wknHomo i (IsThinner thin1) (IsThinner thin2) = wkn'Homo i thin2 thin1