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

module Spartan6.Examples.HierarchyComposition where

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

import Spartan6.Hierarchy.Component as Component
import Spartan6.Hierarchy.CertifiedFlattening as Certified
import Spartan6.Hierarchy.Flatten as Flatten
import Spartan6.Hierarchy.Provenance as Provenance
import Spartan6.Hierarchy.StableCompose as Compose
import Spartan6.Netlist.Provenance as Netlist
import Spartan6.Netlist.StableDAG as Stable
import Spartan6.Semantics.Design as Semantics
import Spartan6.Semantics.Machine as Machine

bitPort : StablePort
bitPort = stablePort  "bit" 

bitInterface : Interface
bitInterface = signalInterface bitPort

constructedOrigin : Provenance.SourceOrigin
constructedOrigin =
  Provenance.sourceOrigin noArtifact noModule []ᴸ "constructed.scalar"
  where
  noArtifact : Maybe Netlist.ArtifactId
  noArtifact = nothing

  noModule : Maybe Netlist.ModuleId
  noModule = nothing

invertBits : Environment bitInterface -> Environment bitInterface
invertBits (bit ∷ []) = not bit ∷ []

identityBits : Environment bitInterface -> Environment bitInterface
identityBits bits = bits

statelessStep : Unit -> Environment bitInterface -> Unit -> Unit
statelessStep event input state = tt

invertObserve : Environment bitInterface -> Unit -> Environment bitInterface
invertObserve input state = invertBits input

identityObserve : Environment bitInterface -> Unit -> Environment bitInterface
identityObserve input state = identityBits input

invertComponent : Component.Component bitInterface bitInterface Unit Unit
invertComponent =
  Component.leafComponent  "invert" constructedOrigin
    (Machine.machine tt
      invertObserve statelessStep)

identityComponent : Component.Component bitInterface bitInterface Unit Unit
identityComponent =
  Component.leafComponent  "identity" constructedOrigin
    (Machine.machine tt
      identityObserve statelessStep)

twoInverters : Component.Component bitInterface bitInterface Unit (Unit × Unit)
twoInverters =
  Component.serial  "double-invert" invertComponent invertComponent

scalar-serial-reduces : ∀ (bit : Bit)
  -> Component.componentObserve twoInverters
      (bit ∷ []) (tt , tt)
    ≡ bit ∷ []
scalar-serial-reduces false = refl
scalar-serial-reduces true = refl

serial-transition-uses-common-pre-state :
  Component.componentStep twoInverters tt
    (high ∷ []) (tt , tt)
  ≡ (tt , tt)
serial-transition-uses-common-pre-state = refl

twoParallel : Component.Component
  (bitInterface ∥ᵢ bitInterface)
  (bitInterface ∥ᵢ bitInterface)
  Unit (Unit × Unit)
twoParallel =
  Component.parallel  "parallel" invertComponent identityComponent

parallel-components-reduce :
  Component.componentObserve twoParallel
    ((low ∷ []) , (high ∷ [])) (tt , tt)
  ≡ ((high ∷ []) , (high ∷ []))
parallel-components-reduce = refl

swappedParallel : Component.Component
  (bitInterface ∥ᵢ bitInterface)
  (bitInterface ∥ᵢ bitInterface)
  Unit (Unit × Unit)
swappedParallel =
  Component.renameComponent  "swap-outputs"
    (identityRenaming (bitInterface ∥ᵢ bitInterface))
    swapParallel twoParallel

parallel-output-renaming-reduces :
  Component.componentObserve swappedParallel
    ((high ∷ []) , (low ∷ [])) (tt , tt)
  ≡ ((low ∷ []) , (low ∷ []))
parallel-output-renaming-reduces = refl

visibleLeft : Component.Component
  (bitInterface ∥ᵢ bitInterface) bitInterface
  Unit (Unit × Unit)
visibleLeft =
  Component.hideOutputs  "hide-right" leftProjection twoParallel

hiding-projects-one-output :
  Component.componentObserve visibleLeft
    ((low ∷ []) , (high ∷ [])) (tt , tt)
  ≡ high ∷ []
hiding-projects-one-output = refl

rightInputBoundHigh : Component.Component
  bitInterface (bitInterface ∥ᵢ bitInterface)
  Unit (Unit × Unit)
rightInputBoundHigh =
  Component.bindHiddenInput  "bind-right-high"
    (high ∷ []) twoParallel

