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

module Spartan6.Examples.ReadinessSchedule where

open import Spartan6.Prelude

import Spartan6.Netlist.Provenance as Provenance
import Spartan6.Netlist.ReadySchedule as Schedule
import Spartan6.Validation.CheckResult as Result
import Spartan6.Validation.Diagnostic as Diagnostic

late early : Schedule.Operation
late = Schedule.operation (Provenance.occurrenceId 0)
  (2 ∷ᴸ []ᴸ) (3 ∷ᴸ []ᴸ)
early = Schedule.operation (Provenance.occurrenceId 1)
  (1 ∷ᴸ []ᴸ) (2 ∷ᴸ []ᴸ)

reverseSource : List Schedule.Operation
reverseSource = late ∷ᴸ early ∷ᴸ []ᴸ

topologicalHint : List Provenance.OccurrenceId
topologicalHint =
  Provenance.occurrenceId 1 ∷ᴸ Provenance.occurrenceId 0 ∷ᴸ []ᴸ

reverse-certificate-is-accepted :
  Result.accepted?
    (Schedule.checkSchedule (1 ∷ᴸ []ᴸ)
      reverseSource topologicalHint)
  ≡ true
reverse-certificate-is-accepted = refl

orderedHint : List Provenance.OccurrenceId
orderedHint =
  Provenance.occurrenceId 0 ∷ᴸ Provenance.occurrenceId 1 ∷ᴸ []ᴸ

blocked-certificate-is-distinct :
  Schedule.checkSchedule (1 ∷ᴸ []ᴸ) reverseSource orderedHint
  ≡ Diagnostic.rejected
      (Schedule.blockedHintDiagnostic ∷ᴸ []ᴸ)
blocked-certificate-is-distinct = refl

cycleLeft cycleRight : Schedule.Operation
cycleLeft = Schedule.operation (Provenance.occurrenceId 2)
  (5 ∷ᴸ []ᴸ) (4 ∷ᴸ []ᴸ)
cycleRight = Schedule.operation (Provenance.occurrenceId 3)
  (4 ∷ᴸ []ᴸ) (5 ∷ᴸ []ᴸ)

empty-hint-with-cycle-is-deadlock :
  Schedule.checkSchedule []ᴸ
    (cycleLeft ∷ᴸ cycleRight ∷ᴸ []ᴸ) []ᴸ
  ≡ Diagnostic.rejected
      (Schedule.deadlockDiagnostic ∷ᴸ []ᴸ)
empty-hint-with-cycle-is-deadlock = refl

acceptedCost : Schedule.ScheduleCost
acceptedCost with
  Schedule.checkSchedule (1 ∷ᴸ []ᴸ) reverseSource topologicalHint
... | Diagnostic.accepted result = Schedule.checkedCost result
... | Diagnostic.rejected diagnostics = Schedule.scheduleCost 0 0 0 0 0

reverse-checked-work-is-linear :
  acceptedCost ≡ Schedule.scheduleCost 2 2 2 2 2
reverse-checked-work-is-linear = refl