------------------------------------------------------------------------
-- Reduction semantics
------------------------------------------------------------------------

module SimplyTyped.Semantics where

open import SimplyTyped.TypeSystem
open import SimplyTyped.Substitution
open TmSubst
open import Data.Star hiding (_▻_)
open import Level
open import Relation.Binary

-- One-step reduction relation.

infix  _⇾_

data _⇾_ : ∀ {Γ σ} → Rel (Γ ⊢ σ) zero where
  β : ∀ {Γ σ τ} (t₁ : Γ ▻ σ ⊢ τ) t₂ →
      (ƛ t₁) · t₂ ⇾ t₁ [ sub t₂ ]
  η : ∀ {Γ σ τ} (t : Γ ⊢ σ ⟶ τ) →
      t ⇾ ƛ (t [ wk {σ = σ} ]) · var vz

-- Reduction contexts. (Often reduction contexts are defined so that
-- only one reduction is possible in a given term. I have not done so
-- here.)

infixl  _•·_ _·•_
infix   ƛ•_

data RedCtxt (Δ : Ctxt) (χ : Ty) : TmLike where
  •    : RedCtxt Δ χ Δ χ
  ƛ•_  : ∀ {Γ σ τ} → RedCtxt Δ χ (Γ ▻ σ) τ → RedCtxt Δ χ Γ (σ ⟶ τ)
  _•·_ : ∀ {Γ σ τ} → RedCtxt Δ χ Γ (σ ⟶ τ) → Γ ⊢ σ → RedCtxt Δ χ Γ τ
  _·•_ : ∀ {Γ σ τ} → Γ ⊢ σ ⟶ τ → RedCtxt Δ χ Γ σ → RedCtxt Δ χ Γ τ

-- Filling a hole.

infix  _⟨_⟩

_⟨_⟩ : ∀ {Δ χ Γ σ} → RedCtxt Δ χ Γ σ → Δ ⊢ χ → Γ ⊢ σ
•       ⟨ t  ⟩ = t
ƛ• C    ⟨ t  ⟩ = ƛ (C ⟨ t ⟩)
C •· t₂ ⟨ t₁ ⟩ = (C ⟨ t₁ ⟩) · t₂
t₁ ·• C ⟨ t₂ ⟩ = t₁ · (C ⟨ t₂ ⟩)

-- Full one-step reduction relation.

infix  _⇛_

data _⇛_ : ∀ {Γ σ} → Rel (Γ ⊢ σ) zero where
  red : ∀ {Γ σ Δ τ t₁ t₂} (C : RedCtxt Γ σ Δ τ) →
        t₁ ⇾ t₂ → C ⟨ t₁ ⟩ ⇛ C ⟨ t₂ ⟩

-- Reflexive transitive closure.

infix  _⇛⋆_

_⇛⋆_ : ∀ {Γ σ} → Rel (Γ ⊢ σ) zero
_⇛⋆_ = Star _⇛_