{-|
This module defines intrinsically well-staged types and typing contexts for λ○▷
as described in section 3.1.
It also re-exports context operations from the Data.StagedTree module.
-}

{-# OPTIONS --safe #-}
module CtxTyp.Context where

open import Data.Nat using (ℕ; suc; zero; _≥‴_; ≤‴-refl; ≤‴-step)

data Type (n : ℕ) : Set

-- | Context is a StagedForest of Type
open import Data.StagedTree Type renaming (StagedForest to Context; StagedTree to ContextItem) public

variable
  A B A′ B′ : Type n
  Γ Δ Γ′ Δ′ Γ″ Δ″ : Context n
  Γ₁ Γ₂ Γ₃ : Context n
  Δ₁ Δ₂ Δ₃ : Context n
  Δ₁′ Δ₂′ Δ₃′ : Context n

infixl 5 _,_^_
pattern _,_^_ Γ A n = Γ ,[ ∅ {n = n} ⊢ A ^ ≤‴-refl ]

{-|
Intrinsically well-staged types.

Parameters:
  n : ℕ - The stage level of the type.

Constructors:
  [_⊢_]⇒_ - The unhygienic function type.
  _▷_     - The unhygienic value type.
  `Bool   - The boolean type.
  ◯       - The code type.
-}
infixr 7 [_⊢_]⇒_
infixr 8 _▷_
data Type n where
  [_⊢_]⇒_ : (Δ : Context (suc n)) → (A : Type n) → (B : Type n) → Type n
  _▷_ : (Δ : Context (suc n)) → (A : Type n) → Type n
  `Bool : Type n
  ◯ : (A : Type (suc n)) → Type n

infixr 7 _⇒_
pattern _⇒_ A B = [ ∅ ⊢ A ]⇒ B