Feat: Support for full UTF8 parsing by default.

RELEASE_NOTES.md

@@ -1,5 +1,6 @@
 # Upcoming
 
+- feat: Support for parsing Basic Multilingual Plane characters from UTF-8 in code and comments (https://github.com/dafny-lang/dafny/pull/2717)
 - feat: Command-line arguments are now available from `Main` in Dafny programs, using `Main(args: seq<string>)` (https://github.com/dafny-lang/dafny/pull/2594)
 - feat: Generate warning when 'old' has no effect (https://github.com/dafny-lang/dafny/pull/2610)
 - fix: Missing related position in failing precondition (https://github.com/dafny-lang/dafny/pull/2658)

Source/DafnyCore/Coco/Scanner.frame

@@ -354,6 +354,9 @@ public class Scanner {
       }
       buffer = new UTF8Buffer(buffer); col = 0;
       NextCh();
+    } else {
+      // We consider all files to be UTF-8 by default 
+      buffer = new UTF8Buffer(buffer);
     }
     pt = tokens = new Token();  // first token is a dummy
   }

Source/DafnyPipeline.Test/Trivia.cs

@@ -24,7 +24,7 @@ public void TriviaSplitWorksOnLinuxMacAndWindows() {
       foreach (Newlines newLinesType in Enum.GetValues(typeof(Newlines))) {
         currentNewlines = newLinesType;
         var programString = @"
-// Comment before
+// Comment ∈ before
 module Test // Module docstring
 {}
 
@@ -92,7 +92,7 @@ ensures true
         var f = defaultClass.Members[1];
         var g = defaultClass.Members[2];
         var m = defaultClass.Members[3];
-        AssertTrivia(moduleTest, "\n// Comment before\n", " // Module docstring\n");
+        AssertTrivia(moduleTest, "\n// Comment ∈ before\n", " // Module docstring\n");
         AssertTrivia(trait1, "/** Trait docstring */\n", " ");
         AssertTrivia(trait2, "// Just a comment\n", "\n// Trait docstring\n");
         AssertTrivia(subsetType, "// This is attached to n\n", "\n// This is attached to n as well\n\n");

Test/dafny0/PrintUTF8.dfy

@@ -0,0 +1,6 @@
+// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+  print "Mikaël fixed UTF8\n";
+}

Test/dafny0/PrintUTF8.dfy.expect

@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+Mikaël fixed UTF8

Test/dafny0/PrintUTF8Fails.dfy

@@ -0,0 +1,6 @@
+// RUN: %dafny_0 /compile:3 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+  print "Mikaël did not fix 😎\n";
+}

Test/dafny0/PrintUTF8Fails.dfy.expect

@@ -0,0 +1,2 @@
+PrintUTF8Fails.dfy(5,8): Error: invalid LogicalExpression
+1 parse errors detected in PrintUTF8Fails.dfy

docs/DafnyRef/Grammar.md

@@ -89,10 +89,9 @@ let you reconstruct the original grammar.
 
 ## 2.1. Dafny Input {#sec-unicode}
 
-Dafny source code files are readable text encoded as UTF-8 Unicode
-(because this is what the Coco/R-generated scanner and parser read).
+Dafny source code files are readable text encoded in UTF-8, where each decoded character has to be from the Basic Multilingual Plane and therefore encodable with a single UTF-16 code unit. This is what the Coco/R-generated scanner and parser read.
 All program text other than the contents of comments, character, string and verbatim string literals
-consists of printable and white-space ASCII characters,
+consists of printable and white-space ASCII characters.
 that is, ASCII characters in the range `!` to `~`, plus space, tab, cr and nl (ASCII, 9, 10, 13, 32)  characters.
 
 However, a current limitation of the Coco/R tool used by `dafny`