Dafny: added Statement.SubExpressions getter

DafnyExtension: added hover text for identifiers

1 files changed, 92 insertions, 0 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 1c43a530..223e0b28 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1665,6 +1665,13 @@ namespace Microsoft.Dafny {
     public virtual IEnumerable<Statement> SubStatements {

       get { yield break; }

     }

+

+    /// <summary>

+    /// Returns the non-null expressions of this statement proper (that is, do not include the expressions of substatements).

+    /// </summary>

+    public virtual IEnumerable<Expression> SubExpressions {

+      get { yield break; }

+    }

   }

 

   public class LList<T>

@@ -1729,6 +1736,11 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr != null);

       this.Expr = expr;

     }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Expr;

+      }

+    }

   }

 

   public class AssertStmt : PredicateStmt {

@@ -1761,6 +1773,15 @@ namespace Microsoft.Dafny {
 

       Args = args;

     }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        foreach (var arg in Args) {

+          if (arg.E != null) {

+            yield return arg.E;

+          }

+        }

+      }

+    }

   }

 

   public class BreakStmt : Statement {

@@ -1795,6 +1816,15 @@ namespace Microsoft.Dafny {
       this.rhss = rhss;

       hiddenUpdate = null;

     }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        foreach (var rhs in rhss) {

+          foreach (var ee in rhs.SubExpressions) {

+            yield return ee;

+          }

+        }

+      }

+    }

   }

 

   public abstract class AssignmentRhs {

@@ -2103,6 +2133,15 @@ namespace Microsoft.Dafny {
       }

     }

 

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Lhs;

+        foreach (var ee in Rhs.SubExpressions) {

+          yield return ee;

+        }

+      }

+    }

+

     /// <summary>

     /// This method assumes "lhs" has been successfully resolved.

     /// </summary>

@@ -2221,6 +2260,18 @@ namespace Microsoft.Dafny {
       this.MethodName = methodName;

       this.Args = args;

     }

+

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        foreach (var ee in Lhs) {

+          yield return ee;

+        }

+        yield return Receiver;

+        foreach (var ee in Args) {

+          yield return ee;

+        }

+      }

+    }

   }

 

   public class BlockStmt : Statement {

@@ -2263,6 +2314,13 @@ namespace Microsoft.Dafny {
         }

       }

     }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        if (Guard != null) {

+          yield return Guard;

+        }

+      }

+    }

   }

 

   public class GuardedAlternative

@@ -2309,6 +2367,13 @@ namespace Microsoft.Dafny {
         }

       }

     }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        foreach (var alt in Alternatives) {

+          yield return alt.Guard;

+        }

+      }

+    }

   }

 

   public abstract class LoopStmt : Statement

@@ -2360,6 +2425,13 @@ namespace Microsoft.Dafny {
         yield return Body;

       }

     }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        if (Guard != null) {

+          yield return Guard;

+        }

+      }

+    }

   }

 

   /// <summary>

@@ -2401,6 +2473,13 @@ namespace Microsoft.Dafny {
         }

       }

     }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        foreach (var alt in Alternatives) {

+          yield return alt.Guard;

+        }

+      }

+    }

   }

 

   public class ParallelStmt : Statement

@@ -2482,6 +2561,14 @@ namespace Microsoft.Dafny {
         yield return Body;

       }

     }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Range;

+        foreach (var ee in Ens) {

+          yield return ee.E;

+        }

+      }

+    }

   }

 

   public class MatchStmt : Statement

@@ -2515,6 +2602,11 @@ namespace Microsoft.Dafny {
         }

       }

     }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Source;

+      }

+    }

   }

 

   public class MatchCaseStmt : MatchCase