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

module Spartan6.Validation.Parameter where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Foundation.Hex as Hex
import Spartan6.Netlist.Raw as Raw
import Spartan6.Primitive.LUT as LUT
import Spartan6.Validation.Diagnostic as Diagnostic

open import Agda.Builtin.String using (primStringEquality)

-- This module validates only the canonical parameter encoding at the raw
-- boundary.  It does not admit ports, connectivity, clocks, or a complete
-- instance.  In particular, a successful result here is only one obligation
-- in the larger raw-to-checked admission pipeline.
--
-- The canonical spelling of a vector-valued INIT is a fixed-width string of
-- hexadecimal digits with no prefix or separators.  That spelling is a
-- project boundary decision: an external format adapter must preserve or
-- translate its own lexical convention before invoking this checker.
--
-- For LUT6, UG615 v14.7, printed pages 186-189, documents the 64-bit INIT
-- attribute, its all-zero default, and the rule that INIT[0] corresponds to
-- all-low inputs while I0 is the least-significant address bit.  Hex decoding
-- therefore produces a table whose vector head is INIT[0].
--
-- For FDRE, UG615 v14.7, printed pages 103-104, documents binary INIT values
-- and gives low as the default/recommended value.  The canonical raw schema
-- carries this scalar in rawInstanceInitialBit, not as a string parameter.
-- FDSE uses the same scalar field; UG615 printed pages 105-106 give high as
-- its default/recommended INIT value.

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

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

defaultLUT6INIT : LUT.LUT6Table
defaultLUT6INIT = replicate low

malformedLUT6INIT : String → String → Diagnostic.Diagnostics
malformedLUT6INIT subject observed =
  singleton
    (parameterIssue Diagnostic.malformedInitialisation
      subject
      "exactly 16 hexadecimal digits in canonical INIT order"
      observed
      "LUT6 INIT must decode to exactly 64 bits; prefixes, separators, truncation, and padding are not accepted.")

illegalLUT6Parameters : String → String → Diagnostic.Diagnostics
illegalLUT6Parameters subject observed =
  singleton
    (parameterIssue Diagnostic.illegalParameter
      subject
      "zero parameters or exactly one parameter named INIT"
      observed
      "Unknown and duplicate raw parameters are rejected rather than ignored or assigned precedence.")

unexpectedVectorInitialBit : String → Diagnostic.Diagnostics
unexpectedVectorInitialBit subject =
  singleton
    (parameterIssue Diagnostic.malformedInitialisation
      subject
      "vector INIT represented by the fixed-width INIT parameter only"
      "a scalar rawInstanceInitialBit"
      "The scalar initial-bit field cannot be combined with a LUT truth table.")

normaliseLUT6ParameterList : String → List Raw.RawParameter
                           → Diagnostic.CheckResult LUT.LUT6Table
normaliseLUT6ParameterList subject []ᴸ =
  Diagnostic.accepted defaultLUT6INIT
normaliseLUT6ParameterList subject
  (Raw.rawParameter name value ∷ᴸ []ᴸ) =
  if primStringEquality name "INIT"
  then decode value
  else Diagnostic.rejected (illegalLUT6Parameters subject name)
  where
  decode : String → Diagnostic.CheckResult LUT.LUT6Table
  decode text with Hex.decodeHexINITFixed 64 text
  ... | nothing = Diagnostic.rejected (malformedLUT6INIT subject text)
  ... | just table = Diagnostic.accepted table
normaliseLUT6ParameterList subject (first ∷ᴸ second ∷ᴸ rest) =
  Diagnostic.rejected
    (illegalLUT6Parameters subject "multiple raw parameter entries")

requireNoVectorInitialBit : String → Maybe Bit
                          → Diagnostic.CheckResult Unit
requireNoVectorInitialBit subject nothing = Diagnostic.accepted tt
requireNoVectorInitialBit subject (just bit) =
  Diagnostic.rejected (unexpectedVectorInitialBit subject)

normaliseLUT6Parameters : String → List Raw.RawParameter → Maybe Bit
                       → Diagnostic.CheckResult LUT.LUT6Table
