inductive Sparkle.IR.Type.DimExpr : Type

A hardware dimension that is either concrete or depends on retained module parameters. This is deliberately a small, closed language: the compiler must reject Lean computations it cannot preserve instead of evaluating them only at a parameter's default value.

• literal (value : Nat) : DimExpr
• parameter (name : String) : DimExpr
• add (lhs rhs : DimExpr) : DimExpr
• sub (lhs rhs : DimExpr) : DimExpr
• mul (lhs rhs : DimExpr) : DimExpr
• div (lhs rhs : DimExpr) : DimExpr
• mod (lhs rhs : DimExpr) : DimExpr
• pow (base exponent : DimExpr) : DimExpr
• clog2 (value : DimExpr) : DimExpr
• min (lhs rhs : DimExpr) : DimExpr
• max (lhs rhs : DimExpr) : DimExpr

def Sparkle.IR.Type.instReprDimExpr.repr : DimExpr → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Sparkle.IR.Type.instReprDimExpr : Repr DimExpr

Equations

• Sparkle.IR.Type.instReprDimExpr = { reprPrec := Sparkle.IR.Type.instReprDimExpr.repr }

@[implicit_reducible]

instance Sparkle.IR.Type.instBEqDimExpr : BEq DimExpr

Equations

• Sparkle.IR.Type.instBEqDimExpr = { beq := Sparkle.IR.Type.instBEqDimExpr.beq }

def Sparkle.IR.Type.instBEqDimExpr.beq : DimExpr → DimExpr → Bool

Equations

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

@[implicit_reducible]

instance Sparkle.IR.Type.instDecidableEqDimExpr : DecidableEq DimExpr

Equations

• Sparkle.IR.Type.instDecidableEqDimExpr = Sparkle.IR.Type.instDecidableEqDimExpr.decEq

def Sparkle.IR.Type.instDecidableEqDimExpr.decEq (x✝ x✝¹ : DimExpr) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Sparkle.IR.Type.instInhabitedDimExpr : Inhabited DimExpr

Equations

• Sparkle.IR.Type.instInhabitedDimExpr = { default := Sparkle.IR.Type.instInhabitedDimExpr.default }

def Sparkle.IR.Type.DimExpr.isConcrete : DimExpr → Bool

Equations

• (Sparkle.IR.Type.DimExpr.literal value).isConcrete = true
• x✝.isConcrete = false

def Sparkle.IR.Type.DimExpr.toNat? : DimExpr → Option Nat

Equations

• (Sparkle.IR.Type.DimExpr.literal value).toNat? = some value
• x✝.toNat? = none

def Sparkle.IR.Type.DimExpr.mkAdd : DimExpr → DimExpr → DimExpr

Equations

• (Sparkle.IR.Type.DimExpr.literal 0).mkAdd x✝ = x✝
• x✝.mkAdd (Sparkle.IR.Type.DimExpr.literal 0) = x✝
• (Sparkle.IR.Type.DimExpr.literal lhs).mkAdd (Sparkle.IR.Type.DimExpr.literal rhs) = Sparkle.IR.Type.DimExpr.literal (lhs + rhs)
• x✝¹.mkAdd x✝ = x✝¹.add x✝

def Sparkle.IR.Type.DimExpr.mkSub : DimExpr → DimExpr → DimExpr

Equations

• x✝.mkSub (Sparkle.IR.Type.DimExpr.literal 0) = x✝
• (Sparkle.IR.Type.DimExpr.literal lhs).mkSub (Sparkle.IR.Type.DimExpr.literal rhs) = Sparkle.IR.Type.DimExpr.literal (lhs - rhs)
• x✝¹.mkSub x✝ = x✝¹.sub x✝

def Sparkle.IR.Type.DimExpr.mkMul : DimExpr → DimExpr → DimExpr

Equations

