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

module Spartan6.Netlist.NormalizeRegister where

open import Spartan6.Prelude

import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.Raw as Raw
open import Spartan6.Netlist.RegisterMode public
  using
    ( lookupInputIndex
    ; RegisterPorts; registerPorts; registerD; registerC; registerCE
    ; registerControl; registerQ; parseRegisterPorts; outputNet
    ; RegisterMode; fdreMode; fdseMode; modeInitial; modeForcedValue
    ; normaliseFDREMode; normaliseFDSEMode; normaliseRegisterMode
    )
import Spartan6.Netlist.TopInterface as TopInterface
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

open import Cubical.Data.Nat using (_≡ᵇ_)
open import Agda.Builtin.String using (primShowNat)

-- A narrow but complete sequential raw-to-checked slice for exactly one FDRE
-- or FDSE instance and no combinational instances.  Clock is validated as a
-- retained top-level input and recorded explicitly, while the compiled Design
-- continues to receive its edge through the abstract Event argument.  This
-- makes the raw clock-to-event abstraction visible instead of silently using
-- the clock input as ordinary data.

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

resolveBaseConnection : (input-nets : List Raw.NetId)
                      → Raw.NetId
                      → Raw.Connection
                      → Maybe
                          (Checked.Wire
                            (lengthList input-nets)  )
resolveBaseConnection input-nets q-net (Raw.constant bit) =
  just (Checked.literalWire bit)
resolveBaseConnection input-nets q-net Raw.disconnected = nothing
resolveBaseConnection input-nets q-net (Raw.net net-id) =
  if net-id ≡ᵇ q-net
  then just (Checked.storedWire fzero)
  else external (lookupInputIndex net-id input-nets)
  where
  external : Maybe (Fin (lengthList input-nets))
           → Maybe (Checked.Wire (lengthList input-nets)  )
  external nothing = nothing
  external (just index) = just (Checked.externalWire index)

unresolved : String → Raw.Connection → Diagnostic.Diagnostics
unresolved subject (Raw.net net-id) =
  singleton
    (issue Diagnostic.undrivenInput subject
      "the register Q net, a top-level input net, or a constant"
      (primShowNat net-id)
      "The single-register normaliser does not invent a source for an unresolved net.")
unresolved subject (Raw.constant bit) =
  singleton
    (issue Diagnostic.undrivenInput subject "a resolvable connection"
      "an internal resolution failure"
      "Constants are normally resolvable; this total branch records an impossible internal mismatch.")
unresolved subject Raw.disconnected =
  singleton
    (issue Diagnostic.undrivenInput subject "a connected semantic input"
      "an explicit disconnection"
      "Required register data/control inputs may not be discarded.")

resolveBasePort : (input-nets : List Raw.NetId)
                → Raw.NetId
                → String
                → Raw.RawPort
                → Diagnostic.CheckResult
                    (Checked.Wire (lengthList input-nets)  )
resolveBasePort input-nets q-net subject port
  with Raw.rawPortConnections port
... | []ᴸ =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.widthMismatch subject "one scalar connection"
        "an empty connection list" "The checked register interface is scalar."))
... | connection ∷ᴸ []ᴸ =
  resolve-one connection
  where
  resolve-one : Raw.Connection
              → Diagnostic.CheckResult
                  (Checked.Wire (lengthList input-nets)  )
  resolve-one connection with
    resolveBaseConnection input-nets q-net connection
  ... | nothing = Diagnostic.rejected (unresolved subject connection)
  ... | just wire = Diagnostic.accepted wire
... | first ∷ᴸ second ∷ᴸ rest =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.widthMismatch subject "one scalar connection"
        "multiple connections" "The checked register interface is scalar."))

clockNetInput : (input-nets : List Raw.NetId)
              → Raw.RawPort
              → Raw.NetId
              → Diagnostic.CheckResult (Fin (lengthList input-nets))
clockNetInput input-nets port net-id with lookupInputIndex net-id input-nets
... | nothing =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.unsupportedEvent (Raw.rawPortName port)
        "a retained top-level input net used as the abstract clock"
        (primShowNat net-id)
        "Clock must be exposed at the raw boundary; generated/multiple clock handling is not yet admitted."))
... | just index = Diagnostic.accepted index

