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

module Spartan6.Netlist.BuildOBUFDS where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.BuilderCore as Generic
import Spartan6.Netlist.PortDecode as PortDecode
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Parameter as Parameter
import Spartan6.Validation.Raw as Validation

open import Cubical.Data.Nat using (_≡ᵇ_)
open import Agda.Builtin.String using (primShowNat)
open import Spartan6.Validation.CheckResult using (rejected≢accepted)
open import Cubical.Foundations.Path using (inspect; [_]ᵢ)
import Cubical.Data.Empty as Empty

-- Isolated raw-to-builder support for only the two-valued OBUFDS truth table:
-- O carries I and OB carries not I.  It adds no pad, differential signalling,
-- voltage, I/O-standard, drive-strength, slew, placement, timing, or other
-- electrical claim.  In particular, this module does not translate OBUFT and
-- introduces no high-impedance or multi-driver semantics.
--
-- OBUFDS now enters through the same indexed CoreParameters family as ordinary
-- handlers.  The specialized builder retains its narrower structural and
-- two-output evidence without bypassing the authoritative mode decoder.

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

unknownPrimitiveDiagnostics : String → String → Diagnostic.Diagnostics
unknownPrimitiveDiagnostics subject unknown =
  singleton
    (issue Diagnostic.unknownPrimitive subject
      "the known OBUFDS primitive" unknown
      "This isolated builder recognizes only the documented two-valued OBUFDS mode.")

wrongPrimitiveDiagnostics : String → Diagnostic.Diagnostics
wrongPrimitiveDiagnostics subject =
  singleton
    (issue Diagnostic.unsupportedMode subject
      "the OBUFDS primitive" "another known primitive kind"
      "No other buffer, differential, or tri-state behavior is added by this slice.")

malformedPortsDiagnostics : String → Diagnostic.Diagnostics
malformedPortsDiagnostics subject =
  singleton
    (issue Diagnostic.widthMismatch subject
      "canonical scalar I, O, and OB ports"
      "a different raw OBUFDS port list"
      "The local parser consumes exactly the structurally validated OBUFDS port order.")

sameOutputNetDiagnostics : Raw.NetId → Diagnostic.Diagnostics
sameOutputNetDiagnostics net-id =
  singleton
    (issue Diagnostic.multipleDriver (primShowNat net-id)
      "distinct raw nets for O and OB" "the same raw output net"
      "Complementary outputs retain separate raw net identities in the checked builder.")

record OBUFDSPorts : Type₀ where
  constructor obufdsPorts
  field
    obufdsI  : Raw.RawPort
    obufdsO  : Raw.RawPort
    obufdsOB : Raw.RawPort

open OBUFDSPorts public

-- Exact names, directions, declared widths, and connection counts are checked
-- by instanceStructuralDiagnostics before this positional parser is used.

parseOBUFDSPorts : List Raw.RawPort → Maybe OBUFDSPorts
parseOBUFDSPorts
  (input-port ∷ᴸ positive-port ∷ᴸ negative-port ∷ᴸ []ᴸ) =
  just (obufdsPorts input-port positive-port negative-port)
parseOBUFDSPorts ports = nothing

distinctOutputNets : Raw.NetId → Raw.NetId
                   → Diagnostic.CheckResult Unit
distinctOutputNets positive-net negative-net with
  positive-net ≡ᵇ negative-net
... | false = Diagnostic.accepted tt
... | true =
  Diagnostic.rejected (sameOutputNetDiagnostics positive-net)

-- Accepted mode evidence remains instance-indexed.  The parameter proof uses
-- the existing checker, so it entails both an empty string-parameter list and
-- no raw scalar initial bit without adding a second parameter convention.