• (Sparkle.IR.Type.DimExpr.literal 0).mkMul x✝ = Sparkle.IR.Type.DimExpr.literal 0
• x✝.mkMul (Sparkle.IR.Type.DimExpr.literal 0) = Sparkle.IR.Type.DimExpr.literal 0
• (Sparkle.IR.Type.DimExpr.literal 1).mkMul x✝ = x✝
• x✝.mkMul (Sparkle.IR.Type.DimExpr.literal 1) = x✝
• (Sparkle.IR.Type.DimExpr.literal lhs).mkMul (Sparkle.IR.Type.DimExpr.literal rhs) = Sparkle.IR.Type.DimExpr.literal (lhs * rhs)
• x✝¹.mkMul x✝ = x✝¹.mul x✝

partial def Sparkle.IR.Type.DimExpr.toString : DimExpr → String

@[implicit_reducible]

instance Sparkle.IR.Type.DimExpr.instToString : ToString DimExpr

Equations

• Sparkle.IR.Type.DimExpr.instToString = { toString := Sparkle.IR.Type.DimExpr.toString }

inductive Sparkle.IR.Type.HWType : Type

Hardware Type: The subset of types that can be synthesized to hardware.

• Bit: Single bit (wire)
• BitVector: n-bit vector
• Array: Fixed-size array (for memories/ROMs)

• bit : HWType
• bitVector (width : Nat) : HWType
• bitVectorDim (width : DimExpr) : HWType
• array (size : Nat) (elemType : HWType) : HWType

@[implicit_reducible]

instance Sparkle.IR.Type.instReprHWType : Repr HWType

Equations

• Sparkle.IR.Type.instReprHWType = { reprPrec := Sparkle.IR.Type.instReprHWType.repr }

def Sparkle.IR.Type.instReprHWType.repr : HWType → Nat → Std.Format

Equations

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

def Sparkle.IR.Type.instBEqHWType.beq : HWType → HWType → Bool

Equations

• Sparkle.IR.Type.instBEqHWType.beq Sparkle.IR.Type.HWType.bit Sparkle.IR.Type.HWType.bit = true
• Sparkle.IR.Type.instBEqHWType.beq (Sparkle.IR.Type.HWType.bitVector a) (Sparkle.IR.Type.HWType.bitVector b) = (a == b)
• Sparkle.IR.Type.instBEqHWType.beq (Sparkle.IR.Type.HWType.bitVectorDim a) (Sparkle.IR.Type.HWType.bitVectorDim b) = (a == b)
• Sparkle.IR.Type.instBEqHWType.beq (Sparkle.IR.Type.HWType.array a a_1) (Sparkle.IR.Type.HWType.array b b_1) = (a == b && Sparkle.IR.Type.instBEqHWType.beq a_1 b_1)
• Sparkle.IR.Type.instBEqHWType.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Sparkle.IR.Type.instBEqHWType : BEq HWType

Equations

• Sparkle.IR.Type.instBEqHWType = { beq := Sparkle.IR.Type.instBEqHWType.beq }

def Sparkle.IR.Type.instDecidableEqHWType.decEq (x✝ x✝¹ : HWType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.IR.Type.instDecidableEqHWType.decEq Sparkle.IR.Type.HWType.bit Sparkle.IR.Type.HWType.bit = isTrue ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq Sparkle.IR.Type.HWType.bit (Sparkle.IR.Type.HWType.bitVector width) = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq Sparkle.IR.Type.HWType.bit (Sparkle.IR.Type.HWType.bitVectorDim width) = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq Sparkle.IR.Type.HWType.bit (Sparkle.IR.Type.HWType.array size elemType) = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.bitVector width) Sparkle.IR.Type.HWType.bit = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.bitVector a) (Sparkle.IR.Type.HWType.bitVector b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.bitVector width) (Sparkle.IR.Type.HWType.bitVectorDim width_1) = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.bitVector width) (Sparkle.IR.Type.HWType.array size elemType) = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.bitVectorDim width) Sparkle.IR.Type.HWType.bit = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.bitVectorDim width) (Sparkle.IR.Type.HWType.bitVector width_1) = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.bitVectorDim a) (Sparkle.IR.Type.HWType.bitVectorDim b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.bitVectorDim width) (Sparkle.IR.Type.HWType.array size elemType) = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.array size elemType) Sparkle.IR.Type.HWType.bit = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.array size elemType) (Sparkle.IR.Type.HWType.bitVector width) = isFalse ⋯
• Sparkle.IR.Type.instDecidableEqHWType.decEq (Sparkle.IR.Type.HWType.array size elemType) (Sparkle.IR.Type.HWType.bitVectorDim width) = isFalse ⋯

