From 47e3c9e215f1c5f51d35a974fccb5bd612eaa8be Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 18 May 2015 23:41:08 +0200
Subject: DafnyExtension: Added experimental support for diagnosing timeouts.

---
 Source/DafnyMenu/DafnyMenuPackage.cs | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

(limited to 'Source/DafnyMenu/DafnyMenuPackage.cs')

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 0acf3554..58c8f0ab 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -53,6 +53,12 @@ namespace DafnyLanguage.DafnyMenu
 
 
     void ShowErrorModel(IWpfTextView activeTextView);
+
+
+    bool DiagnoseTimeoutsCommandEnabled(IWpfTextView activeTextView);
+
+
+    void DiagnoseTimeouts(IWpfTextView activeTextView);
   }
 
 
@@ -88,6 +94,7 @@ namespace DafnyLanguage.DafnyMenu
     private OleMenuCommand toggleSnapshotVerificationCommand;
     private OleMenuCommand toggleMoreAdvancedSnapshotVerificationCommand;
     private OleMenuCommand toggleBVDCommand;
+    private OleMenuCommand diagnoseTimeoutsCommand;
 
     bool BVDDisabled;
 
@@ -157,6 +164,12 @@ namespace DafnyLanguage.DafnyMenu
         toggleBVDCommand.BeforeQueryStatus += showErrorModelCommand_BeforeQueryStatus;
         mcs.AddCommand(toggleBVDCommand);
 
+        var diagnoseTimeoutsCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidDiagnoseTimeouts);
+        diagnoseTimeoutsCommand = new OleMenuCommand(DiagnoseTimeoutsCallback, diagnoseTimeoutsCommandID);
+        diagnoseTimeoutsCommand.Enabled = true;
+        diagnoseTimeoutsCommand.BeforeQueryStatus += diagnoseTimeoutsCommand_BeforeQueryStatus;
+        mcs.AddCommand(diagnoseTimeoutsCommand);
+
         var menuCommandID = new CommandID(GuidList.guidDafnyMenuPkgSet, (int)PkgCmdIDList.cmdidMenu);
         menuCommand = new OleMenuCommand(new EventHandler((sender, e) => { }), menuCommandID);
         menuCommand.BeforeQueryStatus += menuCommand_BeforeQueryStatus;
@@ -301,6 +314,16 @@ namespace DafnyLanguage.DafnyMenu
       }
     }
 
+    void diagnoseTimeoutsCommand_BeforeQueryStatus(object sender, EventArgs e)
+    {
+      var atv = ActiveTextView;
+      if (MenuProxy != null && atv != null)
+      {
+        var visible = MenuProxy.DiagnoseTimeoutsCommandEnabled(atv);
+        diagnoseTimeoutsCommand.Visible = visible;
+      }
+    }
+
     private void toggleMoreAdvancedSnapshotVerificationCommand_BeforeQueryStatus(object sender, EventArgs e)
     {
       var atv = ActiveTextView;
@@ -317,6 +340,15 @@ namespace DafnyLanguage.DafnyMenu
       toggleBVDCommand.Text = (BVDDisabled ? "Enable" : "Disable") + " BVD";
     }
 
