{-# OPTIONS --safe #-}
module Splice.Term where
open import Relation.Nullary using (¬_)
open import Function.Base using (id; _∘_)
open import Data.Nat.Base using (ℕ; suc; zero; _≥‴_; ≤‴-refl; ≤‴-step)
open import Splice.Context
data Term : (n : ℕ) → Context → Type n → Set
infix 4 Term
syntax Term n Γ A = Γ ⊢ A ^ n
infix 5 `λ_
infixl 7 _·_
infixr 7 `if_`then_`else_
infix 9 `_
data Term where
`_
: (x : Γ ∋ A ^ n)
→ Γ ⊢ A ^ n
`true
: Γ ⊢ `Bool ^ n
`false
: Γ ⊢ `Bool ^ n
`if_`then_`else_
: (e₁ : Γ ⊢ `Bool ^ n)
→ (e₂ : Γ ⊢ A ^ n)
→ (e₃ : Γ ⊢ A ^ n)
→ Γ ⊢ A ^ n
`λ_
: (e : Γ , A ^ n ⊢ B ^ n)
→ Γ ⊢ A ⇒ B ^ n
_·_
: (e₁ : Γ ⊢ A ⇒ B ^ n)
→ (e₂ : Γ ⊢ A ^ n)
→ Γ ⊢ B ^ n
⟨_⟩
: (e : Γ ⊢ A ^ suc n)
→ Γ ⊢ ◯ A ^ n
$_
: (e : Γ ⊢ ◯ A ^ n)
→ Γ ⊢ A ^ suc n
`let_`in_
: (e₁ : Γ ⊢ A ^ n)
→ (e₂ : Γ , A ^ n ⊢ B ^ n)
→ Γ ⊢ B ^ n
`let e₁ `in e₂ = (`λ e₂) · e₁
ext : Rename Γ Γ′ → Rename (Γ , A ^ m) (Γ′ , A ^ m)
ext ρ Z = Z
ext ρ (S x) = S (ρ x)
rename : Rename Γ Γ′ → Term n Γ A → Term n Γ′ A
rename ρ (` x) = ` ρ x
rename ρ `true = `true
rename ρ `false = `false
rename ρ (`if e₁ `then e₂ `else e₃) = `if rename ρ e₁ `then rename ρ e₂ `else rename ρ e₃
rename ρ (`λ e) = `λ (rename (ext ρ) e)
rename ρ (e₁ · e₂) = rename ρ e₁ · rename ρ e₂
rename ρ ⟨ e ⟩ = ⟨ rename ρ e ⟩
rename ρ ($ e) = $ rename ρ e
Subst : Context → Context → Set
Subst Γ Γ′ = ∀ {m} {A} → Γ ∋ A ^ m → Γ′ ⊢ A ^ m
exts : Subst Γ Γ′ → Subst (Γ , A ^ m) (Γ′ , A ^ m)
exts σ Z = ` Z
exts σ (S x) = rename S (σ x)
subst : Subst Γ Γ′ → Term n Γ A → Term n Γ′ A
subst σ (` x) = σ x
subst σ `true = `true
subst σ `false = `false
subst σ (`if e₁ `then e₂ `else e₃) = `if subst σ e₁ `then subst σ e₂ `else subst σ e₃
subst σ (`λ e) = `λ (subst (exts σ) e)
subst σ (e₁ · e₂) = subst σ e₁ · subst σ e₂
subst σ ⟨ e ⟩ = ⟨ subst σ e ⟩
subst σ ($ e) = $ subst σ e