record AcceptedOBUFDSMode (item : Raw.RawInstance) : Type₀ where
  constructor acceptedOBUFDSMode
  field
    obufdsKindAccepted :
      Raw.rawInstanceKind item
      ≡ Raw.knownPrimitive Architecture.OBUFDS
    parameterlessModeAccepted :
      Parameter.normaliseCoreParameters Architecture.OBUFDS
        (Raw.rawInstanceName item)
        (Raw.rawInstanceParameters item)
        (Raw.rawInstanceInitialBit item)
      ≡ Diagnostic.accepted Parameter.obufdsParameters

open AcceptedOBUFDSMode public

-- A successful result retains every provenance-producing decision.  The
-- final equality says precisely that O is an alias of the resolved I wire and
-- OB is the raw net bound by a newly appended explicit invertNode.

record OBUFDSBuildResult
  {inputCount registerCount : ℕ}
  (item : Raw.RawInstance)
  (current : Generic.Builder inputCount registerCount)
  : Type₀ where
  constructor obufdsBuildResult
  field
    acceptedMode : AcceptedOBUFDSMode item
    instanceShapeAccepted :
      Validation.instanceStructuralDiagnostics item ≡ []ᴸ

    parsedPorts : OBUFDSPorts
    portsParsed :
      parseOBUFDSPorts (Raw.rawInstancePorts item)
      ≡ just parsedPorts

    resolvedInput :
      Checked.Wire
        inputCount registerCount (Generic.builderLocalCount current)
    inputResolved :
      Generic.resolveScalarPort
        "OBUFDS.I" (Generic.builderBindings current)
        (obufdsI parsedPorts)
      ≡ Diagnostic.accepted resolvedInput

    positiveOutputNet : Raw.NetId
    positiveOutputAccepted :
      PortDecode.outputNet
        (Raw.rawInstanceName item) (obufdsO parsedPorts)
      ≡ Diagnostic.accepted positiveOutputNet

    negativeOutputNet : Raw.NetId
    negativeOutputAccepted :
      PortDecode.outputNet
        (Raw.rawInstanceName item) (obufdsOB parsedPorts)
      ≡ Diagnostic.accepted negativeOutputNet

    outputNetsDistinct :
      distinctOutputNets positiveOutputNet negativeOutputNet
      ≡ Diagnostic.accepted tt

    resultBuilder : Generic.Builder inputCount registerCount
    resultBuilderBuilt :
      resultBuilder
      ≡ Generic.extendBuilder
          (Generic.aliasBuilder current positiveOutputNet resolvedInput)
          negativeOutputNet
          (Checked.invertNode resolvedInput)

open OBUFDSBuildResult public

buildKnownOBUFDS : ∀ {inputCount registerCount}
  (item : Raw.RawInstance)
  → Raw.rawInstanceKind item
    ≡ Raw.knownPrimitive Architecture.OBUFDS
  → (current : Generic.Builder inputCount registerCount)
  → Diagnostic.CheckResult (OBUFDSBuildResult item current)
buildKnownOBUFDS item kind-path current with
  Validation.instanceStructuralDiagnostics item
  | inspect Validation.instanceStructuralDiagnostics item
... | problem ∷ᴸ problems | [ shape-path ]ᵢ =
  Diagnostic.rejected (problem ∷ᴸ problems)
... | []ᴸ | [ shape-path ]ᵢ with
  parseOBUFDSPorts (Raw.rawInstancePorts item)
  | inspect parseOBUFDSPorts (Raw.rawInstancePorts item)
...   | nothing | [ ports-path ]ᵢ =
  Diagnostic.rejected
    (malformedPortsDiagnostics (Raw.rawInstanceName item))
...   | just ports | [ ports-path ]ᵢ with
  Parameter.normaliseCoreParameters Architecture.OBUFDS
    (Raw.rawInstanceName item)
    (Raw.rawInstanceParameters item)
    (Raw.rawInstanceInitialBit item)
  | inspect
      (Parameter.normaliseCoreParameters Architecture.OBUFDS
        (Raw.rawInstanceName item)
        (Raw.rawInstanceParameters item))
      (Raw.rawInstanceInitialBit item)
