search

dafny-lang / libraries

Libraries useful for Dafny programs
Other
43 stars 25 forks source link

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

Closed robin-aws closed 1 year ago

robin-aws commented 1 year ago

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.

robin-aws commented 1 year ago

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