{-|
This module defines the operational semantics of λ○▷ as described in section 4.2.
It includes the reduction relation, the definition of values, and the progress theorem (Theorem 4.4).
Intrinsic typing ensures that reduction relation preserve typing (Theorem 4.3).
The module also defines the reflexive transitive closure of the reduction relation.
-}

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

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; suc; zero; _≥‴_; ≤‴-refl; ≤‴-step)
open import Function using (id; _∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import CtxTyp.Context
open import CtxTyp.Term
open import CtxTyp.Depth
open import CtxTyp.Substitution

variable
  e e₁ e₂ e₃ e′ e₁′ e₂′ e₃′ e″ : Term n Γ A

-- | Single substitution
_[_] : Γ ,[ Δ ⊢ A ^ m≥n ] ⊢ B ^ n → Γ ↾≥ m≥n ++ Δ ⊢ A ^ m → Γ ⊢ B ^ n
e₁ [ e₂ ] = subst (lift id , term e₂) e₁

-- | The value judgment, where (Value e) asserts that e is a value.
data Value : Γ ⊢ A ^ n → Set where
  `λ⟨_⟩_ : ∀ Δ → (e : Γ ,[ inject₁ Δ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n) → Value (`λ⟨ Δ ⟩ e)
  `true : Value {Γ = Γ} `true
  `false : Value {Γ = Γ} `false
  ⟨_⟩ : (e : Γ ↾ ⊢ A ^ suc n) → Value {Γ = Γ} ⟨ e ⟩
  `wrap : ∀ Δ → (e : Γ ++ inject₁ Δ ⊢ A ^ n) → (v : Value e) → Value (`wrap Δ e)

