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

module Spartan6.Netlist.Schedule where

open import Spartan6.Prelude
open import Spartan6.Validation.CycleSoundness
  using (_∈_; here; there)

import Spartan6.Netlist.GenericBuilder as Generic
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic

private
  variable
    ℓ : Level

-- Occurrence-sensitive removal is the provenance primitive.  Equal-valued
-- duplicate instances remain distinct list occurrences, just as dependency
-- edges do in CycleFuel.

data Removed {A : Type ℓ} (item : A) : List A → List A → Type ℓ where
  removeHere : ∀ {items}
    → Removed item (item ∷ᴸ items) items

  removeThere : ∀ {other items remaining}
    → Removed item items remaining
    → Removed item
        (other ∷ᴸ items) (other ∷ᴸ remaining)

removed-item-listed : ∀ {A : Type ℓ} {item : A} {items remaining}
  → Removed item items remaining
  → item ∈ items
removed-item-listed removeHere = here
removed-item-listed (removeThere removed) =
  there (removed-item-listed removed)

removed-retains : ∀ {A : Type ℓ} {item other : A} {items remaining}
  → Removed item items remaining
  → other ∈ remaining
  → other ∈ items
removed-retains removeHere membership = there membership
removed-retains (removeThere removed) here = here
removed-retains (removeThere removed) (there membership) =
  there (removed-retains removed membership)

removed-length : ∀ {A : Type ℓ} {item : A} {items remaining}
  → Removed item items remaining
  → lengthList items ≡ suc (lengthList remaining)
removed-length removeHere = refl
removed-length (removeThere removed) =
  cong suc (removed-length removed)

-- A successful scan returns the first instance that GenericBuilder can
-- process with the current bindings.  Its certificate retains the exact
-- source occurrence, the list with that occurrence removed, and the checked
-- processing equation.

record BuildableSelection
  {inputCount registerCount : ℕ}
  (current : Generic.Builder inputCount registerCount)
  (source : List Raw.RawInstance)
  : Type₀ where
  field
    selectedInstance : Raw.RawInstance
    remainingInstances : List Raw.RawInstance
    nextBuilder : Generic.Builder inputCount registerCount
    selectedRemoved :
      Removed selectedInstance source remainingInstances
    selectedProcessed :
      Generic.processInstance selectedInstance current
      ≡ Diagnostic.accepted nextBuilder

open BuildableSelection public

skipSelection : ∀ {inputCount registerCount}
  → (skipped : Raw.RawInstance)
  → {current : Generic.Builder inputCount registerCount}
  → {items : List Raw.RawInstance}
  → BuildableSelection current items
  → BuildableSelection current (skipped ∷ᴸ items)
skipSelection skipped selection =
  record
    { selectedInstance = selectedInstance selection
    ; remainingInstances =
        skipped ∷ᴸ remainingInstances selection
    ; nextBuilder = nextBuilder selection
    ; selectedRemoved =
        removeThere (selectedRemoved selection)
    ; selectedProcessed = selectedProcessed selection
    }

singleton : Diagnostic.Diagnostic → Diagnostic.Diagnostics
singleton item = item ∷ᴸ []ᴸ

noBuildableDiagnostic : Diagnostic.Diagnostic
noBuildableDiagnostic =
  Diagnostic.diagnostic
    Diagnostic.combinationalLoop
    Diagnostic.reject
    "combinational scheduler"
    "a remaining instance whose checked inputs are already bound"
    "no processable remaining instance"
    "This can mean a combinational cycle, an undriven/forward-only component, or an independently invalid/unsupported primitive; preceding diagnostics retain each concrete builder failure."

fuelDiagnostic : Diagnostic.Diagnostic
fuelDiagnostic =
  Diagnostic.diagnostic
    Diagnostic.unsupportedMode
    Diagnostic.reject
    "combinational scheduler fuel"
    "one removal step per remaining instance"
    "the explicit bound was exhausted"
    "scheduleInstances supplies the source length, so this branch is exposed only for direct callers of scheduleFuel with a smaller bound."

selectBuildable : ∀ {inputCount registerCount}
  → (current : Generic.Builder inputCount registerCount)
  → (items : List Raw.RawInstance)
  → Diagnostic.CheckResult (BuildableSelection current items)
