Splice.Translate

{-# OPTIONS --safe #-}
module Splice.Translate where

open import Data.Nat.Base using (ℕ; zero; suc; _≥‴_; ≤‴-refl; ≤‴-step)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; subst)

import Splice.Context as S
import Splice.Term as S
import CtxTyp.Context as C
import CtxTyp.Term as C

variable
  n m n′ m′ n″ m″ : ℕ
  m≥n m′≥n : m ≥‴ n

◯^ : m ≥‴ n → S.Type m → S.Type n
◯^ ≤‴-refl A = A
◯^ (≤‴-step m≥n) A = S.◯ (◯^ m≥n A)

infixr 7 _^_⇛_ _⇛₀_ _⇛₁_

_^_⇛_ : C.Context m → m ≥‴ n → S.Type n → S.Type n
⟦_⟧ᵗ : C.Type n → S.Type n

_⇛₀_ : C.Context n → S.Type n → S.Type n
Δ ⇛₀ A = Δ ^ ≤‴-refl ⇛ A

_⇛₁_ : C.Context (suc n) → S.Type n → S.Type n
Δ ⇛₁ A = _^_⇛_ Δ (≤‴-step ≤‴-refl) A

C.∅ ^ m≥n ⇛ A = A
(Γ C.,[ Δ C.⊢ A′ ^ m′≥m ]) ^ m≥n ⇛ A = _^_⇛_ Γ m≥n (◯^ m≥n (◯^ m′≥m (Δ ⇛₀ ⟦ A′ ⟧ᵗ)) S.⇒ A)

⟦ C.[ Δ ⊢ A ]⇒ B ⟧ᵗ = (Δ ⇛₁ ⟦ A ⟧ᵗ) S.⇒ ⟦ B ⟧ᵗ
⟦ Δ C.▷ A ⟧ᵗ = (Δ ⇛₁ ⟦ A ⟧ᵗ)
⟦ C.`Bool ⟧ᵗ = S.`Bool
⟦ C.◯ A ⟧ᵗ = S.◯ ⟦ A ⟧ᵗ

⟦_⟧ᶜ : C.Context n → S.Context
⟦ C.∅ ⟧ᶜ = S.∅   
⟦ Γ C.,[ Δ C.⊢ A ^ m≥n ] ⟧ᶜ = ⟦ Γ ⟧ᶜ S., (Δ ⇛₀ ⟦ A ⟧ᵗ)

⟦_⟧ˣ : ∀ {Γ} {Δ} {A} {m≥n : m ≥‴ n} → Γ C.∋[ Δ C.⊢ A ^ m≥n ] → ⟦ Γ ⟧ᶜ S.∋ (_^_⇛_ Δ ≤‴-refl ⟦ A ⟧ᵗ) ^ _
⟦ C.Z ⟧ˣ = S.Z
⟦ C.S x ⟧ˣ = S.S ⟦ x ⟧ˣ

inject₁-⇛₀ : ∀ Δ {A : S.Type n} → C.inject₁ Δ ⇛₀ A ≡ Δ ⇛₁ A
inject₁-⇛₀ C.∅ = refl
inject₁-⇛₀ (Δ C.,[ Δ′ C.⊢ A′ ^ m≥n ]) = inject₁-⇛₀ Δ

⟨_⟩^_ : ∀ {Γ} {A} → S.Term m Γ A → (m≥n : m ≥‴ n) → S.Term n Γ (◯^ m≥n A)
⟨ e ⟩^ ≤‴-refl = e
⟨ e ⟩^ ≤‴-step m≥n = S.⟨ ⟨ e ⟩^ m≥n ⟩

$^ : ∀ {Γ} {A} → (m≥n : m ≥‴ n) → S.Term n Γ (◯^ m≥n A) → S.Term m Γ A
$^ ≤‴-refl e = e
$^ (≤‴-step m≥n) e = $^ m≥n (S.$ e)

`λλ : ∀ {Γ} Δ {A} →  S.Term n ⟦ Γ C.++ Δ ⟧ᶜ A → S.Term n ⟦ Γ ⟧ᶜ (Δ ⇛₀ A)
`λλ C.∅ e = e
`λλ (Δ C.,[ Δ₁ C.⊢ A ^ m≥n ]) e =  `λλ Δ (S.`λ S.subst (λ { S.Z → $^ m≥n (S.` S.Z); (S.S x) → S.` S.S x }) e)

`λλ₁ : ∀ {Γ} Δ {A} → S.Term (suc n) ⟦ Γ C.++ C.inject₁ Δ ⟧ᶜ A  → S.Term (suc n) ⟦ Γ ⟧ᶜ (Δ ⇛₀ A) 
`λλ₁ C.∅ e = e
`λλ₁ (Δ C.,[ Δ₁ C.⊢ A ^ m≥n ]) e = `λλ₁ Δ (S.`λ S.subst (λ { S.Z → $^ m≥n (S.` S.Z); (S.S x) → S.` S.S x }) e)

