feat: allow opt-out of grouping in formatter#867
Conversation
|
|
||
| abbrev Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δ := | ||
| fun x => f (g x) | ||
| abbrev Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δ := fun x => f (g x) |
There was a problem hiding this comment.
Ah, that fun but not other terms can now be used in a single line is an interesting consequence... I think we should really introduce ppLineUnlessUngrouped and use it instead of ppHardline... but that doesn't have to be in this PR
| do | ||
| discard (pure 2) | ||
| let y : Nat := 3 | ||
| pure (x + y)) |
There was a problem hiding this comment.
Should we care about this one? Arguably the indent of do was wrong to begin with.
| IO.println x | ||
| IO.println "even" else do | ||
| IO.println x | ||
| IO.println "odd" |
There was a problem hiding this comment.
Okay, I've pushed a changed that puts newlines after then and before/after else (by exposing Format.group as a pretty-printing combinator, which requires a stage0 update).
There's still the structure instance issue, where the formatter produces { a := 42 b:= 1 }. I've tried replacing optional ", " by ", " <|> (ppLine >> group skip). This produces parseable syntax, but formats every structure instance in multi-line format... Ideally we'd define structure instances in terms of sepBy ", " structInstField (", " <|> (checkColGe >> ppLine)) (so that the final ppLine is omitted), but that requires big changes in the structure instance elaborator (with the accompanying bootstrapping problems).
fabbd93 to
586097c
Compare
0dcbb1e to
6a25154
Compare
Currently, the pretty-printer formats tactics proofs like this:
The main goal of this PR is to format theorems as follows (which is important for mathport because we use the formatter to generate the Lean 4 source code):
The reason why the by is indented at the moment is that the formatter for category parsers automatically inserts fill+nest nodes around the produced format object (confusingly, this is called a group in the formatter).
We add a new no-op parser combinator called
ppAllowUngroupedthat instructs the category pretty-printer to omit this fill+nest operation, and add this combinator to by/do/fun. This causes theorems with tactics proofs to be printed in the desired wayThere are also two new pretty-printing combinators which can do different things depending on whether the following parser was ungrouped or not.
ppDedentIfGroupedundos the nest step (but keeps the fill) if the parser is grouped (used in parentheses), andppHardLineUnlessUngroupedprints a hard newline if the parser is grouped, and a soft newline otherwise (used in declarations after:=).I have prepared a branch where all Lean source files have been reformatted with these changes: https://github.com/leanprover/lean4/compare/master...gebner:formatted?diff=split There is of course still lots of low-hanging fruit left (and some more serious bugs).
There are several changes in this PR, I can split it up if desired:
Reformat.leanfile in the tests directory, this also works if the lean file defines notation and hence requires elaboration.pushTokenfunction in the formatter which printed extra spaces, for example two spaces afterhaveand very often trailing spaces ("fix: suppress extra spaces in formatter").ppAllowUngrouped("feat: allow opt-out of grouping in formatter")