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

module Spartan6.Netlist.DecodedOperation where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Import.Artifact as Artifact
import Spartan6.Netlist.Provenance as Provenance
import Spartan6.Netlist.Raw as Raw
import Spartan6.Netlist.ReadySchedule as Schedule
import Spartan6.Validation.DecodedDesign as Decoded
import Spartan6.Validation.Design as Validated
import Spartan6.Validation.Raw as Legacy

open import Cubical.Data.Bool.Properties using (false≢true)
import Cubical.Data.Empty as Empty

record TypedOperation : Type₀ where
  constructor typedOperation
  field
    typedOperationId : Provenance.OccurrenceId
    sourceOccurrence : Raw.RawInstance
    decodedOccurrence :
      Decoded.DecodedOccurrence typedOperationId sourceOccurrence
    scheduleOperation : Schedule.Operation
    scheduleOperation-id :
      Schedule.operationId scheduleOperation ≡ typedOperationId

open TypedOperation public

toTypedOperation : ∀ {identifier source}
  → Decoded.DecodedOccurrence identifier source → TypedOperation
toTypedOperation {identifier} {source} decoded =
  typedOperation identifier source decoded
    (Schedule.operation identifier
      (Legacy.instanceSinks source) (Legacy.instanceDrivers source))
    refl

operationsFrom : ∀ {next sources}
  → Decoded.DecodedOccurrences next sources → List TypedOperation
operationsFrom Decoded.decodedDone = []ᴸ
operationsFrom (Decoded.decodedNext decoded rest) =
  toTypedOperation decoded ∷ᴸ operationsFrom rest

statefulKind? : Architecture.PrimitiveKind → Bool
statefulKind? kind with Architecture.stateBitCount kind
... | zero = false
... | suc count = true

typedStateful? : TypedOperation → Bool
typedStateful? item =
  statefulKind?
    (Decoded.decodedKind (decodedOccurrence item))

record OperationPlan : Type₀ where
  constructor operationPlan
  field
    allTypedOperations : List TypedOperation
    stateOperations : List TypedOperation
    combinationalTypedOperations : List TypedOperation
    combinationalOperations : List Schedule.Operation
    initiallyAvailableNets : List Raw.NetId

open OperationPlan public

addTopInputs : Raw.RawDesign → List Raw.NetId
addTopInputs design =
  Legacy.concatMapList Legacy.topPortDrivers (Raw.rawTopPorts design)

prependState : TypedOperation → OperationPlan → OperationPlan
prependState item
  (operationPlan all stateful combinational metadata available) =
  operationPlan (item ∷ᴸ all) (item ∷ᴸ stateful)
    combinational metadata available

prependCombinational : TypedOperation → OperationPlan → OperationPlan
prependCombinational item
  (operationPlan all stateful combinational metadata available) =
  operationPlan (item ∷ᴸ all) stateful
    (item ∷ᴸ combinational)
    (scheduleOperation item ∷ᴸ metadata) available

partitionFrom : List Raw.NetId → List TypedOperation → OperationPlan
partitionFrom available []ᴸ =
  operationPlan []ᴸ []ᴸ []ᴸ []ᴸ available
partitionFrom available (item ∷ᴸ items) with typedStateful? item
... | true = prependState item
  (partitionFrom
    (Schedule.producedNets (scheduleOperation item) ++ᴸ available) items)
... | false = prependCombinational item (partitionFrom available items)

planValidated : ∀ {artifact : Artifact.RawArtifact}
  → Validated.ValidatedDesign artifact → OperationPlan
planValidated {artifact} validated =
  partitionFrom
    (addTopInputs (Artifact.decodedDesign artifact))
    (operationsFrom
      (Decoded.decodedOccurrences (Validated.decoded validated)))

state-outputs-are-preallocated : ∀ available item items
  → typedStateful? item ≡ true
  → OperationPlan.initiallyAvailableNets
      (partitionFrom available (item ∷ᴸ items))
    ≡ OperationPlan.initiallyAvailableNets
      (partitionFrom
        (Schedule.producedNets (scheduleOperation item) ++ᴸ available)
        items)
state-outputs-are-preallocated available item items stateful
  with typedStateful? item
... | true = refl
... | false = Empty.rec (false≢true stateful)