From 4f2f785d121651c62cf0a7da7c7bcaef13ee14b4 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Tue, 19 Jun 2012 14:35:22 -0700
Subject: 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.
---
 Dafny/Dafny.atg | 40 +++++++++++++++++++++++++---------------
 Dafny/Parser.cs | 40 +++++++++++++++++++++++++---------------
 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) {
-- 
cgit v1.2.3