Spartan6.Netlist.BuilderCore

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

module Spartan6.Netlist.BuilderCore where

open import Spartan6.Prelude

import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic

open import Cubical.Data.Nat using (_≡ᵇ_)
open import Agda.Builtin.String using (primShowNat)

-- Register-aware builder infrastructure shared by the generic dispatcher and
-- specialized primitive builders.  Keeping this layer free of primitive
-- dispatch dependencies prevents cycles while preserving intrinsic input,
-- register, and local-wire bounds.

singleton : Diagnostic.Diagnostic → Diagnostic.Diagnostics
singleton item = item ∷ᴸ []ᴸ

issue : Diagnostic.DiagnosticCode
      → String → String → String → String
      → Diagnostic.Diagnostic
issue code subject expected observed detail =
  Diagnostic.diagnostic
    code Diagnostic.reject subject expected observed detail

record NetBinding
  (inputCount registerCount localCount : ℕ)
  : Type₀ where
  constructor bindNet
  field
    bindingNet : Raw.NetId
    bindingWire :
      Checked.Wire inputCount registerCount localCount

open NetBinding public

Bindings : ℕ → ℕ → ℕ → Type₀
Bindings inputCount registerCount localCount =
  List (NetBinding inputCount registerCount localCount)

liftInputWire : ∀ {inputCount registerCount localCount}
  → Checked.Wire inputCount registerCount localCount
  → Checked.Wire (suc inputCount) registerCount localCount
liftInputWire (Checked.externalWire index) =
  Checked.externalWire (fsuc index)
liftInputWire (Checked.storedWire index) = Checked.storedWire index
liftInputWire (Checked.localWire index) = Checked.localWire index
liftInputWire (Checked.literalWire bit) = Checked.literalWire bit

liftInputBindings : ∀ {inputCount registerCount localCount}
  → Bindings inputCount registerCount localCount
  → Bindings (suc inputCount) registerCount localCount
liftInputBindings []ᴸ = []ᴸ
liftInputBindings (bindNet net-id wire ∷ᴸ bindings) =
  bindNet net-id (liftInputWire wire)
  ∷ᴸ liftInputBindings bindings

inputBindings : ∀ {registerCount}
  → (net-ids : List Raw.NetId)
  → Bindings (lengthList net-ids) registerCount 0
inputBindings []ᴸ = []ᴸ
inputBindings (net-id ∷ᴸ net-ids) =
  bindNet net-id (Checked.externalWire fzero)
  ∷ᴸ liftInputBindings (inputBindings net-ids)

liftRegisterWire : ∀ {inputCount registerCount localCount}
  → Checked.Wire inputCount registerCount localCount
  → Checked.Wire inputCount (suc registerCount) localCount
liftRegisterWire (Checked.externalWire index) =
  Checked.externalWire index
liftRegisterWire (Checked.storedWire index) =
  Checked.storedWire (fsuc index)
liftRegisterWire (Checked.localWire index) = Checked.localWire index
liftRegisterWire (Checked.literalWire bit) = Checked.literalWire bit

liftRegisterBindings : ∀ {inputCount registerCount localCount}
  → Bindings inputCount registerCount localCount
  → Bindings inputCount (suc registerCount) localCount
liftRegisterBindings []ᴸ = []ᴸ
liftRegisterBindings (bindNet net-id wire ∷ᴸ bindings) =
  bindNet net-id (liftRegisterWire wire)
  ∷ᴸ liftRegisterBindings bindings

registerBindings : ∀ {inputCount}
  → (net-ids : List Raw.NetId)
  → Bindings inputCount (lengthList net-ids) 0
registerBindings []ᴸ = []ᴸ
registerBindings (net-id ∷ᴸ net-ids) =
  bindNet net-id (Checked.storedWire fzero)
  ∷ᴸ liftRegisterBindings (registerBindings net-ids)

initialBindings :
  (input-net-ids register-q-net-ids : List Raw.NetId)
  → Bindings
      (lengthList input-net-ids)
      (lengthList register-q-net-ids)
      0
initialBindings input-net-ids register-q-net-ids =
  registerBindings register-q-net-ids
  ++ᴸ inputBindings input-net-ids

liftLocalWire : ∀ {inputCount registerCount localCount}
  → Checked.Wire inputCount registerCount localCount
  → Checked.Wire inputCount registerCount (suc localCount)
liftLocalWire (Checked.externalWire index) = Checked.externalWire index
liftLocalWire (Checked.storedWire index) = Checked.storedWire index
liftLocalWire (Checked.localWire index) =
  Checked.localWire (fsuc index)
liftLocalWire (Checked.literalWire bit) = Checked.literalWire bit

liftLocalBindings : ∀ {inputCount registerCount localCount}
  → Bindings inputCount registerCount localCount
  → Bindings inputCount registerCount (suc localCount)
liftLocalBindings []ᴸ = []ᴸ
liftLocalBindings (bindNet net-id wire ∷ᴸ bindings) =
  bindNet net-id (liftLocalWire wire)
  ∷ᴸ liftLocalBindings bindings

lookupNet : ∀ {inputCount registerCount localCount}
  → Raw.NetId
  → Bindings inputCount registerCount localCount
  → Maybe (Checked.Wire inputCount registerCount localCount)