normaliseLUT6Parameters subject parameters initial-bit =
  Diagnostic.mapResult fst
    (Diagnostic.appendResult
      (normaliseLUT6ParameterList subject parameters)
      (requireNoVectorInitialBit subject initial-bit))

malformedFixedINIT : String → String → String → Diagnostic.Diagnostics
malformedFixedINIT subject expected observed =
  singleton
    (parameterIssue Diagnostic.malformedInitialisation
      subject expected observed
      "The canonical vector INIT decoder requires an exact hexadecimal width and never truncates or pads.")

normaliseFixedINITParameterList : (bit-count : ℕ)
  → String
  → Vec Bit bit-count
  → String
  → List Raw.RawParameter
  → Diagnostic.CheckResult (Vec Bit bit-count)
normaliseFixedINITParameterList bit-count expected default subject []ᴸ =
  Diagnostic.accepted default
normaliseFixedINITParameterList bit-count expected default subject
  (Raw.rawParameter name value ∷ᴸ []ᴸ) =
  if primStringEquality name "INIT"
  then decode value
  else Diagnostic.rejected (illegalLUT6Parameters subject name)
  where
  decode : String → Diagnostic.CheckResult (Vec Bit bit-count)
  decode text with Hex.decodeHexINITFixed bit-count text
  ... | nothing =
    Diagnostic.rejected (malformedFixedINIT subject expected text)
  ... | just table = Diagnostic.accepted table
normaliseFixedINITParameterList bit-count expected default subject
  (first ∷ᴸ second ∷ᴸ rest) =
  Diagnostic.rejected
    (illegalLUT6Parameters subject "multiple raw parameter entries")

normaliseFixedVectorParameters : (bit-count : ℕ)
  → String
  → Vec Bit bit-count
  → String
  → List Raw.RawParameter
  → Maybe Bit
  → Diagnostic.CheckResult (Vec Bit bit-count)
normaliseFixedVectorParameters bit-count expected default subject
  parameters initial-bit =
  Diagnostic.mapResult fst
    (Diagnostic.appendResult
      (normaliseFixedINITParameterList
        bit-count expected default subject parameters)
      (requireNoVectorInitialBit subject initial-bit))

defaultLUT2INIT : LUT.TruthTable 2
defaultLUT2INIT = replicate low

defaultLUT1INIT : LUT.TruthTable 1
defaultLUT1INIT = replicate low

defaultLUT3INIT : LUT.TruthTable 3
defaultLUT3INIT = replicate low

defaultLUT4INIT : LUT.TruthTable 4
defaultLUT4INIT = replicate low

defaultLUT5INIT : LUT.TruthTable 5
defaultLUT5INIT = replicate low

normaliseLUT1ParameterList : String → List Raw.RawParameter
                           → Diagnostic.CheckResult (LUT.TruthTable 1)
normaliseLUT1ParameterList subject []ᴸ =
  Diagnostic.accepted defaultLUT1INIT
normaliseLUT1ParameterList subject
  (Raw.rawParameter name value ∷ᴸ []ᴸ) =
  if primStringEquality name "INIT"
  then decode value
  else Diagnostic.rejected (illegalLUT6Parameters subject name)
  where
  decode : String → Diagnostic.CheckResult (LUT.TruthTable 1)
  decode text with Hex.decodeHexINIT2 text
  ... | nothing =
    Diagnostic.rejected
      (malformedFixedINIT subject
        "exactly 1 hexadecimal digit in the range 0..3 encoding 2 INIT bits"
        text)
  ... | just table = Diagnostic.accepted table
normaliseLUT1ParameterList subject (first ∷ᴸ second ∷ᴸ rest) =
  Diagnostic.rejected
    (illegalLUT6Parameters subject "multiple raw parameter entries")

normaliseLUT1Parameters : String → List Raw.RawParameter → Maybe Bit
                       → Diagnostic.CheckResult (LUT.TruthTable 1)
normaliseLUT1Parameters subject parameters initial-bit =
  Diagnostic.mapResult fst
    (Diagnostic.appendResult
      (normaliseLUT1ParameterList subject parameters)
      (requireNoVectorInitialBit subject initial-bit))

