\begin{code}
{-# OPTIONS --sized-types --without-K --postfix-projections --prop #-}
module Generic.Linear.Example.PaperExamples where

open import Algebra.Po
open import Data.Product
open import Data.Unit
open import Level
open import Proposition

module Example1 (poSemiring : PoSemiring 0ℓ 0ℓ 0ℓ) where

  open PoSemiring poSemiring
    renaming (Carrier to Ann
             ; _≤_ to _⊴_
             ; refl to ⊴-refl; trans to ⊴-trans
             )

  infixr 5 _·_⊸_
  infixr 6 _⊕_
\end{code}

%<*exItypes>
\begin{code}
  data Ty : Set where
    ι : Ty
    _·_⊸_ : (r : Ann) (A B : Ty) → Ty
    _⊕_ : (A B : Ty) → Ty
\end{code}
%</exItypes>

\begin{code}
  open import Generic.Linear.Syntax Ty Ann
  open import Generic.Linear.Syntax.Interpretation Ty rawPoSemiring
  open import Generic.Linear.Syntax.Term Ty rawPoSemiring
\end{code}

%<*exIlabels>
\begin{code}
  data `Sys : Set where
    `lam `app : (r : Ann) (A B : Ty) → `Sys
    `inl `inr : (A B : Ty) → `Sys
    `case : (A B C : Ty) → `Sys
\end{code}
%</exIlabels>

\begin{code}
  Sys : System allPremisesFlags
  Sys .Label = `Sys
\end{code}
%<*exIfunrules>
\begin{code}
  Sys .rules (`lam r A B) =
    ⟨ [ r , A ]ᶜ `⊢ B ⟩
    =⇒ r · A ⊸ B
  Sys .rules (`app r A B) =
    ⟨ []ᶜ `⊢ r · A ⊸ B ⟩ `✴ r `· ⟨ []ᶜ `⊢ A ⟩
    =⇒ B
\end{code}
%</exIfunrules>
%<*exIsumrules>
\begin{code}
  Sys .rules (`inl A B) =
    ⟨ []ᶜ `⊢ A ⟩
    =⇒ A ⊕ B
  Sys .rules (`inr A B) =
    ⟨ []ᶜ `⊢ B ⟩
    =⇒ A ⊕ B
  Sys .rules (`case A B C) =
    ⟨ []ᶜ `⊢ A ⊕ B ⟩ `✴ (⟨ [ 1# , A ]ᶜ `⊢ C ⟩ `∧ ⟨ [ 1# , B ]ᶜ `⊢ C ⟩)
    =⇒ C
\end{code}
%</exIsumrules>
