module Core.Environment

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

import Syntax.PreorderReasoning

%prefix_record_projections off

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

public export
data Env : Context -> Type where
  Lin : Env [<]
  Add : Env sx -> Thinned sx -> Env (sx :< n)

%name Env env

-- Constructors ----------------------------------------------------------------

public export
(:<) : Env sx -> Term sx -> Env (sx :< n)
env :< t = Add env (t `Over` id sx)

-- Equality --------------------------------------------------------------------

namespace Eq
  public export
  data EnvEq : Env sx -> Env sx -> Type where
    Base : EnvEq env env
    (:<) : EnvEq env1 env2 -> expand t = expand u -> EnvEq (Add env1 t) (Add env2 u)

  %name EnvEq prf

-- Indexing --------------------------------------------------------------------

doIndex : Env sx -> {0 i : Var sx} -> View i -> Thinned sx
doIndex (Add env t) Here = shift t (wkn1 _ _)
doIndex (Add env t) (There i) = shift (doIndex env $ view i) (wkn1 _ _)

export
index : Env sx -> Var sx -> Term sx
index env i = expand $ doIndex env $ view i

-- Respects Equality

doIndexEqIsEq :
  EnvEq env1 env2 ->
  {0 i : Var sx} ->
  (view : View i) ->
  expand (doIndex env1 view) = expand (doIndex env2 view)
doIndexEqIsEq Base view = Refl
doIndexEqIsEq {sx = sx :< n} ((:<) {t, u} prf eq) Here = Calc $
  |~ expand (shift t $ wkn1 sx n)
  ~~ wkn (expand t) (wkn1 sx n)   ...(expandShift t (wkn1 sx n))
  ~~ wkn (expand u) (wkn1 sx n)   ...(cong (\t => wkn t (wkn1 sx n)) $ eq)
  ~~ expand (shift u $ wkn1 sx n) ...(sym $ expandShift u (wkn1 sx n))
doIndexEqIsEq {sx = sx :< n} ((:<) {env1, env2} prf eq) (There i) = Calc $
  |~ expand (shift (doIndex env1 $ view i) (wkn1 sx n))
  ~~ wkn (expand (doIndex env1 $ view i)) (wkn1 sx n)   ...(expandShift (doIndex env1 $ view i) (wkn1 sx n))
  ~~ wkn (expand (doIndex env2 $ view i)) (wkn1 sx n)   ...(cong (\t => wkn t (wkn1 sx n)) $ doIndexEqIsEq prf (view i))
  ~~ expand (shift (doIndex env2 $ view i) (wkn1 sx n)) ...(sym $ expandShift (doIndex env2 $ view i) (wkn1 sx n))

export
indexEqIsEq : EnvEq env1 env2 -> (i : Var sx) -> index env1 i = index env2 i
indexEqIsEq prf i = doIndexEqIsEq prf $ view i