module SF.PHOAS where

open import Agda.Primitive using (_⊔_)

module Prelude where

  infixr  ∃𝑠𝑡
  infixl  _∨_
  infixr  _∷_
  
  data 𝔹 : Set where
    T : 𝔹
    F : 𝔹

  data _∨_ {ℓ₁ ℓ₂} (A : Set ℓ₁) (B : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
    Inl : A → A ∨ B
    Inr : B → A ∨ B

  syntax ∃𝑠𝑡 A (λ x → B) = ∃ x ⦂ A 𝑠𝑡 B
  data ∃𝑠𝑡 {ℓ₁ ℓ₂} (A : Set ℓ₁) (B : A → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
    ⟨∃_,_⟩ : ∀ (x : A) → B x → ∃ x ⦂ A 𝑠𝑡 B x

  data ⟬_⟭ {ℓ} (A : Set ℓ) : Set ℓ where
    [] : ⟬ A ⟭
    _∷_ : A → ⟬ A ⟭ → ⟬ A ⟭

open Prelude

data type : Set where
  _⟨→⟩_ : type → type → type

data exp-phoas (var : type → ⟬ type ⟭ → Set) : ∀ (Γ : ⟬ type ⟭) (τ : type) → Set where
  Var : ∀ {Γ τ}
    (x : var τ Γ)
    → exp-phoas var Γ τ
  ⟨λ⟩ : ∀ {Γ τ₁ τ₂}
    (e : var τ₁ (τ₁ ∷ Γ) → exp-phoas var (τ₁ ∷ Γ) τ₂)
    → exp-phoas var Γ (τ₁ ⟨→⟩ τ₂)
  _⟨⋅⟩_ : ∀ {Γ τ₁ τ₂}
    (e₁ : exp-phoas var Γ (τ₁ ⟨→⟩ τ₂))
    (e₂ : exp-phoas var Γ τ₁)
    → exp-phoas var Γ τ₂

infix  _∈_
data _∈_ {ℓ} {A : Set ℓ} (x : A) : ∀ (xs : ⟬ A ⟭) → Set ℓ where
  Z : ∀ {xs} → x ∈ x ∷ xs
  S : ∀ {x′ xs} → x ∈ xs → x ∈ x′ ∷ xs

infix  _⊢_
data _⊢_ : ∀ (Γ : ⟬ type ⟭) (τ : type) → Set where
  Var : ∀ {Γ τ}
    (x : τ ∈ Γ)
    → Γ ⊢ τ
  ⟨λ⟩ : ∀ {Γ τ₁ τ₂}
    (e : τ₁ ∷ Γ ⊢ τ₂)
    → Γ ⊢ τ₁ ⟨→⟩ τ₂
  _⟨⋅⟩_ : ∀ {Γ τ₁ τ₂}
    (e₁ : Γ ⊢ τ₁ ⟨→⟩ τ₂)
    (e₂ : Γ ⊢ τ₁)
    → Γ ⊢ τ₂

⟦_⟧₁ : ∀ {Γ τ} (e : exp-phoas _∈_ Γ τ) → Γ ⊢ τ
⟦ Var x ⟧₁ = Var x
⟦ ⟨λ⟩ e ⟧₁ = ⟨λ⟩ ⟦ e Z ⟧₁
⟦ e₁ ⟨⋅⟩ e₂ ⟧₁ = ⟦ e₁ ⟧₁ ⟨⋅⟩ ⟦ e₂ ⟧₁

⟦_⟧₂ : ∀ {Γ τ} (e : Γ ⊢ τ) → exp-phoas _∈_ Γ τ
⟦ Var x ⟧₂ = Var x
⟦ ⟨λ⟩ e ⟧₂ = ⟨λ⟩ (λ _ → ⟦ e ⟧₂)
⟦ e₁ ⟨⋅⟩ e₂ ⟧₂ = ⟦ e₁ ⟧₂ ⟨⋅⟩ ⟦ e₂ ⟧₂