Improve trigger related warnings (#5000)

### Description
- Refactor trigger related code. Sorry for not having this be a separate
PR. I can still try to split it if that helps a lot.
- Add a section to the reference manual to help debug trigger related
warnings
- Improve diagnostics generated for triggers.
- Trigger generation related warnings now point to the relevant section
in the reference manual
  - Trigger generation related warnings now mention how to silence them
  - Splitting of quantifiers is reported more explicitly
- UI tweaks to the diagnostics, best inspected through the diff of the
expect files

### How has this been tested?
- Updated expect files of existing tests

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/Attributes.cs

@@ -235,7 +235,7 @@ public interface IAttributeBearingDeclaration {
   Attributes Attributes { get; }
 }
 
-public static class IAttributeBearingDeclarationExtensions {
+public static class AttributeBearingDeclarationExtensions {
   public static bool HasUserAttribute(this IAttributeBearingDeclaration decl, string name, out Attributes attribute) {
     if (Attributes.Find(decl.Attributes, name) is UserSuppliedAttributes attr) {
       attribute = attr;

Source/DafnyCore/AST/Expressions/Comprehensions/ForallExpr.cs

@@ -5,7 +5,7 @@ namespace Microsoft.Dafny;
 
 public class ForallExpr : QuantifierExpr, ICloneable<ForallExpr> {
   public override string WhatKind => "forall expression";
-  protected override BinaryExpr.ResolvedOpcode SplitResolvedOp { get { return BinaryExpr.ResolvedOpcode.And; } }
+  protected override BinaryExpr.ResolvedOpcode SplitResolvedOp => BinaryExpr.ResolvedOpcode.And;
 
   public ForallExpr(IToken tok, RangeToken rangeToken, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)
     : base(tok, rangeToken, bvars, range, term, attrs) {

Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs

@@ -11,7 +11,7 @@ public abstract class QuantifierExpr : ComprehensionExpr, TypeParameter.ParentTy
   private readonly int UniqueId;
   private static int currentQuantId = -1;
 
-  protected virtual BinaryExpr.ResolvedOpcode SplitResolvedOp { get { return BinaryExpr.ResolvedOpcode.Or; } }
+  protected virtual BinaryExpr.ResolvedOpcode SplitResolvedOp => BinaryExpr.ResolvedOpcode.Or;
 
   private Expression SplitQuantifierToExpression() {
     Contract.Requires(SplitQuantifier != null && SplitQuantifier.Any());

Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs

@@ -7,8 +7,7 @@ namespace Microsoft.Dafny;
 
 public class NestedMatchCaseExpr : NestedMatchCase, IAttributeBearingDeclaration {
   public Expression Body;
-  public Attributes Attributes;
-  Attributes IAttributeBearingDeclaration.Attributes => Attributes;
+  public Attributes Attributes { get; set; }
 
   public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Attributes attrs) : base(tok, pat) {
     Contract.Requires(body != null);

Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs

@@ -7,8 +7,7 @@ namespace Microsoft.Dafny;
 
 public class NestedMatchCaseStmt : NestedMatchCase, IAttributeBearingDeclaration, ICloneable<NestedMatchCaseStmt> {
   public readonly List<Statement> Body;
-  public Attributes Attributes;
-  Attributes IAttributeBearingDeclaration.Attributes => Attributes;
+  public Attributes Attributes { get; set; }
   public NestedMatchCaseStmt(RangeToken rangeToken, ExtendedPattern pat, List<Statement> body) : base(rangeToken.StartToken, pat) {
     RangeToken = rangeToken;
     Contract.Requires(body != null);

Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs

@@ -9,8 +9,7 @@ public class LetExpr : Expression, IAttributeBearingDeclaration, IBoundVarsBeari
   public readonly List<Expression> RHSs;
   public readonly Expression Body;
   public readonly bool Exact;  // Exact==true means a regular let expression; Exact==false means an assign-such-that expression
-  public readonly Attributes Attributes;
-  Attributes IAttributeBearingDeclaration.Attributes => Attributes;
+  public Attributes Attributes { get; set; }
   [FilledInDuringResolution] public List<ComprehensionExpr.BoundedPool> Constraint_Bounds;  // null for Exact=true and for when expression is in a ghost context
   // invariant Constraint_Bounds == null || Constraint_Bounds.Count == BoundVars.Count;
   private Expression translationDesugaring;  // filled in during translation, lazily; to be accessed only via Translation.LetDesugaring; always null when Exact==true

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -62,8 +62,7 @@ public string FullName {
   public readonly List<IToken> PrefixIds; // The qualified module name, except the last segment when a
                                           // nested module declaration is outside its enclosing module
   public ModuleDefinition EnclosingModule;  // readonly, except can be changed by resolver for prefix-named modules when the real parent is discovered
-  public readonly Attributes Attributes;
-  Attributes IAttributeBearingDeclaration.Attributes => Attributes;
+  public Attributes Attributes { get; set; }
   public readonly Implements Implements; // null if no refinement base
   public bool SuccessfullyResolved;  // set to true upon successful resolution; modules that import an unsuccessfully resolved module are not themselves resolved
   public readonly ModuleKindEnum ModuleKind;

Source/DafnyCore/AST/Statements/ControlFlow/GuardedAlternative.cs

@@ -8,10 +8,9 @@ public class GuardedAlternative : TokenNode, IAttributeBearingDeclaration {
   public readonly bool IsBindingGuard;
   public readonly Expression Guard;
   public readonly List<Statement> Body;
-  public Attributes Attributes;
+  public Attributes Attributes { get; set; }
   public override IEnumerable<INode> Children => (Attributes != null ? new List<Node> { Attributes } : Enumerable.Empty<Node>()).Concat(new List<Node>() { Guard }).Concat<Node>(Body);
   public override IEnumerable<INode> PreResolveChildren => Children;
-  Attributes IAttributeBearingDeclaration.Attributes => Attributes;
 
   [ContractInvariantMethod]
   void ObjectInvariant() {

Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs

@@ -374,7 +374,7 @@ private CaseBody CompileHeadsContainingConstructor(MatchCompilationState mti, Ma
       var freshMatchees = freshPatBV.ConvertAll(x => new IdentifierExpr(x.tok, x));
       // Update the current context
       var newContext = context.FillHole(new IdCtx(ctor));
-      var body = CompilePatternPaths(mti, newContext, LinkedLists.Concat(freshMatchees, remainingMatchees), constructorPaths);
+      var body = CompilePatternPaths(mti, newContext, LinkedLists.FromList(freshMatchees, remainingMatchees), constructorPaths);
       if (body is null) {
         // If no path matches this constructor, drop the case
         continue;

Source/DafnyCore/Generic/PredicateEqualityComparer.cs

@@ -0,0 +1,20 @@
+using System;
+using System.Collections.Generic;
+
+namespace DafnyCore.Generic;
+
+public class PredicateEqualityComparer<T> : IEqualityComparer<T> {
+  private readonly Func<T, T, bool> comparer;
+
+  public PredicateEqualityComparer(Func<T, T, bool> comparer) {
+    this.comparer = comparer;
+  }
+
+  public bool Equals(T a, T b) {
+    return comparer(a, b);
+  }
+
+  public int GetHashCode(T a) {
+    return a.GetHashCode();
+  }
+}

Source/DafnyCore/Generic/SinglyLinkedList.cs

@@ -38,20 +38,32 @@ public abstract record SinglyLinkedList<T> : IEnumerable<T> {
   IEnumerator IEnumerable.GetEnumerator() {
     return GetEnumerator();
   }
+
+  public bool Any() {
+    return this is not Nil<T>;
+  }
 }
 
 public static class LinkedLists {
-  public static SinglyLinkedList<T> Concat<T>(IEnumerable<T> left, SinglyLinkedList<T> right) {
-    SinglyLinkedList<T> result = right;
-    foreach (var value in left.Reverse()) {
-      result = new Cons<T>(value, result);
-    }
+  public static SinglyLinkedList<T> Concat<T>(SinglyLinkedList<T> left, SinglyLinkedList<T> right) {
+    return left switch {
+      Nil<T> => right,
+      Cons<T> cons => new Cons<T>(cons.Head, Concat<T>(cons.Tail, right)),
+      _ => throw new ArgumentOutOfRangeException(nameof(left))
+    };
+  }
+
 
+  public static SinglyLinkedList<T> FromList<T>(IReadOnlyList<T> values, SinglyLinkedList<T> tail = null) {
+    SinglyLinkedList<T> result = tail ?? new Nil<T>();
+    for (int i = values.Count - 1; i >= 0; i--) {
+      result = new Cons<T>(values[i], result);
+    }
     return result;
   }
 
   public static SinglyLinkedList<T> Create<T>(params T[] values) {
-    return Concat(values, new Nil<T>());
+    return FromList(values);
   }
 }
 

Source/DafnyCore/Rewriters/TriggerGeneratingRewriter.cs

@@ -19,7 +19,7 @@ internal override void PostCyclicityResolve(ModuleDefinition definition, ErrorRe
     var triggersCollector = new Triggers.TriggersCollector(finder.exprsInOldContext, Reporter.Options, definition);
     foreach (var quantifierCollection in finder.quantifierCollections) {
       quantifierCollection.ComputeTriggers(triggersCollector);
-      quantifierCollection.CommitTriggers(Reporter.Options, systemModuleManager);
+      quantifierCollection.CommitTriggers(systemModuleManager);
     }
   }
 }

Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs

@@ -0,0 +1,234 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Diagnostics.Contracts;
+using DafnyCore.Generic;
+
+namespace Microsoft.Dafny.Triggers {
+
+  record QuantifierGroup(SplitPartTriggerWriter Quantifier, List<ComprehensionExpr> Expressions);
+
+  /// <summary>
+  /// For a comprehension that has been split into parts, determine triggers for each part.
+  ///
+  /// See section 2.3 of "Trigger Selection Strategies to Stabilize Program Verifiers" to learn
+  /// why we introduce these splits, and what interaction there is between the generation of their triggers.
+  /// </summary>
+  class ComprehensionTriggerGenerator {
+    private readonly ErrorReporter reporter;
+    private readonly ComprehensionExpr comprehension;  //  the expression where the splits are originated from
+    private List<SplitPartTriggerWriter> partWriters;
+
+    internal ComprehensionTriggerGenerator(ComprehensionExpr comprehension, IEnumerable<ComprehensionExpr> quantifiers, ErrorReporter reporter) {
+      Contract.Requires(quantifiers.All(q => !(q is QuantifierExpr) || ((QuantifierExpr)q).SplitQuantifier == null));
+      this.reporter = reporter;
+      this.comprehension = comprehension;
+      partWriters = quantifiers.Select(q => new SplitPartTriggerWriter(q)).ToList();
+    }
+
+    internal void ComputeTriggers(TriggersCollector triggersCollector) {
+      CollectAndShareTriggers(triggersCollector);
+      TrimInvalidTriggers();
+      BuildDependenciesGraph();
+      if (DetectAndFilterLoopingCandidates() && RewriteMatchingLoop(triggersCollector.ForModule)) {
+        CollectWithoutShareTriggers(triggersCollector);
+        TrimInvalidTriggers();
+        DetectAndFilterLoopingCandidates();
+      }
+      FilterWeakerTriggers();
+      CombineSplitQuantifier();
+    }
+
+    private bool SubsetGenerationPredicate(TriggerTermSet terms, TriggerTerm additionalTerm) {
+      return true; // FIXME Remove this
+      //return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any();
+    }
+
+    /// <summary>
+    /// Collect triggers from the body of each quantifier, and share them
+    /// between all quantifiers. This method assumes that all quantifiers
+    /// actually come from the same context, and were the result of a split that
+    /// gave them all the same variables.
+    /// 
+    /// See section 2.1 of "Trigger Selection Strategies to Stabilize Program Verifiers" to learn
+    /// how we collect triggers
+    /// </summary>
+    void CollectAndShareTriggers(TriggersCollector triggersCollector) {
+      var pool = new List<TriggerTerm>();
+      foreach (var triggerWriter in partWriters) {
+        var candidates = triggersCollector.CollectTriggers(triggerWriter.Comprehension).Deduplicate(TriggerTerm.Eq);
+        var greatTerms = candidates.Where(term => !triggersCollector.TranslateToFunctionCall(term.Expr)).ToList();
+        if (greatTerms.Any()) {
+          // If we have great terms, only use those
+          candidates = greatTerms;
+        }
+        pool.AddRange(candidates);
+      }
+      var distinctPool = pool.Deduplicate(TriggerTerm.Eq);
+
+      foreach (var triggerWriter in partWriters) {
+        triggerWriter.CandidateTerms = distinctPool; // The list of candidate terms is immutable
+        triggerWriter.Candidates = TriggerTermSet.ComputeNonEmptyTriggerCandidatesTerms(LinkedLists.FromList(distinctPool), triggerWriter.Comprehension.BoundVars)
+          .Select(set => set.ToTriggerCandidate()).ToList();
+      }
+    }
+
+    void CollectWithoutShareTriggers(TriggersCollector triggersCollector) {
+      foreach (var triggerWriter in partWriters) {
+        var candidates = triggersCollector.CollectTriggers(triggerWriter.Comprehension).Deduplicate(TriggerTerm.Eq);
+        triggerWriter.CandidateTerms = candidates; // The list of candidate terms is immutable
+        triggerWriter.Candidates = TriggerTermSet.ComputeNonEmptyTriggerCandidatesTerms(
+          LinkedLists.FromList(candidates), triggerWriter.Comprehension.BoundVars).
+          Select(set => set.ToTriggerCandidate()).ToList();
+      }
+    }
+
+    private void TrimInvalidTriggers() {
+      foreach (var triggerWriter in partWriters) {
+        triggerWriter.TrimInvalidTriggers();
+      }
+    }
+
+    void BuildDependenciesGraph() {
+      // The problem of finding matching loops between multiple-triggers is hard; it
+      // seems to require one to track exponentially-sized dependencies between parts
+      // of triggers and quantifiers. For now, we only do single-quantifier loop
+      // detection
+    }
+
+    bool DetectAndFilterLoopingCandidates() {
+      // NOTE: This only looks for self-loops; that is, loops involving a single
+      // quantifier.
+
+      // For a given quantifier q, we introduce a triggering relation between trigger
+      // candidates by writing t1 → t2 if instantiating q from t1 introduces a ground
+      // term that matches t2. Then, we notice that this relation is transitive, since
+      // all triggers yield the same set of terms. This means that any matching loop
+      // t1 → ... → t1 can be reduced to a self-loop t1 → t1. Detecting such
+      // self-loops is then only a matter of finding terms in the body of the
+      // quantifier that match a given trigger.
+
+      // Of course, each trigger that actually appears in the body of the quantifier
+      // yields a trivial self-loop (e.g. P(i) in [∀ i {P(i)} ⋅ P(i)]), so we
+      // ignore this type of loops. In fact, we ignore any term in the body of the
+      // quantifier that matches one of the terms of the trigger (this ensures that
+      // [∀ x {f(x), f(f(x))} ⋅ f(x) = f(f(x))] is not a loop). And we even
+      // ignore terms that almost match a trigger term, modulo a single variable
+      // (this ensures that [∀ x y {a(x, y)} ⋅ a(x, y) == a(y, x)] is not a loop).
+
+      // In addition, we ignore cases where the only differences between a trigger
+      // and a trigger match are places where a variable is replaced with an
+      // expression whose free variables do not intersect that of the quantifier
+      // in which that expression is found. For examples of this behavious, see
+      // triggers/literals-do-not-cause-loops.
+      // This ignoring logic is implemented by the CouldCauseLoops method.
+      bool foundLoop = false;
+      foreach (var quantifier in partWriters) {
+        foundLoop |= quantifier.DetectAndFilterLoopingCandidates(reporter);
+      }
+      return foundLoop;
+    }
+
+    private bool RewriteMatchingLoop(ModuleDefinition module) {
+      if (comprehension is QuantifierExpr unSplitQuantifier) {
+        bool rewritten = false;
+        foreach (var triggerWriter in partWriters) {
+          rewritten |= triggerWriter.RewriteMatchingLoop(reporter, module);
+        }
+        if (rewritten) {
+          unSplitQuantifier.SplitQuantifier = partWriters.Select(q => (Expression)q.Comprehension).ToList();
+          return true;
+        }
+      }
+      return false;
+    }
+
+    void FilterWeakerTriggers() {
+      foreach (var triggerWriter in partWriters) {
+        triggerWriter.FilterStrongCandidates();
+      }
+    }
+
+    // group split quantifier by what triggers they got, and merged them back into one quantifier.
+    private void CombineSplitQuantifier() {
+      if (partWriters.Count > 1) {
+        var groups = new List<QuantifierGroup>();
+        groups.Add(new QuantifierGroup(partWriters[0], new List<ComprehensionExpr> { partWriters[0].Comprehension }));
+        for (int i = 1; i < partWriters.Count; i++) {
+          bool found = false;
+          for (int j = 0; j < groups.Count; j++) {
+            if (HasSameTriggers(partWriters[i], groups[j].Quantifier)) {
+              // belong to the same group
+              groups[j].Expressions.Add(partWriters[i].Comprehension);
+              found = true;
+              break;
+            }
+          }
+          if (!found) {
+            // start a new group
+            groups.Add(new QuantifierGroup(partWriters[i], new List<ComprehensionExpr> { partWriters[i].Comprehension }));
+          }
+        }
+        if (groups.Count == partWriters.Count) {
+          // have the same number of splits, so no splits are combined.
+          return;
+        }
+        // merge expressions in each group back to one quantifier.
+        List<SplitPartTriggerWriter> list = new List<SplitPartTriggerWriter>();
+        List<Expression> splits = new List<Expression>();
+        foreach (var group in groups) {
+          SplitPartTriggerWriter q = group.Quantifier;
+          if (q.Comprehension is ForallExpr forallExpr) {
+            IToken tok = forallExpr.tok is NestedToken nestedToken ? nestedToken.Outer : forallExpr.tok;
+            Expression expr = QuantifiersToExpression(tok, BinaryExpr.ResolvedOpcode.And, group.Expressions);
+            q.Comprehension = new ForallExpr(tok, forallExpr.RangeToken, forallExpr.BoundVars, forallExpr.Range, expr, TriggerUtils.CopyAttributes(forallExpr.Attributes)) { Type = forallExpr.Type, Bounds = forallExpr.Bounds };
+          } else if (q.Comprehension is ExistsExpr existsExpr) {
+            IToken tok = existsExpr.tok is NestedToken nestedToken ? nestedToken.Outer : existsExpr.tok;
+            Expression expr = QuantifiersToExpression(tok, BinaryExpr.ResolvedOpcode.Or, group.Expressions);
+            q.Comprehension = new ExistsExpr(tok, existsExpr.RangeToken, existsExpr.BoundVars, existsExpr.Range, expr, TriggerUtils.CopyAttributes(existsExpr.Attributes)) { Type = existsExpr.Type, Bounds = existsExpr.Bounds };
+          }
+          list.Add(q);
+          splits.Add(q.Comprehension);
+        }
+
+        partWriters = list;
+        Contract.Assert(this.comprehension is QuantifierExpr); // only QuantifierExpr has SplitQuantifier
+        ((QuantifierExpr)this.comprehension).SplitQuantifier = splits;
+      }
+    }
+
+    private bool HasSameTriggers(SplitPartTriggerWriter one, SplitPartTriggerWriter other) {
+      return one.Candidates.SequenceEqual(other.Candidates, new PredicateEqualityComparer<TriggerCandidate>(SameTriggerCandidate));
+    }
+
+    private static bool SameTriggerCandidate(TriggerCandidate arg1, TriggerCandidate arg2) {
+      Func<TriggerTerm, TriggerTerm, bool> comparer = TriggerTerm.Eq;
+      return arg1.Terms.SequenceEqual(arg2.Terms, new PredicateEqualityComparer<TriggerTerm>(comparer));
+    }
+
+    private Expression QuantifiersToExpression(IToken tok, BinaryExpr.ResolvedOpcode op, List<ComprehensionExpr> expressions) {
+      var expr = expressions[0].Term;
+      for (int i = 1; i < expressions.Count; i++) {
+        expr = new BinaryExpr(tok, op, expr, expressions[i].Term);
+      }
+      return expr;
+    }
+
+    internal void CommitTriggers(SystemModuleManager systemModuleManager) {
+      if (partWriters.Count > 1) {
+        reporter.Message(MessageSource.Rewriter, ErrorLevel.Info, null,
+          comprehension.Tok, $"Quantifier was split into {partWriters.Count} parts. " +
+           "Better verification performance and error reporting may be obtained by splitting the quantifier in source. " +
+           $"For more information, see the section quantifier instantiation rules in the reference manual.");
+      }
+
+      for (var index = 0; index < partWriters.Count; index++) {
+        var triggerWriter = partWriters[index];
+        triggerWriter.CommitTrigger(reporter, partWriters.Count > 1 ? index : null, systemModuleManager);
+      }
+    }
+  }
+}