Interval integral pretty print

Stream: new members

[Simon Sorg]

If I check the type of an intervalIntegral with

import Mathlib
#check ∫ (x : ℝ) in (0)..1, x

the resulting command yields

∫ (x : ℝ) in 0 ..1, x

If I copy paste that pretty print into the same Lean file, this is invalid syntax. Note that the spaces around the .. have changed, and the parentheses are gone. I'm finding this somewhat odd. Is this intended? Why is the prettyPrint different, and no valid syntax? And to avoid future confusion: where can I find the definition for the prettyPrint? I couldn't find any delaborators, which I thought was what I might need.

Edit: the import of whole mathlib takes quite some time, sorry. Here's a more efficient #mwe

import Mathlib.Data.Real.Basic
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

#check ∫ (x : ℝ) in (0 : ℝ)..1, x

[Jireh Loreaux]

The delaborator comes for free as part of the notation3 command that defines this syntax here

[Kyle Miller]

Possibly, changing ".." to " .. " would make pretty printing round trip.

It's possibly a Lean core bug that this doesn't pretty print with an extra space before the 1. The reason there's a space after 0 is to make sure the . doesn't get parsed as part of 0.. The core pretty printer inserts spaces to break up tokens.

[Simon Sorg]

Thanks! This makes delaboration a lot less magical :)
Still, this leaves me wondering a bit why the core pretty printer inserts the initial space at "0.." (resulting in "0 .."), since this is not valid either.

#check ∫ (x : ℝ) in (0 : ℝ) ..1, x

returns a syntax error.

[Kyle Miller]

Does it work if you put a space before the 1? That would confirm what I was guessing, that this is a core bug.

[Simon Sorg]

#check ∫ (x : ℝ) in (0 : ℝ).. 1, x

is valid syntax, but the resulting pretty print is still the same.

∫ (x : ℝ) in 0 ..1, x : ℝ

[Kyle Miller]

I would not expect it to change how it is pretty printed. The pretty printer remembers nothing about the original input syntax.

[Simon Sorg]

As the different syntax is elaborated into the same Expr, and the delaborator only uses the Expr, right?

[Kyle Miller]

Yes

[Kyle Miller]

The likely problem is that a dot before a number is lexically a floating point literal.

[Kyle Miller]

The pretty printer doesn't have many levers to pull to try to fix lexical errors like this. Inserting whitespace is one of them.

I don't think there's any case of parenthesis insertion (there's no framework for that...) but it would help here.

[Mario Carneiro]

Kyle Miller said:

parenthesis insertion (there's no framework for that...)

Are you familiar with the Parenthesizer?

[Kyle Miller]

I'm sure that you know that I am @Mario Carneiro

As you might recall, the parenthesizer is designed for inserting parentheses where they are syntactically necessary, not lexically necessary.

Or maybe you think this is purely a precedence issue?

[Mario Carneiro]

I think it usually makes most sense to fix lexical errors by inserting whitespace, although vertical alignment is problematic

[Mario Carneiro]

I was just reacting to the claim that there is no framework for parenthesis insertion