feat: Unicode strings (--unicode-char) #3016
Merged
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
I guess it helps to have no actual character type. Or type checking for that matter. :)
Can’t just use string directly as a sequence without extra customization when —unicode-char
Just to close the loop, this is justified in "Printing Strings and Characters" in |
…code-strings # Conflicts: # Source/DafnyDriver/Commands/CommandRegistry.cs
RustanLeino
requested changes
Nov 23, 2022
RustanLeino
reviewed
Nov 23, 2022
| | Java | `char` | `int` / `dafny.CodePoint` | | ||
| | JavaScript | `string` of length 1 | `_dafny.CodePoint` (`number` wrapper) | | ||
| | Python | `str` of length 1 | `_dafny.CodePoint` (`str` of length 1 wrapper) | | ||
| | Go | `_dafny.Char` (`rune` wrapper) | `_dafny.CodePoint` (`rune` wrapper) | |
There was a problem hiding this comment.
Why is a wrapper needed around Go's rune?
RustanLeino
requested changes
Nov 23, 2022
Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/CodePoint.java
Outdated
Show resolved
Hide resolved
I originally thought compilers would need to reject some string values, but Go now handles invalid UTF-16 properly.
…code-strings # Conflicts: # Source/DafnyCore/Compilers/Compiler-js.cs
RustanLeino
approved these changes
Nov 23, 2022
|
Awesome to see this process of careful design followed by implementation! |
This was referenced Nov 24, 2022
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.
Implementation of the design from dafny-lang/rfcs#13.
Resolves #413. Fixes #2928. Fixes #818. Fixes #3058. Fixes #1293. Fixes #3001.
Depends on #2976 to be fixed for the tests to pass consistently across platforms.
I've documented some of the less obvious compilation strategy decisions in
docs/Compilation/StringsAndChars.md.Ready for review,
but will still add the fix to #2928 in the meantime (since it's easy to add as another test case in this set and most of the work is already done).By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.