1 files changed, 57 insertions, 0 deletions
diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs
new file mode 100644
index 00000000..cb2d5c6d
--- /dev/null
+++ b/Source/Dafny/Triggers/QuantifiersCollector.cs
@@ -0,0 +1,57 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Collections.ObjectModel;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Dafny.Triggers {
+  internal class QuantifierCollector : TopDownVisitor<bool> {
+    readonly ErrorReporter reporter;
+    private readonly HashSet<Expression> quantifiers = new HashSet<Expression>();
+    internal readonly HashSet<Expression> exprsInOldContext = new HashSet<Expression>();
+    internal readonly List<QuantifiersCollection> quantifierCollections = new List<QuantifiersCollection>();
+
+    public QuantifierCollector(ErrorReporter reporter) {
+      Contract.Requires(reporter != null);
+      this.reporter = reporter;
+    }
+
+    protected override bool VisitOneExpr(Expression expr, ref bool inOldContext) {
+      var quantifier = expr as QuantifierExpr;
+
+      // only consider quantifiers that are not empty (Bound.Vars.Count > 0)
+      if (quantifier != null && (quantifier.BoundVars.Count > 0) && !quantifiers.Contains(quantifier)) {
+        quantifiers.Add(quantifier);
+        if (quantifier.SplitQuantifier != null) {
+          var collection = quantifier.SplitQuantifier.Select(q => q as QuantifierExpr).Where(q => q != null);
+          quantifierCollections.Add(new QuantifiersCollection(collection, reporter));
+          quantifiers.UnionWith(quantifier.SplitQuantifier);
+        } else {
+          quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter));
+        }
+      }
+
+      if (expr is OldExpr) {
+        inOldContext = true;
+      } else if (inOldContext) { // FIXME be more restrctive on the type of stuff that we annotate
+        exprsInOldContext.Add(expr);
+      }
+
+      return true;
+    }
+
+    protected override bool VisitOneStmt(Statement stmt, ref bool st) {
+      if (stmt is ForallStmt) {
+        ForallStmt s = (ForallStmt)stmt;
+        if (s.ForallExpressions != null) {
+          foreach (Expression expr in s.ForallExpressions) {
+            VisitOneExpr(expr, ref st);
+          }
+        }
+      }
+      return true;
+    }
+  }
+}