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

module Tutorials.Project07.Main where

open import Spartan6.API.Hierarchy
open Interface

import Cubical.Data.Empty as Empty

bitPort : StablePort
bitPort = stablePort 70 "bit" 1

bitInterface : Interface
bitInterface = signalInterface bitPort

tutorialOrigin : Provenance.SourceOrigin
tutorialOrigin =
  Provenance.sourceOrigin noArtifact noModule []ᴸ "tutorial.inverter"
  where
  noArtifact : Maybe Netlist.ArtifactId
  noArtifact = nothing

  noModule : Maybe Netlist.ModuleId
  noModule = nothing

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

inverterOrigins : Vec Provenance.NodeOrigin 1
inverterOrigins = Provenance.nodeOrigin tutorialOrigin 0 ∷ []

inverterOriginsAccounted :
  Provenance.NodesAccountedFor
    (Provenance.leafProvenance tutorialOrigin) inverterOrigins
inverterOriginsAccounted =
  Provenance.accountedNodesNext
    (Provenance.accountedLeaf
      (Provenance.sourceWithin refl refl []ᴸ refl))
    Provenance.accountedNodesDone

inverterLeaf : Flatten.FlatLeaf bitInterface bitInterface
inverterLeaf =
  Flatten.flatLeaf 70 "inverter" tutorialOrigin
    0 1 inverterNetlist inverterOrigins

leftOccurrence rightOccurrence : Netlist.OccurrenceId
leftOccurrence = Netlist.occurrenceId 0
rightOccurrence = Netlist.occurrenceId 1

doubleIdentity : Provenance.ComponentIdentity
doubleIdentity = Provenance.componentIdentity 71 "double-inverter"

leftIdentity rightIdentity : Provenance.InstanceIdentity
leftIdentity = Provenance.instanceIdentity leftOccurrence "left-inverter"
rightIdentity = Provenance.instanceIdentity rightOccurrence "right-inverter"

inverterCertificate :
  Certified.ProvenanceCertifiedFlattening
    (Flatten.leafComponent inverterLeaf)
inverterCertificate =
  Certified.leafFlattens inverterLeaf inverterOriginsAccounted

doubleInverterHierarchy : Component.Component
  bitInterface bitInterface Semantics.Event (Vec Bit 0 × Vec Bit 0)
doubleInverterHierarchy =
  Component.serialInstances doubleIdentity leftIdentity rightIdentity
    (Flatten.leafComponent inverterLeaf)
    (Flatten.leafComponent inverterLeaf)

doubleInverterCertificate :
  Certified.ProvenanceCertifiedFlattening doubleInverterHierarchy
doubleInverterCertificate =
  Certified.serialFlattens doubleIdentity tutorialOrigin
    leftIdentity rightIdentity inverterCertificate inverterCertificate

doubleInverterLeaf : Flatten.FlatLeaf bitInterface bitInterface
doubleInverterLeaf =
  Certified.certifiedLeaf doubleInverterCertificate

flattened-double-inverter-is-identity : ∀ bit
  -> Stable.stableDirectOutputs
      (Flatten.leafNetlist doubleInverterLeaf) (bit ∷ []) []
    ≡ bit ∷ []
flattened-double-inverter-is-identity false = refl
flattened-double-inverter-is-identity true = refl

flattening-emits-the-sum-of-source-nodes :
  Flatten.leafLocalCount doubleInverterLeaf
  ≡ Flatten.leafLocalCount inverterLeaf
    + Flatten.leafLocalCount inverterLeaf
flattening-emits-the-sum-of-source-nodes =
  Compose.serialLocalCount-correct inverterNetlist inverterNetlist

flattened-node-provenance-is-accounted-for :
  Provenance.NodesAccountedFor
    (Component.componentProvenance doubleInverterHierarchy)
    (Flatten.leafNodeOrigins doubleInverterLeaf)
flattened-node-provenance-is-accounted-for =
  Certified.provenancePreserved doubleInverterCertificate

-- Feedback cannot be admitted as a combinational loop.  The only executable
-- constructor stores the feedback value as state and updates it under a guard.

pure-feedback-is-rejected :
  Feedback.checkFeedbackMode
    (Feedback.pureCombinational {Semantics.Event})
  ≡ nothing
pure-feedback-is-rejected = Feedback.pure-combinational-feedback-rejected

pure-feedback-cannot-have-admission :
  Feedback.FeedbackAdmission
    (Feedback.pureCombinational {Semantics.Event})
  -> Empty.⊥
pure-feedback-cannot-have-admission =
  Feedback.pure-combinational-feedback-impossible

risingGuard : Feedback.FeedbackGuard Semantics.Event
risingGuard = Feedback.feedbackGuard advances
  where
  advances : Semantics.Event -> Bool
  advances Semantics.idle = false
  advances Semantics.risingEdge = true

feedbackBodyIdentity : Provenance.ComponentIdentity
feedbackBodyIdentity =
  Provenance.componentIdentity 72 "feedback-body"

guardedToggleIdentity : Provenance.ComponentIdentity
guardedToggleIdentity =
  Provenance.componentIdentity 73 "guarded-toggle"

feedbackBody : Component.Component
  (emptyInterface ∥ᵢ bitInterface)
  (bitInterface ∥ᵢ bitInterface)
  Semantics.Event Unit
feedbackBody =
  Component.leafWithIdentity feedbackBodyIdentity tutorialOrigin
    (Machine.machine tt observeBody stepBody)
  where
  observeBody :
    Environment (emptyInterface ∥ᵢ bitInterface) -> Unit
    -> Environment (bitInterface ∥ᵢ bitInterface)
  observeBody (tt , bit ∷ []) state = (bit ∷ []) , (not bit ∷ [])

  stepBody : Semantics.Event
    -> Environment (emptyInterface ∥ᵢ bitInterface) -> Unit -> Unit
  stepBody event input state = tt

guardedToggle : Component.Component
  emptyInterface bitInterface Semantics.Event
  (Unit × Environment bitInterface)
guardedToggle =
  Feedback.guardedFeedbackWithIdentity guardedToggleIdentity
    risingGuard (low ∷ []) feedbackBody

guarded-feedback-is-real-state :
  Component.componentInitial guardedToggle ≡ (tt , low ∷ [])
guarded-feedback-is-real-state = refl

rising-edge-advances-the-feedback :
  Component.componentStep guardedToggle Semantics.risingEdge tt
    (Component.componentInitial guardedToggle)
  ≡ (tt , high ∷ [])
rising-edge-advances-the-feedback = refl