src/Core/Term/Environment.idr


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

module Core.Term.Environment

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

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

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

%name Env env

-- 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 (env :< t) Here = MkRes t (drop (id _) _)
doIndex (env :< 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