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

module Spartan6.Netlist.GenericBuilder where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.BuildOBUFDS as OBUFDS
open import Spartan6.Netlist.BuilderCore public
import Spartan6.Netlist.Carry4Builder as Carry4
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.PortDecode as PortDecode
import Spartan6.Netlist.Raw as Raw
import Spartan6.Primitive.LUT as LUT
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Parameter as Parameter
resolveLUTInputPorts :
  ∀ {inputCount registerCount localCount arity}
  → String
  → Bindings inputCount registerCount localCount
  → Vec Raw.RawPort arity
  → Diagnostic.CheckResult
      (Vec
        (Checked.Wire inputCount registerCount localCount)
        arity)
resolveLUTInputPorts subject bindings [] = Diagnostic.accepted []
resolveLUTInputPorts subject bindings (port ∷ ports)
  with resolveScalarPort subject bindings port
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted wire
  with resolveLUTInputPorts subject bindings ports
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted wires = Diagnostic.accepted (wire ∷ wires)

processLUTBundle : ∀ {inputCount registerCount arity}
  → Raw.RawInstance
  → LUT.TruthTable arity
  → PortDecode.LUTPortBundle arity
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processLUTBundle item table bundle current
  with resolveLUTInputPorts
    "LUT input"
    (builderBindings current)
    (PortDecode.lutInputPorts bundle)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted wires
  with PortDecode.outputNet
    (Raw.rawInstanceName item)
    (PortDecode.lutOutputPort bundle)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted net-id =
  Diagnostic.accepted
    (extendBuilder current net-id (Checked.lutNode table wires))

processFixedLUT : ∀ {inputCount registerCount}
  → (arity : ℕ)
  → Raw.RawInstance
  → LUT.TruthTable arity
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processFixedLUT arity item table current
  with PortDecode.parseLUTPortBundle
    arity (Raw.rawInstancePorts item)
... | just bundle = processLUTBundle item table bundle current
... | nothing =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.widthMismatch
        (Raw.rawInstanceName item)
        "the canonical ordered LUT input ports followed by O"
        "a different raw LUT port list"
        "StructurallyValid should make this branch unreachable for the selected LUT arity."))

processLUT1 : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processLUT1 item current
  with Parameter.normaliseCoreParameters Architecture.LUT1
    (Raw.rawInstanceName item)
    (Raw.rawInstanceParameters item)
    (Raw.rawInstanceInitialBit item)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted (Parameter.lut1Parameters table) =
  processFixedLUT  item table current

processLUT2 : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processLUT2 item current
  with Parameter.normaliseCoreParameters Architecture.LUT2
    (Raw.rawInstanceName item)
    (Raw.rawInstanceParameters item)
    (Raw.rawInstanceInitialBit item)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted (Parameter.lut2Parameters table) =
  processFixedLUT  item table current

processLUT3 : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processLUT3 item current
  with Parameter.normaliseCoreParameters Architecture.LUT3
    (Raw.rawInstanceName item)
    (Raw.rawInstanceParameters item)
    (Raw.rawInstanceInitialBit item)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted (Parameter.lut3Parameters table) =
  processFixedLUT  item table current

processLUT4 : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processLUT4 item current
  with Parameter.normaliseCoreParameters Architecture.LUT4
    (Raw.rawInstanceName item)
    (Raw.rawInstanceParameters item)
    (Raw.rawInstanceInitialBit item)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted (Parameter.lut4Parameters table) =
  processFixedLUT  item table current

processLUT5 : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processLUT5 item current
  with Parameter.normaliseCoreParameters Architecture.LUT5
    (Raw.rawInstanceName item)
    (Raw.rawInstanceParameters item)
    (Raw.rawInstanceInitialBit item)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted (Parameter.lut5Parameters table) =
  processFixedLUT  item table current

processLUT6 : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processLUT6 item current
  with Parameter.normaliseCoreParameters Architecture.LUT6
    (Raw.rawInstanceName item)
    (Raw.rawInstanceParameters item)
    (Raw.rawInstanceInitialBit item)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted (Parameter.lut6Parameters table) =
  processFixedLUT  item table current

processParsedMux : ∀ {inputCount registerCount}
  → String
  → PortDecode.MuxPorts
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processParsedMux subject ports current
  with resolveScalarPort
    "mux.I0" (builderBindings current)
    (PortDecode.muxI0 ports)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted input0
  with resolveScalarPort
    "mux.I1" (builderBindings current)
    (PortDecode.muxI1 ports)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted input1
  with resolveScalarPort
    "mux.S" (builderBindings current)
    (PortDecode.muxS ports)
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted select
  with PortDecode.outputNet subject (PortDecode.muxO ports)
...       | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...       | Diagnostic.accepted net-id =
  Diagnostic.accepted
    (extendBuilder current net-id
      (Checked.muxNode select input0 input1))

processMuxPorts : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processMuxPorts item current
  with PortDecode.parseMuxPorts (Raw.rawInstancePorts item)
... | just ports =
  processParsedMux (Raw.rawInstanceName item) ports current
... | nothing =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.widthMismatch
        (Raw.rawInstanceName item)
        "canonical scalar I0, I1, S, and O ports"
        "a different raw mux port list"
        "StructurallyValid should make this branch unreachable for MUXF7/MUXF8."))

processMUXF7 : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processMUXF7 item current
  with Parameter.normaliseCoreParameters Architecture.MUXF7
    (Raw.rawInstanceName item)
    (Raw.rawInstanceParameters item)
    (Raw.rawInstanceInitialBit item)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted Parameter.muxf7Parameters =
  processMuxPorts item current

