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

module Spartan6.Examples.HierarchyImported where

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

import Spartan6.Examples.ImportedYosys as Imported
import Spartan6.Generated.YosysToggleEnable as Generated
import Spartan6.Hierarchy.CertifiedFlattening as Certified
import Spartan6.Hierarchy.Component as Component
import Spartan6.Hierarchy.Flatten as Flatten
import Spartan6.Hierarchy.Provenance as Provenance
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.Provenance as Netlist
import Spartan6.Netlist.StableDAG as Stable
import Spartan6.Semantics.Design as Semantics
import Spartan6.Semantics.Machine as Machine
import Spartan6.Semantics.Refinement as Refinement

clockPort resetPort enablePort qPort : StablePort
clockPort = stablePort 100 "clock" 1
resetPort = stablePort 101 "reset" 1
enablePort = stablePort 102 "toggle_enable" 1
qPort = stablePort 103 "q" 1

clockInterface resetInterface enableInterface qInterface : Interface
clockInterface = signalInterface clockPort
resetInterface = signalInterface resetPort
enableInterface = signalInterface enablePort
qInterface = signalInterface qPort

importedInput : Interface
importedInput =
  clockInterface ∥ᵢ (resetInterface ∥ᵢ enableInterface)

artifact : Netlist.ArtifactId
artifact = Netlist.artifactId Generated.adapterSourceSHA256

module-id : Netlist.ModuleId
module-id = Netlist.moduleId 0

lut-occurrence register-occurrence : Netlist.OccurrenceId
lut-occurrence = Netlist.occurrenceId 0
register-occurrence = Netlist.occurrenceId 1

designOrigin : Provenance.SourceOrigin
designOrigin =
  Provenance.sourceOrigin
    (just artifact) (just module-id) []ᴸ "toggle_enable"

lutOrigin : Provenance.SourceOrigin
lutOrigin =
  Provenance.sourceOrigin
    (just artifact) (just module-id)
    (lut-occurrence ∷ᴸ []ᴸ) "LUT2"

registerOrigin : Provenance.SourceOrigin
registerOrigin =
  Provenance.sourceOrigin
    (just artifact) (just module-id)
    (register-occurrence ∷ᴸ []ᴸ) "FDRE"

importedNodeOrigins : Vec Provenance.NodeOrigin 3
importedNodeOrigins =
  Provenance.nodeOrigin lutOrigin 0
  ∷ Provenance.nodeOrigin registerOrigin 0
  ∷ Provenance.nodeOrigin registerOrigin 1
  ∷ []

importedNodeOriginsAccounted :
  Provenance.NodesAccountedFor
    (Provenance.leafProvenance designOrigin) importedNodeOrigins
importedNodeOriginsAccounted =
  Provenance.accountedNodesNext
    (Provenance.accountedLeaf
      (Provenance.sourceWithin refl refl
        (lut-occurrence ∷ᴸ []ᴸ) refl))
    (Provenance.accountedNodesNext
      (Provenance.accountedLeaf
        (Provenance.sourceWithin refl refl
          (register-occurrence ∷ᴸ []ᴸ) refl))
      (Provenance.accountedNodesNext
        (Provenance.accountedLeaf
          (Provenance.sourceWithin refl refl
            (register-occurrence ∷ᴸ []ᴸ) refl))
        Provenance.accountedNodesDone))

importedLeaf : Flatten.FlatLeaf importedInput qInterface
importedLeaf =
  Flatten.flatLeaf 100 "imported-toggle" designOrigin 1 3
    (Stable.convertNetlist Imported.importedNetlist)
    importedNodeOrigins

importedComponent : Component.Component
  importedInput qInterface Semantics.Event (Vec Bit 1)
importedComponent = Flatten.leafComponent importedLeaf

allLowInput : Environment importedInput
allLowInput =
  unflattenEnvironment {importedInput} (low ∷ low ∷ low ∷ [])

