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

module Spartan6.Hierarchy.Component where

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

import Spartan6.Hierarchy.Provenance as Provenance
import Spartan6.Netlist.Provenance as Netlist
import Spartan6.Semantics.Machine as Machine

record Component
  (Input Output : Interface)
  (Event State : Type₀) : Type₀ where
  constructor component
  field
    componentStableId : ℕ
    componentName : String
    componentMachine :
      Machine.Machine (Environment Input) (Environment Output) Event State
    componentProvenance : Provenance.HierarchyProvenance

open Component public

leafComponent : ∀ {Input Output Event State}
  -> ℕ -> String -> Provenance.SourceOrigin
  -> Machine.Machine (Environment Input) (Environment Output) Event State
  -> Component Input Output Event State
leafComponent stable-id name origin implementation =
  component stable-id name implementation (Provenance.leafProvenance origin)

componentInitial : ∀ {Input Output Event State}
  -> Component Input Output Event State -> State
componentInitial value = Machine.initialState (componentMachine value)

componentObserve : ∀ {Input Output Event State}
  -> Component Input Output Event State
  -> Environment Input -> State -> Environment Output
componentObserve value = Machine.observe (componentMachine value)

componentStep : ∀ {Input Output Event State}
  -> Component Input Output Event State
  -> Event -> Environment Input -> State -> State
componentStep value = Machine.step (componentMachine value)

renameComponent :
  ∀ {OldInput NewInput OldOutput NewOutput Event State}
  -> ℕ -> String
  -> Renaming NewInput OldInput
  -> Renaming OldOutput NewOutput
  -> Component OldInput OldOutput Event State
  -> Component NewInput NewOutput Event State
renameComponent stable-id name input-map output-map original =
  component stable-id name
    (Machine.machine
      (componentInitial original)
      (λ input state ->
        applyRenaming output-map
          (componentObserve original (applyRenaming input-map input) state))
      (λ event input state ->
        componentStep original event (applyRenaming input-map input) state))
    (Provenance.renamedProvenance name
      (componentProvenance original))

rename-observe :
  ∀ {OldInput NewInput OldOutput NewOutput Event State}
  (stable-id : ℕ) (name : String)
  (input-map : Renaming NewInput OldInput)
  (output-map : Renaming OldOutput NewOutput)
  (original : Component OldInput OldOutput Event State)
  (input : Environment NewInput) (state : State)
  -> componentObserve
      (renameComponent stable-id name input-map output-map original)
      input state
    ≡ applyRenaming output-map
        (componentObserve original (applyRenaming input-map input) state)
rename-observe stable-id name input-map output-map original input state = refl

rename-step :
  ∀ {OldInput NewInput OldOutput NewOutput Event State}
  (stable-id : ℕ) (name : String)
  (input-map : Renaming NewInput OldInput)
  (output-map : Renaming OldOutput NewOutput)
  (original : Component OldInput OldOutput Event State)
  event (input : Environment NewInput) (state : State)
  -> componentStep
      (renameComponent stable-id name input-map output-map original)
      event input state
    ≡ componentStep original event (applyRenaming input-map input) state
rename-step stable-id name input-map output-map original event input state = refl

serial : ∀ {Input Middle Output Event LeftState RightState}
  -> ℕ -> String
  -> Component Input Middle Event LeftState
  -> Component Middle Output Event RightState
  -> Component Input Output Event (LeftState × RightState)
serial stable-id name first second =
  component stable-id name
    (Machine.machine
      (componentInitial first , componentInitial second)
      (λ input states ->
        componentObserve second
          (componentObserve first input (fst states))
          (snd states))
      (λ event input states ->
        componentStep first event input (fst states)
        , componentStep second event
            (componentObserve first input (fst states))
            (snd states)))
    (Provenance.serialProvenance
      (componentProvenance first) (componentProvenance second))

serial-observe : ∀ {Input Middle Output Event LeftState RightState}
  (stable-id : ℕ) (name : String)
  (first : Component Input Middle Event LeftState)
  (second : Component Middle Output Event RightState)
  input (left-state : LeftState) (right-state : RightState)
  -> componentObserve (serial stable-id name first second)
      input (left-state , right-state)
    ≡ componentObserve second
        (componentObserve first input left-state) right-state
serial-observe stable-id name first second input left-state right-state = refl

