Calling the parser at a point

Stream: metaprogramming / tactics

[Snir Broshi]

How do I call the parser? Basically I have a String and I want to parse it into Syntax, while letting it use any locally defined notation at a specific point in a source file. I'm running inside a linter if that helps, so I have a Syntax object that came from that specific point.
I found docs#Lean.Parser.runParserCategory but I'm not sure that's it

[Snir Broshi]

(specifically, I'm taking the stx : Syntax object I get, modifying the string stx.getSubstring?, then I want to reparse it as if it was written at the same place)

[Edward van de Meent]

I think usually it's just easier to manually create the Syntax you want?

[Snir Broshi]

But I don't know what Syntax I want, the point is to check what the parser parses it as

[Snir Broshi]

I assume the parser has round-trip tests together with the pretty-printer, which have to call a "parse" function at some point, can you point me to them?

[Thomas Murrills]

Would you mind #xy ’ing bit? It’s a bit unusual to be in this situation, and maybe this is the only way, but I’d really hope there’s another way :) This doesn’t sound like something a linter would usually do (but maybe there’s a specific use case).

(Note also that you would need to take care of open scopeds that appear within the command itself if you were to parse!)

[Snir Broshi]

Sure- I'm trying to solve this TODO for factorial notation, using a linter.
The idea is to find all uses of the factorial notation with a space before it, attempt to remove the spaces, and the reparsing is to figure out if we need to add parentheses or not.

Not all situations need parentheses, and while we can do a conservative approximation with "is this a numeral or already surrounded by parentheses", I really want to know precisely if we need to add parentheses or not.
I started out with the approximation, then found out 3.! is valid, then I found out that if I add notation "/" => 3 then /! is valid, so I decided to ask the parser.

[Snir Broshi]

There's also the strange [0][0] ! which needs parentheses

[Snir Broshi]

Code skeleton

module
public meta import Mathlib.Tactic.Linter.Header
import Lean.Parser.Syntax
import Init.Data.String.TakeDrop
meta section
open Lean Elab Command Linter
namespace Mathlib.Linter

public register_option linter.style.testing : Bool := { defValue := false }

partial def foo {m} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] :
    Syntax → m Unit
  | stx@(.node _info kind args) => do
    match kind, args with
    | `Nat.term_!, #[child, .atom _ "!"] =>
      -- TODO: remove the space after `child`, reparse, and compare to `stx`.
      --       if the result changes (besides the offset of the `!`), add parentheses.
      logInfo m!"'{stx.getSubstring?.getD default}' '{child.getSubstring?.getD default}'"
    | _, _ =>
      for arg in args do
        foo arg
  | _ => return

initialize addLinter { run := withSetOptionIn fun stx ↦ do
  unless Linter.getLinterValue linter.style.testing (← getLinterOptions) do
    return
  foo stx
}

end Mathlib.Linter

[Thomas Murrills]

Ah, I see!

This does seem like the right approach from one perspective! But I actually wonder if it’s better for human readability to just say

• numeric literals are unparenthesized
• everything else is parenthesized

Then you know it’s a factorial, and not part of the name or notation. (We’d save some code complexity too.) But, are there real-world examples where we have some notation and want it followed by a !, without parentheses? Then it makes sense to take a reparsing approach.

[Snir Broshi]

I don't think we have such a case in Mathlib based on a rudimentary regex search, so this sounds good, thanks!

[Snir Broshi]

I am still interested to know how to call the parser, though

[Thomas Murrills]

Yes, me too—especially "in the middle of a command" like this! :) I started poking around, and I'm pretty sure runParserCategory is designed just for testing. It seems to use empty options and an empty parser state. To parse correctly, one approach would be to run the appropriate ParserFn (e.g. categoryParserFnImpl catName as runParserCategory uses, with catName being `term), but then set up the state so that the right declarations are open (and possibly some other facts?). I'm not sure what exactly this looks like yet.

To get the open decls, at least, I think it might be sufficient to just consider open syntax that appears in the command, and collect them on your way to the nested syntax. I think docs#Lean.Parser.withOpenDecl (and component declarations) are the only thing that affects the parser, that they check for open explicitly, and that parsing completes entirely before any kind of elaboration, meaning that e.g. syntax like classical which opens scopes for elaboration do not also open scopes for parsing. Maybe!

[Thomas Murrills]

Hmm, actually, I suppose it's possible that a parser could depend on withNamespaces directly, and not check for open syntax. (Or be written from the ground up to modify the parser state.) Does e.g. classical do this? (Is there any scoped classical notation?)

[Snir Broshi]

Snir Broshi said:

I don't think we have such a case in Mathlib based on a rudimentary regex search

Actually I found this and this

[Snir Broshi]

And here's the same case but with a redundant space

[Thomas Murrills]

Nice finds! Those in fact reinforce my feeling that they would be more readable/predictable if parenthesized, but I'm open to differing opinions :grinning_face_with_smiling_eyes: