DelabCode

This module provides delaborators rendering MRiscX Code back to assembly syntax.

def SyntaxInstrMap : Type

A total map from instruction indices to parsed instruction syntax, used while delaborating a Code value back into surface assembly.

Equations

• SyntaxInstrMap = TMap UInt64 (Lean.TSyntax `mriscxInstr)

@[instance_reducible]

instance instReprSyntaxInstrMap : Repr SyntaxInstrMap

Equations

• instReprSyntaxInstrMap = { reprPrec := instReprSyntaxInstrMap._aux_1 }

@[instance_reducible]

instance instInhabitedSyntaxInstrMap : Inhabited SyntaxInstrMap

Equations

• instInhabitedSyntaxInstrMap = { default := instInhabitedSyntaxInstrMap._aux_1 }

def termToInstr (t : Lean.TSyntax `term) : Lean.PrettyPrinter.UnexpandM (Lean.TSyntax `mriscxInstr)

Unexpand a term-level Instr constructor application back into surface instruction syntax.

Equations

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

def termToInstrMapAux (fuel : Nat) (t : Lean.TSyntax `term) : Lean.PrettyPrinter.UnexpandM SyntaxInstrMap

Fuel-bounded core of termToInstrMap; fuel bounds the syntax-tree recursion.

Equations

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

def termToInstrMap (t : Lean.TSyntax `term) : Lean.PrettyPrinter.UnexpandM SyntaxInstrMap

Reconstruct a SyntaxInstrMap from its term representation t.

Equations

• termToInstrMap t = termToInstrMapAux (termSyntaxSize✝ t.raw) t

def termToLabelMapAux (fuel : Nat) (t : Lean.TSyntax `term) : LabelMap

Fuel-bounded core of termToLabelMap; fuel bounds the syntax-tree recursion.

Equations

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

def termToLabelMap (t : Lean.TSyntax `term) : LabelMap

Reconstruct a LabelMap from its term representation t.

Equations

• termToLabelMap t = termToLabelMapAux (termSyntaxSize✝ t.raw) t

def createLabelInstructionArray (instructionMap : SyntaxInstrMap) (labelMap : LabelMap) : Array (String × Array (Lean.TSyntax `mriscxInstr))

Group the parsed instructions of instructionMap under their labels, producing the per-label instruction arrays used to render an assembly block.

Equations

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

def CodeUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander rendering a Code.mk application as a full mriscx ... end block.

Equations

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