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

module Spartan6.Hierarchy.Feedback 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.Provenance as Provenance
import Spartan6.Semantics.Machine as Machine

record FeedbackGuard (Event : Type₀) : Type₀ where
  constructor feedbackGuard
  field advancesFeedback : Event -> Bool

open FeedbackGuard public

data FeedbackMode (Event : Type₀) : Type₀ where
  pureCombinational : FeedbackMode Event
  stateGuarded : FeedbackGuard Event -> FeedbackMode Event

data FeedbackAdmission {Event : Type₀} : FeedbackMode Event -> Type₀ where
  guardedAdmission : (guard : FeedbackGuard Event)
    -> FeedbackAdmission (stateGuarded guard)

checkFeedbackMode : ∀ {Event} (mode : FeedbackMode Event)
  -> Maybe (FeedbackAdmission mode)
checkFeedbackMode pureCombinational = nothing
checkFeedbackMode (stateGuarded guard) = just (guardedAdmission guard)

pure-combinational-feedback-rejected : ∀ {Event}
  -> checkFeedbackMode (pureCombinational {Event}) ≡ nothing
pure-combinational-feedback-rejected = refl

pure-combinational-feedback-impossible : ∀ {Event}
  -> FeedbackAdmission (pureCombinational {Event}) -> Empty.⊥
pure-combinational-feedback-impossible ()

guardedFeedback :
  ∀ {ExternalInput ExternalOutput Feedback Event State}
  -> ℕ -> String
  -> FeedbackGuard Event
  -> Environment Feedback
  -> Component.Component
      (ExternalInput ∥ᵢ Feedback)
      (ExternalOutput ∥ᵢ Feedback)
      Event State
  -> Component.Component
      ExternalInput ExternalOutput Event
      (State × Environment Feedback)
guardedFeedback stable-id name guard initial-feedback original =
  Component.component stable-id name
    (Machine.machine
      (Component.componentInitial original , initial-feedback)
      (λ input state ->
        fst
          (Component.componentObserve original
            (input , snd state) (fst state)))
      (λ event input state ->
        (Component.componentStep original event
          (input , snd state) (fst state)
        , (if advancesFeedback guard event
           then snd
             (Component.componentObserve original
               (input , snd state) (fst state))
           else snd state))))
    (Provenance.feedbackProvenance name
      (Component.componentProvenance original))

guarded-feedback-observe :
  ∀ {ExternalInput ExternalOutput Feedback Event State}
  (stable-id : ℕ) (name : String)
  (guard : FeedbackGuard Event)
  (initial-feedback : Environment Feedback)
  (original : Component.Component
    (ExternalInput ∥ᵢ Feedback)
    (ExternalOutput ∥ᵢ Feedback)
    Event State)
  input (state : State) (feedback : Environment Feedback)
  -> Component.componentObserve
      (guardedFeedback stable-id name guard initial-feedback original)
      input (state , feedback)
    ≡ fst
        (Component.componentObserve original
          (input , feedback) state)
guarded-feedback-observe stable-id name guard initial-feedback
  original input state feedback = refl

guarded-feedback-step :
  ∀ {ExternalInput ExternalOutput Feedback Event State}
  (stable-id : ℕ) (name : String)
  (guard : FeedbackGuard Event)
  (initial-feedback : Environment Feedback)
  (original : Component.Component
    (ExternalInput ∥ᵢ Feedback)
    (ExternalOutput ∥ᵢ Feedback)
    Event State)
  event input (state : State) (feedback : Environment Feedback)
  -> Component.componentStep
      (guardedFeedback stable-id name guard initial-feedback original)
      event input (state , feedback)
    ≡ (Component.componentStep original event
          (input , feedback) state
      , (if advancesFeedback guard event
         then snd
           (Component.componentObserve original
             (input , feedback) state)
         else feedback))
guarded-feedback-step stable-id name guard initial-feedback
  original event input state feedback = refl

guardedFeedbackWithIdentity :
  ∀ {ExternalInput ExternalOutput Feedback Event State}
  -> Provenance.ComponentIdentity
  -> FeedbackGuard Event
  -> Environment Feedback
  -> Component.Component
      (ExternalInput ∥ᵢ Feedback)
      (ExternalOutput ∥ᵢ Feedback)
      Event State
  -> Component.Component
      ExternalInput ExternalOutput Event
      (State × Environment Feedback)
guardedFeedbackWithIdentity identity =
  guardedFeedback
    (Provenance.identityStableId identity)
    (Provenance.identityName identity)