Leios.FFD

1
module Leios.FFD where

123456
record FFDAbstract : Type₁ where
  field Header Body ID : Type
        ⦃ DecEq-Header ⦄ : DecEq Header
        ⦃ DecEq-Body ⦄ : DecEq Body
        match : Header → Body → Type
        msgID : Header → ID

123
  data Input : Type where
    Send  : Header → Maybe Body → Input
    Fetch : Input

123
  data Output : Type where
    SendRes  : Output
    FetchRes : List (Header ⊎ Body) → Output

1234
  record Functionality : Type₁ where
    field State : Type
          initFFDState : State
          _-⟦_/_⟧⇀_ : State → Input → Output → State → Type

12
    open Input public
    open Output public