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

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

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

open import Core.Context
open import Core.Term
open import Core.Substitution

variable
  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 (Γ , A ^ n) B) → Value (`λ e)
  `true : Value {Γ = Γ} `true
  `false : Value {Γ = Γ} `false
  ⟨_⟩ : (e : Term (suc n) (Γ ↾) A) → Value {Γ = Γ} ⟨ e ⟩

infix  _-→_
data _-→_ : 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₁ ]

  ξ-∙₁ : 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₂

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 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⟨⟩