feat: Compute matching patterns for automatic induction

Source/DafnyCore/AST/ExtremeCloner.cs

@@ -17,7 +17,7 @@ protected ExtremeCloner(Expression k, ErrorReporter reporter) {
     Contract.Requires(reporter != null);
     this.k = k;
     this.reporter = reporter;
-    this.suffix = string.Format("#[{0}]", Printer.ExprToString(reporter.Options, k));
+    this.suffix = $"#[{Printer.ExprToString(reporter.Options, k)}]";
   }
   protected Expression CloneCallAndAddK(ApplySuffix e) {
     Contract.Requires(e != null);
@@ -63,4 +63,16 @@ protected Expression CloneCallAndAddK(FunctionCallExpr e) {
     reporter.Info(MessageSource.Cloner, e.tok, e.Name + suffix);
     return fexp;
   }
+
+  protected Expression CloneEqualityAndAndK(BinaryExpr binaryExpr) {
+    if (this.CloneResolvedFields) {
+      throw new NotImplementedException();
+    }
+
+    var eq = new TernaryExpr(Tok(binaryExpr.tok),
+      binaryExpr.ResolvedOp == BinaryExpr.ResolvedOpcode.EqCommon ? TernaryExpr.Opcode.PrefixEqOp : TernaryExpr.Opcode.PrefixNeqOp,
+      k, CloneExpr(binaryExpr.E0), CloneExpr(binaryExpr.E1));
+    reporter.Info(MessageSource.Cloner, binaryExpr.tok, "==" + suffix);
+    return eq;
+  }
 }

Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs

@@ -11,99 +11,78 @@ namespace Microsoft.Dafny;
 class ExtremeLemmaBodyCloner : ExtremeCloner {
   readonly ExtremeLemma context;
   readonly ISet<ExtremePredicate> focalPredicates;
-  public ExtremeLemmaBodyCloner(ExtremeLemma context, Expression k, ISet<ExtremePredicate> focalPredicates, ErrorReporter reporter)
+  readonly ISet<CoDatatypeDecl> focalCodatatypeEquality;
+  public ExtremeLemmaBodyCloner(ExtremeLemma context, Expression k,
+    ISet<ExtremePredicate> focalPredicates, ISet<CoDatatypeDecl> focalCodatatypeEquality, ErrorReporter reporter)
     : base(k, reporter) {
     Contract.Requires(context != null);
     Contract.Requires(k != null);
     Contract.Requires(reporter != null);
     this.context = context;
     this.focalPredicates = focalPredicates;
+    this.focalCodatatypeEquality = focalCodatatypeEquality;
   }
 
   public override Expression CloneExpr(Expression expr) {
     if (reporter.Options.RewriteFocalPredicates) {
-      if (expr is FunctionCallExpr) {
-        var e = (FunctionCallExpr)expr;
-#if DEBUG_PRINT
-          if (e.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => e.Function.Name == p.Name + "#")) {
-            Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(e));
-          }
-#endif
+      if (expr is FunctionCallExpr functionCallExpr) {
         // Note, we don't actually ever get here, because all calls will have been parsed as ApplySuffix.
         // However, if something changes in the future (for example, some rewrite that changing an ApplySuffix
         // to its resolved FunctionCallExpr), then we do want this code, so with the hope of preventing
         // some error in the future, this case is included.  (Of course, it is currently completely untested!)
-        var f = e.Function as ExtremePredicate;
-        if (f != null && focalPredicates.Contains(f)) {
-#if DEBUG_PRINT
-            var r = CloneCallAndAddK(e);
-            Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(r));
-            return r;
-#else
-          return CloneCallAndAddK(e);
-#endif
+        if (functionCallExpr.Function is ExtremePredicate f && focalPredicates.Contains(f)) {
+          return CloneCallAndAddK(functionCallExpr);
         }
       } else if (expr is StaticReceiverExpr ee) {
         return new StaticReceiverExpr(Tok(ee.tok), ee.Type, ee.IsImplicit);
-      } else if (expr is ApplySuffix) {
-        var apply = (ApplySuffix)expr;
+      } else if (expr is ApplySuffix apply) {
         if (!apply.WasResolved()) {
           // Since we're assuming the enclosing statement to have been resolved, this ApplySuffix must
           // be part of an ExprRhs that actually designates a method call.  Such an ApplySuffix does
           // not get listed as being resolved, but its components (like its .Lhs) are resolved.
           var mse = (MemberSelectExpr)apply.Lhs.Resolved;
           Contract.Assume(mse.Member is Method);
         } else {
-          var fce = apply.Resolved as FunctionCallExpr;
-          if (fce != null) {
-#if DEBUG_PRINT
-              if (fce.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => fce.Function.Name == p.Name + "#")) {
-                Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(fce));
-              }
-#endif
-            var f = fce.Function as ExtremePredicate;
-            if (f != null && focalPredicates.Contains(f)) {
-#if DEBUG_PRINT
-                var r = CloneCallAndAddK(fce);
-                Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(r));
-                return r;
-#else
+          if (apply.Resolved is FunctionCallExpr fce) {
+            if (fce.Function is ExtremePredicate f && focalPredicates.Contains(f)) {
               return CloneCallAndAddK(fce);
-#endif
             }
           }
         }
+      } else if (expr is BinaryExpr { ResolvedOp: BinaryExpr.ResolvedOpcode.EqCommon or BinaryExpr.ResolvedOpcode.NeqCommon } binaryExpr) {
+        if (binaryExpr.E0.Type.AsCoDatatype is { } coDatatypeDecl && focalCodatatypeEquality.Contains(coDatatypeDecl)) {
+          return CloneEqualityAndAndK(binaryExpr);
+        }
       }
     }
     return base.CloneExpr(expr);
   }
   public override AssignmentRhs CloneRHS(AssignmentRhs rhs) {
-    var r = rhs as ExprRhs;
-    if (r != null && r.Expr is ApplySuffix) {
-      var apply = (ApplySuffix)r.Expr;
-      var mse = apply.Lhs.Resolved as MemberSelectExpr;
-      if (mse != null && mse.Member is ExtremeLemma && ModuleDefinition.InSameSCC(context, (ExtremeLemma)mse.Member)) {
+    if (rhs is ExprRhs { Expr: ApplySuffix apply }) {
+      if (apply.Lhs.Resolved is MemberSelectExpr { Member: ExtremeLemma extremeLemma } && ModuleDefinition.InSameSCC(context, extremeLemma)) {
         // we're looking at a recursive call to an extreme lemma
-        Contract.Assert(apply.Lhs is NameSegment || apply.Lhs is ExprDotName);  // this is the only way a call statement can have been parsed
+        Contract.Assert(apply.Lhs is NameSegment or ExprDotName); // this is the only way a call statement can have been parsed
         // clone "apply.Lhs", changing the least/greatest lemma to the prefix lemma; then clone "apply", adding in the extra argument
         Expression lhsClone;
         if (apply.Lhs is NameSegment) {
           var lhs = (NameSegment)apply.Lhs;
-          lhsClone = new NameSegment(Tok(lhs.tok), lhs.Name + "#", lhs.OptTypeArguments == null ? null : lhs.OptTypeArguments.ConvertAll(CloneType));
+          lhsClone = new NameSegment(Tok(lhs.tok), lhs.Name + "#", lhs.OptTypeArguments?.ConvertAll(CloneType));
         } else {
           var lhs = (ExprDotName)apply.Lhs;
-          lhsClone = new ExprDotName(Tok(lhs.tok), CloneExpr(lhs.Lhs), lhs.SuffixName + "#", lhs.OptTypeArguments == null ? null : lhs.OptTypeArguments.ConvertAll(CloneType));
+          lhsClone = new ExprDotName(Tok(lhs.tok), CloneExpr(lhs.Lhs), lhs.SuffixName + "#", lhs.OptTypeArguments?.ConvertAll(CloneType));
         }
+
         var args = new List<ActualBinding>();
         args.Add(new ActualBinding(null, k));
         apply.Bindings.ArgumentBindings.ForEach(arg => args.Add(CloneActualBinding(arg)));
         var applyClone = new ApplySuffix(Tok(apply.tok), apply.AtTok == null ? null : Tok(apply.AtTok),
           lhsClone, args, Tok(apply.CloseParen));
         var c = new ExprRhs(applyClone, CloneAttributes(rhs.Attributes));
-        reporter.Info(MessageSource.Cloner, apply.Lhs.tok, mse.Member.Name + suffix);
+        reporter.Info(MessageSource.Cloner, apply.Lhs.tok, extremeLemma.Name + suffix);
         return c;
       }
     }
+
     return base.CloneRHS(rhs);
   }
 }

Source/DafnyCore/Resolver/CollectFriendlyCallsInSpec_Visitor.cs

@@ -19,9 +19,8 @@ protected override bool VisitOneExpr(Expression expr, ref CallingPosition cp) {
       // no friendly calls in "expr"
       return false;  // don't recurse into subexpressions
     }
-    if (expr is FunctionCallExpr) {
+    if (expr is FunctionCallExpr fexp) {
       if (cp == CallingPosition.Positive) {
-        var fexp = (FunctionCallExpr)expr;
         if (IsCoContext ? fexp.Function is GreatestPredicate : fexp.Function is LeastPredicate) {
           if (Context.KNat != ((ExtremePredicate)fexp.Function).KNat) {
             KNatMismatchError(expr.tok, Context.Name, Context.TypeOfK, ((ExtremePredicate)fexp.Function).TypeOfK);
@@ -31,8 +30,7 @@ protected override bool VisitOneExpr(Expression expr, ref CallingPosition cp) {
         }
       }
       return false;  // don't explore subexpressions any further
-    } else if (expr is BinaryExpr && IsCoContext) {
-      var bin = (BinaryExpr)expr;
+    } else if (expr is BinaryExpr bin && IsCoContext) {
       if (cp == CallingPosition.Positive && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.EqCommon && bin.E0.Type.IsCoDatatype) {
         friendlyCalls.Add(bin);
         return false;  // don't explore subexpressions any further

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -174,7 +174,7 @@ public void ComputeIsRecursiveBit(CompilationData compilation, ModuleDefinition
       }
 
       foreach (var rewriter in rewriters) {
-        rewriter.PostCyclicityResolve(module, Reporter);
+        rewriter.PostCyclicityResolve(module);
       }
     }
 
@@ -1685,6 +1685,7 @@ private void FillInPostConditionsAndBodiesOfPrefixLemmas(List<TopLevelDecl> decl
 
         var k = prefixLemma.Ins[0];
         var focalPredicates = new HashSet<ExtremePredicate>();
+        var focalCodatatypeEquality = new HashSet<CoDatatypeDecl>();
         if (com is GreatestLemma) {
           // compute the postconditions of the prefix lemma
           Contract.Assume(prefixLemma.Ens.Count == 0); // these are not supposed to have been filled in before
@@ -1696,19 +1697,19 @@ private void FillInPostConditionsAndBodiesOfPrefixLemmas(List<TopLevelDecl> decl
             var post = subst.CloneExpr(p.E);
             prefixLemma.Ens.Add(new AttributedExpression(post));
             foreach (var e in coConclusions) {
-              var fce = e as FunctionCallExpr;
-              if (fce != null) {
-                // the other possibility is that "e" is a BinaryExpr
+              if (e is FunctionCallExpr fce) {
                 GreatestPredicate predicate = (GreatestPredicate)fce.Function;
                 focalPredicates.Add(predicate);
                 // For every focal predicate P in S, add to S all greatest predicates in the same strongly connected
                 // component (in the call graph) as P
-                foreach (var node in predicate.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCC(
-                           predicate)) {
-                  if (node is GreatestPredicate) {
-                    focalPredicates.Add((GreatestPredicate)node);
+                foreach (var node in predicate.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCC(predicate)) {
+                  if (node is GreatestPredicate greatestPredicate) {
+                    focalPredicates.Add(greatestPredicate);
                   }
                 }
+              } else {
+                var binExpr = (BinaryExpr)e; // each "coConclusion" is either a FunctionCallExpr or a BinaryExpr
+                focalCodatatypeEquality.Add(binExpr.E0.Type.AsCoDatatype ?? binExpr.E1.Type.AsCoDatatype);
               }
             }
           }
@@ -1729,24 +1730,29 @@ private void FillInPostConditionsAndBodiesOfPrefixLemmas(List<TopLevelDecl> decl
               // For every focal predicate P in S, add to S all least predicates in the same strongly connected
               // component (in the call graph) as P
               foreach (var node in predicate.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCC(predicate)) {
-                if (node is LeastPredicate) {
-                  focalPredicates.Add((LeastPredicate)node);
+                if (node is LeastPredicate leastPredicate) {
+                  focalPredicates.Add(leastPredicate);
                 }
               }
             }
           }
         }
 
-        reporter.Info(MessageSource.Resolver, com.tok,
-          focalPredicates.Count == 0
-            ? $"{com.PrefixLemma.Name} has no focal predicates"
-            : $"{com.PrefixLemma.Name} with focal predicate{Util.Plural(focalPredicates.Count)} {Util.Comma(focalPredicates, p => p.Name)}");
+        var focalCount = focalPredicates.Count + focalCodatatypeEquality.Count;
+        if (focalCount == 0) {
+          reporter.Info(MessageSource.Resolver, com.tok, $"{com.PrefixLemma.Name} has no focal predicates");
+        } else {
+          var predicates = Util.Comma(focalPredicates, p => p.Name);
+          var equalities = Util.Comma(focalCodatatypeEquality, decl => $"{decl.Name}.==");
+          var focals = predicates + (predicates.Length != 0 && equalities.Length != 0 ? ", " : "") + equalities;
+          reporter.Info(MessageSource.Resolver, com.tok, $"{com.PrefixLemma.Name} with focal predicate{Util.Plural(focalCount)} {focals}");
+        }
         // Compute the statement body of the prefix lemma
         Contract.Assume(prefixLemma.Body == null); // this is not supposed to have been filled in before
         if (com.Body != null) {
           var kMinusOne = new BinaryExpr(com.tok, BinaryExpr.Opcode.Sub, new IdentifierExpr(k.tok, k.Name),
             new LiteralExpr(com.tok, 1));
-          var subst = new ExtremeLemmaBodyCloner(com, kMinusOne, focalPredicates, this.reporter);
+          var subst = new ExtremeLemmaBodyCloner(com, kMinusOne, focalPredicates, focalCodatatypeEquality, this.reporter);
           var mainBody = subst.CloneBlockStmt(com.Body);
           Expression kk;
           Statement els;

Source/DafnyCore/Rewriters/IRewriter.cs

@@ -76,7 +76,7 @@ internal virtual void PostResolveIntermediate(ModuleDefinition moduleDefinition)
     /// <param name="moduleDefinition">A module definition after it
     ///   is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed</param>
     /// <param name="errorReporter"></param>
-    internal virtual void PostCyclicityResolve(ModuleDefinition moduleDefinition, ErrorReporter errorReporter) {
+    internal virtual void PostCyclicityResolve(ModuleDefinition moduleDefinition) {
       Contract.Requires(moduleDefinition != null);
     }
 

Source/DafnyCore/Rewriters/InductionHeuristic.cs

@@ -1,3 +1,4 @@
+#nullable enable
 using System.Diagnostics.Contracts;
 
 namespace Microsoft.Dafny;
@@ -6,6 +7,8 @@
 
   /// <summary>
   /// Returns 'true' iff by looking at 'expr' the Induction Heuristic determines that induction should be applied to 'n'.
+  /// Variable 'n' can be passed in as 'null', in which case it stands for 'this'.
+  /// 
   /// More precisely:
   ///   DafnyInductionHeuristic      Return 'true'
   ///   -----------------------      -------------
@@ -17,10 +20,15 @@
   ///        5    if 'n' occurs as   a prominent subexpression of                                                               any                       argument to a recursive function
   ///        6    if 'n' occurs as   a prominent subexpression of                                                               any decreases-influencing argument to a recursive function
   /// </summary>
-  public static bool VarOccursInArgumentToRecursiveFunction(DafnyOptions options, Expression expr, IVariable n) {
+  public static bool VarOccursInArgumentToRecursiveFunction(DafnyOptions options, Expression expr, IVariable? n) {
     switch (options.InductionHeuristic) {
       case 0: return true;
-      case 1: return FreeVariablesUtil.ContainsFreeVariable(expr, false, n);
+      case 1:
+        if (n == null) {
+          return FreeVariablesUtil.ContainsFreeVariable(expr, true, null);
+        } else {
+          return FreeVariablesUtil.ContainsFreeVariable(expr, false, n);
+        }
       default: return VarOccursInArgumentToRecursiveFunction(options, expr, n, false);
     }
   }
@@ -30,16 +38,18 @@
   /// not 'expr' has prominent status in its context.
   /// DafnyInductionHeuristic cases 0 and 1 are assumed to be handled elsewhere (i.e., a precondition of this method is DafnyInductionHeuristic is at least 2).
   /// </summary>
-  static bool VarOccursInArgumentToRecursiveFunction(DafnyOptions options, Expression expr, IVariable n, bool exprIsProminent) {
+  static bool VarOccursInArgumentToRecursiveFunction(DafnyOptions options, Expression expr, IVariable? n, bool exprIsProminent) {
     Contract.Requires(expr != null);
     Contract.Requires(n != null);
 
     // The following variable is what gets passed down to recursive calls if the subexpression does not itself acquire prominent status.
     var subExprIsProminent = options.InductionHeuristic == 2 || options.InductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false;
 
-    if (expr is IdentifierExpr) {
+    if (n != null && expr is IdentifierExpr) {
       var e = (IdentifierExpr)expr;
       return exprIsProminent && e.Var == n;
+    } else if (n == null && expr is ThisExpr) {
+      return exprIsProminent;
     } else if (expr is SeqSelectExpr) {
       var e = (SeqSelectExpr)expr;
       var q = options.InductionHeuristic < 4 || subExprIsProminent;
@@ -108,7 +118,7 @@
       }
     } else if (expr is DatatypeValue) {
       var e = (DatatypeValue)expr;
-      var q = n.Type.IsDatatype ? exprIsProminent : subExprIsProminent;  // prominent status continues, if we're looking for a variable whose type is a datatype
+      var q = n != null && n.Type.IsDatatype ? exprIsProminent : subExprIsProminent;  // prominent status continues, if we're looking for a variable whose type is a datatype
       return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(options, exp, n, q));
     } else if (expr is UnaryExpr) {
       var e = (UnaryExpr)expr;
@@ -145,7 +155,7 @@
     } else if (expr is StmtExpr) {
       var e = (StmtExpr)expr;
       // ignore the statement
-      return VarOccursInArgumentToRecursiveFunction(options, e.E, n);
+      return VarOccursInArgumentToRecursiveFunction(options, e.E, n, exprIsProminent);
 
     } else if (expr is ITEExpr) {
       var e = (ITEExpr)expr;
@@ -164,7 +174,7 @@
       return false;
     } else {
       // in all other cases, reset the prominence status and recurse on the subexpressions
       foreach (var exp in expr.SubExpressions) {
         if (VarOccursInArgumentToRecursiveFunction(options, exp, n, subExprIsProminent)) {
           return true;
         }