@[implicit_reducible]

instance Sparkle.IR.Type.instDecidableEqHWType : DecidableEq HWType

Equations

• Sparkle.IR.Type.instDecidableEqHWType = Sparkle.IR.Type.instDecidableEqHWType.decEq

@[implicit_reducible]

instance Sparkle.IR.Type.instInhabitedHWType : Inhabited HWType

Equations

• Sparkle.IR.Type.instInhabitedHWType = { default := Sparkle.IR.Type.instInhabitedHWType.default }

def Sparkle.IR.Type.HWType.bitWidth : HWType → Nat

Get the bit width of a hardware type

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.IR.Type.HWType.bit.bitWidth = 1
• (Sparkle.IR.Type.HWType.bitVector w).bitWidth = w
• (Sparkle.IR.Type.HWType.bitVectorDim (Sparkle.IR.Type.DimExpr.literal w)).bitWidth = w
• (Sparkle.IR.Type.HWType.array size elemType).bitWidth = size * elemType.bitWidth

def Sparkle.IR.Type.HWType.bitWidth? : HWType → Option Nat

Checked concrete width for consumers that do not support retained dimensions.

Equations

• Sparkle.IR.Type.HWType.bit.bitWidth? = some 1
• (Sparkle.IR.Type.HWType.bitVector w).bitWidth? = some w
• (Sparkle.IR.Type.HWType.bitVectorDim (Sparkle.IR.Type.DimExpr.literal w)).bitWidth? = some w
• (Sparkle.IR.Type.HWType.bitVectorDim width).bitWidth? = none
• (Sparkle.IR.Type.HWType.array size elemType).bitWidth? = Option.map (fun (x : Nat) => size * x) elemType.bitWidth?

def Sparkle.IR.Type.HWType.bitWidthDim : HWType → DimExpr

Return the packed width without discarding symbolic dimensions.

Equations

• Sparkle.IR.Type.HWType.bit.bitWidthDim = Sparkle.IR.Type.DimExpr.literal 1
• (Sparkle.IR.Type.HWType.bitVector a).bitWidthDim = Sparkle.IR.Type.DimExpr.literal a
• (Sparkle.IR.Type.HWType.bitVectorDim a).bitWidthDim = a
• (Sparkle.IR.Type.HWType.array a a_1).bitWidthDim = (Sparkle.IR.Type.DimExpr.literal a).mkMul a_1.bitWidthDim

def Sparkle.IR.Type.HWType.isBit : HWType → Bool

Check if a hardware type is a single bit

Equations

• Sparkle.IR.Type.HWType.bit.isBit = true
• x✝.isBit = false

def Sparkle.IR.Type.HWType.isBitVector : HWType → Bool

Check if a hardware type is a bit vector

Equations

• (Sparkle.IR.Type.HWType.bitVector width).isBitVector = true
• (Sparkle.IR.Type.HWType.bitVectorDim width).isBitVector = true
• x✝.isBitVector = false

def Sparkle.IR.Type.HWType.isArray : HWType → Bool

Check if a hardware type is an array

Equations

• (Sparkle.IR.Type.HWType.array size elemType).isArray = true
• x✝.isArray = false

def Sparkle.IR.Type.HWType.toString : HWType → String

Convert hardware type to a human-readable string

Equations

• Sparkle.IR.Type.HWType.bit.toString = "Bit"
• (Sparkle.IR.Type.HWType.bitVector 1).toString = "Bit"
• (Sparkle.IR.Type.HWType.bitVector w).toString = toString "BitVec" ++ toString w
• (Sparkle.IR.Type.HWType.bitVectorDim width).toString = toString "BitVec(" ++ toString width ++ toString ")"
• (Sparkle.IR.Type.HWType.array size elemType).toString = toString "Array[" ++ toString size ++ toString "](" ++ toString elemType.toString ++ toString ")"

