Spartan6.Netlist.ReadySchedule

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

module Spartan6.Netlist.ReadySchedule where

open import Spartan6.Prelude

import Spartan6.Netlist.Provenance as Provenance
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

open import Cubical.Data.Nat using (_≡ᵇ_)
open import Cubical.Data.Bool.Base using (Bool→Type)
open import Cubical.Data.Nat.Properties using (≡ᵇ→≡)

record Operation : Type₀ where
  constructor operation
  field
    operationId : Provenance.OccurrenceId
    requiredNets : List Raw.NetId
    producedNets : List Raw.NetId

open Operation public

sameOccurrence : Provenance.OccurrenceId → Provenance.OccurrenceId → Bool
sameOccurrence (Provenance.occurrenceId left)
  (Provenance.occurrenceId right) = left ≡ᵇ right

allAvailable : List Raw.NetId → List Raw.NetId → Bool
allAvailable []ᴸ available = true
allAvailable (required ∷ᴸ requireds) available =
  Validation.containsNet required available
  and allAvailable requireds available

Ready : List Raw.NetId → Operation → Type₀
Ready available item = allAvailable (requiredNets item) available ≡ true

addProduced : Operation → List Raw.NetId → List Raw.NetId
addProduced item available = producedNets item ++ᴸ available

data Removed (item : Operation) : List Operation → List Operation → Type₀ where
  removeHere : ∀ {items} → Removed item (item ∷ᴸ items) items
  removeThere : ∀ {other items remaining}
    → Removed item items remaining
    → Removed item (other ∷ᴸ items) (other ∷ᴸ remaining)

record Selection
  (identifier : Provenance.OccurrenceId)
  (source : List Operation) : Type₀ where
  field
    selected : Operation
    remaining : List Operation
    selectedId : operationId selected ≡ identifier
    selectedRemoved : Removed selected source remaining

open Selection public

prependSelection : ∀ identifier skipped {items}
  → Selection identifier items → Selection identifier (skipped ∷ᴸ items)
prependSelection identifier skipped selection = record
  { selected = selected selection
  ; remaining = skipped ∷ᴸ remaining selection
  ; selectedId = selectedId selection
  ; selectedRemoved = removeThere (selectedRemoved selection)
  }

selectById : (identifier : Provenance.OccurrenceId)
  → (source : List Operation) → Maybe (Selection identifier source)
selectById identifier []ᴸ = nothing
selectById identifier (item ∷ᴸ items) with
  sameOccurrence (operationId item) identifier UsingEq
... | true , same-path = just record
  { selected = item
  ; remaining = items
  ; selectedId = occurrence-equality item identifier same-path
  ; selectedRemoved = removeHere
  }
  where
  occurrence-equality : (item : Operation)
    → (identifier : Provenance.OccurrenceId)
    → sameOccurrence (operationId item) identifier ≡ true
    → operationId item ≡ identifier
  occurrence-equality
    (operation (Provenance.occurrenceId left) required produced)
    (Provenance.occurrenceId right) equality =
    cong Provenance.occurrenceId
      (≡ᵇ→≡ (subst Bool→Type (sym equality) tt))
... | false , same-path with selectById identifier items
...   | nothing = nothing
...   | just selection = just (prependSelection identifier item selection)

data ScheduleTrace :
  List Raw.NetId → List Operation → List Operation
  → List Raw.NetId → Type₀ where
  scheduleDone : ∀ {available}
    → ScheduleTrace available []ᴸ []ᴸ available
  scheduleNext : ∀ {available source item remaining scheduled final}
    → Removed item source remaining
    → Ready available item
    → ScheduleTrace (addProduced item available)
        remaining scheduled final
    → ScheduleTrace available source (item ∷ᴸ scheduled) final

record Scheduled (initial : List Raw.NetId) (source : List Operation) : Type₀ where
  constructor scheduled
  field
    scheduledOperations : List Operation
    finalAvailable : List Raw.NetId
    schedulingTrace :
      ScheduleTrace initial source scheduledOperations finalAvailable

open Scheduled public

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

deadlockDiagnostic invalidHintDiagnostic blockedHintDiagnostic :
  Diagnostic.Diagnostic
deadlockDiagnostic =
  Diagnostic.diagnostic Diagnostic.combinationalLoop Diagnostic.reject
    "readiness scheduler" "a complete ready occurrence certificate"
    "pending operations after the certificate ended"
    "All permanent failures were excluded before scheduling; remaining work is a dependency deadlock or an incomplete certificate."
invalidHintDiagnostic =
  Diagnostic.diagnostic Diagnostic.malformedImport Diagnostic.reject
    "schedule certificate" "each source occurrence exactly once"
    "an unknown or repeated occurrence identifier"
    "The certificate checker never invents an operation or assigns precedence to a duplicate identifier."
blockedHintDiagnostic =
  Diagnostic.diagnostic Diagnostic.undrivenInput Diagnostic.reject
    "schedule certificate" "all required nets available at this step"
    "a temporarily blocked selected occurrence"
    "A certificate must order operations by readiness; another valid order may still exist."

