make syntax cat accept empty string

Stream: lean4

[Alexander Bentkamp]

How can I make a syntax category accept the empty string?

import Lean

open Lean
open Lean.Parser

declare_syntax_cat manyPlus
syntax ("+"*) : manyPlus

#eval ((do logInfo s!"{runParserCategory (← getEnv) `manyPlus "+ +"}") : Elab.TermElabM _)
-- ok: («manyPlus+» ["+" "+"])

#eval ((do logInfo s!"{runParserCategory (← getEnv) `manyPlus "+"}") : Elab.TermElabM _)
-- ok: («manyPlus+» ["+"])

#eval ((do logInfo s!"{runParserCategory (← getEnv) `manyPlus ""}") : Elab.TermElabM _)
-- error: <input>:1:0: unexpected end of input

[Sebastian Ullrich]

:astonished:

[Sebastian Ullrich]

Is using a wrapper syntax foo := (manyPlus)? not an option?

[Alexander Bentkamp]

I am using runParserCategory, so I think it has to be a syntax category. Or is there a similar function for syntax that does not have its own category? Of course, I can work around the whole issue by checking whether what I am parsing is only whitespace. I just wanted to make sure I am not missing a better solution here.

[Mario Carneiro]

you can just run Parser.optional (runParserCategory ...) in that case, I think?

[Sebastian Ullrich]

Not quite, you'd have to copy its implementation and change the invoked parser p

[Mario Carneiro]

hm, there should be a Parser.run frontend that just takes a string and a Parser

[François G. Dorais]

I'm running into a related issue and, before I try to work on a workaround, what is the issue behind having a Parser.run frontend as @Mario Carneiro just described?

[Mario Carneiro]

it's not difficult to write, you can just adapt runParserCategory

[Mario Carneiro]

import Lean
open Lean Parser

/-- convenience function for testing -/
def Parser.run (env : Environment) (p : Parser) (input : String) (fileName := "<input>") : Except String Syntax :=
  let c := mkParserContext (mkInputContext input fileName) { env := env, options := {} }
  let s := mkParserState input
  let s := whitespace c s
  let s := p.fn c s
  if s.hasError then
    Except.error (s.toErrorMsg c)
  else if input.atEnd s.pos then
    Except.ok s.stxStack.back
  else
    Except.error ((s.mkError "end of input").toErrorMsg c)

[François G. Dorais]

Can I drop env if I don't need fileName? (I'm only parsing strings in my use case.)

[François G. Dorais]

Seems like mkParserState might use the environment.

[Mario Carneiro]

no, parsers need the environment because a parser might call a category parser which needs everything in the parser extension

[Mario Carneiro]

fileName is only used in error messages AFAIK

[François G. Dorais]

Right. That makes sense. Thanks!

[Sebastian Ullrich]

You can keep the environment empty if all your parsers are builtin, though that is not currently possible with syntax