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

module Tutorials.Project06.Main where

open import Spartan6.API.Netlist

-- Source order need not be dependency order.  `consumer` appears first, but
-- requires net 2, which `producer` creates from already-available net 1.

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

reverseSource : List Schedule.Operation
reverseSource = consumer ∷ᴸ producer ∷ᴸ []ᴸ

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

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

dependency-order-is-accepted :
  Result.accepted?
    (Schedule.checkSchedule (1 ∷ᴸ []ᴸ) reverseSource readyHint)
  ≡ true
dependency-order-is-accepted = refl

blocked-source-order-is-rejected :
  Schedule.checkSchedule (1 ∷ᴸ []ᴸ) reverseSource sourceOrderHint
  ≡ Diagnostic.rejected (Schedule.blockedHintDiagnostic ∷ᴸ []ᴸ)
blocked-source-order-is-rejected = refl

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

each-operation-and-edge-is-accounted-for-once :
  acceptedCost ≡ Schedule.scheduleCost 2 2 2 2 2
each-operation-and-edge-is-accounted-for-once = refl

-- A handler is not only code generation.  It packages an independent
-- denotation, lowered expressions, and a local proof relating them.

xorTable : LUT.TruthTable 2
xorTable = low ∷ high ∷ high ∷ low ∷ []

xorHandler : Handler.CertifiedHandler 2 1
xorHandler = Handler.lutHandler xorTable

xor-independent-denotation :
  Handler.denotation xorHandler (high ∷ low ∷ []) ≡ high ∷ []
xor-independent-denotation = refl

xor-lowering-agrees-with-denotation :
  Expression.evalAll (high ∷ low ∷ []) []
    (Handler.loweredOutputs xorHandler)
  ≡ Handler.denotation xorHandler (high ∷ low ∷ [])
xor-lowering-agrees-with-denotation =
  Handler.outputsCorrect xorHandler (high ∷ low ∷ [])

differential-output-has-opposite-pins :
  Handler.denotation Handler.obufdsHandler (high ∷ [])
  ≡ high ∷ low ∷ []
differential-output-has-opposite-pins = refl

enabled-fdre-handler-loads-data :
  Handler.stateDenotationNext (Handler.fdreHandler low)
    (high ∷ high ∷ low ∷ []) (low ∷ [])
  ≡ high ∷ []
enabled-fdre-handler-loads-data = refl