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

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

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

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 Γ Γ′

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

-- | Multi substitution
_[_]ˢ : Γ ++ Π ⊢ B ^ n → Γ ⊩ Π → Γ ⊢ B ^ n
e [ σ ]ˢ = subst (lift id ++ˢ σ) 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
  β-iflet⟨⟩₁ : {e₂ : Γ ++ inject₁ Π ⊢ B ^ n}
    → match p (rename (ext++ˡ (Γ ↾) (∋-inject₁⁻ ∘ ∋-↾⁻)) e₁) ≡ just σ
    → `iflet⟨ Δ ⟩ p ⟨ e₁ ⟩ e₂ e₃ -→ e₂ [ ⊩-↾⁻ σ ]ˢ -- ^ Rule IfLetQuote1
  β-iflet⟨⟩₂ : {e₂ : Γ ++ inject₁ Π ⊢ B ^ n}
    → match p (rename (ext++ˡ (Γ ↾) (∋-inject₁⁻ ∘ ∋-↾⁻)) e₁) ≡ nothing
    → `iflet⟨ Δ ⟩ p ⟨ e₁ ⟩ e₂ e₃ -→ e₃ -- ^ Rule IfLetQuote2
  β-rewrite⟨⟩⟨⟩ : (`rewrite {Π = Π} ⟨ e₁ ⟩ p ⟨ e₂ ⟩) -→ ⟨ rewriteBottomUp e₁ p (rename (ext++ˡ (Γ ↾) (∋-inject₁⁻ ∘ ∋-↾⁻)) e₂) ⟩ -- ^ Rule RewriteQuoteQuote
  
  ξ-·₁ : 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
  ξ-iflet⟨⟩₁ : e₁ -→ e₁′ → `iflet⟨ Δ ⟩ p e₁ e₂ e₃ -→ `iflet⟨ Δ ⟩ p e₁′ e₂ e₃ -- ^ Rule CongIfLet1
  ξ-rewrite₁ : e₁ -→ e₁′ → `rewrite {B = B} e₁ p e₂ -→ `rewrite e₁′ p e₂ -- ^ Rule CongRewrite1
  ξ-rewrite₂ : Value e₁ → e₂ -→ e₂′ → `rewrite {B = B} e₁ p e₂ -→ `rewrite e₁ p e₂′ -- ^ Rule CongRewrite2

-- | 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 for λ○▷pat.
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₁)
progress {Γ = Γ} (`iflet⟨ Δ ⟩ p e₁ e₂ e₃) with progress e₁
... | p-step e₁-→e₁′ = p-step (ξ-iflet⟨⟩₁ e₁-→e₁′)
... | p-value ⟨ e ⟩ with match p (rename (ext++ˡ (inject₁ Γ ↾) (∋-inject₁⁻ ∘ ∋-↾⁻)) e) in eq
... | just σ = p-step (β-iflet⟨⟩₁ eq)
... | nothing = p-step (β-iflet⟨⟩₂ eq)
progress (`rewrite {Π = Π} e₁ p e₂) with progress e₁
... | p-step e₁-→e₁′ = p-step (ξ-rewrite₁ e₁-→e₁′)
... | p-value ve₁@(⟨ e₁ ⟩) with progress e₂
... | p-step e₂-→e₂′ = p-step (ξ-rewrite₂ ⟨ e₁ ⟩ e₂-→e₂′)
... | p-value ⟨ e₂ ⟩ = p-step β-rewrite⟨⟩⟨⟩