hidden-input-instantiation-reduces :
  Component.componentObserve rightInputBoundHigh
    (low ∷ []) (tt , tt)
  ≡ ((high ∷ []) , (high ∷ []))
hidden-input-instantiation-reduces = refl

parallel-environment-flat-order :
  flattenEnvironment
    {bitInterface ∥ᵢ bitInterface}
    ((low ∷ []) , (high ∷ []))
  ≡ low ∷ high ∷ []
parallel-environment-flat-order = refl

parallel-environment-round-trip :
  unflattenEnvironment
    {bitInterface ∥ᵢ bitInterface}
    (flattenEnvironment
      {bitInterface ∥ᵢ bitInterface}
      ((low ∷ []) , (high ∷ [])))
  ≡ ((low ∷ []) , (high ∷ []))
parallel-environment-round-trip =
  unflatten-flatten
    {interface = bitInterface ∥ᵢ bitInterface}
    ((low ∷ []) , (high ∷ []))

-- Concrete StableDAG flattening probes ------------------------------------

leftDAGOccurrence rightDAGOccurrence : Netlist.OccurrenceId
leftDAGOccurrence = Netlist.occurrenceId 
rightDAGOccurrence = Netlist.occurrenceId 

invertNodeOrigins : Vec Provenance.NodeOrigin 
invertNodeOrigins = Provenance.nodeOrigin constructedOrigin  ∷ []

invertNodeOriginsAccounted :
  Provenance.NodesAccountedFor
    (Provenance.leafProvenance constructedOrigin) invertNodeOrigins
invertNodeOriginsAccounted =
  Provenance.accountedNodesNext
    (Provenance.accountedLeaf
      (Provenance.sourceWithin refl refl []ᴸ refl))
    Provenance.accountedNodesDone

invertNetlist : Stable.StableNetlist    
invertNetlist =
  Stable.stableNetlist []
    (Stable.stableNoNodes Stable.▹
      Stable.stableInvert (Stable.stableExternal fzero))
    (Stable.stableLocal fzero ∷ [])
    []

invertLeaf : Flatten.FlatLeaf bitInterface bitInterface
invertLeaf =
  Flatten.flatLeaf  "invert.dag" constructedOrigin
      invertNetlist invertNodeOrigins

invertCertificate :
  Certified.ProvenanceCertifiedFlattening
    (Flatten.leafComponent invertLeaf)
invertCertificate =
  Certified.leafFlattens invertLeaf invertNodeOriginsAccounted

serialIdentity : Provenance.ComponentIdentity
serialIdentity = Provenance.componentIdentity  "double-invert.dag"

leftDAGIdentity rightDAGIdentity : Provenance.InstanceIdentity
leftDAGIdentity =
  Provenance.instanceIdentity leftDAGOccurrence "left-invert.dag"
rightDAGIdentity =
  Provenance.instanceIdentity rightDAGOccurrence "right-invert.dag"

serialDAGHierarchy : Component.Component
  bitInterface bitInterface Semantics.Event (Vec Bit  × Vec Bit )
serialDAGHierarchy =
  Component.serialInstances serialIdentity
    leftDAGIdentity rightDAGIdentity
    (Flatten.leafComponent invertLeaf)
    (Flatten.leafComponent invertLeaf)

serialDAGCertificate :
  Certified.ProvenanceCertifiedFlattening serialDAGHierarchy
serialDAGCertificate =
  Certified.serialFlattens serialIdentity constructedOrigin
    leftDAGIdentity rightDAGIdentity invertCertificate invertCertificate

serialDAGLeaf : Flatten.FlatLeaf bitInterface bitInterface
serialDAGLeaf =
  Certified.certifiedLeaf serialDAGCertificate

serial-DAG-observation : ∀ (bit : Bit)
  -> Stable.stableDirectOutputs
      (Flatten.leafNetlist serialDAGLeaf) (bit ∷ []) []
    ≡ bit ∷ []
serial-DAG-observation false = refl
serial-DAG-observation true = refl

serial-DAG-rising-next-preserved : ∀ (bit : Bit)
  -> Component.componentStep
      (Flatten.leafComponent serialDAGLeaf)
      Semantics.risingEdge (bit ∷ []) []
    ≡ appendVec
        (Component.componentStep (Flatten.leafComponent invertLeaf)
          Semantics.risingEdge (bit ∷ []) [])
        (Component.componentStep (Flatten.leafComponent invertLeaf)
          Semantics.risingEdge
          (Component.componentObserve (Flatten.leafComponent invertLeaf)
            (bit ∷ []) [])
          [])
