Make environments do weakening lazily.

This is in anticipation for defining well-formed thinnings.

2 files changed, 11 insertions, 5 deletions

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index 8efda89..4a27923 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -27,9 +27,9 @@ data EnvWf where
     EnvWf [<]
   (:<) :
     EnvWf env ->
-    TypeWf env a ->
+    TypeWf env (wkn a thin) ->
     ---
-    EnvWf (env :< a)
+    EnvWf (Add env thin a)
 
 data TypeWf where
   SetType :
diff --git a/src/Core/Term/Environment.idr b/src/Core/Term/Environment.idr
index 7b05ec0..62e3b60 100644
--- a/src/Core/Term/Environment.idr
+++ b/src/Core/Term/Environment.idr
@@ -12,10 +12,16 @@ import Core.Var
 public export
 data Env : Context -> Type where
   Lin : Env [<]
-  (:<) : Env sx -> Term sx -> Env (sx :< n)
+  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
@@ -25,8 +31,8 @@ record IndexResult (sx : Context) where
   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) =
+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 _)