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.

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

Generalize JSON code to work with either --unicode-char mode #118

Merged
merged 17 commits into from
Apr 19, 2023

Conversation

robin-aws
Copy link
Member

@robin-aws robin-aws commented Apr 12, 2023

Replaced the src/JSON/Utils/Unicode.dfy code with references to the Unicode library, not only because the latter has more correctness proofs but also because it more safely fails to translate invalid data rather than using replacement characters. This introduces more cases of needing Result wrappers, but most of the library needed them already anyway so it does not impact usability. I've also likely introduced some minor performance regressions compared to the current state of json-merge by using the less-optimized Unicode library, but they should be worth it so this code can be merged, since performance can always be improved later.

Adds a generic UnicodeStrings module to help with this, which should be helpful for other codebases that need to support both modes. This also addresses #111.

Open question: which of the two options in UnicodeStrings.dfy should we use in this repository in general?

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

Copy link
Collaborator

@davidcok davidcok left a comment

Choose a reason for hiding this comment

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

Please put these changes under src/dafny -- that is the copy of the library we are trying to move ahead with.

@robin-aws
Copy link
Member Author

Please put these changes under src/dafny -- that is the copy of the library we are trying to move ahead with.

More relevant to address in #51 - this one just builds on that one

@fabiomadge fabiomadge marked this pull request as ready for review April 19, 2023 22:40
@fabiomadge fabiomadge merged commit 942be81 into dafny-lang:json-merge Apr 19, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants