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 +++--- 6 files changed, 100 insertions(+), 52 deletions(-) (limited to 'Source') 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; -- cgit v1.2.3