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).

1 files changed, 6 insertions, 2 deletions

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));

     }