Node and edge kinds

inductive Sparkle.Display.Diagram.NodeKind : Type

The visual class of a diagram node.

Each variant gets its own SVG art in renderNode below — a rectangle for a register, a trapezoid for a mux, a gate body for combinational primitives, etc. Use gen for anything you don't have a dedicated shape for; it falls back to a plain box with the node's label.

• reg : NodeKind
• mux : NodeKind
• port : NodeKind
• const : NodeKind
• clk : NodeKind
• adder : NodeKind
• andG : NodeKind
• orG : NodeKind
• notG : NodeKind
• cloud : NodeKind
• gen : NodeKind

def Sparkle.Display.Diagram.instReprNodeKind.repr : NodeKind → Nat → Std.Format

Equations

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

instance Sparkle.Display.Diagram.instReprNodeKind : Repr NodeKind

Equations

• Sparkle.Display.Diagram.instReprNodeKind = { reprPrec := Sparkle.Display.Diagram.instReprNodeKind.repr }

instance Sparkle.Display.Diagram.instInhabitedNodeKind : Inhabited NodeKind

Equations

• Sparkle.Display.Diagram.instInhabitedNodeKind = { default := Sparkle.Display.Diagram.instInhabitedNodeKind.default }

def Sparkle.Display.Diagram.instInhabitedNodeKind.default : NodeKind

Equations

• Sparkle.Display.Diagram.instInhabitedNodeKind.default = Sparkle.Display.Diagram.NodeKind.reg

def Sparkle.Display.Diagram.instBEqNodeKind.beq : NodeKind → NodeKind → Bool

Equations

• Sparkle.Display.Diagram.instBEqNodeKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Sparkle.Display.Diagram.instBEqNodeKind : BEq NodeKind

Equations

• Sparkle.Display.Diagram.instBEqNodeKind = { beq := Sparkle.Display.Diagram.instBEqNodeKind.beq }

inductive Sparkle.Display.Diagram.EdgeKind : Type

The visual class of an edge.

data is the default — a thin arrow. clock is dashed and terminates in a small triangle at the destination's clock pin. bus n carries an n-bit width label and is drawn thicker.

• data : EdgeKind
• clock : EdgeKind
• bus (width : Nat) : EdgeKind

def Sparkle.Display.Diagram.instReprEdgeKind.repr : EdgeKind → Nat → Std.Format

Equations

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

instance Sparkle.Display.Diagram.instReprEdgeKind : Repr EdgeKind

Equations

• Sparkle.Display.Diagram.instReprEdgeKind = { reprPrec := Sparkle.Display.Diagram.instReprEdgeKind.repr }

instance Sparkle.Display.Diagram.instInhabitedEdgeKind : Inhabited EdgeKind

Equations

• Sparkle.Display.Diagram.instInhabitedEdgeKind = { default := Sparkle.Display.Diagram.instInhabitedEdgeKind.default }

def Sparkle.Display.Diagram.instInhabitedEdgeKind.default : EdgeKind

Equations

• Sparkle.Display.Diagram.instInhabitedEdgeKind.default = Sparkle.Display.Diagram.EdgeKind.data

def Sparkle.Display.Diagram.instBEqEdgeKind.beq : EdgeKind → EdgeKind → Bool

Equations

• Sparkle.Display.Diagram.instBEqEdgeKind.beq Sparkle.Display.Diagram.EdgeKind.data Sparkle.Display.Diagram.EdgeKind.data = true
• Sparkle.Display.Diagram.instBEqEdgeKind.beq Sparkle.Display.Diagram.EdgeKind.clock Sparkle.Display.Diagram.EdgeKind.clock = true
• Sparkle.Display.Diagram.instBEqEdgeKind.beq (Sparkle.Display.Diagram.EdgeKind.bus a) (Sparkle.Display.Diagram.EdgeKind.bus b) = (a == b)
• Sparkle.Display.Diagram.instBEqEdgeKind.beq x✝¹ x✝ = false

