Use CanCall everywhere

Source/DafnyCore/AST/Expressions/Expression.cs

@@ -156,15 +156,41 @@ public virtual IEnumerable<Type> ComponentTypes {
 
   public virtual bool IsImplicit => false;
 
+  public static IEnumerable<Expression> ConjunctsWithLetsOnOutside(Expression expr) {
+    foreach (var conjunct in Conjuncts(expr)) {
+      if (conjunct is LetExpr { Exact: true } letExpr) {
+        foreach (var letBodyConjunct in ConjunctsWithLetsOnOutside(letExpr.Body)) {
+          yield return new LetExpr(letExpr.tok, letExpr.LHSs, letExpr.RHSs, letBodyConjunct, letExpr.Exact, letExpr.Attributes) {
+            Type = letExpr.Type
+          };
+        }
+      } else {
+        yield return conjunct;
+      }
+    }
+  }
+
+  /// <summary>
+  /// Return the negation of each of the expressions in "expressions".
+  /// If there is just one expression in "expressions", then use the given token "tok" for the negation.
+  /// Otherwise, use the token from each expression.
+  /// </summary>
+  static IEnumerable<Expression> NegateEach(IToken tok, IEnumerable<Expression> expressions) {
+    var exprs = expressions.ToList();
+    foreach (Expression e in exprs) {
+      yield return Expression.CreateNot(exprs.Count == 1 ? tok : e.tok, e);
+    }
+  }
+
   public static IEnumerable<Expression> Conjuncts(Expression expr) {
     Contract.Requires(expr != null);
     Contract.Requires(expr.Type.IsBoolType);
     Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expression>>()));
 
     expr = StripParens(expr);
