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, 4 insertions, 3 deletions

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

     }