serial-step : ∀ {Input Middle Output Event LeftState RightState}
  (stable-id : ℕ) (name : String)
  (first : Component Input Middle Event LeftState)
  (second : Component Middle Output Event RightState)
  event input (left-state : LeftState) (right-state : RightState)
  -> componentStep (serial stable-id name first second)
      event input (left-state , right-state)
    ≡ (componentStep first event input left-state
      , componentStep second event
          (componentObserve first input left-state) right-state)
serial-step stable-id name first second event input left-state right-state = refl

parallel :
  ∀ {LeftInput RightInput LeftOutput RightOutput Event LeftState RightState}
  -> ℕ -> String
  -> Component LeftInput LeftOutput Event LeftState
  -> Component RightInput RightOutput Event RightState
  -> Component
      (LeftInput ∥ᵢ RightInput)
      (LeftOutput ∥ᵢ RightOutput)
      Event (LeftState × RightState)
parallel stable-id name left right =
  component stable-id name
    (Machine.machine
      (componentInitial left , componentInitial right)
      (λ input states ->
        componentObserve left (fst input) (fst states)
        , componentObserve right (snd input) (snd states))
      (λ event input states ->
        componentStep left event (fst input) (fst states)
        , componentStep right event (snd input) (snd states)))
    (Provenance.parallelProvenance
      (componentProvenance left) (componentProvenance right))

parallel-observe :
  ∀ {LeftInput RightInput LeftOutput RightOutput Event LeftState RightState}
  (stable-id : ℕ) (name : String)
  (left : Component LeftInput LeftOutput Event LeftState)
  (right : Component RightInput RightOutput Event RightState)
  (left-input : Environment LeftInput)
  (right-input : Environment RightInput)
  (left-state : LeftState) (right-state : RightState)
  -> componentObserve (parallel stable-id name left right)
      (left-input , right-input) (left-state , right-state)
    ≡ (componentObserve left left-input left-state
      , componentObserve right right-input right-state)
parallel-observe stable-id name left right
  left-input right-input left-state right-state = refl

parallel-step :
  ∀ {LeftInput RightInput LeftOutput RightOutput Event LeftState RightState}
  (stable-id : ℕ) (name : String)
  (left : Component LeftInput LeftOutput Event LeftState)
  (right : Component RightInput RightOutput Event RightState)
  event
  (left-input : Environment LeftInput)
  (right-input : Environment RightInput)
  (left-state : LeftState) (right-state : RightState)
  -> componentStep (parallel stable-id name left right)
      event (left-input , right-input) (left-state , right-state)
    ≡ (componentStep left event left-input left-state
      , componentStep right event right-input right-state)
parallel-step stable-id name left right event
  left-input right-input left-state right-state = refl

hideOutputs : ∀ {Input FullOutput VisibleOutput Event State}
  -> ℕ -> String
  -> Renaming FullOutput VisibleOutput
  -> Component Input FullOutput Event State
  -> Component Input VisibleOutput Event State
hideOutputs stable-id name projection original =
  component stable-id name
    (Machine.machine
      (componentInitial original)
      (λ input state ->
        applyRenaming projection (componentObserve original input state))
      (componentStep original))
    (Provenance.hiddenProvenance name (componentProvenance original))

hideOutputs-observe : ∀ {Input FullOutput VisibleOutput Event State}
  (stable-id : ℕ) (name : String)
  (projection : Renaming FullOutput VisibleOutput)
  (original : Component Input FullOutput Event State)
  input state
  -> componentObserve (hideOutputs stable-id name projection original)
      input state
    ≡ applyRenaming projection (componentObserve original input state)
hideOutputs-observe stable-id name projection original input state = refl

bindHiddenInput : ∀ {VisibleInput HiddenInput Output Event State}
  -> ℕ -> String
  -> Environment HiddenInput
  -> Component (VisibleInput ∥ᵢ HiddenInput) Output Event State
  -> Component VisibleInput Output Event State
bindHiddenInput stable-id name hidden original =
  component stable-id name
    (Machine.machine
      (componentInitial original)
      (λ input state -> componentObserve original (input , hidden) state)
      (λ event input state ->
        componentStep original event (input , hidden) state))
    (Provenance.hiddenProvenance name (componentProvenance original))

bindHiddenInput-observe : ∀ {VisibleInput HiddenInput Output Event State}
  (stable-id : ℕ) (name : String)
  (hidden : Environment HiddenInput)
  (original : Component (VisibleInput ∥ᵢ HiddenInput) Output Event State)
  input state
  -> componentObserve (bindHiddenInput stable-id name hidden original)
      input state
    ≡ componentObserve original (input , hidden) state
bindHiddenInput-observe stable-id name hidden original input state = refl

