module Core.Thinning

import Core.Context

import Syntax.PreorderReasoning

-- 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) ->
    {auto 0 prf : IsNotId thin} -> -- For uniqueness
    (0 n : Name) ->
    View (keep thin n)

%name View view

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

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

comp : Thinner sy sz -> Thinner sx sy -> Thinner sx sz
comp (IsBase n) thinner1 = IsDrop thinner1 n
comp (IsDrop thinner2 n) thinner1 = IsDrop (comp thinner2 thinner1) n
comp (IsKeep thinner2 n) (IsBase n) = IsDrop thinner2 n
comp (IsKeep thinner2 n) (IsDrop thinner1 n) = IsDrop (comp thinner2 thinner1) n
comp (IsKeep thinner2 n) (IsKeep thinner1 n) = IsKeep (comp thinner2 thinner1) n

export
(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz
IsId . thin1 = thin1
(IsThinner thinner2) . IsId = IsThinner thinner2
(IsThinner thinner2) . (IsThinner thinner1) = IsThinner (comp thinner2 thinner1)

-- Composition Properties ------------------------------------------------------

-- Identities

export
compLeftIdentity : (thin : sx `Thins` sy) -> id sy . thin = thin
compLeftIdentity thin = Refl

export
compRightIdentity : (thin : sx `Thins` sy) -> thin . id sx = thin
compRightIdentity IsId = Refl
compRightIdentity (IsThinner thinner) = Refl

-- Drop

export
compLeftDrop :
  (thin2 : sy `Thins` sz) ->
  (thin1 : sx `Thins` sy) ->
  (0 n : Name) ->
  drop thin2 n . thin1 = drop (thin2 . thin1) n
compLeftDrop IsId IsId n = Refl
compLeftDrop IsId (IsThinner thinner) n = Refl
compLeftDrop (IsThinner thinner) IsId n = Refl
compLeftDrop (IsThinner thinner) (IsThinner thinner1) n = Refl

export
compRightDrop :
  (thin2 : sy `Thins` sz) ->
  (thin1 : sx `Thins` sy) ->
  (0 n : Name) ->
  keep thin2 n . drop thin1 n = drop (thin2 . thin1) n
compRightDrop IsId thin1 n = Refl
compRightDrop (IsThinner thinner) IsId n = Refl
compRightDrop (IsThinner thinner) (IsThinner thinner1) n = Refl

-- Keep

export
compKeep :
  (thin2 : sy `Thins` sz) ->
  (thin1 : sx `Thins` sy) ->
  (0 n : Name) ->
  keep thin2 n . keep thin1 n = keep (thin2 . thin1) n
compKeep IsId thin1 n = Refl
compKeep (IsThinner thinner) IsId n = Refl
compKeep (IsThinner thinner) (IsThinner thinner1) n = Refl

-- Associative

compAssoc' :
  {thin3 : sz `Thins` sw} ->
  {thin2 : sy `Thins` sz} ->
  {thin1 : sx `Thins` sy} ->
  View thin3 ->
  View thin2 ->
  View thin1 ->
  thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1

compAssoc' (Id sw) view2 view1 = Refl
compAssoc' (Drop thin3 n) view2 view1 = Calc $
  |~ drop thin3 n . (thin2 . thin1)
  ~~ drop (thin3 . (thin2 . thin1)) n ...(compLeftDrop thin3 (thin2 . thin1) n)
  ~~ drop ((thin3 . thin2) . thin1) n ...(cong (\thin => drop thin n) $ compAssoc' (view thin3) view2 view1)
  ~~ drop (thin3 . thin2) n . thin1   ..<(compLeftDrop (thin3 . thin2) thin1 n)
  ~~ (drop thin3 n . thin2) . thin1   ..<(cong (. thin1) $ compLeftDrop thin3 thin2 n)
compAssoc' (Keep thin3 n) (Id _) view1 = cong (. thin1) $ sym $ compRightIdentity (keep thin3 n)
compAssoc' (Keep thin3 n) (Drop thin2 n) view1 = Calc $
  |~ keep thin3 n . (drop thin2 n . thin1)
  ~~ keep thin3 n . drop (thin2 . thin1) n ...(cong (keep thin3 n .) $ compLeftDrop thin2 thin1 n)
  ~~ drop (thin3 . (thin2 . thin1)) n      ...(compRightDrop thin3 (thin2 . thin1) n)
  ~~ drop ((thin3 . thin2) . thin1) n      ...(cong (\thin => drop thin n) $ compAssoc' (view thin3) (view thin2) view1)
  ~~ drop (thin3 . thin2) n . thin1        ..<(compLeftDrop (thin3 . thin2) thin1 n)
  ~~ (keep thin3 n . drop thin2 n) . thin1 ..<(cong (. thin1) $ compRightDrop thin3 thin2 n)
compAssoc' (Keep thin3 n) (Keep thin2 n) (Id _) = Calc $
  |~ keep thin3 n . (keep thin2 n . id _)
  ~~ keep thin3 n . keep thin2 n          ...(cong (keep thin3 n .) $ compRightIdentity (keep thin2 n))
  ~~ (keep thin3 n . keep thin2 n) . id _ ..<(compRightIdentity (keep thin3 n . keep thin2 n))
compAssoc' (Keep thin3 n) (Keep thin2 n) (Drop thin1 n) = Calc $
  |~ keep thin3 n . (keep thin2 n . drop thin1 n)
  ~~ keep thin3 n . drop (thin2 . thin1) n        ...(cong (keep thin3 n .) $ compRightDrop thin2 thin1 n)
  ~~ drop (thin3 . (thin2 . thin1)) n             ...(compRightDrop thin3 (thin2 . thin1) n)
  ~~ drop ((thin3 . thin2) . thin1) n             ...(cong (\thin => drop thin n) $ compAssoc' (view thin3) (view thin2) (view thin1))
  ~~ keep (thin3 . thin2) n . drop thin1 n        ..<(compRightDrop (thin3 . thin2) thin1 n)
  ~~ (keep thin3 n . keep thin2 n) . drop thin1 n ..<(cong (. drop thin1 n) $ compKeep thin3 thin2 n)
compAssoc' (Keep thin3 n) (Keep thin2 n) (Keep thin1 n) = Calc $
  |~ keep thin3 n . (keep thin2 n . keep thin1 n)
  ~~ keep thin3 n . keep (thin2 . thin1) n        ...(cong (keep thin3 n .) $ compKeep thin2 thin1 n)
  ~~ keep (thin3 . (thin2 . thin1)) n             ...(compKeep thin3 (thin2 . thin1) n)
  ~~ keep ((thin3 . thin2) . thin1) n             ...(cong (\thin => keep thin n) $ compAssoc' (view thin3) (view thin2) (view thin1))
  ~~ keep (thin3 . thin2) n . keep thin1 n        ..<(compKeep (thin3 . thin2) thin1 n)
  ~~ (keep thin3 n . keep thin2 n) . keep thin1 n ..<(cong (. keep thin1 n) $ compKeep thin3 thin2 n)

export
compAssoc :
  (thin3 : sz `Thins` sw) ->
  (thin2 : sy `Thins` sz) ->
  (thin1 : sx `Thins` sy) ->
  thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1
compAssoc thin3 thin2 thin1 = compAssoc' (view thin3) (view thin2) (view thin1)

-- Non-Identities

export
compPresNotId : IsNotId thin2 -> IsNotId thin1 -> IsNotId (thin2 . thin1)
compPresNotId ItIsThinner ItIsThinner = ItIsThinner