{-|
This module defines intrinsically well-typed terms for Davies' λ○ calculus,
as described in "A Temporal-Logic Approach to Binding-Time Analysis."
It also defines renaming and substitution operations for terms.

The definitions follow the style used in the DeBruijn section of
the PLFA book.
-}

{-# OPTIONS --safe #-}
module Splice.Term where

open import Data.Nat 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 `_

{-|
Intrinsically well-typed terms.
Each constructor corresponds to a rule in the type system.
We add additional rules for the boolean type, which are standard.
-}
data Term where
  -- Rule V
  `_
    : (x : Γ ∋ A ^ n)
      ----------------------
    → Γ ⊢ A ^ n

  -- The true literal
  `true
      --------------
    : Γ ⊢ `Bool ^ n

  -- The false literal
  `false
      --------------
    : Γ ⊢ `Bool ^ n

  -- The if-then-else expression
  `if_`then_`else_
    : (e₁ : Γ ⊢ `Bool ^ n)
    → (e₂ : Γ ⊢ A ^ n)
    → (e₃ : Γ ⊢ A ^ n)
      --------------
    → Γ ⊢ A ^ n

  -- Rule ⇒I
  `λ_
    : (e : Γ , A ^ n ⊢ B ^ n)
      ---------------------------
    → Γ ⊢ A ⇒ B ^ n

  -- Rule ⇒E
  _·_
    : (e₁ : Γ ⊢ A ⇒ B ^ n)
    → (e₂ : Γ ⊢ A ^ n)
      -------------
    → Γ ⊢ B ^ n

  -- Rule ◯I
  ⟨_⟩
    : (e : Γ ⊢ A ^ suc n)
      -------------
    → Γ ⊢ ◯ A ^ n

  -- Rule ◯E
  $_
    : (e : Γ ⊢ ◯ A ^ n)
      ----------------
    → Γ ⊢ A ^ suc n

-- | let-expression encoded as an abstraction followed by an application.
`let_`in_
  : (e₁ : Γ ⊢ A ^ n)
  → (e₂ : Γ , A ^ n ⊢ B ^ n)
    ---------------------------
  → Γ ⊢ B ^ n

`let e₁ `in e₂ = (`λ e₂) · e₁

-- | Extend a renaming function with a new variable.
ext : Rename Γ Γ′ → Rename (Γ , A ^ m) (Γ′ , A ^ m)
ext ρ Z = Z
ext ρ (S x) = S (ρ x)

-- | Rename a term.
rename : Rename Γ Γ′ → Γ ⊢ A ^ n → Γ′ ⊢ A ^ n
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

-- | Substitutions, which map variables in one context to terms in another.
Subst : Context → Context → Set
Subst Γ Γ′ = ∀ {m} {A} → Γ ∋ A ^ m → Γ′ ⊢ A ^ m

-- | Extend a substitution with a new variable.
exts : Subst Γ Γ′ → Subst (Γ , A ^ m) (Γ′ , A ^ m)
exts σ Z = ` Z
exts σ (S x) = rename S (σ x)

-- | Apply a substitution to a term.
subst : Subst Γ Γ′ → Γ ⊢ A ^ n → Γ′ ⊢ A ^ n
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