{-|
This module defines the denotational semantics of λ○▷,
as described in section 7.1-7.3.
-}

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

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

open import CtxTyp.Context
open import CtxTyp.Term
open import CtxTyp.Substitution

-- | Type interpretation.
⟦_⟧ : Type n → Context (suc n) → Set
⟦ [ Δ ⊢ A ]⇒ B ⟧ Γ = ∀ {Γ′} → Subst Γ Γ′ → ⟦ A ⟧ (Γ′ ++ Δ) → ⟦ B ⟧ Γ′
⟦ Δ ▷ A ⟧ Γ = ⟦ A ⟧ (Γ ++ Δ)
⟦ `Bool ⟧ Γ = Bool
⟦ ◯ A ⟧ Γ = Term (suc _) Γ A

-- | Type interpretation is monotonic in the context.
subst⟦_⟧ : ∀ A → Subst Γ₁ Γ₂ → ⟦ A ⟧ Γ₁ → ⟦ A ⟧ Γ₂
subst⟦ [ Δ ⊢ A ]⇒ B ⟧ σ f = λ σ′ d → f (substSubst σ′ σ) d
subst⟦ Δ ▷ A ⟧ σ d = subst⟦ A ⟧ (exts++ Δ σ) d
subst⟦ `Bool ⟧ σ b = b
subst⟦ ◯ A ⟧ σ e = subst σ e

-- | Context interpretation, i.e. environments.
-- We define it recursively as iterated products instead of using the product type directly.
G⟦_⟧  : Context n → Context (suc n) → Set
Item⟦_⊢_^_⟧ : Context m → Type m → m ≥‴ n → Context (suc n) → Set

G⟦ ∅ ⟧ Γ′ = ⊤
G⟦ Γ ,[ Δ ⊢ A ^ m≥n ] ⟧ Γ′ = G⟦ Γ ⟧ Γ′ × Item⟦ Δ ⊢ A ^ m≥n ⟧ Γ′
G⟦ Γ₁ ++ Γ₂ ⟧ Γ′ = G⟦ Γ₁ ⟧ Γ′ × G⟦ Γ₂ ⟧ Γ′

Item⟦ Δ ⊢ A ^ ≤‴-refl ⟧ Γ′ = ∀ {Γ″} → Subst Γ′ Γ″ → G⟦ Δ ⟧ Γ″ → ⟦ A ⟧ Γ″
Item⟦ Δ ⊢ A ^ ≤‴-step m≥n ⟧ Γ′ = Γ′ ⊩[ Δ ⊢ A ^ m≥n ]

-- | Lookup an item from an environment.
lookupG : G⟦ Γ ⟧ Γ′ → ∀ {m} {Δ} {A} {m≥n : m ≥‴ _} → Γ ∋[ Δ ⊢ A ^ m≥n ] → Item⟦ Δ ⊢ A ^ m≥n ⟧ Γ′
lookupG {Γ = Γ ,[ _ ^ _ ]} γ Z = γ .proj₂
lookupG {Γ = Γ ,[ _ ^ _ ]} γ (S x) = lookupG (γ .proj₁) x
lookupG {Γ = Γ₁ ++ Γ₂} (γ₁ P., γ₂) (L x) = lookupG γ₁ x
lookupG {Γ = Γ₁ ++ Γ₂} (γ₁ P., γ₂) (R x) = lookupG γ₂ x

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

-- | Lift a later-stage substitution to an environment.
liftS : Subst Γ Γ′ → G⟦ inject₁ Γ ⟧ Γ′
liftS ∅ = tt
liftS (σ , item) = liftS σ P., item
liftS (σ₁ ++ˢ σ₂) = liftS σ₁ P., liftS σ₂