enabledInput : Environment importedInput
enabledInput =
  unflattenEnvironment {importedInput} (high ∷ low ∷ high ∷ [])

input-order-is-retained :
  flattenEnvironment {importedInput} enabledInput
  ≡ high ∷ low ∷ high ∷ []
input-order-is-retained =
  flatten-unflatten {interface = importedInput}
    (high ∷ low ∷ high ∷ [])

wrapped-imported-starts-low :
  Component.componentObserve importedComponent allLowInput
    (Component.componentInitial importedComponent)
  ≡ low ∷ []
wrapped-imported-starts-low = refl

wrapped-enabled-edge-toggles-high :
  Component.componentStep importedComponent Semantics.risingEdge
    enabledInput (low ∷ [])
  ≡ high ∷ []
wrapped-enabled-edge-toggles-high = refl

wrapped-observation-preserves-checked :
  ∀ (input : Environment importedInput) (state : Vec Bit 1)
  -> flattenEnvironment {qInterface}
      (Component.componentObserve importedComponent input state)
    ≡ Semantics.observe
        (Checked.compileNetlist Imported.importedNetlist)
        (flattenEnvironment {importedInput} input) state
wrapped-observation-preserves-checked input state =
  Flatten.leaf-observation-flat importedLeaf input state
  ∙ Stable.convertOutputs-compile
      Imported.importedNetlist
      (flattenEnvironment {importedInput} input) state

wrapped-transition-preserves-checked :
  ∀ (input : Environment importedInput) (state : Vec Bit 1)
  -> Component.componentStep importedComponent Semantics.risingEdge
      input state
    ≡ Semantics.step
        (Checked.compileNetlist Imported.importedNetlist)
        Semantics.risingEdge
        (flattenEnvironment {importedInput} input) state
wrapped-transition-preserves-checked input state =
  Flatten.leaf-rising-transition-flat importedLeaf input state
  ∙ Stable.convertNext-compile
      Imported.importedNetlist
      (flattenEnvironment {importedInput} input) state

importedFlattening :
  Certified.ProvenanceCertifiedFlattening importedComponent
importedFlattening =
  Certified.leafFlattens importedLeaf importedNodeOriginsAccounted

importedImplementsFlat :
  Refinement.Implements
    (Component.componentMachine importedComponent)
    (Machine.machineSystem (Component.componentMachine importedComponent))
importedImplementsFlat = Certified.certificateImplements importedFlattening

wrapper-occurrence : Netlist.OccurrenceId
wrapper-occurrence = Netlist.occurrenceId 42

wrapperIdentity : Provenance.InstanceIdentity
wrapperIdentity =
  Provenance.instanceIdentity wrapper-occurrence "top.imported"

instantiatedImported : Component.Component
  importedInput qInterface Semantics.Event (Vec Bit 1)
instantiatedImported =
  Component.instantiate wrapper-occurrence "top.imported" importedComponent

wrapped-theorem-reused-after-instantiation :
  Component.componentObserve instantiatedImported allLowInput
    (Component.componentInitial instantiatedImported)
  ≡ low ∷ []
wrapped-theorem-reused-after-instantiation =
  Component.reuse-observation-under-instantiation
    wrapper-occurrence "top.imported" importedComponent
    allLowInput (Component.componentInitial importedComponent)
    (low ∷ []) wrapped-imported-starts-low

instantiatedFlattening :
  Certified.ProvenanceCertifiedFlattening instantiatedImported
instantiatedFlattening =
  Certified.instantiateFlattens wrapperIdentity importedFlattening

instantiated-first-node-path-retained :
  Provenance.originInstancePath
    (Provenance.nodeSource
      (lookup fzero
        (Flatten.leafNodeOrigins
          (Certified.certifiedLeaf instantiatedFlattening))))
  ≡ wrapper-occurrence ∷ᴸ lut-occurrence ∷ᴸ []ᴸ
instantiated-first-node-path-retained = refl