Spartan6.Netlist.NormalizeCombinational

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

module Spartan6.Netlist.NormalizeCombinational where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.BuilderCore as BuilderCore
open BuilderCore public
  using
    ( bindNet; bindingNet; bindingWire
    ; builder; builderLocalCount; builderNodes; builderBindings
    )
open import Spartan6.Netlist.Candidate public
import Spartan6.Netlist.Checked as Checked
open import Spartan6.Netlist.PortDecode public
  using
    ( LUTPortBundle; lutPortBundle; lutInputPorts; lutOutputPort
    ; parseLUTPortBundle
    ; LUT6Ports; lut6Ports; lut6I0; lut6I1; lut6I2; lut6I3
    ; lut6I4; lut6I5; lut6O; parseLUT6Ports
    ; MuxPorts; muxPorts; muxI0; muxI1; muxS; muxO; parseMuxPorts
    ; BufferPorts; bufferPorts; bufferI; bufferO; parseBufferPorts
    ; EnabledBufferPorts; enabledBufferPorts; enabledBufferI
    ; enabledBufferCE; enabledBufferO; parseEnabledBufferPorts
    ; outputNet
    )
import Spartan6.Netlist.Raw as Raw
import Spartan6.Netlist.TopInterface as TopInterface
open TopInterface public
  using
    ( collectInputConnections; collectInputNets
    ; listToVec; checkDevelopmentTarget
    )
import Spartan6.Primitive.LUT as LUT
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Parameter as Parameter
import Spartan6.Validation.Raw as Validation

open import Agda.Builtin.String using (primShowNat)

-- First executable raw-to-checked translation slice.
--
-- The input is already structurally checked.  Instances must be presented in
-- topological order, which is the canonical order expected from the external
-- flattening/normalisation stage described by IMPORT_BOUNDARY.md.  This pass
-- independently resolves every consumed net and rejects a forward reference.
-- It currently translates LUT1-LUT6, MUXF7/MUXF8, scalar IBUF/OBUF/BUFG
-- aliases, and BUFGCE suppression with canonical parameters. Sequential cells and
-- the other typed primitive evaluators are deliberately rejected until their
-- state/provenance correspondence is added.
--
-- A result is named Candidate, not Admitted: complete profile validation and
-- a whole-translation correspondence theorem remain separate obligations.

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

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

NetBinding : ℕ → ℕ → Type₀
NetBinding inputCount localCount =
  BuilderCore.NetBinding inputCount 0 localCount

Bindings : ℕ → ℕ → Type₀
Bindings inputCount localCount =
  BuilderCore.Bindings inputCount 0 localCount

liftInputWire : ∀ {inputCount localCount}
              → Checked.Wire inputCount 0 localCount
              → Checked.Wire (suc inputCount) 0 localCount
liftInputWire = BuilderCore.liftInputWire

liftInputBindings : ∀ {inputCount localCount}
                  → Bindings inputCount localCount
                  → Bindings (suc inputCount) localCount
liftInputBindings = BuilderCore.liftInputBindings

inputBindings : (net-ids : List Raw.NetId)
              → Bindings (lengthList net-ids) 0
inputBindings = BuilderCore.inputBindings

liftLocalWire : ∀ {inputCount localCount}
              → Checked.Wire inputCount 0 localCount
              → Checked.Wire inputCount 0 (suc localCount)
liftLocalWire = BuilderCore.liftLocalWire

liftLocalBindings : ∀ {inputCount localCount}
                  → Bindings inputCount localCount
                  → Bindings inputCount (suc localCount)
liftLocalBindings = BuilderCore.liftLocalBindings

lookupNet : ∀ {inputCount localCount}
          → Raw.NetId
          → Bindings inputCount localCount
          → Maybe (Checked.Wire inputCount 0 localCount)
lookupNet = BuilderCore.lookupNet

resolveConnection : ∀ {inputCount localCount}
                  → Bindings inputCount localCount
                  → Raw.Connection
                  → Maybe (Checked.Wire inputCount 0 localCount)
