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)

public export
wkn1 : (0 sx : Context) -> (0 n : Name) -> sx `Thins` sx :< n
wkn1 sx n = drop (id sx) n

-- Properties

export
dropIsNotId : (thin : sx `Thins` sy) -> (0 n : Name) -> IsNotId (drop thin n)
dropIsNotId IsId n = ItIsThinner
dropIsNotId (IsThinner thinner) n = ItIsThinner

export
keepIdIsId : (0 sx : Context) -> (0 n : Name) -> keep (id sx) n = id (sx :< n)
keepIdIsId sx n = Refl

export
keepNotIdIsNotId : IsNotId thin -> (0 n : Name) -> IsNotId (keep thin n)
keepNotIdIsNotId ItIsThinner n = ItIsThinner

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

-- Unique

viewInverse : {0 thin : sx `Thins` sy} -> View thin -> sx `Thins` sy
viewInverse (Id sy) = id sy
viewInverse (Drop thin n) = drop thin n
viewInverse (Keep thin n) = keep thin n

viewInversePrf1 : (view : View thin) -> viewInverse view = thin
viewInversePrf1 (Id _) = Refl
viewInversePrf1 (Drop _ _) = Refl
viewInversePrf1 (Keep _ _) = Refl

viewInversePrf2 : (v : View thin) -> view (viewInverse v) = (rewrite viewInversePrf1 v in v)
viewInversePrf2 (Id sy) = Refl
viewInversePrf2 (Drop IsId n) = Refl
viewInversePrf2 (Drop (IsThinner thinner) n) = Refl
viewInversePrf2 (Keep {prf} IsId n) impossible
viewInversePrf2 (Keep {prf = ItIsThinner} (IsThinner thinner) n) = Refl

export
viewUnique : (view1, view2 : View thin) -> view1 = view2
viewUnique view1 view2 =
  rewrite sym $ viewInversePrf2 view1 in
  rewrite sym $ viewInversePrf2 view2 in
  rewrite viewInversePrf1 view1 in
  rewrite viewInversePrf1 view2 in
  Refl

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

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)

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

-- Other Properties

export
compLeftWkn1 :
  (thin : sx `Thins` sy) ->
  (0 n : Name) ->
  wkn1 sy n . thin = drop thin n
compLeftWkn1 thin n = Calc $
  |~ drop (id sy) n . thin
  ~~ drop (id sy . thin) n ...(compLeftDrop (id sy) thin n)
  ~~ drop thin n           ...(cong (\thin => drop thin n) $ compLeftIdentity thin)

export
compRightWkn1 :
  (thin : sx `Thins` sy) ->
  (0 n : Name) ->
  keep thin n . wkn1 sx n = drop thin n
compRightWkn1 thin n = Calc $
  |~ keep thin n . drop (id sx) n
  ~~ drop (thin . id sx) n        ...(compRightDrop thin (id sx) n)
  ~~ drop thin n                  ...(cong (\thin => drop thin n) $ compRightIdentity thin)