module Core.Term

import Core.Context
import Core.Var
import Core.Thinning

import Syntax.PreorderReasoning

%prefix_record_projections off

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

public export
data Term : Context -> Type where
  Var : Var sx -> Term sx

  Set : Term sx

  Pi : (n : Name) -> Term sx -> Term (sx :< n) -> Term sx
  Abs : (n : Name) -> Term (sx :< n) -> Term sx
  App : Term sx -> Term sx -> Term sx

%name Term t, u, v

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

public export
wkn : Term sx -> sx `Thins` sy -> Term sy
wkn (Var i) thin = Var $ wkn i thin
wkn Set thin = Set
wkn (Pi n t u) thin = Pi n (wkn t thin) (wkn u $ keep thin n)
wkn (Abs n t) thin = Abs n (wkn t $ keep thin n)
wkn (App t u) thin = App (wkn t thin) (wkn u thin)

-- Is Homomorphic

export
wknHomo :
  (t : Term sx) ->
  (thin1 : sx `Thins` sy) ->
  (thin2 : sy `Thins` sz) ->
  wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1)
wknHomo (Var i) thin1 thin2 = cong Var $ wknHomo i thin1 thin2
wknHomo Set thin1 thin2 = Refl
wknHomo (Pi n t u) thin1 thin2 =
  cong2 (Pi n) (wknHomo t thin1 thin2) $
  Calc $
  |~ wkn (wkn u (keep thin1 n)) (keep thin2 n)
  ~~ wkn u (keep thin2 n . keep thin1 n)       ...(wknHomo u (keep thin1 n) (keep thin2 n))
  ~~ wkn u (keep (thin2 . thin1) n)            ...(cong (wkn u) $ compKeep thin2 thin1 n)
wknHomo (Abs n t) thin1 thin2 =
  cong (Abs n) $
  Calc $
  |~ wkn (wkn t (keep thin1 n)) (keep thin2 n)
  ~~ wkn t (keep thin2 n . keep thin1 n)       ...(wknHomo t (keep thin1 n) (keep thin2 n))
  ~~ wkn t (keep (thin2 . thin1) n)            ...(cong (wkn t) $ compKeep thin2 thin1 n)
wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)

-- Thinned Terms ---------------------------------------------------------------

public export
record Thinned (sx : Context) where
  constructor Over
  {0 sy : Context}
  term : Term sy
  thin : sy `Thins` sx

%name Thinned t, u, v

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

public export
shift : Thinned sx -> sx `Thins` sy -> Thinned sy
shift (term `Over` thin') thin = term `Over` thin . thin'

export
expandShift :
  (t : Thinned sx) ->
  (thin : sx `Thins` sy) ->
  expand (shift t thin) = wkn (expand t) thin
expandShift (term `Over` thin') thin = sym $ wknHomo term thin' thin

export
shiftHomo :
  (t : Thinned sx) ->
  (thin1 : sx `Thins` sy) ->
  (thin2 : sy `Thins` sz) ->
  shift (shift t thin1) thin2 = shift t (thin2 . thin1)
shiftHomo (term `Over` thin) thin1 thin2 = cong (term `Over`) $ compAssoc thin2 thin1 thin