instantiate : ∀ {Input Output Event State}
  -> Netlist.OccurrenceId -> String
  -> Component Input Output Event State
  -> Component Input Output Event State
instantiate occurrence name original =
  component (Netlist.occurrenceOrdinal occurrence) name
    (componentMachine original)
    (Provenance.instantiatedProvenance occurrence name
      (componentProvenance original))

instantiate-observe : ∀ {Input Output Event State}
  (occurrence : Netlist.OccurrenceId) (name : String)
  (original : Component Input Output Event State)
  input state
  -> componentObserve (instantiate occurrence name original) input state
    ≡ componentObserve original input state
instantiate-observe occurrence name original input state = refl

instantiate-step : ∀ {Input Output Event State}
  (occurrence : Netlist.OccurrenceId) (name : String)
  (original : Component Input Output Event State)
  event input state
  -> componentStep (instantiate occurrence name original) event input state
    ≡ componentStep original event input state
instantiate-step occurrence name original event input state = refl

reuse-observation-under-instantiation :
  ∀ {Input Output Event State}
  (occurrence : Netlist.OccurrenceId) (name : String)
  (original : Component Input Output Event State)
  (input : Environment Input) (state : State)
  (expected : Environment Output)
  -> componentObserve original input state ≡ expected
  -> componentObserve (instantiate occurrence name original) input state
    ≡ expected
reuse-observation-under-instantiation occurrence name original
  input state expected theorem = theorem

-- Metadata-coherent construction -----------------------------------------

-- These additive constructors package identities once and ensure that
-- composed children are instantiated in the same hierarchy tree from which
-- certified flattening later derives occurrence paths.  The positional APIs
-- above remain compatibility wrappers.

leafWithIdentity : ∀ {Input Output Event State}
  -> Provenance.ComponentIdentity
  -> Provenance.SourceOrigin
  -> Machine.Machine (Environment Input) (Environment Output) Event State
  -> Component Input Output Event State
leafWithIdentity identity origin implementation =
  leafComponent
    (Provenance.identityStableId identity)
    (Provenance.identityName identity)
    origin implementation

serialWithIdentity : ∀ {Input Middle Output Event LeftState RightState}
  -> Provenance.ComponentIdentity
  -> Component Input Middle Event LeftState
  -> Component Middle Output Event RightState
  -> Component Input Output Event (LeftState × RightState)
serialWithIdentity identity left right =
  serial
    (Provenance.identityStableId identity)
    (Provenance.identityName identity)
    left right

parallelWithIdentity :
  ∀ {LeftInput RightInput LeftOutput RightOutput Event LeftState RightState}
  -> Provenance.ComponentIdentity
  -> Component LeftInput LeftOutput Event LeftState
  -> Component RightInput RightOutput Event RightState
  -> Component
      (LeftInput ∥ᵢ RightInput)
      (LeftOutput ∥ᵢ RightOutput)
      Event (LeftState × RightState)
parallelWithIdentity identity left right =
  parallel
    (Provenance.identityStableId identity)
    (Provenance.identityName identity)
    left right

instantiateWithIdentity : ∀ {Input Output Event State}
  -> Provenance.InstanceIdentity
  -> Component Input Output Event State
  -> Component Input Output Event State
instantiateWithIdentity identity original =
  instantiate
    (Provenance.instanceOccurrence identity)
    (Provenance.instanceName identity)
    original

serialInstances : ∀ {Input Middle Output Event LeftState RightState}
  -> Provenance.ComponentIdentity
  -> Provenance.InstanceIdentity
  -> Provenance.InstanceIdentity
  -> Component Input Middle Event LeftState
  -> Component Middle Output Event RightState
  -> Component Input Output Event (LeftState × RightState)
serialInstances identity left-identity right-identity left right =
  serialWithIdentity identity
    (instantiateWithIdentity left-identity left)
    (instantiateWithIdentity right-identity right)

parallelInstances :
  ∀ {LeftInput RightInput LeftOutput RightOutput Event LeftState RightState}
  -> Provenance.ComponentIdentity
  -> Provenance.InstanceIdentity
  -> Provenance.InstanceIdentity
  -> Component LeftInput LeftOutput Event LeftState
  -> Component RightInput RightOutput Event RightState
  -> Component
      (LeftInput ∥ᵢ RightInput)
      (LeftOutput ∥ᵢ RightOutput)
      Event (LeftState × RightState)
parallelInstances identity left-identity right-identity left right =
  parallelWithIdentity identity
    (instantiateWithIdentity left-identity left)
    (instantiateWithIdentity right-identity right)