Syntax category for circuit-do statements.

Mirrors `circuitStmt` from `Signal.lean` so the macro
flattener logic transfers verbatim, but lowering emits
`Circuit.next` calls inside a v2 `Circuit dom S _`
expression instead of macro-managed `bundleAll!` rows. 

def Sparkle.Core.cdoStmt.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.cdoStmt : Category

Equations

• Lean.Parser.Category.cdoStmt = { }

def Sparkle.Core.«cdoStmtLet_←Signal.reg__;» : Lean.ParserDescr

let r ← Signal.reg init — declares one register.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.Core.«cdoStmt_<~__;» : Lean.ParserDescr

r <~ rhs — schedules the next-cycle value for register r.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.Core.«cdoStmtLet_:=__;» : Lean.ParserDescr

let x := expr — branch-local Lean value binding.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.Core.«cdoStmtReturn__;» : Lean.ParserDescr

return expr — produces the circuit's output Signal.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.Core.cdoStmtIf__Then__Else__ : Lean.ParserDescr

Statement-level if cond then … else … over a Signal Bool. Both branches use the same cdoStmt grammar; the macro lowers them by merging per-register <~ rows with Signal.mux cond thenRhs elseRhs. A register assigned in only one branch holds its current value on the other side.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.Core.cdoMatchArm.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.cdoMatchArm : Category

Statement-level match scrut with | pat => stmts*.

Lowered to a right-folded Signal.mux chain on equality of the scrutinee against each non-wildcard pattern, with the wildcard arm's rhs at the tail. A wildcard _ => … is required — otherwise the lowered chain has no defined fallthrough. Same per-arm restrictions as if: Signal.reg and return are forbidden inside arms; branch-local let _ := _ is allowed.

Equations

• Lean.Parser.Category.cdoMatchArm = { }

def Sparkle.Core.«cdoMatchArm|_=>__» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.Core.cdoStmtMatch__With__ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.Core.termCircuitDo___ : Lean.ParserDescr

The top-level circuit do { … } term. Wraps a sequence of cdoStmts, lowering to the appropriate Sparkle.Core.runCircuit{N} call based on how many Signal.reg declarations the body has.

Equations

• One or more equations did not get rendered due to their size.

Flattener — same shape as Signal.lean's macro.

Walks branch bodies, collapses branch-local `let` bindings
into the rhs of every following `<~`, and rejects nested
register declarations or `return` statements inside arms. 

def Sparkle.Core.collectCdoBranchAssigns (kind : String) (flat : Array (Lean.TSyntax `cdoStmt)) : Lean.MacroM (Array (Lean.Name × Lean.TSyntax `term × Lean.TSyntax `ident))

Equations

• One or more equations did not get rendered due to their size.

partial def Sparkle.Core.flattenCdoStmts (stmts : Array (Lean.TSyntax `cdoStmt)) : Lean.MacroM (Array (Lean.TSyntax `cdoStmt))

Flatten a sequence of cdoStmts, lowering any if cond then … else … to per-register muxed <~ assignments.

Recursive: nested ifs collapse bottom-up. A register assigned on only one side keeps its current value on the other (hold semantics — the missing rhs becomes the register identifier itself).

Main expansion: circuit do { … } → runCircuit{N}.

Strategy:
  1. Flatten if/else into single muxed `<~` rows.
  2. Collect all `Signal.reg` declarations in source order.
  3. Lower to the matching `runCircuit{N}` call with a body
     that uses Lean's standard `do`-notation over the v2
     Circuit monad.