module Core.Term.Environment

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

%prefix_record_projections off

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

public export
data Env : Context -> Type where
  Lin : Env [<]
  Add : Env sx -> sy `Thins` sx -> Term sy -> Env (sx :< n)

%name Env env

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

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

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

record IndexResult (sx : Context) where
  constructor MkRes
  {0 sy : Context}
  val : Term sy
  thin : sy `Thins` sx

doIndex : Env sx -> {0 i : Var sx} -> View i -> IndexResult sx
doIndex (Add env thin t) Here = MkRes t (drop thin _)
doIndex (Add env thin t) (There i) =
  let MkRes val thin = doIndex env $ view i in
  MkRes val (drop thin _)

export
index : Env sx -> Var sx -> Term sx
index env i =
  let MkRes val thin = doIndex env $ view i in
  wkn val thin

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

namespace Eq
  public export
  data EnvEq : Env sx -> Env sx -> Type where
    Lin : EnvEq [<] [<]
    Add :
      EnvEq env1 env2 ->
      Term.wkn t thin1 = wkn u thin2 ->
      EnvEq (Add env1 thin1 t) (Add env2 thin2 u)

  %name EnvEq prf

  public export
  (:<) : EnvEq env1 env2 -> (0 t : Term sx) -> EnvEq (env1 :< t) (env2 :< t)
  prf :< t = Add prf Refl