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

module Spartan6.Semantics.Design where

open import Spartan6.Prelude
open import Spartan6.Netlist.Expression

data Event : Type₀ where
  idle       : Event
  risingEdge : Event

record Design (inputCount outputCount registerCount : ℕ) : Type₀ where
  constructor mkDesign
  field
    initialState      : Vec Bit registerCount
    outputExpressions : Vec (Expr inputCount registerCount) outputCount
    nextExpressions   : Vec (Expr inputCount registerCount) registerCount

open Design public

-- The common stateless case should not require callers to repeat two empty
-- vectors.  The result is still the established `Design` representation, so
-- existing evaluators and theorems apply without conversion.

combinationalDesign : ∀ {inputCount outputCount}
  → Vec (Expr inputCount ) outputCount
  → Design inputCount outputCount 
combinationalDesign outputs = mkDesign [] outputs []

Inputs : ∀ {inputCount outputCount registerCount}
       → Design inputCount outputCount registerCount → Type₀
Inputs {inputCount} d = Vec Bit inputCount

State : ∀ {inputCount outputCount registerCount}
      → Design inputCount outputCount registerCount → Type₀
State {registerCount = registerCount} d = Vec Bit registerCount

Observation : ∀ {inputCount outputCount registerCount}
            → Design inputCount outputCount registerCount → Type₀
Observation {outputCount = outputCount} d = Vec Bit outputCount

observe : ∀ {inputCount outputCount registerCount}
        → (design : Design inputCount outputCount registerCount)
        → Inputs design
        → State design
        → Observation design
observe design external state =
  evalAll external state (outputExpressions design)

step : ∀ {inputCount outputCount registerCount}
     → (design : Design inputCount outputCount registerCount)
     → Event
     → Inputs design
     → State design
     → State design
step design idle external state = state
step design risingEdge external state =
  evalAll external state (nextExpressions design)

initial : ∀ {inputCount outputCount registerCount}
        → (design : Design inputCount outputCount registerCount)
        → State design
initial = initialState

ObservationOf : ∀ {inputCount outputCount registerCount}
              → (design : Design inputCount outputCount registerCount)
              → Inputs design → State design → Observation design → Type₀
ObservationOf design external state result =
  observe design external state ≡ result

Transition : ∀ {inputCount outputCount registerCount}
           → (design : Design inputCount outputCount registerCount)
           → Event → Inputs design → State design → State design → Type₀
Transition design event external before after =
  step design event external before ≡ after

observation-deterministic :
  ∀ {inputCount outputCount registerCount}
    {design : Design inputCount outputCount registerCount}
    {external : Inputs design} {state : State design}
    {left right : Observation design}
  → ObservationOf design external state left
  → ObservationOf design external state right
  → left ≡ right
observation-deterministic left-path right-path =
  sym left-path ∙ right-path

transition-deterministic :
  ∀ {inputCount outputCount registerCount}
    {design : Design inputCount outputCount registerCount}
    {event : Event} {external : Inputs design} {before : State design}
    {left right : State design}
  → Transition design event external before left
  → Transition design event external before right
  → left ≡ right
transition-deterministic left-path right-path =
  sym left-path ∙ right-path

idle-holds :
  ∀ {inputCount outputCount registerCount}
    (design : Design inputCount outputCount registerCount)
    (external : Inputs design) (state : State design)
  → step design idle external state ≡ state
idle-holds design external state = refl

combinational-step-empty : ∀ {inputCount outputCount}
  (outputs : Vec (Expr inputCount ) outputCount)
  (event : Event) (external : Vec Bit inputCount)
  → step (combinationalDesign outputs) event external [] ≡ []
combinational-step-empty outputs idle external = refl
combinational-step-empty outputs risingEdge external = refl

record Stimulus (inputCount : ℕ) : Type₀ where
  constructor stimulus
  field
    stimulusInputs : Vec Bit inputCount
    stimulusEvent  : Event

open Stimulus public

record Frame (outputCount registerCount : ℕ) : Type₀ where
  constructor frame
  field
    frameObservation : Vec Bit outputCount
    frameStateBefore : Vec Bit registerCount
    frameStateAfter  : Vec Bit registerCount

open Frame public

run : ∀ {inputCount outputCount registerCount}
    → (design : Design inputCount outputCount registerCount)
    → State design
    → List (Stimulus inputCount)
    → State design
run design state []ᴸ = state
run design state (sample ∷ᴸ samples) =
  run design
      (step design (stimulusEvent sample) (stimulusInputs sample) state)
      samples

execute : ∀ {inputCount outputCount registerCount}
        → (design : Design inputCount outputCount registerCount)
        → State design
        → List (Stimulus inputCount)
        → List (Frame outputCount registerCount)
execute design state []ᴸ = []ᴸ
execute design state (sample ∷ᴸ samples) =
  frame (observe design (stimulusInputs sample) state)
        state
        next-state
  ∷ᴸ execute design next-state samples
  where
  next-state : State design
  next-state =
    step design (stimulusEvent sample) (stimulusInputs sample) state