CodeElaborator

This module provides the elaborator turning MRiscX assembly syntax into Code.

def getInstrExpr (t : Lean.TSyntax `mriscxInstr) : Lean.Elab.TermElabM Lean.Expr

Elaborate a single parsed instruction into the Expr of its Instr value.

Equations

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

def getInstructionExprArr (seq : Lean.TSyntaxArray `mriscxInstr) : Lean.Elab.TermElabM (Array Lean.Expr)

Elaborate an array of parsed instructions into an array of Instr expressions.

Equations

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

def getLabelInstrArr (t : Lean.TSyntax `mriscxLabel) : Lean.Elab.TermElabM (String × Array Lean.Expr)

Create a tuple holding a label and the expressions of its instructions.

Equations

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

def getLabelMapFromSyntax (syn : Lean.TSyntax `mriscxSyntax) : Lean.Elab.TermElabM LabelMap

Build the LabelMap of an assembly block by assigning each label its index.

Equations

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

def getCodeFromSyntax (syn : Lean.TSyntax `mriscxSyntax) : Lean.Elab.TermElabM Lean.Expr

Elaborate a full mriscx ... end block into the Expr of its Code value.

Equations

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

def term__1 : Lean.ParserDescr

Term elaborator turning a mriscx ... end assembly block into its Code value.

Equations

• term__1 = Lean.ParserDescr.node `term__1 1022 (Lean.ParserDescr.cat `mriscxSyntax 0)

def term__2 : Lean.ParserDescr

Term elaborator turning a single bracketed instruction specification ⟪i⟫ into the Expr of its Instr value.

Equations

• term__2 = Lean.ParserDescr.node `term__2 1022 (Lean.ParserDescr.cat `mriscxSpec 0)