/-
  IP.Net.UsbWebServer — full synthesizable top-level for the
  Tang Nano 50K USB-Web demo.

  Wiring (single `circuit do` so the synth elaborator sees one
  module):

      uart_rx_line ──> uartRxHW ──> slipDeframerHW
                                     │  outByte/outValid
                                     ▼
                                 ipv4RxParser    (sopIp = frame-start register)
                                     │
                                     ▼
                                 tcpRxParser     (sopTcp = ip-done register)
                                     │
                                     ▼
                                 httpRequestParser
                                     │  gotRequest
                                     ▼
                                 TX sequencer (74-cycle FSM)
                                     │  byte/valid/frameEnd
                                     ▼
                                 slipFramerHW ──> uartTxHW ──> uart_tx_line

  Fixed parameters (compile-time):
    src IP  : 192.168.7.2  (FPGA)
    dst IP  : 192.168.7.1  (host)
    src port: 80
    dst port: 12345
    response body: "HTTP/1.0 200 OK\r\n\r\nHello, Sparkle!"

  Clock / baud:
    27 MHz Tang Nano 50K crystal → PLL → 100 MHz design clock
    UART 1 Mbps → bitDiv = 99

  Outputs (the only board-level pins after synth):
    uart_tx_line : Bool
-/
import Sparkle
import Sparkle.Core.Lut
import IP.Net.UART
import IP.Net.SLIP
import IP.Net.IPv4
import IP.Net.TCP
import IP.Net.HTTP

namespace Sparkle.IP.Net.UsbWebServer

open Sparkle.Core
open Sparkle.Core.Domain
open Sparkle.Core.Signal
open Sparkle.IP.Net.UART
open Sparkle.IP.Net.SLIP

/-! ### TX sequencer.

    Drives an 80-cycle FSM that emits, byte by byte, a complete
    response packet: IPv4 header (20) + TCP header (20) + HTTP
    body (34) + 6-cycle slack to let slipFramer emit closing END.

    State numbering:
      0          = idle, waiting for `trigger` pulse
      1..20      = IPv4 header byte 0..19
      21..40     = TCP header byte 0..19
      41..74     = HTTP body byte 0..33
      75         = frameEnd pulse (1 cycle)
      76..79     = slack (let slipFramer finish trailing END)
      → back to 0
-/
structure TxSeqOut (dom : DomainConfig) where
  byte     : Signal dom (BitVec 8)
  valid    : Signal dom Bool
  frameEnd : Signal dom Bool

instance {dom : DomainConfig} :
    Sparkle.Core.HasDomain (TxSeqOut dom) dom := ⟨⟩

/-- Pre-computed response packet bytes (76 = 20+20+34+2-padding).
    All constants here; the synth elaborator turns this into a
    big mux. -/
def respPacketBytes : List (BitVec 8) :=
  let ipHeader : List Nat :=
    [0x45, 0x00,        -- ver/IHL, DSCP
     0x00, 0x4A,        -- total length = 74
     0x00, 0x01,        -- ID
     0x40, 0x00,        -- flags+frag (DF)
     0x40, 0x06,        -- TTL 64, proto TCP
     0x00, 0x00,        -- chksum (host accepts without checking)
     0xC0, 0xA8, 0x07, 0x02,   -- src IP = 192.168.7.2
     0xC0, 0xA8, 0x07, 0x01]   -- dst IP = 192.168.7.1
  let tcpHeader : List Nat :=
    [0x00, 0x50,        -- src port = 80
     0x30, 0x39,        -- dst port = 12345
     0x00, 0x00, 0x00, 0x00,   -- seq num
     0x00, 0x00, 0x00, 0x00,   -- ack num
     0x50, 0x18,        -- data offset 5 + flags PSH+ACK
     0xFF, 0xFF,        -- window
     0x00, 0x00,        -- chksum
     0x00, 0x00]        -- urgent
  let httpBody : List Nat :=
    -- "HTTP/1.0 200 OK\r\n\r\nHello, Sparkle!"
    [0x48, 0x54, 0x54, 0x50, 0x2F, 0x31, 0x2E, 0x30, 0x20, 0x32, 0x30, 0x30,
     0x20, 0x4F, 0x4B, 0x0D, 0x0A, 0x0D, 0x0A, 0x48, 0x65, 0x6C, 0x6C, 0x6F,
     0x2C, 0x20, 0x53, 0x70, 0x61, 0x72, 0x6B, 0x6C, 0x65, 0x21]
  (ipHeader ++ tcpHeader ++ httpBody).map (BitVec.ofNat 8 ·)

/-- Build a byte-mux: given a register holding offset 0..73,
    return the corresponding response packet byte via the
    `kLut!` macro (which fully unrolls into 74 nested
    Signal.mux's at elaboration time — synth-elaborator-
    friendly). -/
