{-|
This module defines intrinsically well-typed terms and substitutions for λ○▷
as described in sections 3.2 and 3.3.
It also defines renaming operations for terms and substitutions.

The definitions follow the style used in the DeBruijn section of
the PLFA book, with the exception that substitutions are defined as a concrete 
data type rather than as functions.
-}

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

open import Data.Nat using (ℕ; suc; zero; _≥‴_; ≤‴-refl; ≤‴-step)
open import Function using (id; _∘_)

open import CtxTyp.Context

data Term : (n : ℕ) → Context n → Type n → Set
infix 4 Term
syntax Term n Γ A = Γ ⊢ A ^ n

-- Substitution

infix 4 _⊩_
infix 4 _⊩[_⊢_^_]
infixl 5 _,_
infixl 5 _++ˢ_

{-|
Intrinsically well-typed substitution entries.

Constructors:
  term - An entry whose right-hand side is a term (rule S-Subst).
  var - An entry whose right-hand side is a variable (rule S-Rename).
-}
data _⊩[_⊢_^_] Γ′ {m} (Δ : Context m) (A : Type m) (m≥n : m ≥‴ n) : Set where
  term
    : (e : Γ′ ↾≥ m≥n ++ Δ ⊢ A ^ m)
      ----------------------------
    → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]
  var
    : (x : Γ′ ∋[ Δ ⊢ A ^ m≥n ])
      -------------------------
    → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]

{-|
Intrinsically well-typed substitutions.

Constructors:
  ∅ - The empty substitution.
  _,_ - Add an entry to a substitution.
  _++ˢ_ - Concatenate two substitutions.
-}
data _⊩_ (Γ′ : Context n) : Context n → Set where
  ∅ : Γ′ ⊩ ∅
  _,_ :  (σ : Γ′ ⊩ Γ) → (item : Γ′ ⊩[ Δ ⊢ A ^ m≥n ]) → Γ′ ⊩ Γ ,[ Δ ⊢ A ^ m≥n ]
  _++ˢ_ : Γ′ ⊩ Γ₁ → Γ′ ⊩ Γ₂ →  Γ′ ⊩ Γ₁ ++ Γ₂

-- | Lookup a substitution by a variable (debruijn index).
lookup : Γ′ ⊩ Γ → Γ ∋[ Δ ⊢ A ^ m≥n ] → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]
lookup (σ , e) Z = e
lookup (σ , e) (S x) = lookup σ x
lookup (σ₁ ++ˢ σ₂) (L x) = lookup σ₁ x
lookup (σ₁ ++ˢ σ₂) (R x) = lookup σ₂ x

-- | Turn a function from variables to substitution entries into a substitution.
lookup⁻¹ : (f : ∀ {m} {Δ} {A} {m≥n : m ≥‴ _} → Γ ∋[ Δ ⊢ A ^ m≥n ] → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]) → Γ′ ⊩ Γ
lookup⁻¹ {Γ = ∅} f = ∅
lookup⁻¹ {Γ = Γ ,[ _ ⊢ _ ^ _ ]} f = lookup⁻¹ (f ∘ S) , f Z
lookup⁻¹ {Γ = Γ₁ ++ Γ₂} f = lookup⁻¹ (f ∘ L) ++ˢ lookup⁻¹ (f ∘ R)

-- | Flipped version of the _⊩_ type.
Subst : Context n → Context n → Set
Subst Γ Γ′ = Γ′ ⊩ Γ

-- Term definition

infix 5 `λ⟨_⟩_
infixl 7 _·_
infixr 7 `if_`then_`else_
infix 9 `_`with_

{-|
Intrinsically well-typed terms.
Each constructor corresponds to a rule in the type system.
-}
data Term where
  -- | Rule VarSubst
  `_`with_
    : (x : Γ ∋[ Δ ⊢ A ^ ≤‴-refl ])
    → (σ : Γ ⊩ Δ)
      ----------------------
    → Γ ⊢ A ^ n

  -- | Rule True
  `true
      --------------
    : Γ ⊢ `Bool ^ n

  -- | Rule False
  `false
      --------------
    : Γ ⊢ `Bool ^ n

  -- | Rule If
  `if_`then_`else_
    : (e₁ : Γ ⊢ `Bool ^ n)
    → (e₂ : Γ ⊢ A ^ n)
    → (e₃ : Γ ⊢ A ^ n)
      --------------
    → Γ ⊢ A ^ n

  -- | Rule CtxAbs
  `λ⟨_⟩_
    : ∀ Δ
    → (e : Γ ,[ inject₁ Δ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n)
      ---------------------------
    → Γ ⊢ [ Δ ⊢ A ]⇒ B ^ n

  -- | Rule CtxApp
  _·_
    : (e₁ : Γ ⊢ [ Δ ⊢ A ]⇒ B ^ n)
    → (e₂ : Γ ++ inject₁ Δ ⊢ A ^ n)
      -------------
    → Γ ⊢ B ^ n

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

  -- | Rule LetQuote
  `let⟨_⟩ : ∀ Δ
    → (e₁ : Γ ++ inject₁ Δ ⊢ ◯ A ^ n)
    → (e₂ : Γ ,[ Δ ⊢ A ^ ≤‴-step ≤‴-refl ] ⊢ B ^ n)
      --------------------------------------
    → Γ ⊢ B ^ n

  -- | Rule Wrap
  `wrap : ∀ Δ
    → (e : Γ ++ inject₁ Δ ⊢ A ^ n)
      ----------------------
    → Γ ⊢ Δ ▷ A ^ n
  
  -- | Rule LetWrap
  `letwrap : ∀ Δ
    → (e₁ : Γ ⊢ Δ ▷ A ^ n)
    → (e₂ : Γ ,[ inject₁ Δ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n)
      --------------------------------------
    → Γ ⊢ B ^ n


-- Renaming

-- | Rename a term.
rename : Rename Γ Γ′ → Γ ⊢ A ^ n → Γ′ ⊢ A ^ n
-- | Rename a substitution.
renameSubst : Rename Γ Γ′ → Γ ⊩ Δ → Γ′ ⊩ Δ
-- | Rename a substitution entry.
renameSubstItem : Rename Γ Γ′ → Γ ⊩[ Δ ⊢ A ^ m≥n ] → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]

