summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2015-10-26 17:36:25 -0500
committerGravatar wuestholz <unknown>2015-10-26 17:36:25 -0500
commit5e4bcf8e63a3351dc3f0f9bc6cbff8176adddd8b (patch)
treeb68f21a15903606993f46a12e83343e9eae9c0e5
parentb35216f55d22123ae4c35eacf28e99a2b6dbbfaf (diff)
DafnyExtension: Add menu item for automatic induction (mainly developed by Rustan).
-rw-r--r--Source/DafnyExtension/DafnyDriver.cs7
-rw-r--r--Source/DafnyExtension/MenuProxy.cs8
-rw-r--r--Source/DafnyMenu/DafnyMenu.vsct14
-rw-r--r--Source/DafnyMenu/DafnyMenuPackage.cs31
-rw-r--r--Source/DafnyMenu/PkgCmdID.cs3
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