fix: Default to /unicodeChar:0 in legacy CLI as well #3635
Conversation
This solution uses an AutoGeneratedToken when filling in an omitted size. Previously, the code looked at the LiteralExpr in ArrayDimensions[0], which had the effect of also eliding a programmer-supplied size. Also, the previous implementation would crash if a size was given but wasn’t a LiteralExpr.
* Remove duplicate check * Add omitted check * Change error message to talk about “memory limit” rather than some C# property
…ble-unicode-char-by-default-in-legacy-cli
…r-by-default-in-legacy-cli
…/dafny into java-unicode-char-improvements
…/dafny into java-unicode-char-improvements
…r-by-default-in-legacy-cli # Conflicts: # Source/DafnyCore/Compilers/Java/Compiler-java.cs # Test/comp/UnicodeStrings.dfy # Test/concurrency/10-SequenceInvariant.dfy # Test/concurrency/11-MutexGuard2.dfy # Test/concurrency/12-MutexLifetime-short.dfy # Test/dafny0/Strings.dfy # Test/dafny4/git-issue245.dfy # Test/dafny4/git-issue245.dfy.expect
Fixes #3413. Addresses the issues uncovered during #2818 by adding a `--unicode-char` mode version of `Test/comp/Arrays.dfy`, which all stem from incomplete handling of manual boxing/unboxing of the `CodePoint` type at various Java code generation points. Note this is still incomplete as there must be other spots that do not handle coercion correctly in general, but these changes at least cover `Arrays.dfy`. It turned out that handling arrow coercion as in the Go compiler was not necessary for Java, because the initial casting of a function reference as a lambda is where the necessary boxing/unboxing needs to happen instead anyway. That is, a reference to a Dafny `function f(x: char): char` has to end up as a Java `Function<CodePoint, CodePoint>` and therefore be eta expanded from the start. Also removed the fail-fast behavior from `%testDafnyForEachCompiler` as I found it more useful for debugging that way. Also implemented `ConcreteSyntaxTree.Comma` as part of an initial implementation of Java arrow conversion, which ended up not directly used but seems useful enough to keep (and I refactored one spot to use it as an example). Edit: I've also added a few more similar cases exposed as part of enabling `/unicodeChar:1` by default for Dafny 4.0: #3635 Co-authored-by: Rustan Leino <[email protected]> Co-authored-by: Fabio Madge <[email protected]> Co-authored-by: Aaron Tomb <[email protected]>
Picking up recent changes from master, especially #3630 as those fixes are necessary to unblock #3635. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
….com:robin-aws/dafny into enable-unicode-char-by-default-in-legacy-cli
| @@ -18,7 +18,7 @@ Stream.Next | |||
| {Berry.Smultron, Berry.Jordgubb, Berry.Hallon} | |||
| CoBerry.Hjortron true true false | |||
| false | |||
| 42 q hello | |||
| 42 'q' hello | |||
There was a problem hiding this comment.
It's strange to me for this to be an artifact to switching to proper Unicode characters, but I'm not opposed to it.
There was a problem hiding this comment.
It's an intentional side-effect, although only documented internally: https://github.com/dafny-lang/dafny/blob/master/docs/Compilation/StringsAndChars.md#printing-strings-and-characters
As you're not the first to ask it might be worth following up on with documentation, but since the behavior of print is all but unspecified in the reference manual or anywhere else I'm not sure it's worth it. :)
| @@ -1,3 +1,3 @@ | |||
|
|
|||
| Dafny program verifier finished with 21 verified, 0 errors | |||
| Send cards to: {Mike, Susan} | |||
| Send cards to: {['M', 'i', 'k', 'e'], ['S', 'u', 's', 'a', 'n']} | |||
There was a problem hiding this comment.
This is a little weirder than the character instance. Is this the best way to print strings? Does it only come about due to refinement?
There was a problem hiding this comment.
See other answer, same root cause. Nothing to do with refinement at least.
There was a problem hiding this comment.
It seems to me that other tests were printing strings like "Mike" (adding double quotes), which seems like a nice behavior to me. Was I misinterpreting that, or is something different going on here?
There was a problem hiding this comment.
It's only because this is the result of (effectively) print {"Mike", "Susan"};. So it's printing a set<string> rather than string values. The runtimes COULD handle this better, but they'd need to accept a areElementsStrings parameter which the compiler would fill in when it knows the target set<T> type is in fact a set<string>.
| (0,-1): Error: UserDefinedTypeName _#Func1 | ||
|
|
||
| Error: | ||
|
|
There was a problem hiding this comment.
No it's actually that the C++ compiler gives up earlier because it doesn't support /unicodeChar:1 :)
This was accidentally missed from #3623.
Mostly I just updated expect files or added
/unicodeChar:0where the testing coverage wasn't really relevant, but in a few cases I added/unicodeChar:1variants underTest/unicodecharswhere testing both modes was better.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.