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 -> (sz `Thins` sy, Term sz) -> 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 ------------------------------------------------------------------

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

index (Base thin) i = Var $ wkn i thin
index (sub :< p) i = doIndex sub p (view i)

doIndex sub (thin, t) Here = wkn t thin
doIndex sub p (There i) = index sub i

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)

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)

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)