{-# OPTIONS --without-K --safe #-}

-- Definition of readback functions
--
-- The readback functions read from the domain model back to the syntax as
-- normal/neutral forms. The readback function is tyle-intended value directed and
-- performs η expansion during the process. Combined with evaluation, after reading
-- back, we obtain β-η normal form.
--
-- All readback functions receive a nonempty list of natural numbers. This list
-- contains the length of each context in a context stack and is responsible for
-- maintaining the correspondence between syntactic variables and domain
-- variables. The correspondence is at context level and can be seen in the Rl
-- constructor.
module Mints.Semantics.Readback where

open import Lib
open import Mints.Semantics.Domain
open import Mints.Semantics.Evaluation


instance
  ℕsHasTr : HasTr (List⁺ ℕ)
  ℕsHasTr = record { _∥_ = λ ns n → drop+ n ns }

-- Increment the topmost length, corresponding to entering a closure
inc : List⁺ ℕ → List⁺ ℕ
inc (n ∷ ns) = (suc n ∷ ns)

-- Readback functions
--
-- There are three readback functions:
-- Rf: readback from domain normal forms to syntactic normal forms, performing η expansion as well
-- Re: readback from domain neutral forms to syntactic neutral forms
-- Rty: readback from domain value that is intended to represent types to syntactic normal forms
infix  Rf_-_↘_ Re_-_↘_ Rty_-_↘_

mutual

  data Rf_-_↘_ : List⁺ ℕ → Df → Nf → Set where
    RU  : ∀ {i} ns →
          Rty ns - A ↘ W →
          ---------------------
          Rf ns - ↓ (U i) A ↘ W
    Rze : ∀ ns →
          Rf ns - ↓ N ze ↘ ze
    Rsu : ∀ ns →
          Rf ns - ↓ N a ↘ w →
          ---------------------------
          Rf ns - ↓ N (su a) ↘ (su w)
    RΛ  : ∀ ns →
          a ∙ l′ A (head ns) ↘ b →
          ⟦ T ⟧ ρ ↦ l′ A (head ns) ↘ B →
          Rf inc ns - ↓ B b ↘ w →
          ------------------------------
          Rf ns - ↓ (Π A T ρ) a ↘ Λ w
    R□  : ∀ ns →
          unbox∙  , a ↘ b →
          Rf  ∷⁺ ns - ↓ A b ↘ w →
          -------------------------
          Rf ns - ↓ (□ A) a ↘ box w
    RN  : ∀ ns →
          Re ns - c ↘ u →
          --------------------------
          Rf ns - ↓ N (↑ N c) ↘ ne u
    Rne : ∀ ns →
          Re ns - c′ ↘ u →
          ----------------------------------
          Rf ns - ↓ (↑ A c) (↑ A′ c′) ↘ ne u

  data Re_-_↘_ : List⁺ ℕ → Dn → Ne → Set where
    Rl : ∀ ns x →
         Re ns - l x ↘ v (head ns ∸ x ∸ )
    R$ : ∀ ns →
         Re ns - c ↘ u →
         Rf ns - d ↘ w →
         ---------------------
         Re ns - c $ d ↘ u $ w
    Ru : ∀ ns k →
         Re ns ∥ k - c ↘ u →
         -------------------------
         Re ns - unbox k c ↘ unbox k u
    Rr : ∀ ns →
         -- compute normal form of the motive
         ⟦ T ⟧ ρ ↦ l′ N (head ns) ↘ A →
         Rty inc ns - A ↘ W →
         -- compute normal form of the base case
         ⟦ T ⟧ ρ ↦ ze ↘ A′ →
         Rf ns - ↓ A′ a ↘ w →
         -- compute normal form of the step case
         ⟦ t ⟧ ρ ↦ l′ N (head ns) ↦ l′ A (suc (head ns)) ↘ b →
         ⟦ T ⟧ ρ ↦ su (l′ N (head ns)) ↘ A″ →
         Rf inc (inc ns) - ↓ A″ b ↘ w′ →
         -- compute neutral form of the number
         Re ns - c ↘ u →
         Re ns - rec T a t ρ c ↘ rec W w w′ u

  data Rty_-_↘_ : List⁺ ℕ → D → Nf → Set where
    RU  : ∀ {i} ns →
          Rty ns - U i ↘ Se i
    RN  : ∀ ns →
          Rty ns - N ↘ N
    R□  : ∀ ns →
          Rty  ∷⁺ ns - A ↘ W →
          ---------------------
          Rty ns - □ A ↘ □ W
    RΠ  : ∀ ns →
          Rty ns - A ↘ W →
          ⟦ T ⟧ ρ ↦ l′ A (head ns) ↘ B →
          Rty inc ns - B ↘ W′ →
          ------------------------------
          Rty ns - Π A T ρ ↘ Π W W′
    Rne : ∀ ns →
          Re ns - c ↘ V →
          ---------------------
          Rty ns - ↑ A c ↘ ne V

-- All readback functions are deterministic.
mutual
  Rf-det : ∀ {ns} → Rf ns - d ↘ w → Rf ns - d ↘ w′ → w ≡ w′
  Rf-det (RU _ ↘W) (RU _ ↘W′)   = Rty-det ↘W ↘W′
  Rf-det (Rze _) (Rze _)        = refl
  Rf-det (Rsu _ ↘w) (Rsu _ ↘w′) = cong su (Rf-det ↘w ↘w′)
  Rf-det (RΛ _ ↘a ↘A ↘w) (RΛ _ ↘a′ ↘A′ ↘w′)
    rewrite ap-det ↘a ↘a′
          | ⟦⟧-det ↘A ↘A′       = cong Λ (Rf-det ↘w ↘w′)
  Rf-det (R□ _ ↘a ↘w) (R□ _ ↘a′ ↘w′)
    rewrite unbox-det ↘a ↘a′    = cong box (Rf-det ↘w ↘w′)
  Rf-det (RN _ ↘u) (RN _ ↘u′)   = cong ne (Re-det ↘u ↘u′)
  Rf-det (Rne _ ↘u) (Rne _ ↘u′) = cong ne (Re-det ↘u ↘u′)

  Re-det : ∀ {ns} → Re ns - c ↘ u → Re ns - c ↘ u′ → u ≡ u′
  Re-det (Rl _ x) (Rl _ .x)          = refl
  Re-det (R$ _ ↘c ↘w) (R$ _ ↘c′ ↘w′) = cong₂ _$_ (Re-det ↘c ↘c′) (Rf-det ↘w ↘w′)
  Re-det (Ru _ k ↘c) (Ru _ .k ↘c′)   = cong (unbox k) (Re-det ↘c ↘c′)
  Re-det (Rr _ ↘A ↘W ↘Az ↘w ↘b ↘As ↘w′ ↘c) (Rr _ ↘A′ ↘W′ ↘Az′ ↘w″ ↘b′ ↘As′ ↘w‴ ↘c′)
    rewrite ⟦⟧-det ↘A ↘A′
          | Rty-det ↘W ↘W′
          | ⟦⟧-det ↘Az ↘Az′
          | Rf-det ↘w ↘w″
          | ⟦⟧-det ↘b ↘b′
          | ⟦⟧-det ↘As ↘As′
          | Rf-det ↘w′ ↘w‴
          | Re-det ↘c ↘c′            = refl

  Rty-det : ∀ {ns} → Rty ns - A ↘ W → Rty ns - A ↘ W′ → W ≡ W′
  Rty-det (RU _) (RU _)          = refl
  Rty-det (RN _) (RN _)          = refl
  Rty-det (R□ _ ↘W) (R□ _ ↘W′)   = cong □ (Rty-det ↘W ↘W′)
  Rty-det (RΠ _ ↘W ↘B ↘W′) (RΠ _ ↘W″ ↘B′ ↘W‴)
    rewrite Rty-det ↘W ↘W″
          | ⟦⟧-det ↘B ↘B′
          | Rty-det ↘W′ ↘W‴      = refl
  Rty-det (Rne _ ↘V) (Rne _ ↘V′) = cong ne (Re-det ↘V ↘V′)

-- Normalization by evaluation where an evaluation environment is passed externally
record NbEEnvs ns ρ t T w : Set where
  field
    ⟦t⟧  : D
    ⟦T⟧  : D
    ↘⟦t⟧ : ⟦ t ⟧ ρ ↘ ⟦t⟧
    ↘⟦T⟧ : ⟦ T ⟧ ρ ↘ ⟦T⟧
    ↓⟦t⟧ : Rf ns - ↓ ⟦T⟧ ⟦t⟧ ↘ w

-- Compute an initial global evaluation environment using a context stack
data InitEnvs : Ctxs → Envs → Set where
  base : InitEnvs ([] ∷ []) empty
  s-κ  : InitEnvs Γ ρ →
         ----------------------------
         InitEnvs ([] ∷⁺ Γ) (ext ρ )
  s-∺  : InitEnvs (Ψ ∷ Ψs) ρ →
         ⟦ T ⟧ ρ ↘ A →
         ------------------------------------------
         InitEnvs ((T ∷ Ψ) ∷ Ψs) (ρ ↦ l′ A (len Ψ))

-- Normalization by evaluation
--
-- We will show that if Γ ⊢ t ∶ T, then there must be a normal form w such that NbE Γ t T w
record NbE Γ t T w : Set where
  field
    envs : Envs
    init : InitEnvs Γ envs
    nbe  : NbEEnvs (map len Γ) envs t T w

-- Above definitions are all deterministic
InitEnvs-det : InitEnvs Γ ρ → InitEnvs Γ ρ′ → ρ ≡ ρ′
InitEnvs-det base base                     = refl
InitEnvs-det (s-κ ↘ρ) (s-κ ↘ρ′)            = cong (λ ρ → ext ρ ) (InitEnvs-det ↘ρ ↘ρ′)
InitEnvs-det (s-∺ {Ψ} ↘ρ ↘A) (s-∺ ↘ρ′ ↘A′)
  rewrite InitEnvs-det ↘ρ ↘ρ′ = cong (λ A → _ ↦ l′ A (len Ψ)) (⟦⟧-det ↘A ↘A′)

NbE-det : NbE Γ t T w →
          NbE Γ t T w′ →
          w ≡ w′
NbE-det nbe nbe′
  with nbe | nbe′
... | record { envs = _ ; init = ↘ρ ; nbe = record { ⟦t⟧ = _ ; ⟦T⟧ = _ ; ↘⟦t⟧ = ↘⟦t⟧ ; ↘⟦T⟧ = ↘⟦T⟧ ; ↓⟦t⟧ = ↓⟦t⟧ } }
    | record { envs = _ ; init = ↘ρ′ ; nbe = record { ⟦t⟧ = _ ; ⟦T⟧ = _ ; ↘⟦t⟧ = ↘⟦t⟧′ ; ↘⟦T⟧ = ↘⟦T⟧′ ; ↓⟦t⟧ = ↓⟦t⟧′ } }
    rewrite InitEnvs-det ↘ρ ↘ρ′
          | ⟦⟧-det ↘⟦T⟧ ↘⟦T⟧′
          | ⟦⟧-det ↘⟦t⟧ ↘⟦t⟧′ = Rf-det ↓⟦t⟧ ↓⟦t⟧′