module Core.Term.Substitution

import Core.Term
import Core.Term.Thinned
import Core.Thinning

infix 4 =~=

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

public export
data Subst : Nat -> Nat -> Type where
  Wkn : m `Thins` n -> Subst m n
  (:<) : Subst m n -> Thinned n -> Subst (S m) n

namespace Eq
  public export
  data (=~=) : Subst m n -> Subst m n -> Type where
    Refl : sub =~= sub
    (:<) : sub1 =~= sub2 -> t =~= u -> sub1 :< t =~= sub2 :< u

%name Subst sub
%name Eq.(=~=) prf

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

public export
index : Subst m n -> Fin m -> Thinned n
index (Wkn thin) i = Var i `Over` thin
index (sub :< t) FZ = t
index (sub :< t) (FS i) = index sub i

-- Weakening -------------------------------------------------------------------

public export
wkn : Subst k m -> m `Thins` n -> Subst k n
wkn (Wkn thin') thin = Wkn (thin . thin')
wkn (sub :< t) thin = wkn sub thin :< wkn t thin

-- Constructors ----------------------------------------------------------------

public export
lift : Subst m n -> Subst (S m) (S n)
lift sub = wkn sub (drop $ id n) :< (Var 0 `Over` id (S n))

-- Substitution ----------------------------------------------------------------

public export
subst : Term m -> Subst m n -> Term n
subst (Var i) sub = expand $ index sub i
subst Set sub = Set
subst (Pi t u) sub = Pi (subst t sub) (subst u $ lift sub)
subst (Abs t) sub = Abs (subst t $ lift sub)
subst (App t u) sub = App (subst t sub) (subst u sub)