Dafny: disallow declare identifiers starting with underscore (_)

It is still possible to reference names containing an underscore, but it is not
possible to make a variable, method, class, bound variable, type, or module name
beginning with one.

2 files changed, 50 insertions, 30 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 7ffdcbbc..4b76f9b4 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -175,7 +175,7 @@ SubModuleDecl<ModuleDecl parent, bool isOverallModuleGhost, out SubModuleDecl su
   .)

      "module"

       { Attribute<ref attrs> }

-      Ident<out id>                        (. .)

+      NoUSIdent<out id>                        (. .)

       [ "refines" Ident<out idRefined> ]

       [ "imports" Idents<theImports> ]     (. module = new ModuleDecl(id, id.val, isOverallModuleGhost, idRefined == null ? null : idRefined.val, theImports, attrs);

                                               parent.Dependencies.Add(module); .)

@@ -209,7 +209,7 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
   SYNC

   "class"

   { Attribute<ref attrs> }

-  Ident<out id>

+  NoUSIdent<out id>

   [ GenericParameters<typeArgs> ]

   "{"                                            (. bodyStart = t; .)

   { ClassMemberDecl<members, false, true>

@@ -250,7 +250,7 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
   | "codatatype"     (. co = true; .)

   )

   { Attribute<ref attrs> }

-  Ident<out id>

+  NoUSIdent<out id>

   [ GenericParameters<typeArgs> ]

   "="                                      (. bodyStart = t; .)

   DatatypeMemberDecl<ctors>

@@ -272,7 +272,7 @@ DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>
      List<Formal/*!*/> formals = new List<Formal/*!*/>();

   .)

   { Attribute<ref attrs> }

-  Ident<out id>

+  NoUSIdent<out id>

   [ FormalsOptionalIds<formals> ]

   (. ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); .)

   .

@@ -297,7 +297,7 @@ ArbitraryTypeDecl<ModuleDecl/*!*/ module, out ArbitraryTypeDecl at>
   .)

   "type"

   { Attribute<ref attrs> }

-  Ident<out id>               (. at = new ArbitraryTypeDecl(id, id.val, module, attrs); .)

+  NoUSIdent<out id>               (. at = new ArbitraryTypeDecl(id, id.val, module, attrs); .)

   SYNC ";"

   .

 GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>

@@ -311,14 +311,14 @@ GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out boo
   .

 IdentType<out IToken/*!*/ id, out Type/*!*/ ty>

 = (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.)

-  Ident<out id>

+  NoUSIdent<out id>

   ":"

   Type<out ty>

   .

 LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>

 = (. IToken/*!*/ id;  Type/*!*/ ty;  Type optType = null;

   .)

-  Ident<out id>

+  NoUSIdent<out id>

   [ ":" Type<out ty>             (. optType = ty; .)

   ]

   (. var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)

@@ -326,7 +326,7 @@ LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
 IdentTypeOptional<out BoundVar/*!*/ var>

 = (. Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id;  Type/*!*/ ty;  Type optType = null;

   .)

-  Ident<out id>

+  NoUSIdent<out id>

   [ ":" Type<out ty>             (. optType = ty; .)

   ]

   (. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)

@@ -362,8 +362,8 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
 = (. Contract.Requires(cce.NonNullElements(typeArgs));

      IToken/*!*/ id; .)

   "<"

-  Ident<out id>                       (. typeArgs.Add(new TypeParameter(id, id.val)); .)

-  { "," Ident<out id>                 (. typeArgs.Add(new TypeParameter(id, id.val)); .)

+  NoUSIdent<out id>                       (. typeArgs.Add(new TypeParameter(id, id.val)); .)

+  { "," NoUSIdent<out id>                 (. typeArgs.Add(new TypeParameter(id, id.val)); .)

   }

   ">"

   .

@@ -407,7 +407,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
      }

   .)

   { Attribute<ref attrs> }

-  Ident<out id>

+  NoUSIdent<out id>

   (

     [ GenericParameters<typeArgs> ]

     Formals<true, !mmod.IsGhost, ins, out openParen>

@@ -567,7 +567,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
     (. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }

     .)

     { Attribute<ref attrs> }

-    Ident<out id>

+    NoUSIdent<out id>

     (

       [ GenericParameters<typeArgs> ]

       Formals<true, isFunctionMethod, formals, out openParen>

@@ -584,7 +584,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
     (. if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); }

     .)

     { Attribute<ref attrs> }

-    Ident<out id>

+    NoUSIdent<out id>

     (

       [ GenericParameters<typeArgs> ]

       [ Formals<true, isFunctionMethod, formals, out openParen>

@@ -694,10 +694,10 @@ OneStmt<out Statement/*!*/ s>
   | MatchStmt<out s>

   | ParallelStmt<out s>

   | "label"                            (. x = t; .)

-    Ident<out id> ":"

+    NoUSIdent<out id> ":"

     OneStmt<out s>                     (. s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); .)

   | "break"                            (. x = t; breakCount = 1; label = null; .)

-    ( Ident<out id>                    (. label = id.val; .)

+    ( NoUSIdent<out id>                    (. label = id.val; .)

     | { "break"                        (. breakCount++; .)

       }

     )

@@ -1639,6 +1639,16 @@ Ident<out IToken/*!*/ x>
 = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)

   ident            (. x = t; .)

   .

+// Identifier, disallowing leading underscores

+NoUSIdent<out IToken/*!*/ x>

+= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)

