Implement the SelectTrigger method, removing redundant triggers.

The idea is that we define an partial order on triggers (which may contain
multiple terms), and find all the maximal elements. The algorithm as
implemented is rather inefficient; in particular, is does not look at the
structure of the graph of the relation (thus is does many redundant
comparisons). See triggers/useless-triggers-are-removed.dfy for an example
where such a filter is useful.

1 files changed, 6 insertions, 5 deletions

diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
index 9ebcf846..6f76464b 100644
--- a/Source/Dafny/Triggers/TriggerUtils.cs
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -76,13 +76,14 @@ namespace Microsoft.Dafny.Triggers {
       return it1_has == it2_has && acc;

     }

 

-    internal static IEnumerable<T> Filter<T>(IEnumerable<T> elements, Func<T, bool> predicate, Action<T> reject) {

+    internal static IEnumerable<T> Filter<T, U>(IEnumerable<T> elements, Func<T, U> Converter, Func<T, U, bool> predicate, Action<T, U> reject) {

       var positive = new List<T>();

-      foreach (var c in elements) {

-        if (predicate(c)) {

-          yield return c;

+      foreach (var elem in elements) {

+        var conv = Converter(elem);

+        if (predicate(elem, conv)) {

+          yield return elem;

         } else {

-          reject(c);

+          reject(elem, conv);

         }

       }

     }