serial-DAG-rising-next-preserved bit =
  refl

serial-node-resources-concatenate :
  Flatten.leafLocalCount serialDAGLeaf
  ≡ Flatten.leafLocalCount invertLeaf
    + Flatten.leafLocalCount invertLeaf
serial-node-resources-concatenate =
  Compose.serialLocalCount-correct invertNetlist invertNetlist

serial-node-provenance-combines :
  Provenance.NodesAccountedFor
    (Component.componentProvenance serialDAGHierarchy)
    (Flatten.leafNodeOrigins serialDAGLeaf)
serial-node-provenance-combines =
  Certified.provenancePreserved serialDAGCertificate

parallelIdentity : Provenance.ComponentIdentity
parallelIdentity = Provenance.componentIdentity  "parallel-invert.dag"

parallelDAGHierarchy : Component.Component
  (bitInterface ∥ᵢ bitInterface)
  (bitInterface ∥ᵢ bitInterface)
  Semantics.Event (Vec Bit  × Vec Bit )
parallelDAGHierarchy =
  Component.parallelInstances parallelIdentity
    leftDAGIdentity rightDAGIdentity
    (Flatten.leafComponent invertLeaf)
    (Flatten.leafComponent invertLeaf)

parallelDAGCertificate :
  Certified.ProvenanceCertifiedFlattening parallelDAGHierarchy
parallelDAGCertificate =
  Certified.parallelFlattens parallelIdentity constructedOrigin
    leftDAGIdentity rightDAGIdentity invertCertificate invertCertificate

parallelDAGLeaf : Flatten.FlatLeaf
  (bitInterface ∥ᵢ bitInterface)
  (bitInterface ∥ᵢ bitInterface)
parallelDAGLeaf =
  Certified.certifiedLeaf parallelDAGCertificate

parallel-DAG-output-order :
  Component.componentObserve (Flatten.leafComponent parallelDAGLeaf)
    ((low ∷ []) , (high ∷ [])) []
  ≡ ((high ∷ []) , (low ∷ []))
parallel-DAG-output-order = refl

parallel-DAG-rising-next-preserved :
  Component.componentStep (Flatten.leafComponent parallelDAGLeaf)
    Semantics.risingEdge ((low ∷ []) , (high ∷ [])) []
  ≡ appendVec
      (Component.componentStep (Flatten.leafComponent invertLeaf)
        Semantics.risingEdge (low ∷ []) [])
      (Component.componentStep (Flatten.leafComponent invertLeaf)
        Semantics.risingEdge (high ∷ []) [])
parallel-DAG-rising-next-preserved =
  refl

parallel-node-resources-concatenate :
  Flatten.leafLocalCount parallelDAGLeaf
  ≡ Flatten.leafLocalCount invertLeaf
    + Flatten.leafLocalCount invertLeaf
parallel-node-resources-concatenate =
  Compose.parallelLocalCount-correct invertNetlist invertNetlist

nestedIdentity : Provenance.ComponentIdentity
nestedIdentity = Provenance.componentIdentity  "nested.dag"

nestedLeftIdentity nestedRightIdentity : Provenance.InstanceIdentity
nestedLeftIdentity =
  Provenance.instanceIdentity (Netlist.occurrenceId ) "nested.serial"
nestedRightIdentity =
  Provenance.instanceIdentity (Netlist.occurrenceId ) "nested.invert"

nestedDAGHierarchy : Component.Component
  (bitInterface ∥ᵢ bitInterface)
  (bitInterface ∥ᵢ bitInterface)
  Semantics.Event ((Vec Bit  × Vec Bit ) × Vec Bit )
nestedDAGHierarchy =
  Component.parallelInstances nestedIdentity
    nestedLeftIdentity nestedRightIdentity
    serialDAGHierarchy (Flatten.leafComponent invertLeaf)

nestedDAGCertificate :
  Certified.ProvenanceCertifiedFlattening nestedDAGHierarchy
nestedDAGCertificate =
  Certified.parallelFlattens nestedIdentity constructedOrigin
    nestedLeftIdentity nestedRightIdentity
    serialDAGCertificate invertCertificate