Some pretty printing quirks

Stream: lean4

[Damiano Testa]

let(a) is how the pretty-printer interprets let (a): could it be changed?

Similarly for rcases, have and replace. Also, conv-mode · does not pretty-print a space after itself.

[Kyle Miller]

This doesn't seem to be relevant to this topic @Damiano Testa; could you move this somewhere else?

[Notification Bot]

2 messages were moved here from #Machine Learning for Theorem Proving > Code for turning goal state strings into theorem statements by Damiano Testa.

[Damiano Testa]

Here is some code to show what I mean.

import Lean

open Lean Elab Command in
elab "#pp " cmd:command : command => do
  elabCommand cmd
  logInfo cmd

/-- info: example (h : False) : False := by rcases(h) -/
#guard_msgs in
#pp
example (h : False) : False := by
  rcases (h)

structure X where
  A : {_ : Nat} → Nat → Nat

/-- info: example : X where A{a}b := a + b -/
#guard_msgs in
#pp
example : X where
  A {a} b := a + b

/--
info: example : True :=
  have(h) := trivial
  h
-/
#guard_msgs in
#pp
example : True :=
  have (h) := trivial
  h

/--
info: example (h : ∀ a : Nat, a = a) : 0 = 0 := by
  replace(h) := h 0
  exact h
-/
#guard_msgs in
#pp
example (h : ∀ a : Nat, a = a) : 0 = 0 := by
  replace (h) := h 0
  exact h

/--
info: example {c : Bool} : c = c := by
  induction c with
  | true| _ => rfl
-/
#guard_msgs in
#pp
example {c : Bool} : c = c := by
  induction c with
  | true | _ => rfl

/-- info: example : 0 = 0 := by simp! ; -/
#guard_msgs in
#pp
example : 0 = 0 := by
  simp!;

[Damiano Testa]

I'm no longer at a computer, but I think that also double-quoted names pretty print in a weird (and not round tripping) way.

EDIT:

/--
info: `Nat : Lean.Name
---
info: #check `` Nat
-/
#guard_msgs in
#pp
#check ``Nat

[Robin Arnez]

Can't we define doubleQuotedName as "`" >> checkNoWsBefore >> nameLit? I thought that was how it was done already but apparently only for precheckedQuot (which is in a similar situation).

[Robin Arnez]

inductionAlt is also interesting:

syntax inductionAltLHS := withPosition("| " (("@"? ident) <|> hole) (colGt (ident <|> hole))*)
syntax inductionAlt  := ppDedent(ppLine) inductionAltLHS+ (" => " (hole <|> syntheticHole <|> tacticSeq))?

You could write inductionAltLHS (ppSpace inductionAltLHS)* here but that would change the syntax.
Maybe a many1PPSpace would make sense?

[Damiano Testa]

Here is another one that I did not mention before: pretty printing {} for the focusing of tactics adds a space at the end, but not at the beginning.

/--
info: example : True := by
  · {trivial
  }
-/
#guard_msgs in
#pp
example : True := by
  · {trivial}

[Kyle Miller]

lean4#9475 should fix all these.

[Damiano Testa]

Awesome! I even got a namespace out of this! :octopus:

[Damiano Testa]

Here is a possibly new whitespace issue:

import Lean.Elab.Command

open Lean Elab Command in
elab "#show_pp " cmd:command : command => do
  logInfo cmd

-- `grind_pattern A => B,C`  <-- notice the missing space after the `,`
#show_pp grind_pattern A => B, C

[Kyle Miller]

It looks like docs#Lean.Parser.Command.grindPattern uses "," instead of ", ".

You probably could search for all uses of sepBy/sepBy1 and check for that whitespace systematically.

[Damiano Testa]

Indeed!

Looking at the output of the script below, I think that it is the only exception.

import Lean

open Lean in
run_cmd
  let csts := (← getEnv).constants.map₁
  let mut sepBys := #[]
  for (n, ci) in csts do
    if let some val := ci.value? then
      if let some vs := val.find? (#[``Parser.sepBy, ``Parser.sepBy1].contains ·.getAppFnArgs.1) then
        sepBys := sepBys.push m!"* {.ofConstName n}:\n  {vs}"
  logInfo <| m!"\n".joinSep sepBys.toList

[Damiano Testa]

I opened lean4#11686, in case this is a desirable change!