Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Fix tidySymbol to not drop arg-id #659

Merged
merged 5 commits into from
Nov 4, 2023
Merged

Fix tidySymbol to not drop arg-id #659

merged 5 commits into from
Nov 4, 2023

Conversation

ranjitjhala
Copy link
Member

  • also separate unKArgSymbol for matching qual-patterns

fixes #658

facundominguez
facundominguez approved these changes Nov 4, 2023
View reviewed changes
src/Language/Fixpoint/Types/Names.hs
@@ -518,7 +518,7 @@ tidySymbol s
| otherwise = s''
where
s' = unPrefixSymbol kArgPrefix s
s'' = unPrefixSymbol symSepName . unPrefixSymbol hvarPrefix $ s'
s'' = consSym '$' . unPrefixSymbol symSepName . unSuffixSymbol . unPrefixSymbol hvarPrefix $ s'
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm out of my depth here, but I just wanted to suggest adding a comment to tidySymbol explaining what it is meant to do.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And similar suggestion for the other functions modified in the PR. Alternatively, perhaps the source code could be made more self explanatory if the structure of the symbols is explained in a comment.

@ranjitjhala
Copy link
Member Author

ranjitjhala commented Nov 4, 2023 via email

@ranjitjhala ranjitjhala merged commit f740c34 into develop Nov 4, 2023
11 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@facundominguez facundominguez facundominguez approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Missing suffix in var when printing solution with --save
2 participants
@ranjitjhala @facundominguez