clockInput : (input-nets : List Raw.NetId)
           → Raw.RawPort
           → Diagnostic.CheckResult (Fin (lengthList input-nets))
clockInput input-nets port with Raw.rawPortConnections port
... | Raw.net net-id ∷ᴸ []ᴸ = clockNetInput input-nets port net-id
... | Raw.constant bit ∷ᴸ []ᴸ =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.unsupportedEvent (Raw.rawPortName port)
        "a retained top-level clock input" "a constant clock binding"
        "The rising-edge Event cannot be justified by a constant raw clock."))
... | Raw.disconnected ∷ᴸ []ᴸ =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.unsupportedEvent (Raw.rawPortName port)
        "a retained top-level clock input" "a disconnected clock"
        "A missing raw clock cannot justify abstract rising-edge events."))
... | connections =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.widthMismatch (Raw.rawPortName port)
        "one scalar clock connection" "a non-scalar clock connection list"
        "The initial event model has one scalar abstract clock."))

liftBaseOne : ∀ {inputCount}
            → Checked.Wire inputCount  
            → Checked.Wire inputCount  
liftBaseOne (Checked.externalWire index) = Checked.externalWire index
liftBaseOne (Checked.storedWire index) = Checked.storedWire index
liftBaseOne (Checked.localWire ())
liftBaseOne (Checked.literalWire bit) = Checked.literalWire bit

liftBaseTwo : ∀ {inputCount}
            → Checked.Wire inputCount  
            → Checked.Wire inputCount  
liftBaseTwo (Checked.externalWire index) = Checked.externalWire index
liftBaseTwo (Checked.storedWire index) = Checked.storedWire index
liftBaseTwo (Checked.localWire ())
liftBaseTwo (Checked.literalWire bit) = Checked.literalWire bit

registerNodes : ∀ {inputCount}
              → RegisterMode
              → Checked.Wire inputCount  
              → Checked.Wire inputCount  
              → Checked.Wire inputCount  
              → Checked.Nodes inputCount  
registerNodes mode data-wire enable-wire control-wire =
  (Checked.noNodes Checked.▻
    Checked.muxNode
      enable-wire
      (Checked.storedWire fzero)
      data-wire)
  Checked.▻
    Checked.muxNode
      (liftBaseOne control-wire)
      (Checked.localWire fzero)
      (Checked.literalWire (modeForcedValue mode))

resolveTopOutputConnections : (input-nets : List Raw.NetId)
  → Raw.NetId
  → String
  → List Raw.Connection
  → Diagnostic.CheckResult
      (List (Checked.Wire (lengthList input-nets)  ))
resolveTopOutputConnections input-nets q-net subject []ᴸ =
  Diagnostic.accepted []ᴸ
resolveTopOutputConnections input-nets q-net subject
  (connection ∷ᴸ connections)
  with resolveBaseConnection input-nets q-net connection
... | nothing = Diagnostic.rejected (unresolved subject connection)
... | just wire
  with resolveTopOutputConnections input-nets q-net subject connections
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted wires = Diagnostic.accepted (wire ∷ᴸ wires)

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

liftOutputWires : ∀ {inputCount}
                → List (Checked.Wire inputCount  )
                → List (Checked.Wire inputCount  )
liftOutputWires []ᴸ = []ᴸ
liftOutputWires (wire ∷ᴸ wires) =
  liftBaseTwo wire ∷ᴸ liftOutputWires wires

liftOutputVec : ∀ {inputCount}
              → (wires : List (Checked.Wire inputCount  ))
              → Vec (Checked.Wire inputCount  ) (lengthList wires)
liftOutputVec []ᴸ = []
liftOutputVec (wire ∷ᴸ wires) = liftBaseTwo wire ∷ liftOutputVec wires

record CheckedRegisterCandidate : Type₀ where
  constructor checkedRegisterCandidate
  field
    candidateSource          : Raw.RawDesign
    candidateStructuralProof : Validation.StructurallyValid candidateSource
    candidateInputCount      : ℕ
    candidateOutputCount     : ℕ
    candidateClockInput      : Fin candidateInputCount
    candidateNetlist         :
      Checked.CheckedNetlist candidateInputCount candidateOutputCount  

open CheckedRegisterCandidate public

