Document taclets

.vscode/settings.json

@@ -1,3 +1,4 @@
 {
+    "prettier.enable": false,
     "makefile.configureOnOpen": false
 }

docs/devel/HowToTaclet.md

@@ -1,3 +1,6 @@
+----
+approved: DD 2026-08-11
+----
 # How to write new taclets
 
 New prover rules in KeY can be added in form of built-in rules[^1] written in plain
@@ -72,7 +75,14 @@ The `\rules` block contains the taclet definitions, each of which begins with th
 ("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 application restriction flag `\sameUpdateLevel` ensures that the `\find(...)` and `\add(...)` parts are
+under the same update application (or none). 
+
+!!! info
+
+  Since KeY 3.0, `\sameUpdateLevel` is the default for all (relevant) taclets
+  and does not need to be added manually. Use `\ignoreUpdateLevel` to switch
+  it off.
 
 The taclet creates two new branches, which are defined directly afterwards.
 The first branch is labeled "CUT: #cutFormula TRUE".
@@ -88,6 +98,62 @@ In this branch, the found sub-term is replaced with false (`\replacewith(false)`
 
 Finally, the taclet is added to the `cut_direct` heuristics group.
 
+## Automatically Generating Additional Taclets
+
+KeY 3.1 allows for automatic generation of "derived" taclets. This is
+especially helpful for "EQ" taclets, which are commonly used to achieve more
+performant automation. Assume a taclet like `elementOfUnion`:
+
+```key
+elementOfUnion {
+  \schemaVar \term Object o;
+  \schemaVar \term Field f;
+  \schemaVar \term LocSet s, s2;
+
+  \find(elementOf(o, f, union(s, s2)))
+
+  \replacewith(elementOf(o, f, s) | elementOf(o, f, s2))
+
+  \heuristics(simplify_enlarging)
+  \generate(\EQ(union(s, s2)))
+};
+```
+
+This taclet can only be applied when `union(s, s2)` is directly in the
+`elementOf` function. But a common situation is a sequent such as
+```
+s1 = union(s, s2),
+==>
+elementOf(o, f, s1)
+```
+where `union(s, s2)` has been "pulled out" into `s1`.
+
+We can use _taclet generators_ to deal with this case easily. The
+`\generate(\EQ(...))` generates the following taclet automatically:
+
+```key
+elementOfUnionEQ {
+  \schemaVar \term Object o;
+  \schemaVar \term Field f;
+  \schemaVar \term LocSet s, s2;
+  \schemaVar \term LocSet EQ;
+
+  \assumes(union(s, s2) = EQ ==>)
+  \find(elementOf(o, f, EQ))
+
+  \replacewith(elementOf(o, f, s) | elementOf(o, f, s2))
+
+  \heuristics(simplify_enlarging)
+};
+```
+
+Note that an `\assumes(...)` part with an equation is added and how the term
+given to `\EQ(...)` is replaced in `\find(...)`. The `\find` parts of any rules
+in `\addrules` are also altered the same way. Rule sets are copied from the
+original taclet but can be altered by `\EQ(union(s, s2) : concrete)`.
+
+At the moment, `\EQ` is the only supported generator.
+
 ## How to extend the taclet language
 
 !!! danger
@@ -108,83 +174,76 @@ depend on additional input such as specifications, one can define (automatic or
 interactive) completions for the taclet. We'll discuss all those points in the
 following.
 
-It might be helpful to (additionally?) learn about the process by examples. To
+It might be helpful to learn about the process by examples. To
 get started, an example for a new program statement used for matching is
-"merge_point", the keyword for a merge point statement. A simpler one is
-"ForLoop", a schema variable matching for loops. If you search for those
-identifiers in all files in the "key.core" project, you'll find the entry points
+`merge_point`, the keyword for a merge point statement. A simpler one is
+`ForLoop`, a schema variable matching for loops. If you search for those
+identifiers in all files in the project, you'll find the entry points
 needed for extensions. Note that merge points are also used in JML
 specifications, which is a different topic (therefore, you might want to ignore
-the corresponding parser files "KeYJMLPre{Lexer, Parser}.g, basically everything
-in the `(...)/speclang/jml` directory.). An example for a transformer is the
-"#for-to-while" construct which accepts a for loop as input and transforms it to
+the corresponding parser files `KeYJMLPre{Lexer, Parser}.g`, basically everything
+in the `(...)/speclang/jml` directory). An example for a transformer is the
+`#for-to-while` construct which accepts a for loop as input and transforms it to
 a while loop. Your friends here are the eclipse functionalities `Search -> File`
 (use `*.*` as a pattern here, and only search in the key.core project), `Ctrl+T`
 for finding types, and `Ctrl+R` for finding resources.
 
 ### Parsing
 
 There are several relevant parsers you might need to know. The "main KeY
-parser", `src/de/uka/ilkd/key/parser/KeY{Lexer, Parser}.g` is an ANTLR3 parser
+parser," `src/main/antlr4/JavaKeY{Lexer, Parser}.g4` is an ANTLR4 parser
 which covers KeY's language for sorts, terms, formulas etc., taclets, and proof
-files. For most extensions, this file does not need to be touched.
+files. For most extensions, this file does not need to be touched. It extends
+the more general, largely Java-independent parser in `key.ncore/main/antlr/`.
 
-The parsers for Java extensions in taclets and proof files are
-`src/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj` and
-`src/de/uka/ilkd/key/parser/schemajava/ProofJavaParser.jj`, which are JavaCC
-parsers. In the former, you also find definitions for `#for-to-while` and
-`merge_point`; in the latter, only `merge_point` occurs since it is an extension
-of Java and not a transformer like `#for-to-while` which is only needed in
-taclets, but will never occur in a Java program.
+We use an [extension of the JavaParser project](https://github.com/jmltoolkit/jmltk)
+to parse Java and the KeY's
+extentions for Java, such as schema variables or KeY specific constructs.
+In its JavaCC file, you find definitions for `#for-to-while` and
+`merge_point`.
 
 So, if for your taclet the basic taclet language has to be changed, adapt
-`KeYParser.g` accordingly; for creating new transformers, `SchemaJavaParser.jj`
-is the relevant parser, and for additions to the Java language accepted by KeY,
-`SchemaJavaParser.jj` and `ProofJavaParser.jj` will have to be changed. The best
+`(Java)KeYParser.g4` accordingly and for creating new transformers or language
+extensions, the JavaParser
+is the relevant parser. The best
 advice here is to have a look at the existing definitions to see how to add
 a new one. Note that at the same time when extending the parser by new
 transformers or statement types, you will also have to add new Java classes and
 extend factories. We cover this in the next section.
 
 ### New Program Statement / Expression Types
 
-There are two categories of extensions: (1) New program schema variable sorts, which match existing programming language fragments, and (2) extensions to the language, e.g. by artificial constructs needed for a proof / symbolic execution technique.
+There are two categories of extensions: (1) New program schema variable sorts,
+which match existing programming language fragments, and (2) extensions to the
+language, e.g. by artificial constructs needed for a proof / symbolic
+execution technique.
 
 A new "matcher sort" for taclets is added quite easily. As an example, take the
 "loop init" clause of a for loop. A corresponding schema variable for the use in
 taclets can be declared as `\program LoopInit #loopInit;`. After that,
 `#loopInit` can be used in a taclet to match a loop init clause. It suffices to
-(1) declare a new "program schema variable sort" in
+declare a new "program schema variable sort" in
 `de.uka.ilkd.key.logic.sort.ProgramSVSort` (for instance `LoopInitSort` in the
 example) which calls the constructor of `ProgramSVSort` with the identifier by
-which it later should be referred to in taclet definitions, and (2) to use that
-sort in `SchemaJavaParser.jj`. Have a look how `ForInit` is used there to get
-a feeling.
+which it later should be referred to in taclet definitions.
 
 A language extension like the merge points has to be added to several parts in the system: 
 
-1. A parser model extension is added in `src/de/uka/ilkd/key/java/recoderext/`
+1. A parser model extension is added in [JML ToolKit](https://github.com/jmltoolkit/jmltk)
 (see `MergePointStatement.java` for an example).
-2. The factories `de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java`
-and `(...)/ProofJavaProgramFactory.java` are extended by corresponding factory
-methods.
-3. A mirror of the parser extension for the logic side of KeY is added to
+2. A mirror of the parser extension for the logic side of KeY is added to
 `de/uka/ilkd/key/java/statement/` (also here, there's a `MergePointStatement.java`).
-5. A converter for the parser model extension to the logic representation in
-`de/uka/ilkd/key/java/Recoder2KeYConverter.java`. Look what's done for the
-`MergePointStatement`. The methods there are called by reflection, so the name
-of the new method has to be `convert`, and it has to accept the parser model
-extension as only argument.
-6. Extension of Java visitor classes: Classes `Visitor.java`,
+3. A converter for the parser model extension to the logic representation in
+`de/uka/ilkd/key/java/loader/JP2KeYConverter.java`. Look what's done for the
+`MergePointStatement`.
+4. Extension of Java visitor classes: Classes `Visitor.java`,
 `JavaASTVisitor.java`, `CreatingASTVisitor.java`, and `ProgVarReplaceVisitor.java`
-in directory `de/uka/ilkd/key/java/visitor/`. Note that now all of these might 
+in directory `de/uka/ilkd/key/java/visitor/`. Note that not all of these might 
 apply to you, e.g. if your new statement does not contain program variables that
 might have to be substituted in a proof.
-7. Extension of the pretty printer to nicely render your extension in sequents:
+5. Extension of the pretty printer to nicely render your extension in sequents:
 `de/uka/ilkd/key/java/PrettyPrinter.java`.
 
-The factory methods and parser model classes can then be used in
-`{Schema, Proof}JavaParser.jj`.
 
 ### New Meta Constructs / Transformers
 
@@ -200,19 +259,18 @@ for the bad style of delegating everything to a transformer). For adding
 transformers this to the system, follow these steps:
 
 1. Add a model class to the directory `src/de/uka/ilkd/key/rule/metaconstruct/`
-(see e.g. `ForToWhile.java). The class should extend `ProgramTransformer` and
-pass the keyword to be used to the super class, here "#for-to-while".
-2. Extend the class `src/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter` 
-to return the new class when appropriate. Look for `convert(RKeYMetaConstruct)`
-to see what's done for `#for-to-while`.
-3. Add the construct to the parser (`SchemaJavaParser.jj`).
+(see e.g. `ForToWhile.java`). The class should extend `ProgramTransformer` and
+pass the keyword to be used to the super class, here `#for-to-while`.
+2. Extend the `visit(MetaConstruct, Void)` method in `src/de/uka/ilkd/key/java/JP2KeYConverter` 
+to return the new class when appropriate. See what's done for `#for-to-while`.
+3. Add the construct to [the parser](https://github.com/jmltoolkit/jmltk).
 
 ### Completions
 
 Sometimes the input to a taclet depends on other information than that available
 from a current proof situation (i.e., a sequent). In that case, the rule has to
 be completed before it is applied. A good example is the rule "cut"
-(`resources/de/uka/ilkd/key/proof/rules/propRule.key`) defined as follows:
+(`resources/de/uka/ilkd/key/proof/rules/classicalLogic/propRule.key`) defined as follows:
 
 ```key
 \schemaVariables {