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

open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym)
open import Data.Empty using (⊥; ⊥-elim)
open import Function.Base using (id; _∘_)

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

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

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

transportContext : Γ ≡ Γ′ → Term n Γ A → Term n Γ′ A
transportContext refl e = e

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

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

infix  _-→_
data _-→_ {n} {Γ : Context n} : Term n Γ A → Term n Γ A → Set where
  β-λ⟨⟩· : Value e₂ → (`λ⟨ Δ ⟩ e₁) · e₂ -→ e₁ [ e₂ ]
  β-if-true : `if `true `then e₂ `else e₃ -→ e₂
  β-if-false : `if `false `then e₂ `else e₃ -→ e₃
  β-let⟨⟩ : {e₂ : Term n (Γ ,[ Δ ⊢ A ^ ≤‴-step ≤‴-refl ]) B} → `let⟨ Δ ⟩ (⟨ e₁ ⟩) e₂ -→ e₂ [ transportContext (++-inject₁-↾ Δ) e₁ ]
  β-letwrap : (Value (`wrap Δ e₁)) → `letwrap Δ (`wrap Δ e₁) e₂ -→ e₂ [ e₁ ]

  ξ-∙₁ : e₁ -→ e₁′ → e₁ · e₂ -→ e₁′ · e₂
  ξ-∙₂ : Value e₁ → e₂ -→ e₂′ → e₁ · e₂ -→ e₁ · e₂′
  ξ-if₁ : e₁ -→ e₁′ → `if e₁ `then e₂ `else e₃ -→ `if e₁′ `then e₂ `else e₃
  ξ-let⟨⟩₁ : e₁ -→ e₁′ → `let⟨ Δ ⟩ e₁ e₂ -→ `let⟨ Δ ⟩ e₁′ e₂
  ξ-wrap : e -→ e′ → `wrap Δ e -→ `wrap Δ e′
  ξ-letwrap₁ : e₁ -→ e₁′ → `letwrap Δ e₁ e₂ -→ `letwrap Δ e₁′ e₂

data Progress : Term n Γ A → Set where
  p-step : e -→ e′ → Progress e
  p-value : Value e → Progress e

progress : (e : Term n (inject₁ Γ) A) → Progress e

progress' : inject₁ Γ′ ≡ Γ → (e : Term n Γ A) → Progress e
progress' refl = progress

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' (inject₁-++ Δ) 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' (inject₁-++ Δ) e₁
... | p-step e₁-→e₁′ = p-step (ξ-let⟨⟩₁ e₁-→e₁′)
... | p-value ⟨ e ⟩ = p-step β-let⟨⟩
progress (`wrap Δ e) with progress' (inject₁-++ Δ) 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₁)

infix  _-→*_
data _-→*_ {n} {Γ : Context n} : Term n Γ A → Term n Γ A → Set where
  -→*-refl : e -→* e
  -→*-step : e -→ e′ → e′ -→* e″ → e -→* e″

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