buildCandidate :
  (design : Raw.RawDesign)
  → Validation.StructurallyValid design
  → (item : Raw.RawInstance)
  → (ports : RegisterPorts)
  → (mode : RegisterMode)
  → (input-nets : List Raw.NetId)
  → (q-net : Raw.NetId)
  → (clock-index : Fin (lengthList input-nets))
  → Checked.Wire (lengthList input-nets)  
  → Checked.Wire (lengthList input-nets)  
  → Checked.Wire (lengthList input-nets)  
  → List (Checked.Wire (lengthList input-nets)  )
  → CheckedRegisterCandidate
buildCandidate design structural-proof item ports mode input-nets q-net
  clock-index data-wire enable-wire control-wire outputs =
  checkedRegisterCandidate
    design structural-proof
    (lengthList input-nets)
    (lengthList outputs)
    clock-index
    (Checked.checkedNetlist
      (modeInitial mode ∷ [])
      (registerNodes mode data-wire enable-wire control-wire)
      (liftOutputVec outputs)
      (Checked.localWire fzero ∷ []))

normaliseParsedRegister :
  (design : Raw.RawDesign)
  → Validation.StructurallyValid design
  → Raw.RawInstance
  → RegisterPorts
  → RegisterMode
  → Diagnostic.CheckResult CheckedRegisterCandidate
normaliseParsedRegister design structural-proof item ports mode
  with TopInterface.collectInputNets (Raw.rawTopPorts design)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted input-nets with outputNet item ports
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted q-net
  with clockInput input-nets (registerC ports)
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted clock-index
  with resolveBasePort input-nets q-net "register.D" (registerD ports)
...       | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...       | Diagnostic.accepted data-wire
  with resolveBasePort input-nets q-net "register.CE" (registerCE ports)
...         | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...         | Diagnostic.accepted enable-wire
  with resolveBasePort
    input-nets q-net "register.control" (registerControl ports)
...           | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...           | Diagnostic.accepted control-wire
  with collectTopOutputs input-nets q-net (Raw.rawTopPorts design)
...             | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...             | Diagnostic.accepted outputs =
  Diagnostic.accepted
    (buildCandidate
      design structural-proof item ports mode input-nets q-net clock-index
      data-wire enable-wire control-wire outputs)

normaliseRegisterItem :
  (design : Raw.RawDesign)
  → Validation.StructurallyValid design
  → Raw.RawInstance
  → Diagnostic.CheckResult CheckedRegisterCandidate
normaliseRegisterItem design structural-proof item
  with parseRegisterPorts (Raw.rawInstancePorts item)
... | nothing =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.widthMismatch (Raw.rawInstanceName item)
        "canonical D, C, CE, control, and Q scalar ports"
        "a different raw port list"
        "StructurallyValid should make this branch unreachable for FDRE/FDSE."))
... | just ports with normaliseRegisterMode item
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted mode =
  normaliseParsedRegister design structural-proof item ports mode

wrong-count : Diagnostic.CheckResult CheckedRegisterCandidate
wrong-count =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.unsupportedMode "raw instance list"
        "exactly one FDRE or FDSE instance"
        "zero or multiple instances"
        "Multi-register and mixed combinational/state translation remains a later admission layer."))

normaliseTargetedRegister :
  (design : Raw.RawDesign)
  → Validation.StructurallyValid design
  → Raw.RawInstance
  → Diagnostic.CheckResult CheckedRegisterCandidate
normaliseTargetedRegister design structural-proof item
  with TopInterface.checkDevelopmentTarget design
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted tt =
  normaliseRegisterItem design structural-proof item

normaliseSingleRegister : Validation.StructurallyChecked
                        → Diagnostic.CheckResult CheckedRegisterCandidate
normaliseSingleRegister
  (Raw.rawDesign target top-ports (item ∷ᴸ []ᴸ) , structural-proof) =
  normaliseTargetedRegister
    (Raw.rawDesign target top-ports (item ∷ᴸ []ᴸ)) structural-proof item
normaliseSingleRegister
  (Raw.rawDesign target top-ports []ᴸ , structural-proof) =
  wrong-count
normaliseSingleRegister
  (Raw.rawDesign target top-ports (first ∷ᴸ second ∷ᴸ rest) ,
   structural-proof) =
  wrong-count