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

module Spartan6.Hierarchy.FlatMachine where

open import Spartan6.Prelude
open import Spartan6.Hierarchy.Interface

import Spartan6.Hierarchy.CertifiedFlattening as DAG
import Spartan6.Hierarchy.Component as Component
import Spartan6.Hierarchy.Flatten as Legacy
import Spartan6.Hierarchy.Provenance as Provenance
import Spartan6.Semantics.Design as Flat
import Spartan6.Semantics.Machine as Machine

-- A flat machine fixes an explicit bit layout for state while leaving the
-- event type general.  Observation and transition are deliberately separate:
-- simultaneous-domain selection cannot be encoded by the legacy netlist's
-- single rising-edge next vector.

record FlatMachine
  (Input Output : Interface) (Event : Type₀) : Type₁ where
  constructor flatMachine
  field
    flatIdentity : Provenance.ComponentIdentity
    flatProvenance : Provenance.HierarchyProvenance
    flatStateCount : ℕ
    flatImplementation :
      Machine.Machine
        (Environment Input) (Environment Output) Event
        (Vec Bit flatStateCount)

open FlatMachine public

flatInitial : ∀ {Input Output Event}
  -> (target : FlatMachine Input Output Event)
  -> Vec Bit (flatStateCount target)
flatInitial target = Machine.initialState (flatImplementation target)

flatObserve : ∀ {Input Output Event}
  -> (target : FlatMachine Input Output Event)
  -> Environment Input
  -> Vec Bit (flatStateCount target)
  -> Environment Output
flatObserve target = Machine.observe (flatImplementation target)

flatStep : ∀ {Input Output Event}
  -> (target : FlatMachine Input Output Event)
  -> Event
  -> Environment Input
  -> Vec Bit (flatStateCount target)
  -> Vec Bit (flatStateCount target)
flatStep target = Machine.step (flatImplementation target)

record CertifiedMachineFlattening
  {Input Output : Interface} {Event State : Type₀}
  (hierarchy : Component.Component Input Output Event State) : Type₁ where
  constructor certifiedMachineFlattening
  field
    flatTarget : FlatMachine Input Output Event
    StateRelation :
      State -> Vec Bit (flatStateCount flatTarget) -> Type₀
    initialRelated :
      StateRelation
        (Component.componentInitial hierarchy)
        (flatInitial flatTarget)
    observationPreserved : ∀ input hierarchy-state flat-state
      -> StateRelation hierarchy-state flat-state
      -> Component.componentObserve hierarchy input hierarchy-state
        ≡ flatObserve flatTarget input flat-state
    transitionPreserved : ∀ event input hierarchy-state flat-state
      -> StateRelation hierarchy-state flat-state
      -> StateRelation
          (Component.componentStep hierarchy event input hierarchy-state)
          (flatStep flatTarget event input flat-state)
    provenanceRetained :
      flatProvenance flatTarget
      ≡ Component.componentProvenance hierarchy

open CertifiedMachineFlattening public

-- The legacy DAG leaf is recovered without changing its semantics.  Its
-- provenance-certified wrapper supplies the exact hierarchy provenance that
-- the older flat leaf summary did not itself retain.

fromLegacyDAG :
  ∀ {Input Output State}
  {hierarchy : Component.Component Input Output Flat.Event State}
  -> DAG.ProvenanceCertifiedFlattening hierarchy
  -> CertifiedMachineFlattening hierarchy
flatTarget (fromLegacyDAG {hierarchy = hierarchy} certificate) =
  flatMachine
    (Provenance.componentIdentity
      (Component.componentStableId hierarchy)
      (Component.componentName hierarchy))
    (Component.componentProvenance hierarchy)
    (Legacy.leafStateCount (DAG.certifiedLeaf certificate))
    (Component.componentMachine
      (Legacy.leafComponent (DAG.certifiedLeaf certificate)))
StateRelation (fromLegacyDAG certificate) =
  Legacy.StateRelation (DAG.semanticCertificate certificate)
initialRelated (fromLegacyDAG certificate) =
  Legacy.initialRelated (DAG.semanticCertificate certificate)
observationPreserved (fromLegacyDAG certificate) =
  Legacy.observationPreserved (DAG.semanticCertificate certificate)
transitionPreserved (fromLegacyDAG certificate) =
  Legacy.transitionPreserved (DAG.semanticCertificate certificate)
provenanceRetained (fromLegacyDAG certificate) = refl