New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Discrepancy between terminal and single-match regex terminal #4082
Comments
I dug into this.
I think you identified the reason here, but for concreteness the issue is a collision with the regex for
Regex terminals have a lower priority than non-regex terminals. The logic isn't especially obvious, but when we generate scanners there's a sorting process that happens here: k/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java Lines 153 to 156 in 67ef71b
k/kore/src/main/scala/org/kframework/definition/outer.scala Lines 969 to 992 in 67ef71b
This ordering places regexes at the end of the list, which means that if any non-regex matches first then the overlapping regex won't get considered. It also answers the question of why the
Because of the tokenization problem, inner parsing hasn't even finished when the error in (2) is emitted. This means that we don't have the full semantic information to validate the attributes. For (3), inner parsing has succeeded and we can validate the attributes. |
Consider the following definitions.
1. With terminal
This works as expected.
2. With regex terminal
Let's change the symbol to a regex terminal.
This defines the same set of valid tokens for
Foo
as the previous definition. But now there's a parse error:3. Fix potential lexical conflicts
Speculatively, let's change the token to be disjoint from other lexicals in the prelude.
Now the error is something different:
4. Add the
format
attributeAfter adding the
format
attribute, kompilation works.Questions
This raises a few questions.
format
attribute for (3) if for (2) it does not?The text was updated successfully, but these errors were encountered: