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

module Spartan6.Validation.ParameterlessSoundness where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.Raw as Raw
open import Spartan6.Validation.CheckResult using (rejected≢accepted)
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Parameter as Parameter

open import Cubical.Foundations.Path using (inspect; [_]ᵢ)
import Cubical.Data.Empty as Empty

-- The exact canonical raw representation shared by the selected stateless
-- parameterless modes: no string attributes and no scalar initial-state bit.
-- This predicate says nothing about ports, connectivity, placement, timing,
-- electrical attributes, or whole-instance/profile admission.

data CanonicalParameterlessRaw
  : List Raw.RawParameter → Maybe Bit → Type₀ where
  canonicalParameterlessRaw :
    CanonicalParameterlessRaw []ᴸ nothing

-- Soundness and completeness of the shared checker itself.

normaliseParameterless-sound : ∀ subject parameters initial-bit
  → Parameter.normaliseParameterless subject parameters initial-bit
    ≡ Diagnostic.accepted tt
  → CanonicalParameterlessRaw parameters initial-bit
normaliseParameterless-sound subject []ᴸ nothing result =
  canonicalParameterlessRaw
normaliseParameterless-sound subject []ᴸ (just bit) result =
  Empty.rec (rejected≢accepted result)
normaliseParameterless-sound
  subject (parameter ∷ᴸ parameters) nothing result =
  Empty.rec (rejected≢accepted result)
normaliseParameterless-sound
  subject (parameter ∷ᴸ parameters) (just bit) result =
  Empty.rec (rejected≢accepted result)

normaliseParameterless-complete : ∀ subject {parameters initial-bit}
  → CanonicalParameterlessRaw parameters initial-bit
  → Parameter.normaliseParameterless subject parameters initial-bit
    ≡ Diagnostic.accepted tt
normaliseParameterless-complete subject canonicalParameterlessRaw = refl

-- normaliseCoreParameters implements each selected mode by mapping its typed
-- constructor over normaliseParameterless.  These generic lemmas preserve the
-- raw characterization through exactly that map, without claiming that every
-- parameterless primitive kind is supported.

mapParameterless-sound : ∀ {A : Type₀}
  (wrap : Unit → A) subject parameters initial-bit
  → Diagnostic.mapResult wrap
      (Parameter.normaliseParameterless subject parameters initial-bit)
    ≡ Diagnostic.accepted (wrap tt)
  → CanonicalParameterlessRaw parameters initial-bit
mapParameterless-sound wrap subject parameters initial-bit result with
  Parameter.normaliseParameterless subject parameters initial-bit
  | inspect
      (Parameter.normaliseParameterless subject parameters)
      initial-bit
... | Diagnostic.rejected diagnostics | [ parameter-path ]ᵢ =
  Empty.rec (rejected≢accepted result)
... | Diagnostic.accepted tt | [ parameter-path ]ᵢ =
  normaliseParameterless-sound
    subject parameters initial-bit parameter-path

mapParameterless-complete : ∀ {A : Type₀}
  (wrap : Unit → A) subject {parameters initial-bit}
  → CanonicalParameterlessRaw parameters initial-bit
  → Diagnostic.mapResult wrap
      (Parameter.normaliseParameterless subject parameters initial-bit)
    ≡ Diagnostic.accepted (wrap tt)
mapParameterless-complete wrap subject canonicalParameterlessRaw = refl

-- MUXF7.

muxf7-parameterless-sound : ∀ subject parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.MUXF7 subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.muxf7Parameters
  → CanonicalParameterlessRaw parameters initial-bit
muxf7-parameterless-sound subject parameters initial-bit result =
  mapParameterless-sound
    (λ ignored → Parameter.muxf7Parameters)
    subject parameters initial-bit result

muxf7-parameterless-complete : ∀ subject {parameters initial-bit}
  → CanonicalParameterlessRaw parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.MUXF7 subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.muxf7Parameters
muxf7-parameterless-complete subject canonical =
  mapParameterless-complete
    (λ ignored → Parameter.muxf7Parameters) subject canonical

-- MUXF8.

muxf8-parameterless-sound : ∀ subject parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.MUXF8 subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.muxf8Parameters
  → CanonicalParameterlessRaw parameters initial-bit
muxf8-parameterless-sound subject parameters initial-bit result =
  mapParameterless-sound
    (λ ignored → Parameter.muxf8Parameters)
    subject parameters initial-bit result

muxf8-parameterless-complete : ∀ subject {parameters initial-bit}
  → CanonicalParameterlessRaw parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.MUXF8 subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.muxf8Parameters
muxf8-parameterless-complete subject canonical =
  mapParameterless-complete
    (λ ignored → Parameter.muxf8Parameters) subject canonical

-- CARRY4.

carry4-parameterless-sound : ∀ subject parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.CARRY4 subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.carry4Parameters
  → CanonicalParameterlessRaw parameters initial-bit
carry4-parameterless-sound subject parameters initial-bit result =
  mapParameterless-sound
    (λ ignored → Parameter.carry4Parameters)
    subject parameters initial-bit result

carry4-parameterless-complete : ∀ subject {parameters initial-bit}
  → CanonicalParameterlessRaw parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.CARRY4 subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.carry4Parameters
carry4-parameterless-complete subject canonical =
  mapParameterless-complete
    (λ ignored → Parameter.carry4Parameters) subject canonical

