diff options
| -rw-r--r-- | Source/Dafny/Resolver.cs | 96 | ||||
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 46 | ||||
| -rw-r--r-- | Source/DafnyExtension/IdentifierTagger.cs | 24 |
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;
|