processMUXF8 : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processMUXF8 item current
  with Parameter.normaliseCoreParameters Architecture.MUXF8
    (Raw.rawInstanceName item)
    (Raw.rawInstanceParameters item)
    (Raw.rawInstanceInitialBit item)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted Parameter.muxf8Parameters =
  processMuxPorts item current

processBufferPorts : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → PortDecode.BufferPorts
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processBufferPorts item ports current
  with resolveScalarPort
    "buffer.I" (builderBindings current)
    (PortDecode.bufferI ports)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted input-wire
  with PortDecode.outputNet
    (Raw.rawInstanceName item) (PortDecode.bufferO ports)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted net-id =
  Diagnostic.accepted (aliasBuilder current net-id input-wire)

processAliasBuffer : ∀ {inputCount registerCount}
  → Architecture.PrimitiveKind
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processAliasBuffer kind item current
  with Parameter.normaliseCoreParameters kind
    (Raw.rawInstanceName item)
    (Raw.rawInstanceParameters item)
    (Raw.rawInstanceInitialBit item)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted parameters
  with PortDecode.parseBufferPorts (Raw.rawInstancePorts item)
...   | nothing =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.widthMismatch
        (Raw.rawInstanceName item)
        "canonical scalar I and O ports"
        "a different raw buffer port list"
        "StructurallyValid should make this branch unreachable for alias buffers."))
...   | just ports = processBufferPorts item ports current

processEnabledBufferPorts : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → PortDecode.EnabledBufferPorts
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processEnabledBufferPorts item ports current
  with resolveScalarPort
    "BUFGCE.I" (builderBindings current)
    (PortDecode.enabledBufferI ports)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted input-wire
  with resolveScalarPort
    "BUFGCE.CE" (builderBindings current)
    (PortDecode.enabledBufferCE ports)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted enable-wire
  with PortDecode.outputNet
    (Raw.rawInstanceName item)
    (PortDecode.enabledBufferO ports)
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted net-id =
  Diagnostic.accepted
    (extendBuilder current net-id
      (Checked.muxNode
        enable-wire (Checked.literalWire low) input-wire))

processBUFGCE : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processBUFGCE item current
  with Parameter.normaliseCoreParameters Architecture.BUFGCE
    (Raw.rawInstanceName item)
    (Raw.rawInstanceParameters item)
    (Raw.rawInstanceInitialBit item)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted Parameter.bufgceParameters
  with PortDecode.parseEnabledBufferPorts
    (Raw.rawInstancePorts item)
...   | nothing =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.widthMismatch
        (Raw.rawInstanceName item)
        "canonical scalar I, CE, and O ports"
        "a different raw BUFGCE port list"
        "StructurallyValid should make this branch unreachable for BUFGCE."))
...   | just ports = processEnabledBufferPorts item ports current

processCARRY4 : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processCARRY4 item current =
  Diagnostic.mapResult Carry4.carryBuilder
    (Carry4.processCARRY4 item current)

processOBUFDS : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processOBUFDS = OBUFDS.processOBUFDS

processKnownInstance : ∀ {inputCount registerCount}
  → Architecture.PrimitiveKind
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processKnownInstance Architecture.LUT1 item current =
  processLUT1 item current
processKnownInstance Architecture.LUT2 item current =
  processLUT2 item current
processKnownInstance Architecture.LUT3 item current =
  processLUT3 item current
processKnownInstance Architecture.LUT4 item current =
  processLUT4 item current
processKnownInstance Architecture.LUT5 item current =
  processLUT5 item current
processKnownInstance Architecture.LUT6 item current =
  processLUT6 item current
processKnownInstance Architecture.MUXF7 item current =
  processMUXF7 item current
processKnownInstance Architecture.MUXF8 item current =
  processMUXF8 item current
processKnownInstance Architecture.CARRY4 item current =
  processCARRY4 item current
processKnownInstance Architecture.IBUF item current =
  processAliasBuffer Architecture.IBUF item current
processKnownInstance Architecture.OBUF item current =
  processAliasBuffer Architecture.OBUF item current
processKnownInstance Architecture.OBUFDS item current =
  processOBUFDS item current
processKnownInstance Architecture.BUFG item current =
  processAliasBuffer Architecture.BUFG item current
processKnownInstance Architecture.BUFGCE item current =
  processBUFGCE item current
processKnownInstance kind item current =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.unsupportedMode
        (Raw.rawInstanceName item)
        "LUT1-LUT6, MUXF7/MUXF8, CARRY4, IBUF/OBUF/OBUFDS/BUFG, or BUFGCE"
        "another primitive kind"
        "This builder only constructs the established combinational checked-node slice."))

processInstance : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processInstance item current with Raw.rawInstanceKind item
... | Raw.unknownPrimitive name =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.unknownPrimitive
        (Raw.rawInstanceName item)
        "a supported known combinational primitive"
        name
        "Unknown cells never receive checked semantics."))
... | Raw.knownPrimitive kind = processKnownInstance kind item current

-- Sequential processing is the topological boundary: each item can see the
-- initial input/state bindings and outputs already installed by earlier
-- items, never outputs that occur later in this list.

processInstances : ∀ {inputCount registerCount}
  → List Raw.RawInstance
  → Builder inputCount registerCount
  → Diagnostic.CheckResult (Builder inputCount registerCount)
processInstances []ᴸ current = Diagnostic.accepted current
processInstances (item ∷ᴸ items) current
  with processInstance item current
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted next = processInstances items next