summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar qunyanm <unknown>2015-06-29 15:18:31 -0700
committerGravatar qunyanm <unknown>2015-06-29 15:18:31 -0700
commit3ca52e0f1bdc1ee0edfe19f774661bf02bf0e6b3 (patch)
treedf90b1988da3a2201a9f48f1dc5495dc31472275 /Source
parent9e0c60f26bc3c228447154f0d2f9cbeaee9c1974 (diff)
Fix identifiers in nested match patterns not showing in the IDE bug. Remember
BoundVars that are combined in rewriting of the nested match patterns so they show up in the IDE correctly.
Diffstat (limited to 'Source')
-rw-r--r--Source/Dafny/Resolver.cs96
-rw-r--r--Source/Dafny/Rewriter.cs46
-rw-r--r--Source/DafnyExtension/IdentifierTagger.cs24
3 files changed, 147 insertions, 19 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index ecb76ae8..835871d9 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -5244,7 +5244,8 @@ namespace Microsoft.Dafny
// convert CasePattern in MatchCaseExpr to BoundVar and flatten the MatchCaseExpr.
Type type = new InferredTypeProxy();
string name = FreshTempVarName("_mc#", codeContext);
- BoundVar bv = new BoundVar(s.Tok, name, type);
+ MatchCaseToken mcToken = new MatchCaseToken(s.Tok);
+ BoundVar bv = new BoundVar(mcToken, name, type);
List<CasePattern> patternSubst = new List<CasePattern>();
if (dtd != null) {
DesugarMatchCaseStmt(s, dtd, bv, patternSubst, codeContext);
@@ -5283,6 +5284,14 @@ namespace Microsoft.Dafny
Error(stmt, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
}
v.IsGhost = formal.IsGhost;
+
+ // update the type of the boundvars in the MatchCaseToken
+ if (v.tok is MatchCaseToken) {
+ MatchCaseToken mt = (MatchCaseToken)v.tok;
+ foreach (Tuple<IToken, BoundVar, bool> entry in mt.varList) {
+ UnifyTypes(entry.Item2.Type, v.Type);
+ }
+ }
}
i++;
}
@@ -5331,11 +5340,11 @@ namespace Microsoft.Dafny
* case (Suc(a), Suc(b)) => minus(a, b)
* To:
* match x
- * case Zero => match y
+ * case Zero => match y (originalToken)
* case _ => zero
- * case Suc(_) => match y
+ * case Suc(_) => match y (AutoGeneratedToken)
* case Zero => x
- * case Suc(a) => match y
+ * case Suc(a) => match y (AutoGeneratedToken)
* case (b) => minus(a,b)
*/
void DesugarMatchStmtWithTupleExpression(MatchStmt me) {
@@ -5347,6 +5356,9 @@ namespace Microsoft.Dafny
} else {
Expression source = e.Arguments[0];
List<MatchCaseStmt> cases = new List<MatchCaseStmt>();
+ // only keep the token for the first appearance, use autogenerated for the rest, otherwise more than one hovertext
+ // will show up in the IDE.
+ bool keepOrigToken = true;
foreach (MatchCaseStmt mc in me.Cases) {
if (mc.CasePatterns == null || mc.CasePatterns.Count != e.Arguments.Count) {
Error(mc.tok, "case arguments count does not match source arguments count");
@@ -5362,9 +5374,10 @@ namespace Microsoft.Dafny
List<Statement> body = mc.Body;
for (int i = e.Arguments.Count; 1 <= --i; ) {
// others go into the body
- body = CreateMatchCaseStmtBody(me.Tok, e.Arguments[i], mc.CasePatterns[i], body);
+ body = CreateMatchCaseStmtBody(me.Tok, e.Arguments[i], mc.CasePatterns[i], body, keepOrigToken);
}
cases.Add(new MatchCaseStmt(cp.tok, cp.Id, patterns, body));
+ keepOrigToken = false;
}
}
me.UpdateSource(source);
@@ -5373,7 +5386,7 @@ namespace Microsoft.Dafny
}
}
- List<Statement> CreateMatchCaseStmtBody(Boogie.IToken tok, Expression source, CasePattern cp, List<Statement> body) {
+ List<Statement> CreateMatchCaseStmtBody(Boogie.IToken tok, Expression source, CasePattern cp, List<Statement> body, bool keepToken) {
List<MatchCaseStmt> cases = new List<MatchCaseStmt>();
List<CasePattern> patterns;
if (cp.Var != null) {
@@ -5387,6 +5400,10 @@ namespace Microsoft.Dafny
patterns = cp.Arguments;
}
cases.Add(new MatchCaseStmt(cp.tok, cp.Id, patterns, body));
+ if (!keepToken) {
+ AutoGeneratedTokenCloner cloner = new AutoGeneratedTokenCloner();
+ source = cloner.CloneExpr(source);
+ }
List<Statement> list = new List<Statement>();
// endTok??
list.Add(new MatchStmt(tok, tok, source, cases, false));
@@ -5522,7 +5539,7 @@ namespace Microsoft.Dafny
// case Cons(y, #mc#) => match #mc#
// case Cons(z, zs) => body
- Expression source = new NameSegment(pat.tok, v.Name, null);
+ Expression source = new NameSegment(new AutoGeneratedToken(pat.tok), v.Name, null);
List<MatchCaseStmt> cases = new List<MatchCaseStmt>();
cases.Add(new MatchCaseStmt(pat.tok, pat.Id, pat.Arguments == null ? new List<CasePattern>() : pat.Arguments, mc.Body));
List<Statement> list = new List<Statement>();
@@ -5547,6 +5564,27 @@ namespace Microsoft.Dafny
foreach (MatchCaseStmt c in current.Cases) {
old.Cases.Add(c);
}
+ // add the token from mc to old_mc so the identifiers will show correctly in the IDE
+ List<BoundVar> arguments = new List<BoundVar>();
+ Contract.Assert(old_mc.Arguments.Count == mc.Arguments.Count);
+ for (int i = 0; i < old_mc.Arguments.Count; i++) {
+ var bv = old_mc.Arguments[i];
+ MatchCaseToken mcToken;
+ if (!(bv.tok is MatchCaseToken)) {
+ // create a MatchCaseToken
+ mcToken = new MatchCaseToken(bv.tok);
+ // clone the bv but with the MatchCaseToken
+ var bvNew = new BoundVar(mcToken, bv.Name, bv.Type);
+ bvNew.IsGhost = bv.IsGhost;
+ arguments.Add(bvNew);
+ } else {
+ mcToken = (MatchCaseToken)bv.tok;
+ arguments.Add(bv);
+ }
+ mcToken.AddVar(bv.tok, bv, true);
+ mcToken.AddVar(mc.Arguments[i].tok, mc.Arguments[i], true);
+ }
+ old_mc.Arguments = arguments;
thingsChanged = true;
}
} else {
@@ -5596,7 +5634,9 @@ namespace Microsoft.Dafny
// what if match body already has the bv?? need to make a new bv
Type type = new InferredTypeProxy();
string name = FreshTempVarName("_mc#", codeContext);
- BoundVar bv = new BoundVar(one.tok, name, type);
+ BoundVar bv = new BoundVar(new MatchCaseToken(one.tok), name, type);
+ ((MatchCaseToken)bv.tok).AddVar(bv1.tok, bv1, true);
+ ((MatchCaseToken)bv.tok).AddVar(bv2.tok, bv2, true);
SubstituteMatchCaseBoundVar(one, bv1, bv);
SubstituteMatchCaseBoundVar(other, bv2, bv);
}
@@ -7708,7 +7748,7 @@ namespace Microsoft.Dafny
// convert CasePattern in MatchCaseExpr to BoundVar and flatten the MatchCaseExpr.
Type type = new InferredTypeProxy();
string name = FreshTempVarName("_mc#", opts.codeContext);
- BoundVar bv = new BoundVar(me.tok, name, type);
+ BoundVar bv = new BoundVar(new MatchCaseToken(me.tok), name, type);
List<CasePattern> patternSubst = new List<CasePattern>();
if (dtd != null) {
DesugarMatchCaseExpr(me, dtd, bv, patternSubst, opts.codeContext);
@@ -7748,6 +7788,14 @@ namespace Microsoft.Dafny
Error(expr, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
}
v.IsGhost = formal.IsGhost;
+
+ // update the type of the boundvars in the MatchCaseToken
+ if (v.tok is MatchCaseToken) {
+ MatchCaseToken mt = (MatchCaseToken)v.tok;
+ foreach (Tuple<IToken, BoundVar, bool> entry in mt.varList) {
+ UnifyTypes(entry.Item2.Type, v.Type);
+ }
+ }
}
i++;
}
@@ -7945,7 +7993,7 @@ namespace Microsoft.Dafny
// case Cons(y, #mc#) => match #mc#
// case Cons(z, zs) => body
- Expression source = new NameSegment(pat.tok, v.Name, null);
+ Expression source = new NameSegment(new AutoGeneratedToken(pat.tok), v.Name, null);
List<MatchCaseExpr> cases = new List<MatchCaseExpr>();
cases.Add(new MatchCaseExpr(pat.tok, pat.Id, pat.Arguments == null ? new List<CasePattern>() : pat.Arguments, mc.Body));
MatchExpr e = new MatchExpr(pat.tok, source, cases, false);
@@ -7975,6 +8023,27 @@ namespace Microsoft.Dafny
foreach (MatchCaseExpr c in current.Cases) {
old.Cases.Add(c);
}
+ // add the token from mc to old_mc so the identifiers will show correctly in the IDE
+ List<BoundVar> arguments = new List<BoundVar>();
+ Contract.Assert(old_mc.Arguments.Count == mc.Arguments.Count);
+ for (int i = 0; i < old_mc.Arguments.Count; i++) {
+ var bv = old_mc.Arguments[i];
+ MatchCaseToken mcToken;
+ if (!(bv.tok is MatchCaseToken)) {
+ // create a MatchCaseToken
+ mcToken = new MatchCaseToken(bv.tok);
+ // clone the bv but with the MatchCaseToken
+ var bvNew = new BoundVar(mcToken, bv.Name, bv.Type);
+ bvNew.IsGhost = bv.IsGhost;
+ arguments.Add(bvNew);
+ } else {
+ mcToken = (MatchCaseToken)bv.tok;
+ arguments.Add(bv);
+ }
+ mcToken.AddVar(bv.tok, bv, true);
+ mcToken.AddVar(mc.Arguments[i].tok, mc.Arguments[i], true);
+ }
+ old_mc.Arguments = arguments;
thingsChanged = true;
} else {
// duplicate cases, do nothing for now. The error will be reported during resolving
@@ -7987,6 +8056,7 @@ namespace Microsoft.Dafny
return thingsChanged;
}
+
bool SameMatchCaseExpr(MatchCaseExpr one, MatchCaseExpr other, ICodeContext codeContext) {
// this method is called after all the CasePattern in the match cases are converted
// into BoundVars.
@@ -8018,7 +8088,11 @@ namespace Microsoft.Dafny
// what if match body already has the bv?? need to make a new bv
Type type = new InferredTypeProxy();
string name = FreshTempVarName("_mc#", codeContext);
- BoundVar bv = new BoundVar(one.tok, name, type);
+ MatchCaseToken mcToken = new MatchCaseToken(one.tok);
+ BoundVar bv = new BoundVar(mcToken, name, type);
+ mcToken.AddVar(bv1.tok, bv1, true);
+ mcToken.AddVar(bv2.tok, bv2, true);
+ // substitute the appeareance of old bv with the new bv in the match case
SubstituteMatchCaseBoundVar(one, bv1, bv);
SubstituteMatchCaseBoundVar(other, bv2, bv);
}
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 1dd985cb..9eb6bac2 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -2,6 +2,7 @@
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using Bpl = Microsoft.Boogie;
+using IToken = Microsoft.Boogie.IToken;
namespace Microsoft.Dafny
{
@@ -1140,10 +1141,10 @@ namespace Microsoft.Dafny
}
public override BoundVar CloneBoundVar(BoundVar bv) {
- // replace bv with this.var is bv == oldvar
+ // replace bv with this.var if bv == oldvar
BoundVar bvNew;
if (oldvar != null && bv.Name.Equals(oldvar.Name)) {
- bvNew = new BoundVar(Tok(bv.tok), oldvar.Name, CloneType(bv.Type));
+ bvNew = new BoundVar(new AutoGeneratedToken(bv.tok), var.Name, CloneType(bv.Type));
} else {
bvNew = new BoundVar(Tok(bv.tok), bv.Name, CloneType(bv.Type));
}
@@ -1154,7 +1155,7 @@ namespace Microsoft.Dafny
public override NameSegment CloneNameSegment(Expression expr) {
var e = (NameSegment)expr;
if (oldvar != null && e.Name.Equals(oldvar.Name)) {
- return new NameSegment(Tok(e.tok), var.Name, e.OptTypeArguments == null ? null : e.OptTypeArguments.ConvertAll(CloneType));
+ return new NameSegment(new AutoGeneratedToken(e.tok), var.Name, e.OptTypeArguments == null ? null : e.OptTypeArguments.ConvertAll(CloneType));
} else {
return new NameSegment(Tok(e.tok), e.Name, e.OptTypeArguments == null ? null : e.OptTypeArguments.ConvertAll(CloneType));
}
@@ -1162,14 +1163,22 @@ namespace Microsoft.Dafny
public override Expression CloneApplySuffix(ApplySuffix e) {
// if the ApplySuffix matches the CasePattern, then replace it with the BoundVar.
- if (FindMatchingPattern(e)) {
- return new NameSegment(e.tok, this.var.Name, null);
+ CasePattern cp = null;
+ if (FindMatchingPattern(e, out cp)) {
+ if (this.var.tok is MatchCaseToken) {
+ Contract.Assert(e.Args.Count == cp.Arguments.Count);
+ for (int i = 0; i < e.Args.Count; i++) {
+ ((MatchCaseToken)this.var.tok).AddVar(e.Args[i].tok, cp.Arguments[i].Var, false);
+ }
+ }
+ return new NameSegment(new AutoGeneratedToken(e.tok), this.var.Name, null);
} else {
return new ApplySuffix(Tok(e.tok), CloneExpr(e.Lhs), e.Args.ConvertAll(CloneExpr));
}
}
- private bool FindMatchingPattern(ApplySuffix e) {
+ private bool FindMatchingPattern(ApplySuffix e, out CasePattern pattern) {
+ pattern = null;
if (patternSubst == null) {
return false;
}
@@ -1197,12 +1206,37 @@ namespace Microsoft.Dafny
}
}
if (found) {
+ pattern = cp;
return true;
}
}
return false;
}
}
+
+ // MatchCaseToken is used to record BoundVars that are consolidated due to rewrite of
+ // nested match patterns. We want to record the original BoundVars that are consolidated
+ // so that they will show up in the IDE correctly.
+ public class MatchCaseToken : AutoGeneratedToken
+ {
+ public readonly List<Tuple<IToken, BoundVar, bool>> varList;
+ public MatchCaseToken(IToken tok)
+ : base(tok) {
+ varList = new List<Tuple<IToken, BoundVar, bool>>();
+ }
+
+ public void AddVar(IToken tok, BoundVar var, bool isDefinition) {
+ varList.Add(new Tuple<IToken, BoundVar, bool>(tok, var, isDefinition));
+ }
+ }
+
+ // A cloner that replace the original token with AutoGeneratedToken.
+ class AutoGeneratedTokenCloner : Cloner
+ {
+ public override IToken Tok(IToken tok) {
+ return new AutoGeneratedToken(tok);
+ }
+ }
}
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 086ac8e4..262dddcd 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -270,7 +270,17 @@ namespace DafnyLanguage
} else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
foreach (var kase in e.Cases) {
- kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
+ kase.Arguments.ForEach(bv => {
+ IdRegion.Add(regions, bv.tok, bv, true, module);
+ // if the arguments is an encapsulation of different boundvars from nested match cases,
+ // add the boundvars so that they can show up in the IDE correctly
+ if (bv.tok is MatchCaseToken) {
+ MatchCaseToken mt = (MatchCaseToken)bv.tok;
+ foreach(Tuple<Bpl.IToken, BoundVar, bool> entry in mt.varList) {
+ IdRegion.Add(regions, entry.Item1, entry.Item2, entry.Item3, module);
+ }
+ }
+ });
}
} else if (expr is ChainingExpression) {
var e = (ChainingExpression)expr;
@@ -313,7 +323,17 @@ namespace DafnyLanguage
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
foreach (var kase in s.Cases) {
- kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
+ kase.Arguments.ForEach(bv => {
+ IdRegion.Add(regions, bv.tok, bv, true, module);
+ // if the arguments is an encapsulation of different boundvars from nested match cases,
+ // add the boundvars so that they can show up in the IDE correctly
+ if (bv.tok is MatchCaseToken) {
+ MatchCaseToken mt = (MatchCaseToken)bv.tok;
+ foreach (Tuple<Bpl.IToken, BoundVar, bool> entry in mt.varList) {
+ IdRegion.Add(regions, entry.Item1, entry.Item2, entry.Item3, module);
+ }
+ }
+ });
}
} else if (stmt is LoopStmt) {
var s = (LoopStmt)stmt;