-- | Context interpretation is monotonic in the (indexing) context.
substG : Subst Γ₁ Γ₂ → G⟦ Γ ⟧ Γ₁ → G⟦ Γ ⟧ Γ₂
substG {Γ = ∅} σ γ = tt
substG {Γ = Γ ,[ _ ^ ≤‴-refl ]} σ (γ P., f) = substG σ γ P., λ σ′ →  f (substSubst σ′ σ)
substG {Γ = Γ ,[ Δ ⊢ A ^ ≤‴-step m≥n ]} σ (γ P., item) = substG σ γ P., substSubstItem σ item
substG {Γ = Γ₁ ++ Γ₂} σ (γ₁ P., γ₂) = substG σ γ₁ P., substG σ γ₂

-- | Lift a later-stage renaming to an environment.
liftG : Rename Γ Γ′ → G⟦ inject₁ Γ ⟧ Γ′
liftG {Γ = ∅} ρ = tt
liftG {Γ = Γ ,[ _ ^ _ ]} ρ = liftG (ρ ∘ S) P., var (ρ Z)
liftG {Γ = Γ₁ ++ Γ₂} ρ = liftG (ρ ∘ L) P., liftG (ρ ∘ R)

-- | liftG respects equivalence of renamings.
liftG-resp-≗ : ∀ {ρ ρ′ : Rename Γ Γ′} → ρ ≗ ρ′ → liftG ρ ≡ liftG ρ′
liftG-resp-≗ {Γ = ∅} ρ≗ρ′ = refl
liftG-resp-≗ {Γ = Γ ,[ _ ^ _ ]} ρ≗ρ′ = cong₂ P._,_ (liftG-resp-≗ (ρ≗ρ′ ∘ S)) (cong var (ρ≗ρ′ Z))
liftG-resp-≗ {Γ = Γ₁ ++ Γ₂} ρ≗ρ′ = cong₂ P._,_ (liftG-resp-≗ (ρ≗ρ′ ∘ L)) (liftG-resp-≗ (ρ≗ρ′ ∘ R))

-- | Extend an environment with an identity entry at later stage.
extG : G⟦ Γ ⟧ Γ′ → G⟦ Γ ,[ Δ ⊢ A ^ ≤‴-step m≥n ] ⟧ (Γ′ ,[ Δ ⊢ A ^ m≥n ])
extG γ = substG (lift S) γ P., var Z

-- | Extend an environment with multiple identity entries at later stages.
extG++ : ∀ Δ → G⟦ Γ ⟧ Γ′ → G⟦ Γ ++ inject₁ Δ ⟧ (Γ′ ++ Δ)
extG++ Δ γ = substG (lift L) γ P., liftG R

-- | Lift a denotation to an environment entry.
single⟦_⟧ : (A : Type n) → ⟦ A ⟧ (Γ′ ++ Δ) → ∀ {Γ″} → Subst Γ′ Γ″ → G⟦ inject₁ Δ ⟧ Γ″ → ⟦ A ⟧ Γ″
single⟦ A ⟧ d σ γ = subst⟦ A ⟧ (σ ++ˢ renameSubstʳ (∋-↾⁺ ∘ ∋-inject₁⁺) (γ ↾ᴳ)) d

-- | Merge two environments.
_∪_ : G⟦ Γ ⟧ Γ′ → G⟦ Δ ⟧ Γ′ → G⟦ Γ ++ Δ ⟧ Γ′
_∪_ γ₁ γ₂ = γ₁ P., γ₂

-- | 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₂ ⟧ (extG++ _ γ))
E⟦ ⟨ e ⟩ ⟧ γ = subst (γ ↾ᴳ) e
E⟦ `let⟨ Δ ⟩ e₁ e₂ ⟧ γ = let e = E⟦ e₁ ⟧ (extG++ Δ γ) in E⟦ e₂ ⟧ (γ P., term e)
E⟦ `wrap Δ e ⟧ γ = E⟦ e ⟧ (extG++ Δ γ)
E⟦ `letwrap {A = A} Δ e₁ e₂ ⟧ γ = let d = E⟦ e₁ ⟧ γ in E⟦ e₂ ⟧ (γ P., single⟦ A ⟧ d)

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


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

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

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

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

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

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