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

module Spartan6.Examples.HierarchyFeedback where

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

import Cubical.Data.Empty as Empty
import Spartan6.Hierarchy.Component as Component
import Spartan6.Hierarchy.Feedback as Feedback
import Spartan6.Hierarchy.FeedbackFlattening as FeedbackFlattening
import Spartan6.Hierarchy.FlatMachine as Flat
import Spartan6.Hierarchy.Provenance as Provenance
import Spartan6.Netlist.Provenance as Netlist
import Spartan6.Semantics.Machine as Machine

feedbackPort : StablePort
feedbackPort = stablePort  "feedback" 

outputPort : StablePort
outputPort = stablePort  "q" 

feedbackInterface : Interface
feedbackInterface = signalInterface feedbackPort

outputInterface : Interface
outputInterface = signalInterface outputPort

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

  noModule : Maybe Netlist.ModuleId
  noModule = nothing

toggleObserve :
  Environment (emptyInterface ∥ᵢ feedbackInterface)
  -> Unit
  -> Environment (outputInterface ∥ᵢ feedbackInterface)
toggleObserve (tt , bit ∷ []) state =
  (bit ∷ []) , (not bit ∷ [])

toggleStep : Bool
  -> Environment (emptyInterface ∥ᵢ feedbackInterface)
  -> Unit -> Unit
toggleStep event input state = tt

combinationalToggleBody : Component.Component
  (emptyInterface ∥ᵢ feedbackInterface)
  (outputInterface ∥ᵢ feedbackInterface)
  Bool Unit
combinationalToggleBody =
  Component.leafComponent  "toggle-body" toggleOrigin
    (Machine.machine tt toggleObserve toggleStep)

risingGuard : Feedback.FeedbackGuard Bool
risingGuard = Feedback.feedbackGuard (λ event -> event)

feedbackToggleIdentity : Provenance.ComponentIdentity
feedbackToggleIdentity =
  Provenance.componentIdentity  "feedback-toggle"

feedbackToggle : Component.Component
  emptyInterface outputInterface Bool
  (Unit × Environment feedbackInterface)
feedbackToggle =
  Feedback.guardedFeedbackWithIdentity feedbackToggleIdentity
    risingGuard (low ∷ []) combinationalToggleBody

feedback-is-explicit-state :
  Component.componentInitial feedbackToggle ≡ (tt , low ∷ [])
feedback-is-explicit-state = refl

feedback-toggle-starts-low :
  Component.componentObserve feedbackToggle tt
    (Component.componentInitial feedbackToggle)
  ≡ low ∷ []
feedback-toggle-starts-low = refl

guarded-edge-toggles-high :
  Component.componentStep feedbackToggle true tt
    (Component.componentInitial feedbackToggle)
  ≡ (tt , high ∷ [])
guarded-edge-toggles-high = refl

unguarded-event-holds-feedback :
  Component.componentStep feedbackToggle false tt
    (tt , high ∷ [])
  ≡ (tt , high ∷ [])
unguarded-event-holds-feedback = refl

second-guarded-edge-toggles-low :
  Component.componentStep feedbackToggle true tt
    (Component.componentStep feedbackToggle true tt
      (Component.componentInitial feedbackToggle))
  ≡ Component.componentInitial feedbackToggle
second-guarded-edge-toggles-low = refl

twoEdges : List (Machine.Stimulus (Environment emptyInterface) Bool)
twoEdges =
  Machine.stimulus tt true
  ∷ᴸ Machine.stimulus tt true
  ∷ᴸ []ᴸ

feedback-toggle-trace-returns-to-initial :
  Machine.run (Component.componentMachine feedbackToggle)
    (Component.componentInitial feedbackToggle) twoEdges
  ≡ Component.componentInitial feedbackToggle
feedback-toggle-trace-returns-to-initial = refl

pure-feedback-check-is-rejection :
  Feedback.checkFeedbackMode (Feedback.pureCombinational {Bool}) ≡ nothing
