fix ordinals not being applied to return types of symbols #1162
Conversation
This file contains 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
theo25
approved these changes
Oct 28, 2024
| } | ||
| if (symbol->get_sort()->is_concrete()) { | ||
| process_sort_ordinal( | ||
| symbol->get_sort().get(), sorts, all_sorts_, next_sort); |
There was a problem hiding this comment.
I noticed that I missed processing the return sort in my implementation of the work list. However checking back at the original code, I don't think this was there either. So could you explain why this is needed? Is it the case that it missing was a bug even before we added the work list implementation?
There was a problem hiding this comment.
It was a bug that was there before your changes were made, yes. The issue is that formal parameters that appear only in the return sort of the symbol (e.g. the second parameter of inj) were not getting their ordinal set and thus were getting serialized incorrectly.
Robertorosmaninho
approved these changes
Oct 29, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This fixes a bug where the sort ordinals for formal parameters mentioned only in the return type of the symbol were not correct, leading to incorrect serialization of terms containing injections.