normaliseLUT2Parameters : String → List Raw.RawParameter → Maybe Bit
                       → Diagnostic.CheckResult (LUT.TruthTable 2)
normaliseLUT2Parameters =
  normaliseFixedVectorParameters 4
    "exactly 1 hexadecimal digit encoding 4 INIT bits"
    defaultLUT2INIT

normaliseLUT3Parameters : String → List Raw.RawParameter → Maybe Bit
                       → Diagnostic.CheckResult (LUT.TruthTable 3)
normaliseLUT3Parameters =
  normaliseFixedVectorParameters 8
    "exactly 2 hexadecimal digits encoding 8 INIT bits"
    defaultLUT3INIT

normaliseLUT4Parameters : String → List Raw.RawParameter → Maybe Bit
                       → Diagnostic.CheckResult (LUT.TruthTable 4)
normaliseLUT4Parameters =
  normaliseFixedVectorParameters 16
    "exactly 4 hexadecimal digits encoding 16 INIT bits"
    defaultLUT4INIT

normaliseLUT5Parameters : String → List Raw.RawParameter → Maybe Bit
                       → Diagnostic.CheckResult (LUT.TruthTable 5)
normaliseLUT5Parameters =
  normaliseFixedVectorParameters 32
    "exactly 8 hexadecimal digits encoding 32 INIT bits"
    defaultLUT5INIT

illegalScalarRegisterParameters : String → Diagnostic.Diagnostics
illegalScalarRegisterParameters subject =
  singleton
    (parameterIssue Diagnostic.illegalParameter
      subject
      "no string parameters; INIT is represented by rawInstanceInitialBit"
      "one or more raw parameter entries"
      "The canonical boundary has exactly one representation for scalar register initial state.")

requireNoScalarRegisterParameters : String → List Raw.RawParameter
                                  → Diagnostic.CheckResult Unit
requireNoScalarRegisterParameters subject []ᴸ = Diagnostic.accepted tt
requireNoScalarRegisterParameters subject (parameter ∷ᴸ parameters) =
  Diagnostic.rejected (illegalScalarRegisterParameters subject)

normaliseFDREInitialBit : Maybe Bit → Diagnostic.CheckResult Bit
normaliseFDREInitialBit nothing = Diagnostic.accepted low
normaliseFDREInitialBit (just bit) = Diagnostic.accepted bit

normaliseFDSEInitialBit : Maybe Bit → Diagnostic.CheckResult Bit
normaliseFDSEInitialBit nothing = Diagnostic.accepted high
normaliseFDSEInitialBit (just bit) = Diagnostic.accepted bit

normaliseFDREParameters : String → List Raw.RawParameter → Maybe Bit
                       → Diagnostic.CheckResult Bit
normaliseFDREParameters subject parameters initial-bit =
  Diagnostic.mapResult snd
    (Diagnostic.appendResult
      (requireNoScalarRegisterParameters subject parameters)
      (normaliseFDREInitialBit initial-bit))

illegalParameterlessParameters : String → Diagnostic.Diagnostics
illegalParameterlessParameters subject =
  singleton
    (parameterIssue Diagnostic.illegalParameter
      subject
      "no semantic string parameters in the selected digital mode"
      "one or more raw parameter entries"
      "Unknown attributes are rejected rather than ignored by the guaranteed digital core.")

unexpectedParameterlessInitialBit : String → Diagnostic.Diagnostics
unexpectedParameterlessInitialBit subject =
  singleton
    (parameterIssue Diagnostic.malformedInitialisation
      subject
      "no initial state for a combinational primitive"
      "a scalar rawInstanceInitialBit"
      "A combinational primitive has no stored initial bit.")

requireParameterlessList : String → List Raw.RawParameter
                         → Diagnostic.CheckResult Unit
requireParameterlessList subject []ᴸ = Diagnostic.accepted tt
requireParameterlessList subject (parameter ∷ᴸ parameters) =
  Diagnostic.rejected (illegalParameterlessParameters subject)