`λλ◯ : ∀ {Γ} Δ {A} → S.Term n ⟦ Γ C.++ C.inject₁ Δ ⟧ᶜ A → S.Term n ⟦ Γ ⟧ᶜ (Δ ⇛₁ A)
`λλ◯ C.∅ e = e
`λλ◯ (Δ C.,[ Δ₁ C.⊢ A ^ m≥n ]) e = `λλ◯ Δ (S.`λ S.subst (λ { S.Z → $^ m≥n (S.$ (S.` S.Z)); (S.S x) → S.` S.S x }) e)

wk↾ : ∀ {Γ : C.Context n} → S.Rename ⟦ Γ C.↾ ⟧ᶜ ⟦ Γ ⟧ᶜ
wk↾ {Γ = Γ C.,[ Δ C.⊢ A ^ ≤‴-refl ]} x = S.S (wk↾ x)
wk↾ {Γ = Γ C.,[ Δ C.⊢ A ^ ≤‴-step m≥n ]} S.Z = S.Z
wk↾ {Γ = Γ C.,[ Δ C.⊢ A ^ ≤‴-step m≥n ]} (S.S x) = S.S (wk↾ x) 

wk↾≥ : ∀ {Γ : C.Context n} → (m≥n : m ≥‴ n) → S.Rename ⟦ Γ C.↾≥ m≥n ⟧ᶜ ⟦ Γ ⟧ᶜ
wk↾≥ ≤‴-refl x = x
wk↾≥ (≤‴-step m≥n) x = wk↾ (wk↾≥ m≥n x)

applyTerm : ∀ {Γ} {Δ} {A} → S.Term n ⟦ Γ ⟧ᶜ (Δ ⇛₀ A) → Γ C.⊩ Δ → S.Term n ⟦ Γ ⟧ᶜ A
⟦_⟧ᵉ : ∀ {Γ} {A} → C.Term n Γ A → S.Term n (⟦ Γ ⟧ᶜ) (⟦ A ⟧ᵗ)

applyTerm e C.∅ = e
applyTerm e (C._,_ {Δ = Δ} {m≥n = m≥n} σ (C.term e′)) = applyTerm e σ S.· ⟨ S.rename (wk↾≥ m≥n) (`λλ Δ ⟦ e′ ⟧ᵉ) ⟩^ m≥n
applyTerm e (C._,_ {m≥n = m≥n} σ (C.var y)) = applyTerm e σ S.· (⟨ S.` ⟦ y ⟧ˣ ⟩^ m≥n)

⟦ C.` x `with σ ⟧ᵉ = applyTerm (S.` ⟦ x ⟧ˣ) σ
⟦ C.`true ⟧ᵉ = S.`true
⟦ C.`false ⟧ᵉ = S.`false
⟦ C.`if e₁ `then e₂ `else e₃ ⟧ᵉ = S.`if ⟦ e₁ ⟧ᵉ `then ⟦ e₂ ⟧ᵉ `else ⟦ e₃ ⟧ᵉ
⟦ C.`λ⟨ Δ ⟩ e ⟧ᵉ = S.`λ subst (λ d → (S.Term _ (_ S., d) _)) (inject₁-⇛₀ Δ) ⟦ e ⟧ᵉ
⟦ e₁ C.· e₂ ⟧ᵉ = ⟦ e₁ ⟧ᵉ  S.· `λλ◯ _ ⟦ e₂ ⟧ᵉ
⟦ C.⟨ e ⟩ ⟧ᵉ = S.⟨ S.rename wk↾ ⟦ e ⟧ᵉ ⟩ 
⟦ C.`let⟨ Δ ⟩ e₁ e₂ ⟧ᵉ =
  S.`let S.⟨ `λλ₁ Δ (S.$ ⟦ e₁ ⟧ᵉ) ⟩ `in          
  S.subst (λ {S.Z → S.$ (S.` S.Z); (S.S x) → S.` S.S x }) ⟦ e₂ ⟧ᵉ 
⟦ C.`wrap Δ e ⟧ᵉ = `λλ◯ Δ ⟦ e ⟧ᵉ 
⟦ C.`letwrap Δ e₁ e₂ ⟧ᵉ = S.`let ⟦ e₁ ⟧ᵉ `in subst (λ ΔA → (S.Term _ (_ S., ΔA) _)) (inject₁-⇛₀ Δ) ⟦ e₂ ⟧ᵉ