instance Sparkle.Compiler.Elab.instInhabitedPort : Inhabited IR.AST.Port

Equations

• Sparkle.Compiler.Elab.instInhabitedPort = { default := { name := "default", ty := Sparkle.IR.Type.HWType.bit } }

structure Sparkle.Compiler.Elab.CompilerState : Type

Compiler state tracking variable mappings and context

• varMap : List (Lean.FVarId × String)
• clockWire : Option String
• resetWire : Option String
• exprCache : Option (IO.Ref (Lean.ExprStructMap String))

@[reducible, inline]

abbrev Sparkle.Compiler.Elab.CompilerM (α : Type) : Type

Compiler monad: combines CircuitM builder with MetaM

Equations

• Sparkle.Compiler.Elab.CompilerM = ReaderT Sparkle.Compiler.Elab.CompilerState (StateT Sparkle.IR.Builder.CircuitState Lean.MetaM)

def Sparkle.Compiler.Elab.CompilerM.getCompilerState : CompilerM CompilerState

Get the current compiler state (from ReaderT)

Equations

• Sparkle.Compiler.Elab.CompilerM.getCompilerState = read

def Sparkle.Compiler.Elab.CompilerM.lookupVar (fvarId : Lean.FVarId) : CompilerM (Option String)

Lookup a variable mapping. Consults the reader-scoped varMap first, then falls back to the persistent sparkleFvarWireMap IORef.

Equations

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

def Sparkle.Compiler.Elab.CompilerM.withVarMapping {α : Type} (fvarId : Lean.FVarId) (wireName : String) (k : CompilerM α) : CompilerM α

Execute an action with an additional variable mapping in scope

Equations

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

def Sparkle.Compiler.Elab.CompilerM.withLocalDecl {α : Type} (name : Lean.Name) (type : Lean.Expr) (k : Lean.Expr → CompilerM α) : CompilerM α

Execute an action with a new local declaration in MetaM scope

Equations

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

def Sparkle.Compiler.Elab.CompilerM.withLetDecl {α : Type} (name : Lean.Name) (type value : Lean.Expr) (k : Lean.Expr → CompilerM α) : CompilerM α

Execute an action with a new let declaration in MetaM scope (for logic values)

Equations

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

def Sparkle.Compiler.Elab.CompilerM.liftMetaM {α : Type} (m : Lean.MetaM α) : CompilerM α

Lift MetaM into CompilerM

Equations

• Sparkle.Compiler.Elab.CompilerM.liftMetaM m = liftM m

def Sparkle.Compiler.Elab.CompilerM.makeWire (hint : String) (ty : IR.Type.HWType) (named : Bool := false) : CompilerM String

Lift CircuitM operations by modifying the circuit state

def Sparkle.Compiler.Elab.CompilerM.freshName (hint : String) (named : Bool := false) : CompilerM String

Equations

