Preventing Parser Backtracking

Stream: lean4

[Mac]

Is there a way to stop the Lean parser from backtracking after certain in a parse. That is, is there some way to tell the Pratt parser to treat syntax errors after a certain point as just that (syntax errors) rather than trying to parser it with a different (lower priority).

Alternatively, is there a way to tell Lean to use the syntax/errors from the higher priority parser (i.e., the first one tried), rather than the syntax/errors of the lower priority parser (i.e., the last one tried).

[Mac]

Here is a #mwe:

declare_syntax_cat foo (behavior := symbol)

macro (priority := low) x:term : foo => x
macro "bar " x:str " baz" : foo => x
macro "foo " x:foo : term => x

#check foo bar "hi" bap
/-
  Errors on `bar` with `unknown identifier 'bar'`
  Instead of on `baz` with `expected 'baz'`
  Also breaks semantic syntax highlighting
-/

[Sebastian Ullrich]

Is <|> an option in your case?

[Mac]

Sadly, no, the category is very categorical. To be specific, the case in questions is for the augmented do notation of Papyrus.

[Mac]

The regular doElem syntax preempts that of the augmented keywords (when syntax errors occur) which makes me think there is a bug when it is just a typo on my part (which I imagine would also flummox end-users). It also makes such typos hard to debug (as the errors are nonsensical).

[Mac]

In addition to the uniformative errors, the low priority parser also kicks in when its parse is longer than that of the higher priority parser. This cases a short instruction (e.g., ret i32 0) to get merged with a subsequent assignment (e.g., %foo = load i1, bar) because it ends up parsing them as two terms joined by the % operator.

[Mac]

I can likely get around this by just require pure Lean statements to be prefixed with some token (e.g., #), but I was curious if there was a way to avoid such a requirement.

[Mario Carneiro]

One approach that is used in the lean grammar is the selective use of notFollowedBy in the fallback parser to make it inapplicable when you use a keyword. So for example your term => doElem' parser would instead be syntax notFollowedBy("ret") term : doElem', where you extend the list to include all keywords you want to avoid. It's not perfect since you are still using an exhaustive list, but perhaps you can at least list your keywords.

[Sebastian Ullrich]

I don't think there is. But you are essentially writing a quasiquotation syntax, so I would definitely expect special tokens for introducing antiquotations there.

[Mac]

@Sebastian Ullrich Fair enough. I was actually wondering there was a way I could use the antiquotation syntax itself (i.e., $(x)), but I don't think there is a way to use that without also making things like $(x):ident valid, which makes no sense in this context.