-- | The reduction relation. Intrinsic typing ensures that reduction preserves typing (Theorem 4.3).
infix  _-→_
data _-→_ {n} {Γ} : Γ ⊢ A ^ n → Γ ⊢ A ^ n → Set where
  β-λ⟨⟩· : Value e₂ → (`λ⟨ Δ ⟩ e₁) · e₂ -→ e₁ [ e₂ ] -- ^ Rule CtxAppAbs
  β-if-true : `if `true `then e₂ `else e₃ -→ e₂ -- ^ Rule IfTrue
  β-if-false : `if `false `then e₂ `else e₃ -→ e₃ -- ^ Rule IfFalse
  β-let⟨⟩ : {e₂ : Γ ,[ Δ ⊢ A ^ ≤‴-step ≤‴-refl ] ⊢ B ^ n} → `let⟨ Δ ⟩ ⟨ e₁ ⟩ e₂ -→ e₂ [ rename (ext++ˡ (Γ ↾) (∋-inject₁⁻ ∘ ∋-↾⁻)) e₁ ] -- ^ Rule LetQuoteQuote
  β-letwrap : Value (`wrap Δ e₁) → `letwrap Δ (`wrap Δ e₁) e₂ -→ e₂ [ e₁ ] -- ^ Rule LetWrapWrap

  ξ-·₁ : e₁ -→ e₁′ → e₁ · e₂ -→ e₁′ · e₂ -- ^ Rule CongCtxApp1
  ξ-·₂ : Value e₁ → e₂ -→ e₂′ → e₁ · e₂ -→ e₁ · e₂′ -- ^ Rule CongCtxApp2
  ξ-if₁ : e₁ -→ e₁′ → `if e₁ `then e₂ `else e₃ -→ `if e₁′ `then e₂ `else e₃ -- ^ Rule CongIf1
  ξ-let⟨⟩₁ : e₁ -→ e₁′ → `let⟨ Δ ⟩ e₁ e₂ -→ `let⟨ Δ ⟩ e₁′ e₂ -- ^ Rule CongLetQuote1
  ξ-wrap : e -→ e′ → `wrap Δ e -→ `wrap Δ e′ -- ^ Rule CongWrap
  ξ-letwrap₁ : e₁ -→ e₁′ → `letwrap Δ e₁ e₂ -→ `letwrap Δ e₁′ e₂ -- ^ Rule CongLetWrap1

-- | The output of the progress theorem, which states that a term can either take a step or is a value.
data Progress : Γ ⊢ A ^ n → Set where
  p-step : e -→ e′ → Progress e
  p-value : Value e → Progress e

-- | The progress theorem (Theorem 4.4).
progress : (e : inject₁ Γ ⊢ A ^ n) → Progress e

progress (` x `with σ) = ⊥-elim (inject₁-∌-refl x)
progress `true = p-value `true
progress `false = p-value `false
progress (`if e₁ `then e₂ `else e₃) with progress e₁
... | p-step e₁-→e₁′ = p-step (ξ-if₁ e₁-→e₁′)
... | p-value `true = p-step β-if-true
... | p-value `false = p-step β-if-false
progress (`λ⟨ Δ ⟩ e) = p-value (`λ⟨ Δ ⟩ e)
progress (e₁ · e₂) with progress e₁
... | p-step e₁-→e₁′ = p-step (ξ-·₁ e₁-→e₁′)
... | p-value ve₁@(`λ⟨ Δ ⟩ e₁′) with progress e₂
...   | p-step e₂-→e₂′ = p-step (ξ-·₂ ve₁ e₂-→e₂′)
...   | p-value ve₂ = p-step (β-λ⟨⟩· ve₂)
progress ⟨ e ⟩ = p-value ⟨ e ⟩
progress (`let⟨ Δ ⟩ e₁ e₂) with progress e₁
... | p-step e₁-→e₁′ = p-step (ξ-let⟨⟩₁ e₁-→e₁′)
... | p-value ⟨ e ⟩ = p-step β-let⟨⟩
progress (`wrap Δ e) with progress e
... | p-step e-→e′ = p-step (ξ-wrap e-→e′)
... | p-value ve = p-value (`wrap Δ e ve)
progress (`letwrap Δ e₁ e₂) with progress e₁
... | p-step e₁-→e₁′ = p-step (ξ-letwrap₁ e₁-→e₁′)
... | p-value v₁@(`wrap Δ e ve) = p-step (β-letwrap v₁)


-- The following definition are for the adequacy theorem proved in CtxTyp.Denotational.Adequacy.

-- | Reflexive transitive closure of the reduction relation
infix  _-→*_
data _-→*_ {n} {Γ} : Γ ⊢ A ^ n → Γ ⊢ A ^ n → Set where
  -→*-refl : e -→* e
  -→*-step : e -→ e′ → e′ -→* e″ → e -→* e″

-→*-reflexive : e ≡ e′ → e -→* e′
-→*-reflexive refl = -→*-refl

-→*-trans : e -→* e′ → e′ -→* e″ → e -→* e″
-→*-trans -→*-refl = id
-→*-trans (-→*-step e-→e₁ e₁-→*e′) = -→*-step e-→e₁ ∘ -→*-trans e₁-→*e′

ξ-if₁* : e₁ -→* e₁′ → `if e₁ `then e₂ `else e₃ -→* `if e₁′ `then e₂ `else e₃
ξ-if₁* -→*-refl = -→*-refl
ξ-if₁* (-→*-step e₁-→e₁′ e₁′-→*e₁″) = -→*-step (ξ-if₁ e₁-→e₁′) (ξ-if₁* e₁′-→*e₁″)

ξ-·₁* : e₁ -→* e₁′ → e₁ · e₂ -→* e₁′ · e₂
ξ-·₁* -→*-refl = -→*-refl
ξ-·₁* (-→*-step e₁-→e₁′ e₁′-→*e₁″) = -→*-step (ξ-·₁ e₁-→e₁′) (ξ-·₁* e₁′-→*e₁″)

ξ-·₂* : Value e₁ → e₂ -→* e₂′ → e₁ · e₂ -→* e₁ · e₂′
ξ-·₂* ve₁ -→*-refl = -→*-refl
ξ-·₂* ve₁ (-→*-step e₂-→e₂′ e₂′-→*e₂″) = -→*-step (ξ-·₂ ve₁ e₂-→e₂′) (ξ-·₂* ve₁ e₂′-→*e₂″)

ξ-let⟨⟩₁* : e₁ -→* e₁′ → `let⟨ Δ ⟩ e₁ e₂ -→* `let⟨ Δ ⟩ e₁′ e₂
ξ-let⟨⟩₁* -→*-refl = -→*-refl
ξ-let⟨⟩₁* (-→*-step e₁-→e₁′ e₁′-→*e₁″) = -→*-step (ξ-let⟨⟩₁ e₁-→e₁′) (ξ-let⟨⟩₁* e₁′-→*e₁″)

ξ-wrap* : e -→* e′ → `wrap Δ e -→* `wrap Δ e′
ξ-wrap* -→*-refl = -→*-refl
ξ-wrap* (-→*-step e-→e′ e′-→*e″) = -→*-step (ξ-wrap e-→e′) (ξ-wrap* e′-→*e″)

ξ-letwrap₁* : e₁ -→* e₁′ → `letwrap Δ e₁ e₂ -→* `letwrap Δ e₁′ e₂
ξ-letwrap₁* -→*-refl = -→*-refl
ξ-letwrap₁* (-→*-step e₁-→e₁′ e₁′-→*e₁″) = -→*-step (ξ-letwrap₁ e₁-→e₁′) (ξ-letwrap₁* e₁′-→*e₁″)

-- | Values are preserved under substitution, because they don't contain current variables.
Value-substᵈ : ∀ {e : Γ ⊢ A ^ n} {σ : Γ′ ⊩ Γ} {d} (σᵈ : σ ≤ᵈ′ d) → Value e → Value (substᵈ σᵈ e)
Value-substᵈ σᵈ (`λ⟨ Δ ⟩ e) = `λ⟨ Δ ⟩ substᵈ (extsᵈ σᵈ) e
Value-substᵈ σᵈ `true = `true 
Value-substᵈ σᵈ `false = `false
Value-substᵈ σᵈ ⟨ e ⟩ = ⟨ substᵈ (exts↾ᵈ σᵈ) e ⟩
Value-substᵈ σᵈ (`wrap Δ e ve) = `wrap Δ (substᵈ (exts++ᵈ (inject₁ Δ) σᵈ) e) (Value-substᵈ (exts++ᵈ (inject₁ Δ) σᵈ) ve)

Value-subst : ∀ {e : Γ ⊢ A ^ n} (σ : Γ′ ⊩ Γ)  → Value e → Value (subst σ e)
Value-subst σ ve = Value-substᵈ (≤ᵈ′-refl σ) ve