• Sparkle.Compiler.Elab.CompilerM.freshName hint named = do let cs ← get match Sparkle.IR.Builder.CircuitM.freshName hint named cs with | (name, cs') => do set cs' pure name

def Sparkle.Compiler.Elab.CompilerM.emitAssign (lhs : String) (rhs : IR.AST.Expr) : CompilerM Unit

Equations

• Sparkle.Compiler.Elab.CompilerM.emitAssign lhs rhs = do let cs ← get match Sparkle.IR.Builder.CircuitM.emitAssign lhs rhs cs with | (PUnit.unit, cs') => set cs'

def Sparkle.Compiler.Elab.CompilerM.addInput (name : String) (ty : IR.Type.HWType) : CompilerM Unit

Equations

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

def Sparkle.Compiler.Elab.CompilerM.addOutput (name : String) (ty : IR.Type.HWType) : CompilerM Unit

Equations

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

def Sparkle.Compiler.Elab.CompilerM.getWireWidth (wireName : String) : CompilerM Nat

Look up the HW width of a wire by name (from wires, inputs, or outputs)

Equations

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

def Sparkle.Compiler.Elab.CompilerM.emitRegister (hint clk rst : String) (input : IR.AST.Expr) (initVal : Nat) (ty : IR.Type.HWType) (named : Bool := false) (resetKind : IR.Type.ResetKind := IR.Type.ResetKind.asynchronous) : CompilerM String

def Sparkle.Compiler.Elab.CompilerM.emitMemory (hint : String) (addrWidth dataWidth : Nat) (clk : String) (writeAddr writeData writeEnable readAddr : IR.AST.Expr) (named : Bool := false) : CompilerM String

Equations

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

def Sparkle.Compiler.Elab.CompilerM.emitMemoryComboRead (hint : String) (addrWidth dataWidth : Nat) (clk : String) (writeAddr writeData writeEnable readAddr : IR.AST.Expr) (named : Bool := false) : CompilerM String

Equations

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

def Sparkle.Compiler.Elab.CompilerM.emitInstance (moduleName instName : String) (connections : List (String × IR.AST.Expr)) : CompilerM Unit

Equations

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

def Sparkle.Compiler.Elab.CompilerM.addModuleToDesign (m : IR.AST.Module) : CompilerM Unit

Equations

• Sparkle.Compiler.Elab.CompilerM.addModuleToDesign m = do let cs ← get match Sparkle.IR.Builder.CircuitM.addModuleToDesign m cs with | (PUnit.unit, cs') => set cs'

def Sparkle.Compiler.Elab.primitiveRegistry : List (Lean.Name × IR.AST.Operator)

Primitive Registry: Maps Lean function names to IR operators

Equations

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

def Sparkle.Compiler.Elab.isPrimitive (name : Lean.Name) : Bool

Equations

• Sparkle.Compiler.Elab.isPrimitive name = Sparkle.Compiler.Elab.primitiveRegistry.any fun (x : Lean.Name × Sparkle.IR.AST.Operator) => match x with | (n, snd) => n == name

def Sparkle.Compiler.Elab.getOperator (name : Lean.Name) : Option IR.AST.Operator

Equations

• Sparkle.Compiler.Elab.getOperator name = List.lookup name Sparkle.Compiler.Elab.primitiveRegistry

partial def Sparkle.Compiler.Elab.inferHWType (type : Lean.Expr) : Lean.MetaM (Option IR.Type.HWType)

partial def Sparkle.Compiler.Elab.inferHWType.extractWidth (e : Lean.Expr) : Lean.MetaM Nat

def Sparkle.Compiler.Elab.inferResetKindFromSignal (signalType : Lean.Expr) : CompilerM IR.Type.ResetKind

Extract ResetKind from a Signal dom α expression.

We whnf-reduce the dom argument and then use Lean's evalExpr to evaluate it as a DomainConfig, reading the resetKind field directly. Falls back to .asynchronous (the historical default) if the expression doesn't reduce to a literal DomainConfig.

Equations

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

def Sparkle.Compiler.Elab.inferHWTypeFromSignal (signalType : Lean.Expr) : CompilerM IR.Type.HWType

Equations

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

partial def Sparkle.Compiler.Elab.extractNat (e : Lean.Expr) : CompilerM Nat

Helper to extract a Nat literal or OfNat.ofNat wrap.

def Sparkle.Compiler.Elab.extractBitVecLiteral (expr : Lean.Expr) : CompilerM (Nat × Nat)

Equations

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

def Sparkle.Compiler.Elab.extractNatLiteral (expr : Lean.Expr) : CompilerM (Nat × Unit)

Extract a Nat literal from an expression

Equations

• Sparkle.Compiler.Elab.extractNatLiteral expr = do let n ← Sparkle.Compiler.Elab.extractNat expr pure (n, ())

partial def Sparkle.Compiler.Elab.extractBitVecList (expr : Lean.Expr) : CompilerM (Array (Nat × Nat))

Extract values from a List (BitVec n) expression into an array of (value, width) pairs

def Sparkle.Compiler.Elab.extractBitVecArray (expr : Lean.Expr) : CompilerM (Array (Nat × Nat))

Extract values from an Array (BitVec n) expression

Equations

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

def Sparkle.Compiler.Elab.countedWhnf (e : Lean.Expr) : CompilerM Lean.Expr

Wrap a MetaM whnf with counters.

Equations

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

def Sparkle.Compiler.Elab.countedUnfoldDefinition? (e : Lean.Expr) : CompilerM (Option Lean.Expr)

Wrap Lean.Meta.unfoldDefinition? with counters.

Equations

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

def Sparkle.Compiler.Elab.cachedInferType (e : Lean.Expr) : CompilerM Lean.Expr

Equations

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

partial def Sparkle.Compiler.Elab.translateExprToWire (e : Lean.Expr) (hint : String := "wire") (isTopLevel isNamed : Bool := false) : CompilerM String

Caching shim around translateExprToWireImpl. All early- intercept handlers (Signal HAdd/HSub/etc., OfNat literals, ...) currently return straight from the inner impl, which means they never write back to the cache. Wrapping here means every successful translate caches its result — so subsequent identical sub-trees become a HashMap lookup instead of a full re-walk through ~10 handlers + Meta.

partial def Sparkle.Compiler.Elab.translateExprToWireImpl (e : Lean.Expr) (hint : String := "wire") (isTopLevel isNamed : Bool := false) : CompilerM String

partial def Sparkle.Compiler.Elab.translateExprToWireImpl.toIR (wireS : String) (fvarId : Lean.FVarId) (e : Lean.Expr) : CompilerM (Option IR.AST.Expr)

def Sparkle.Compiler.Elab.handleErrorPatterns (_e : Lean.Expr) (name : Lean.Name) (_args : Array Lean.Expr) (_hint : String) (_isNamed : Bool) : CompilerM Unit

Detect unsynthesizable patterns (if-then-else, Decidable) and throw errors

Equations

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

partial def Sparkle.Compiler.Elab.handleTupleProjections (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) : CompilerM (Option String)

Handle Signal.fst, Signal.snd, Signal.map Prod.fst/Prod.snd

partial def Sparkle.Compiler.Elab.handleApplicative (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) : CompilerM (Option String)

Handle Signal.ap — binary op lifting, concat/sshiftRight special cases.

Also handles N-ary applicative chains f <$> a₁ <*> a₂ <*> ... <*> aₙ (n ≥ 2). These desugar to nested Signal.ap calls — the outermost is Signal.ap (Signal.ap (... (Signal.map f a₁) ...) aₙ₋₁) aₙ. We strip the chain into the inner Signal.map f a₁ plus the trailing argument signals [a₂, ..., aₙ], then apply f to the wires sequentially. For chains whose f is a pure op (or / and / xor / add / etc.) operating pairwise on a left-fold, this resolves into a chain of binary IR ops.

partial def Sparkle.Compiler.Elab.handleApplicative.collectAp (acc : Array Lean.Expr) (cur : Lean.Expr) : Option (Lean.Expr × Array Lean.Expr)

partial def Sparkle.Compiler.Elab.handleBitVecOps (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) : CompilerM (Option String)

Handle BitVec.extractLsb', shifts, concat, isPrimitive dispatch

partial def Sparkle.Compiler.Elab.handleRegister (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) : CompilerM (Option String)

Handle Signal.register, Signal.registerWithEnable

partial def Sparkle.Compiler.Elab.handleMux (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) : CompilerM (Option String)

Handle Signal.mux, lutMuxTree

partial def Sparkle.Compiler.Elab.handleMemory (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) : CompilerM (Option String)

Handle Signal.memory, Signal.memoryComboRead

partial def Sparkle.Compiler.Elab.handleLoop (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) : CompilerM (Option String)

Handle Signal.loop, HWVector.get

partial def Sparkle.Compiler.Elab.handleLoop.peelMemoize : Lean.Expr → Lean.Expr

partial def Sparkle.Compiler.Elab.handleCircuitMonad (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) : CompilerM (Option String)

Handle Bind.bind / Pure.pure specialised to the Sparkle Circuit monad.

Lean's do-notation desugars to Bind.bind m k / Pure.pure v where Bind/Pure are typeclass projections. unfoldDefinition? (the default tryInline path) cannot reduce typeclass projections — it stops at the symbol with the instance still opaque, and the elaborator gives up.

For Sparkle's Circuit monad the bind/pure unfold to pure value-level Prod manipulation that the existing Prod / Signal-map rules already lower. We force a .all transparency reduce on the whole expression and recurse, mirroring how Prod.rec / Prod.casesOn are handled.

partial def Sparkle.Compiler.Elab.handleCircuitMonad.peelLambdas : Lean.Expr → Lean.Expr

partial def Sparkle.Compiler.Elab.handleDefinitionUnfold (e : Lean.Expr) (name : Lean.Name) (args : Array Lean.Expr) (hint : String) (isNamed : Bool) : CompilerM (Option String)

Handle a Lean function call by either inlining the body (the default) or emitting a sub-module instance (only when the declaration is tagged @[hardware_module]).

Default = inline keeps the generated Verilog flat, which is what most users want for alias-style helpers and small combinational functions: writing def passthrough x := x shouldn't multiply the module count of every caller.

Opt INTO sub-module emission with @[hardware_module] for designs you want to see as their own Verilog module foo block — a CPU, an ALU you intend to re-use, an arbiter, etc. Downstream tools (P&R, OOC synth, hierarchical timing) can then treat the boundary as a real compile unit.

@[inline_hardware] is accepted as a self-documenting synonym for "always inline". Today it has no effect over the default, but it stays binding if a future heuristic ever auto-promotes a definition to a module.

partial def Sparkle.Compiler.Elab.translateExprToWireApp (e : Lean.Expr) (hint : String) (isNamed : Bool := false) : CompilerM String

partial def Sparkle.Compiler.Elab.translateShiftAmount (bvExpr natExpr : Lean.Expr) (hint : String) : CompilerM String

Translate a Nat shift amount argument to a hardware wire. Unwraps BitVec.toNat / Fin.val if the Nat came from a BitVec signal, otherwise treats it as a constant shift amount.

partial def Sparkle.Compiler.Elab.getPrimitiveNameFromLambda (e : Lean.Expr) : CompilerM Lean.Name

partial def Sparkle.Compiler.Elab.splitReturnLeaves (e : Lean.Expr) (prefix? : Option String := none) : Lean.MetaM (Array (String × Lean.Expr))

Split a return value of type ρ into a list of (suggested-port-name, leaf-Lean-expr) pairs at the Lean-expression level — one entry per Signal dom τ leaf under ρ.

Handled shapes:

• Signal dom τ → one anonymous leaf carrying the original expression.
• Prod α β → recursively split Prod.fst e / Prod.snd e (positional names out_0, out_1, …).
• single-constructor inductive (i.e. user record) → for each field, recurse on e.field and prefix the field name so each leaf gets a human-readable port (dmac, payloadValid, …).

Falls back to [(none, e)] if the type doesn't match any of the above — that keeps non-Signal payloads round- tripping through the legacy single-wire path.

def Sparkle.Compiler.Elab.openRecordInputs (body : Lean.Expr) : Lean.MetaM Lean.Expr

"Open" record-typed parameters at the synth boundary.

For a function body = fun (p₁ : T₁) (rec : MyRec) (p₂) => … where MyRec is a single-constructor inductive whose fields are all Signal …, rewrite to fun (p₁) (f₁ : F₁) (f₂ : F₂) … (p₂) => body p₁ { f₁, f₂, … } p₂ so the IR elaborator sees per-field Signal inputs instead of an unsplittable record argument.

Records with no Signal fields (or with non-Signal mixed in) are left untouched. Recursion is one-level — a record whose fields are themselves records is partially opened (the outer record is unwrapped; inner records pass through). Good enough for the common HFT-NIC case where each layer's RxIn is a flat record of Signals.

Implementation: walk params with a worker that recurses inside successive forallTelescopeReducing callbacks so every fvar stays in scope when mkLambdaFVars runs at the deepest layer. No IO.Ref shenanigans — the worker threads state purely.

Equations

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

partial def Sparkle.Compiler.Elab.openRecordInputs.walk (body : Lean.Expr) (params : Array Lean.Expr) (inner : Lean.Expr) (idx : Nat) (binders : Array Lean.Expr) (subst : Array (Lean.FVarId × Lean.Expr)) (opened : Bool) : Lean.MetaM Lean.Expr

partial def Sparkle.Compiler.Elab.stripMemoizeWrappers (e : Lean.Expr) : Lean.Expr

Deep-strip every Signal.memoize x sub-expression to x in a Lean expression tree. Signal.memoize is a sim-only identity wrapper used by Compiler C2 to cache per-cycle register reads; for synthesis it serves no purpose and causes infinite-loop hangs in FSM-shaped circuits where register-read → register-write → memoize chain re-enters via Signal.loop body inlining. Stripping them once at the synth entry point breaks the cycle definitively.

Implementation: post-order traversal — strip children first, then check if THIS node is Signal.memoize and unwrap if so. Does not recurse under binders (lambdas) because BVars under a binder have no fvar-binding yet and the memoize wrap there will be handled by Signal.loop's handler when it instantiates the binder.

partial def Sparkle.Compiler.Elab.synthesizeCombinational (declName : Lean.Name) : Lean.MetaM (IR.AST.Module × IR.AST.Design)

partial def Sparkle.Compiler.Elab.synthesizeCombinational.buildEnv (xs : Array Lean.Expr) (i : Nat) (k : CompilerM String) : CompilerM String

def Sparkle.Compiler.Elab.printModule (m : IR.AST.Module) : Lean.MetaM Unit

Equations

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

def Sparkle.Compiler.Elab.«command#synthesize_» : Lean.ParserDescr

Equations

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

def Sparkle.Compiler.Elab.runDesignDRC (design : IR.AST.Design) : Lean.MetaM Unit

Equations

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

def Sparkle.Compiler.Elab.«command#synthesizeVerilog_» : Lean.ParserDescr

Plain-text Verilog elaborator.

#synthesizeVerilog id synthesises id and prints the resulting SystemVerilog to stdout. Output is plain text — no MIME wrapper, no highlighting — so it works identically under lake build, lake env lean, CI, and any Jupyter kernel.

For a syntax-highlighted view inside JupyterLab use #showVerilog instead; for writing to a file use #writeVerilogDesign id "path".

Equations

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

def Sparkle.Compiler.Elab.«command#showVerilog_» : Lean.ParserDescr

Highlighted Verilog viewer for JupyterLab.

#showVerilog id synthesises id and renders the SystemVerilog output inside an HTML <pre><code class="language-verilog"> block, routed through xeus-lean's text/html MIME channel so JupyterLab's bundled highlight.js paints the source.

Outside Jupyter (plain lake env lean, CI) the MIME marker bytes are still emitted but ESC / RS aren't visible, so the listing reads as the raw HTML. In that case prefer #synthesizeVerilog for a clean text dump or #writeVerilogDesign to land the SV on disk.

Equations

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

def Sparkle.Compiler.Elab.synthesizeHierarchical (declName : Lean.Name) : Lean.MetaM IR.AST.Design

Equations

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

def Sparkle.Compiler.Elab.«command#synthesizeDesign_» : Lean.ParserDescr

Equations

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

def Sparkle.Compiler.Elab.«command#synthesizeVerilogDesign_» : Lean.ParserDescr

Equations

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

def Sparkle.Compiler.Elab.«command#writeVerilogDesign__» : Lean.ParserDescr

Equations

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

def Sparkle.Compiler.Elab.«command#writeCppSimDesign__» : Lean.ParserDescr

Equations

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

def Sparkle.Compiler.Elab.«command#writeDesign___» : Lean.ParserDescr

Combined command: synthesize once, emit both Verilog and optimized C++ simulation

Equations

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

def Sparkle.Compiler.Elab.«command#writeDesign____» : Lean.ParserDescr

Combined command with observable wires: emit both Verilog and optimized C++ simulation, with JIT code restricted to only the specified observable wires

Equations

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

def Sparkle.Compiler.Elab.«command#sim_» : Lean.ParserDescr

#sim — Generate typed JIT simulator from a Signal DSL definition.

Usage: def counter : Signal Domain (BitVec 8) := ... #sim counter

Generates: counter.Sim.SimInput, SimOutput, Simulator, load, jitCppPath

Equations

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