Removing unicode representations of mathematical symbols from the par…

…ser (#4023)

Fixes #3755

The documentation has long stated that only ACSII symbols are allowed in
Dafny source text (outside of strings. characters and comments). This PR
removes the representations of math symbols from the input parser.

<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>

Co-authored-by: davidcok <davidcok@github.com>

Source/DafnyCore/Dafny.atg

@@ -430,19 +430,19 @@ bool IsExpliesOp() => IsExpliesOp(la);
 bool IsAndOp() => IsAndOp(la);
 bool IsOrOp() => IsOrOp(la);
 static bool IsEquivOp(IToken la) {
-  return la.val == "<==>" || la.val == "\u21d4";
+  return la.val == "<==>";
 }
 static bool IsImpliesOp(IToken la) {
-  return la.val == "==>" || la.val == "\u21d2";
+  return la.val == "==>";
 }
 static bool IsExpliesOp(IToken la) {
-  return la.val == "<==" || la.val == "\u21d0";
+  return la.val == "<==";
 }
 static bool IsAndOp(IToken la) {
-  return la.val == "&&" || la.val == "\u2227";
+  return la.val == "&&";
 }
 static bool IsOrOp(IToken la) {
-  return la.val == "||" || la.val == "\u2228";
+  return la.val == "||";
 }
 bool IsBitwiseAndOp() {
   return la.val == "&";
@@ -468,10 +468,7 @@ bool IsRelOp() {
       || la.val == "!="
       || la.val == "in"
       || la.kind == _notIn
-      || la.val =="!"
-      || la.val == "\u2260"
-      || la.val == "\u2264"
-      || la.val == "\u2265";
+      || la.val == "!";
 }
 bool IsShiftOp() {
   if (la.kind == _openAngleBracket) {
@@ -493,7 +490,7 @@ bool IsMulOp() {
   return la.kind == _star || la.val == "/" || la.val == "%";
 }
 bool IsQSep() {
-  return la.kind == _doublecolon || la.kind == _bullet;
+  return la.kind == _doublecolon;
 }
 
 bool IsNonFinalColon() {
@@ -642,7 +639,6 @@ bool IsGenericInstantiation(bool inExpressionContext) {
     case _case:
     case _eq:
     case _neq:
-    case _neqAlt:
     case _as:
     case _is:
     case _darrow:
@@ -930,7 +926,6 @@ TOKENS
   doublecolon = "::".
   gets = ":=".
   boredSmiley = ":|".
-  bullet = '\u2022'. // •
   dot = '.'.
   backtick = "`".
   semicolon = ';'.
@@ -995,7 +990,6 @@ TOKENS
   singleeq = "=".
   eq = "==".
   neq = "!=".
-  neqAlt = '\u2260'. // ≠
   star = '*'.
   at = '@'.
   notIn = "!in" CONTEXT (nonidchar).
@@ -3911,9 +3905,6 @@ CalcOp<out IToken x, out CalcStmt.CalcOp/*!*/ op>
   | "<="           (. x = t;  binOp = BinaryExpr.Opcode.Le; .)
   | ">="           (. x = t;  binOp = BinaryExpr.Opcode.Ge; .)
   | "!="           (. x = t;  binOp = BinaryExpr.Opcode.Neq; .)
-  | '\u2260'       (. x = t;  binOp = BinaryExpr.Opcode.Neq; .)
-  | '\u2264'       (. x = t;  binOp = BinaryExpr.Opcode.Le; .)
-  | '\u2265'       (. x = t;  binOp = BinaryExpr.Opcode.Ge; .)
   | EquivOp        (. x = t;  binOp = BinaryExpr.Opcode.Iff; .)
   | ImpliesOp      (. x = t;  binOp = BinaryExpr.Opcode.Imp; .)
   | ExpliesOp      (. x = t;  binOp = BinaryExpr.Opcode.Exp; .)
@@ -3933,16 +3924,16 @@ CalcOp<out IToken x, out CalcStmt.CalcOp/*!*/ op>
  * these operators, both in Is...() methods (defined above) and as grammar non-terminals (defined
  * here).  These pairs of definitions must be changed together.
  */
-EquivOp = "<==>" | '\u21d4'.
-ImpliesOp = "==>" | '\u21d2'.
-ExpliesOp = "<==" | '\u21d0'.
-AndOp = "&&" | '\u2227'.
-OrOp = "||" | '\u2228'.
+EquivOp = "<==>".
+ImpliesOp = "==>".
+ExpliesOp = "<==".
+AndOp = "&&".
+OrOp = "||".
 
-NegOp = "!" | '\u00ac'.
-Forall = "forall" | '\u2200'.
-Exists = "exists" | '\u2203'.
-QSep = "::" | '\u2022'.
+NegOp = "!".
+Forall = "forall".
+Exists = "exists".
+QSep = "::".
 
 /* The "allowLemma" argument says whether or not the expression
  * to be parsed is allowed to have the form S;E where S is a call to a lemma.
@@ -4202,10 +4193,7 @@ RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op, out Expression k>
                         op = BinaryExpr.Opcode.Disjoint;
                       }
                    .)
-  | '\u2260'       (. x = t;  op = BinaryExpr.Opcode.Neq; .)
-  | '\u2264'       (. x = t;  op = BinaryExpr.Opcode.Le; .)
-  | '\u2265'       (. x = t;  op = BinaryExpr.Opcode.Ge; .)
-  )
+   )
   .
 
 /*------------------------------------------------------------------------*/

docs/DafnyRef/Grammar.md

@@ -22,6 +22,8 @@ All program text other than the contents of comments, character, string and verb
 consists of printable and white-space ASCII characters,
 that is, ASCII characters in the range `!` to `~`, plus space, tab, 
 carriage return and newline (ASCII 9, 10, 13, 32) characters.
+(In some past versions of Dafny, non-ASCII, unicode representations of some mathematical symbols were
+permitted in Dafny source text; these are no longer recognized.)
 
 String and character literals and comments may contain any unicode character,
 either directly or as an escape sequence.

docs/dev/3755.feat

@@ -0,0 +1 @@
+Unicode representations of mathemtical symbols (such as logical implies, and, and or) are no longer recognized by the parser.