-
Notifications
You must be signed in to change notification settings - Fork 261
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
fix: Default to /unicodeChar:0 in legacy CLI as well #3635
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 <leino@amazon.com> Co-authored-by: Fabio Madge <fabio@madge.me> Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
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
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I had a couple of questions, but I think the current status is good to go, assuming the answers to those questions are what I expect.
@@ -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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
See other answer, same root cause. Nothing to do with refinement at least.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh, so does this work now? Nice!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No it's actually that the C++ compiler gives up earlier because it doesn't support /unicodeChar:1
:)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Still a nicer outcome. :)
This was accidentally missed from #3623.
Mostly I just updated expect files or added
/unicodeChar:0
where the testing coverage wasn't really relevant, but in a few cases I added/unicodeChar:1
variants underTest/unicodechars
where testing both modes was better.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.