-- IBUF.

ibuf-parameterless-sound : ∀ subject parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.IBUF subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.ibufParameters
  → CanonicalParameterlessRaw parameters initial-bit
ibuf-parameterless-sound subject parameters initial-bit result =
  mapParameterless-sound
    (λ ignored → Parameter.ibufParameters)
    subject parameters initial-bit result

ibuf-parameterless-complete : ∀ subject {parameters initial-bit}
  → CanonicalParameterlessRaw parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.IBUF subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.ibufParameters
ibuf-parameterless-complete subject canonical =
  mapParameterless-complete
    (λ ignored → Parameter.ibufParameters) subject canonical

-- OBUF.

obuf-parameterless-sound : ∀ subject parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.OBUF subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.obufParameters
  → CanonicalParameterlessRaw parameters initial-bit
obuf-parameterless-sound subject parameters initial-bit result =
  mapParameterless-sound
    (λ ignored → Parameter.obufParameters)
    subject parameters initial-bit result

obuf-parameterless-complete : ∀ subject {parameters initial-bit}
  → CanonicalParameterlessRaw parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.OBUF subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.obufParameters
obuf-parameterless-complete subject canonical =
  mapParameterless-complete
    (λ ignored → Parameter.obufParameters) subject canonical

-- OBUFDS.

obufds-parameterless-sound : ∀ subject parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.OBUFDS subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.obufdsParameters
  → CanonicalParameterlessRaw parameters initial-bit
obufds-parameterless-sound subject parameters initial-bit result =
  mapParameterless-sound
    (λ ignored → Parameter.obufdsParameters)
    subject parameters initial-bit result

obufds-parameterless-complete : ∀ subject {parameters initial-bit}
  → CanonicalParameterlessRaw parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.OBUFDS subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.obufdsParameters
obufds-parameterless-complete subject canonical =
  mapParameterless-complete
    (λ ignored → Parameter.obufdsParameters) subject canonical

-- BUFG.

bufg-parameterless-sound : ∀ subject parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.BUFG subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.bufgParameters
  → CanonicalParameterlessRaw parameters initial-bit
bufg-parameterless-sound subject parameters initial-bit result =
  mapParameterless-sound
    (λ ignored → Parameter.bufgParameters)
    subject parameters initial-bit result

bufg-parameterless-complete : ∀ subject {parameters initial-bit}
  → CanonicalParameterlessRaw parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.BUFG subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.bufgParameters
bufg-parameterless-complete subject canonical =
  mapParameterless-complete
    (λ ignored → Parameter.bufgParameters) subject canonical

-- BUFGCE.

bufgce-parameterless-sound : ∀ subject parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.BUFGCE subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.bufgceParameters
  → CanonicalParameterlessRaw parameters initial-bit
bufgce-parameterless-sound subject parameters initial-bit result =
  mapParameterless-sound
    (λ ignored → Parameter.bufgceParameters)
    subject parameters initial-bit result

bufgce-parameterless-complete : ∀ subject {parameters initial-bit}
  → CanonicalParameterlessRaw parameters initial-bit
  → Parameter.normaliseCoreParameters
      Architecture.BUFGCE subject parameters initial-bit
    ≡ Diagnostic.accepted Parameter.bufgceParameters
bufgce-parameterless-complete subject canonical =
  mapParameterless-complete
    (λ ignored → Parameter.bufgceParameters) subject canonical

-- Checked rejection boundaries.  An attribute's spelling or multiplicity
-- never makes it ignorable, and a combinational primitive never acquires a
-- scalar initial state through this raw mode.

unknown-attribute-is-rejected :
  Parameter.normaliseParameterless
    "u_mux"
    (Raw.rawParameter "UNKNOWN" "1" ∷ᴸ []ᴸ)
    nothing
  ≡ Diagnostic.rejected
      (Parameter.illegalParameterlessParameters "u_mux")
unknown-attribute-is-rejected = refl

duplicate-attributes-are-rejected-through-core :
  Parameter.normaliseCoreParameters
    Architecture.OBUF
    "u_obuf"
    (Raw.rawParameter "IOSTANDARD" "LVCMOS33"
     ∷ᴸ Raw.rawParameter "IOSTANDARD" "LVTTL"
     ∷ᴸ []ᴸ)
    nothing
  ≡ Diagnostic.rejected
      (Parameter.illegalParameterlessParameters "u_obuf")
duplicate-attributes-are-rejected-through-core = refl

unexpected-initial-bit-is-rejected-through-core :
  Parameter.normaliseCoreParameters
    Architecture.BUFGCE "u_bufgce" []ᴸ (just high)
  ≡ Diagnostic.rejected
      (Parameter.unexpectedParameterlessInitialBit "u_bufgce")
unexpected-initial-bit-is-rejected-through-core = refl

attribute-and-initial-bit-report-both-boundaries :
  Parameter.normaliseParameterless
    "u_mux8"
    (Raw.rawParameter "UNKNOWN" "1" ∷ᴸ []ᴸ)
    (just low)
  ≡ Diagnostic.rejected
      (Parameter.illegalParameterlessParameters "u_mux8"
       ++ᴸ Parameter.unexpectedParameterlessInitialBit "u_mux8")
attribute-and-initial-bit-report-both-boundaries = refl