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

module Spartan6.Netlist.NormalizeScheduledCombinational where

open import Spartan6.Prelude

import Spartan6.Netlist.Candidate as Candidate
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.GenericBuilder as Generic
import Spartan6.Netlist.Raw as Raw
import Spartan6.Netlist.Schedule as Schedule
import Spartan6.Netlist.TopInterface as TopInterface
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

-- Purely combinational scheduled translation.  The builder's register index
-- is definitionally zero, while Schedule may reorder concrete source
-- occurrences until their GenericBuilder inputs are ready.  Scheduler failure
-- retains its concrete diagnostics; no theorem here claims that raw graph
-- acyclicity alone is sufficient for acceptance.

initialBuilder : (input-nets : List Raw.NetId)
  → Generic.Builder (lengthList input-nets) 
initialBuilder input-nets = Generic.initialBuilder input-nets []ᴸ

finishCandidate :
  (design : Raw.RawDesign)
  → Validation.StructurallyValid design
  → (input-nets : List Raw.NetId)
  → (current : Generic.Builder (lengthList input-nets) )
  → (outputs :
      List
        (Checked.Wire
          (lengthList input-nets) 
          (Generic.builderLocalCount current)))
  → Candidate.CheckedCombinationalCandidate
finishCandidate = Candidate.finishCandidate

normaliseScheduledCombinational :
  Validation.StructurallyChecked
  → Diagnostic.CheckResult
      Candidate.CheckedCombinationalCandidate
normaliseScheduledCombinational (design , structural-proof)
  with TopInterface.checkDevelopmentTarget design
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted tt
  with TopInterface.collectInputNets (Raw.rawTopPorts design)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted input-nets
  with Schedule.scheduleInstances
         (initialBuilder input-nets)
         (Raw.rawInstances design)
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted scheduled
  with TopInterface.collectBuilderOutputWires
         (Raw.rawTopPorts design)
         (Schedule.finalBuilder scheduled)
...       | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...       | Diagnostic.accepted outputs =
  Diagnostic.accepted
    (finishCandidate
      design structural-proof input-nets
      (Schedule.finalBuilder scheduled) outputs)