erasure.agda

open import prelude

open import core.typ
open import core.uexp
open import core.mexp

module core.erasure where
  mutual
    _⇒□ : ∀ {Γ τ} → (ě : Γ ⊢⇒ τ) → UExp
    (⊢⦇-⦈^ u)                     ⇒□ = ‵⦇-⦈^ u
    ⊢_ {x = x} ∋x                 ⇒□ = ‵ x
    (⊢λ x ∶ τ ∙ ě)                ⇒□ = ‵λ x ∶ τ ∙ (ě ⇒□)
    ⊢ ě₁ ∙ ě₂ [ τ▸ ]              ⇒□ = ‵ (ě₁ ⇒□) ∙ (ě₂ ⇐□)
    ⊢⸨ ě₁ ⸩∙ ě₂ [ τ!▸ ]           ⇒□ = ‵ (ě₁ ⇒□) ∙ (ě₂ ⇐□)
    (⊢ x ← ě₁ ∙ ě₂)               ⇒□ = ‵ x ← (ě₁ ⇒□) ∙ (ě₂ ⇒□)
    (⊢ℕ n)                        ⇒□ = ‵ℕ n
    (⊢ ě₁ + ě₂)                   ⇒□ = ‵ (ě₁ ⇐□) + (ě₂ ⇐□)
    ⊢tt                           ⇒□ = ‵tt
    ⊢ff                           ⇒□ = ‵ff
    ⊢ ě₁ ∙ ě₂ ∙ ě₃ [ τ₁⊓τ₂ ]      ⇒□ = ‵ (ě₁ ⇐□) ∙ (ě₂ ⇒□) ∙ (ě₃ ⇒□)
    ⊢⟦_⟧ {y = y} ∌y               ⇒□ = ‵ y
    ⊢⦉ ě₁ ∙ ě₂ ∙ ě₃ ⦊[ τ₁~̸τ₂ ]    ⇒□ = ‵ (ě₁ ⇐□) ∙ (ě₂ ⇒□) ∙ (ě₃ ⇒□)
    ⊢⟨ ě₁ , ě₂ ⟩                  ⇒□ = ‵⟨ ě₁ ⇒□ , ě₂ ⇒□ ⟩
    ⊢π₁ ě [ τ▸ ]                  ⇒□ = ‵π₁ (ě ⇒□)
    ⊢π₁⸨ ě ⸩[ τ!▸ ]               ⇒□ = ‵π₁ (ě ⇒□)
    ⊢π₂ ě [ τ▸ ]                  ⇒□ = ‵π₂ (ě ⇒□)
    ⊢π₂⸨ ě ⸩[ τ!▸ ]               ⇒□ = ‵π₂ (ě ⇒□)

    _⇐□ : ∀ {Γ τ} → (ě : Γ ⊢⇐ τ) → UExp
    ⊢λ x ∶ τ ∙ ě [ τ₃▸ ∙ τ~τ₁ ]   ⇐□ = ‵λ x ∶ τ ∙ (ě ⇐□)
    ⊢⸨λ x ∶ τ ∙ ě ⸩[ τ′!▸ ]       ⇐□ = ‵λ x ∶ τ ∙ (ě ⇐□)
    ⊢λ x ∶⸨ τ ⸩∙ ě [ τ₃▸ ∙ τ~̸τ₁ ] ⇐□ = ‵λ x ∶ τ ∙ (ě ⇐□)
    (⊢ x ← ě₁ ∙ ě₂)               ⇐□ = ‵ x ← (ě₁ ⇒□) ∙ (ě₂ ⇐□)
    (⊢ ě₁ ∙ ě₂ ∙ ě₃)              ⇐□ = ‵ (ě₁ ⇐□) ∙ (ě₂ ⇐□) ∙ (ě₃ ⇐□)
    ⊢⟨ ě₁ , ě₂ ⟩[ τ▸ ]            ⇐□ = ‵⟨ ě₁ ⇐□ , ě₂ ⇐□ ⟩
    ⊢⸨⟨ ě₁ , ě₂ ⟩⸩[ τ!▸ ]         ⇐□ = ‵⟨ ě₁ ⇐□ , ě₂ ⇐□ ⟩
    ⊢⸨ ě ⸩[ τ~̸τ′ ∙ su ]           ⇐□ = ě ⇒□
    ⊢∙ ě [ τ~τ′ ∙ su ]            ⇐□ = ě ⇒□