selectBuildable current []ᴸ =
  Diagnostic.rejected (singleton noBuildableDiagnostic)
selectBuildable current (item ∷ᴸ items)
  with Generic.processInstance item current UsingEq
... | Diagnostic.accepted next , processed-path =
  Diagnostic.accepted
    record
      { selectedInstance = item
      ; remainingInstances = items
      ; nextBuilder = next
      ; selectedRemoved = removeHere
      ; selectedProcessed = processed-path
      }
... | Diagnostic.rejected item-diagnostics , processed-path
  with selectBuildable current items
...   | Diagnostic.accepted selection =
  Diagnostic.accepted (skipSelection item selection)
...   | Diagnostic.rejected later-diagnostics =
  Diagnostic.rejected (item-diagnostics ++ᴸ later-diagnostics)

-- A trace certifies both ordering and builder readiness.  scheduleNext says
-- that one concrete source occurrence was removed and successfully processed
-- before the certified suffix.

data ScheduleTrace {inputCount registerCount : ℕ}
  : Generic.Builder inputCount registerCount
  → List Raw.RawInstance
  → List Raw.RawInstance
  → Generic.Builder inputCount registerCount
  → Type₀ where
  scheduleDone : ∀ {current}
    → ScheduleTrace current []ᴸ []ᴸ current

  scheduleNext :
    ∀ {current source selected remaining next scheduled final}
    → Removed selected source remaining
    → Generic.processInstance selected current
      ≡ Diagnostic.accepted next
    → ScheduleTrace next remaining scheduled final
    → ScheduleTrace
        current source (selected ∷ᴸ scheduled) final

record Scheduled
  {inputCount registerCount : ℕ}
  (initial : Generic.Builder inputCount registerCount)
  (source : List Raw.RawInstance)
  : Type₀ where
  field
    scheduledInstances : List Raw.RawInstance
    finalBuilder : Generic.Builder inputCount registerCount
    schedulingTrace :
      ScheduleTrace initial source scheduledInstances finalBuilder

open Scheduled public

scheduleFuel : ∀ {inputCount registerCount}
  → ℕ
  → (current : Generic.Builder inputCount registerCount)
  → (items : List Raw.RawInstance)
  → Diagnostic.CheckResult (Scheduled current items)
scheduleFuel fuel current []ᴸ =
  Diagnostic.accepted
    record
      { scheduledInstances = []ᴸ
      ; finalBuilder = current
      ; schedulingTrace = scheduleDone
      }
scheduleFuel zero current (item ∷ᴸ items) =
  Diagnostic.rejected (singleton fuelDiagnostic)
scheduleFuel (suc fuel) current items
  with selectBuildable current items
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted selection
  with scheduleFuel fuel
    (nextBuilder selection) (remainingInstances selection)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted suffix =
  Diagnostic.accepted
    record
      { scheduledInstances =
          selectedInstance selection
          ∷ᴸ scheduledInstances suffix
      ; finalBuilder = finalBuilder suffix
      ; schedulingTrace =
          scheduleNext
            (selectedRemoved selection)
            (selectedProcessed selection)
            (schedulingTrace suffix)
      }

-- The public scheduler is bounded by exactly the number of source
-- occurrences.  Every recursive success removes one occurrence, so the bound
-- is sufficient without inventing a graph-size heuristic.

scheduleInstances : ∀ {inputCount registerCount}
  → (current : Generic.Builder inputCount registerCount)
  → (items : List Raw.RawInstance)
  → Diagnostic.CheckResult (Scheduled current items)
scheduleInstances current items =
  scheduleFuel (lengthList items) current items

-- Erasing the builder equations from a trace leaves an occurrence-sensitive
-- permutation proof.  This is the retained provenance/order information for
-- downstream correspondence arguments.

data RemovalPermutation {A : Type ℓ} : List A → List A → Type ℓ where
  permutationDone : RemovalPermutation []ᴸ []ᴸ

  permutationNext : ∀ {source selected remaining scheduled}
    → Removed selected source remaining
    → RemovalPermutation remaining scheduled
    → RemovalPermutation source (selected ∷ᴸ scheduled)

