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

module Spartan6.Semantics.DesignMachine where

open import Spartan6.Prelude
import Spartan6.Semantics.Design as Flat
import Spartan6.Semantics.Execution as Legacy
import Spartan6.Semantics.Machine as Generic
import Spartan6.Semantics.Refinement as Refinement
import Spartan6.Semantics.Trace as Trace

asMachine : ∀ {inputCount outputCount registerCount}
  → Flat.Design inputCount outputCount registerCount
  → Generic.Machine
      (Vec Bit inputCount) (Vec Bit outputCount) Flat.Event
      (Vec Bit registerCount)
asMachine design =
  Generic.machine
    (Flat.initial design)
    (Flat.observe design)
    (Flat.step design)

asMachine-initial :
  ∀ {inputCount outputCount registerCount}
    (design : Flat.Design inputCount outputCount registerCount)
  → Generic.initialState (asMachine design) ≡ Flat.initial design
asMachine-initial design = refl

asMachine-observe :
  ∀ {inputCount outputCount registerCount}
    (design : Flat.Design inputCount outputCount registerCount)
    input state
  → Generic.observe (asMachine design) input state
    ≡ Flat.observe design input state
asMachine-observe design input state = refl

asMachine-step :
  ∀ {inputCount outputCount registerCount}
    (design : Flat.Design inputCount outputCount registerCount)
    event input state
  → Generic.step (asMachine design) event input state
    ≡ Flat.step design event input state
asMachine-step design event input state = refl

toGenericStimulus : ∀ {inputCount}
  → Flat.Stimulus inputCount
  → Generic.Stimulus (Vec Bit inputCount) Flat.Event
toGenericStimulus sample =
  Generic.stimulus
    (Flat.stimulusInputs sample) (Flat.stimulusEvent sample)

toFlatFrame : ∀ {outputCount registerCount}
  → Generic.Frame (Vec Bit outputCount) (Vec Bit registerCount)
  → Flat.Frame outputCount registerCount
toFlatFrame (Generic.frame observation before after) =
  Flat.frame observation before after

run-preserved :
  ∀ {inputCount outputCount registerCount}
    (design : Flat.Design inputCount outputCount registerCount)
    (state : Vec Bit registerCount)
    (samples : List (Flat.Stimulus inputCount))
  → Generic.run (asMachine design) state
      (mapList toGenericStimulus samples)
    ≡ Flat.run design state samples
run-preserved design state []ᴸ = refl
run-preserved design state (sample ∷ᴸ samples) =
  run-preserved design
    (Flat.step design
      (Flat.stimulusEvent sample) (Flat.stimulusInputs sample) state)
    samples

execute-preserved :
  ∀ {inputCount outputCount registerCount}
    (design : Flat.Design inputCount outputCount registerCount)
    (state : Vec Bit registerCount)
    (samples : List (Flat.Stimulus inputCount))
  → mapList toFlatFrame
      (Generic.execute (asMachine design) state
        (mapList toGenericStimulus samples))
    ≡ Flat.execute design state samples
execute-preserved design state []ᴸ = refl
execute-preserved design state (sample ∷ᴸ samples) =
  cong
    (Flat.frame
      (Flat.observe design (Flat.stimulusInputs sample) state)
      state
      (Flat.step design
        (Flat.stimulusEvent sample) (Flat.stimulusInputs sample) state)
      ∷ᴸ_)
    (execute-preserved design
      (Flat.step design
        (Flat.stimulusEvent sample) (Flat.stimulusInputs sample) state)
      samples)

execution-to-steps :
  ∀ {inputCount outputCount registerCount}
    {design : Flat.Design inputCount outputCount registerCount}
    {state final samples}
  → Legacy.Executes design state samples final
  → Trace.Steps (Generic.machineSystem (asMachine design)) state
      (mapList toGenericStimulus samples) final
execution-to-steps Legacy.executionDone = Trace.stepsDone
execution-to-steps
  {design = design} {state = state}
  (Legacy.executionStep sample execution) =
  Trace.stepsNext (toGenericStimulus sample)
    (Flat.observe design (Flat.stimulusInputs sample) state)
    refl refl (execution-to-steps execution)

steps-to-execution :
  ∀ {inputCount outputCount registerCount}
    {design : Flat.Design inputCount outputCount registerCount}
    {state final samples}
  → Trace.Steps (Generic.machineSystem (asMachine design)) state
      (mapList toGenericStimulus samples) final
  → Legacy.Executes design state samples final
steps-to-execution {design = design} {state = state} {final = final}
  {samples = samples} steps =
  subst (Legacy.Executes design state samples)
    (sym (run-preserved design state samples)
      ∙ Trace.machine-steps-complete steps)
    (Legacy.run-executes design state samples)

designImplements :
  ∀ {inputCount outputCount registerCount}
    (design : Flat.Design inputCount outputCount registerCount)
  → Refinement.Implements
      (asMachine design) (Generic.machineSystem (asMachine design))
designImplements design = Refinement.machine-implements-system (asMachine design)