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

module Spartan6.Netlist.NormalizeRegisters where

open import Spartan6.Prelude

import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.Raw as Raw
import Spartan6.Netlist.RegisterMode as Single
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)

-- Multi-register, no-combinational-instance translation.
--
-- Every raw instance must be FDRE or FDSE, all C ports must name the same
-- retained top-level input net, and D/CE/R/S may refer to constants, any
-- top-level input, or any register Q net.  All Q nets are allocated before
-- next-state logic is constructed, so feedback and cross-coupling read the
-- same pre-event state.  The resulting CheckedNetlist has two mux nodes per
-- register and a simultaneous next-state vector.

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

record RegisterDescriptor : Type₀ where
  constructor registerDescriptor
  field
    descriptorItem  : Raw.RawInstance
    descriptorPorts : Single.RegisterPorts
    descriptorMode  : Single.RegisterMode
    descriptorQNet  : Raw.NetId

open RegisterDescriptor public

finishDescriptor : Raw.RawInstance
                 → Single.RegisterPorts
                 → Single.RegisterMode
                 → Diagnostic.CheckResult RegisterDescriptor
finishDescriptor item ports mode with Single.outputNet item ports
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted q-net =
  Diagnostic.accepted (registerDescriptor item ports mode q-net)

descriptorWithPorts : Raw.RawInstance
                    → Single.RegisterPorts
                    → Diagnostic.CheckResult RegisterDescriptor
descriptorWithPorts item ports with Single.normaliseRegisterMode item
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted mode = finishDescriptor item ports mode

normaliseDescriptor : Raw.RawInstance
                    → Diagnostic.CheckResult RegisterDescriptor
normaliseDescriptor item with
  Single.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"
        "Every instance in this slice must be a structurally valid FDRE or FDSE."))
... | just ports = descriptorWithPorts item ports

normaliseDescriptors : List Raw.RawInstance
                     → Diagnostic.CheckResult (List RegisterDescriptor)
normaliseDescriptors []ᴸ = Diagnostic.accepted []ᴸ
normaliseDescriptors (item ∷ᴸ items) with normaliseDescriptor item
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted descriptor with normaliseDescriptors items
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted descriptors =
  Diagnostic.accepted (descriptor ∷ᴸ descriptors)

clockNet : RegisterDescriptor → Diagnostic.CheckResult Raw.NetId
clockNet descriptor with
  Raw.rawPortConnections
    (Single.registerC (descriptorPorts descriptor))
... | Raw.net net-id ∷ᴸ []ᴸ = Diagnostic.accepted net-id
... | Raw.constant bit ∷ᴸ []ᴸ =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.unsupportedEvent
        (Raw.rawInstanceName (descriptorItem descriptor))
        "a retained top-level clock input net"
        "a constant clock binding"
        "The abstract rising-edge event cannot be justified by a constant clock."))
... | Raw.disconnected ∷ᴸ []ᴸ =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.unsupportedEvent
        (Raw.rawInstanceName (descriptorItem descriptor))
        "a retained top-level clock input net"
        "a disconnected clock"
        "A missing clock cannot justify the abstract rising-edge event."))
... | connections =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.widthMismatch
        (Raw.rawInstanceName (descriptorItem descriptor))
        "one scalar clock connection"
        "a non-scalar clock connection list"
        "The initial event model has one scalar clock."))

sameClock : Raw.NetId → List RegisterDescriptor
          → Diagnostic.CheckResult Unit
sameClock expected []ᴸ = Diagnostic.accepted tt
sameClock expected (descriptor ∷ᴸ descriptors) with clockNet descriptor
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted observed =
  if expected ≡ᵇ observed
  then sameClock expected descriptors
  else Diagnostic.rejected
    (singleton
      (issue Diagnostic.unsupportedEvent
        (Raw.rawInstanceName (descriptorItem descriptor))
        "the same raw clock net for every register"
        (primShowNat observed)
        "Multiple clock domains/interleavings are outside the initial event model."))

commonClock : (input-nets : List Raw.NetId)
            → List RegisterDescriptor
            → Diagnostic.CheckResult (Fin (lengthList input-nets))