requireNoParameterlessInitialBit : String → Maybe Bit
                                 → Diagnostic.CheckResult Unit
requireNoParameterlessInitialBit subject nothing = Diagnostic.accepted tt
requireNoParameterlessInitialBit subject (just bit) =
  Diagnostic.rejected (unexpectedParameterlessInitialBit subject)

normaliseParameterless : String → List Raw.RawParameter → Maybe Bit
                       → Diagnostic.CheckResult Unit
normaliseParameterless subject parameters initial-bit =
  Diagnostic.mapResult fst
    (Diagnostic.appendResult
      (requireParameterlessList subject parameters)
      (requireNoParameterlessInitialBit subject initial-bit))

-- Only configurations whose exact raw encoding is validated here have a
-- constructor.  Other primitive kinds remain rejected by this parameter
-- normaliser even when a separately constructed typed evaluator exists.

data CoreParameters : Architecture.PrimitiveKind → Type₀ where
  lut1Parameters : LUT.TruthTable 1 → CoreParameters Architecture.LUT1
  lut2Parameters : LUT.TruthTable 2 → CoreParameters Architecture.LUT2
  lut3Parameters : LUT.TruthTable 3 → CoreParameters Architecture.LUT3
  lut4Parameters : LUT.TruthTable 4 → CoreParameters Architecture.LUT4
  lut5Parameters : LUT.TruthTable 5 → CoreParameters Architecture.LUT5
  lut6Parameters : LUT.LUT6Table → CoreParameters Architecture.LUT6
  muxf7Parameters : CoreParameters Architecture.MUXF7
  muxf8Parameters : CoreParameters Architecture.MUXF8
  carry4Parameters : CoreParameters Architecture.CARRY4
  fdreParameters : Bit → CoreParameters Architecture.FDRE
  fdseParameters : Bit → CoreParameters Architecture.FDSE
  ibufParameters : CoreParameters Architecture.IBUF
  obufParameters : CoreParameters Architecture.OBUF
  obufdsParameters : CoreParameters Architecture.OBUFDS
  bufgParameters : CoreParameters Architecture.BUFG
  bufgceParameters : CoreParameters Architecture.BUFGCE

unsupportedParameterMode : String → Diagnostic.Diagnostics
unsupportedParameterMode subject =
  singleton
    (parameterIssue Diagnostic.unsupportedMode
      subject
      "a primitive with a complete canonical parameter decoder"
      "a primitive whose raw parameter mode is not normalized here"
      "Typed primitive semantics alone does not justify raw parameter admission.")

normaliseCoreParameters : (kind : Architecture.PrimitiveKind)
                        → String
                        → List Raw.RawParameter
                        → Maybe Bit
                        → Diagnostic.CheckResult (CoreParameters kind)
normaliseCoreParameters Architecture.LUT1 subject parameters initial-bit =
  Diagnostic.mapResult lut1Parameters
    (normaliseLUT1Parameters subject parameters initial-bit)
normaliseCoreParameters Architecture.LUT2 subject parameters initial-bit =
  Diagnostic.mapResult lut2Parameters
    (normaliseLUT2Parameters subject parameters initial-bit)
normaliseCoreParameters Architecture.LUT3 subject parameters initial-bit =
  Diagnostic.mapResult lut3Parameters
    (normaliseLUT3Parameters subject parameters initial-bit)
normaliseCoreParameters Architecture.LUT4 subject parameters initial-bit =
  Diagnostic.mapResult lut4Parameters
    (normaliseLUT4Parameters subject parameters initial-bit)
normaliseCoreParameters Architecture.LUT5 subject parameters initial-bit =
  Diagnostic.mapResult lut5Parameters
    (normaliseLUT5Parameters subject parameters initial-bit)
normaliseCoreParameters Architecture.LUT6 subject parameters initial-bit =
  Diagnostic.mapResult lut6Parameters
    (normaliseLUT6Parameters subject parameters initial-bit)
normaliseCoreParameters Architecture.MUXF7 subject parameters initial-bit =
  Diagnostic.mapResult (λ ignored → muxf7Parameters)
    (normaliseParameterless subject parameters initial-bit)
