MLIR Syntax Parsing

This file uses Lean's parser extensions to parse generic MLIR syntax into datastructures defined in MLIRSyntax.AST.

Key definitions are the [mlir_op| ...] and [mlir_region| ...] term elaborators

inductive MLIR.EDSL.Bracket : Type

• Square: MLIR.EDSL.Bracket
• Round: MLIR.EDSL.Bracket
• Curly: MLIR.EDSL.Bracket
• Angle: MLIR.EDSL.Bracket

instance MLIR.EDSL.instInhabitedBracket : Inhabited MLIR.EDSL.Bracket

Equations

• MLIR.EDSL.instInhabitedBracket = { default := MLIR.EDSL.Bracket.Square }

instance MLIR.EDSL.instDecidableEqBracket : DecidableEq MLIR.EDSL.Bracket

Equations

• MLIR.EDSL.instDecidableEqBracket x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance MLIR.EDSL.instToStringBracket : ToString MLIR.EDSL.Bracket

Equations

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

def MLIR.EDSL.isOpenBracket (c : Char) : Option MLIR.EDSL.Bracket

Equations

• MLIR.EDSL.isOpenBracket '(' = some MLIR.EDSL.Bracket.Round
• MLIR.EDSL.isOpenBracket '[' = some MLIR.EDSL.Bracket.Square
• MLIR.EDSL.isOpenBracket '{' = some MLIR.EDSL.Bracket.Curly
• MLIR.EDSL.isOpenBracket '<' = some MLIR.EDSL.Bracket.Angle
• MLIR.EDSL.isOpenBracket c = none

def MLIR.EDSL.isCloseBracket (c : Char) : Option MLIR.EDSL.Bracket

Equations

• MLIR.EDSL.isCloseBracket ')' = some MLIR.EDSL.Bracket.Round
• MLIR.EDSL.isCloseBracket ']' = some MLIR.EDSL.Bracket.Square
• MLIR.EDSL.isCloseBracket '{' = some MLIR.EDSL.Bracket.Curly
• MLIR.EDSL.isCloseBracket '<' = some MLIR.EDSL.Bracket.Angle
• MLIR.EDSL.isCloseBracket c = none

partial def MLIR.EDSL.consumeCloseBracket (c : MLIR.EDSL.Bracket) (startPos : String.Pos) (i : String.Pos) (input : String) (brackets : List MLIR.EDSL.Bracket) (ctx : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

partial def MLIR.EDSL.balancedBracketsFnAux (startPos : String.Pos) (i : String.Pos) (input : String) (bs : List MLIR.EDSL.Bracket) (ctx : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

def MLIR.EDSL.balancedBracketsFnEntry (ctx : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

Equations

• MLIR.EDSL.balancedBracketsFnEntry ctx s = if (ctx.input.get s.pos == '<') = true then MLIR.EDSL.balancedBracketsFnAux s.pos s.pos ctx.input [] ctx s else s.mkError "Expected '<'"

@[inline]

def MLIR.EDSL.balancedBrackets : Lean.Parser.Parser

Equations

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

def MLIR.EDSL.MLIR.EDSL.balancedBrackets.formatter : Lean.PrettyPrinter.Formatter

Equations

• MLIR.EDSL.MLIR.EDSL.balancedBrackets.formatter = pure ()

def MLIR.EDSL.MLIR.EDSL.balancedBracketsParenthesizer : Lean.PrettyPrinter.Parenthesizer

Equations

• MLIR.EDSL.MLIR.EDSL.balancedBracketsParenthesizer = pure ()

def MLIR.EDSL.«term[balanced_brackets|_]» : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.mlir_int : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_int = { }

def MLIR.EDSL.mlir_int_ : Lean.ParserDescr

Equations

• MLIR.EDSL.mlir_int_ = Lean.ParserDescr.node `MLIR.EDSL.mlir_int_ 1022 (Lean.ParserDescr.parser `Lean.Parser.numLit)

def MLIR.EDSL.IntToString (i : ℤ) : String

Equations

• MLIR.EDSL.IntToString i = i.repr

instance MLIR.EDSL.instQuoteIntMkStr1_sSA : Lean.Quote ℤ

Equations

• MLIR.EDSL.instQuoteIntMkStr1_sSA = Lean.Quote.mk `term fun (n : ℤ) => { raw := (Lean.Syntax.mkNumLit n.repr).raw }

def MLIR.EDSL.quoteMList (k : List (Lean.TSyntax `term)) (ty : Lean.TSyntax `term) : Lean.MacroM (Lean.TSyntax `term)

Equations

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

def Lean.Parser.Category.affine_expr : Lean.Parser.Category

Equations

• Lean.Parser.Category.affine_expr = { }

def Lean.Parser.Category.affine_tuple : Lean.Parser.Category

