AssemblySyntax

This module provides the parser/grammar for MRiscX assembly syntax.

def mriscxLabel.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.mriscxLabel : Category

Syntax category for a labelled block of MRiscX assembly instructions.

Equations

• Lean.Parser.Category.mriscxLabel = { }

def Lean.Parser.Category.mriscxInstr : Category

Syntax category for a single MRiscX assembly instruction.

Equations

• Lean.Parser.Category.mriscxInstr = { }

def mriscxInstr.quot : Lean.ParserDescr

Equations

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

def mriscxSyntax.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.mriscxSyntax : Category

Syntax category for a complete MRiscX assembly program (mriscx ... end).

Equations

• Lean.Parser.Category.mriscxSyntax = { }

def Lean.Parser.Category.mriscxProgram : Category

Syntax category for an MRiscX program body.

Equations

• Lean.Parser.Category.mriscxProgram = { }

def mriscxProgram.quot : Lean.ParserDescr

Equations

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

def mriscxNumOrIdent.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.mriscxNumOrIdent : Category

Syntax category for an MRiscX operand: a numeral or a register/variable identifier.

Equations

• Lean.Parser.Category.mriscxNumOrIdent = { }

def Lean.Parser.Category.hoare : Category

Syntax category for MRiscX Hoare-triple notation.

Equations

• Lean.Parser.Category.hoare = { }

def hoare.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.mriscxSpec : Category

Syntax category for a single-instruction MRiscX specification (⟪i⟫).

Equations

• Lean.Parser.Category.mriscxSpec = { }

def mriscxSpec.quot : Lean.ParserDescr

Equations

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

def mriscxNumOrIdent_ : Lean.ParserDescr

Numeral operand syntax.

Equations

• mriscxNumOrIdent_ = Lean.ParserDescr.node `mriscxNumOrIdent_ 1022 (Lean.ParserDescr.const `num)

def mriscxNumOrIdent__1 : Lean.ParserDescr

Identifier (register/variable) operand syntax.

Equations

• mriscxNumOrIdent__1 = Lean.ParserDescr.node `mriscxNumOrIdent__1 1022 (Lean.ParserDescr.const `ident)

def «mriscxInstrLaX_,___» : Lean.ParserDescr

Concrete syntax for the MRiscX la instruction.

Equations

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

def «mriscxInstrLiX_,___» : Lean.ParserDescr

Concrete syntax for the MRiscX li instruction.

Equations

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

def «mriscxInstrMvX_,X___» : Lean.ParserDescr

Concrete syntax for the MRiscX mv instruction.

Equations

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

def «mriscxInstrAddiX_,X_,___» : Lean.ParserDescr

Concrete syntax for the MRiscX addi instruction.

Equations

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

def mriscxInstrIncX___ : Lean.ParserDescr

Concrete syntax for the MRiscX inc instruction.

Equations

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

def «mriscxInstrAddX_,X_,X___» : Lean.ParserDescr

Concrete syntax for the MRiscX add instruction.

Equations

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

def «mriscxInstrSubiX_,X_,___» : Lean.ParserDescr

Concrete syntax for the MRiscX subi instruction.

Equations

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

def mriscxInstrDecX___ : Lean.ParserDescr

Concrete syntax for the MRiscX dec instruction.

Equations

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

def «mriscxInstrSubX_,X_,X___» : Lean.ParserDescr

Concrete syntax for the MRiscX sub instruction.

Equations

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

def «mriscxInstrXoriX_,X_,___» : Lean.ParserDescr

Concrete syntax for the MRiscX xori instruction.

Equations

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

def «mriscxInstrXorX_,X_,X___» : Lean.ParserDescr

Concrete syntax for the MRiscX xor instruction.

Equations

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

def «mriscxInstrLwX_,___» : Lean.ParserDescr

Concrete syntax for the MRiscX lw instruction.

Equations

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

def «mriscxInstrLwX_,X___» : Lean.ParserDescr

Concrete syntax for the MRiscX lw instruction.

Equations

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

def «mriscxInstrSwX_,X___» : Lean.ParserDescr

Concrete syntax for the MRiscX sw instruction.

Equations

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

def mriscxInstrJ___ : Lean.ParserDescr

Concrete syntax for the MRiscX j instruction.

Equations

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

def «mriscxInstrJ.___» : Lean.ParserDescr

Concrete syntax for the MRiscX j instruction.

Equations

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

def «mriscxInstrBeqX_,X_,___» : Lean.ParserDescr

Concrete syntax for the MRiscX beq instruction.

Equations

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

def «mriscxInstrBeqX_,X_,.___» : Lean.ParserDescr

Concrete syntax for the MRiscX beq instruction.

Equations

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

def «mriscxInstrBneX_,X_,___» : Lean.ParserDescr

Concrete syntax for the MRiscX bne instruction.

Equations

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

def «mriscxInstrBneX_,X_,.___» : Lean.ParserDescr

Concrete syntax for the MRiscX bne instruction.

Equations

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

def «mriscxInstrBgtX_,X_,___» : Lean.ParserDescr

Concrete syntax for the MRiscX bgt instruction.

Equations

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

def «mriscxInstrBgtX_,X_,.___» : Lean.ParserDescr

Concrete syntax for the MRiscX bgt instruction.

Equations

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

def «mriscxInstrBleX_,X_,___» : Lean.ParserDescr

Concrete syntax for the MRiscX ble instruction.

Equations

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

def «mriscxInstrBleX_,X_,.___» : Lean.ParserDescr

Concrete syntax for the MRiscX ble instruction.

Equations

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

def «mriscxInstrBeqzX_,___» : Lean.ParserDescr

Concrete syntax for the MRiscX beqz instruction.

Equations

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

def «mriscxInstrBeqzX_,.___» : Lean.ParserDescr

Concrete syntax for the MRiscX beqz instruction.

Equations

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

def «mriscxInstrBnezX_,___» : Lean.ParserDescr

Concrete syntax for the MRiscX bnez instruction.

Equations

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

def «mriscxInstrBnezX_,.___» : Lean.ParserDescr

Concrete syntax for the MRiscX bnez instruction.

Equations

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

def mriscxInstrPANIC!__ : Lean.ParserDescr

Concrete syntax for the MRiscX PANIC! instruction.

Equations

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

def «mriscxLabel__:_» : Lean.ParserDescr

Concrete syntax for a labelled block name: instr... of instructions.

Equations

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

def «mriscxLabel_._:_» : Lean.ParserDescr

Concrete syntax for a dotted labelled block .name: instr... of instructions.

Equations

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

def mriscxSyntaxBlock : Lean.ParserDescr

A complete MRiscX assembly program: a sequence of labelled instruction blocks delimited by mriscx ... end.

Equations

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

def term_ : Lean.ParserDescr

Inject a parsed mriscx ... end block into the term language.

Equations

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

def «mriscxSpec⟪_⟫» : Lean.ParserDescr

Bracket notation ⟪i⟫ marking a single-instruction specification.

Equations

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