-------------------------------------------------------------------------------
-- Normalization by Evaluation
-------------------------------------------------------------------------------

module NBE where
  open import Data.Function
    using (_∘_)

  open import Ctx
  open import Modalities
  open import Model
  open import Subsumption
  open import Syntax
  open import Vars
  open import Weaken

-------------------------------------------------------------------------------
-- Abbreviations

  -- The following type aliases are intended to make the logical
  -- structure of the nbe algorithm more apparent from the type
  -- signatures.
  _⊩*_ = Env
  _⊧_  = Models
  _↑_  = Neu
  _↓_  = Nrm
  _⊢_  = Term
  _∋_  = Var {Type}
  _⊩_  = Val

-------------------------------------------------------------------------------
-- Soundness (Easy Part)

  -- The meaning function can be viewed as the computational content
  -- of the soundness theorem for deduction in intuitionistic
  -- propositional logic with respect to entailment in a Kripke model.
  soundness : ∀ {Γ α} → Γ ⊢ α → Γ ⊧ α
  soundness (var x)   ρ = lookup ρ x
  soundness (ƛ e)     ρ = λ Σ⊇Δ v → soundness e (wknEnv* Σ⊇Δ ρ ▸ v)
  soundness (e₁ · e₂) ρ = (soundness e₁ ρ) ⊇-refl (soundness e₂ ρ)

-------------------------------------------------------------------------------
-- Completeness (Hard Part)

  mutual
    -- Quote (reify) a semantic value in the Kripke model to a normal
    -- form.
    ⌜_⌝ : ∀ {Γ α} → Γ ⊩ α → Γ ↓ α
    ⌜_⌝ {α = ●}     x = neu x
    ⌜_⌝ {α = α ⇒ β} f = ƛ ⌜ f ▸-step ⌞ var vz ⌟ ⌝

    -- Unquote (reflect) a neutral form to a semantic value in the
    -- Kripke model.
    ⌞_⌟ : ∀ {Γ α} → Γ ↑ α → Γ ⊩ α
    ⌞_⌟ {α = ●}     x = x
    ⌞_⌟ {α = α ⇒ β} f = λ Δ⊇Γ x → ⌞ wknNeu* Δ⊇Γ f · ⌜ x ⌝ ⌟

  -- Convert a variable to a value in the model.
  varToVal : ∀ {Γ α} → Γ ∋ α → Γ ⊩ α
  varToVal {α = ●}     x = var x
  varToVal {α = α ⇒ β} f = λ Δ⊇Γ x → ⌞ var (lookup Δ⊇Γ f) · ⌜ x ⌝ ⌟

  -- The identity environment.
  idEnv : ∀ {Γ} → Γ ⊩* Γ
  idEnv = tabulate varToVal

  -- The inverse of the meaning function can be viewed as the
  -- computational content of the completeness theorem for deduction
  -- in intuitionistic propositional logic with respect to entailment
  -- in a Kripke model.
  completeness : ∀ {Γ α} → Γ ⊧ α → Γ ⊢ α
  completeness v = termOfNrm ⌜ v idEnv ⌝

-------------------------------------------------------------------------------
-- Normalization by Evaluation (a.k.a. Reduction-free normalization)

  -- Normalization by evaluation, i.e., reduction-free normalization.
  -- Maps a term to its meaning in the Kripke model then quotes the
  -- meaning into a canonical (β-normal, η-long) term.
  nbe : ∀ {Γ α} → Γ ⊢ α → Γ ⊢ α
  nbe = completeness ∘ soundness