Equations

• Lean.Parser.Category.affine_tuple = { }

def Lean.Parser.Category.affine_map : Lean.Parser.Category

Equations

• Lean.Parser.Category.affine_map = { }

def MLIR.EDSL.affine_expr_ : Lean.ParserDescr

Equations

• MLIR.EDSL.affine_expr_ = Lean.ParserDescr.node `MLIR.EDSL.affine_expr_ 1022 (Lean.ParserDescr.const `ident)

def MLIR.EDSL.«affine_tuple(_,)» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«affine_mapAffine_map<_->_>» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«term[affine_expr|_]» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«term[affine_tuple|_]» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«term[affine_map|_]» : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.mlir_bb : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_bb = { }

def Lean.Parser.Category.mlir_region : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_region = { }

def Lean.Parser.Category.mlir_op : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_op = { }

def Lean.Parser.Category.mlir_op_args : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_op_args = { }

def Lean.Parser.Category.mlir_op_successor_args : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_op_successor_args = { }

def Lean.Parser.Category.mlir_op_type : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_op_type = { }

def Lean.Parser.Category.mlir_op_operand : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_op_operand = { }

def Lean.Parser.Category.mlir_ops : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_ops = { }

def Lean.Parser.Category.mlir_type : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_type = { }

def MLIR.EDSL.«mlir_op_operand%_» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«mlir_op_operand%__1» : Lean.ParserDescr

Equations

• MLIR.EDSL.«mlir_op_operand%__1» = Lean.ParserDescr.node `MLIR.EDSL.«mlir_op_operand%__1» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "%") (Lean.ParserDescr.const `ident))

def MLIR.EDSL.«term[mlir_op_operand|_]» : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.mlir_op_successor_arg : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_op_successor_arg = { }

def MLIR.EDSL.«mlir_op_successor_arg^_» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«term[mlir_op_successor_arg|_]» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«term[mlir_type|_]» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.mlir_type!_ : Lean.ParserDescr

Equations

• MLIR.EDSL.mlir_type!_ = Lean.ParserDescr.node `MLIR.EDSL.mlir_type!_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "!") (Lean.ParserDescr.const `str))

def MLIR.EDSL.mlir_type!__1 : Lean.ParserDescr

Equations

• MLIR.EDSL.mlir_type!__1 = Lean.ParserDescr.node `MLIR.EDSL.mlir_type!__1 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "!") (Lean.ParserDescr.const `ident))

def MLIR.EDSL.mlir_type_ : Lean.ParserDescr

Equations

• MLIR.EDSL.mlir_type_ = Lean.ParserDescr.node `MLIR.EDSL.mlir_type_ 1022 (Lean.ParserDescr.const `ident)

def MLIR.EDSL.mlir_type__1 : Lean.ParserDescr

Equations

• MLIR.EDSL.mlir_type__1 = Lean.ParserDescr.node `MLIR.EDSL.mlir_type__1 1024 (Lean.ParserDescr.symbol "_")

def Lean.Parser.Category.static_dim_list : Lean.Parser.Category

Equations

• Lean.Parser.Category.static_dim_list = { }

def MLIR.EDSL.«static_dim_list_××_[» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«term[static_dim_list|_]» : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.vector_dim_list : Lean.Parser.Category

Equations

• Lean.Parser.Category.vector_dim_list = { }

def MLIR.EDSL.«vector_dim_list_×[_]×» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«mlir_typeVector<__>» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.mlir_typeTensor1d : Lean.ParserDescr

Equations

• MLIR.EDSL.mlir_typeTensor1d = Lean.ParserDescr.node `MLIR.EDSL.mlir_typeTensor1d 1024 (Lean.ParserDescr.symbol "tensor1d")

def MLIR.EDSL.mlir_typeTensor2d : Lean.ParserDescr

Equations

• MLIR.EDSL.mlir_typeTensor2d = Lean.ParserDescr.node `MLIR.EDSL.mlir_typeTensor2d 1024 (Lean.ParserDescr.symbol "tensor2d")

def Lean.Parser.Category.mlir_bb_operand : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_bb_operand = { }

def MLIR.EDSL.«mlir_bb_operand_:_» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«term[mlir_bb_operand|_]» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.mlir_ops_ : Lean.ParserDescr

Equations

• MLIR.EDSL.mlir_ops_ = Lean.ParserDescr.node `MLIR.EDSL.mlir_ops_ 1022 (Lean.ParserDescr.unary `many (Lean.ParserDescr.cat `mlir_op 0))

def MLIR.EDSL.«term[mlir_op|_]» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«term[mlir_ops|_]» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.mlir_suffix_id : Lean.ParserDescr