resolveConnection = BuilderCore.resolveConnection

unresolvedConnection : String → Raw.Connection → Diagnostic.Diagnostics
unresolvedConnection subject (Raw.net net-id) =
  singleton
    (normalisationIssue Diagnostic.undrivenInput
      subject
      "a constant, top-level input, or earlier topological instance output"
      (primShowNat net-id)
      "The combinational normaliser rejects unresolved and forward net references.")
unresolvedConnection subject (Raw.constant bit) =
  singleton
    (normalisationIssue Diagnostic.undrivenInput
      subject "a resolvable connection" "an internal resolution failure"
      "Constants are normally resolvable; this branch is retained to keep the checker total.")
unresolvedConnection subject Raw.disconnected =
  singleton
    (normalisationIssue Diagnostic.undrivenInput
      subject "a connected semantic input" "an explicit disconnection"
      "A required LUT input cannot be discarded during normalisation.")

nonScalarPort : String → Diagnostic.Diagnostics
nonScalarPort subject =
  singleton
    (normalisationIssue Diagnostic.widthMismatch
      subject "one structurally checked scalar connection"
      "a non-scalar connection list"
      "The translator remains total even though StructurallyValid makes this case unreachable for LUT6.")

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

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

Builder : ℕ → Type₀
Builder inputCount = BuilderCore.Builder inputCount 0

initialBuilder : (input-net-ids : List Raw.NetId)
               → Builder (lengthList input-net-ids)
initialBuilder input-net-ids =
  BuilderCore.initialBuilder input-net-ids []ᴸ

extendBuilder : ∀ {inputCount}
              → (current : Builder inputCount)
              → Raw.NetId
              → Checked.Node inputCount 0 (builderLocalCount current)
              → Builder inputCount
extendBuilder = BuilderCore.extendBuilder

aliasBuilder : ∀ {inputCount}
             → (current : Builder inputCount)
             → Raw.NetId
             → Checked.Wire inputCount 0 (builderLocalCount current)
             → Builder inputCount
aliasBuilder = BuilderCore.aliasBuilder

private
  legacyBindingPattern : ∀ {inputCount localCount}
    → NetBinding inputCount localCount → Raw.NetId
  legacyBindingPattern (bindNet net-id wire) = net-id

  legacyBuilderPattern : ∀ {inputCount}
    → Builder inputCount → ℕ
  legacyBuilderPattern (builder local-count nodes bindings) = local-count

  empty-initial-builder-reduces :
    initialBuilder []ᴸ ≡ builder 0 Checked.noNodes []ᴸ
  empty-initial-builder-reduces = refl

