module Core.Term.Substitution

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

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

public export
data Subst : Context -> Context -> Type where
  Base : sx `Thins` sy -> Subst sx sy
  (:<) : Subst sx sy -> Thinned sy -> Subst (sx :< x) sy

%name Subst sub

-- Indexing --------------------------------------------------------------------

export
index : Subst sx sy -> Var sx -> 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 :< t) i = doIndex sub t (view i)

doIndex sub t Here = expand t
doIndex sub t (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 :< 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 (wkn1 sy n) :< (Var here `Over` id (sy :< n))

public export
subst : Term sx -> Subst sx sy -> Term sy
subst (Var i) sub = index sub i
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)