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
- Square: MLIR.EDSL.Bracket
- Round: MLIR.EDSL.Bracket
- Curly: MLIR.EDSL.Bracket
- Angle: MLIR.EDSL.Bracket
Instances For
Equations
- MLIR.EDSL.instInhabitedBracket = { default := MLIR.EDSL.Bracket.Square }
Equations
- MLIR.EDSL.instDecidableEqBracket x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
Instances For
Equations
Instances For
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 '<'"
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- MLIR.EDSL.mlir_int_ = Lean.ParserDescr.node `MLIR.EDSL.mlir_int_ 1022 (Lean.ParserDescr.parser `Lean.Parser.numLit)
Instances For
Equations
- MLIR.EDSL.IntToString i = i.repr
Instances For
Equations
- MLIR.EDSL.instQuoteIntMkStr1_sSA = Lean.Quote.mk `term fun (n : ℤ) => { raw := (Lean.Syntax.mkNumLit n.repr).raw }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- MLIR.EDSL.affine_expr_ = Lean.ParserDescr.node `MLIR.EDSL.affine_expr_ 1022 (Lean.ParserDescr.const `ident)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- MLIR.EDSL.mlir_type!_ = Lean.ParserDescr.node `MLIR.EDSL.mlir_type!_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "!") (Lean.ParserDescr.const `str))
Instances For
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))
Instances For
Equations
- MLIR.EDSL.mlir_type_ = Lean.ParserDescr.node `MLIR.EDSL.mlir_type_ 1022 (Lean.ParserDescr.const `ident)
Instances For
Equations
- MLIR.EDSL.mlir_type__1 = Lean.ParserDescr.node `MLIR.EDSL.mlir_type__1 1024 (Lean.ParserDescr.symbol "_")
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- MLIR.EDSL.mlir_typeTensor1d = Lean.ParserDescr.node `MLIR.EDSL.mlir_typeTensor1d 1024 (Lean.ParserDescr.symbol "tensor1d")
Instances For
Equations
- MLIR.EDSL.mlir_typeTensor2d = Lean.ParserDescr.node `MLIR.EDSL.mlir_typeTensor2d 1024 (Lean.ParserDescr.symbol "tensor2d")
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- MLIR.EDSL.mlir_ops_ = Lean.ParserDescr.node `MLIR.EDSL.mlir_ops_ 1022 (Lean.ParserDescr.unary `many (Lean.ParserDescr.cat `mlir_op 0))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
- MLIR.EDSL.dialect_attribute_contents_ = Lean.ParserDescr.node `MLIR.EDSL.dialect_attribute_contents_ 1022 (Lean.ParserDescr.cat `mlir_attr_val 0)
Instances For
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
neg_num
is a possibly negated numeric literal
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- MLIR.EDSL.mlir_attr_val_ = Lean.ParserDescr.node `MLIR.EDSL.mlir_attr_val_ 1022 (Lean.ParserDescr.const `str)
Instances For
Equations
- MLIR.EDSL.mlir_attr_val__1 = Lean.ParserDescr.node `MLIR.EDSL.mlir_attr_val__1 1022 (Lean.ParserDescr.cat `mlir_type 0)
Instances For
Equations
- MLIR.EDSL.mlir_attr_val__2 = Lean.ParserDescr.node `MLIR.EDSL.mlir_attr_val__2 1022 (Lean.ParserDescr.cat `affine_map 0)
Instances For
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)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- MLIR.EDSL.mlir_attr_val__4 = Lean.ParserDescr.node `MLIR.EDSL.mlir_attr_val__4 1022 (Lean.ParserDescr.const `ident)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
MLIR ATTRIBUTE #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- MLIR.EDSL.mlir_attr_val__5 = Lean.ParserDescr.node `MLIR.EDSL.mlir_attr_val__5 1022 (Lean.ParserDescr.cat `mlir_attr_dict 0)
Instances For
Equations
- MLIR.EDSL.attr0Str = MLIR.AST.AttrEntry.mk "sym_name" (MLIR.AST.AttrValue.str "add")
Instances For
Equations
- MLIR.EDSL.attr3Unit = MLIR.AST.AttrEntry.mk "sym_name" MLIR.AST.AttrValue.unit
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
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")]
Instances For
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")]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
MLIR OPS WITH REGIONS AND ATTRIBUTES AND BASIC BLOCK ARGS #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
test simple ops (no regions) #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.