module A201607.BasicIS4.Metatheory.Hilbert-TarskiClosedOvergluedHilbert where

open import A201607.BasicIS4.Syntax.Hilbert public
open import A201607.BasicIS4.Semantics.TarskiClosedOvergluedHilbert public


-- Internalisation of syntax as syntax representation in a particular model, for closed terms only.

module _ {{_ : Model}} where
  [_]₀ : ∀ {A} → ∅ ⊢ A → [⊢] A
  [ var () ]₀
  [ app t u ]₀ = [app] [ t ]₀ [ u ]₀
  [ ci ]₀      = [ci]
  [ ck ]₀      = [ck]
  [ cs ]₀      = [cs]
  [ box t ]₀   = [box] [ t ]₀
  [ cdist ]₀   = [cdist]
  [ cup ]₀     = [cup]
  [ cdown ]₀   = [cdown]
  [ cpair ]₀   = [cpair]
  [ cfst ]₀    = [cfst]
  [ csnd ]₀    = [csnd]
  [ unit ]₀    = [unit]


-- Soundness with respect to all models, or evaluation.

eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
eval (var i)   γ = lookup i γ
eval (app t u) γ = eval t γ ⟪$⟫ eval u γ
eval ci        γ = [ci] ⅋ I
eval ck        γ = [ck] ⅋ ⟪K⟫
eval cs        γ = [cs] ⅋ ⟪S⟫′
eval (box t)   γ = [ box t ]₀ ⅋ eval t ∙
eval cdist     γ = [cdist] ⅋ _⟪D⟫′_
eval cup       γ = [cup] ⅋ ⟪↑⟫
eval cdown     γ = [cdown] ⅋ ⟪↓⟫
eval cpair     γ = [cpair] ⅋ _⟪,⟫′_
eval cfst      γ = [cfst] ⅋ π₁
eval csnd      γ = [csnd] ⅋ π₂
eval unit      γ = ∙


-- Correctness of evaluation with respect to conversion.

eval✓ : ∀ {{_ : Model}} {A Γ} {t t′ : Γ ⊢ A} → t ⋙ t′ → eval t ≡ eval t′
eval✓ refl⋙                   = refl
eval✓ (trans⋙ p q)            = trans (eval✓ p) (eval✓ q)
eval✓ (sym⋙ p)                = sym (eval✓ p)
eval✓ (congapp⋙ p q)          = cong² _⟦$⟧_ (eval✓ p) (eval✓ q)
eval✓ (congi⋙ p)              = cong I (eval✓ p)
eval✓ (congk⋙ p q)            = cong² K (eval✓ p) (eval✓ q)
eval✓ (congs⋙ p q r)          = cong³ ⟦S⟧ (eval✓ p) (eval✓ q) (eval✓ r)
eval✓ (congdist⋙ p q)         = cong² _⟦D⟧_ (eval✓ p) (eval✓ q)
eval✓ (congup⋙ p)             = cong ⟦↑⟧ (eval✓ p)
eval✓ (congdown⋙ p)           = cong ⟦↓⟧ (eval✓ p)
eval✓ (congpair⋙ {A} {B} p q) = cong² (_⟦,⟧_ {A} {B}) (eval✓ p) (eval✓ q)
eval✓ (congfst⋙ {A} {B} p)    = cong (⟦π₁⟧ {A} {B}) (eval✓ p)
eval✓ (congsnd⋙ {A} {B} p)    = cong (⟦π₂⟧ {A} {B}) (eval✓ p)
eval✓ beta▻ₖ⋙                 = refl
eval✓ beta▻ₛ⋙                 = refl
eval✓ beta∧₁⋙                 = refl
eval✓ beta∧₂⋙                 = refl
eval✓ eta∧⋙                   = refl
eval✓ eta⊤⋙                  = refl


-- The canonical model.

private
  instance
    canon : Model
    canon = record
      { ⊩ᵅ_    = λ P → ∅ ⊢ α P
      ; [⊢]_   = ∅ ⊢_
      ; [app]   = app
      ; [ci]    = ci
      ; [ck]    = ck
      ; [cs]    = cs
      ; [box]   = box
      ; [cdist] = cdist
      ; [cup]   = cup
      ; [cdown] = cdown
      ; [cpair] = cpair
      ; [cfst]  = cfst
      ; [csnd]  = csnd
      ; [unit]  = unit
      }


-- Completeness with respect to all models, or quotation, for closed terms only.

quot₀ : ∀ {A} → ∅ ⊨ A → ∅ ⊢ A
quot₀ t = reifyʳ (t ∙)


-- Normalisation by evaluation, for closed terms only.

norm₀ : ∀ {A} → ∅ ⊢ A → ∅ ⊢ A
norm₀ = quot₀ ∘ eval


-- TODO: Correctness of normalisation with respect to conversion.