Define Env indexing.

1 files changed, 22 insertions, 0 deletions

diff --git a/src/Core/Term/Environment.idr b/src/Core/Term/Environment.idr
index 8e7ce4f..1cc7ba8 100644
--- a/src/Core/Term/Environment.idr
+++ b/src/Core/Term/Environment.idr
@@ -2,6 +2,8 @@ module Core.Term.Environment
 
 import Core.Context
 import Core.Term
+import Core.Thinning
+import Core.Var
 
 -- Definition ------------------------------------------------------------------
 
@@ -11,3 +13,23 @@ data Env : Context -> Type where
   (:<) : 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