@[hardware_module] def respByteMux {dom : DomainConfig}
    (offset : Signal dom (BitVec 7)) :
    Signal dom (BitVec 8) :=
  kLut! offset [
    -- IPv4 header (20)
    Signal.pure 0x45#8, Signal.pure 0x00#8, Signal.pure 0x00#8, Signal.pure 0x4A#8,
    Signal.pure 0x00#8, Signal.pure 0x01#8, Signal.pure 0x40#8, Signal.pure 0x00#8,
    Signal.pure 0x40#8, Signal.pure 0x06#8, Signal.pure 0x00#8, Signal.pure 0x00#8,
    Signal.pure 0xC0#8, Signal.pure 0xA8#8, Signal.pure 0x07#8, Signal.pure 0x02#8,
    Signal.pure 0xC0#8, Signal.pure 0xA8#8, Signal.pure 0x07#8, Signal.pure 0x01#8,
    -- TCP header (20)
    Signal.pure 0x00#8, Signal.pure 0x50#8, Signal.pure 0x30#8, Signal.pure 0x39#8,
    Signal.pure 0x00#8, Signal.pure 0x00#8, Signal.pure 0x00#8, Signal.pure 0x00#8,
    Signal.pure 0x00#8, Signal.pure 0x00#8, Signal.pure 0x00#8, Signal.pure 0x00#8,
    Signal.pure 0x50#8, Signal.pure 0x18#8, Signal.pure 0xFF#8, Signal.pure 0xFF#8,
    Signal.pure 0x00#8, Signal.pure 0x00#8, Signal.pure 0x00#8, Signal.pure 0x00#8,
    -- HTTP body: "HTTP/1.0 200 OK\r\n\r\nHello, Sparkle!" (34)
    Signal.pure 0x48#8, Signal.pure 0x54#8, Signal.pure 0x54#8, Signal.pure 0x50#8,
    Signal.pure 0x2F#8, Signal.pure 0x31#8, Signal.pure 0x2E#8, Signal.pure 0x30#8,
    Signal.pure 0x20#8, Signal.pure 0x32#8, Signal.pure 0x30#8, Signal.pure 0x30#8,
    Signal.pure 0x20#8, Signal.pure 0x4F#8, Signal.pure 0x4B#8, Signal.pure 0x0D#8,
    Signal.pure 0x0A#8, Signal.pure 0x0D#8, Signal.pure 0x0A#8, Signal.pure 0x48#8,
    Signal.pure 0x65#8, Signal.pure 0x6C#8, Signal.pure 0x6C#8, Signal.pure 0x6F#8,
    Signal.pure 0x2C#8, Signal.pure 0x20#8, Signal.pure 0x53#8, Signal.pure 0x70#8,
    Signal.pure 0x61#8, Signal.pure 0x72#8, Signal.pure 0x6B#8, Signal.pure 0x6C#8,
    Signal.pure 0x65#8, Signal.pure 0x21#8
  ]

/-- FSM that, on each `trigger` pulse, emits a 74-byte response
    packet across the next 74 cycles with `valid` high, then a
    single `frameEnd` pulse, then idle.

    State layout:
      `running` : Bool   — false = idle, true = actively emitting
      `phase`   : BV 7  — 0..73 = byte offset (valid),
                          74 = frameEnd pulse,
                          75..79 = slack (let slipFramer drain),
                          then `running` falls and FSM goes idle.

    Separating "are we running" from "where in the sequence" lets
    `respByteMux` consume `phase` directly (0..73) without needing
    a state-1-based off-by-one ladder. -/
