BCS.agda

open import Data.Empty

-- Intuition: We have objects (Struct) which consist of a bunch of fields (Atomic)
-- which can be in different states (state).

record Struct : Set₁ where
  field
    Atomic : Set
    State  : Atomic → Set
open Struct

-- We want to define a language which allows us to specify in what state is a specific Atomic
-- of a Struct (_⟨_⊳_⟩),
-- but also which allows us to put multiple such statements in different juxtapositions (_⊗_, _⊕_).

mutual
  data Form : Set₁ where
    𝟏       : Form
    St      : Struct → Form
    _⟨_⊳_⟩  : (ϕ : Form) → (A : Atomic (toS ϕ)) → State (toS ϕ) A → Form
    _⊕_ _⊗_ : Form → Form → Form

  toS : Form → Struct
  toS (St x)        = x
  toS (ϕ ⟨ A ⊳ x ⟩) = toS ϕ
  toS _             = Empty
    where Empty : Struct
          Empty = record {Atomic = ⊥; State = λ ()}


-- Example
data Atomics : Set where -- Example collection of Atomic's
  A B : Atomics

data States : Set where -- Example collection of State's for our Atomic A.
  u p : States

S : Struct -- Example Struct object. Both Atomic's have the same states, for simplicity.
S = record {Atomic = Atomics; State = λ _ → States}


-- So now we can write e.g.
ex₁ : Form -- Inside our S, A is in state u and B is in state p
ex₁ = (St S) ⟨ A ⊳ u ⟩ ⟨ B ⊳ p ⟩

ex₂ : Form -- But we can only specify one of the atomics.
ex₂ = (St S) ⟨ A ⊳ u ⟩

ex₃ : Form -- And we can put these together
ex₃ = ex₁ ⊗ ex₂