normaliseCoreParameters Architecture.MUXF8 subject parameters initial-bit =
  Diagnostic.mapResult (λ ignored → muxf8Parameters)
    (normaliseParameterless subject parameters initial-bit)
normaliseCoreParameters Architecture.CARRY4 subject parameters initial-bit =
  Diagnostic.mapResult (λ ignored → carry4Parameters)
    (normaliseParameterless subject parameters initial-bit)
normaliseCoreParameters Architecture.FDRE subject parameters initial-bit =
  Diagnostic.mapResult fdreParameters
    (normaliseFDREParameters subject parameters initial-bit)
normaliseCoreParameters Architecture.FDSE subject parameters initial-bit =
  Diagnostic.mapResult fdseParameters
    (Diagnostic.mapResult snd
      (Diagnostic.appendResult
        (requireNoScalarRegisterParameters subject parameters)
        (normaliseFDSEInitialBit initial-bit)))
normaliseCoreParameters Architecture.SRL16E subject parameters initial-bit =
  Diagnostic.rejected (unsupportedParameterMode subject)
normaliseCoreParameters Architecture.RAM64X1S subject parameters initial-bit =
  Diagnostic.rejected (unsupportedParameterMode subject)
normaliseCoreParameters Architecture.IBUF subject parameters initial-bit =
  Diagnostic.mapResult (λ ignored → ibufParameters)
    (normaliseParameterless subject parameters initial-bit)
normaliseCoreParameters Architecture.OBUF subject parameters initial-bit =
  Diagnostic.mapResult (λ ignored → obufParameters)
    (normaliseParameterless subject parameters initial-bit)
normaliseCoreParameters Architecture.OBUFDS subject parameters initial-bit =
  Diagnostic.mapResult (λ ignored → obufdsParameters)
    (normaliseParameterless subject parameters initial-bit)
normaliseCoreParameters Architecture.OBUFT subject parameters initial-bit =
  Diagnostic.rejected (unsupportedParameterMode subject)
normaliseCoreParameters Architecture.BUFG subject parameters initial-bit =
  Diagnostic.mapResult (λ ignored → bufgParameters)
    (normaliseParameterless subject parameters initial-bit)
normaliseCoreParameters Architecture.BUFGCE subject parameters initial-bit =
  Diagnostic.mapResult (λ ignored → bufgceParameters)
    (normaliseParameterless subject parameters initial-bit)

CoreParameterResult : Type₀
CoreParameterResult =
  Σ Architecture.PrimitiveKind CoreParameters

normaliseInstanceCoreParameters : Raw.RawInstance
                                → Diagnostic.CheckResult CoreParameterResult
normaliseInstanceCoreParameters item with Raw.rawInstanceKind item
... | Raw.unknownPrimitive name =
  Diagnostic.rejected
    (singleton
      (parameterIssue Diagnostic.unknownPrimitive
        (Raw.rawInstanceName item)
        "a primitive kind with a canonical parameter decoder"
        name
        "An unknown primitive has no parameter semantics."))
... | Raw.knownPrimitive kind =
  Diagnostic.mapResult (λ configuration → kind , configuration)
    (normaliseCoreParameters
      kind
      (Raw.rawInstanceName item)
      (Raw.rawInstanceParameters item)
      (Raw.rawInstanceInitialBit item))

-- Reduction checks cover defaults, explicit values, INIT bit order, malformed
-- width, duplicate parameters, and the scalar/vector representation split.

lut6-default-is-zero :
  normaliseLUT6Parameters "u_lut" []ᴸ nothing
  ≡ Diagnostic.accepted defaultLUT6INIT
lut6-default-is-zero = refl

lut6-explicit-one-places-high-at-INIT0 :
  normaliseLUT6Parameters "u_lut"
    (Raw.rawParameter "INIT" "0000000000000001" ∷ᴸ []ᴸ)
    nothing
  ≡ Diagnostic.accepted (high ∷ replicate low)
lut6-explicit-one-places-high-at-INIT0 = refl