commonClock input-nets []ᴸ =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.unsupportedMode "raw instance list"
        "one or more FDRE/FDSE instances" "no instances"
        "A register candidate must contain state."))
commonClock input-nets (descriptor ∷ᴸ descriptors) with clockNet descriptor
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted net-id
  with Single.lookupInputIndex net-id input-nets
...   | nothing =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.unsupportedEvent
        (Raw.rawInstanceName (descriptorItem descriptor))
        "a clock net exposed by a top-level input"
        (primShowNat net-id)
        "Generated clocks are not yet related to the single abstract event."))
...   | just index with sameClock net-id descriptors
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted tt = Diagnostic.accepted index

lookupRegisterIndex : (net-id : Raw.NetId)
  → (descriptors : List RegisterDescriptor)
  → Maybe (Fin (lengthList descriptors))
lookupRegisterIndex net-id []ᴸ = nothing
lookupRegisterIndex net-id (descriptor ∷ᴸ descriptors) =
  if net-id ≡ᵇ descriptorQNet descriptor
  then just fzero
  else liftIndex (lookupRegisterIndex net-id descriptors)
  where
  liftIndex : Maybe (Fin (lengthList descriptors))
            → Maybe (Fin (suc (lengthList descriptors)))
  liftIndex nothing = nothing
  liftIndex (just index) = just (fsuc index)

resolveRegisterBase :
  (input-nets : List Raw.NetId)
  → (descriptors : List RegisterDescriptor)
  → Raw.Connection
  → Maybe
      (Checked.Wire
        (lengthList input-nets) (lengthList descriptors) )
resolveRegisterBase input-nets descriptors (Raw.constant bit) =
  just (Checked.literalWire bit)
resolveRegisterBase input-nets descriptors Raw.disconnected = nothing
resolveRegisterBase input-nets descriptors (Raw.net net-id)
  with lookupRegisterIndex net-id descriptors
... | just index = just (Checked.storedWire index)
... | nothing = external (Single.lookupInputIndex net-id input-nets)
  where
  external : Maybe (Fin (lengthList input-nets))
           → Maybe
               (Checked.Wire
                 (lengthList input-nets) (lengthList descriptors) )
  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
      "a top-level input, register Q net, or constant"
      (primShowNat net-id)
      "The multi-register translator never invents a source for a 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.")

resolveRegisterPort :
  (input-nets : List Raw.NetId)
  → (descriptors : List RegisterDescriptor)
  → String
  → Raw.RawPort
  → Diagnostic.CheckResult
      (Checked.Wire
        (lengthList input-nets) (lengthList descriptors) )
resolveRegisterPort input-nets descriptors 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) (lengthList descriptors) )
  resolve-one connection with
    resolveRegisterBase input-nets descriptors 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."))

record ResolvedRegister (inputCount registerCount : ℕ) : Type₀ where
  constructor resolvedRegister
  field
    resolvedMode    : Single.RegisterMode
    resolvedCurrent : Checked.Wire inputCount registerCount 
    resolvedData    : Checked.Wire inputCount registerCount 
    resolvedEnable  : Checked.Wire inputCount registerCount 
    resolvedControl : Checked.Wire inputCount registerCount 

open ResolvedRegister public

resolveDescriptor :
  (input-nets : List Raw.NetId)
  → (all-descriptors : List RegisterDescriptor)
  → RegisterDescriptor
  → Diagnostic.CheckResult
      (ResolvedRegister
        (lengthList input-nets) (lengthList all-descriptors))
resolveDescriptor input-nets all-descriptors descriptor with
  lookupRegisterIndex (descriptorQNet descriptor) all-descriptors
... | nothing =
  Diagnostic.rejected
    (singleton
      (issue Diagnostic.undrivenInput
        (Raw.rawInstanceName (descriptorItem descriptor))
        "its Q net allocated in the register state vector"
        (primShowNat (descriptorQNet descriptor))
        "Every descriptor must occur in the allocation list."))
... | just current-index
  with resolveRegisterPort input-nets all-descriptors "register.D"
    (Single.registerD (descriptorPorts descriptor))
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted data-wire
  with resolveRegisterPort input-nets all-descriptors "register.CE"
    (Single.registerCE (descriptorPorts descriptor))
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted enable-wire
  with resolveRegisterPort input-nets all-descriptors "register.control"
    (Single.registerControl (descriptorPorts descriptor))