pure-feedback-check-is-rejection =
  Feedback.pure-combinational-feedback-rejected

pure-feedback-has-no-admission :
  Feedback.FeedbackAdmission (Feedback.pureCombinational {Bool})
  -> Empty.⊥
pure-feedback-has-no-admission =
  Feedback.pure-combinational-feedback-impossible

guarded-feedback-is-admitted :
  Feedback.checkFeedbackMode (Feedback.stateGuarded risingGuard)
  ≡ just (Feedback.guardedAdmission risingGuard)
guarded-feedback-is-admitted = refl

-- Flat lowering is a separate claim.  The body has no state bits; the
-- feedback environment receives one bit only through an explicit allocation
-- contract.  This keeps guarded hierarchy construction usable even when no
-- bit layout is available.

toggleBodyIdentity : Provenance.ComponentIdentity
toggleBodyIdentity = Provenance.componentIdentity  "toggle-body"

toggleBodyFlatTarget : Flat.FlatMachine
  (emptyInterface ∥ᵢ feedbackInterface)
  (outputInterface ∥ᵢ feedbackInterface)
  Bool
toggleBodyFlatTarget =
  Flat.flatMachine toggleBodyIdentity
    (Provenance.leafProvenance toggleOrigin) 
    (Machine.machine [] observe-flat step-flat)
  where
  observe-flat :
    Environment (emptyInterface ∥ᵢ feedbackInterface)
    -> Vec Bit 
    -> Environment (outputInterface ∥ᵢ feedbackInterface)
  observe-flat input state = toggleObserve input tt

  step-flat : Bool
    -> Environment (emptyInterface ∥ᵢ feedbackInterface)
    -> Vec Bit  -> Vec Bit 
  step-flat event input state = []

toggleBodyFlattening :
  Flat.CertifiedMachineFlattening combinationalToggleBody
Flat.flatTarget toggleBodyFlattening = toggleBodyFlatTarget
Flat.StateRelation toggleBodyFlattening semantic-state flat-state = Unit
Flat.initialRelated toggleBodyFlattening = tt
Flat.observationPreserved toggleBodyFlattening
  input semantic-state flat-state related = refl
Flat.transitionPreserved toggleBodyFlattening
  event input semantic-state flat-state related = tt
Flat.provenanceRetained toggleBodyFlattening = refl

feedbackAllocation :
  FeedbackFlattening.FeedbackAllocation feedbackInterface
feedbackAllocation =
  FeedbackFlattening.interfaceFeedbackAllocation feedbackInterface

feedbackToggleFlattening :
  Flat.CertifiedMachineFlattening feedbackToggle
feedbackToggleFlattening =
  FeedbackFlattening.feedbackFlattens
    feedbackToggleIdentity risingGuard (low ∷ [])
    feedbackAllocation toggleBodyFlattening

flat-feedback-state-is-explicitly-allocated :
  Flat.flatStateCount (Flat.flatTarget feedbackToggleFlattening) ≡ 
flat-feedback-state-is-explicitly-allocated = refl

flat-guarded-edge-toggles-high :
  Flat.flatStep (Flat.flatTarget feedbackToggleFlattening)
    true tt (Flat.flatInitial (Flat.flatTarget feedbackToggleFlattening))
  ≡ high ∷ []
flat-guarded-edge-toggles-high = refl

feedback-flattening-preserves-the-guarded-step :
  Flat.StateRelation feedbackToggleFlattening
    (Component.componentStep feedbackToggle true tt
      (Component.componentInitial feedbackToggle))
    (Flat.flatStep (Flat.flatTarget feedbackToggleFlattening)
      true tt (Flat.flatInitial (Flat.flatTarget feedbackToggleFlattening)))
feedback-flattening-preserves-the-guarded-step =
  Flat.transitionPreserved feedbackToggleFlattening
    true tt (tt , low ∷ []) (low ∷ []) (tt , refl)