Merge pull request #27 from FliegendeWurst/misc2

Extend HowToTaclet with information on the new tagging mechanism
KeYProject · Oct 31, 2024 · c1a78dc · c1a78dc
2 parents b753a47 + f89bcad
commit c1a78dc
Show file tree

Hide file tree

Showing 8 changed files with 82 additions and 3 deletions.
diff --git a/docs/devel/HowToTaclet.md b/docs/devel/HowToTaclet.md
@@ -19,8 +19,8 @@ system. In particular, the following topics are discussed:
 
 The standard location for `.key` files containing taclets is in the `key.core`
 project, location `resources/de/uka/ilkd/key/proof/rules` (*note*: unless stated
-otherwise, all locations in this article are relative to `key.core`). The file
-`standardRules.key` lists all the taclet files that are are loaded as defaults
+otherwise, all locations in this article are relative to the main source root of `key.core`).
+The file `standardRules.key` lists all the taclet files that are are loaded as defaults
 when starting KeY with the Java profile. New taclets can be added to either of
 the existing files listed there (if they fit into the scope), or can be added to
 a new file which is then referred to in `standardRules.key`.
@@ -36,6 +36,55 @@ Taclets can be added to "rule sets" which are used, e.g., by strategy
 heuristics. Default rule sets are defined in the file
 `resources/de/uka/ilkd/key/proof/rules/ruleSetDeclarations.key`.
 
+### Quick example
+
+Consider the definition of `cut_direct` below (part of `propRule.key`).
+
+```
+\schemaVariables {
+  \formula cutFormula;
+}
+
+\rules {
+  cut_direct {
+    \find(cutFormula)
+    \sameUpdateLevel
+    "CUT: #cutFormula TRUE" [main]:
+        \replacewith(true) \add(cutFormula ==>);
+    "CUT: #cutFormula FALSE":
+        \replacewith(false) \add( ==> cutFormula)
+    \heuristics(cut_direct)
+  };
+}
+```
+
+First, we need to define the variables we want to use in the taclet.
+This is the `\schemaVariables` block at the start of the `.key` file.
+We only require a single `\formula` type schema variable called `cutFormula`.
+
+Then, we define the actual taclets in this file by creating a `\rules` block.
+For the purposes of this example, we limit ourselves to the cut_direct taclet.
+`propRule.key` contains many more taclets.
+The `\rules` block contains the taclet definitions, each of which begins with the name of the taclet
+("cut_direct"), creating a new block defined by curly brackets and a semicolon at the end.
+
+Since the `\find(...)` part of the taclet definition does not contain a `==>`, the `cut_direct` taclet finds (matches) a sub-term anywhere in a sequent formula.
+The `\sameUpdateLevel` essentially ensures it doesn't match under an update application.
+
+The taclet creates two new branches, which are defined directly afterwards.
+The first branch is labeled "CUT: #cutFormula TRUE".
+In this branch, the found sub-term is replaced with true (`\replacewith(true)`), and the found sub-term is added as a new sequent formula to the antecedent: `\add(cutFormula ==>)`.
+
+A particular branch of the taclet can be tagged by enclosing the tag in brackets.
+This tag must be written after the branch label.
+The first branch in this example is tagged with "main".
+This particular value causes the branch to be visually continued on the parent branch if [the linearized Proof Tree mode](../../user/ProofTreeLinearMode/) is active.
+
+The second branch of the taclet is labeled "CUT: #cutFormula FALSE".
+In this branch, the found sub-term is replaced with false (`\replacewith(false)`), and the found sub-term is added as a new sequent formula to the succedent: `\add( ==> cutFormula)`.
+
+Finally, the taclet is added to the `cut_direct` heuristics group.
+
 ## How to extend the taclet language
 
 !!! danger

diff --git a/docs/user/ProofCaching/index.md b/docs/user/ProofCaching/index.md
@@ -39,6 +39,12 @@ Without condition 1, the replay may fail.
 In KeY's settings dialog, enable the Proof Caching extension.
 You can toggle the automatic search for references in the "Proof Caching" section (on by default).
 
+### Enabling/disabling the functionality
+
+In the toolbar, a new Proof Caching toggle button is added.
+In the options menu, a Proof Caching checkbox is synchronized to the same state.
+When these are not activated, the automated reference search is disabled.
+
 ## Automated reference search
 
 When running the auto pilot or a strategy macro, KeY will automatically search for references
@@ -53,6 +59,11 @@ Right-click on an open goal in the proof tree and select "close by reference".
 If a matching branch is found, the goal will be closed.
 Otherwise, a dialog with an error message will open.
 
+## Re-opening cached proof branches
+
+It is possible to re-open proof goals closed by the cache.
+To do so, just activate the "Re-open cached goal" context menu entry on the goal you wish to re-open.
+
 ## Copying referenced proof steps
 
 In the status line, a button indicates whether cached goals are present:

diff --git a/docs/user/ProofTreeLinearMode.md b/docs/user/ProofTreeLinearMode.md
@@ -0,0 +1,17 @@
+# Proof Tree: linearized mode
+
+In the proof tree settings, you can enable the "Linearize Proof Tree" option.
+
+![Screenshot of option](ProofTreeLinearMode_enable.png)
+
+## Effect when enabled
+
+For symbolic execution steps, the "Normal Execution" branch will (visually) continue on the parent branch. See the screenshot below for a quick example.
+The exceptional case branches (e.g. Null Reference, Index Out of Bounds) are therefore placed above the steps of the Normal Execution branch.
+
+![Screenshot of tree with option enabled](ProofTreeLinearMode_example.png)
+
+Additionally, the TRUE branch of cut_direct applications will visually continue on the parent branch.
+This mechanism may be extended further by other taclets tagging their "main" created branch.
+
+![Screenshot of tree with cut_direct](ProofTreeLinearMode_example2.png)
diff --git a/docs/user/ProofTreeLinearMode_enable.png b/docs/user/ProofTreeLinearMode_enable.png
diff --git a/docs/user/ProofTreeLinearMode_example.png b/docs/user/ProofTreeLinearMode_example.png
diff --git a/docs/user/ProofTreeLinearMode_example2.png b/docs/user/ProofTreeLinearMode_example2.png
diff --git a/docs/user/UiFeatures/index.md b/docs/user/UiFeatures/index.md
@@ -1,4 +1,5 @@
 - [Exploration](../Exploration)
 - [Node Differences](../NodeDiff)
 - [Proof Slicing](../ProofSlicing)
-- [Proof Caching](../ProofCaching)
+- [Proof Caching](../ProofCaching)
+- [Proof Tree: linearized mode](../ProofTreeLinearMode)
diff --git a/mkdocs.yml b/mkdocs.yml
@@ -112,6 +112,7 @@ nav:
           - user/NodeDiff.md
           - user/ProofSlicing/index.md
           - user/ProofCaching/index.md
+          - user/ProofTreeLinearMode.md
       - Languages:
           - user/HowToTaclet.md
           - user/JMLGrammar.md