{-# OPTIONS --without-K #-}
open import Type
open import Control.Protocol.Core
open import Control.Protocol.Additive
open import Control.Protocol.Multiplicative
module Control.Protocol.CLL where
data CLL : ★ where
`1 `⊤ `0 `⊥ : CLL
_`⊗_ _`⅋_ _`⊕_ _`&_ : (A B : CLL) → CLL
_⊥ : CLL → CLL
`1 ⊥ = `⊥
`⊥ ⊥ = `1
`0 ⊥ = `⊤
`⊤ ⊥ = `0
(A `⊗ B)⊥ = A ⊥ `⅋ B ⊥
(A `⅋ B)⊥ = A ⊥ `⊗ B ⊥
(A `⊕ B)⊥ = A ⊥ `& B ⊥
(A `& B)⊥ = A ⊥ `⊕ B ⊥
CLL-proto : CLL → Proto
CLL-proto `1 = end
CLL-proto `⊥ = end
CLL-proto `0 = P0
CLL-proto `⊤ = P⊤
CLL-proto (A `⊗ B) = CLL-proto A ⊗ CLL-proto B
CLL-proto (A `⅋ B) = CLL-proto A ⅋ CLL-proto B
CLL-proto (A `⊕ B) = CLL-proto A ⊕ CLL-proto B
CLL-proto (A `& B) = CLL-proto A & CLL-proto B