...       | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...       | Diagnostic.accepted control-wire =
  Diagnostic.accepted
    (resolvedRegister
      (descriptorMode descriptor)
      (Checked.storedWire current-index)
      data-wire enable-wire control-wire)

resolveDescriptors :
  (input-nets : List Raw.NetId)
  → (all-descriptors : List RegisterDescriptor)
  → (descriptors : List RegisterDescriptor)
  → Diagnostic.CheckResult
      (Vec
        (ResolvedRegister
          (lengthList input-nets) (lengthList all-descriptors))
        (lengthList descriptors))
resolveDescriptors input-nets all-descriptors []ᴸ = Diagnostic.accepted []
resolveDescriptors input-nets all-descriptors (descriptor ∷ᴸ descriptors)
  with resolveDescriptor input-nets all-descriptors descriptor
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted resolved with
  resolveDescriptors input-nets all-descriptors descriptors
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted rest = Diagnostic.accepted (resolved ∷ rest)

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

liftLocalTwice : ∀ {inputCount registerCount localCount}
               → Checked.Wire inputCount registerCount localCount
               → Checked.Wire inputCount registerCount
                   (suc (suc localCount))
liftLocalTwice (Checked.externalWire index) = Checked.externalWire index
liftLocalTwice (Checked.storedWire index) = Checked.storedWire index
liftLocalTwice (Checked.localWire index) =
  Checked.localWire (fsuc (fsuc index))
liftLocalTwice (Checked.literalWire bit) = Checked.literalWire bit

liftNextTwice : ∀ {inputCount registerCount localCount count}
  → Vec (Checked.Wire inputCount registerCount localCount) count
  → Vec
      (Checked.Wire inputCount registerCount (suc (suc localCount)))
      count
liftNextTwice [] = []
liftNextTwice (wire ∷ wires) =
  liftLocalTwice wire ∷ liftNextTwice wires

record BuiltNext (inputCount registerCount nextCount : ℕ) : Type₀ where
  constructor builtNext
  field
    builtLocalCount : ℕ
    builtNodes : Checked.Nodes inputCount registerCount builtLocalCount
    builtNextWires :
      Vec (Checked.Wire inputCount registerCount builtLocalCount) nextCount

open BuiltNext public

buildNext : ∀ {inputCount registerCount count}
  → Vec (ResolvedRegister inputCount registerCount) count
  → BuiltNext inputCount registerCount count
buildNext [] = builtNext  Checked.noNodes []
buildNext (resolved ∷ resolveds) with buildNext resolveds
... | builtNext local-count nodes next-wires =
  builtNext
    (suc (suc local-count))
    ((nodes Checked.▻
      Checked.muxNode
        (weakenBase (resolvedEnable resolved))
        (weakenBase (resolvedCurrent resolved))
        (weakenBase (resolvedData resolved)))
     Checked.▻
      Checked.muxNode
        (weakenBase (resolvedControl resolved))
        (Checked.localWire fzero)
        (Checked.literalWire
          (Single.modeForcedValue (resolvedMode resolved))))
    (Checked.localWire fzero ∷ liftNextTwice next-wires)

initialValues : ∀ {inputCount registerCount count}
  → Vec (ResolvedRegister inputCount registerCount) count
  → Vec Bit count
initialValues [] = []
initialValues (resolved ∷ resolveds) =
  Single.modeInitial (resolvedMode resolved) ∷ initialValues resolveds

resolveVisible :
  (input-nets : List Raw.NetId)
  → (descriptors : List RegisterDescriptor)
  → Raw.Connection
  → Maybe
      (Checked.Wire
        (lengthList input-nets) (lengthList descriptors) )
resolveVisible = resolveRegisterBase

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

collectOutputs :
  (input-nets : List Raw.NetId)
  → (descriptors : List RegisterDescriptor)
  → List Raw.RawTopPort
  → Diagnostic.CheckResult
      (List
        (Checked.Wire
          (lengthList input-nets) (lengthList descriptors) ))