-    if (expr is UnaryOpExpr unary && unary.Op == UnaryOpExpr.Opcode.Not) {
-      foreach (Expression e in Disjuncts(unary.E)) {
-        yield return Expression.CreateNot(e.tok, e);
+    if (expr is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Not } unary) {
+      foreach (Expression e in NegateEach(expr.tok, Disjuncts(unary.E))) {
+        yield return e;
       }
       yield break;
 
@@ -189,26 +215,26 @@ public static IEnumerable<Expression> Disjuncts(Expression expr) {
     Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expression>>()));
 
     expr = StripParens(expr);
-    if (expr is UnaryOpExpr unary && unary.Op == UnaryOpExpr.Opcode.Not) {
-      foreach (Expression e in Conjuncts(unary.E)) {
-        yield return Expression.CreateNot(e.tok, e);
+    if (expr is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Not } unary) {
+      foreach (Expression e in NegateEach(expr.tok, Conjuncts(unary.E))) {
+        yield return e;
       }
       yield break;
 
     } else if (expr is BinaryExpr bin) {
       if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) {
-        foreach (Expression e in Conjuncts(bin.E0)) {
+        foreach (Expression e in Disjuncts(bin.E0)) {
           yield return e;
         }
-        foreach (Expression e in Conjuncts(bin.E1)) {
+        foreach (Expression e in Disjuncts(bin.E1)) {
           yield return e;
         }
         yield break;
       } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {
         foreach (Expression e in Conjuncts(bin.E0)) {
           yield return Expression.CreateNot(e.tok, e);
         }
-        foreach (Expression e in Conjuncts(bin.E1)) {
+        foreach (Expression e in Disjuncts(bin.E1)) {
           yield return e;
         }
         yield break;

Source/DafnyCore/CounterExampleGeneration/DafnyModel.cs

@@ -72,7 +72,7 @@ public DafnyModel(Model model, DafnyOptions options) {
       fMapEmpty = new ModelFuncWrapper(this, "Map#Empty", 0, 0);
       fIs = new ModelFuncWrapper(this, "$Is", 2, tyArgMultiplier);
       fIsBox = new ModelFuncWrapper(this, "$IsBox", 2, 0);
-      fBox = new ModelFuncWrapper(this, "$Box", 1, tyArgMultiplier);
+      fBox = new ModelFuncWrapper(this, BoogieGenerator.BoxFunctionName, 1, tyArgMultiplier);
       fDim = new ModelFuncWrapper(this, "FDim", 1, 0);
       fIndexField = new ModelFuncWrapper(this, "IndexField", 1, 0);
       fMultiIndexField = new ModelFuncWrapper(this, "MultiIndexField", 2, 0);
@@ -84,7 +84,7 @@ public DafnyModel(Model model, DafnyOptions options) {
       fU2Int = new ModelFuncWrapper(this, "U_2_int", 1, 0);
       fTag = new ModelFuncWrapper(this, "Tag", 1, 0);
       fBv = new ModelFuncWrapper(this, "TBitvector", 1, 0);
-      fUnbox = new ModelFuncWrapper(this, "$Unbox", 2, 0);
+      fUnbox = new ModelFuncWrapper(this, BoogieGenerator.UnboxFunctionName, 2, 0);
       fLs = new ModelFuncWrapper(this, "$LS", 1, 0);
       fLz = new ModelFuncWrapper(this, "$LZ", 0, 0);
       InitDataTypes();

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

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/InductionRewriter.cs

@@ -1,5 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Linq;
+using JetBrains.Annotations;
 using static Microsoft.Dafny.RewriterErrors;
 
 namespace Microsoft.Dafny;
@@ -40,20 +42,17 @@ internal override void PostDecreasesResolve(ModuleDefinition m) {
           }
         }
 
-        if (decl is NewtypeDecl) {
-          var nt = (NewtypeDecl)decl;
-          if (nt.Constraint != null) {
-            var visitor = new Induction_Visitor(this);
-            visitor.Visit(nt.Constraint);
-          }
+        if (decl is NewtypeDecl { Constraint: { } constraint }) {
+          var visitor = new InductionVisitor(this);
+          visitor.Visit(constraint);
         }
       }
     }
   }
 
   void ProcessMethodExpressions(Method method) {
     Contract.Requires(method != null);
-    var visitor = new Induction_Visitor(this);
+    var visitor = new InductionVisitor(this);
     method.Req.ForEach(mfe => visitor.Visit(mfe.E));
     method.Ens.ForEach(mfe => visitor.Visit(mfe.E));
     if (method.Body != null) {
@@ -63,7 +62,7 @@ void ProcessMethodExpressions(Method method) {
 
   void ProcessFunctionExpressions(Function function) {
     Contract.Requires(function != null);
-    var visitor = new Induction_Visitor(this);
+    var visitor = new InductionVisitor(this);
     function.Req.ForEach(visitor.Visit);
     function.Ens.ForEach(visitor.Visit);
     if (function.Body != null) {
@@ -73,20 +72,29 @@ void ProcessFunctionExpressions(Function function) {
 
   void ComputeLemmaInduction(Method method) {
     Contract.Requires(method != null);
-    if (method.Body != null && method.IsGhost && method.Mod.Expressions.Count == 0 && method.Outs.Count == 0 &&
-        !(method is ExtremeLemma)) {
-      var specs = new List<Expression>();
-      method.Req.ForEach(mfe => specs.Add(mfe.E));
-      method.Ens.ForEach(mfe => specs.Add(mfe.E));
-      ComputeInductionVariables(method.tok, method.Ins, specs, method, ref method.Attributes);
+    if (method is Lemma or PrefixLemma && method is { Body: not null, Outs: { Count: 0 } }) {
+      Expression pre = Expression.CreateBoolLiteral(method.tok, true);
+      foreach (var req in method.Req) {
+        pre = Expression.CreateAnd(pre, req.E);
+      }
+      Expression post = Expression.CreateBoolLiteral(method.tok, true);
+      foreach (var ens in method.Ens) {
+        post = Expression.CreateAnd(post, ens.E);
+      }
+      ComputeInductionVariables(method.tok, method.Ins, Expression.CreateImplies(pre, post), method, ref method.Attributes);
     }
   }
 
-  void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, List<Expression> searchExprs,
-    Method lemma, ref Attributes attributes) where VarType : class, IVariable {
+  /// <summary>
+  /// Look at the command-line options and any {:induction} attribute to determine a good list of induction
+  /// variables. If there are any, then record them in an attribute {:_induction ...} added to "attributes".
+  /// "body" is the condition that the induction would support.
+  /// </summary>
+  void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, Expression body,
+    [CanBeNull] Method lemma, ref Attributes attributes) where TVarType : class, IVariable {
     Contract.Requires(tok != null);
     Contract.Requires(boundVars != null);
-    Contract.Requires(searchExprs != null);
+    Contract.Requires(body != null);
     Contract.Requires(Reporter.Options.Induction != 0);
 
     var args = Attributes.FindExpressions(attributes,
@@ -106,9 +114,9 @@ void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, Lis
     } else if (args.Count == 0) {
       // {:induction} is treated the same as {:induction true}, which says to automatically infer induction variables
       // GO INFER below (all boundVars)
-    } else if (args.Count == 1 && args[0] is LiteralExpr && ((LiteralExpr)args[0]).Value is bool) {
+    } else if (args.Count == 1 && args[0] is LiteralExpr { Value: bool and var boolValue }) {
       // {:induction false} or {:induction true}
-      if (!(bool)((LiteralExpr)args[0]).Value) {
+      if (!boolValue) {
         // we're told not to infer anything
         return;
       }
@@ -117,12 +125,11 @@ void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, Lis
       // Here, we're expecting the arguments to {:induction args} to be a sublist of "this;boundVars", where "this" is allowed only
       // if "lemma" denotes an instance lemma.
       var goodArguments = new List<Expression>();
-      var i = lemma != null && !lemma.IsStatic
+      var i = lemma is { IsStatic: false }
         ? -1
         : 0; // -1 says it's okay to see "this" or any other parameter; 0 <= i says it's okay to see parameter i or higher
       foreach (var arg in args) {
-        var ie = arg.Resolved as IdentifierExpr;
-        if (ie != null) {
+        if (arg.Resolved is IdentifierExpr ie) {
           var j = boundVars.FindIndex(v => v == ie.Var);
           if (0 <= j && i <= j) {
             goodArguments.Add(ie);
@@ -163,20 +170,37 @@ void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, Lis
 
     // Okay, here we go, coming up with good induction setting for the given situation
     var inductionVariables = new List<Expression>();
-    if (lemma != null && !lemma.IsStatic) {
-      if (args != null || searchExprs.Exists(expr => FreeVariablesUtil.ContainsFreeVariable(expr, true, null))) {
+    if (lemma is { IsStatic: false }) {
+      if (args != null || FreeVariablesUtil.ContainsFreeVariable(body, true, null)) {
         inductionVariables.Add(new ThisExpr(lemma));
       }
     }
 
     foreach (IVariable n in boundVars) {
-      if (!(n.Type.IsTypeParameter || n.Type.IsAbstractType || n.Type.IsInternalTypeSynonym) && (args != null ||
-            searchExprs.Exists(expr => InductionHeuristic.VarOccursInArgumentToRecursiveFunction(Reporter.Options, expr, n)))) {
+      if (!(n.Type.IsTypeParameter || n.Type.IsAbstractType || n.Type.IsInternalTypeSynonym) &&
+          (args != null || InductionHeuristic.VarOccursInArgumentToRecursiveFunction(Reporter.Options, body, n))) {
         inductionVariables.Add(new IdentifierExpr(n.Tok, n));
       }
     }
 
     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.
@@ -189,19 +213,60 @@ void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, Lis
     }
   }
 
-  class Induction_Visitor : BottomUpVisitor {
+  /// <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;
 
-    public Induction_Visitor(InductionRewriter inductionRewriter) {
+    public InductionVisitor(InductionRewriter inductionRewriter) {
       Contract.Requires(inductionRewriter != null);
       IndRewriter = inductionRewriter;
     }
 
     protected override void VisitOneExpr(Expression expr) {
-      var q = expr as QuantifierExpr;
-      if (q != null && q.SplitQuantifier == null) {
-        IndRewriter.ComputeInductionVariables(q.tok, q.BoundVars, new List<Expression>() { q.LogicalBody() }, null,
-          ref q.Attributes);
+      if (expr is QuantifierExpr { SplitQuantifier: null } q) {
+        IndRewriter.ComputeInductionVariables(q.tok, q.BoundVars, q.LogicalBody(), null, ref q.Attributes);
       }
     }
   }

Source/DafnyCore/Rewriters/TriggerGeneratingRewriter.cs

@@ -9,8 +9,8 @@ internal TriggerGeneratingRewriter(ErrorReporter reporter, SystemModuleManager s
     this.systemModuleManager = systemModuleManager;
   }
 
-  internal override void PostCyclicityResolve(ModuleDefinition definition, ErrorReporter reporter) {
-    var finder = new Triggers.QuantifierCollector(reporter);
+  internal override void PostCyclicityResolve(ModuleDefinition definition) {
+    var finder = new Triggers.QuantifierCollector(Reporter);
 
     foreach (var decl in ModuleDefinition.AllCallablesIncludingPrefixDeclarations(definition.TopLevelDecls)) {
       finder.Visit(decl, null);

Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs

@@ -122,7 +122,7 @@ bool DetectAndFilterLoopingCandidates() {
       // 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
+      // in which that expression is found. For examples of this behavior, see
       // triggers/literals-do-not-cause-loops.
       // This ignoring logic is implemented by the CouldCauseLoops method.
       bool foundLoop = false;
@@ -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;
+    }
   }
 }