Feat: Support for full UTF8 parsing by default.

[MikaelMayer]

This PR enables support for parsing any UTF-8 string in a source file and in comments.

Is it a fix for #2620 ?

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

[robin-aws]

So glad the fix was as simple as I suspected! :)

Let's add at least one integration test too. Something like:

method Main() {
  print "Mikaël Mayer fixed UTF8 parsing!", "\n";
}

I'd like to verify whether this is enough to support arbitrary characters in string literals (I suspect it is but I'm not sure).

We also need to update the reference manual since it touches on this: https://dafny.org/dafny/DafnyRef/DafnyRef#sec-unicode.

[robin-aws]

Is it a fix for #2620 ?

Nope, because that issue talking about invalid uses of \u escape sequences. But you may be fixing the separate issue that directly included non-ASCII characters are truncated by the parser:

method Main() {
  var s := "Unicode is just so 😎";
  print s, "\n";
}

This currently prints "Unicode is just so ð" (in C# at least), because the parser only retains the first byte (0xF0) of the emoji character's UTF8 encoding and then interprets it as a UTF16 code unit.

[MikaelMayer]

I'm able to make it work with ë (the utf-8 sequence compiles the value of the two byte sequence to 240, which is interpreted as the ë in ASCII)
but not the smiley. I tried my best for 30 minutes to change the scanner so that the smiley would pass, but 1) although it's one character, it takes two columns on an editor and 2) it would require not casting from (int) to (char), and I haven't found the good recipe.
So, do we want smileys for now, or should I just be happy with this change for now?

[robin-aws]

No don't worry about smileys for now. :) I just wanted to understand the extent of the fix. If ë works please do add a test to lock that down, but that's enough.

[robin-aws]

We need to be excruciatingly precise about what is working and what still isn't, given how much confusion Unicode tends to cause users.

AFAICT UTF-8 sequences that map to a single UTF-16 code unit (such as ∈ in your unit test) definitely round-trip successfully through parsing and printing, but I'm not convinced those that need UTF-16 surrogates do (such as 😎, which maps to 0xD83D 0xDE0E in UTF-16 - note that I've been using that emoji as a canonical example because many other emojis actually map to multiple Unicode scalar values, and that's a layer of complexity we can avoid for now :).

It's going to be challenging to nail that in a single sentence, so I'd suggest tackling the reference manual section edit first. We'll likely want to include a link to that here too.

[robin-aws]

Thanks for continuing to entertain my nit-picking.

[robin-aws]

Oh wow that's worse than I thought 😎

[robin-aws]

❤️ (even if we can't quite parse that yet)

[davidcok]

The change from , to . is wrong here -- it leaves a sentence fragment on the next line.

[MikaelMayer]

Can you fix it in your next PR please? I can review that. Thanks for reporting.

[davidcok]

Added to cok-docs-TODOs, PR#2817