Conditionally pretty-printing with spaces

Stream: metaprogramming / tactics

[Robert Maxton]

I'm trying to make a syntax that will pretty pretty spaces between its parameters only if those parameters are not numeric literals. Specifically, I want [O2|C4], but [O n|C3], [O2|C k], and [O n|C m].

I think I need to write a PrettyPrinter.Formatter, but there's no equivalent to app_unexpander or app_delab that I'm aware of, for example, and I don't know how else to set up the trigger. (combinator_formatter termFoo at least typechecks but doesn't actually run, as verified by dbgTrace). I would like to be able to just write something like

macro "[O" (lookahead(num) <|> ppSpace)  a:term "|C" (lookahead(num) <|> ppSpace) b:term "]" : term => ...

but you can't use notation with general syntax and since I don't know any way of putting explicit whitespace into a Syntax object I can't make an unexpander to make the above macro pretty-print the way I want.

[Kyle Miller]

You might run into some trouble here since the formatter is token-aware. It'll insert spaces automatically between O and 2 because O2 parses as an identifier.

How is O2 able to parse? It's generally not a good idea to pretty print in a way that's not parseable.

One hack you can do is use a zero-width space.

[Kyle Miller]

Oh, right, "[O" makes the parsing possible.

[Kyle Miller]

Here's a hack:

import Lean

def f : Nat → Nat := id

macro "[O" n:term "]" : term => `(f $n)

section
local syntax (name := preSpace) ppSpace term : term
end

open Lean.Syntax in
def mkPreSpace (t : Term) : Term := ⟨Lean.Unhygienic.run `(preSpace| $t)⟩

@[app_unexpander f]
def unexpandF : Lean.PrettyPrinter.Unexpander
  | `($_ $n:num) => `([O $n])
  | `($_ $x) => `([O $(mkPreSpace x)])
  | _ => throw ()

#check [O2]
-- [O2]
variable (n : Nat)
#check [O n]
-- [O n]

[Robert Maxton]

So that's how you do it. I was thinking about something like that, but I'd forgotten (if I ever knew) how to set up a term generator outside of a quasiquote. Thanks, that'll work nicely!