@[implicit_reducible]

instance Sparkle.IR.Type.HWType.instToString : ToString HWType

Equations

• Sparkle.IR.Type.HWType.instToString = { toString := Sparkle.IR.Type.HWType.toString }

def Sparkle.IR.Type.toHWType (α : Type u) (n : Nat) [Data.BitPack.BitPack α n] : HWType

Convert a Lean type with BitPack instance to HWType

Equations

• Sparkle.IR.Type.toHWType α n = if (n == 1) = true then Sparkle.IR.Type.HWType.bit else Sparkle.IR.Type.HWType.bitVector n

def Sparkle.IR.Type.hwTypeFromWidth (w : Nat) : HWType

Helper to infer HWType from a Nat width

Equations

• Sparkle.IR.Type.hwTypeFromWidth w = if (w == 1) = true then Sparkle.IR.Type.HWType.bit else Sparkle.IR.Type.HWType.bitVector w

def Sparkle.IR.Type.hwTypeFromDim (width : DimExpr) : HWType

Construct a packed hardware type while preserving a symbolic dimension.

Equations

• Sparkle.IR.Type.hwTypeFromDim (Sparkle.IR.Type.DimExpr.literal value) = Sparkle.IR.Type.hwTypeFromWidth value
• Sparkle.IR.Type.hwTypeFromDim width = Sparkle.IR.Type.HWType.bitVectorDim width

def Sparkle.IR.Type.byte : HWType

8-bit hardware type

Equations

• Sparkle.IR.Type.byte = Sparkle.IR.Type.HWType.bitVector 8

def Sparkle.IR.Type.word16 : HWType

16-bit hardware type

Equations

• Sparkle.IR.Type.word16 = Sparkle.IR.Type.HWType.bitVector 16

def Sparkle.IR.Type.word32 : HWType

32-bit hardware type

Equations

• Sparkle.IR.Type.word32 = Sparkle.IR.Type.HWType.bitVector 32

def Sparkle.IR.Type.word64 : HWType

64-bit hardware type

Equations

• Sparkle.IR.Type.word64 = Sparkle.IR.Type.HWType.bitVector 64

def Sparkle.IR.Type.hwBool : HWType

Boolean hardware type

Equations

• Sparkle.IR.Type.hwBool = Sparkle.IR.Type.HWType.bit

inductive Sparkle.IR.Type.ResetKind : Type

Reset kind: synchronous or asynchronous.

Lives here (not in Sparkle.Core.Domain) so the IR layer can reference it without importing Core/Domain.lean (which would create a layering inversion). Sparkle.Core.Domain re-exports this so user code keeps seeing Sparkle.Core.Domain.ResetKind.

• synchronous : ResetKind
• asynchronous : ResetKind

def Sparkle.IR.Type.instReprResetKind.repr : ResetKind → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Sparkle.IR.Type.instReprResetKind : Repr ResetKind

Equations

• Sparkle.IR.Type.instReprResetKind = { reprPrec := Sparkle.IR.Type.instReprResetKind.repr }

@[implicit_reducible]

instance Sparkle.IR.Type.instBEqResetKind : BEq ResetKind

Equations

• Sparkle.IR.Type.instBEqResetKind = { beq := Sparkle.IR.Type.instBEqResetKind.beq }

def Sparkle.IR.Type.instBEqResetKind.beq : ResetKind → ResetKind → Bool

Equations

• Sparkle.IR.Type.instBEqResetKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Sparkle.IR.Type.instDecidableEqResetKind : DecidableEq ResetKind

Equations

• Sparkle.IR.Type.instDecidableEqResetKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Sparkle.IR.Type.instInhabitedResetKind : Inhabited ResetKind

Equations

• Sparkle.IR.Type.instInhabitedResetKind = { default := Sparkle.IR.Type.instInhabitedResetKind.default }