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