Reference from the MLIR standard https://mlir.llvm.org/docs/LangRef/#identifiers-and-keywords // Identifiers bare-id ::= (letter|[]) (letter|digit|[$.])* bare-id-list ::= bare-id (, bare-id)* value-id ::= % suffix-id alias-name :: = bare-id suffix-id ::= (digit+ | ((letter|id-punct) (letter|id-punct|digit)*))

symbol-ref-id ::= @ (suffix-id | string-literal) (:: symbol-ref-id)? value-id-list ::= value-id (, value-id)*

// Uses of value, e.g. in an operand list to an operation. value-use ::= value-id (# decimal-literal)? value-use-list ::= value-use (, value-use)*

Equations

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

def MLIR.EDSL.«mlir_region{^_(_,):_}» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«term[mlir_region|_]» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.getSuffixId : Lean.TSyntax `MLIR.EDSL.mlir_suffix_id → String

getSuffixId converts the syntax object of a suffix id to a string. A suffix id is a notion from the MLIR standard defined as

suffix-id ::= (digit+ | ((letter|id-punct) (letter|id-punct|digit)*))

See more at https://mlir.llvm.org/docs/LangRef/#identifiers-and-keywords If the suffix id is a number (the left choice), we convert that number to a string If the suffix id is an identifier (the right choice), we convert that identifier to a string

getSuffixId is used in parsing the syntax of MLIR to a Lean AST

Equations

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

def Lean.Parser.Category.mlir_attr_val : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_attr_val = { }

def Lean.Parser.Category.mlir_attr_val_symbol : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_attr_val_symbol = { }

def MLIR.EDSL.«mlir_attr_val_symbol@_» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«mlir_attr_val_symbol@__1» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«mlir_attr_val#_» : Lean.ParserDescr

Equations

• MLIR.EDSL.«mlir_attr_val#_» = Lean.ParserDescr.node `MLIR.EDSL.«mlir_attr_val#_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.const `ident))

def MLIR.EDSL.«mlir_attr_val#__1» : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.dialect_attribute_contents : Lean.Parser.Category

Equations

• Lean.Parser.Category.dialect_attribute_contents = { }

def MLIR.EDSL.dialect_attribute_contents_ : Lean.ParserDescr

Equations

• MLIR.EDSL.dialect_attribute_contents_ = Lean.ParserDescr.node `MLIR.EDSL.dialect_attribute_contents_ 1022 (Lean.ParserDescr.cat `mlir_attr_val 0)

def MLIR.EDSL.«dialect_attribute_contents(_)» : Lean.ParserDescr

Following https://mlir.llvm.org/docs/LangRef/, we define a dialect-attribute, which is a particular case of an mlir-attr-val that is namespaced to a particular dialect

dialect-namespace ::= bare-id

dialect-attribute ::= `#` (opaque-dialect-attribute | pretty-dialect-attribute)
opaque-dialect-attribute ::= dialect-namespace dialect-attribute-body
pretty-dialect-attribute ::= dialect-namespace `.` pretty-dialect-attribute-lead-ident
                                              dialect-attribute-body?
pretty-dialect-attribute-lead-ident ::= `[A-Za-z][A-Za-z0-9._]*`

dialect-attribute-body ::= `<` dialect-attribute-contents+ `>`
dialect-attribute-contents ::= dialect-attribute-body
                            | `(` dialect-attribute-contents+ `)`
                            | `[` dialect-attribute-contents+ `]`
                            | `{` dialect-attribute-contents+ `}`
                            | [^\[<({\]>)}\0]+

Equations

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

def MLIR.EDSL.«dialect_attribute_contents[_]» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«dialect_attribute_contents{_}» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«mlir_attr_val#_<_>» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«mlir_attr_val#opaque<_,_>:_» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«mlir_attr_val_symbol_::_» : Lean.TrailingParserDescr

Equations

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

def Lean.Parser.Category.balanced_parens : Lean.Parser.Category

Equations

• Lean.Parser.Category.balanced_parens = { }

def MLIR.EDSL.neg_num : Lean.ParserDescr

neg_num is a possibly negated numeric literal

Equations

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

def MLIR.EDSL.mlir_attr_val_ : Lean.ParserDescr

Equations

• MLIR.EDSL.mlir_attr_val_ = Lean.ParserDescr.node `MLIR.EDSL.mlir_attr_val_ 1022 (Lean.ParserDescr.const `str)

def MLIR.EDSL.mlir_attr_val__1 : Lean.ParserDescr

Equations

• MLIR.EDSL.mlir_attr_val__1 = Lean.ParserDescr.node `MLIR.EDSL.mlir_attr_val__1 1022 (Lean.ParserDescr.cat `mlir_type 0)

def MLIR.EDSL.mlir_attr_val__2 : Lean.ParserDescr

Equations

