feat: Compute matching patterns for automatic induction

Source/DafnyCore/Rewriters/InductionRewriter.cs

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Linq;
 using JetBrains.Annotations;
 using static Microsoft.Dafny.RewriterErrors;
 
@@ -183,6 +184,23 @@ void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, E
     }
 
     if (inductionVariables.Count != 0) {
+      if (lemma != null) {
+        var triggers = ComputeInductionTriggers(inductionVariables, body, lemma.EnclosingClass.EnclosingModuleDefinition);
+        if (triggers.Count == 0) {
+          var msg = "omitting automatic induction because of lack of triggers";
+          if (args != null) {
+            Reporter.Warning(MessageSource.Rewriter, GenericErrors.ErrorId.none, tok, msg);
+          } else {
+            Reporter.Info(MessageSource.Rewriter, tok, msg);
+          }
+          return;
+        }
+
+        foreach (var trigger in triggers) {
+          attributes = new Attributes("_inductionPattern", trigger, attributes);
+        }
+      }
+
       // We found something usable, so let's record that in an attribute
       attributes = new Attributes("_induction", inductionVariables, attributes);
       // And since we're inferring something, let's also report that in a hover text.
@@ -195,6 +213,49 @@ void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, E
     }
   }
 
+  /// <summary>
+  /// Obtain and return matching patterns for
+  ///     (forall inductionVariables :: body)
+  /// If there aren't any, then return null.
+  /// </summary>
+  List<List<Expression>> ComputeInductionTriggers(List<Expression> inductionVariables, Expression body, ModuleDefinition moduleDefinition) {
+    Contract.Requires(inductionVariables.Count != 0);
+
+    // Construct a quantifier, because that's what the trigger-generating machinery expects.
+    // We start by creating a new BoundVar for each ThisExpr-or-IdentifierExpr in "inductionVariables".
+    var boundVars = new List<BoundVar>();
+    var substMap = new Dictionary<IVariable, Expression>();
+    var reverseSubstMap = new Dictionary<IVariable, Expression>();
+    Expression receiverReplacement = null;
+    foreach (var inductionVariableExpr in inductionVariables) {
+      var tok = inductionVariableExpr.tok;
+      BoundVar boundVar;
+      if (inductionVariableExpr is IdentifierExpr identifierExpr) {
+        boundVar = new BoundVar(tok, identifierExpr.Var.Name, identifierExpr.Var.Type);
+        substMap.Add(identifierExpr.Var, new IdentifierExpr(tok, boundVar));
+      } else {
+        Contract.Assert(inductionVariableExpr is ThisExpr);
+        boundVar = new BoundVar(tok, "this", inductionVariableExpr.Type);
+        receiverReplacement = new IdentifierExpr(tok, boundVar);
+      }
+      boundVars.Add(boundVar);
+      reverseSubstMap.Add(boundVar, inductionVariableExpr);
+    }
+
+    var substituter = new Substituter(receiverReplacement, substMap, new Dictionary<TypeParameter, Type>());
+    var quantifier = new ForallExpr(body.tok, body.RangeToken, boundVars, null, substituter.Substitute(body), null) {
+      Type = Type.Bool
+    };
+
+    var finder = new Triggers.QuantifierCollector(Reporter);
+    var triggersCollector = new Triggers.TriggersCollector(finder.exprsInOldContext, Reporter.Options, moduleDefinition);
+    var quantifierCollection = new Triggers.ComprehensionTriggerGenerator(quantifier, Enumerable.Repeat(quantifier, 1), Reporter);
+    quantifierCollection.ComputeTriggers(triggersCollector);
+    var triggers = quantifierCollection.GetTriggers();
+    var reverseSubstituter = new Substituter(null, reverseSubstMap, new Dictionary<TypeParameter, Type>());
+    return triggers.ConvertAll(trigger => trigger.ConvertAll(reverseSubstituter.Substitute));
+  }
+
   class InductionVisitor : BottomUpVisitor {
     readonly InductionRewriter IndRewriter;
 

Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs

@@ -230,5 +230,19 @@ internal void CommitTriggers(SystemModuleManager systemModuleManager) {
         triggerWriter.CommitTrigger(reporter, partWriters.Count > 1 ? index : null, systemModuleManager);
       }
     }
+
+    public List<List<Expression>> GetTriggers() {
+      var triggers = new List<List<Expression>>();
+      foreach (var triggerWriter in partWriters) {
+        foreach (var triggerTerms in triggerWriter.Candidates) {
+          var trigger = new List<Expression>();
+          foreach (var triggerTerm in triggerTerms.Terms) {
+            trigger.Add(triggerTerm.Expr);
+          }
+          triggers.Add(trigger);
+        }
+      }
+      return triggers;
+    }
   }
 }

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -782,14 +782,17 @@ private StmtList TrMethodBody(Method m, BoogieStmtListBuilder builder, Variables
             null, null, false, true);
         };
 
+        var triggers = Attributes.FindAllExpressions(m.Attributes, "_inductionPattern");
 #if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE
