DafnyExtension: Add menu item for automatic induction (mainly developed by Rustan).

5 files changed, 59 insertions, 4 deletions

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