Migrate Substitution to use Thinned.

1 files changed, 16 insertions, 14 deletions

diff --git a/src/Core/Term/Substitution.idr b/src/Core/Term/Substitution.idr
index 248c44f..e69e82f 100644
--- a/src/Core/Term/Substitution.idr
+++ b/src/Core/Term/Substitution.idr
@@ -10,36 +10,32 @@ import Core.Thinning
 public export
 data Subst : Context -> Context -> Type where
   Base : sx `Thins` sy -> Subst sx sy
-  (:<) : Subst sx sy -> (sz `Thins` sy, Term sz) -> Subst (sx :< x) sy
+  (:<) : Subst sx sy -> Thinned sy -> Subst (sx :< x) sy
 
 %name Subst sub
 
--- Constructors ----------------------------------------------------------------
-
-public export
-sub1 : Term sx -> Subst (sx :< n) sx
-sub1 t = Base (id sx) :< (id sx, t)
-
--- Operations ------------------------------------------------------------------
+-- Indexing --------------------------------------------------------------------
 
 export
 index : Subst sx sy -> Var sx -> Term sy
-doIndex : Subst sx sy -> (sz `Thins` sy, Term sz) -> {0 i : Var (sx :< n)} -> View i -> Term sy
+doIndex : Subst sx sy -> Thinned sy -> {0 i : Var (sx :< n)} -> View i -> Term sy
 
 index (Base thin) i = Var $ wkn i thin
-index (sub :< p) i = doIndex sub p (view i)
+index (sub :< t) i = doIndex sub t (view i)
+
+doIndex sub t Here = expand t
+doIndex sub t (There i) = index sub i
 
-doIndex sub (thin, t) Here = wkn t thin
-doIndex sub p (There i) = index sub i
+-- Weakening -------------------------------------------------------------------
 
 public export
 wkn : Subst sx sy -> sy `Thins` sz -> Subst sx sz
 wkn (Base thin') thin = Base (thin . thin')
-wkn (sub :< (thin', t)) thin = wkn sub thin :< (thin . thin', t)
+wkn (sub :< t) thin = wkn sub thin :< shift t thin
 
 public export
 lift : Subst sx sy -> (0 n : Name) -> Subst (sx :< n) (sy :< n)
-lift sub n = wkn sub (drop (id sy) n) :< (id _, Var here)
+lift sub n = wkn sub (wkn1 sy n) :< (Var here `Over` id (sy :< n))
 
 public export
 subst : Term sx -> Subst sx sy -> Term sy
@@ -48,3 +44,9 @@ subst Set sub = Set
 subst (Pi n t u) sub = Pi n (subst t sub) (subst u $ lift sub n)
 subst (Abs n t) sub = Abs n (subst t $ lift sub n)
 subst (App t u) sub = App (subst t sub) (subst u sub)
+
+-- Constructors ----------------------------------------------------------------
+
+public export
+sub1 : Term sx -> Subst (sx :< n) sx
+sub1 t = Base (id sx) :< (t `Over` id sx)