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

module Spartan6.Semantics.Refinement where

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

record Implements
  {Input Output Event MachineState SystemState : Type₀}
  (implementation : Executable.Machine Input Output Event MachineState)
  (specification : Relational.System Input Output Event SystemState)
  : Type₁ where
  field
    StateRelation : MachineState → SystemState → Type₀
    specificationInitial : SystemState
    initialAllowed : Relational.Initial specification specificationInitial
    initialRelated :
      StateRelation (Executable.initialState implementation) specificationInitial
    observationPreserved : ∀ input machine-state system-state
      → StateRelation machine-state system-state
      → Relational.ObservationAllowed specification input system-state
          (Executable.observe implementation input machine-state)
    transitionPreserved : ∀ event input machine-state system-state
      → StateRelation machine-state system-state
      → Σ[ next ∈ SystemState ]
          (Relational.TransitionAllowed specification event input
            system-state next
          × StateRelation
              (Executable.step implementation event input machine-state)
              next)

open Implements public

machine-implements-system :
  ∀ {Input Output Event State}
    (implementation : Executable.Machine Input Output Event State)
  → Implements implementation (Executable.machineSystem implementation)
StateRelation (machine-implements-system implementation) left right =
  left ≡ right
specificationInitial (machine-implements-system implementation) =
  Executable.initialState implementation
initialAllowed (machine-implements-system implementation) = refl
initialRelated (machine-implements-system implementation) = refl
observationPreserved (machine-implements-system implementation)
  input machine-state system-state related =
  sym (cong (Executable.observe implementation input) related)
transitionPreserved (machine-implements-system implementation)
  event input machine-state system-state related =
  Executable.step implementation event input machine-state
  , sym (cong (Executable.step implementation event input) related)
  , refl

implementsSteps :
  ∀ {Input Output Event MachineState SystemState}
    {implementation : Executable.Machine Input Output Event MachineState}
    {specification : Relational.System Input Output Event SystemState}
  → (proof : Implements implementation specification)
  → (machine-state : MachineState)
  → (system-state : SystemState)
  → StateRelation proof machine-state system-state
  → (samples : List (Executable.Stimulus Input Event))
  → Σ[ final ∈ SystemState ]
      (Trace.Steps specification system-state samples final
      × StateRelation proof
          (Executable.run implementation machine-state samples) final)
implementsSteps {implementation = implementation}
  proof machine-state system-state related []ᴸ =
  system-state , Trace.stepsDone , related
implementsSteps {implementation = implementation}
  proof machine-state system-state related (sample ∷ᴸ samples)
  with transitionPreserved proof
    (Executable.stimulusEvent sample)
    (Executable.stimulusInput sample)
    machine-state system-state related
... | next , transitioned , next-related
  with implementsSteps proof
    (Executable.step implementation
      (Executable.stimulusEvent sample)
      (Executable.stimulusInput sample) machine-state)
    next next-related samples
... | final , rest , final-related =
  final
  , Trace.stepsNext sample
      (Executable.observe implementation
        (Executable.stimulusInput sample) machine-state)
      (observationPreserved proof
        (Executable.stimulusInput sample)
        machine-state system-state related)
      transitioned rest
  , final-related

implementation-trace :
  ∀ {Input Output Event MachineState SystemState}
    {implementation : Executable.Machine Input Output Event MachineState}
    {specification : Relational.System Input Output Event SystemState}
  → (proof : Implements implementation specification)
  → (samples : List (Executable.Stimulus Input Event))
  → Σ[ final ∈ SystemState ] Trace.Trace specification samples final
implementation-trace {implementation = implementation}
  proof samples
  with implementsSteps proof
    (Executable.initialState implementation)
    (specificationInitial proof)
    (initialRelated proof) samples
... | final , steps , related =
  final , Trace.trace
    (specificationInitial proof) (initialAllowed proof) steps