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

module Spartan6.Netlist.TopInterface where

open import Spartan6.Prelude

import Spartan6.Architecture.Profile as Profile
import Spartan6.Netlist.BuilderCore as Builder
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

-- Format-neutral collection of the checked top-level interface.  The
-- connection resolver is supplied by the caller so legacy normalizers retain
-- their exact diagnostics while sharing the recursive traversal.

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

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

collectInputConnections : String → List Raw.Connection
                        → Diagnostic.CheckResult (List Raw.NetId)
collectInputConnections subject []ᴸ = Diagnostic.accepted []ᴸ
collectInputConnections subject (Raw.net net-id ∷ᴸ connections)
  with collectInputConnections subject connections
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted net-ids =
  Diagnostic.accepted (net-id ∷ᴸ net-ids)
collectInputConnections subject (Raw.constant bit ∷ᴸ connections) =
  Diagnostic.rejected
    (singleton
      (interfaceIssue Diagnostic.directionMismatch
        subject "top-level inputs connected to driven nets"
        "a constant top-level input connection"
        "External inputs become indexed checked inputs; constants belong at internal sinks."))
collectInputConnections subject (Raw.disconnected ∷ᴸ connections) =
  Diagnostic.rejected
    (singleton
      (interfaceIssue Diagnostic.undrivenInput
        subject "top-level inputs connected to driven nets"
        "an explicit disconnection"
        "A declared external input bit must have a retained internal net identity."))

collectInputNets : List Raw.RawTopPort
                 → Diagnostic.CheckResult (List Raw.NetId)
collectInputNets []ᴸ = Diagnostic.accepted []ᴸ
collectInputNets (port ∷ᴸ ports) with Raw.rawTopPortDirection port
... | Raw.bidirectionalPort =
  Diagnostic.rejected
    (singleton
      (interfaceIssue Diagnostic.unsupportedMode
        (Raw.rawTopPortName port) "input or output" "bidirectional"
        "Resolved bidirectional behavior is outside the checked two-valued core."))
... | Raw.outputPort = collectInputNets ports
... | Raw.inputPort
  with collectInputConnections
    (Raw.rawTopPortName port) (Raw.rawTopPortConnections port)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted here
  with collectInputNets ports
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted later =
  Diagnostic.accepted (here ++ᴸ later)

resolveOutputConnectionsWith :
  ∀ {inputCount registerCount localCount}
  → (String → Raw.Connection → Diagnostic.Diagnostics)
  → String
  → Builder.Bindings inputCount registerCount localCount
  → List Raw.Connection
  → Diagnostic.CheckResult
      (List (Checked.Wire inputCount registerCount localCount))
resolveOutputConnectionsWith unresolved subject bindings []ᴸ =
  Diagnostic.accepted []ᴸ
resolveOutputConnectionsWith unresolved subject bindings
  (connection ∷ᴸ connections)
  with Builder.resolveConnection bindings connection
... | nothing = Diagnostic.rejected (unresolved subject connection)
... | just wire
  with resolveOutputConnectionsWith unresolved subject bindings connections
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted wires =
  Diagnostic.accepted (wire ∷ᴸ wires)

collectOutputWiresWith :
  ∀ {inputCount registerCount localCount}
  → (String → Raw.Connection → Diagnostic.Diagnostics)
  → List Raw.RawTopPort
  → Builder.Bindings inputCount registerCount localCount
  → Diagnostic.CheckResult
      (List (Checked.Wire inputCount registerCount localCount))
collectOutputWiresWith unresolved []ᴸ bindings = Diagnostic.accepted []ᴸ
collectOutputWiresWith unresolved (port ∷ᴸ ports) bindings
  with Raw.rawTopPortDirection port
... | Raw.bidirectionalPort =
  Diagnostic.rejected
    (singleton
      (interfaceIssue Diagnostic.unsupportedMode
        (Raw.rawTopPortName port) "input or output" "bidirectional"
        "Resolved bidirectional behavior is outside the checked two-valued core."))
... | Raw.inputPort = collectOutputWiresWith unresolved ports bindings
... | Raw.outputPort
  with resolveOutputConnectionsWith unresolved
    (Raw.rawTopPortName port) bindings (Raw.rawTopPortConnections port)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted here
  with collectOutputWiresWith unresolved ports bindings
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted later =
  Diagnostic.accepted (here ++ᴸ later)

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

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

collectBuilderOutputWires : ∀ {inputCount registerCount}
  → List Raw.RawTopPort
  → (current : Builder.Builder inputCount registerCount)
  → Diagnostic.CheckResult
      (List
        (Checked.Wire inputCount registerCount
          (Builder.builderLocalCount current)))
collectBuilderOutputWires ports current =
  collectOutputWires ports (Builder.builderBindings current)

listToVec : ∀ {ℓ} {A : Type ℓ} (values : List A)
          → Vec A (lengthList values)
listToVec []ᴸ = []
listToVec (value ∷ᴸ values) = value ∷ listToVec values

checkDevelopmentTarget : Raw.RawDesign → Diagnostic.CheckResult Unit
checkDevelopmentTarget design with
  Validation.targetDiagnosticsFor Profile.developmentProfile design
... | []ᴸ = Diagnostic.accepted tt
... | problem ∷ᴸ problems = Diagnostic.rejected (problem ∷ᴸ problems)