{-|
This module defines the translation from λ◯▷ to λ○,
as described in section 5.1
-}

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

open import Data.Nat using (ℕ; zero; suc; _≥‴_; ≤‴-refl; ≤‴-step)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; cong) renaming (subst to cast)
open import Function using (_∘_)

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

-- | Given an m ≥ n witness, apply ◯ to a type by m - n times.
◯^ : m ≥‴ n → S.Type m → S.Type n
◯^ ≤‴-refl A = A
◯^ (≤‴-step m≥n) A = S.◯ (◯^ m≥n A)

infixr  _^_↘_ _↘₀_ _↘₁_
-- | Dependency translation. The middle argument is a witness for m ≥‴ n.
_^_↘_ : C.Context m → m ≥‴ n → S.Type n → S.Type n
-- | Type translation.
⟦_⟧ᵗ : C.Type n → S.Type n

-- | _^_↘_ where the middle argument is ≤‴-refl.
_↘₀_ : C.Context n → S.Type n → S.Type n
Δ ↘₀ A = Δ ^ ≤‴-refl ↘ A

-- | _^_↘_ where the middle argument is ≤‴-step m≥n.
_↘₁_ : 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.++ Γ₂) ^ m≥n ↘ A = Γ₁ ^ m≥n ↘ (Γ₂ ^ m≥n ↘ A)

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

-- | Δ ↘₁ A is equivalent to (inject₁ Δ) ↘₀ A, though not definitionally.
-- We define them in terms of _^_↘_ to avoid termination issues.
inject₁-↘₀ : ∀ Δ {A : S.Type n} → C.inject₁ Δ ↘₀ A ≡ Δ ↘₁ A
inject₁-↘₀ C.∅ = refl
inject₁-↘₀ (Δ C.,[ Δ′ C.⊢ A′ ^ m≥n ]) = inject₁-↘₀ Δ
inject₁-↘₀ (Δ₁ C.++ Δ₂) = trans (inject₁-↘₀ Δ₁) (cong (Δ₁ ↘₁_) (inject₁-↘₀ Δ₂))

-- | Context translation.
⟦_⟧ᶜ : C.Context n → S.Context
⟦ C.∅ ⟧ᶜ = S.∅   
⟦ Γ C.,[ Δ C.⊢ A ^ m≥n ] ⟧ᶜ = ⟦ Γ ⟧ᶜ S., (Δ ↘₀ ⟦ A ⟧ᵗ)
⟦ Γ₁ C.++ Γ₂ ⟧ᶜ = ⟦ Γ₁ ⟧ᶜ S.++ ⟦ Γ₂ ⟧ᶜ

-- | Variable translation.
⟦_⟧ˣ : ∀ {Γ} {Δ} {A} {m≥n : m ≥‴ n} → Γ C.∋[ Δ C.⊢ A ^ m≥n ] → ⟦ Γ ⟧ᶜ S.∋ (Δ ↘₀ ⟦ A ⟧ᵗ) ^ m
⟦ C.Z ⟧ˣ = S.Z
⟦ C.S x ⟧ˣ = S.S ⟦ x ⟧ˣ
⟦ C.L x ⟧ˣ = S.L ⟦ x ⟧ˣ
⟦ C.R x ⟧ˣ = S.R ⟦ x ⟧ˣ

-- | Quoting a term by m - n times.
⟨_⟩^_ : ∀ {Γ} {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 ⟩

-- | Splicing a term by m - n times.
$^ : ∀ {Γ} {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)

-- | Dependency abstraction.
𝝀 : ∀ {Γ} Δ {A} → S.Term n ⟦ Γ C.++ Δ ⟧ᶜ A → S.Term n ⟦ Γ ⟧ᶜ (Δ ↘₀ A)
𝝀 C.∅ e = S.rename (λ { (S.L x) → x }) e
𝝀 (Δ C.,[ Δ₁ C.⊢ A ^ m≥n ]) e = 𝝀 Δ (S.`λ S.subst ((λ { S.Z → $^ m≥n (S.` S.Z); (S.S x) → S.` (S.S x) }) ∘ S.∋-++-,⁻¹) e)
𝝀 (Δ₁ C.++ Δ₂) e = 𝝀 Δ₁ (𝝀 Δ₂ (S.rename S.∋-++-++⁻¹ e))

-- | Dependency abstraction, followed by some casting.
𝝀′ : ∀ {Γ} Δ {A} → S.Term n ⟦ Γ C.++ C.inject₁ Δ ⟧ᶜ A → S.Term n ⟦ Γ ⟧ᶜ (Δ ↘₁ A)
𝝀′ {n = n} {Γ = Γ} Δ e = cast (S.Term n ⟦ Γ ⟧ᶜ) (inject₁-↘₀ Δ) (𝝀 (C.inject₁ Δ) e)

-- | Dependency abstraction with different types than 𝝀..
-- Note that the definition is exactly the same as 𝝀, so they represent the same operation on terms.
𝝀″ : ∀ {Γ} Δ {A} → S.Term (suc n) ⟦ Γ C.++ C.inject₁ Δ ⟧ᶜ A  → S.Term (suc n) ⟦ Γ ⟧ᶜ (Δ ↘₀ A)
𝝀″ C.∅ e = S.rename (λ { (S.L x) → x }) e
𝝀″ (Δ C.,[ Δ₁ C.⊢ A ^ m≥n ]) e = 𝝀″ Δ (S.`λ S.subst ((λ { S.Z → $^ m≥n (S.` S.Z); (S.S x) → S.` (S.S x) }) ∘ S.∋-++-,⁻¹) e)
𝝀″ (Δ₁ C.++ Δ₂) e = 𝝀″ Δ₁ (𝝀″ Δ₂ (S.rename S.∋-++-++⁻¹ e))

-- | Restrition (↾) of a context is a subset of the original context.
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.++ Γ₁} (S.L x) = S.L (wk↾ x)
wk↾ {Γ = Γ C.++ Γ₁} (S.R x) = S.R (wk↾ x)

-- | Restrition (↾≥) of a context is a subset of the original context.
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)

-- | Dependency application.
_•_ : ∀ {Γ} {Δ} {A} → S.Term n ⟦ Γ ⟧ᶜ (Δ ↘₀ A) → Γ C.⊩ Δ → S.Term n ⟦ Γ ⟧ᶜ A
-- | Expression translation.
⟦_⟧ᵉ : ∀ {Γ} {A} → C.Term n Γ A → S.Term n (⟦ Γ ⟧ᶜ) (⟦ A ⟧ᵗ)

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

⟦ C.` x `with σ ⟧ᵉ = (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.`λ cast (λ 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 cast (λ ΔA → (S.Term _ (_ S., ΔA) _)) (inject₁-↘₀ Δ) ⟦ e₂ ⟧ᵉ