trace-permutation :
  ∀ {inputCount registerCount current source scheduled final}
  → ScheduleTrace
      {inputCount = inputCount} {registerCount = registerCount}
      current source scheduled final
  → RemovalPermutation source scheduled
trace-permutation scheduleDone = permutationDone
trace-permutation (scheduleNext removed processed rest) =
  permutationNext removed (trace-permutation rest)

permutation-preserves-length : ∀ {A : Type ℓ} {source scheduled}
  → RemovalPermutation {A = A} source scheduled
  → lengthList source ≡ lengthList scheduled
permutation-preserves-length permutationDone = refl
permutation-preserves-length
  (permutationNext removed rest) =
  removed-length removed
  ∙ cong suc (permutation-preserves-length rest)

permutation-preserves-membership :
  ∀ {A : Type ℓ} {item : A} {source scheduled}
  → RemovalPermutation {A = A} source scheduled
  → item ∈ scheduled
  → item ∈ source
permutation-preserves-membership
  (permutationNext removed rest) here =
  removed-item-listed removed
permutation-preserves-membership
  (permutationNext removed rest) (there membership) =
  removed-retains removed
    (permutation-preserves-membership rest membership)

scheduled-permutation : ∀ {inputCount registerCount initial source}
  → (result :
      Scheduled
        {inputCount = inputCount} {registerCount = registerCount}
        initial source)
  → RemovalPermutation source (scheduledInstances result)
scheduled-permutation result =
  trace-permutation (schedulingTrace result)

scheduled-length : ∀ {inputCount registerCount initial source}
  → (result :
      Scheduled
        {inputCount = inputCount} {registerCount = registerCount}
        initial source)
  → lengthList source ≡ lengthList (scheduledInstances result)
scheduled-length result =
  permutation-preserves-length (scheduled-permutation result)

continueProcessing : ∀ {inputCount registerCount}
  → List Raw.RawInstance
  → Diagnostic.CheckResult (Generic.Builder inputCount registerCount)
  → Diagnostic.CheckResult (Generic.Builder inputCount registerCount)
continueProcessing items (Diagnostic.rejected diagnostics) =
  Diagnostic.rejected diagnostics
continueProcessing items (Diagnostic.accepted next) =
  Generic.processInstances items next

processInstances-step : ∀ {inputCount registerCount}
  → (item : Raw.RawInstance)
  → (items : List Raw.RawInstance)
  → (current : Generic.Builder inputCount registerCount)
  → Generic.processInstances (item ∷ᴸ items) current
    ≡ continueProcessing items (Generic.processInstance item current)
processInstances-step item items current
  with Generic.processInstance item current
... | Diagnostic.rejected diagnostics = refl
... | Diagnostic.accepted next = refl

trace-replays :
  ∀ {inputCount registerCount current source scheduled final}
  → ScheduleTrace
      {inputCount = inputCount} {registerCount = registerCount}
      current source scheduled final
  → Generic.processInstances scheduled current
    ≡ Diagnostic.accepted final
trace-replays scheduleDone = refl
trace-replays
  {current = current}
  {scheduled = selected ∷ᴸ scheduled}
  (scheduleNext {selected = selected} removed processed rest) =
  processInstances-step selected scheduled current
  ∙ cong (continueProcessing scheduled) processed
  ∙ trace-replays rest

scheduled-replays : ∀ {inputCount registerCount initial source}
  → (result :
      Scheduled
        {inputCount = inputCount} {registerCount = registerCount}
        initial source)
  → Generic.processInstances (scheduledInstances result) initial
    ≡ Diagnostic.accepted (finalBuilder result)
scheduled-replays result = trace-replays (schedulingTrace result)

-- Honest boundary: acceptance is fully certified, but this module does not
-- claim that `combinationalCycle? design ≡ false` alone implies scheduling
-- success.  The cycle detector speaks only about raw net dependency edges,
-- whereas GenericBuilder additionally checks primitive support, canonical
-- parameters, exact scalar port shape, output retention, and initial
-- input/register-Q bindings.  Relating graph acyclicity plus all those raw
-- admission premises to existence of a buildable occurrence is a separate
-- whole-design theorem; failures here retain every concrete builder
-- diagnostic instead of silently treating that gap as a cycle proof.