collectOutputs input-nets descriptors []ᴸ = Diagnostic.accepted []ᴸ
collectOutputs input-nets descriptors (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 = collectOutputs input-nets descriptors ports
... | Raw.outputPort with
  resolveVisibleConnections input-nets descriptors
    (Raw.rawTopPortName port) (Raw.rawTopPortConnections port)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted here with collectOutputs input-nets descriptors ports
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted later = Diagnostic.accepted (here ++ᴸ later)

weakenOutputVec : ∀ {inputCount registerCount localCount}
  → (wires : List (Checked.Wire inputCount registerCount ))
  → Vec (Checked.Wire inputCount registerCount localCount)
      (lengthList wires)
weakenOutputVec []ᴸ = []
weakenOutputVec (wire ∷ᴸ wires) =
  weakenBase wire ∷ weakenOutputVec wires

record CheckedRegistersCandidate : Type₀ where
  constructor checkedRegistersCandidate
  field
    candidateSource          : Raw.RawDesign
    candidateStructuralProof : Validation.StructurallyValid candidateSource
    candidateInputCount      : ℕ
    candidateOutputCount     : ℕ
    candidateRegisterCount   : ℕ
    candidateLocalCount      : ℕ
    candidateClockInput      : Fin candidateInputCount
    candidateNetlist         :
      Checked.CheckedNetlist
        candidateInputCount candidateOutputCount
        candidateRegisterCount candidateLocalCount

open CheckedRegistersCandidate public

finishCandidate :
  (design : Raw.RawDesign)
  → Validation.StructurallyValid design
  → (input-nets : List Raw.NetId)
  → (descriptors : List RegisterDescriptor)
  → (clock-index : Fin (lengthList input-nets))
  → (resolved :
      Vec
        (ResolvedRegister
          (lengthList input-nets) (lengthList descriptors))
        (lengthList descriptors))
  → (built : BuiltNext
      (lengthList input-nets) (lengthList descriptors)
      (lengthList descriptors))
  → (outputs :
      List
        (Checked.Wire
          (lengthList input-nets) (lengthList descriptors) ))
  → CheckedRegistersCandidate
finishCandidate design structural-proof input-nets descriptors clock-index
  resolved built outputs =
  checkedRegistersCandidate
    design structural-proof
    (lengthList input-nets)
    (lengthList outputs)
    (lengthList descriptors)
    (builtLocalCount built)
    clock-index
    (Checked.checkedNetlist
      (initialValues resolved)
      (builtNodes built)
      (weakenOutputVec outputs)
      (builtNextWires built))

normaliseResolved :
  (design : Raw.RawDesign)
  → Validation.StructurallyValid design
  → (input-nets : List Raw.NetId)
  → (descriptors : List RegisterDescriptor)
  → Fin (lengthList input-nets)
  → Diagnostic.CheckResult CheckedRegistersCandidate
normaliseResolved design structural-proof input-nets descriptors clock-index
  with resolveDescriptors input-nets descriptors descriptors
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted resolved with
  collectOutputs input-nets descriptors (Raw.rawTopPorts design)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted outputs =
  Diagnostic.accepted
    (finishCandidate design structural-proof input-nets descriptors clock-index
      resolved (buildNext resolved) outputs)

normaliseWithDescriptors :
  (design : Raw.RawDesign)
  → Validation.StructurallyValid design
  → List Raw.NetId
  → List RegisterDescriptor
  → Diagnostic.CheckResult CheckedRegistersCandidate
normaliseWithDescriptors design structural-proof input-nets descriptors
  with commonClock input-nets descriptors
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted clock-index =
  normaliseResolved
    design structural-proof input-nets descriptors clock-index

normaliseRegisters : Validation.StructurallyChecked
                   → Diagnostic.CheckResult CheckedRegistersCandidate
normaliseRegisters (design , structural-proof) with
  TopInterface.checkDevelopmentTarget design
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted tt with
  TopInterface.collectInputNets (Raw.rawTopPorts design)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted input-nets with
  normaliseDescriptors (Raw.rawInstances design)
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted descriptors =
  normaliseWithDescriptors design structural-proof input-nets descriptors