Pretty MLIR Syntax

This file buils some common functionality that dialects can use to define pretty syntax. Note that since pretty syntax is just defined as Lean macros, none of this is required.

The category of uniform operation (names). Syntax of this category is expected to be just a single atom, which is seen as the name of a MLIR operation where all inputs and outputs have the same type

def MLIR.EDSL.Pretty.MLIR.Pretty.uniform_op.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.MLIR.Pretty.uniform_op : Lean.Parser.Category

Equations

• Lean.Parser.Category.MLIR.Pretty.uniform_op = { }

def MLIR.EDSL.Pretty.extractOpName : Lean.Syntax → Option (Lean.TSyntax `str)

Given syntax which consists of just a node with a single atom (as expected by uniform_op), extract the name of the operation and return it as a string literal syntax.

Equations

• MLIR.EDSL.Pretty.extractOpName (Lean.Syntax.node info kind { toList := Lean.Syntax.atom info_1 name :: tail }) = some (Lean.Syntax.mkStrLit name)
• MLIR.EDSL.Pretty.extractOpName x = none

If we register foo.bar as a uniform op, then syntax like the following will be parsed

$x = foo.bar $y, $z : $t

The uniformity means only a single mlir type has to be specified, this is expanded to:

$x = "foo.bar"($y, $z) : ($t, $t) -> $t

Where the number of repeated ts is determined by the number of arguments given.

It's also possible to leave out the : $t type annotation entirely, in which case t will be assumed to be _, the "hole" type.

def MLIR.EDSL.Pretty.«mlir_op_=__:_» : Lean.ParserDescr

Equations

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