%include agda.fmt

\subsection{Typing rules}
\label{well-typed}

\AgdaHide{
\begin{code}
module Issue854.WellTyped where

open import Function hiding (_∋_)
open import Data.Fin
open import Data.Product
open import Data.List
open import Data.List.Any as Any
open import Relation.Binary.List.Pointwise

open Membership-≡
open import Issue854.Terms
open import Issue854.Types
open import Issue854.Context as Ctx hiding (Rel; index)

infix 1 _⊢^v_∶_
infix 1 _⊢^c_∶_
infix 1 _⊢^cs_∶_
infixl 3 _·_
\end{code}
}

\begin{code}
mutual

  data _⊢^v_∶_ (Γ : Ctx) : VTerm → VType → Set where

    var : ∀ {V} →  (m : Γ ∋ V) →
                   -----------------------
                   Γ ⊢^v var (toℕ (Ctx.index m)) ∶ V


    con : ∀ {Δ P A p k} →  (m : (P , A) ∈ Δ) → Γ ⊢^v p ∶ P →
                           Γ ▻ A ⊢^v k ∶ μ Δ →
                           -------------------------------
                           Γ ⊢^v con (toℕ (index m)) p ∶ μ Δ

    thunk : ∀ {Σ V c} →  Γ ⊢^c c ∶ Σ ⋆ V →
                         -------------------
                         Γ ⊢^v thunk c ∶ ⁅ Σ ⋆ V ⁆

    ⟨⟩ :  ------------
          Γ ⊢^v ⟨⟩ ∶ 𝟙

    _,_ : ∀ {U V u v} →  Γ ⊢^v u ∶ U → Γ ⊢^v v ∶ V →
                         -------------------------
                         Γ ⊢^v u , v ∶ U ⊗ V

    𝟘-elim : ∀ {V v} →  Γ ⊢^v v ∶ 𝟘 →
                        -------------
                        Γ ⊢^v 𝟘-elim v ∶ V

    ι₁ : ∀ {U V u} →  Γ ⊢^v u ∶ U →
                      -------------
                      Γ ⊢^v ι₁ u ∶ U ⊕ V

    ι₂ : ∀ {U V v} →  Γ ⊢^v v ∶ V →
                      -------------
                      Γ ⊢^v ι₂ v ∶ U ⊕ V

  -- Pointwise version of the computation judgement.
  _⊢^cs_∶_ : Ctx → List CTerm → List CType → Set
  _⊢^cs_∶_ Γ = Rel (_⊢^c_∶_ Γ)

  data _⊢^c_∶_ (Γ : Ctx) : CTerm → CType → Set where

    return : ∀ {Σ V v} →  Γ ⊢^v v ∶ V →
                          -----------
                          Γ ⊢^c return v ∶ Σ ⋆ V

    _to_ : ∀ {Σ Σ′ Σ″ U V c k} →  Γ ⊢^c c ∶ Σ ⋆ U → Γ ▻ U ⊢^c k ∶ Σ′ ⋆ V →
                                  Σ ⊆ Σ″ → Σ′ ⊆ Σ″ →
                                  ---------------------------------
                                  Γ ⊢^c c to k ∶ Σ″ ⋆ V

    force : ∀ {C t} →  Γ ⊢^v t ∶ ⁅ C ⁆ →
                       ----------------
                       Γ ⊢^c force t ∶ C

    let′_be_ : ∀ {V C v k} →  Γ ⊢^v v ∶ V → Γ ▻ V ⊢^c k ∶ C →
                              -----------------------------
                              Γ ⊢^c let′ v be k ∶ C

    ⟨⟩ :  -------------
          Γ ⊢^c ⟨⟩ ∶ ⊤′

    split : ∀ {U V C p k} →  Γ ⊢^v p ∶ U ⊗ V → Γ ▻ U ▻ V ⊢^c k ∶ C →
                             -------------------------------------
                             Γ ⊢^c split p k ∶ C

    π₁ : ∀ {B C p} →  Γ ⊢^c p ∶ B & C →
                      --------------------
                      Γ ⊢^c π₁ p ∶ B

    π₂ : ∀ {B C p} →  Γ ⊢^c p ∶ B & C →
                      --------------------
                      Γ ⊢^c π₂ p ∶ C

    _,_ : ∀ {B C b c} →  Γ ⊢^c b ∶ B → Γ ⊢^c c ∶ C →
                         -------------------------
                         Γ ⊢^c b , c ∶ B & C

    ƛ_ : ∀ {V C b} →  Γ ▻ V ⊢^c b ∶ C →
                      ---------------
                      Γ ⊢^c ƛ b ∶ V ⇒ C

    _·_ : ∀ {V C f a} →  Γ ⊢^c f ∶ V ⇒ C → Γ ⊢^v a ∶ V →
                         -----------------------------
                         Γ ⊢^c f · a ∶ C

    op : ∀ {Σ P A} →  (m : (P , A) ∈ Σ) →
                      -----------------
                      Γ ⊢^c op (toℕ (Any.index m)) ∶ P ⇒ Σ ⋆ A

    iter : ∀ {Δ C φ x} →  Γ ⊢^cs φ ∶ Alg Δ C → Γ ⊢^v x ∶ μ Δ →
                          --------------------------------------
                          Γ ⊢^c iter φ x ∶ C

    run : ∀ {Σ Σ′ Σ″ Σ‴ I U V φ u} →  Γ ⊢^cs φ ∶ PHomo Σ′ U I Σ″ V →
                                      Γ ⊢^c u ∶ Σ ⋆ U → Σ ⊆ (Σ′ ++ Σ″) → Σ″ ⊆ Σ‴ →
                                      ---------------------------------------
                                      Γ ⊢^c run φ u ∶ I ⇒ Σ‴ ⋆ V
\end{code}