-          var definedness = new BoogieStmtListBuilder(this, options);
-          var exporter = new BoogieStmtListBuilder(this, options);
-          TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, null, recursiveCall, definedness, exporter, localVariables, etran);
-          // All done, so put the two pieces together
-          builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
+        var definedness = new BoogieStmtListBuilder(this, options, builder.Context);
+        var exporter = new BoogieStmtListBuilder(this, options, builder.Context);
+        TrForallStmtCall(m.tok, parBoundVars, parBounds, parRange, decrCheck, null, triggers, recursiveCall, definedness,
+          exporter, localVariables, etran);
+        // All done, so put the two pieces together
+        builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
 #else
-        TrForallStmtCall(m.tok, parBoundVars, parBounds, parRange, decrCheck, null, recursiveCall, null, builder, localVariables, etran);
+        TrForallStmtCall(m.tok, parBoundVars, parBounds, parRange, decrCheck, null, triggers, recursiveCall, null,
+          builder, localVariables, etran);
 #endif
       }
       // translate the body of the method

Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs

@@ -40,12 +40,14 @@ private void TrForallStmt(BoogieStmtListBuilder builder, Variables locals, Expre
       } else {
         var s0 = (CallStmt)forallStmt.S0;
         if (Attributes.Contains(forallStmt.Attributes, "_trustWellformed")) {
-          TrForallStmtCall(forallStmt.Tok, forallStmt.BoundVars, forallStmt.Bounds, forallStmt.Range, null, forallStmt.EffectiveEnsuresClauses, s0, null, builder, locals, etran);
+          TrForallStmtCall(forallStmt.Tok, forallStmt.BoundVars, forallStmt.Bounds, forallStmt.Range, null,
+            forallStmt.EffectiveEnsuresClauses, null, s0, null, builder, locals, etran);
         } else {
           var definedness = new BoogieStmtListBuilder(this, options, builder.Context);
           DefineFuelConstant(forallStmt.Tok, forallStmt.Attributes, definedness, etran);
           var exporter = new BoogieStmtListBuilder(this, options, builder.Context);
-          TrForallStmtCall(forallStmt.Tok, forallStmt.BoundVars, forallStmt.Bounds, forallStmt.Range, null, forallStmt.EffectiveEnsuresClauses, s0, definedness, exporter, locals, etran);
+          TrForallStmtCall(forallStmt.Tok, forallStmt.BoundVars, forallStmt.Bounds, forallStmt.Range, null,
+            forallStmt.EffectiveEnsuresClauses, null, s0, definedness, exporter, locals, etran);
           // All done, so put the two pieces together
           builder.Add(new Bpl.IfCmd(forallStmt.Tok, null, definedness.Collect(forallStmt.Tok), null, exporter.Collect(forallStmt.Tok)));
         }
@@ -71,13 +73,14 @@ private void TrForallStmt(BoogieStmtListBuilder builder, Variables locals, Expre
 
 
   void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, List<BoundedPool> bounds,
-    Expression range, ExpressionConverter additionalRange, List<Expression> forallExpressions, CallStmt s0,
+    Expression range, ExpressionConverter additionalRange, List<Expression> forallExpressions, List<List<Expression>> triggers, CallStmt s0,
     BoogieStmtListBuilder definedness, BoogieStmtListBuilder exporter, Variables locals, ExpressionTranslator etran) {
     Contract.Requires(tok != null);
     Contract.Requires(boundVars != null);
     Contract.Requires(bounds != null);
     Contract.Requires(range != null);
     // additionalRange is allowed to be null
+    Contract.Requires(forallExpressions == null || triggers == null || triggers.Count == 0);
     Contract.Requires(s0 != null);
     // definedness is allowed to be null
     Contract.Requires(exporter != null);
@@ -203,7 +206,18 @@ void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, List<BoundedPool> bo
           p = Substitute(ens.E, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents());  // substitute the call's actuals for the method's formals
           post = BplAnd(post, callEtran.TrExpr(p));
         }
+
         tr = null;
+        if (triggers != null) {
+          foreach (var trigger in triggers) {
+            Contract.Assert(trigger.Count != 0);
+            var terms = trigger.ConvertAll(expr => {
+              expr = Substitute(expr, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents());
+              return callEtran.TrExpr(expr);
+            });
+            tr = new Trigger(trigger[0].tok, true, terms, tr);
+          }
+        }
       }
 
       // TRIG (forall $ih#s0#0: Seq :: $Is($ih#s0#0, TSeq(TChar)) && $IsAlloc($ih#s0#0, TSeq(TChar), $initHeapForallStmt#0) && Seq#Length($ih#s0#0) != 0 && Seq#Rank($ih#s0#0) < Seq#Rank(s#0) ==> (forall i#2: int :: true ==> LitInt(0) <= i#2 && i#2 < Seq#Length($ih#s0#0) ==> char#ToInt(_module.CharChar.MinChar($LS($LZ), $Heap, this, $ih#s0#0)) <= char#ToInt($Unbox(Seq#Index($ih#s0#0, i#2)): char)))