+  ident            (. x = t; 

+                      if (x.val.Length > 0 && x.val.StartsWith("_")) {

+                        SemErr("cannot declare identifier beginning with underscore");

+                      }

+                   .)

+  .

+

 Nat<out BigInteger n>

 =

   digits

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 142d963e..3f58c1db 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -238,7 +238,7 @@ bool IsAttribute() {
 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

-		Ident(out id);

+		NoUSIdent(out id);

 		

 		if (la.kind == 10) {

 			Get();

@@ -297,7 +297,7 @@ bool IsAttribute() {
 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

-		Ident(out id);

+		NoUSIdent(out id);

 		if (la.kind == 22) {

 			GenericParameters(typeArgs);

 		}

@@ -333,7 +333,7 @@ bool IsAttribute() {
 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

-		Ident(out id);

+		NoUSIdent(out id);

 		if (la.kind == 22) {

 			GenericParameters(typeArgs);

 		}

@@ -364,7 +364,7 @@ bool IsAttribute() {
 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

-		Ident(out id);

+		NoUSIdent(out id);

 		at = new ArbitraryTypeDecl(id, id.val, module, attrs); 

 		while (!(la.kind == 0 || la.kind == 18)) {SynErr(114); Get();}

 		Expect(18);

@@ -403,6 +403,16 @@ bool IsAttribute() {
 		Expect(7);

 	}

 

+	void NoUSIdent(out IToken/*!*/ x) {

+		Contract.Ensures(Contract.ValueAtReturn(out x) != null); 

+		Expect(1);

+		x = t; 

+		if (x.val.Length > 0 && x.val.StartsWith("_")) {

+		 SemErr("cannot declare identifier beginning with underscore");

+		}

+		

+	}

+

 	void Ident(out IToken/*!*/ x) {

 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); 

 		Expect(1);

@@ -424,11 +434,11 @@ bool IsAttribute() {
 		Contract.Requires(cce.NonNullElements(typeArgs));

 		IToken/*!*/ id; 

 		Expect(22);

-		Ident(out id);

+		NoUSIdent(out id);

 		typeArgs.Add(new TypeParameter(id, id.val)); 

 		while (la.kind == 20) {

 			Get();

-			Ident(out id);

+			NoUSIdent(out id);

 			typeArgs.Add(new TypeParameter(id, id.val)); 

 		}

 		Expect(23);

@@ -487,7 +497,7 @@ bool IsAttribute() {
 			while (la.kind == 6) {

 				Attribute(ref attrs);

 			}

-			Ident(out id);

+			NoUSIdent(out id);

 			if (la.kind == 22 || la.kind == 33) {

 				if (la.kind == 22) {

 					GenericParameters(typeArgs);

@@ -512,7 +522,7 @@ bool IsAttribute() {
 			while (la.kind == 6) {

 				Attribute(ref attrs);

 			}

-			Ident(out id);

+			NoUSIdent(out id);

 			if (StartOf(3)) {

 				if (la.kind == 22) {

 					GenericParameters(typeArgs);

@@ -592,7 +602,7 @@ bool IsAttribute() {
 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

-		Ident(out id);

+		NoUSIdent(out id);

 		if (la.kind == 22 || la.kind == 33) {

 			if (la.kind == 22) {

 				GenericParameters(typeArgs);

@@ -634,7 +644,7 @@ bool IsAttribute() {
 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

-		Ident(out id);

+		NoUSIdent(out id);

 		if (la.kind == 33) {

 			FormalsOptionalIds(formals);

 		}

@@ -658,7 +668,7 @@ bool IsAttribute() {
 

 	void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {

 		Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);

-		Ident(out id);

+		NoUSIdent(out id);

 		Expect(5);

 		Type(out ty);

 	}

@@ -682,7 +692,7 @@ bool IsAttribute() {
 	void LocalIdentTypeOptional(out VarDecl/*!*/ var, bool isGhost) {

 		IToken/*!*/ id;  Type/*!*/ ty;  Type optType = null;

 		

-		Ident(out id);

+		NoUSIdent(out id);

 		if (la.kind == 5) {

 			Get();

 			Type(out ty);

@@ -694,7 +704,7 @@ bool IsAttribute() {
 	void IdentTypeOptional(out BoundVar/*!*/ var) {

 		Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id;  Type/*!*/ ty;  Type optType = null;

 		

-		Ident(out id);

+		NoUSIdent(out id);

 		if (la.kind == 5) {

 			Get();

 			Type(out ty);

@@ -1101,7 +1111,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		case 49: {

 			Get();

 			x = t; 

-			Ident(out id);

+			NoUSIdent(out id);

 			Expect(5);

 			OneStmt(out s);

 			s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); 

@@ -1111,7 +1121,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			x = t; breakCount = 1; label = null; 

 			if (la.kind == 1) {

-				Ident(out id);

+				NoUSIdent(out id);

 				label = id.val; 

 			} else if (la.kind == 18 || la.kind == 50) {

 				while (la.kind == 50) {