...     | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Diagnostic.rejected diagnostics
...     | Diagnostic.accepted Parameter.obufdsParameters
          | [ parameter-path ]ᵢ with
  Generic.resolveScalarPort
    "OBUFDS.I" (Generic.builderBindings current) (obufdsI ports)
  | inspect
      (Generic.resolveScalarPort
        "OBUFDS.I" (Generic.builderBindings current))
      (obufdsI ports)
...       | Diagnostic.rejected diagnostics | [ input-path ]ᵢ =
  Diagnostic.rejected diagnostics
...       | Diagnostic.accepted input-wire | [ input-path ]ᵢ with
  PortDecode.outputNet
    (Raw.rawInstanceName item) (obufdsO ports)
  | inspect
      (PortDecode.outputNet (Raw.rawInstanceName item))
      (obufdsO ports)
...         | Diagnostic.rejected diagnostics | [ positive-path ]ᵢ =
  Diagnostic.rejected diagnostics
...         | Diagnostic.accepted positive-net | [ positive-path ]ᵢ with
  PortDecode.outputNet
    (Raw.rawInstanceName item) (obufdsOB ports)
  | inspect
      (PortDecode.outputNet (Raw.rawInstanceName item))
      (obufdsOB ports)
...           | Diagnostic.rejected diagnostics | [ negative-path ]ᵢ =
  Diagnostic.rejected diagnostics
...           | Diagnostic.accepted negative-net | [ negative-path ]ᵢ with
  distinctOutputNets positive-net negative-net
  | inspect (distinctOutputNets positive-net) negative-net
...             | Diagnostic.rejected diagnostics | [ distinct-path ]ᵢ =
  Diagnostic.rejected diagnostics
...             | Diagnostic.accepted tt | [ distinct-path ]ᵢ =
  Diagnostic.accepted
    (obufdsBuildResult
      (acceptedOBUFDSMode kind-path parameter-path)
      shape-path
      ports ports-path
      input-wire input-path
      positive-net positive-path
      negative-net negative-path
      distinct-path
      (Generic.extendBuilder
        (Generic.aliasBuilder current positive-net input-wire)
        negative-net
        (Checked.invertNode input-wire))
      refl)

buildOBUFDS : ∀ {inputCount registerCount}
  (item : Raw.RawInstance)
  → (current : Generic.Builder inputCount registerCount)
  → Diagnostic.CheckResult (OBUFDSBuildResult item current)
buildOBUFDS
  item@(Raw.rawInstance name
    (Raw.knownPrimitive Architecture.OBUFDS) ports parameters initial-bit)
  current =
  buildKnownOBUFDS item refl current
buildOBUFDS
  (Raw.rawInstance name (Raw.unknownPrimitive unknown)
    ports parameters initial-bit)
  current =
  Diagnostic.rejected (unknownPrimitiveDiagnostics name unknown)
buildOBUFDS
  (Raw.rawInstance name (Raw.knownPrimitive kind)
    ports parameters initial-bit)
  current =
  Diagnostic.rejected (wrongPrimitiveDiagnostics name)

-- Builder-only projection for callers that do not need to retain the witness.

processOBUFDS : ∀ {inputCount registerCount}
  → Raw.RawInstance
  → Generic.Builder inputCount registerCount
  → Diagnostic.CheckResult (Generic.Builder inputCount registerCount)
processOBUFDS item current =
  Diagnostic.mapResult resultBuilder (buildOBUFDS item current)

-- Even after projecting to a bare Builder, successful processing can only
-- have arisen from the accepted instance-indexed OBUFDS mode.

processOBUFDS-mode-sound : ∀ {inputCount registerCount}
  (item : Raw.RawInstance)
  (current next : Generic.Builder inputCount registerCount)
  → processOBUFDS item current ≡ Diagnostic.accepted next
  → AcceptedOBUFDSMode item
processOBUFDS-mode-sound item current next result with
  buildOBUFDS item current
... | Diagnostic.rejected diagnostics =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted built = acceptedMode built