Allow macros on hooked sorts#2489
Merged
rv-jenkins merged 4 commits intoruntimeverification:masterfrom Mar 22, 2022
Merged
Conversation
added 3 commits
March 17, 2022 14:38
The previous implementation of macros on productions forgot to account for macros on hooked sorts. This led kompile to assume that macro productions on hooked sorts implied that the productions were constructors. Code like this ``` syntax Int ::= "LABEL" [macro] rule LABEL => 4 // or some other number ``` would result in errors like this: ``` $ kompile test.k [Error] Compiler: Cannot add new constructors to hooked sort Int ``` However, `"LABEL"` in this case is not a constructor but a term that would be translated to `4` during compilation so this error is not applicable to productions that are macros. This change add changes to the CheckAtt class to allow macros on hooked sorts.
Baltoli
reviewed
Mar 22, 2022
| if (sortAtt.contains(Att.HOOK()) && !sortAtt.get(Att.HOOK()).equals("ARRAY.Array") && !(sortAtt.get(Att.HOOK()).equals("KVAR.KVar") && isSymbolicKast)) { | ||
| if (!prod.att().contains(Att.FUNCTION()) && !prod.att().contains(Att.BRACKET()) && | ||
| !prod.att().contains("token") && !(prod.klabel().isDefined() && macros.contains(prod.klabel().get()))) { | ||
| !prod.att().contains("token") && !prod.att().contains("macro") && !(prod.klabel().isDefined() && macros.contains(prod.klabel().get()))) { |
Contributor
There was a problem hiding this comment.
This isn't a change to this specific PR (which looks good to me), but it would be nice in general to have this kind of deeply nested / long chain code factored out into a helper method with a comment explaining the logic. Perhaps it would be worth someone spending some time on the API design of the frontend to make this kind of code easier to write
5 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The previous implementation of macros on productions forgot to account for
macros on hooked sorts. This led kompile to assume that macro productions on
hooked sorts implied that the productions were constructors. Code like this
would result in errors like this:
However,
"LABEL"in this case is not a constructor but a term thatwould be translated to
4during compilation so this error is notapplicable to productions that are macros. This change add changes to
the CheckAtt class to allow macros on hooked sorts.
Fixes: #2488