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

module Spartan6.Netlist.StableBuilder where

open import Spartan6.Prelude

open import Cubical.Data.FinData.Base using (fromℕ)
import Spartan6.Netlist.Raw as Raw
import Spartan6.Netlist.StableDAG as Stable

-- Hybrid builder references deliberately leave local ordinals as naturals.
-- They cannot be evaluated directly: `materializeReference` checks the current
-- bound before producing an intrinsically bounded StableWire.

data BuilderReference (inputCount stateCount : ℕ) : Type₀ where
  externalReference : Fin inputCount → BuilderReference inputCount stateCount
  storedReference : Fin stateCount → BuilderReference inputCount stateCount
  localReference : ℕ → BuilderReference inputCount stateCount
  literalReference : Bit → BuilderReference inputCount stateCount

record StableBinding (inputCount stateCount : ℕ) : Type₀ where
  constructor bindStable
  field
    bindingNet : Raw.NetId
    bindingReference : BuilderReference inputCount stateCount

open StableBinding public

StableBindings : ℕ → ℕ → Type₀
StableBindings inputCount stateCount =
  List (StableBinding inputCount stateCount)

record StableBuilder (inputCount stateCount : ℕ) : Type₀ where
  constructor stableBuilder
  field
    builderLocalCount : ℕ
    builderNodes : Stable.StableNodes
      inputCount stateCount builderLocalCount
    builderBindings : StableBindings inputCount stateCount

open StableBuilder public

emptyBuilder : ∀ inputCount stateCount → StableBuilder inputCount stateCount
emptyBuilder inputCount stateCount =
  stableBuilder  Stable.stableNoNodes []ᴸ

extendBuilder : ∀ {inputCount stateCount}
  → (current : StableBuilder inputCount stateCount)
  → Raw.NetId
  → Stable.StableNode inputCount stateCount
      (builderLocalCount current)
  → StableBuilder inputCount stateCount
extendBuilder (stableBuilder localCount nodes bindings) net-id node =
  stableBuilder
    (suc localCount)
    (nodes Stable.▹ node)
    (bindStable net-id (localReference localCount) ∷ᴸ bindings)

mapMaybe : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → (A → B) → Maybe A → Maybe B
mapMaybe function nothing = nothing
mapMaybe function (just value) = just (function value)

boundedIndex : (ordinal bound : ℕ) → Maybe (Fin bound)
boundedIndex zero zero = nothing
boundedIndex zero (suc bound) = just fzero
boundedIndex (suc ordinal) zero = nothing
boundedIndex (suc ordinal) (suc bound) =
  mapMaybe fsuc (boundedIndex ordinal bound)

materializeReference : ∀ {inputCount stateCount}
  → (localCount : ℕ)
  → BuilderReference inputCount stateCount
  → Maybe (Stable.StableWire inputCount stateCount localCount)
materializeReference localCount (externalReference index) =
  just (Stable.stableExternal index)
materializeReference localCount (storedReference index) =
  just (Stable.stableStored index)
materializeReference localCount (localReference ordinal) =
  mapMaybe Stable.stableLocal (boundedIndex ordinal localCount)
materializeReference localCount (literalReference bit) =
  just (Stable.stableLiteral bit)

boundedIndex-self : ∀ ordinal
  → boundedIndex ordinal (suc ordinal) ≡ just (fromℕ ordinal)
boundedIndex-self zero = refl
boundedIndex-self (suc ordinal) =
  cong (mapMaybe fsuc) (boundedIndex-self ordinal)

new-reference-materializes : ∀ {inputCount stateCount} localCount
  → materializeReference {inputCount} {stateCount}
      (suc localCount) (localReference localCount)
    ≡ just (Stable.stableLocal (fromℕ localCount))
new-reference-materializes localCount =
  cong (mapMaybe Stable.stableLocal) (boundedIndex-self localCount)

-- These reduction laws are the performance probe: extension adds one binding
-- and retains the complete prior list as its tail.  No map or local-reference
-- weakening traverses the old bindings.

extension-retains-bindings : ∀ {inputCount stateCount}
  (current : StableBuilder inputCount stateCount)
  (net-id : Raw.NetId)
  (node : Stable.StableNode inputCount stateCount
    (builderLocalCount current))
  → builderBindings (extendBuilder current net-id node)
    ≡ bindStable net-id (localReference (builderLocalCount current))
      ∷ᴸ builderBindings current
extension-retains-bindings
  (stableBuilder localCount nodes bindings) net-id node = refl

extension-adds-one-node : ∀ {inputCount stateCount}
  (current : StableBuilder inputCount stateCount)
  (net-id : Raw.NetId)
  (node : Stable.StableNode inputCount stateCount
    (builderLocalCount current))
  → builderLocalCount (extendBuilder current net-id node)
    ≡ suc (builderLocalCount current)
extension-adds-one-node
  (stableBuilder localCount nodes bindings) net-id node = refl