[Merged by Bors] - feat: notation3 delaborator generation

[kmill]

Gives the notation3 command the ability to generate a delaborator in most common situations. When it succeeds, notation3-defined syntax is pretty printable.

Examples:

(⋃ (i : ι) (i' : ι'), s i i') = ⋃ (i' : ι') (i : ι), s i i'
(⨆ (g : α → ℝ≥0∞) (_ : Measurable g) (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ) = ∫⁻ (a : α), f a ∂μ

---

[kmill]

@digama0 It's still in CI, but in my local testing it seems to work. It's an extension to the notation3 command to generate a delaborator, and the output is comparable to what we used to have in Lean 3.

I'm trying to add some usability improvement to mathlib in time for the Lean workshop at MSRI that starts next week, so it would be helpful having an expedited review, though worst case we could use a custom branch of mathlib for TPIL.

[kmill]

Just to explain: the Syntax needs to get turned into an Expr pattern for use in the delaborator, and pattern construction needs to be able to walk along the syntax without elaborating it. The walker only handles just enough Syntax features to be useful, and that does not include ↑ or dot notation.

This is not necessary for the syntax to work, but this change causes notation3 to generate a delaborator. set_option trace.notation3 true gives some information about its successes and failures.

[digama0]

It looks like the syntax here could be reconstructed from the elaborated expression though, although maybe you can't even elaborate this expression in context?

[kmill]

I'd thought about trying to elaborate the expressions to generate patterns, but then I wasn't sure if there'd be other things that would introduce into the expressions that'd get in the way of being a pattern, like maybe the elaborator might fill in some instance arguments with instances it wouldn't choose for some concrete arguments. With this syntax walker, I felt more confidant that it's doing the right thing in the cases it accepts.

The code's set up where you can swap out mkExprMatcher for a fancier implementation

[digama0]

What fraction of existing notation3's are delaborated successfully? I think it would be better to have an explicit indication of whether the delaborator is constructed or not, e.g. by a warning that users have to suppress by some additional syntax (like lean 3 @[parsing_only], which maybe we would spell (parsing_only := true) now).

[kmill]

In principle there should only be three that don't work right now. ∀ᵐ and ∃ᵐ use <| in a superficial way, and it's easily fixed either in the declarations or more generally by macro expanding syntax before generating patterns.

The notation for Lex in Mathlib.Data.Pi.Lex seems trickier to support, and maybe that one deserves (parsing_only := true).

I'll take a look at them all tomorrow more carefully once I have a compiled mathlib.

[kmill]

@digama0 I added a (prettyPrint := false) option to notation3. It's running through CI, but as far as I understand only one notation3 needed it, and everything else delaborates.

[kmill]

@digama0 It builds, and I did a spot check for each notation to see that they delaborate, especially the Lesbegue integral notation (no need for its unexpanders now).

[digama0]

As I discussed with @kmill privately, I have a rewrite of large parts of this code to move more of the matcher algorithm to compile time. But this implementation sets bar for the intended behavior of the delaborator, and I have no complaints about the code itself. So let's get this in the hands of mathlib users.

bors r+

[ChrisHughes24]

Conflicts

bors r-

[bors]

Canceled.

[digama0]

bors r+

[bors]

👎 Rejected by label

[digama0]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style