def txSequencer {dom : DomainConfig}
    (trigger : Signal dom Bool) :
    TxSeqOut dom :=
  circuit do
    let running ← Signal.reg false
    let phase ← Signal.reg (0#7)

    let runSig := (running : Signal dom Bool)
    let phSig := (phase : Signal dom (BitVec 7))

    let p0 := (Signal.pure 0#7 : Signal dom (BitVec 7))
    let p1 := (Signal.pure 1#7 : Signal dom (BitVec 7))
    let p73 := (Signal.pure 73#7 : Signal dom (BitVec 7))
    let p74 := (Signal.pure 74#7 : Signal dom (BitVec 7))
    let p75 := (Signal.pure 75#7 : Signal dom (BitVec 7))
    let p76 := (Signal.pure 76#7 : Signal dom (BitVec 7))
    let p77 := (Signal.pure 77#7 : Signal dom (BitVec 7))
    let p78 := (Signal.pure 78#7 : Signal dom (BitVec 7))
    let p79 := (Signal.pure 79#7 : Signal dom (BitVec 7))

    -- Detect each phase value (we need explicit equality muxes
    -- because the synth elaborator can't translate arithmetic
    -- comparisons).
    let isByteLast := (phSig === p73 : Signal dom Bool)
    let isFrameEnd := (phSig === p74 : Signal dom Bool)
    let is75 := (phSig === p75 : Signal dom Bool)
    let is76 := (phSig === p76 : Signal dom Bool)
    let is77 := (phSig === p77 : Signal dom Bool)
    let is78 := (phSig === p78 : Signal dom Bool)
    let isPhaseEnd := (phSig === p79 : Signal dom Bool)

    -- inSlack = phase ∈ [75..79]
    let inSlack :=
      ((· || ·) <$> is75 <*>
        (((· || ·) <$> is76 <*>
          (((· || ·) <$> is77 <*>
            ((is78 ||| isPhaseEnd : Signal dom Bool))
            : Signal dom Bool))
          : Signal dom Bool))
        : Signal dom Bool)
    -- inBytes = running AND phase ∈ [0..73]
    -- = running AND !isFrameEnd AND !inSlack
    let notFrameEnd := (~~~isFrameEnd : Signal dom Bool)
    let notSlack := (~~~inSlack : Signal dom Bool)
    let inBodyPhase :=
      (notFrameEnd &&& notSlack : Signal dom Bool)
    let inBytes := (runSig &&& inBodyPhase : Signal dom Bool)

    -- Phase next: when running, increment phase; when at slot 79
    -- (phaseEnd), wrap to 0 and clear running.
    -- When idle (running=false), trigger latches phase=0 and sets running=true.
    let phInc := (phSig + p1 : Signal dom (BitVec 7))
    let phNext :=
      Signal.mux trigger p0
        (Signal.mux runSig
          (Signal.mux isPhaseEnd p0 phInc)
          phSig)
    let runNext :=
      Signal.mux trigger (Signal.pure true)
        (Signal.mux isPhaseEnd (Signal.pure false) runSig)

    phase <~ phNext
    running <~ runNext

    -- Output byte = respByteMux phase  (only meaningful when
    -- inBytes is high; downstream gates on `valid`).
    let byteOut := respByteMux phSig
    -- frameEnd pulse = running AND phase == 74
    let frameEndOut := (runSig &&& isFrameEnd : Signal dom Bool)

    -- Suppress unused warning
    let _useIsByteLast := isByteLast

    return ({ byte := byteOut
            , valid := inBytes
            , frameEnd := frameEndOut } : TxSeqOut dom)

/-! ### SOP pulse generator.

    Hardware-friendly: take a `valid` stream + a `reset` pulse
    (e.g. SLIP `frameDone`), and emit a single-cycle pulse on
    the first `valid` byte after each reset.
-/
def sopPulse {dom : DomainConfig}
    (validIn : Signal dom Bool)
    (reset : Signal dom Bool) :
    Signal dom Bool :=
  circuit do
    -- `armed` register: true when waiting for the next valid.
    -- On reset we set armed=true; on the first valid while
    -- armed we pulse and clear armed.
    let armed ← Signal.reg true
    let armedSig := (armed : Signal dom Bool)
    let pulse := (armedSig &&& validIn : Signal dom Bool)
    -- next armed = (reset OR (armed AND !validIn))
    let stillArmed :=
      ((· && ·) <$> armedSig <*>
        (~~~validIn : Signal dom Bool) : Signal dom Bool)
    let armedNext := (reset ||| stillArmed : Signal dom Bool)
    armed <~ armedNext
    return pulse

/-! ### Full top-level. -/

structure WebServerOut (dom : DomainConfig) where
  /-- Serial line driven onto the BL616 TX pin. -/
  uartTx : Signal dom Bool

instance {dom : DomainConfig} :
    Sparkle.Core.HasDomain (WebServerOut dom) dom := ⟨⟩

/-- One-shot Web server module.  Takes the UART RX line plus a
    bit-divider constant (so the same module compiles for any
    baud / clock), drives the full pipeline, and exposes the
    UART TX line. -/
def usbWebServer {dom : DomainConfig}
    (uartRxLine : Signal dom Bool)
    (bitDiv : Signal dom (BitVec 16)) :
    WebServerOut dom :=
  -- All wiring is done OUTSIDE a single `circuit do` block: the
  -- individual sub-IPs are themselves `circuit do` modules, and
  -- Sparkle's elaborator inlines them as needed.
  let rx := uartRxHW uartRxLine bitDiv
  let deframer := slipDeframerHW rx.rxByte rx.rxValid

  let sopIp := sopPulse deframer.outValid deframer.frameDone

  let ipv4 := Sparkle.IP.Net.IPv4.ipv4RxParser
                deframer.outByte deframer.outValid sopIp

  let sopTcp := sopPulse deframer.outValid ipv4.done

  let tcp := Sparkle.IP.Net.TCP.tcpRxParser
               deframer.outByte deframer.outValid sopTcp

  -- HTTP parser sees all deframer bytes; it only fires on
  -- "GET " so it's tolerant of seeing the IP/TCP header
  -- bytes first (they don't match the pattern).
  let http := Sparkle.IP.Net.HTTP.httpRequestParser
                deframer.outByte deframer.outValid

  -- TX side: sequencer driven by gotRequest, then SLIP+UART.
  let txSeq := txSequencer http.gotRequest
  let framer := slipFramerHW txSeq.byte txSeq.valid txSeq.frameEnd
  let tx := uartTxHW framer.txByte framer.txValid bitDiv

  ({ uartTx := tx.txLine } : WebServerOut dom)

end Sparkle.IP.Net.UsbWebServer
