From fef3a31594c700f4846882a07d096eafaa4bd407 Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 15 Aug 2012 17:49:54 -0700 Subject: DafnyExtension: fixed more missing cases for hover texts --- Source/Dafny/Cloner.cs | 2 +- Source/Dafny/Dafny.atg | 19 ++-- Source/Dafny/DafnyAst.cs | 41 +++++++- Source/Dafny/Parser.cs | 18 ++-- Source/Dafny/Resolver.cs | 64 +++++------ Source/Dafny/Rewriter.cs | 8 +- .../DafnyExtension/IdentifierTagger.cs | 117 +++++++++++++-------- 7 files changed, 176 insertions(+), 93 deletions(-) diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 2f254135..b1b8828a 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -151,7 +151,7 @@ namespace Microsoft.Dafny } public FrameExpression CloneFrameExpr(FrameExpression frame) { - return new FrameExpression(CloneExpr(frame.E), frame.FieldName); + return new FrameExpression(Tok(frame.tok), CloneExpr(frame.E), frame.FieldName); } public Attributes.Argument CloneAttrArg(Attributes.Argument aa) { if (aa.E != null) { diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index d8d95079..1629fe51 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -18,7 +18,7 @@ static ModuleDecl theModule; static BuiltIns theBuiltIns; static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken); static AssignmentRhs/*!*/ dummyRhs = new ExprRhs(dummyExpr, null); -static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null); +static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null); static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null); static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg"); static int anonymousIds = 0; @@ -703,19 +703,24 @@ PossiblyWildFrameExpression * any use of the function. Nevertheless, as an experimental feature, the * language allows it (and it is sound). */ - ( "*" (. fe = new FrameExpression(new WildcardExpr(t), null); .) + ( "*" (. fe = new FrameExpression(t, new WildcardExpr(t), null); .) | FrameExpression ) . FrameExpression -= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; fe = null; .) - (( Expression - [ "`" Ident (. fieldName = id.val; .) += (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); + Expression/*!*/ e; + IToken/*!*/ id; + string fieldName = null; IToken feTok = null; + fe = null; + .) + (( Expression (. feTok = e.tok; .) + [ "`" Ident (. fieldName = id.val; feTok = id; .) ] - (. fe = new FrameExpression(e, fieldName); .) + (. fe = new FrameExpression(feTok, e, fieldName); .) ) | ( "`" Ident (. fieldName = id.val; .) - (. fe = new FrameExpression(new ImplicitThisExpr(id), fieldName); .) + (. fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); .) )) . FunctionBody diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index f342ecca..66ad49e9 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2075,6 +2075,14 @@ namespace Microsoft.Dafny { AssumeToken = assumeToken; } } + public override IEnumerable SubExpressions { + get { + yield return Expr; + foreach (var lhs in Lhss) { + yield return lhs; + } + } + } } public class UpdateStmt : ConcreteUpdateStatement @@ -2401,6 +2409,23 @@ namespace Microsoft.Dafny { this.Decreases = decreases; this.Mod = mod; } + public override IEnumerable SubExpressions { + get { + foreach (var mfe in Invariants) { + yield return mfe.E; + } + if (Decreases.Expressions != null) { + foreach (var e in Decreases.Expressions) { + yield return e; + } + } + if (Mod.Expressions != null) { + foreach (var fe in Mod.Expressions) { + yield return fe.E; + } + } + } + } } public class WhileStmt : LoopStmt @@ -2432,6 +2457,9 @@ namespace Microsoft.Dafny { if (Guard != null) { yield return Guard; } + foreach (var e in base.SubExpressions) { + yield return e; + } } } } @@ -2480,6 +2508,9 @@ namespace Microsoft.Dafny { foreach (var alt in Alternatives) { yield return alt.Guard; } + foreach (var e in base.SubExpressions) { + yield return e; + } } } } @@ -3962,6 +3993,7 @@ namespace Microsoft.Dafny { public class FrameExpression { + public readonly IToken tok; public readonly Expression E; // may be a WildcardExpr [ContractInvariantMethod] void ObjectInvariant() { @@ -3972,10 +4004,15 @@ namespace Microsoft.Dafny { public readonly string FieldName; public Field Field; // filled in during resolution (but is null if FieldName is) - public FrameExpression(Expression e, string fieldName) { + /// + /// If a "fieldName" is given, then "tok" denotes its source location. Otherwise, "tok" + /// denotes the source location of "e". + /// + public FrameExpression(IToken tok, Expression e, string fieldName) { + Contract.Requires(tok != null); Contract.Requires(e != null); Contract.Requires(!(e is WildcardExpr) || fieldName == null); - + this.tok = tok; E = e; FieldName = fieldName; } diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index a81b256e..2f49f689 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -38,7 +38,7 @@ static ModuleDecl theModule; static BuiltIns theBuiltIns; static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken); static AssignmentRhs/*!*/ dummyRhs = new ExprRhs(dummyExpr, null); -static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null); +static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null); static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null); static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg"); static int anonymousIds = 0; @@ -979,20 +979,26 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } void FrameExpression(out FrameExpression/*!*/ fe) { - Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; fe = null; + Contract.Ensures(Contract.ValueAtReturn(out fe) != null); + Expression/*!*/ e; + IToken/*!*/ id; + string fieldName = null; IToken feTok = null; + fe = null; + if (StartOf(10)) { Expression(out e); + feTok = e.tok; if (la.kind == 53) { Get(); Ident(out id); - fieldName = id.val; + fieldName = id.val; feTok = id; } - fe = new FrameExpression(e, fieldName); + fe = new FrameExpression(feTok, e, fieldName); } else if (la.kind == 53) { Get(); Ident(out id); fieldName = id.val; - fe = new FrameExpression(new ImplicitThisExpr(id), fieldName); + fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); } else SynErr(139); } @@ -1129,7 +1135,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; if (la.kind == 52) { Get(); - fe = new FrameExpression(new WildcardExpr(t), null); + fe = new FrameExpression(t, new WildcardExpr(t), null); } else if (StartOf(8)) { FrameExpression(out fe); } else SynErr(147); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index bf6dce17..c281aa4e 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -742,13 +742,13 @@ namespace Microsoft.Dafny return new Specification(ee, null); } FrameExpression CloneFrameExpr(FrameExpression frame) { - return new FrameExpression(CloneExpr(frame.E), frame.FieldName); + return new FrameExpression(frame.tok, CloneExpr(frame.E), frame.FieldName); } MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) { return new MaybeFreeExpression(CloneExpr(expr.E), expr.IsFree); } BoundVar CloneBoundVar(BoundVar bv) { - return new BoundVar((bv.tok), bv.Name, CloneType(bv.Type)); + return new BoundVar(bv.tok, bv.Name, CloneType(bv.Type)); } Expression CloneExpr(Expression expr) { if (expr == null) { @@ -756,37 +756,37 @@ namespace Microsoft.Dafny } else if (expr is LiteralExpr) { var e = (LiteralExpr)expr; if (e.Value == null) { - return new LiteralExpr((e.tok)); + return new LiteralExpr(e.tok); } else if (e.Value is bool) { - return new LiteralExpr((e.tok), (bool)e.Value); + return new LiteralExpr(e.tok, (bool)e.Value); } else { - return new LiteralExpr((e.tok), (BigInteger)e.Value); + return new LiteralExpr(e.tok, (BigInteger)e.Value); } } else if (expr is ThisExpr) { if (expr is ImplicitThisExpr) { - return new ImplicitThisExpr((expr.tok)); + return new ImplicitThisExpr(expr.tok); } else { - return new ThisExpr((expr.tok)); + return new ThisExpr(expr.tok); } } else if (expr is IdentifierExpr) { var e = (IdentifierExpr)expr; - return new IdentifierExpr((e.tok), e.Name); + return new IdentifierExpr(e.tok, e.Name); } else if (expr is DatatypeValue) { var e = (DatatypeValue)expr; - return new DatatypeValue((e.tok), e.DatatypeName, e.MemberName, e.Arguments.ConvertAll(CloneExpr)); + return new DatatypeValue(e.tok, e.DatatypeName, e.MemberName, e.Arguments.ConvertAll(CloneExpr)); } else if (expr is DisplayExpression) { DisplayExpression e = (DisplayExpression)expr; if (expr is SetDisplayExpr) { - return new SetDisplayExpr((e.tok), e.Elements.ConvertAll(CloneExpr)); + return new SetDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr)); } else if (expr is MultiSetDisplayExpr) { - return new MultiSetDisplayExpr((e.tok), e.Elements.ConvertAll(CloneExpr)); + return new MultiSetDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr)); } else { Contract.Assert(expr is SeqDisplayExpr); - return new SeqDisplayExpr((e.tok), e.Elements.ConvertAll(CloneExpr)); + return new SeqDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr)); } } else if (expr is MapDisplayExpr) { @@ -795,50 +795,50 @@ namespace Microsoft.Dafny foreach (ExpressionPair p in e.Elements) { pp.Add(new ExpressionPair(CloneExpr(p.A), CloneExpr(p.B))); } - return new MapDisplayExpr((expr.tok), pp); + return new MapDisplayExpr(expr.tok, pp); } else if (expr is ExprDotName) { var e = (ExprDotName)expr; - return new ExprDotName((e.tok), CloneExpr(e.Obj), e.SuffixName); + return new ExprDotName(e.tok, CloneExpr(e.Obj), e.SuffixName); } else if (expr is FieldSelectExpr) { var e = (FieldSelectExpr)expr; - return new FieldSelectExpr((e.tok), CloneExpr(e.Obj), e.FieldName); + return new FieldSelectExpr(e.tok, CloneExpr(e.Obj), e.FieldName); } else if (expr is SeqSelectExpr) { var e = (SeqSelectExpr)expr; - return new SeqSelectExpr((e.tok), e.SelectOne, CloneExpr(e.Seq), CloneExpr(e.E0), CloneExpr(e.E1)); + return new SeqSelectExpr(e.tok, e.SelectOne, CloneExpr(e.Seq), CloneExpr(e.E0), CloneExpr(e.E1)); } else if (expr is MultiSelectExpr) { var e = (MultiSelectExpr)expr; - return new MultiSelectExpr((e.tok), CloneExpr(e.Array), e.Indices.ConvertAll(CloneExpr)); + return new MultiSelectExpr(e.tok, CloneExpr(e.Array), e.Indices.ConvertAll(CloneExpr)); } else if (expr is SeqUpdateExpr) { var e = (SeqUpdateExpr)expr; - return new SeqUpdateExpr((e.tok), CloneExpr(e.Seq), CloneExpr(e.Index), CloneExpr(e.Value)); + return new SeqUpdateExpr(e.tok, CloneExpr(e.Seq), CloneExpr(e.Index), CloneExpr(e.Value)); } else if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; - return new FunctionCallExpr((e.tok), e.Name, CloneExpr(e.Receiver), e.OpenParen == null ? null : (e.OpenParen), e.Args.ConvertAll(CloneExpr)); + return new FunctionCallExpr(e.tok, e.Name, CloneExpr(e.Receiver), e.OpenParen == null ? null : (e.OpenParen), e.Args.ConvertAll(CloneExpr)); } else if (expr is OldExpr) { var e = (OldExpr)expr; - return new OldExpr((e.tok), CloneExpr(e.E)); + return new OldExpr(e.tok, CloneExpr(e.E)); } else if (expr is MultiSetFormingExpr) { var e = (MultiSetFormingExpr)expr; - return new MultiSetFormingExpr((e.tok), CloneExpr(e.E)); + return new MultiSetFormingExpr(e.tok, CloneExpr(e.E)); } else if (expr is FreshExpr) { var e = (FreshExpr)expr; - return new FreshExpr((e.tok), CloneExpr(e.E)); + return new FreshExpr(e.tok, CloneExpr(e.E)); } else if (expr is UnaryExpr) { var e = (UnaryExpr)expr; - return new UnaryExpr((e.tok), e.Op, CloneExpr(e.E)); + return new UnaryExpr(e.tok, e.Op, CloneExpr(e.E)); } else if (expr is BinaryExpr) { var e = (BinaryExpr)expr; - return new BinaryExpr((e.tok), e.Op, CloneExpr(e.E0), CloneExpr(e.E1)); + return new BinaryExpr(e.tok, e.Op, CloneExpr(e.E0), CloneExpr(e.E1)); } else if (expr is ChainingExpression) { var e = (ChainingExpression)expr; @@ -846,11 +846,11 @@ namespace Microsoft.Dafny } else if (expr is LetExpr) { var e = (LetExpr)expr; - return new LetExpr((e.tok), e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body)); + return new LetExpr(e.tok, e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body)); } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; - var tk = (e.tok); + var tk = e.tok; var bvs = e.BoundVars.ConvertAll(CloneBoundVar); var range = CloneExpr(e.Range); var term = CloneExpr(e.Term); @@ -866,20 +866,20 @@ namespace Microsoft.Dafny } } else if (expr is WildcardExpr) { - return new WildcardExpr((expr.tok)); + return new WildcardExpr(expr.tok); } else if (expr is PredicateExpr) { var e = (PredicateExpr)expr; if (e is AssertExpr) { - return new AssertExpr((e.tok), CloneExpr(e.Guard), CloneExpr(e.Body)); + return new AssertExpr(e.tok, CloneExpr(e.Guard), CloneExpr(e.Body)); } else { Contract.Assert(e is AssumeExpr); - return new AssumeExpr((e.tok), CloneExpr(e.Guard), CloneExpr(e.Body)); + return new AssumeExpr(e.tok, CloneExpr(e.Guard), CloneExpr(e.Body)); } } else if (expr is ITEExpr) { var e = (ITEExpr)expr; - return new ITEExpr((e.tok), CloneExpr(e.Test), CloneExpr(e.Thn), CloneExpr(e.Els)); + return new ITEExpr(e.tok, CloneExpr(e.Test), CloneExpr(e.Thn), CloneExpr(e.Els)); } else if (expr is ParensExpression) { var e = (ParensExpression)expr; @@ -892,8 +892,8 @@ namespace Microsoft.Dafny } else if (expr is MatchExpr) { var e = (MatchExpr)expr; - return new MatchExpr((e.tok), CloneExpr(e.Source), - e.Cases.ConvertAll(c => new MatchCaseExpr((c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body)))); + return new MatchExpr(e.tok, CloneExpr(e.Source), + e.Cases.ConvertAll(c => new MatchCaseExpr(c.tok, c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body)))); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 4dea968e..d88830a7 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -87,13 +87,13 @@ namespace Microsoft.Dafny if (member is Function && member.Name == "Valid" && !member.IsStatic) { var valid = (Function)member; // reads this; - valid.Reads.Add(new FrameExpression(new ThisExpr(tok), null)); + valid.Reads.Add(new FrameExpression(tok, new ThisExpr(tok), null)); // reads Repr; - valid.Reads.Add(new FrameExpression(new FieldSelectExpr(tok, new ImplicitThisExpr(tok), "Repr"), null)); + valid.Reads.Add(new FrameExpression(tok, new FieldSelectExpr(tok, new ImplicitThisExpr(tok), "Repr"), null)); } else if (member is Constructor) { var ctor = (Constructor)member; // modifies this; - ctor.Mod.Expressions.Add(new FrameExpression(new ImplicitThisExpr(tok), null)); + ctor.Mod.Expressions.Add(new FrameExpression(tok, new ImplicitThisExpr(tok), null)); // ensures Valid(); ctor.Ens.Insert(0, new MaybeFreeExpression(new FunctionCallExpr(tok, "Valid", new ImplicitThisExpr(tok), tok, new List()))); // ensures fresh(Repr - {this}); @@ -230,7 +230,7 @@ namespace Microsoft.Dafny var m = (Method)member; if (Valid != null && !IsSimpleQueryMethod(m)) { // modifies Repr; - m.Mod.Expressions.Add(new FrameExpression(Repr, null)); + m.Mod.Expressions.Add(new FrameExpression(Repr.tok, Repr, null)); // ensures Valid(); var valid = new FunctionCallExpr(tok, "Valid", implicitSelf, tok, new List()); valid.Function = Valid; diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs index bec65954..77a1fcf8 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs @@ -20,7 +20,7 @@ using Microsoft.VisualStudio.Text.Projection; using Microsoft.VisualStudio.Utilities; using System.Diagnostics.Contracts; using Bpl = Microsoft.Boogie; -using Dafny = Microsoft.Dafny; +using Microsoft.Dafny; namespace DafnyLanguage { @@ -47,7 +47,7 @@ namespace DafnyLanguage { ITextBuffer _buffer; ITextSnapshot _snapshot; // the most recent snapshot of _buffer that we have been informed about - Dafny.Program _program; // the program parsed from _snapshot + Microsoft.Dafny.Program _program; // the program parsed from _snapshot List _regions = new List(); // the regions generated from _program ITagAggregator _aggregator; @@ -104,7 +104,7 @@ namespace DafnyLanguage } } - bool ComputeIdentifierRegions(Dafny.Program program, ITextSnapshot snapshot) { + bool ComputeIdentifierRegions(Microsoft.Dafny.Program program, ITextSnapshot snapshot) { Contract.Requires(snapshot != null); if (program == _program) @@ -113,12 +113,12 @@ namespace DafnyLanguage List newRegions = new List(); foreach (var module in program.Modules) { - foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) { - if (!HasBodyTokens(d) && !(d is Dafny.ClassDecl)) { + foreach (var d in module.TopLevelDecls) { + if (!HasBodyTokens(d) && !(d is ClassDecl)) { continue; } - if (d is Dafny.DatatypeDecl) { - var dt = (Dafny.DatatypeDecl)d; + if (d is DatatypeDecl) { + var dt = (DatatypeDecl)d; foreach (var ctor in dt.Ctors) { foreach (var dtor in ctor.Destructors) { if (dtor != null) { @@ -126,26 +126,26 @@ namespace DafnyLanguage } } } - } else if (d is Dafny.ClassDecl) { - var cl = (Dafny.ClassDecl)d; + } else if (d is ClassDecl) { + var cl = (ClassDecl)d; foreach (var member in cl.Members) { if (!HasBodyTokens(member)) { continue; } - if (member is Dafny.Function) { - var f = (Dafny.Function)member; + if (member is Function) { + var f = (Function)member; foreach (var p in f.Formals) { newRegions.Add(new IdRegion(p.tok, p, true)); } f.Req.ForEach(e => ExprRegions(e, newRegions)); - f.Reads.ForEach(e => ExprRegions(e.E, newRegions)); + f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true)); f.Ens.ForEach(e => ExprRegions(e, newRegions)); f.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions)); if (f.Body != null) { ExprRegions(f.Body, newRegions); } - } else if (member is Dafny.Method) { - var m = (Dafny.Method)member; + } else if (member is Method) { + var m = (Method)member; foreach (var p in m.Ins) { newRegions.Add(new IdRegion(p.tok, p, true)); } @@ -153,14 +153,14 @@ namespace DafnyLanguage newRegions.Add(new IdRegion(p.tok, p, true)); } m.Req.ForEach(e => ExprRegions(e.E, newRegions)); - m.Mod.Expressions.ForEach(e => ExprRegions(e.E, newRegions)); + m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true)); m.Ens.ForEach(e => ExprRegions(e.E, newRegions)); m.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions)); if (m.Body != null) { StatementRegions(m.Body, newRegions); } - } else if (member is Dafny.Field) { - var fld = (Dafny.Field)member; + } else if (member is Field) { + var fld = (Field)member; newRegions.Add(new IdRegion(fld.tok, fld, "field", true)); } } @@ -173,27 +173,38 @@ namespace DafnyLanguage return true; } - static void ExprRegions(Dafny.Expression expr, List regions) { + static void FrameExprRegions(FrameExpression fe, List regions, bool descendIntoExpressions) { + Contract.Requires(fe != null); + Contract.Requires(regions != null); + if (descendIntoExpressions) { + ExprRegions(fe.E, regions); + } + if (fe.Field != null) { + regions.Add(new IdRegion(fe.tok, fe.Field, "field", false)); + } + } + + static void ExprRegions(Microsoft.Dafny.Expression expr, List regions) { Contract.Requires(expr != null); Contract.Requires(regions != null); - if (expr is Dafny.IdentifierExpr) { - var e = (Dafny.IdentifierExpr)expr; + if (expr is IdentifierExpr) { + var e = (IdentifierExpr)expr; regions.Add(new IdRegion(e.tok, e.Var, false)); - } else if (expr is Dafny.FieldSelectExpr) { - var e = (Dafny.FieldSelectExpr)expr; + } else if (expr is FieldSelectExpr) { + var e = (FieldSelectExpr)expr; regions.Add(new IdRegion(e.tok, e.Field, "field", false)); - } else if (expr is Dafny.ComprehensionExpr) { - var e = (Dafny.ComprehensionExpr)expr; + } else if (expr is ComprehensionExpr) { + var e = (ComprehensionExpr)expr; foreach (var bv in e.BoundVars) { regions.Add(new IdRegion(bv.tok, bv, true)); } - } else if (expr is Dafny.MatchExpr) { - var e = (Dafny.MatchExpr)expr; + } else if (expr is MatchExpr) { + var e = (MatchExpr)expr; foreach (var kase in e.Cases) { kase.Arguments.ForEach(bv => regions.Add(new IdRegion(bv.tok, bv, true))); } - } else if (expr is Dafny.ChainingExpression) { - var e = (Dafny.ChainingExpression)expr; + } else if (expr is ChainingExpression) { + var e = (ChainingExpression)expr; // Do the subexpressions only once (that is, avoid the duplication that occurs in the desugared form of the ChainingExpression) e.Operands.ForEach(ee => ExprRegions(ee, regions)); return; // return here, so as to avoid doing the subexpressions below @@ -203,20 +214,44 @@ namespace DafnyLanguage } } - static void StatementRegions(Dafny.Statement stmt, List regions) { + static void StatementRegions(Statement stmt, List regions) { Contract.Requires(stmt != null); Contract.Requires(regions != null); - if (stmt is Dafny.VarDecl) { - var s = (Dafny.VarDecl)stmt; + if (stmt is VarDeclStmt) { + var s = (VarDeclStmt)stmt; + // Add the variables here, once, and then go directly to the RHS's (without letting the sub-statements re-do the LHS's) + foreach (var lhs in s.Lhss) { + regions.Add(new IdRegion(lhs.Tok, lhs, true)); + } + if (s.Update is UpdateStmt) { + var upd = (UpdateStmt)s.Update; + foreach (var rhs in upd.Rhss) { + foreach (var ee in rhs.SubExpressions) { + ExprRegions(ee, regions); + } + } + } else { + var upd = (AssignSuchThatStmt)s.Update; + ExprRegions(upd.Expr, regions); + } + // we're done, so don't do the sub-statements/expressions again + return; + } else if (stmt is VarDecl) { + var s = (VarDecl)stmt; regions.Add(new IdRegion(s.Tok, s, true)); - } else if (stmt is Dafny.ParallelStmt) { - var s = (Dafny.ParallelStmt)stmt; + } else if (stmt is ParallelStmt) { + var s = (ParallelStmt)stmt; s.BoundVars.ForEach(bv => regions.Add(new IdRegion(bv.tok, bv, true))); - } else if (stmt is Dafny.MatchStmt) { - var s = (Dafny.MatchStmt)stmt; + } else if (stmt is MatchStmt) { + var s = (MatchStmt)stmt; foreach (var kase in s.Cases) { kase.Arguments.ForEach(bv => regions.Add(new IdRegion(bv.tok, bv, true))); } + } else if (stmt is LoopStmt) { + var s = (LoopStmt)stmt; + if (s.Mod.Expressions != null) { + s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false)); + } } foreach (var ee in stmt.SubExpressions) { ExprRegions(ee, regions); @@ -226,7 +261,7 @@ namespace DafnyLanguage } } - bool HasBodyTokens(Dafny.Declaration decl) { + bool HasBodyTokens(Declaration decl) { Contract.Requires(decl != null); return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken; } @@ -237,24 +272,24 @@ namespace DafnyLanguage public readonly int Length; public readonly string HoverText; public readonly bool IsDefinition; - public IdRegion(Bpl.IToken tok, Dafny.IVariable v, bool isDefinition) { + public IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition) { Contract.Requires(tok != null); Contract.Requires(v != null); Start = tok.pos; Length = v.Name.Length; string kind; - if (v is Dafny.VarDecl) { + if (v is VarDecl) { kind = "local variable"; - } else if (v is Dafny.BoundVar) { + } else if (v is BoundVar) { kind = "bound variable"; } else { - var formal = (Dafny.Formal)v; + var formal = (Formal)v; kind = formal.InParam ? "in-parameter" : "out-parameter"; } HoverText = string.Format("({2}{3}) {0}: {1}", v.Name, v.Type.ToString(), v.IsGhost ? "ghost " : "", kind); IsDefinition = isDefinition; } - public IdRegion(Bpl.IToken tok, Dafny.Field decl, string kind, bool isDefinition) { + public IdRegion(Bpl.IToken tok, Field decl, string kind, bool isDefinition) { Contract.Requires(tok != null); Contract.Requires(decl != null); Contract.Requires(kind != null); -- cgit v1.2.3