From 5e4bcf8e63a3351dc3f0f9bc6cbff8176adddd8b Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 26 Oct 2015 17:36:25 -0500
Subject: DafnyExtension: Add menu item for automatic induction (mainly
 developed by Rustan).

---
 Source/DafnyExtension/DafnyDriver.cs | 7 +++++++
 Source/DafnyExtension/MenuProxy.cs   | 8 ++++++++
 2 files changed, 15 insertions(+)

(limited to 'Source/DafnyExtension')

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 2ad05e85..27471d56 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -251,6 +251,13 @@ namespace DafnyLanguage
       return Dafny.DafnyOptions.Clo.VerifySnapshots;
     }
 
+    public static bool ChangeAutomaticInduction() {
+      var old = Dafny.DafnyOptions.O.Induction;
+      // toggle between modes 1 and 3
+      Dafny.DafnyOptions.O.Induction = old == 1 ? 3 : 1;
+      return Dafny.DafnyOptions.O.Induction == 3;
+    }
+
     public static bool Verify(Dafny.Program dafnyProgram, ResolverTagger resolver, string uniqueIdPrefix, string requestId, ErrorReporterDelegate er) {
       Dafny.Translator translator = new Dafny.Translator(dafnyProgram.reporter);
       translator.InsertChecksums = true;
diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs
index 9ddc8344..0e061cd3 100644
--- a/Source/DafnyExtension/MenuProxy.cs
+++ b/Source/DafnyExtension/MenuProxy.cs
@@ -33,6 +33,14 @@ namespace DafnyLanguage
              && 0 < DafnyDriver.IncrementalVerificationMode();
     }
 
+    public bool ToggleAutomaticInduction(IWpfTextView activeTextView) {
+      return DafnyDriver.ChangeAutomaticInduction();
+    }
+
+    public bool AutomaticInductionCommandEnabled(IWpfTextView activeTextView) {
+      return activeTextView != null;
+    }
+
     public bool StopVerifierCommandEnabled(IWpfTextView activeTextView)
     {
       DafnyLanguage.ProgressTagger tagger;
-- 
cgit v1.2.3