I found this paragraph about meta constructs in the docs:
|
### New Meta Constructs / Transformers |
|
|
|
Meta constructs give additional powers to taclets. By them, it is even possible |
|
to create taclets which are actually built-in rules since all the work (maybe |
|
except for some matcher preprocessing) is deferred to a powerful transformer. |
|
Note that we discourage from using that style; meta constructs should be used at |
|
a very small scope. If that's not possible, directly using built-in rules is |
|
a more "honest" and better maintainable approach. |
|
|
|
Our running example here is the `#for-to-while` construct (actually an example |
|
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`). |
Is is still relevant for modern KeY versions? As far as I can tell these constructs are no longer used.
cc @WolframPfeifer