+    void DiagnoseTimeoutsCallback(object sender, EventArgs e)
+    {
+      var atv = ActiveTextView;
+      if (MenuProxy != null && atv != null)
+      {
+        MenuProxy.DiagnoseTimeouts(atv);
+      }
+    }
+
     public void ExecuteAsCompiling(Action action, TextWriter outputWriter)
     {
       IVsStatusbar statusBar = (IVsStatusbar)GetGlobalService(typeof(SVsStatusbar));
-- 
cgit v1.2.3


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 ++++++++
 Source/DafnyMenu/DafnyMenu.vsct      | 14 ++++++++++++--
 Source/DafnyMenu/DafnyMenuPackage.cs | 31 ++++++++++++++++++++++++++++++-
 Source/DafnyMenu/PkgCmdID.cs         |  3 ++-
 5 files changed, 59 insertions(+), 4 deletions(-)

(limited to 'Source/DafnyMenu/DafnyMenuPackage.cs')

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;
diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index 4c9a4913..02ffcf48 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -112,6 +112,15 @@
         </Strings>
       </Button>
 
+      <Button guid="guidDafnyMenuCmdSet" id="cmdidToggleAutomaticInduction" priority="0x0106" type="Button">
+        <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />
+        <CommandFlag>DynamicVisibility</CommandFlag>
+        <CommandFlag>TextChanges</CommandFlag>
+        <Strings>
+          <ButtonText>Disable automatic induction</ButtonText>
+        </Strings>
+      </Button>
+
       <Button guid="guidDafnyMenuCmdSet" id="cmdidToggleBVD" priority="0x010a" type="Button">
         <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />
         <CommandFlag>DynamicVisibility</CommandFlag>
@@ -122,7 +131,7 @@
         </Strings>
       </Button>
 
-      <Button guid="guidDafnyMenuCmdSet" id="cmdidDiagnoseTimeouts" priority="0x0106" type="Button">
+      <Button guid="guidDafnyMenuCmdSet" id="cmdidDiagnoseTimeouts" priority="0x0107" type="Button">
         <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />
         <CommandFlag>DynamicVisibility</CommandFlag>
         <CommandFlag>DefaultInvisible</CommandFlag>
@@ -164,7 +173,8 @@
       <IDSymbol name="cmdidToggleSnapshotVerification" value="0x0103" />
       <IDSymbol name="cmdidToggleBVD" value="0x0104" />
       <IDSymbol name="cmdidToggleMoreAdvancedSnapshotVerification" value="0x0105" />
-      <IDSymbol name="cmdidDiagnoseTimeouts" value="0x0106" />
+      <IDSymbol name="cmdidToggleAutomaticInduction" value="0x0106" />
+      <IDSymbol name="cmdidDiagnoseTimeouts" value="0x0107" />
     </GuidSymbol>
 
     <!--
diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 58c8f0ab..0addda47 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -28,6 +28,12 @@ namespace DafnyLanguage.DafnyMenu
     bool MoreAdvancedSnapshotVerificationCommandEnabled(IWpfTextView activeTextView);
 
 
+    bool ToggleAutomaticInduction(IWpfTextView activeTextView);
+
+
+    bool AutomaticInductionCommandEnabled(IWpfTextView activeTextView);
+
+    
     bool StopVerifierCommandEnabled(IWpfTextView activeTextView);
 
 
@@ -93,6 +99,7 @@ namespace DafnyLanguage.DafnyMenu
     private OleMenuCommand stopVerifierCommand;
     private OleMenuCommand toggleSnapshotVerificationCommand;
     private OleMenuCommand toggleMoreAdvancedSnapshotVerificationCommand;
+    private OleMenuCommand toggleAutomaticInductionCommand;
     private OleMenuCommand toggleBVDCommand;
     private OleMenuCommand diagnoseTimeoutsCommand;
 
@@ -158,6 +165,12 @@ namespace DafnyLanguage.DafnyMenu
         toggleMoreAdvancedSnapshotVerificationCommand.BeforeQueryStatus += toggleMoreAdvancedSnapshotVerificationCommand_BeforeQueryStatus;
         mcs.AddCommand(toggleMoreAdvancedSnapshotVerificationCommand);
 
+        var toggleAutomaticInductionCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleAutomaticInduction);
+        toggleAutomaticInductionCommand = new OleMenuCommand(ToggleAutomaticInductionCallback, toggleAutomaticInductionCommandID);
+        toggleAutomaticInductionCommand.Enabled = true;
+        toggleAutomaticInductionCommand.BeforeQueryStatus += toggleAutomaticInductionCommand_BeforeQueryStatus;
+        mcs.AddCommand(toggleAutomaticInductionCommand);
+
         var showErrorModelCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleBVD);
         toggleBVDCommand = new OleMenuCommand(ToggleBVDCallback, showErrorModelCommandID);
         toggleBVDCommand.Enabled = true;
@@ -234,6 +247,14 @@ namespace DafnyLanguage.DafnyMenu
       }
     }
 
+    void ToggleAutomaticInductionCallback(object sender, EventArgs e) {
+      var atv = ActiveTextView;
+      if (MenuProxy != null && atv != null) {
+        var nowAutomatic = MenuProxy.ToggleAutomaticInduction(atv);
+        toggleAutomaticInductionCommand.Text = (nowAutomatic ? "Disable" : "Enable") + " automatic induction";
+      }
+    }
+
     void stopVerifierCommand_BeforeQueryStatus(object sender, EventArgs e)
     {
       var atv = ActiveTextView;
@@ -334,6 +355,14 @@ namespace DafnyLanguage.DafnyMenu
       }
     }
 
+    private void toggleAutomaticInductionCommand_BeforeQueryStatus(object sender, EventArgs e) {
+      var atv = ActiveTextView;
+      if (MenuProxy != null && atv != null) {
+        var visible = MenuProxy.AutomaticInductionCommandEnabled(atv);
+        toggleAutomaticInductionCommand.Visible = visible;
+      }
+    }
+
     void ToggleBVDCallback(object sender, EventArgs e)
     {
       BVDDisabled = !BVDDisabled;
@@ -379,7 +408,7 @@ namespace DafnyLanguage.DafnyMenu
         var window = this.FindToolWindow(typeof(BvdToolWindow), 0, true);
         if ((window == null) || (window.Frame == null))
         {
-          throw new NotSupportedException("Can not create BvdToolWindow.");
+          throw new NotSupportedException("Cannot create BvdToolWindow.");
         }
 
         BvdToolWindow.BVD.HideMenuStrip();
diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs
index 427dd888..ba4b786d 100644
--- a/Source/DafnyMenu/PkgCmdID.cs
+++ b/Source/DafnyMenu/PkgCmdID.cs
@@ -13,6 +13,7 @@ namespace DafnyLanguage.DafnyMenu
     public static uint cmdidToggleSnapshotVerification = 0x103;
     public const uint cmdidToggleBVD = 0x104;
     public static uint cmdidToggleMoreAdvancedSnapshotVerification = 0x105;
-    public static uint cmdidDiagnoseTimeouts = 0x106;
+    public static uint cmdidToggleAutomaticInduction = 0x106;
+    public static uint cmdidDiagnoseTimeouts = 0x107;
   };
 }
\ No newline at end of file
-- 
cgit v1.2.3