resolveLUTInputPorts : ∀ {inputCount localCount arity}
  → String
  → Bindings inputCount localCount
  → Vec Raw.RawPort arity
  → Diagnostic.CheckResult
      (Vec (Checked.Wire inputCount 0 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 arity}
  → Raw.RawInstance
  → LUT.TruthTable arity
  → LUTPortBundle arity
  → (current : Builder inputCount)
  → Diagnostic.CheckResult (Builder inputCount)
processLUTBundle item table bundle current
  with resolveLUTInputPorts
    "LUT input" (builderBindings current) (lutInputPorts bundle)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted wires
  with outputNet (Raw.rawInstanceName item) (lutOutputPort bundle)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted net-id =
  Diagnostic.accepted
    (extendBuilder current net-id (Checked.lutNode table wires))

processFixedLUT : ∀ {inputCount}
  → (arity : ℕ)
  → Raw.RawInstance
  → LUT.TruthTable arity
  → Builder inputCount
  → Diagnostic.CheckResult (Builder inputCount)
processFixedLUT arity item table current
  with parseLUTPortBundle arity (Raw.rawInstancePorts item)
... | just bundle = processLUTBundle item table bundle current
... | nothing =
  Diagnostic.rejected
    (singleton
      (normalisationIssue 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}
            → Raw.RawInstance → Builder inputCount
            → Diagnostic.CheckResult (Builder inputCount)
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 1 item table current

processLUT2 : ∀ {inputCount}
            → Raw.RawInstance → Builder inputCount
            → Diagnostic.CheckResult (Builder inputCount)
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 2 item table current

processLUT3 : ∀ {inputCount}
            → Raw.RawInstance → Builder inputCount
            → Diagnostic.CheckResult (Builder inputCount)
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 3 item table current

processLUT4 : ∀ {inputCount}
            → Raw.RawInstance → Builder inputCount
            → Diagnostic.CheckResult (Builder inputCount)
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 4 item table current

processLUT5 : ∀ {inputCount}
            → Raw.RawInstance → Builder inputCount
            → Diagnostic.CheckResult (Builder inputCount)
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 5 item table current

processParsedLUT6 : ∀ {inputCount}
                  → (item : Raw.RawInstance)
                  → LUT.LUT6Table
                  → LUT6Ports
                  → (current : Builder inputCount)
                  → Diagnostic.CheckResult (Builder inputCount)
processParsedLUT6 item table ports current
  with resolveScalarPort
    "LUT6.I0" (builderBindings current) (lut6I0 ports)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted w0
  with resolveScalarPort
    "LUT6.I1" (builderBindings current) (lut6I1 ports)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted w1
  with resolveScalarPort
    "LUT6.I2" (builderBindings current) (lut6I2 ports)
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted w2
  with resolveScalarPort
    "LUT6.I3" (builderBindings current) (lut6I3 ports)
...       | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...       | Diagnostic.accepted w3
  with resolveScalarPort
    "LUT6.I4" (builderBindings current) (lut6I4 ports)
...         | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...         | Diagnostic.accepted w4
  with resolveScalarPort
    "LUT6.I5" (builderBindings current) (lut6I5 ports)
...           | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...           | Diagnostic.accepted w5
  with outputNet (Raw.rawInstanceName item) (lut6O ports)
...             | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...             | Diagnostic.accepted net-id =
  Diagnostic.accepted
    (extendBuilder current net-id
      (Checked.lutNode table (w0 ∷ w1 ∷ w2 ∷ w3 ∷ w4 ∷ w5 ∷ [])))

processLUT6Ports : ∀ {inputCount}
                 → (item : Raw.RawInstance)
                 → (table : Parameter.CoreParameters Architecture.LUT6)
                 → (current : Builder inputCount)
                 → Diagnostic.CheckResult (Builder inputCount)
processLUT6Ports item (Parameter.lut6Parameters table) current
  with parseLUT6Ports (Raw.rawInstancePorts item)
... | just ports = processParsedLUT6 item table ports current
... | nothing =
  Diagnostic.rejected
    (singleton
      (normalisationIssue Diagnostic.widthMismatch
        (Raw.rawInstanceName item)
        "six canonical scalar inputs followed by one scalar output"
        "a different raw LUT6 port list"
        "StructurallyValid should make this branch unreachable; it remains explicit at the translation boundary."))

processParsedMux : ∀ {inputCount}
                 → String
                 → MuxPorts
                 → (current : Builder inputCount)
                 → Diagnostic.CheckResult (Builder inputCount)
processParsedMux subject ports current
  with resolveScalarPort
    "mux.I0" (builderBindings current) (muxI0 ports)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted input0
  with resolveScalarPort
    "mux.I1" (builderBindings current) (muxI1 ports)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted input1
  with resolveScalarPort
    "mux.S" (builderBindings current) (muxS ports)
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted select
  with outputNet subject (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}
                → Raw.RawInstance
                → Builder inputCount
                → Diagnostic.CheckResult (Builder inputCount)
processMuxPorts item current with parseMuxPorts (Raw.rawInstancePorts item)
... | just ports = processParsedMux (Raw.rawInstanceName item) ports current
... | nothing =
  Diagnostic.rejected
    (singleton
      (normalisationIssue 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; it remains explicit at the translation boundary."))

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

processAliasBuffer : ∀ {inputCount}
                   → Architecture.PrimitiveKind
                   → Raw.RawInstance
                   → Builder inputCount
                   → Diagnostic.CheckResult (Builder inputCount)
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 parseBufferPorts (Raw.rawInstancePorts item)
...   | nothing =
  Diagnostic.rejected
    (singleton
      (normalisationIssue Diagnostic.widthMismatch
        (Raw.rawInstanceName item) "canonical scalar I and O ports"
        "a different raw buffer port list"
        "StructurallyValid should make this branch unreachable for the selected buffer kinds."))
...   | just ports = processBufferPorts item ports current

processEnabledBufferPorts : ∀ {inputCount}
  → Raw.RawInstance
  → EnabledBufferPorts
  → Builder inputCount
  → Diagnostic.CheckResult (Builder inputCount)
processEnabledBufferPorts item ports current
  with resolveScalarPort
    "BUFGCE.I" (builderBindings current) (enabledBufferI ports)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted input-wire
  with resolveScalarPort
    "BUFGCE.CE" (builderBindings current) (enabledBufferCE ports)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted enable-wire
  with outputNet (Raw.rawInstanceName item) (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}
              → Raw.RawInstance
              → Builder inputCount
              → Diagnostic.CheckResult (Builder inputCount)
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 parseEnabledBufferPorts (Raw.rawInstancePorts item)
...   | nothing =
  Diagnostic.rejected
    (singleton
      (normalisationIssue 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

processKnownInstance : ∀ {inputCount}
                     → Architecture.PrimitiveKind
                     → Raw.RawInstance
                     → Builder inputCount
                     → Diagnostic.CheckResult (Builder inputCount)
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
  with Parameter.normaliseCoreParameters
    Architecture.LUT6
    (Raw.rawInstanceName item)
    (Raw.rawInstanceParameters item)
    (Raw.rawInstanceInitialBit item)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted parameters =
  processLUT6Ports item parameters current
processKnownInstance Architecture.MUXF7 item current =
  processMUXF7 item current
processKnownInstance Architecture.MUXF8 item current =
  processMUXF8 item current
processKnownInstance Architecture.IBUF item current =
  processAliasBuffer Architecture.IBUF item current
processKnownInstance Architecture.OBUF item current =
  processAliasBuffer Architecture.OBUF 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
      (normalisationIssue Diagnostic.unsupportedMode
        (Raw.rawInstanceName item)
        "LUT1-LUT6, MUXF7/MUXF8, IBUF/OBUF/BUFG, or BUFGCE in the combinational translation slice"
        "another primitive kind"
        "The typed evaluator may exist, but this raw-to-checked translator has not established its correspondence obligations."))

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

processInstances : ∀ {inputCount}
                 → List Raw.RawInstance
                 → Builder inputCount
                 → Diagnostic.CheckResult (Builder inputCount)
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

resolveOutputConnections : ∀ {inputCount localCount}
  → String
  → Bindings inputCount localCount
  → List Raw.Connection
  → Diagnostic.CheckResult
      (List (Checked.Wire inputCount 0 localCount))
resolveOutputConnections =
  TopInterface.resolveOutputConnectionsWith unresolvedConnection

collectOutputWires : ∀ {inputCount localCount}
  → List Raw.RawTopPort
  → Bindings inputCount localCount
  → Diagnostic.CheckResult
      (List (Checked.Wire inputCount 0 localCount))
collectOutputWires =
  TopInterface.collectOutputWiresWith unresolvedConnection

normaliseCombinational : Validation.StructurallyChecked
                       → Diagnostic.CheckResult CheckedCombinationalCandidate
normaliseCombinational (design , structural-proof)
  with checkDevelopmentTarget design
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted tt
  with collectInputNets (Raw.rawTopPorts design)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted input-net-ids
  with processInstances
    (Raw.rawInstances design) (initialBuilder input-net-ids)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted current
  with collectOutputWires
    (Raw.rawTopPorts design) (builderBindings current)
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted outputs =
  Diagnostic.accepted
    (finishCandidate
      design structural-proof input-net-ids current outputs)