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

module Spartan6.Netlist.PortDecode where

open import Spartan6.Prelude

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

-- Dependency-light positional port decoding shared by legacy normalization and
-- the generic/specialized builders.  Name, direction, declared-width, and
-- connection-count validation remains authoritative in Validation.Raw.

record LUTPortBundle (arity : ℕ) : Type₀ where
  constructor lutPortBundle
  field
    lutInputPorts : Vec Raw.RawPort arity
    lutOutputPort : Raw.RawPort

open LUTPortBundle public

parseLUTPortBundle : (arity : ℕ) → List Raw.RawPort
                   → Maybe (LUTPortBundle arity)
parseLUTPortBundle zero (output ∷ᴸ []ᴸ) =
  just (lutPortBundle [] output)
parseLUTPortBundle zero []ᴸ = nothing
parseLUTPortBundle zero (first ∷ᴸ second ∷ᴸ rest) = nothing
parseLUTPortBundle (suc arity) []ᴸ = nothing
parseLUTPortBundle (suc arity) (input-port ∷ᴸ ports)
  with parseLUTPortBundle arity ports
... | nothing = nothing
... | just bundle =
  just
    (lutPortBundle
      (input-port ∷ lutInputPorts bundle)
      (lutOutputPort bundle))

record LUT6Ports : Type₀ where
  constructor lut6Ports
  field
    lut6I0 : Raw.RawPort
    lut6I1 : Raw.RawPort
    lut6I2 : Raw.RawPort
    lut6I3 : Raw.RawPort
    lut6I4 : Raw.RawPort
    lut6I5 : Raw.RawPort
    lut6O  : Raw.RawPort

open LUT6Ports public

parseLUT6Ports : List Raw.RawPort → Maybe LUT6Ports
parseLUT6Ports
  (p0 ∷ᴸ p1 ∷ᴸ p2 ∷ᴸ p3 ∷ᴸ p4 ∷ᴸ p5 ∷ᴸ output ∷ᴸ []ᴸ) =
  just (lut6Ports p0 p1 p2 p3 p4 p5 output)
parseLUT6Ports ports = nothing

record MuxPorts : Type₀ where
  constructor muxPorts
  field
    muxI0 : Raw.RawPort
    muxI1 : Raw.RawPort
    muxS  : Raw.RawPort
    muxO  : Raw.RawPort

open MuxPorts public

parseMuxPorts : List Raw.RawPort → Maybe MuxPorts
parseMuxPorts (input0 ∷ᴸ input1 ∷ᴸ select ∷ᴸ output ∷ᴸ []ᴸ) =
  just (muxPorts input0 input1 select output)
parseMuxPorts ports = nothing

record BufferPorts : Type₀ where
  constructor bufferPorts
  field
    bufferI : Raw.RawPort
    bufferO : Raw.RawPort

open BufferPorts public

parseBufferPorts : List Raw.RawPort → Maybe BufferPorts
parseBufferPorts (input-port ∷ᴸ output-port ∷ᴸ []ᴸ) =
  just (bufferPorts input-port output-port)
parseBufferPorts ports = nothing

record EnabledBufferPorts : Type₀ where
  constructor enabledBufferPorts
  field
    enabledBufferI  : Raw.RawPort
    enabledBufferCE : Raw.RawPort
    enabledBufferO  : Raw.RawPort

open EnabledBufferPorts public

parseEnabledBufferPorts : List Raw.RawPort → Maybe EnabledBufferPorts
parseEnabledBufferPorts
  (input-port ∷ᴸ enable-port ∷ᴸ output-port ∷ᴸ []ᴸ) =
  just (enabledBufferPorts input-port enable-port output-port)
parseEnabledBufferPorts ports = nothing

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

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

-- A scalar output must retain a raw net identity.  Constants, disconnections,
-- and non-scalar lists keep the exact legacy diagnostics.

outputNet : String → Raw.RawPort → Diagnostic.CheckResult Raw.NetId
outputNet subject port with Raw.rawPortConnections port
... | Raw.net net-id ∷ᴸ []ᴸ = Diagnostic.accepted net-id
... | Raw.constant bit ∷ᴸ []ᴸ =
  Diagnostic.rejected
    (portDecodeSingleton
      (portDecodeIssue Diagnostic.directionMismatch
        subject "a net driven by the primitive output"
        "a constant output binding"
        "A translated primitive output introduces a checked local wire."))
... | Raw.disconnected ∷ᴸ []ᴸ =
  Diagnostic.rejected
    (portDecodeSingleton
      (portDecodeIssue Diagnostic.unsupportedMode
        subject "a retained output net" "an explicitly discarded output"
        "Discarded primitive outputs are not yet represented in the checked provenance layer."))
... | connections =
  Diagnostic.rejected
    (portDecodeSingleton
      (portDecodeIssue Diagnostic.widthMismatch
        subject "one structurally checked scalar output connection"
        "a non-scalar connection list"
        "The translator remains total at the untrusted boundary."))

-- Minimal positive and negative reduction probes pin the extracted boundary.

exampleOutputPort : Raw.RawPort
exampleOutputPort =
  Raw.rawPort "O" Raw.outputPort  (Raw.net  ∷ᴸ []ᴸ)

example-output-net : outputNet "example" exampleOutputPort
                   ≡ Diagnostic.accepted 
example-output-net = refl

empty-buffer-ports-are-rejected : parseBufferPorts []ᴸ ≡ nothing
empty-buffer-ports-are-rejected = refl