instance Sparkle.Display.Diagram.instBEqEdgeKind : BEq EdgeKind

Equations

• Sparkle.Display.Diagram.instBEqEdgeKind = { beq := Sparkle.Display.Diagram.instBEqEdgeKind.beq }

Structures

structure Sparkle.Display.Diagram.DiagNode : Type

One block in the diagram.

inputs lets a multi-input node (e.g. a 4:1 mux) declare how many distinct input pins it has on the left; edges can target a specific pin via dst := "muxId.<index>".

• id : String
• label : String
• kind : NodeKind
• col : Nat
• row : Nat
• inputs : Nat

instance Sparkle.Display.Diagram.instInhabitedDiagNode : Inhabited DiagNode

Equations

• Sparkle.Display.Diagram.instInhabitedDiagNode = { default := Sparkle.Display.Diagram.instInhabitedDiagNode.default }

def Sparkle.Display.Diagram.instInhabitedDiagNode.default : DiagNode

Equations

• Sparkle.Display.Diagram.instInhabitedDiagNode.default = { id := default, label := default, kind := default, col := default, row := default, inputs := default }

structure Sparkle.Display.Diagram.DiagEdge : Type

One wire in the diagram. dst is nodeId for a single-input node, or nodeId.k to target the k-th input pin of a multi-input node.

• src : String
• dst : String
• kind : EdgeKind

def Sparkle.Display.Diagram.instInhabitedDiagEdge.default : DiagEdge

Equations

• Sparkle.Display.Diagram.instInhabitedDiagEdge.default = { src := default, dst := default, kind := default }

instance Sparkle.Display.Diagram.instInhabitedDiagEdge : Inhabited DiagEdge

Equations

• Sparkle.Display.Diagram.instInhabitedDiagEdge = { default := Sparkle.Display.Diagram.instInhabitedDiagEdge.default }

structure Sparkle.Display.Diagram.Diagram : Type

A complete diagram. blockDiagram (below) renders it.

• nodes : List DiagNode
• edges : List DiagEdge

instance Sparkle.Display.Diagram.instInhabitedDiagram : Inhabited Diagram

Equations

• Sparkle.Display.Diagram.instInhabitedDiagram = { default := Sparkle.Display.Diagram.instInhabitedDiagram.default }

def Sparkle.Display.Diagram.instInhabitedDiagram.default : Diagram

Equations

• Sparkle.Display.Diagram.instInhabitedDiagram.default = { nodes := default, edges := default }

SVG rendering

def Sparkle.Display.Diagram.toSvg (d : Diagram) : String

Render a Diagram as a single SVG document.

Edges first (so node bodies overlay them), then nodes. Multi-input destinations distribute their incoming edges across the node's left side.

Equations

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

def Sparkle.Display.Diagram.blockDiagram (d : Diagram) : IO Unit

Render a Diagram and emit it to the current cell as an image/svg+xml payload. text/html (an <img> wrapping the SVG) is also acceptable but plain SVG keeps the output smaller and lets JupyterLab's vector-zoom handle scaling.

Equations

• Sparkle.Display.Diagram.blockDiagram d = Sparkle.Display.Mime.svg (Sparkle.Display.Diagram.toSvg d)

IR → Diagram

Walk a Sparkle IR.AST.Module and synthesise a Diagram automatically. Each statement becomes one node; each Expr.ref inside a statement's RHS becomes one edge.

Layout: ports go in column 0 (inputs) and the rightmost column (outputs); registers and combinational gates fan out across the middle columns roughly in topological order. This isn't a real placer — the goal is "good enough to read at a glance", not to match a manually-authored figure.

def Sparkle.Display.Diagram.fromModule (m : IR.AST.Module) : Diagram

Build a Diagram from a Sparkle IR module.

Strategy: each input port is a port node in column 0; each statement gets a node in some intermediate column based on its index in the body; each output port is a port node in the final column. Edges follow Expr.ref dependencies.

Equations

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