lookupNet net-id []ᴸ = nothing
lookupNet net-id (bindNet candidate wire ∷ᴸ bindings) =
  if net-id ≡ᵇ candidate
  then just wire
  else lookupNet net-id bindings

resolveConnection : ∀ {inputCount registerCount localCount}
  → Bindings inputCount registerCount localCount
  → Raw.Connection
  → Maybe (Checked.Wire inputCount registerCount localCount)
resolveConnection bindings (Raw.net net-id) = lookupNet net-id bindings
resolveConnection bindings (Raw.constant bit) =
  just (Checked.literalWire bit)
resolveConnection bindings Raw.disconnected = nothing

unresolvedConnection : String → Raw.Connection
                     → Diagnostic.Diagnostics
unresolvedConnection subject (Raw.net net-id) =
  singleton
    (issue Diagnostic.undrivenInput subject
      "a constant, top-level input, preallocated register Q, or earlier combinational output"
      (primShowNat net-id)
      "Unresolved and topological forward net references are rejected.")
unresolvedConnection subject (Raw.constant bit) =
  singleton
    (issue Diagnostic.undrivenInput subject
      "a resolvable connection" "an internal resolution failure"
      "Constants are normally resolvable; this total branch records an internal mismatch.")
unresolvedConnection subject Raw.disconnected =
  singleton
    (issue Diagnostic.undrivenInput subject
      "a connected semantic input" "an explicit disconnection"
      "Required combinational inputs may not be discarded.")

nonScalarPort : String → Diagnostic.Diagnostics
nonScalarPort subject =
  singleton
    (issue Diagnostic.widthMismatch subject
      "one structurally checked scalar connection"
      "a non-scalar connection list"
      "The generic combinational builder consumes scalar primitive ports.")

resolveOneConnectionWith : ∀ {inputCount registerCount localCount}
  → (String → Raw.Connection → Diagnostic.Diagnostics)
  → String
  → Bindings inputCount registerCount localCount
  → Raw.Connection
  → Diagnostic.CheckResult
      (Checked.Wire inputCount registerCount localCount)
resolveOneConnectionWith unresolved subject bindings connection
  with resolveConnection bindings connection
... | nothing =
  Diagnostic.rejected (unresolved subject connection)
... | just wire = Diagnostic.accepted wire

resolveOneConnection : ∀ {inputCount registerCount localCount}
  → String
  → Bindings inputCount registerCount localCount
  → Raw.Connection
  → Diagnostic.CheckResult
      (Checked.Wire inputCount registerCount localCount)
resolveOneConnection = resolveOneConnectionWith unresolvedConnection

resolveScalarPortWith : ∀ {inputCount registerCount localCount}
  → (String → Diagnostic.Diagnostics)
  → (String → Raw.Connection → Diagnostic.Diagnostics)
  → String
  → Bindings inputCount registerCount localCount
  → Raw.RawPort
  → Diagnostic.CheckResult
      (Checked.Wire inputCount registerCount localCount)
resolveScalarPortWith non-scalar unresolved subject bindings port
  with Raw.rawPortConnections port
... | []ᴸ = Diagnostic.rejected (non-scalar subject)
... | connection ∷ᴸ []ᴸ =
  resolveOneConnectionWith unresolved subject bindings connection
... | first ∷ᴸ second ∷ᴸ rest =
  Diagnostic.rejected (non-scalar subject)

resolveScalarPort : ∀ {inputCount registerCount localCount}
  → String
  → Bindings inputCount registerCount localCount
  → Raw.RawPort
  → Diagnostic.CheckResult
      (Checked.Wire inputCount registerCount localCount)
resolveScalarPort =
  resolveScalarPortWith nonScalarPort unresolvedConnection

record Builder (inputCount registerCount : ℕ) : Type₀ where
  constructor builder
  field
    builderLocalCount : ℕ
    builderNodes :
      Checked.Nodes inputCount registerCount builderLocalCount
    builderBindings :
      Bindings inputCount registerCount builderLocalCount

open Builder public

initialBuilder :
  (input-net-ids register-q-net-ids : List Raw.NetId)
  → Builder
      (lengthList input-net-ids)
      (lengthList register-q-net-ids)
initialBuilder input-net-ids register-q-net-ids =
  builder 0 Checked.noNodes
    (initialBindings input-net-ids register-q-net-ids)

extendBuilder : ∀ {inputCount registerCount}
  → (current : Builder inputCount registerCount)
  → Raw.NetId
  → Checked.Node
      inputCount registerCount (builderLocalCount current)
  → Builder inputCount registerCount
extendBuilder (builder local-count nodes bindings) net-id node =
  builder
    (suc local-count)
    (nodes Checked.▻ node)
    (bindNet net-id (Checked.localWire fzero)
     ∷ᴸ liftLocalBindings bindings)

aliasBuilder : ∀ {inputCount registerCount}
  → (current : Builder inputCount registerCount)
  → Raw.NetId
  → Checked.Wire
      inputCount registerCount (builderLocalCount current)
  → Builder inputCount registerCount
aliasBuilder (builder local-count nodes bindings) net-id wire =
  builder local-count nodes (bindNet net-id wire ∷ᴸ bindings)