{-# OPTIONS --safe #-}
{-# OPTIONS --with-K #-}
module Pat.Reduction where

open import Data.Maybe.Base using (just; nothing)
open import Data.Nat.Base using (ℕ; suc; zero; _≥‴_; ≤‴-refl; ≤‴-step)
open import Function.Base using (id)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym)

open import Pat.Context
open import Pat.Term
open import Pat.Matching
open import Pat.Rewriting
open import Pat.Substitution

variable
  e e₁ e₂ e₃ e′ e₁′ e₂′ e₃′ : Term n Γ A
  p : Pattern n Γ Δ A Π
  σ : Subst Γ Γ′

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

_[_]ˢ : Term n (Γ ++ Π) B → Subst Π Γ → Term n Γ B
e [ σ ]ˢ = subst (lift id ++ˢ σ) 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₂ ]
  β-rewritȩ⟨⟩⟨⟩ : (`rewritȩ {Π = Π} p ⟨ e₁ ⟩ ⟨ e₂ ⟩) -→ ⟨ rewritȩ p (transportContext (++-inject₁-↾ Π) 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₁ ]
  β-iflet⟨⟩₁ : {e₂ : Term n (Γ ++ inject₁ Π) B}
    → match p (transportContext (++-inject₁-↾ Δ) e₁) ≡ just σ
    → `iflet⟨ Δ ⟩ p ⟨ e₁ ⟩ e₂ e₃ -→ e₂ [ ⊩-↾⁻ σ ]ˢ
  β-iflet⟨⟩₂ : {e₂ : Term n (Γ ++ inject₁ Π) B}
    → match p (transportContext (++-inject₁-↾ Δ) e₁) ≡ nothing
    → `iflet⟨ Δ ⟩ p ⟨ 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₂
  ξ-iflet⟨⟩₁ : e₁ -→ e₁′ → `iflet⟨ Δ ⟩ p e₁ e₂ e₃ -→ `iflet⟨ Δ ⟩ p e₁′ e₂ e₃
  ξ-rewritȩ₁ : e₁ -→ e₁′ → `rewritȩ {B = B} p e₁ e₂ -→ `rewritȩ p e₁′ e₂
  ξ-rewritȩ₂ : Value e₁ → e₂ -→ e₂′ → `rewritȩ {B = B} p e₁ e₂ -→ `rewritȩ p 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 σ) with () ← 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₁)
progress (`iflet⟨ Δ ⟩ p e₁ e₂ e₃) with progress' (inject₁-++ Δ) e₁
... | p-step e₁-→e₁′ = p-step (ξ-iflet⟨⟩₁ e₁-→e₁′)
... | p-value ⟨ e ⟩ with match p (transportContext (++-inject₁-↾ Δ) e) in eq
... | just σ = p-step (β-iflet⟨⟩₁ eq)
... | nothing = p-step (β-iflet⟨⟩₂ eq)
progress (`rewritȩ {Π = Π} p e₁ e₂) with progress' (inject₁-++ Π) e₁
... | p-step e₁-→e₁′ = p-step (ξ-rewritȩ₁ e₁-→e₁′)
... | p-value ve₁@(⟨ e₁ ⟩) with progress e₂
... | p-step e₂-→e₂′ = p-step (ξ-rewritȩ₂ ⟨ e₁ ⟩ e₂-→e₂′)
... | p-value ⟨ e₂ ⟩ = p-step β-rewritȩ⟨⟩⟨⟩