\begin{code}
{-# OPTIONS --safe --without-K --postfix-projections #-}
module Generic.Simple.Syntax (Ty : Set) where

  open import Data.LTree
  open import Data.LTree.Vector
  open import Data.Product
  open import Data.Unit.Polymorphic
  open import Level
  open import Relation.Unary using (_⊢_)
  open import Relation.Unary.Checked
  open import Relation.Binary.PropositionalEquality hiding ([_])

  infix 1 _=⇒_ _▹_
  infixr 2 _`∧_

  private
    variable
      ℓ t u x y : Level

  record Ctx : Set where
    constructor ctx
    field
      {shape} : LTree
      ty-ctx : Vector Ty shape
  open Ctx public

  []ᶜ : Ctx
  []ᶜ = ctx []

  [_]ᶜ : Ty → Ctx
  [ A ]ᶜ = ctx [ A ]

  _++ᶜ_ : Ctx → Ctx → Ctx
  ctx Γ ++ᶜ ctx Δ = ctx (Γ ++ Δ)
\end{code}

%<*SimplePremises>
\begin{code}
  data Premises : Set where
    ⟨_`⊢_⟩ : (Γ : Ctx) (A : Ty) → Premises
    `⊤ : Premises
    _`∧_ : (p q : Premises) → Premises
\end{code}
%</SimplePremises>

\begin{code}
  record Rule : Set where
    constructor _=⇒_
    field
      premises : Premises
      conclusion : Ty
  open Rule public

  record System : Set₁ where
    constructor _▹_
    field
      Label : Set
      rules : (l : Label) → Rule
  open System public

  Scoped : ∀ ℓ → Set (suc ℓ)
  Scoped ℓ = Ty → Ctx → Set ℓ

  Scope : ∀ {ℓ} → Scoped ℓ → Ctx → Scoped ℓ
  Scope T QΔ A = (_++ᶜ QΔ) ⊢ T A
\end{code}

\begin{code}
  module WithScope (⟦-,_⊢_⟧ : Ctx → Scoped ℓ) where

    ⟦_⟧p : Premises → Ctx → Set ℓ
    ⟦ ⟨ Γ `⊢ A ⟩ ⟧p = ⟦-, Γ ⊢ A ⟧
    ⟦ `⊤ ⟧p = U
    ⟦ p `∧ q ⟧p = ⟦ p ⟧p ∩ ⟦ q ⟧p

    ⟦_⟧r : Rule → Scoped ℓ
    ⟦ ps =⇒ A′ ⟧r A PΓ = A′ ≡ A × ⟦ ps ⟧p PΓ

    ⟦_⟧s : System → Scoped ℓ
    ⟦ L ▹ rs ⟧s A PΓ = Σ[ l ∈ L ] ⟦ rs l ⟧r A PΓ

  ⟦_⟧p : Premises → (Ctx → Scoped ℓ) → (Ctx → Set ℓ)
  ⟦ ps ⟧p Sc = let module W = WithScope Sc in W.⟦ ps ⟧p

  ⟦_⟧r : Rule → (Ctx → Scoped ℓ) → Scoped ℓ
  ⟦ r ⟧r Sc = let module W = WithScope Sc in W.⟦ r ⟧r

  ⟦_⟧s : System → (Ctx → Scoped ℓ) → Scoped ℓ
  ⟦ s ⟧s Sc = let module W = WithScope Sc in W.⟦ s ⟧s
\end{code}

\begin{code}
  module _ {Γ Δ : Ctx} {X : Ctx → Scoped x} {Y : Ctx → Scoped y} where

    map-p : (ps : Premises) →
            (∀ {Θ A} → X Θ A Γ → Y Θ A Δ) →
            (⟦ ps ⟧p X Γ → ⟦ ps ⟧p Y Δ)
    map-p ⟨ Γ `⊢ A ⟩ f t = f t
    map-p `⊤ f _ = _
    map-p (ps `∧ qs) f (s , t) = map-p ps f s , map-p qs f t

    map-r : (r : Rule) →
            (∀ {Θ A} → X Θ A Γ → Y Θ A Δ) →
            (∀ {A} → ⟦ r ⟧r X A Γ → ⟦ r ⟧r Y A Δ)
    map-r (ps =⇒ A) f (q , t) = q , map-p ps f t

    map-s : (s : System) →
            (∀ {Θ A} → X Θ A Γ → Y Θ A Δ) →
            (∀ {A} → ⟦ s ⟧s X A Γ → ⟦ s ⟧s Y A Δ)
    map-s (L ▹ rs) f (l , t) = l , map-r (rs l) f t
\end{code}
