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

module Spartan6.Examples.UnifiedAdmission where

open import Spartan6.Prelude

import Spartan6.Examples.ImportedYosys as Imported
import Spartan6.Fixtures.YosysArtifacts as ArtifactExample
import Spartan6.Netlist.AdmissionCore as Legacy
import Spartan6.Netlist.DecodedOperation as Operation
import Spartan6.Netlist.ExactAdmission as Admission
import Spartan6.Netlist.Provenance as Provenance
import Spartan6.Netlist.ReadySchedule as Schedule
import Spartan6.Validation.CheckResult as Result

togglePlan : Operation.OperationPlan
togglePlan = Operation.planValidated ArtifactExample.toggleValidated

toggleHint : List Provenance.OccurrenceId
toggleHint = Provenance.occurrenceId  ∷ᴸ []ᴸ

toggle-schedule-is-accepted :
  Result.accepted?
    (Schedule.checkSchedule
      (Operation.initiallyAvailableNets togglePlan)
      (Operation.combinationalOperations togglePlan)
      toggleHint)
  ≡ true
toggle-schedule-is-accepted = refl

toggleSchedule :
  Schedule.Scheduled
    (Operation.initiallyAvailableNets togglePlan)
    (Operation.combinationalOperations togglePlan)
toggleSchedule = Result.extractAccepted
  (Schedule.checkSchedule
    (Operation.initiallyAvailableNets togglePlan)
    (Operation.combinationalOperations togglePlan)
    toggleHint)
  toggle-schedule-is-accepted

toggle-schedule-counts-each-edge-once :
  Schedule.checkedCost toggleSchedule
  ≡ Schedule.scheduleCost     
toggle-schedule-counts-each-edge-once = refl

toggleExactAdmission : Admission.ExactAdmission ArtifactExample.toggleArtifact
toggleExactAdmission = Admission.exactAdmission
  ArtifactExample.toggleValidated
  togglePlan refl
  toggleSchedule
  (Legacy.admittedMixed Imported.importedAdmission)
  refl
  Imported.importedExecutable
  refl

toggle-exact-digest-retained :
  Admission.exact-source-digest toggleExactAdmission ≡ refl
toggle-exact-digest-retained = refl