Migrate Env to use Thinned.

3 files changed, 40 insertions, 53 deletions

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index ae7e3aa..2fff434 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -27,9 +27,9 @@ data EnvWf where
     EnvWf [<]
   (:<) :
     EnvWf env ->
-    TypeWf env (wkn a thin) ->
+    TypeWf env (expand t) ->
     ---
-    EnvWf (Add env thin a)
+    EnvWf (Add env t)
 
 data TypeWf where
   SetType :
@@ -150,11 +150,10 @@ data TermConv where
 public export
 data ThinWf : sx `Thins` sy -> Env sy -> Env sx -> Type where
   IdWf : ThinWf (id sx) env env
-  DropWf : ThinWf thin env2 env1 -> ThinWf (drop thin n) (Add env2 thin' a) env1
+  DropWf : ThinWf thin env2 env1 -> ThinWf (drop thin n) (Add env2 t) env1
   KeepWf :
     ThinWf thin env2 env1 ->
-    {auto 0 prf : IsNotId thin} ->
-    ThinWf (keep thin n) (Add env2 (thin . thin') a) (Add env1 thin' a)
+    ThinWf (keep thin n) (Add env2 (shift t thin)) (Add env1 t)
 
 %name ThinWf thinWf
 
@@ -166,7 +165,7 @@ typeConvRespEnvEq : TypeConv env1 a b -> EnvEq env1 env2 -> TypeConv env2 a b
 termWfRespEnvEq : TermWf env1 t a -> EnvEq env1 env2 -> TermWf env2 t a
 termConvRespEnvEq : TermConv env1 t u b -> EnvEq env1 env2 -> TermConv env2 t u b
 
-envWfRespEnvEq [<] [<] = [<]
+envWfRespEnvEq envWf Base = envWf
 envWfRespEnvEq (envWf :< wf) (prf :< eq) =
   envWfRespEnvEq envWf prf :<
   rewrite sym eq in typeWfRespEnvEq wf prf
@@ -282,10 +281,10 @@ CompWf (KeepWf {thin = thin2, n} thinWf2) IdWf =
 CompWf (KeepWf {thin = thin2, n} thinWf2) (DropWf {thin = thin1} thinWf1) =
   rewrite compRightDrop thin2 thin1 n in
   DropWf (CompWf thinWf2 thinWf1)
-CompWf (KeepWf {thin = thin2, n, prf = prf2} thinWf2) (KeepWf {thin = thin1, thin', prf = prf1} thinWf1) =
+CompWf (KeepWf {thin = thin2, n} thinWf2) (KeepWf {thin = thin1, t} thinWf1) =
   rewrite compKeep thin2 thin1 n in
-  rewrite compAssoc thin2 thin1 thin' in
-  KeepWf {prf = compPresNotId prf2 prf1} (CompWf thinWf2 thinWf1)
+  rewrite shiftHomo t thin1 thin2 in
+  KeepWf (CompWf thinWf2 thinWf1)
 
 -- Weakening Preservation ------------------------------------------------------
 
diff --git a/src/Core/Environment.idr b/src/Core/Environment.idr
index ff484f4..a0a10f4 100644
--- a/src/Core/Environment.idr
+++ b/src/Core/Environment.idr
@@ -14,7 +14,7 @@ import Syntax.PreorderReasoning
 public export
 data Env : Context -> Type where
   Lin : Env [<]
-  Add : Env sx -> sy `Thins` sx -> Term sy -> Env (sx :< n)
+  Add : Env sx -> Thinned sx -> Env (sx :< n)
 
 %name Env env
 
@@ -22,66 +22,46 @@ data Env : Context -> Type where
 
 public export
 (:<) : Env sx -> Term sx -> Env (sx :< n)
-env :< t = Add env (id _) t
+env :< t = Add env (t `Over` id sx)
 
--- Operations ------------------------------------------------------------------
+-- Equality --------------------------------------------------------------------
 
-record IndexResult (sx : Context) where
-  constructor MkRes
-  {0 sy : Context}
-  val : Term sy
-  thin : sy `Thins` sx
+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)
 
-shift : IndexResult sx -> IndexResult (sx :< n)
-shift (MkRes val thin) = MkRes val (drop thin n)
+  %name EnvEq prf
 
-expand : IndexResult sx -> Term sx
-expand (MkRes val thin) = wkn val thin
+-- Indexing --------------------------------------------------------------------
 
-doIndex : Env sx -> {0 i : Var sx} -> View i -> IndexResult sx
-doIndex (Add env thin t) Here = shift $ MkRes t thin
-doIndex (Add env thin t) (There i) = shift $ doIndex env $ view i
+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
 
--- Equality --------------------------------------------------------------------
-
-namespace Eq
-  public export
-  data EnvEq : Env sx -> Env sx -> Type where
-    Lin : EnvEq [<] [<]
-    (:<) :
-      EnvEq env1 env2 ->
-      Term.wkn t thin1 = wkn u thin2 ->
-      EnvEq (Add env1 thin1 t) (Add env2 thin2 u)
-
-  %name EnvEq prf
-
-expandShift : (val : IndexResult sx) -> expand (shift val) = wkn (expand val) (drop (id sx) n)
-expandShift (MkRes val thin) = sym $ Calc $
-  |~ wkn (wkn val thin) (drop (id sx) n)
-  ~~ wkn val (drop (id sx) n . thin)     ...(wknHomo val thin $ drop (id sx) n)
-  ~~ wkn val (drop (id sx . thin) n)     ...(cong (wkn val) $ compLeftDrop (id sx) thin n)
-  ~~ wkn val (drop thin n)               ...(cong (\thin => wkn val (drop thin n)) $ compLeftIdentity thin)
+-- Respects Equality
 
 doIndexEqIsEq :
-  -- {env1, env2 : _} ->
   EnvEq env1 env2 ->
   {0 i : Var sx} ->
   (view : View i) ->
   expand (doIndex env1 view) = expand (doIndex env2 view)
-doIndexEqIsEq {sx = sx :< n} ((:<) {t, u, thin1, thin2} prf eq) Here = Calc $
-  |~ wkn t (drop thin1 n)
-  ~~ wkn (wkn t thin1) (drop (id sx) n) ...(expandShift (MkRes t thin1))
-  ~~ wkn (wkn u thin2) (drop (id sx) n) ...(cong (\t => wkn t (drop (id sx) n)) $ eq)
-  ~~ wkn u (drop thin2 n)               ...(sym $ expandShift (MkRes u thin2))
+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)
-  ~~ wkn (expand $ doIndex env1 $ view i) (drop (id sx) n) ...(expandShift $ doIndex env1 $ view i)
-  ~~ wkn (expand $ doIndex env2 $ view i) (drop (id sx) n) ...(cong (\t => wkn t (drop (id sx) n)) $ doIndexEqIsEq prf (view i))
-  ~~ expand (shift $ doIndex env2 $ view i)                ...(sym $ expandShift $ doIndex env2 $ view i)
+  |~ 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
diff --git a/src/Core/Term.idr b/src/Core/Term.idr
index e52545d..182e1ea 100644
--- a/src/Core/Term.idr
+++ b/src/Core/Term.idr
@@ -81,3 +81,11 @@ expandShift :
   (thin : sx `Thins` sy) ->
   expand (shift t thin) = wkn (expand t) thin
 expandShift (term `Over` thin') thin = sym $ wknHomo term thin' thin
+
+export
+shiftHomo :
+  (t : Thinned sx) ->
+  (thin1 : sx `Thins` sy) ->
+  (thin2 : sy `Thins` sz) ->
+  shift (shift t thin1) thin2 = shift t (thin2 . thin1)
+shiftHomo (term `Over` thin) thin1 thin2 = cong (term `Over`) $ compAssoc thin2 thin1 thin