Check if a `Lean.Name` is roundtrippable

Stream: metaprogramming / tactics

[Aaron Liu]

How do I check if a Lean.Name is roundtrippable?

[Aaron Liu]

meaning, if I convert it into a String and parse the result it should give me the same name

[Thomas Murrills]

I'm pretty sure docs#Lean.Name.toString does this anyway, when escape := true (the default)

[Thomas Murrills]

Ah, wait, I see the caveat...

[Aaron Liu]

how am I supposed to interpret the result

-- "example"
#eval Lean.Name.toString `example

(this one doesn't roundtrip because example is a token)

[Thomas Murrills]

Ah, I see...looking into the code it seems like there's an isToken function passed into helper functions which controls escaping of tokens, which is false by default. Presumably this could be changed... :eyes: Do you have control over the stringification, or do you just need to evaluate if toString roundtrips?

[Aaron Liu]

it's whatever Lean.PrettyPrinter.ppCategory does

[Thomas Murrills]

It seems to me ppCategory successfully escapes tokens in names by experiment—I also found docs#Lean.PrettyPrinter.Formatter.identNoAntiquot.formatter, which seems to avoid all tokens via the isToken argument, so maybe that's what's responsible

[Thomas Murrills]

e.g.

import Lean

open Lean Elab Command

/-- info: «example» -/
#guard_msgs in
run_cmd do
  logInfo <|← liftCoreM <| Lean.PrettyPrinter.ppCategory `ident <|
    Syntax.ident .none "".toRawSubstring `example []

[Thomas Murrills]

It of course doesn't know how to handle num components, though...

[Aaron Liu]

yeah so I need to know whether it will roundtrip

[Thomas Murrills]

You could of course just try roundtripping it and seeing if you get a parse error and, if not, if it matches :grinning_face_with_smiling_eyes:

But assuming you want something better, my guess would be that if the name

• has no numeric components
• has no string components which contain « or »
• is not anonymous

it'll roundtrip. Just a hunch, though.

[Thomas Murrills]

Hmm, actually, nevermind; you can stick all sorts of things in a string component that won't parse. We should just look at what can parse as an ident...

[Thomas Murrills]

This might work:

import Lean

open Lean

def Lean.Name.willRoundTrip (n : Name) : Bool :=
  !n.isAnonymous && go n
where
  go : Lean.Name → Bool
  | .str n s => (Name.escapePart s).isSome && go n
  | .num .. => false
  | .anonymous => true

[Thomas Murrills]

It seems like escapePart might be the "right" bit of infrastructure around toString to rip out here...it looooks like it ultimately recreates the important bits of identifier parsing to determine whether escape is possible.

It does do a bit of extra work constructing the escaped string, but every component declaration is private; so if you need every bit of performance you could ofc rip out the internals and just do the checking.

[Aaron Liu]

this is probably good enough

[Aaron Liu]

there is the little edge case where the name _ doesn't work properly since it's expecting a binderIdent

[Aaron Liu]

and also the thing where when I put newlines in my name it inserts an indentation in the middle of the name which fills it with many spaces

[Aaron Liu]

but this is probably good enough

[Thomas Murrills]

Ah, right, because prettyprinting messes with whitespace, on that second point...I wonder if it messes with anything else?

[Thomas Murrills]

Aaron Liu said:

there is the little edge case where the name _ doesn't work properly since it's expecting a binderIdent

Also, hmm, maybe escapePart is generally inappropriate for the first component of the ident

[Thomas Murrills]

Looks like ? and ?_, ?e, etc. are also edge cases...

[Aaron Liu]

maybe I shouldn't implement this checking and just blame the pretty printer instead

[Thomas Murrills]

Okay, it looks like the pretty printer uses this:

def toStringWithToken (n : Name) (escape := true) (isToken : String → Bool) : String :=
  -- never escape "prettified" inaccessible names or macro scopes or pseudo-syntax introduced by the delaborator
  toStringWithSep "." (escape && !n.isInaccessibleUserName && !n.hasMacroScopes && !maybePseudoSyntax) n isToken
where
  maybePseudoSyntax :=
    if n == `_ then
      -- output hole as is
      true
    else if let .str _ s := n.getRoot then
      -- could be pseudo-syntax for loose bvar or universe mvar, output as is
      "#".isPrefixOf s || "?".isPrefixOf s
    else
      false

which means that whenever escape && !n.isInaccessibleUserName && !n.hasMacroScopes && !maybePseudoSyntax is false, we don't escape, even though we "should". Edge case: isInaccessibleUserName is also true for names containing _inaccessible, which actually does not need to be escaped, it seems?

Putting all that together, I thiiiink:

import Lean

open Lean

def Lean.Name.willRoundTrip (n : Name) : Bool :=
  !n.isAnonymous && !n.hasMacroScopes && !maybePseudoSyntax && go n
where
  go : Lean.Name → Bool
    | .str n s =>
      !s.contains (fun c => c == '✝' || c == '\n')
        && (Name.escapePart s).isSome
        && go n
    | .num .. => false
    | .anonymous => true
  maybePseudoSyntax :=
    if n == `_ then
      -- output hole as is
      true
    else if let .str _ s := n.getRoot then
      -- could be pseudo-syntax for loose bvar or universe mvar, output as is
      "#".isPrefixOf s || "?".isPrefixOf s
    else
      false

[Aaron Liu]

now I'm confused

[Thomas Murrills]

What's up? It's possible I did something silly.

[Aaron Liu]

where did all these checks come from

[Aaron Liu]

why are we checking for '✝' and '\n'

[Thomas Murrills]

I'm copying over "exceptions" made by the pretty printer in toStringWithToken (to make sure we don't count them as exceptions); '✝' is a better isInaccessibleUserName, because isInaccessibleUserName goes too far and considers _inaccessible to be inaccessible; '\n' is actually the only one that doesn't come from toStringWithToken, and is meant to handle the newline edge case you described

[Aaron Liu]

ah I see

[Thomas Murrills]

So, for example, while the pretty printer goes ahead and pretty-prints Name.str .anonymous "?u" as ?u (because it satisfies maybePseudoSyntax), we want to identify that therefore this will not round trip via pretty printing

[Aaron Liu]

is (Name.escapePart s).isSome just the same as s.isEmpty || !s.any Lean.isIdEndEscape

[Aaron Liu]

I guess I'll just plug this in

[Thomas Murrills]

No, I think there's also the needsNoEscape condition in escapePart's source, right? Which handles whether it starts correctly (I think, haven't checked)

[Aaron Liu]

I think if the name contains » then needsNoEscape is always false

[Thomas Murrills]

But doesn't it also e.g. check that the name doesn't include something like a greek letter?

[Aaron Liu]

names can contain greek letters

[Thomas Murrills]

Ah, right, which matters if we want to escape it, but not if it'll roundtrip