summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Dafny.atg34
-rw-r--r--Source/Dafny/DafnyAst.cs20
-rw-r--r--Source/Dafny/Parser.cs30
-rw-r--r--Source/Dafny/Printer.cs18
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs4
5 files changed, 77 insertions, 29 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 50f6859e..c558dd14 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -318,8 +318,8 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
(. if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
.)
{ Attribute<ref attrs> }
- IdentType<out id, out ty> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
- { "," IdentType<out id, out ty> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
+ IdentType<out id, out ty, false> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
+ { "," IdentType<out id, out ty, false> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
}
SYNC ";"
.
@@ -342,18 +342,18 @@ GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out boo
isGhost = false; .)
[ "ghost" (. if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)
]
- IdentType<out id, out ty>
+ IdentType<out id, out ty, true>
.
-IdentType<out IToken/*!*/ id, out Type/*!*/ ty>
+IdentType<out IToken/*!*/ id, out Type/*!*/ ty, bool allowWildcardId>
= (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.)
- NoUSIdent<out id>
+ WildIdent<out id, allowWildcardId>
":"
Type<out ty>
.
LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
= (. IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
.)
- NoUSIdent<out id>
+ WildIdent<out id, true>
[ ":" Type<out ty> (. optType = ty; .)
]
(. var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)
@@ -361,7 +361,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;
.)
- NoUSIdent<out id>
+ WildIdent<out id, true>
[ ":" Type<out ty> (. optType = ty; .)
]
(. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)
@@ -399,10 +399,10 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
TypeParameter.EqualitySupportValue eqSupport;
.)
"<"
- NoUSIdent<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
+ NoUSIdent<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
[ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
- { "," NoUSIdent<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
+ { "," NoUSIdent<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
[ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
}
@@ -1775,12 +1775,26 @@ Ident<out IToken/*!*/ x>
NoUSIdent<out IToken/*!*/ x>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
ident (. x = t;
- if (x.val.Length > 0 && x.val.StartsWith("_")) {
+ if (x.val.StartsWith("_")) {
SemErr("cannot declare identifier beginning with underscore");
}
.)
.
+// Identifier, disallowing leading underscores, except possibly the "wildcard" identifier "_"
+WildIdent<out IToken/*!*/ x, bool allowWildcardId>
+= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
+ ident (. x = t;
+ if (x.val.StartsWith("_")) {
+ if (allowWildcardId && x.val.Length == 1) {
+ t.val = "_v" + anonymousIds++;
+ } else {
+ SemErr("cannot declare identifier beginning with underscore");
+ }
+ }
+ .)
+ .
+
Nat<out BigInteger n>
=
digits
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 2d6d353c..39bfbdd3 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1279,6 +1279,9 @@ namespace Microsoft.Dafny {
string/*!*/ Name {
get;
}
+ string/*!*/ DisplayName { // what the user thinks he wrote
+ get;
+ }
string/*!*/ UniqueName {
get;
}
@@ -1303,6 +1306,12 @@ namespace Microsoft.Dafny {
throw new NotImplementedException();
}
}
+ public string DisplayName {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
+ throw new NotImplementedException();
+ }
+ }
public string UniqueName {
get {
Contract.Ensures(Contract.Result<string>() != null);
@@ -1350,6 +1359,9 @@ namespace Microsoft.Dafny {
return name;
}
}
+ public string/*!*/ DisplayName {
+ get { return VarDecl.DisplayNameHelper(this); }
+ }
readonly int varId = varIdCount++;
public string UniqueName {
get {
@@ -2224,6 +2236,14 @@ namespace Microsoft.Dafny {
return name;
}
}
+ public static string DisplayNameHelper(IVariable v) {
+ Contract.Requires(v != null);
+ string name = v.Name;
+ return name.StartsWith("_") ? "_" : name;
+ }
+ public string/*!*/ DisplayName {
+ get { return DisplayNameHelper(this); }
+ }
readonly int varId = NonglobalVariable.varIdCount++;
public string/*!*/ UniqueName {
get {
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index c422a619..46e17f7e 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -450,7 +450,7 @@ bool IsAttribute() {
Contract.Ensures(Contract.ValueAtReturn(out x) != null);
Expect(1);
x = t;
- if (x.val.Length > 0 && x.val.StartsWith("_")) {
+ if (x.val.StartsWith("_")) {
SemErr("cannot declare identifier beginning with underscore");
}
@@ -515,11 +515,11 @@ bool IsAttribute() {
while (la.kind == 6) {
Attribute(ref attrs);
}
- IdentType(out id, out ty);
+ IdentType(out id, out ty, false);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
while (la.kind == 24) {
Get();
- IdentType(out id, out ty);
+ IdentType(out id, out ty, false);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
while (!(la.kind == 0 || la.kind == 14)) {SynErr(123); Get();}
@@ -754,9 +754,9 @@ bool IsAttribute() {
Expect(28);
}
- void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {
+ void IdentType(out IToken/*!*/ id, out Type/*!*/ ty, bool allowWildcardId) {
Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
- NoUSIdent(out id);
+ WildIdent(out id, allowWildcardId);
Expect(5);
Type(out ty);
}
@@ -769,7 +769,21 @@ bool IsAttribute() {
Get();
if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); }
}
- IdentType(out id, out ty);
+ IdentType(out id, out ty, true);
+ }
+
+ void WildIdent(out IToken/*!*/ x, bool allowWildcardId) {
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null);
+ Expect(1);
+ x = t;
+ if (x.val.StartsWith("_")) {
+ if (allowWildcardId && x.val.Length == 1) {
+ t.val = "_v" + anonymousIds++;
+ } else {
+ SemErr("cannot declare identifier beginning with underscore");
+ }
+ }
+
}
void Type(out Type/*!*/ ty) {
@@ -780,7 +794,7 @@ bool IsAttribute() {
void LocalIdentTypeOptional(out VarDecl/*!*/ var, bool isGhost) {
IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
- NoUSIdent(out id);
+ WildIdent(out id, true);
if (la.kind == 5) {
Get();
Type(out ty);
@@ -792,7 +806,7 @@ bool IsAttribute() {
void IdentTypeOptional(out BoundVar/*!*/ var) {
Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
- NoUSIdent(out id);
+ WildIdent(out id, true);
if (la.kind == 5) {
Get();
Type(out ty);
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 7a84f86e..24941ce1 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -329,7 +329,7 @@ namespace Microsoft.Dafny {
wr.Write("ghost ");
}
if (f.HasName) {
- wr.Write("{0}: ", f.Name);
+ wr.Write("{0}: ", f.DisplayName);
}
PrintType(f.Type);
}
@@ -483,7 +483,7 @@ namespace Microsoft.Dafny {
if (s.IsGhost) {
wr.Write("ghost ");
}
- wr.Write("var {0}", s.Name);
+ wr.Write("var {0}", s.DisplayName);
PrintType(": ", s.OptionalType);
wr.Write(";");
@@ -571,7 +571,7 @@ namespace Microsoft.Dafny {
if (mc.Arguments.Count != 0) {
string sep = "(";
foreach (BoundVar bv in mc.Arguments) {
- wr.Write("{0}{1}", sep, bv.Name);
+ wr.Write("{0}{1}", sep, bv.DisplayName);
sep = ", ";
}
wr.Write(")");
@@ -605,7 +605,7 @@ namespace Microsoft.Dafny {
wr.Write("var ");
string sep = "";
foreach (var lhs in s.Lhss) {
- wr.Write("{0}{1}", sep, lhs.Name);
+ wr.Write("{0}{1}", sep, lhs.DisplayName);
PrintType(": ", lhs.OptionalType);
sep = ", ";
}
@@ -803,7 +803,7 @@ namespace Microsoft.Dafny {
if (mc.Arguments.Count != 0) {
string sep = "(";
foreach (BoundVar bv in mc.Arguments) {
- wr.Write("{0}{1}", sep, bv.Name);
+ wr.Write("{0}{1}", sep, bv.DisplayName);
sep = ", ";
}
wr.Write(")");
@@ -1134,7 +1134,7 @@ namespace Microsoft.Dafny {
wr.Write("var ");
string sep = "";
foreach (var v in e.Vars) {
- wr.Write("{0}{1}", sep, v.Name);
+ wr.Write("{0}{1}", sep, v.DisplayName);
PrintType(": ", v.Type);
sep = ", ";
}
@@ -1174,7 +1174,7 @@ namespace Microsoft.Dafny {
wr.Write("set ");
string sep = "";
foreach (BoundVar bv in e.BoundVars) {
- wr.Write("{0}{1}", sep, bv.Name);
+ wr.Write("{0}{1}", sep, bv.DisplayName);
sep = ", ";
PrintType(": ", bv.Type);
}
@@ -1194,7 +1194,7 @@ namespace Microsoft.Dafny {
wr.Write("map ");
string sep = "";
foreach (BoundVar bv in e.BoundVars) {
- wr.Write("{0}{1}", sep, bv.Name);
+ wr.Write("{0}{1}", sep, bv.DisplayName);
sep = ", ";
PrintType(": ", bv.Type);
}
@@ -1263,7 +1263,7 @@ namespace Microsoft.Dafny {
Contract.Requires(boundVars != null);
string sep = "";
foreach (BoundVar bv in boundVars) {
- wr.Write("{0}{1}", sep, bv.Name);
+ wr.Write("{0}{1}", sep, bv.DisplayName);
PrintType(": ", bv.Type);
sep = ", ";
}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
index 7aaf8944..c2362a72 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
@@ -294,7 +294,7 @@ namespace DafnyLanguage
Contract.Requires(tok != null);
Contract.Requires(v != null);
Start = tok.pos;
- Length = v.Name.Length;
+ Length = v.DisplayName.Length;
string kind;
if (v is VarDecl) {
kind = "local variable";
@@ -304,7 +304,7 @@ namespace DafnyLanguage
var formal = (Formal)v;
kind = formal.InParam ? "in-parameter" : "out-parameter";
}
- HoverText = string.Format("({2}{3}) {0}: {1}", v.Name, v.Type.TypeName(context), v.IsGhost ? "ghost " : "", kind);
+ HoverText = string.Format("({2}{3}) {0}: {1}", v.DisplayName, v.Type.TypeName(context), v.IsGhost ? "ghost " : "", kind);
IsDefinition = isDefinition;
}
private IdRegion(Bpl.IToken tok, Field decl, string kind, bool isDefinition, ModuleDefinition context) {
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 09:35:31 +0000