continueScheduled : ∀ {available source identifier}
  → (selection : Selection identifier source)
  → Ready available (selected selection)
  → Diagnostic.CheckResult
      (Scheduled
        (addProduced (selected selection) available)
        (remaining selection))
  → Diagnostic.CheckResult (Scheduled available source)
continueScheduled selection ready (Diagnostic.rejected diagnostics) =
  Diagnostic.rejected diagnostics
continueScheduled selection ready (Diagnostic.accepted suffix) =
  Diagnostic.accepted
    (scheduled
      (selected selection ∷ᴸ scheduledOperations suffix)
      (finalAvailable suffix)
      (scheduleNext
        (selectedRemoved selection) ready (schedulingTrace suffix)))

checkSchedule : (available : List Raw.NetId)
  → (source : List Operation)
  → List Provenance.OccurrenceId
  → Diagnostic.CheckResult (Scheduled available source)
checkSchedule available []ᴸ []ᴸ =
  Diagnostic.accepted (scheduled []ᴸ available scheduleDone)
checkSchedule available (item ∷ᴸ items) []ᴸ =
  Diagnostic.rejected (singleton deadlockDiagnostic)
checkSchedule available []ᴸ (identifier ∷ᴸ identifiers) =
  Diagnostic.rejected (singleton invalidHintDiagnostic)
checkSchedule available source (identifier ∷ᴸ identifiers) with
  selectById identifier source
... | nothing = Diagnostic.rejected (singleton invalidHintDiagnostic)
... | just selection with
  allAvailable (requiredNets (selected selection)) available UsingEq
...   | false , ready-path =
  Diagnostic.rejected (singleton blockedHintDiagnostic)
...   | true , ready-path with
  checkSchedule
    (addProduced (selected selection) available)
    (remaining selection) identifiers
...     | suffix = continueScheduled selection ready-path suffix

data RemovalPermutation : List Operation → List Operation → Type₀ where
  permutationDone : RemovalPermutation []ᴸ []ᴸ
  permutationNext : ∀ {source item remaining scheduled}
    → Removed item source remaining
    → RemovalPermutation remaining scheduled
    → RemovalPermutation source (item ∷ᴸ scheduled)

tracePermutation : ∀ {available source scheduled final}
  → ScheduleTrace available source scheduled final
  → RemovalPermutation source scheduled
tracePermutation scheduleDone = permutationDone
tracePermutation (scheduleNext removed ready rest) =
  permutationNext removed (tracePermutation rest)

scheduledPermutation : ∀ {available source}
  → (result : Scheduled available source)
  → RemovalPermutation source (scheduledOperations result)
scheduledPermutation result = tracePermutation (schedulingTrace result)

replayAvailable : List Operation → List Raw.NetId → List Raw.NetId
replayAvailable []ᴸ available = available
replayAvailable (item ∷ᴸ items) available =
  replayAvailable items (addProduced item available)

traceReplays : ∀ {available source scheduled final}
  → ScheduleTrace available source scheduled final
  → replayAvailable scheduled available ≡ final
traceReplays scheduleDone = refl
traceReplays (scheduleNext removed ready rest) = traceReplays rest

record ScheduleCost : Type₀ where
  constructor scheduleCost
  field
    readinessChecks : ℕ
    handlerExecutions : ℕ
    dependencyEvents : ℕ
    enqueues : ℕ
    nodeConstructions : ℕ

open ScheduleCost public

sumRequired : List Operation → ℕ
sumRequired []ᴸ = 0
sumRequired (item ∷ᴸ items) =
  lengthList (requiredNets item) + sumRequired items

checkedCost : ∀ {available source} → Scheduled available source
  → ScheduleCost
checkedCost result = scheduleCost count count edges count count
  where
  count = lengthList (scheduledOperations result)
  edges = sumRequired (scheduledOperations result)

data AcyclicOrder : List Raw.NetId → List Operation → Type₀ where
  orderDone : ∀ {available} → AcyclicOrder available []ᴸ
  orderNext : ∀ {available source identifier}
    → (selection : Selection identifier source)
    → selectById identifier source ≡ just selection
    → Ready available (selected selection)
    → AcyclicOrder
        (addProduced (selected selection) available)
        (remaining selection)
    → AcyclicOrder available source

orderHint : ∀ {available source} → AcyclicOrder available source
  → List Provenance.OccurrenceId
orderHint orderDone = []ᴸ
orderHint (orderNext {identifier = identifier} selection found ready rest) =
  identifier ∷ᴸ orderHint rest

scheduledFromOrder : ∀ {available source}
  → AcyclicOrder available source → Scheduled available source
scheduledFromOrder orderDone = scheduled []ᴸ _ scheduleDone
scheduledFromOrder
  (orderNext selection found ready rest) with scheduledFromOrder rest
... | suffix = scheduled
  (selected selection ∷ᴸ scheduledOperations suffix)
  (finalAvailable suffix)
  (scheduleNext (selectedRemoved selection) ready (schedulingTrace suffix))

acyclic-order-schedules : ∀ {available source}
  → AcyclicOrder available source
  → Scheduled available source
acyclic-order-schedules = scheduledFromOrder