module Core.Term.Thinned

import Core.Term
import Core.Thinning

import Syntax.PreorderReasoning

%prefix_record_projections off

infix 4 =~=

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

public export
record Thinned (n : Nat) where
  constructor Over
  {0 m : Nat}
  term : Term m
  thin : m `Thins` n

%name Thinned t, u, v

%inline
public export
pure : Term n -> Thinned n
pure = (`Over` id n)

%inline
public export
expand : Thinned n -> Term n
expand (term `Over` thin) = wkn term thin

public export
(=~=) : Thinned n -> Thinned n -> Type
t =~= u = expand t = expand u

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

public export
wkn : Thinned m -> m `Thins` n -> Thinned n
wkn t thin = { thin $= (thin .) } t

export
wknCong : t =~= u -> (thin : m `Thins` n) -> wkn t thin =~= wkn u thin
wknCong {t = t `Over` thin1, u = u `Over` thin2} prf thin = Calc $
  |~ wkn t (thin . thin1)
  ~~ wkn (wkn t thin1) thin ...(sym $ wknHomo t thin1 thin)
  ~~ wkn (wkn u thin2) thin ...(cong (flip wkn thin) prf)
  ~~ wkn u (thin . thin2)   ...(wknHomo u thin2 thin)

export
wknId : (t : Thinned n) -> wkn t (id n) = t
wknId (t `Over` thin) = cong (t `Over`) (compLeftId thin)

export
wknHomo :
  (t : Thinned k) ->
  (thin1 : k `Thins` m) ->
  (thin2 : m `Thins` n) ->
  wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1)
wknHomo (t `Over` thin) thin1 thin2 = cong (t `Over`) (compAssoc thin2 thin1 thin)

export
wkn1Comm :
  (t : Thinned m) ->
  (thin : m `Thins` n) ->
  wkn (wkn t thin) (wkn1 n) = wkn (wkn t $ wkn1 m) (keep thin)
wkn1Comm (t `Over` thin') thin = cong (t `Over`) $ Calc $
  |~ wkn1 n . (thin . thin')
  ~~ drop (thin . thin')          ...(compLeftWkn1 (thin . thin'))
  ~~ keep thin . drop thin'       ...(sym $ compRightDrop thin thin')
  ~~ keep thin . (wkn1 m . thin') ...(sym $ cong (keep thin .) $ compLeftWkn1 thin')

-- Interaction with Expansion

export
expandHomo :
  (t : Thinned m) ->
  (thin : m `Thins` n) ->
  expand (wkn t thin) = wkn (expand t) thin
expandHomo (t `Over` thin') thin = sym (wknHomo t thin' thin)