{-# OPTIONS --safe --cubical #-}

module Spartan6.Semantics.Machine where

open import Spartan6.Prelude
import Spartan6.Semantics.System as Relational

record Machine
  (Input Output Event State : Type₀) : Type₀ where
  constructor machine
  field
    initialState : State
    observe : Input → State → Output
    step : Event → Input → State → State

open Machine public

record Stimulus (Input Event : Type₀) : Type₀ where
  constructor stimulus
  field
    stimulusInput : Input
    stimulusEvent : Event

open Stimulus public

record Frame (Output State : Type₀) : Type₀ where
  constructor frame
  field
    frameObservation : Output
    frameStateBefore : State
    frameStateAfter : State

open Frame public

run : ∀ {Input Output Event State}
    → Machine Input Output Event State
    → State → List (Stimulus Input Event) → State
run implementation state []ᴸ = state
run implementation state (sample ∷ᴸ samples) =
  run implementation
    (step implementation
      (stimulusEvent sample) (stimulusInput sample) state)
    samples

execute : ∀ {Input Output Event State}
        → Machine Input Output Event State
        → State
        → List (Stimulus Input Event)
        → List (Frame Output State)
execute implementation state []ᴸ = []ᴸ
execute {State = State} implementation state (sample ∷ᴸ samples) =
  frame
    (observe implementation (stimulusInput sample) state)
    state next
  ∷ᴸ execute implementation next samples
  where
  next : State
  next = step implementation
    (stimulusEvent sample) (stimulusInput sample) state

machineSystem : ∀ {Input Output Event State}
              → Machine Input Output Event State
              → Relational.System Input Output Event State
Relational.Initial (machineSystem implementation) state =
  initialState implementation ≡ state
Relational.ObservationAllowed (machineSystem implementation)
  input state output = observe implementation input state ≡ output
Relational.TransitionAllowed (machineSystem implementation)
  event input before after = step implementation event input before ≡ after