feat(printer): declarative assembly-format DSL + custom (pretty) printing

[GZGavinZhao]

Add a TableGen-style declarative assembly-format DSL for printing operations in their custom (pretty) syntax, currently gated behind the --pretty flag.

Currently three examples are given:

• func.return and func.call using the declarative syntax, mirroring the TableGen's declarative syntax.
• func.func uses a dedicated printer hook, mirroring MLIR's hasCustomAssemblyFormat.

Parsing of pretty syntax is added in a follow-up; this PR only changes printing, so the default (generic) output and all existing tests are unaffected.

TBD: document where exactly our format is different from the upstream TableGen syntax. Documented in the header comment of Veir/AssemblyFormat.lean. Almost all of the difference comes from VeIR not having named operands/results for operations. To achieve true 1-1 mapping, we need some form of build-time (ideally run-time as well) map from an operation's field names to index/type.

[github-actions]

VeIR Benchmarks

Details

Benchmark suite	Current: 1c782f7	Previous: edd0716	Ratio
add-fold-worklist/create	1906000 ns (± 95134)	2318000 ns (± 48078)	0.82
add-fold-worklist/rewrite	3557000 ns (± 105537)	4078000 ns (± 34817)	0.87
add-fold-worklist-local/create	1904000 ns (± 25710)	2238000 ns (± 43661)	0.85
add-fold-worklist-local/rewrite	3427000 ns (± 52842)	3833000 ns (± 31118)	0.89
add-zero-worklist/create	1933000 ns (± 92782)	2274000 ns (± 74215)	0.85
add-zero-worklist/rewrite	2415000 ns (± 54953)	2667000 ns (± 40402)	0.91
add-zero-reuse-worklist/create	1567000 ns (± 27083)	1945000 ns (± 88082)	0.81
add-zero-reuse-worklist/rewrite	1933000 ns (± 36325)	2224500 ns (± 22006)	0.87
mul-two-worklist/create	1904000 ns (± 20599)	2194000 ns (± 94499)	0.87
mul-two-worklist/rewrite	5206000 ns (± 56704)	5733000 ns (± 121107)	0.91
add-fold-forwards/create	1904000 ns (± 95889)	2290000 ns (± 64655)	0.83
add-fold-forwards/rewrite	2746500 ns (± 112526)	3055000 ns (± 23864)	0.90
add-zero-forwards/create	1870000 ns (± 19313)	2232000 ns (± 73733)	0.84
add-zero-forwards/rewrite	1720000 ns (± 32207)	2038000 ns (± 47313)	0.84
add-zero-reuse-forwards/create	1648000 ns (± 47262)	1788000 ns (± 29329)	0.92
add-zero-reuse-forwards/rewrite	1519000 ns (± 74292)	1596000 ns (± 23281)	0.95
mul-two-forwards/create	1916500 ns (± 94326)	2215000 ns (± 81864)	0.87
mul-two-forwards/rewrite	3334500 ns (± 137243)	3797000 ns (± 86929)	0.88
add-zero-reuse-first/create	1570000 ns (± 38515)	1887500 ns (± 69700)	0.83
add-zero-reuse-first/rewrite	9000 ns (± 1675)	8000 ns (± 2604)	1.13
add-zero-lots-of-reuse-first/create	1562000 ns (± 71223)	1916000 ns (± 99617)	0.82
add-zero-lots-of-reuse-first/rewrite	783000 ns (± 23713)	840500 ns (± 34761)	0.93

This comment was automatically generated by workflow using github-action-benchmark.

[tobiasgrosser]

Nice. Let's see what @math-fehr says.

[AlexanderViand]

This looks really cool 👍

One (hopefully small) request: could you add an MLIR_ROUNDTRIP-style test that checks that the pretty-printed syntax veir-opt produces matches the real mlir-opt pretty print (i.e., each one can parse what the other prints, and the textual representation stays stable in the process)?

EDIT: Actually, I just tried the mlir->veir direction manually (mlir-opt Test/Func/pretty_syntax.mlir | lake exe veir-opt) and I think in order to make this work you'd also need to add pretty-printing for builtin.module:

<stdin>:1:1: error: operation expected
module {
^

So maybe this is more of a follow-up than something to deal with in this PR

[GZGavinZhao]

As I mentioned in the last meeting, I would prefer having full delcarative ODS/TableGen custom syntax support rather than implementing a large-in-syntax-coverage-but-small-in-usage-coverage subset. With this current subset, most of the custom syntax in MLIR we cannot just copy over; they need to be either rewritten to fit the subset of custom syntax that we support (e.g. func.call implemented here) or straight up un-expressable (e.g. cf.cond_br). I have an idea of how to do this, will submit a draft PR early next week.

[math-fehr]

Wait, so do you mean that you don't think you can iteratively add feature to that particular DSL such that you could cover all of TableGen DSL?
Because I believe that the long term solution is to have a DSL, plus an escape hatch in Lean code. I don't think we want to prevent escape hatches at all.

[GZGavinZhao]

I'll resolve the conflicts and clean it up later today before requesting a review.

[AlexanderViand]

I'll resolve the conflicts and clean it up later today before requesting a review.

@GZGavinZhao Thanks! Do you consider this ready to review now?

[math-fehr]

Do you think you could split this PR further? Currently it introduce both special printing for func.func, and the assembly-format DSL. I think they should both be separate PRs.

Also, I'm wondering if we can make this somehow more separate from the main Printer.lean file. Could you design this so that there is:

1. An entry point outside of the Printer.lean file such that we can register the printing function? For instance just a parameter of Printer.lean that contains a map between operations to printing functions. There might be some difficulties because of partial fixpoints, let's see.
2. Then on top of this build the assembly format DSL, so that it generates the function that can then be passed to the printer.

I think that way we have a solid fundation!

[GZGavinZhao]

Sorry for the delay. This idea sounds good! I'll split out the code so that registering non-generic printing for operations is a separate file. Then, completely hand-written custom printing and assemblyFormat custom printing all go through this non-generic printing code path.

[GZGavinZhao]

Over the weekend I'll rebase this PR on top of #1236.