rename ρ (` x `with σ) = ` ρ x `with renameSubst ρ σ
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 (ext++ _ ρ) e₂
rename ρ ⟨ e ⟩ = ⟨ rename (ext↾ ρ) e ⟩
rename ρ (`let⟨ Δ ⟩ e₁ e₂) = `let⟨ Δ ⟩ (rename (ext++ (inject₁ Δ) ρ) e₁) (rename (ext ρ) e₂)
rename ρ (`wrap Δ e) = `wrap Δ (rename (ext++ (inject₁ Δ) ρ) e)
rename ρ (`letwrap Δ e₁ e₂) = `letwrap Δ (rename ρ e₁) (rename (ext ρ) e₂)

renameSubst ρ ∅ = ∅
renameSubst ρ (σ , item) = renameSubst ρ σ , renameSubstItem ρ item
renameSubst ρ (σ₁ ++ˢ σ₂) = renameSubst ρ σ₁ ++ˢ renameSubst ρ σ₂

renameSubstItem {Δ = Δ} {m≥n = m≥n} ρ (term e) = term (rename (ext++ Δ (ext↾≥ m≥n ρ)) e)
renameSubstItem ρ (var x) = var (ρ x)

-- | Pre-compose a renaming function before a substitution.
renameSubstʳ : Rename Δ′ Δ → Γ ⊩ Δ → Γ ⊩ Δ′
renameSubstʳ ρ σ = lookup⁻¹ (lookup σ ∘ ρ)

-- | Lift a renaming funtion to a substitution.
lift : Rename Γ Γ′ → Subst Γ Γ′
lift ρ = lookup⁻¹ (var ∘ ρ)

-- | Extend a substitution by an identity entry.
exts : Subst Γ Γ′ → Subst (Γ ,[ Δ ⊢ A ^ m≥n ]) (Γ′ ,[ Δ ⊢ A ^ m≥n ])
exts {Δ = Δ} {m≥n = m≥n} σ = renameSubst S σ , var Z

-- | Extend a substitution by multiple identity entries (id_Δ)
exts++ : ∀ Δ → Subst Γ Γ′ → Subst (Γ ++ Δ) (Γ′ ++ Δ)
exts++ Δ σ = renameSubst L σ ++ˢ lift R

-- | Eliminate _↾ from _⊩[_⊢_^_].
⊩[]-↾⁻ : Γ ↾ ⊩[ Δ ⊢ A ^ m≥n ] → Γ ⊩[ Δ ⊢ A ^ ≤‴-step m≥n ]
⊩[]-↾⁻ (term e) = term e
⊩[]-↾⁻ (var x) = var (∋-↾⁻ x)

-- | Introduce _↾ into _⊩[_⊢_^_].
⊩[]-↾⁺ : Γ ⊩[ Δ ⊢ A ^ ≤‴-step m≥n ] → Γ ↾ ⊩[ Δ ⊢ A ^ m≥n ]
⊩[]-↾⁺ (term e) = term e
⊩[]-↾⁺ (var x) = var (∋-↾⁺ x)

-- | Restrict a substitution by removing entries at level n.
exts↾ : Subst Γ Γ′ → Subst (Γ ↾) (Γ′ ↾)
exts↾ ∅ = ∅
exts↾ (_,_ {m≥n = ≤‴-refl} σ item) = exts↾ σ
exts↾ (_,_ {m≥n = ≤‴-step m≥n} σ item) = exts↾ σ , ⊩[]-↾⁺ item
exts↾ (σ₁ ++ˢ σ₂) = exts↾ σ₁ ++ˢ exts↾ σ₂

-- | Restrict a substitution by removing entries below level m.
exts↾≥ : (m≥n : m ≥‴ n) → Subst Γ Γ′ → Subst (Γ ↾≥ m≥n) (Γ′ ↾≥ m≥n)
exts↾≥ ≤‴-refl σ = σ 
exts↾≥ (≤‴-step sm≥n) σ = exts↾≥ sm≥n (exts↾ σ)

-- | Eliminate _↾ from the left of _⊩_ and introduce inject₁ into the right.
⊩-↾⁻ : Γ ↾ ⊩ Δ → Γ ⊩ inject₁ Δ
⊩-↾⁻ ∅ = ∅
⊩-↾⁻ (σ , item) = ⊩-↾⁻ σ , ⊩[]-↾⁻ item
⊩-↾⁻ (σ₁ ++ˢ σ₂) = ⊩-↾⁻ σ₁ ++ˢ ⊩-↾⁻ σ₂

-- | Eliminate inject₁ from the right of _⊩_ and introduce _↾ into the left.
⊩-↾⁺ : Γ ⊩ inject₁ Δ → Γ ↾ ⊩ Δ
⊩-↾⁺ {Δ = ∅} ∅ = ∅
⊩-↾⁺ {Δ = Δ ,[ _ ^ _ ]} (σ , item) = ⊩-↾⁺ σ , ⊩[]-↾⁺ item
⊩-↾⁺ {Δ = Δ₁ ++ Δ₂} (σ₁ ++ˢ σ₂) = ⊩-↾⁺ σ₁ ++ˢ ⊩-↾⁺ σ₂

-- | Eliminate _↾≥_ from the left of _⊩_ and introduce inject≥ into the right.
⊩-↾≥⁻ : ∀ m≥n → Γ ↾≥ m≥n ⊩ Δ → Γ ⊩ inject≥ m≥n Δ
⊩-↾≥⁻ ≤‴-refl σ = σ
⊩-↾≥⁻ (≤‴-step m≥n) σ = ⊩-↾⁻ (⊩-↾≥⁻ m≥n σ)

-- | Eliminate inject≥ from the right of _⊩_ and introduce _↾≥_ into the left.
⊩-↾≥⁺ : ∀ m≥n → Γ ⊩ inject≥ m≥n Δ → Γ ↾≥ m≥n ⊩ Δ
⊩-↾≥⁺ ≤‴-refl σ = σ 
⊩-↾≥⁺ (≤‴-step m≥n) σ = ⊩-↾≥⁺ m≥n (⊩-↾⁺ σ)

-- | Eliminate inject₁ from _⊩[_⊢_^_].
⊩[]-inject₁⁻ : inject₁ Γ ⊩[ Δ′ ⊢ A ^ ≤‴-step m≥n ] → Γ ⊩[ Δ′ ⊢ A ^ m≥n ] 
⊩[]-inject₁⁻ {Δ′ = Δ′} {m≥n = m≥n} (term e) = term (rename (ext++ Δ′ (ext↾≥ m≥n (∋-inject₁⁻ ∘ ∋-↾⁻))) e)
⊩[]-inject₁⁻ (var x) = var (∋-inject₁⁻ x)

-- | Introduce inject₁ into _⊩[_⊢_^_].
⊩[]-inject₁⁺ : Γ ⊩[ Δ′ ⊢ A ^ m≥n ] → inject₁ Γ ⊩[ Δ′ ⊢ A ^ ≤‴-step m≥n ]
⊩[]-inject₁⁺ {Δ′ = Δ′} {m≥n = m≥n} (term e) = term (rename (ext++ Δ′ (ext↾≥ m≥n (∋-↾⁺ ∘ ∋-inject₁⁺))) e)
⊩[]-inject₁⁺ (var x) = var (∋-inject₁⁺ x)

-- | Eliminate inject₁ from both sides of _⊩_.
⊩-inject₁⁻ : inject₁ Γ′ ⊩ inject₁ Γ → Γ′ ⊩ Γ
⊩-inject₁⁻ {Γ = ∅} ∅ = ∅
⊩-inject₁⁻ {Γ = Γ ,[ Δ ⊢ A ^ m≥n ]} (σ , item) = ⊩-inject₁⁻ σ , ⊩[]-inject₁⁻ item
⊩-inject₁⁻ {Γ = Γ ++ Δ} (σ₁ ++ˢ σ₂) = ⊩-inject₁⁻ σ₁ ++ˢ ⊩-inject₁⁻ σ₂

-- | Introduce inject₁ into both sides of _⊩_.
⊩-inject₁⁺ : Γ′ ⊩ Γ → inject₁ Γ′ ⊩ inject₁ Γ
⊩-inject₁⁺ {Γ = ∅} ∅ = ∅ 
⊩-inject₁⁺ {Γ = Γ ,[ Δ ⊢ A ^ m≥n ]} (σ , item) = ⊩-inject₁⁺ σ , ⊩[]-inject₁⁺ item
⊩-inject₁⁺ {Γ = Γ ++ Δ} (σ₁ ++ˢ σ₂) = ⊩-inject₁⁺ σ₁ ++ˢ ⊩-inject₁⁺ σ₂