{-# OPTIONS --safe #-}
module Core.Denotational where

open import Data.Bool.Base using (Bool; true; false; if_then_else_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat.Base using (ℕ; suc; zero; _≥‴_; ≤‴-refl; ≤‴-step)
open import Data.Product.Base as P using (_×_; proj₁; proj₂)
open import Data.Unit.Base using (⊤; tt)
open import Data.Sum.Base as S using (_⊎_; inj₁; inj₂)
open import Function.Base using (id; _∘_; case_of_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; sym)

open import Core.Context
open import Core.Term
open import Core.Depth
open import Core.Substitution

-- Interpretation of Types, indexed by a later-stage context
⟦_⟧ : Type → Context (suc n) → Set
⟦ A ⇒ B ⟧ Γ = ∀ {Γ′} → Subst Γ Γ′ → ⟦ A ⟧ Γ′ → ⟦ B ⟧ Γ′
⟦ `Bool ⟧ Γ = Bool
⟦ ◯ A ⟧ Γ = Term (suc _) Γ A

-- The Kripkean interpretation of the function type allows us to substitute by a later-stage substitution
subst⟦_⟧ : ∀ A → Subst Γ₁ Γ₂ → ⟦ A ⟧ Γ₁ → ⟦ A ⟧ Γ₂
subst⟦ A ⇒ B ⟧ σ f = λ σ′ d → f (substSubst σ′ σ) d
subst⟦ `Bool ⟧ σ b = b
subst⟦ ◯ A ⟧ σ e = subst σ e

-- Interpretation of Contexts i.e. Environments, again indexed by a later-stage context
G⟦_⟧  : Context n → Context (suc n) → Set
G⟦ ∅ ⟧ Γ′ = ⊤
G⟦ Γ ,[ Δ ⊢ A ^ m≥n ] ⟧ Γ′ = G⟦ Γ ⟧ Γ′ × (case m≥n of λ {
    ≤‴-refl → ∀ {Γ″} → Subst Γ′ Γ″ → G⟦ Δ ⟧ Γ″ → ⟦ A ⟧ Γ″;
    (≤‴-step m≥sn) → Γ′ ⊩[ Δ ⊢ A ^ m≥sn ]
  })

lookupG : G⟦ Γ ⟧ Γ′ → ∀ {Δ} {A} → Γ ∋[ Δ ⊢ A ^ ≤‴-refl ] →  ∀ {Γ″} → Subst Γ′ Γ″ → G⟦ Δ ⟧ Γ″ → ⟦ A ⟧ Γ″
lookupG {Γ = Γ ,[ _ ^ _ ]} γ Z = γ .proj₂
lookupG {Γ = Γ ,[ _ ^ _ ]} γ (S x) = lookupG (γ .proj₁) x

_↾ᴳ : G⟦ Γ ⟧ Γ′ → Subst (Γ ↾) Γ′
_↾ᴳ {Γ = ∅} tt = ∅
_↾ᴳ {Γ = Γ ,[ Δ ⊢ A ^ ≤‴-refl ]} γ = γ .proj₁ ↾ᴳ
_↾ᴳ {Γ = Γ ,[ Δ ⊢ A ^ ≤‴-step m≥n ]} γ = (γ .proj₁ ↾ᴳ) , γ .proj₂

liftS : Subst Γ Γ′ → G⟦ inject₁ Γ ⟧ Γ′
liftS ∅ = tt
liftS (σ , item) = liftS σ P., item

-- The Kripkean arrow allows environments to be substituted
substG : Subst Γ₁ Γ₂ → G⟦ Γ ⟧ Γ₁ → G⟦ Γ ⟧ Γ₂
substG {Γ = ∅} σ γ = tt
substG {Γ = Γ ,[ _ ^ ≤‴-refl ]} σ (γ P., f) = substG σ γ P., λ σ′ →  f (substSubst σ′ σ)
substG {Γ = Γ ,[ Δ ⊢ A ^ ≤‴-step m≥n ]} σ (γ P., term e) = substG σ γ P., term (subst (exts++ Δ (exts↾≥ m≥n σ)) e)
substG {Γ = Γ ,[ Δ ⊢ A ^ ≤‴-step m≥n ]} σ (γ P., var x) = substG σ γ P., lookup σ x

extG : G⟦ Γ ⟧ Γ′ → G⟦ Γ ,[ Δ ⊢ A ^ ≤‴-step m≥n ] ⟧ (Γ′ ,[ Δ ⊢ A ^ m≥n ])
extG γ = substG (lift S) γ P., var Z

extG++ : ∀ Δ → G⟦ Γ ⟧ Γ′ → G⟦ Γ ++ inject₁ Δ ⟧ (Γ′ ++ Δ)
extG++ ∅ γ = γ
extG++ (Δ ,[ _ ⊢ _ ^ _ ]) γ = extG (extG++ Δ γ)

⊩-castʳ : Δ ≡ Δ′ → Γ ⊩ Δ → Γ ⊩ Δ′
⊩-castʳ refl = id

liftG : Rename Γ Γ′ → G⟦ inject₁ Γ ⟧ Γ′
liftG {Γ = ∅} ρ = tt
liftG {Γ = Γ ,[ _ ^ _ ]} ρ = liftG (ρ ∘ S) P., var (ρ Z)

single⟦_⟧ : (A : Type) → ⟦ A ⟧ (Γ′ ++ Δ) → ∀ {Γ″} → Subst Γ′ Γ″ → G⟦ inject₁ Δ ⟧ Γ″ → ⟦ A ⟧ Γ″
single⟦ A ⟧ d σ γ = subst⟦ A ⟧ (σ ++ˢ ⊩-castʳ (inject₁-↾ _) (γ ↾ᴳ)) d

_∪_ : G⟦ Γ ⟧ Γ′ → G⟦ Δ ⟧ Γ′ → G⟦ Γ ++ Δ ⟧ Γ′
_∪_ {Δ = ∅} γ₁ γ₂ = γ₁
_∪_ {Δ = Δ ,[ Δ′ ⊢ A ^ m≥n ]} γ₁ γ₂ = (γ₁ ∪ γ₂ .proj₁) P., γ₂ .proj₂

-- Interpretation of Expressions and Substitutions
E⟦_⟧ : Term n Γ A → G⟦ Γ ⟧ Γ′ → ⟦ A ⟧ Γ′
S⟦_⟧ : Subst Δ Γ → G⟦ Γ ⟧ Γ′ → G⟦ Δ ⟧ Γ′

E⟦ ` x `with σ ⟧ γ = (lookupG γ x) (lift id) (S⟦ σ ⟧ γ)
E⟦ `true ⟧ γ = true
E⟦ `false ⟧ γ = false
E⟦ `if e₁ `then e₂ `else e₃ ⟧ γ = if E⟦ e₁ ⟧ γ then E⟦ e₂ ⟧ γ else E⟦ e₃ ⟧ γ
E⟦ `λ_ {A = A} e₁ ⟧ γ = λ σ d → E⟦ e₁ ⟧ (substG σ γ P., single⟦ A ⟧ d)
E⟦ e₁ · e₂ ⟧ γ = E⟦ e₁ ⟧ γ (lift id) (E⟦ e₂ ⟧ γ)
E⟦ ⟨ e ⟩ ⟧ γ = subst (γ ↾ᴳ) e
E⟦ `let⟨ Δ ⟩ e₁ e₂ ⟧ γ = let e = E⟦ e₁ ⟧ (extG++ Δ γ) in E⟦ e₂ ⟧ (γ P., term e)

S⟦ ∅ ⟧ γ = tt
S⟦ _,_ {m≥n = ≤‴-refl} σ (term e) ⟧ γ = S⟦ σ ⟧ γ P., λ σ′ γ′ → E⟦ e ⟧ ((substG σ′ γ) ∪ γ′)
S⟦ _,_ {m≥n = ≤‴-refl} σ (var x) ⟧ γ = S⟦ σ ⟧ γ P., lookupG γ x
S⟦ _,_ {m≥n = ≤‴-step m≥sn} σ (term e) ⟧ γ = S⟦ σ ⟧ γ P., term (subst (exts++ _ (exts↾≥ m≥sn (γ ↾ᴳ))) e)
S⟦ _,_ {m≥n = ≤‴-step m≥sn} σ (var x) ⟧ γ = S⟦ σ ⟧ γ P., lookup (γ ↾ᴳ) (∋-↾⁺ x)

-- Evaluation under a later-stage context
eval : Term n (inject₁ Γ) A → ⟦ A ⟧ Γ
eval e = E⟦ e ⟧ (liftG id)

-- Some tests from the Examples module
test₁ : eval {n = 0} {Γ = ∅} (`if `true `then `true `else `false) ≡ true
test₁ = refl

test₂ : eval {n = 0} {Γ = ∅} (`let⟨ ∅ ⟩ ⟨ `true ⟩ ⟨ `if (` Z `with ∅) `then `true `else `false ⟩) ≡ (`if `true `then `true `else `false)
test₂ = refl

test₃ : eval {n = 0} {Γ = ∅} (`let⟨ ∅ ,[ (∅ , `Bool ^ 1) ⊢ `Bool ^ ≤‴-refl ] ⟩ (`let⟨  ∅ ⟩ ⟨ `true ⟩ ⟨ ` S Z `with (∅ , var Z) ⟩) ⟨ `true ⟩) ≡ (`true)
test₃ = refl

test₄ :  eval {n = 0} {Γ = ∅} (`let⟨ ∅ ,[ (∅ , `Bool ^ 1) ⊢ `Bool ^ ≤‴-refl ] ⟩ (`let⟨ ∅ ⟩ ⟨ `true ⟩ ⟨ ` S Z `with (∅ , var Z) ⟩) (`let⟨ ∅ , `Bool ^ 1 ⟩ ⟨ `if ` Z `with ∅ `then `true `else `false ⟩ (`let⟨ ∅ ⟩ ⟨ `false ⟩ ⟨ ` S (S Z) `with (∅ , var (S Z))⟩))) ≡ (`if `true `then `true `else `false)
test₄ = refl

test₅ : eval {n = 0} {Γ = ∅} (`let⟨ ∅ , `Bool ^ 1 ⟩ ⟨ `if (` Z `with ∅) `then `true `else `false ⟩ (`let⟨ ∅ ⟩ ⟨ `true ⟩ ⟨ ` S Z `with (∅ , var Z)  ⟩)) ≡ (`if `true `then `true `else `false)
test₅ = refl