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

module Spartan6.Examples.SharedDAG where

open import Spartan6.Prelude

import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.DAGEvaluation as Direct
import Spartan6.Netlist.StableBuilder as StableBuilder
import Spartan6.Netlist.StableDAG as Stable
import Spartan6.Semantics.Design as Semantics

input0 input1 : Fin 2
input0 = fzero
input1 = fsuc fzero

-- One XOR source fans out into two AND branches and is joined by OR.  The XOR
-- is represented by one node entry; both branches refer to that shared local.

sharedDiamondNodes : Checked.Nodes 2 1 4
sharedDiamondNodes =
  (((Checked.noNodes Checked.▻
      Checked.xorNode
        (Checked.externalWire input0)
        (Checked.externalWire input1))
    Checked.▻
      Checked.andNode
        (Checked.localWire fzero)
        (Checked.externalWire input0))
   Checked.▻
      Checked.andNode
        (Checked.localWire (fsuc fzero))
        (Checked.externalWire input1))
  Checked.▻
    Checked.orNode
      (Checked.localWire (fsuc fzero))
      (Checked.localWire fzero)

sharedDiamond : Checked.CheckedNetlist 2 1 1 4
sharedDiamond =
  Checked.checkedNetlist
    (low ∷ [])
    sharedDiamondNodes
    (Checked.localWire fzero ∷ [])
    (Checked.localWire fzero ∷ [])

highLowInputs : Vec Bit 2
highLowInputs = high ∷ low ∷ []

lowState : Vec Bit 1
lowState = low ∷ []

-- Locals are newest-first in the compatibility evaluator: join, right branch,
-- left branch, then the single shared XOR source.

shared-diamond-local-reduction :
  Direct.evaluateNodes sharedDiamondNodes highLowInputs lowState
  ≡ high ∷ low ∷ high ∷ high ∷ []
shared-diamond-local-reduction = refl

sharedSourceIndex : Fin 4
sharedSourceIndex = fsuc (fsuc (fsuc fzero))

shared-source-has-one-local-entry :
  lookup sharedSourceIndex
    (Direct.evaluateNodes sharedDiamondNodes highLowInputs lowState)
  ≡ high
shared-source-has-one-local-entry = refl

shared-diamond-output-reduction :
  Direct.directOutputs sharedDiamond highLowInputs lowState
  ≡ high ∷ []
shared-diamond-output-reduction = refl

shared-diamond-next-reduction :
  Direct.directNext sharedDiamond highLowInputs lowState
  ≡ high ∷ []
shared-diamond-next-reduction = refl

shared-diamond-output-agrees-with-compilation :
  Direct.directOutputs sharedDiamond highLowInputs lowState
  ≡ Semantics.observe
      (Checked.compileNetlist sharedDiamond) highLowInputs lowState
shared-diamond-output-agrees-with-compilation =
  Direct.directOutputs-compile sharedDiamond highLowInputs lowState

shared-diamond-next-agrees-with-compilation :
  Direct.directNext sharedDiamond highLowInputs lowState
  ≡ Semantics.step
      (Checked.compileNetlist sharedDiamond)
      Semantics.risingEdge highLowInputs lowState
shared-diamond-next-agrees-with-compilation =
  Direct.directNext-compile sharedDiamond highLowInputs lowState

stableDiamond : Stable.StableNetlist 2 1 1 4
stableDiamond = Stable.convertNetlist sharedDiamond

stable-diamond-output-reduction :
  Stable.stableDirectOutputs stableDiamond highLowInputs lowState
  ≡ high ∷ []
stable-diamond-output-reduction = refl

stable-diamond-next-agrees-with-checked :
  Stable.stableDirectNext stableDiamond highLowInputs lowState
  ≡ Direct.directNext sharedDiamond highLowInputs lowState
stable-diamond-next-agrees-with-checked =
  Stable.convertNext-evaluation sharedDiamond highLowInputs lowState

-- Hybrid-builder reduction: the second extension adds one head binding while
-- the first binding is retained verbatim.  Its local ordinal remains zero;
-- there is no binding-wide lift.

stableStart : StableBuilder.StableBuilder 2 1
stableStart = StableBuilder.emptyBuilder 2 1

stableShared : StableBuilder.StableBuilder 2 1
stableShared =
  StableBuilder.extendBuilder stableStart 10
    (Stable.stableXor
      (Stable.stableExternal input0)
      (Stable.stableExternal input1))

stableLeft : StableBuilder.StableBuilder 2 1
stableLeft =
  StableBuilder.extendBuilder stableShared 11
    (Stable.stableAnd
      (Stable.stableLocal fzero)
      (Stable.stableExternal input0))

stable-extension-does-not-lift-old-binding :
  StableBuilder.builderBindings stableLeft
  ≡ StableBuilder.bindStable 11 (StableBuilder.localReference 1)
    ∷ᴸ StableBuilder.bindStable 10 (StableBuilder.localReference 0)
    ∷ᴸ []ᴸ
stable-extension-does-not-lift-old-binding = refl