Draft out a more advanced version of trigger generation

This new version will include a cleaner pipeline, and trigger splitting.

1 files changed, 94 insertions, 0 deletions

diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
new file mode 100644
index 00000000..5a118a2f
--- /dev/null
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -0,0 +1,94 @@
+#define DEBUG_AUTO_TRIGGERS

+

+using System;

+using System.Collections.Generic;

+using System.Diagnostics;

+using System.Diagnostics.Contracts;

+using System.Linq;

+using System.Text;

+

+namespace Microsoft.Dafny.Triggers {

+  class TriggerUtils {

+    internal static List<T> CopyAndAdd<T>(List<T> seq, T elem) {

+      var copy = new List<T>(seq);

+      copy.Add(elem);

+      return copy;

+    }

+

+    internal static IEnumerable<List<T>> AllSubsets<T>(IList<T> source, int offset) {

+      if (offset >= source.Count) {

+        yield return new List<T>();

+        yield break;

+      }

+

+      foreach (var subset in AllSubsets<T>(source, offset + 1)) {

+        yield return CopyAndAdd(subset, source[offset]);

+        yield return new List<T>(subset);

+      }

+    }

+

+    internal static IEnumerable<List<T>> AllNonEmptySubsets<T>(IEnumerable<T> source) {

+      List<T> all = new List<T>(source);

+      foreach (var subset in AllSubsets(all, 0)) {

+        if (subset.Count > 0) {

+          yield return subset;

+        }

+      }

+    }

+

+    internal static List<T> MergeAlterFirst<T>(List<T> a, List<T> b) {

+      Contract.Requires(a != null);

+      Contract.Requires(b != null);

+      a.AddRange(b);

+      return a;

+    }

+

+    internal static ISet<T> MergeAlterFirst<T>(ISet<T> a, ISet<T> b) {

+      Contract.Requires(a != null);

+      Contract.Requires(b != null);

+      a.UnionWith(b);

+      return a;

+    }

+

+    internal static bool SameLists<T>(IEnumerable<T> list1, IEnumerable<T> list2, Func<T, T, bool> comparer) {

+      if (ReferenceEquals(list1, list2)) {

+        return true;

+      } else if ((list1 == null) != (list2 == null)) {

+        return false;

+      }

+

+      var it1 = list1.GetEnumerator();

+      var it2 = list2.GetEnumerator();

+      bool it1_has, it2_has;

+      bool acc = true;

+

+      do {

+        it1_has = it1.MoveNext();

+        it2_has = it2.MoveNext();

+

+        if (it1_has == true && it2_has == true) {

+          acc = acc && comparer(it1.Current, it2.Current);

+        }

+      } while (it1_has && it2_has);

+

+      return it1_has == it2_has && acc;

+    }

+

+    internal static bool SameNullity<T>(T x1, T x2) where T : class {

+      return (x1 == null) == (x2 == null);

+    }

+

+    internal string JoinStringsWithHeader(string header, IEnumerable<string> lines) {

+      return header + String.Join(Environment.NewLine + new String(' ', header.Length), lines);

+    }

+

+    [Conditional("DEBUG_AUTO_TRIGGERS")]

+    internal static void DebugTriggers(string format, params object[] more) {

+      Console.Error.WriteLine(format, more);

+    }

+

+    internal static bool NeedsAutoTriggers(QuantifierExpr quantifier) {

+      return quantifier.Attributes.AsEnumerable().All(aa => aa.Name != "trigger" && aa.Name != "no_trigger");

+    }

+  }

+}