• MLIR.EDSL.mlir_attr_val__2 = Lean.ParserDescr.node `MLIR.EDSL.mlir_attr_val__2 1022 (Lean.ParserDescr.cat `affine_map 0)

def MLIR.EDSL.mlir_attr_val__3 : Lean.ParserDescr

Equations

• MLIR.EDSL.mlir_attr_val__3 = Lean.ParserDescr.node `MLIR.EDSL.mlir_attr_val__3 1022 (Lean.ParserDescr.cat `mlir_attr_val_symbol 0)

def MLIR.EDSL.«mlir_attr_val_:_» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«mlir_attr_val_:__1» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.mlir_attr_val__4 : Lean.ParserDescr

Equations

• MLIR.EDSL.mlir_attr_val__4 = Lean.ParserDescr.node `MLIR.EDSL.mlir_attr_val__4 1022 (Lean.ParserDescr.const `ident)

def MLIR.EDSL.«mlir_attr_val[_,]» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«term[mlir_attr_val|_]» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«term[mlir_attr_val_symbol|_]» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.negNumToTerm : Lean.TSyntax `MLIR.EDSL.neg_num → Lean.MacroM Lean.Term

Convert a possibly negated numeral into a term representing the same value

Equations

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

MLIR ATTRIBUTE

def MLIR.EDSL.mlir_attr_key : Lean.ParserDescr

Equations

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

def MLIR.EDSL.mlir_attr_entry : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«term[mlir_attr_entry|_]» : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.mlir_attr_dict : Lean.Parser.Category

Equations

• Lean.Parser.Category.mlir_attr_dict = { }

def MLIR.EDSL.«mlir_attr_dict<{_,}>» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«term[mlir_attr_dict|_]» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.mlir_attr_val__5 : Lean.ParserDescr

Equations

• MLIR.EDSL.mlir_attr_val__5 = Lean.ParserDescr.node `MLIR.EDSL.mlir_attr_val__5 1022 (Lean.ParserDescr.cat `mlir_attr_dict 0)

def MLIR.EDSL.attr0Str : MLIR.AST.AttrEntry 0

Equations

• MLIR.EDSL.attr0Str = MLIR.AST.AttrEntry.mk "sym_name" (MLIR.AST.AttrValue.str "add")

def MLIR.EDSL.attr3Unit : MLIR.AST.AttrEntry 0

Equations

• MLIR.EDSL.attr3Unit = MLIR.AST.AttrEntry.mk "sym_name" MLIR.AST.AttrValue.unit

def MLIR.EDSL.attr4Negative : MLIR.AST.AttrEntry 0

Equations

• MLIR.EDSL.attr4Negative = MLIR.AST.AttrEntry.mk "value" (MLIR.AST.AttrValue.int (-1) (MLIR.AST.MLIRType.int MLIR.AST.Signedness.Signless 32))

def MLIR.EDSL.attrDict0 : MLIR.AST.AttrDict 0

Equations

• MLIR.EDSL.attrDict0 = MLIR.AST.AttrDict.mk []

def MLIR.EDSL.attrDict1 : MLIR.AST.AttrDict 0

Equations

• MLIR.EDSL.attrDict1 = MLIR.AST.AttrDict.mk [MLIR.AST.AttrEntry.mk "foo" (MLIR.AST.AttrValue.str "bar")]

def MLIR.EDSL.attrDict2 : MLIR.AST.AttrDict 0

Equations

• MLIR.EDSL.attrDict2 = MLIR.AST.AttrDict.mk [MLIR.AST.AttrEntry.mk "foo" (MLIR.AST.AttrValue.str "bar"), MLIR.AST.AttrEntry.mk "baz" (MLIR.AST.AttrValue.str "quux")]

def MLIR.EDSL.propDict2 : MLIR.AST.AttrDict 0

Equations

• MLIR.EDSL.propDict2 = MLIR.AST.AttrDict.mk [MLIR.AST.AttrEntry.mk "foo" (MLIR.AST.AttrValue.str "bar"), MLIR.AST.AttrEntry.mk "baz" (MLIR.AST.AttrValue.str "quux")]

def MLIR.EDSL.nestedAttrDict0 : MLIR.AST.AttrDict 0

Equations

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

MLIR OPS WITH REGIONS AND ATTRIBUTES AND BASIC BLOCK ARGS

def MLIR.EDSL.«mlir_op_=_(_)(_)_:(_)->(_)» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«mlir_op_=_(_)(_)_:(_)->_» : Lean.ParserDescr

Equations

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

test simple ops (no regions)

def MLIR.EDSL.«mlir_opFunc_(_)->_{_}» : Lean.ParserDescr

Equations

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

def MLIR.EDSL.«mlir_opModule{_}» : Lean.ParserDescr

Equations

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