\begin{code}
{-# OPTIONS --safe --without-K --prop #-}

module Generic.Linear.Syntax (Ty Ann : Set) where

  open import Data.Bool.Base
  open import Data.LTree
  open import Data.LTree.Vector
  open import Data.Product using (_×_; _,_)
  open import Data.Unit.Polymorphic using (⊤; tt)
  open import Level
  open import Function.Base using (_∘_; _⟨_⟩_)
  open import Relation.Unary
  open import Relation.Unary.Bunched using (BoxFlags; boxFlags)

  open import Generic.Linear.Syntax.Core public

  infix 25 _++ᶜ_

  record SizedCtx (s : LTree) : Set where
    constructor sctx
    field
      use-ctx : Vector Ann s
      ty-ctx : Vector Ty s

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

    ctx→sctx : SizedCtx shape
    ctx→sctx = sctx use-ctx ty-ctx
  open Ctx public

  sctx→ctx : ∀ {s} → SizedCtx s → Ctx
  sctx→ctx (sctx P γ) = ctx P γ

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

  [_]ᶜ : Ann × Ty → Ctx
  [(r , A)]ᶜ = ctx [ r ] [ A ]

  [_·_]ᶜ : Ann → Ty → Ctx
  [ ρ · A ]ᶜ = ctx [ ρ ] [ A ]

  _++ᶜ_ : Ctx → Ctx → Ctx
  ctx P γ ++ᶜ ctx Q δ = ctx (P ++ Q) (γ ++ δ)

  IfConcat : ∀ {ℓ} → Ctx → Set ℓ → Set ℓ
  IfConcat (ctx {[-]} P γ) X = ⊤
  IfConcat (ctx {ε} P γ) X = ⊤
  IfConcat (ctx {s <+> t} P γ) X = X

  leftᶜ : (Γ : Ctx) → IfConcat Γ Ctx
  leftᶜ (ctx {[-]} P γ) = _
  leftᶜ (ctx {ε} P γ) = _
  leftᶜ (ctx {s <+> t} P γ) = ctx {s} (P ∘ ↙) (γ ∘ ↙)

  rightᶜ : (Γ : Ctx) → IfConcat Γ Ctx
  rightᶜ (ctx {[-]} P γ) = _
  rightᶜ (ctx {ε} P γ) = _
  rightᶜ (ctx {s <+> t} P γ) = ctx {t} (P ∘ ↘) (γ ∘ ↘)

  leftᶜ′ : ∀ {s t} → SizedCtx (s <+> t) → Ctx
  leftᶜ′ (sctx P γ) = ctx (P ∘ ↙) (γ ∘ ↙)

  rightᶜ′ : ∀ {s t} → SizedCtx (s <+> t) → Ctx
  rightᶜ′ (sctx P γ) = ctx (P ∘ ↘) (γ ∘ ↘)
\end{code}

Premises to each rule form a tree.
At each leaf is a premise, which binds one Ctx's worth of new variables.
Annotations are shared out to the premises via separation logic
connectives:
\begin{verbatim}
\item separating conjunction (`I, _`*_) – e.g, ⊗-introduction
\item sharing conjunction (`⊤, _`∧_)    – e.g, &-introduction
\item scaling (_`·_)                    – e.g, !-introduction
\item the duplicable modality (`□)      – e.g, recursion rules
\end{verbatim}

\begin{code}
  module _ (fl : PremisesFlags) (open PremisesFlags fl) where

    infix 1 _=⇒_ _▹_
    infixr 2 _`✴_
    infixr 2 _`∧_
    infixr 3 _`·_
\end{code}

%<*Premises>
\begin{code}
    data Premises : Set where
      ⟨_`⊢_⟩ : (Δ : Ctx) (A : Ty) → Premises
      `⊤ : {{_ : Has-⊤}} → Premises
      _`∧_ : {{_ : Has-∧}} (p q : Premises) → Premises
      `ℑ : {{_ : Has-ℑ}} → Premises
      _`✴_ : {{_ : Has-✴}} (p q : Premises) → Premises
      _`·_ : {{_ : Has-·}} (r : Ann) (p : Premises) → Premises
      `□ : {{_ : Has-□}} (bf : BoxFlags) (p : Premises) → Premises
\end{code}
%</Premises>

\begin{code}
    pattern `□⁰⁺ˣ p = `□ (boxFlags true true true) p
    pattern `□⁰⁺ p = `□ (boxFlags true true false) p
\end{code}

%<*Rule>
\begin{code}
    record Rule : Set where
      constructor _=⇒_
      field
        premises : Premises
        conclusion : Ty
    open Rule public
\end{code}
%</Rule>

%<*System>
\begin{code}
    record System : Set₁ where
      constructor _▹_
      field
        Label : Set
        rules : (l : Label) → Rule
    open System public
\end{code}
%</System>

%<*OpenFam>
\begin{code}
  OpenType : ∀ ℓ → Set (suc ℓ)
  OpenType ℓ = Ctx → Set ℓ

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

  ExtOpenFam : ∀ ℓ → Set (suc ℓ)
  ExtOpenFam ℓ = Ctx → OpenFam ℓ
\end{code}
%</OpenFam>

%<*Scope>
\begin{code}
  Scope : ∀ {ℓ} → OpenFam ℓ → ExtOpenFam ℓ
  Scope T Δ Γ A = T (Γ ++ᶜ Δ) A
\end{code}
%</Scope>
