From 71b527bf4084763bb48c5c9fc44fc2ee456415d6 Mon Sep 17 00:00:00 2001 From: Unknown Date: Thu, 30 Aug 2012 14:07:34 -0700 Subject: Dafny: allow "_" as don't-care variable name --- Source/Dafny/Dafny.atg | 34 +++++++++++++++------- Source/Dafny/DafnyAst.cs | 20 +++++++++++++ Source/Dafny/Parser.cs | 30 ++++++++++++++----- Source/Dafny/Printer.cs | 18 ++++++------ .../DafnyExtension/IdentifierTagger.cs | 4 +-- 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/*!*/ mm.> (. if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); } .) { Attribute } - IdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .) - { "," IdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .) + IdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .) + { "," IdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .) } SYNC ";" . @@ -342,18 +342,18 @@ GIdentType + IdentType . -IdentType +IdentType = (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.) - NoUSIdent + WildIdent ":" Type . LocalIdentTypeOptional = (. IToken/*!*/ id; Type/*!*/ ty; Type optType = null; .) - NoUSIdent + WildIdent [ ":" Type (. optType = ty; .) ] (. var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .) @@ -361,7 +361,7 @@ LocalIdentTypeOptional IdentTypeOptional = (. Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id; Type/*!*/ ty; Type optType = null; .) - NoUSIdent + WildIdent [ ":" Type (. optType = ty; .) ] (. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .) @@ -399,10 +399,10 @@ GenericParameters<.List/*!*/ typeArgs.> TypeParameter.EqualitySupportValue eqSupport; .) "<" - NoUSIdent (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .) + NoUSIdent (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .) [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .) ] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .) - { "," NoUSIdent (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .) + { "," NoUSIdent (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .) [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .) ] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .) } @@ -1775,12 +1775,26 @@ Ident NoUSIdent = (. 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 += (. 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 = 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() != null); + throw new NotImplementedException(); + } + } public string UniqueName { get { Contract.Ensures(Contract.Result() != 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) { -- cgit v1.2.3