From f28fa68497352ffb57ab2846da4cc1c1aeaf1968 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Wed, 12 Aug 2015 22:44:50 -0700
Subject: Change the induction heuristic for lemmas to also look in
 precondition for clues about which parameters to include. As a result,
 improved many test cases (see, e.g., dafny4/NipkowKlein-chapter7.dfy!) and
 beautified some others.

---
 Source/Dafny/Printer.cs  |  3 ++-
 Source/Dafny/Rewriter.cs | 23 +++++++++++++----------
 2 files changed, 15 insertions(+), 11 deletions(-)

(limited to 'Source')

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 1f63d769..6a6a76ba 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -438,6 +438,7 @@ namespace Microsoft.Dafny {
     public void PrintAttributes(Attributes a) {
       if (a != null) {
         PrintAttributes(a.Prev);
+        wr.Write(" ");
         PrintOneAttribute(a);
       }
     }
@@ -445,7 +446,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(a != null);
       var name = nameSubstitution ?? a.Name;
       var usAttribute = name.StartsWith("_");
-      wr.Write(" {1}{{:{0}", name, usAttribute ? "/*" : "");
+      wr.Write("{1}{{:{0}", name, usAttribute ? "/*" : "");
       if (a.Args != null) {
         PrintAttributeArgs(a.Args, false);
       }
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 4ac709f6..f107a819 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -1336,25 +1336,25 @@ namespace Microsoft.Dafny
     }
     void ComputeLemmaInduction(Method method) {
       Contract.Requires(method != null);
-      if (method.IsGhost && method.Mod.Expressions.Count == 0 && method.Outs.Count == 0 && !(method is FixpointLemma)) {
-        var posts = new List<Expression>();
-        method.Ens.ForEach(mfe => posts.Add(mfe.E));
-        ComputeInductionVariables(method.tok, method.Ins, posts, ref method.Attributes);
+      if (method.Body != null && method.IsGhost && method.Mod.Expressions.Count == 0 && method.Outs.Count == 0 && !(method is FixpointLemma)) {
+        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);
       }
     }
-    void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, List<Expression> searchExprs, ref Attributes attributes) where VarType : class, IVariable {
+    void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, List<Expression> searchExprs, Method lemma, ref Attributes attributes) where VarType : class, IVariable {
       Contract.Requires(tok != null);
       Contract.Requires(boundVars != null);
       Contract.Requires(searchExprs != null);
       Contract.Requires(DafnyOptions.O.Induction != 0);
-      bool forLemma = boundVars is List<Formal>;
 
       var args = Attributes.FindExpressions(attributes, "induction");  // we only look at the first one we find, since it overrides any other ones
       if (args == null) {
         if (DafnyOptions.O.Induction < 2) {
           // No explicit induction variables and we're asked not to infer anything, so we're done
           return;
-        } else if (DafnyOptions.O.Induction == 2 && forLemma) {
+        } else if (DafnyOptions.O.Induction == 2 && lemma != null) {
           // We're asked to infer induction variables only for quantifiers, not for lemmas
           return;
         }
@@ -1384,13 +1384,13 @@ namespace Microsoft.Dafny
             }
             if (0 <= boundVars.FindIndex(v => v == ie.Var)) {
               Resolver.Warning(arg.tok, "{0}s given as :induction arguments must be given in the same order as in the {1}; ignoring attribute",
-                forLemma ? "lemma parameter" : "bound variable", forLemma ? "lemma" : "quantifier");
+                lemma != null ? "lemma parameter" : "bound variable", lemma != null ? "lemma" : "quantifier");
               return;
             }
           }
           Resolver.Warning(arg.tok, "invalid :induction attribute argument; expected {0}{1}; ignoring attribute",
             i == 0 ? "'false' or 'true' or " : "",
-            forLemma ? "lemma parameter" : "bound variable");
+            lemma != null ? "lemma parameter" : "bound variable");
           return;
         }
         // The argument list was legal, so let's use it for the _induction attribute
@@ -1410,6 +1410,9 @@ namespace Microsoft.Dafny
         attributes = new Attributes("_induction", inductionVariables, attributes);
         // And since we're inferring something, let's also report that in a hover text.
         var s = Printer.OneAttributeToString(attributes, "induction");
+        if (lemma is PrefixLemma) {
+          s = lemma.Name + " " + s;
+        }
         Resolver.ReportAdditionalInformation(tok, s);
       }
     }
@@ -1423,7 +1426,7 @@ namespace Microsoft.Dafny
       protected override void VisitOneExpr(Expression expr) {
         var q = expr as QuantifierExpr;
         if (q != null) {
-          IndRewriter.ComputeInductionVariables(q.tok, q.BoundVars, new List<Expression>() { q.LogicalBody() }, ref q.Attributes);
+          IndRewriter.ComputeInductionVariables(q.tok, q.BoundVars, new List<Expression>() { q.LogicalBody() }, null, ref q.Attributes);
         }
       }
       void VisitInductionStmt(Statement stmt) {
-- 
cgit v1.2.3