lut6-rejects-short-INIT :
  normaliseLUT6Parameters "u_lut"
    (Raw.rawParameter "INIT" "1" ∷ᴸ []ᴸ)
    nothing
  ≡ Diagnostic.rejected (malformedLUT6INIT "u_lut" "1")
lut6-rejects-short-INIT = refl

lut6-rejects-duplicate-parameters :
  normaliseLUT6Parameters "u_lut"
    (Raw.rawParameter "INIT" "0000000000000000"
     ∷ᴸ Raw.rawParameter "INIT" "FFFFFFFFFFFFFFFF" ∷ᴸ []ᴸ)
    nothing
  ≡ Diagnostic.rejected
      (illegalLUT6Parameters "u_lut" "multiple raw parameter entries")
lut6-rejects-duplicate-parameters = refl

lut6-rejects-scalar-initial-bit :
  normaliseLUT6Parameters "u_lut" []ᴸ (just low)
  ≡ Diagnostic.rejected (unexpectedVectorInitialBit "u_lut")
lut6-rejects-scalar-initial-bit = refl

fdre-default-is-low :
  normaliseFDREParameters "u_ff" []ᴸ nothing
  ≡ Diagnostic.accepted low
fdre-default-is-low = refl

fdre-explicit-high-is-preserved :
  normaliseFDREParameters "u_ff" []ᴸ (just high)
  ≡ Diagnostic.accepted high
fdre-explicit-high-is-preserved = refl

fdse-default-is-high :
  normaliseCoreParameters Architecture.FDSE "u_ff" []ᴸ nothing
  ≡ Diagnostic.accepted (fdseParameters high)
fdse-default-is-high = refl

muxf7-empty-parameters-are-canonical :
  normaliseCoreParameters Architecture.MUXF7 "u_mux" []ᴸ nothing
  ≡ Diagnostic.accepted muxf7Parameters
muxf7-empty-parameters-are-canonical = refl

muxf8-rejects-initial-state :
  normaliseCoreParameters Architecture.MUXF8 "u_mux" []ᴸ (just low)
  ≡ Diagnostic.rejected (unexpectedParameterlessInitialBit "u_mux")
muxf8-rejects-initial-state = refl

lut2-explicit-identity-table :
  normaliseCoreParameters Architecture.LUT2 "u_lut2"
    (Raw.rawParameter "INIT" "A" ∷ᴸ []ᴸ) nothing
  ≡ Diagnostic.accepted
      (lut2Parameters (low ∷ high ∷ low ∷ high ∷ []))
lut2-explicit-identity-table = refl

lut1-explicit-inverter-table :
  normaliseCoreParameters Architecture.LUT1 "u_lut1"
    (Raw.rawParameter "INIT" "1" ∷ᴸ []ᴸ) nothing
  ≡ Diagnostic.accepted (lut1Parameters (high ∷ low ∷ []))
lut1-explicit-inverter-table = refl

lut1-rejects-out-of-range-nibble :
  normaliseCoreParameters Architecture.LUT1 "u_lut1"
    (Raw.rawParameter "INIT" "4" ∷ᴸ []ᴸ) nothing
  ≡ Diagnostic.rejected
      (malformedFixedINIT "u_lut1"
        "exactly 1 hexadecimal digit in the range 0..3 encoding 2 INIT bits"
        "4")
lut1-rejects-out-of-range-nibble = refl

lut5-rejects-short-INIT :
  normaliseCoreParameters Architecture.LUT5 "u_lut5"
    (Raw.rawParameter "INIT" "0" ∷ᴸ []ᴸ) nothing
  ≡ Diagnostic.rejected
      (malformedFixedINIT "u_lut5"
        "exactly 8 hexadecimal digits encoding 32 INIT bits" "0")
lut5-rejects-short-INIT = refl

fdre-rejects-string-INIT :
  normaliseFDREParameters "u_ff"
    (Raw.rawParameter "INIT" "0" ∷ᴸ []ᴸ)
    nothing
  ≡ Diagnostic.rejected (illegalScalarRegisterParameters "u_ff")
fdre-rejects-string-INIT = refl