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

module Spartan6.Semantics.Trace where

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

data Steps
  {Input Output Event State : Type₀}
  (system : Relational.System Input Output Event State)
  : State → List (Executable.Stimulus Input Event) → State → Type₀ where

  stepsDone : ∀ {state} → Steps system state []ᴸ state

  stepsNext : ∀ {before after final samples}
    → (sample : Executable.Stimulus Input Event)
    → (observation : Output)
    → Relational.ObservationAllowed system
        (Executable.stimulusInput sample) before observation
    → Relational.TransitionAllowed system
        (Executable.stimulusEvent sample)
        (Executable.stimulusInput sample) before after
    → Steps system after samples final
    → Steps system before (sample ∷ᴸ samples) final

record Trace
  {Input Output Event State : Type₀}
  (system : Relational.System Input Output Event State)
  (samples : List (Executable.Stimulus Input Event))
  (final : State) : Type₀ where
  constructor trace
  field
    traceInitialState : State
    traceInitial : Relational.Initial system traceInitialState
    traceSteps : Steps system traceInitialState samples final

open Trace public

eraseSteps : ∀ {Input Output Event State system before samples after}
  → Steps {Input} {Output} {Event} {State} system before samples after
  → List (Executable.Frame Output State)
eraseSteps stepsDone = []ᴸ
eraseSteps {before = before}
  (stepsNext {after = after} sample observation observed transitioned rest) =
  Executable.frame observation before after ∷ᴸ eraseSteps rest

machineSteps : ∀ {Input Output Event State}
  → (implementation : Executable.Machine Input Output Event State)
  → (state : State)
  → (samples : List (Executable.Stimulus Input Event))
  → Steps (Executable.machineSystem implementation) state samples
      (Executable.run implementation state samples)
machineSteps implementation state []ᴸ = stepsDone
machineSteps implementation state (sample ∷ᴸ samples) =
  stepsNext sample
    (Executable.observe implementation
      (Executable.stimulusInput sample) state)
    refl refl
    (machineSteps implementation
      (Executable.step implementation
        (Executable.stimulusEvent sample)
        (Executable.stimulusInput sample) state)
      samples)

machineTrace : ∀ {Input Output Event State}
  → (implementation : Executable.Machine Input Output Event State)
  → (samples : List (Executable.Stimulus Input Event))
  → Trace (Executable.machineSystem implementation) samples
      (Executable.run implementation
        (Executable.initialState implementation) samples)
machineTrace implementation samples =
  trace (Executable.initialState implementation) refl
    (machineSteps implementation
      (Executable.initialState implementation) samples)

machine-steps-complete :
  ∀ {Input Output Event State}
    {implementation : Executable.Machine Input Output Event State}
    {before after samples}
  → Steps (Executable.machineSystem implementation) before samples after
  → Executable.run implementation before samples ≡ after
machine-steps-complete stepsDone = refl
machine-steps-complete
  {implementation = implementation}
  {samples = sample ∷ᴸ samples}
  (stepsNext .sample observation observed transitioned rest) =
  cong (λ state → Executable.run implementation state samples) transitioned
  ∙ machine-steps-complete rest

machine-steps-erase :
  ∀ {Input Output Event State}
    (implementation : Executable.Machine Input Output Event State)
    (state : State)
    (samples : List (Executable.Stimulus Input Event))
  → eraseSteps (machineSteps implementation state samples)
    ≡ Executable.execute implementation state samples
machine-steps-erase implementation state []ᴸ = refl
machine-steps-erase implementation state (sample ∷ᴸ samples) =
  cong
    (Executable.frame
      (Executable.observe implementation
        (Executable.stimulusInput sample) state)
      state
      (Executable.step implementation
        (Executable.stimulusEvent sample)
        (Executable.stimulusInput sample) state) ∷ᴸ_)
    (machine-steps-erase implementation
      (Executable.step implementation
        (Executable.stimulusEvent sample)
        (Executable.stimulusInput sample) state)
      samples)