Print matches for triggers as they appear in the buffer

Triggers themselves, however, are printed exactly as used. For example, a term
(x !in s) yields a trigger (x in s).

3 files changed, 11 insertions, 6 deletions

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index a6340f10..49cd84df 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -118,7 +118,7 @@ namespace Microsoft.Dafny.Triggers {
           c => !loopingSubterms[c].Any(),

           c => {

             looping.Add(c);

-            c.Annotation = "loops with " + loopingSubterms[c].MapConcat(t => Printer.ExprToString(t.Expr), ", ");

+            c.Annotation = "loops with " + loopingSubterms[c].MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", ");

           }).ToList();

 

         q.CouldSuppressLoops = safe.Count > 0;

diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs
index a49ed13a..6c3f4ee7 100644
--- a/Source/Dafny/Triggers/TriggerExtensions.cs
+++ b/Source/Dafny/Triggers/TriggerExtensions.cs
@@ -24,6 +24,7 @@ namespace Microsoft.Dafny.Triggers {
 

   internal struct TriggerMatch {

     internal Expression Expr;

+    internal Expression OriginalExpr;

     internal Dictionary<IVariable, Expression> Bindings;

 

     internal static bool Eq(TriggerMatch t1, TriggerMatch t2) {

@@ -110,10 +111,10 @@ namespace Microsoft.Dafny.Triggers {
       return ShallowEq_Top(expr, trigger) && TriggerUtils.SameLists(expr.SubExpressions, trigger.SubExpressions, (e1, e2) => MatchesTrigger(e1, e2, holes, bindings));

     }

 

-    private static TriggerMatch? MatchAgainst(this Expression expr, Expression trigger, IEnumerable<BoundVar> holes) {

+    private static TriggerMatch? MatchAgainst(this Expression expr, Expression trigger, IEnumerable<BoundVar> holes, Expression originalExpr) {

       var bindings = new Dictionary<IVariable, Expression>();

       if (expr.MatchesTrigger(trigger, new HashSet<BoundVar>(holes), bindings)) {

-        return new TriggerMatch { Expr = expr, Bindings = bindings };

+        return new TriggerMatch { Expr = expr, OriginalExpr = originalExpr ?? expr, Bindings = bindings };

       } else {

         return null;

       }

@@ -121,7 +122,7 @@ namespace Microsoft.Dafny.Triggers {
 

     internal static IEnumerable<TriggerMatch> SubexpressionsMatchingTrigger(this QuantifierExpr quantifier, Expression trigger) {

       return quantifier.Term.AllSubExpressions()

-        .Select(e => TriggerUtils.CleanupExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars))

+        .Select(e => TriggerUtils.CleanupExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars, e))

         .Where(e => e.HasValue).Select(e => e.Value);

     }

 

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index 08d33af6..735baa01 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -13,7 +13,11 @@ namespace Microsoft.Dafny.Triggers {
     internal ISet<IVariable> Variables { get; set; }

 

     public override string ToString() {

-      return Printer.ExprToString(OriginalExpr);

+      return Printer.ExprToString(Expr); 

+      // NOTE: Using OriginalExpr here could cause some confusion: 

+      // for example, {a !in b} is a binary expression, yielding 

+      // trigger {a in b}. Saying the trigger is a !in b would be 

+      // rather misleading.

     }

 

     internal static bool Eq(TriggerTerm t1, TriggerTerm t2) {

@@ -45,7 +49,7 @@ namespace Microsoft.Dafny.Triggers {
 

     internal IEnumerable<TriggerMatch> LoopingSubterms(QuantifierExpr quantifier) {

       Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier

-      var matchingSubterms = MatchingSubterms(quantifier);

+      var matchingSubterms = this.MatchingSubterms(quantifier);

       return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms));

     }