module SimplyTyped.Substitution where
open import SimplyTyped.TypeSystem
open import SimplyTyped.ContextExtension
import SimplyTyped.Environment as Env
open import Function hiding (_∋_)
module SubstDef (_•_ : TmLike)
where
infix 10 _⇒_
private
module Dummy {Δ : Ctxt} where
open Env (_•_ Δ) public
open Dummy public using (∅; _▷_; lookup)
_⇒_ : Ctxt → Ctxt → Set
Γ ⇒ Δ = Dummy.Env {Δ} Γ
Applier : TmLike → TmLike → Set
Applier _•₁_ _•₂_ = ∀ {Γ Δ τ} → Γ •₁ τ → Γ ⇒ Δ → Δ •₂ τ
record SubstKit : Set where
field
vr : ∀ {Γ τ} → Γ ∋ τ → Γ • τ
weaken : ∀ {Γ σ τ} → Γ • τ → (Γ ▻ σ) • τ
tm : ∀ {Γ τ} → Γ • τ → Γ ⊢ τ
record SubstKit⁺ : Set where
field
kit : SubstKit
_/•_ : Applier _•_ _•_
open SubstDef using (SubstKit; SubstKit⁺) hiding (module SubstKit)
module Subst {_•_ : TmLike}
(kit : SubstKit _•_)
where
open SubstDef _•_ public
open SubstKit kit
infix 70 _↑
infix 48 _[_]
wk⇒ : ∀ {Γ Δ σ} → Γ ⇒ Δ → Γ ⇒ Δ ▻ σ
wk⇒ ∅ = ∅
wk⇒ (ρ ▷ t) = wk⇒ ρ ▷ weaken t
_↑ : ∀ {Γ Δ σ} → Γ ⇒ Δ → Γ ▻ σ ⇒ Δ ▻ σ
ρ ↑ = wk⇒ ρ ▷ vr vz
idˢ : ∀ {Γ} → Γ ⇒ Γ
idˢ {Γ = ε} = ∅
idˢ {Γ = Γ ▻ τ} = idˢ ↑
wk : ∀ {Γ σ} → Γ ⇒ Γ ▻ σ
wk = wk⇒ idˢ
sub : ∀ {Γ τ} → Γ • τ → Γ ▻ τ ⇒ Γ
sub t = idˢ ▷ t
_[_] : Applier _⊢_ _⊢_
var x [ ρ ] = tm (lookup x ρ)
ƛ t [ ρ ] = ƛ (t [ ρ ↑ ])
t₁ · t₂ [ ρ ] = (t₁ [ ρ ]) · (t₂ [ ρ ])
wk⇒⋆ : ∀ {Γ Δ} Δ⁺ → Γ ⇒ Δ → Γ ⇒ Δ ▻▻ Δ⁺
wk⇒⋆ ε ρ = ρ
wk⇒⋆ (Δ⁺ ▻ σ) ρ = wk⇒ (wk⇒⋆ Δ⁺ ρ)
wk⋆ : ∀ {Γ} Γ⁺ → Γ ⇒ Γ ▻▻ Γ⁺
wk⋆ Γ⁺ = wk⇒⋆ Γ⁺ idˢ
module Subst⁺ {_•_ : TmLike}
(kit⁺ : SubstKit⁺ _•_)
where
open SubstDef.SubstKit⁺ kit⁺
open Subst kit public
infixl 70 _∘ˢ_
_∘ˢ_ : ∀ {Γ Δ X} → Γ ⇒ Δ → Δ ⇒ X → Γ ⇒ X
∅ ∘ˢ ρ₂ = ∅
(ρ₁ ▷ t) ∘ˢ ρ₂ = ρ₁ ∘ˢ ρ₂ ▷ (t /• ρ₂)
varKit : SubstKit _∋_
varKit = record
{ vr = id
; weaken = vs
; tm = var
}
varKit⁺ : SubstKit⁺ _∋_
varKit⁺ = record { kit = varKit
; _/•_ = Subst.lookup varKit
}
module VarSubst where
open Subst⁺ varKit⁺ public
tmKit : SubstKit _⊢_
tmKit = record
{ vr = var
; weaken = λ t → t [ wk ]
; tm = id
}
where open VarSubst
tmKit⁺ : SubstKit⁺ _⊢_
tmKit⁺ = record { kit = tmKit
; _/•_ = Subst._[_] tmKit
}
module TmSubst where
open Subst⁺ tmKit⁺ public