Add support for generation of varcond documentation

build.gradle

@@ -84,6 +84,9 @@ subprojects {
         testImplementation(libs.logback.classic)
 
 
+        // Therapi runtime javadoc
+        annotationProcessor 'com.github.therapi:therapi-runtime-javadoc-scribe:0.13.0'
+        implementation 'com.github.therapi:therapi-runtime-javadoc:0.13.0'
         compileOnly(libs.jspecify)
         testCompileOnly(libs.jspecify)
         compileOnly(libs.checkerframework.qual)
@@ -316,7 +319,6 @@ subprojects {
             afterEvaluate {
                 description = project.description
                 assert (project.description != null && project.description != "") : "Description of modules are required at maven-central"
-                print(project.description)
             }
             url = 'https://key-project.org/'
 

gradle/libs.versions.toml

@@ -25,6 +25,7 @@ stringtemplate = "4.3.4"
 javapoet = "1.13.0"
 javaparser = "3.28.0-K13.6"
 truth = "1.4.5"
+therapi = "0.13.0"
 
 # UI and CLI
 flatlaf = "3.7.2"
@@ -35,6 +36,7 @@ docking-frames = "1.1.3p1"
 # External tools
 scala-isabelle = "0.4.5"
 
+
 [libraries]
 # SLF4J and logging
 slf4j-api = { module = "org.slf4j:slf4j-api", version.ref = "slf4j" }
@@ -43,6 +45,10 @@ logback-classic = { module = "ch.qos.logback:logback-classic", version.ref = "lo
 # JSpecify (nullability annotations)
 jspecify = { module = "org.jspecify:jspecify", version.ref = "jspecify" }
 
+#Extracting Javadoc
+therapi-processor = { module = "com.github.therapi:therapi-runtime-javadoc-scribe", version.ref = "therapi" }
+therapi-runtime = { module = "com.github.therapi:therapi-runtime-javadoc", version.ref = "therapi" }
+
 # EISOP Checker Framework
 checkerframework-qual = { module = "io.github.eisop:checker-qual", version.ref = "eisop" }
 checkerframework-util = { module = "io.github.eisop:checker-util", version.ref = "eisop" }

key.core/build.gradle

@@ -24,6 +24,9 @@ dependencies {
     testImplementation(libs.truth)
     testImplementation(project(":key.core"))
 
+    annotationProcessor(libs.therapi.processor)
+    api(libs.therapi.runtime)
+
     // https://mvnrepository.com/artifact/com.fasterxml.jackson.dataformat/jackson-dataformat-yaml
     testImplementation(libs.jackson.dataformat.yaml)
 
@@ -32,7 +35,7 @@ dependencies {
 }
 
 tasks.withType(JavaCompile).configureEach {
-    options.compilerArgs << "-Ajavadoc.packages=de.uka.ilkd.key.scripts"
+    options.compilerArgs << "-Ajavadoc.packages=de.uka.ilkd.key.scripts,de.uka.ilkd.key.rule.conditions"
 }
 
 // The target directory for JavaCC (parser generation)

key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java

@@ -0,0 +1,27 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.doc;
+
+import java.util.ArrayList;
+import java.util.Comparator;
+
+import de.uka.ilkd.key.scripts.ProofScriptCommand;
+import de.uka.ilkd.key.scripts.ProofScriptEngine;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (23.08.26)
+ */
+public class ScriptDoc {
+    public static void main(String[] args) {
+        var commands = new ArrayList<>(ProofScriptEngine.loadCommands().values());
+        commands.sort(Comparator.comparing(ProofScriptCommand::getName));
+
+        for (var command : commands) {
+            System.out.println(command.getDocumentation());
+            System.out.println("\n\n\n");
+        }
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java

@@ -0,0 +1,107 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.doc;
+
+import java.util.Arrays;
+import java.util.Comparator;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+import de.uka.ilkd.key.nparser.varexp.TacletBuilderCommand;
+import de.uka.ilkd.key.nparser.varexp.TacletBuilderCommandInfo;
+import de.uka.ilkd.key.nparser.varexp.TacletBuilderManipulators;
+
+import com.github.javaparser.ParserConfiguration;
+import com.github.javaparser.StaticJavaParser;
+import com.github.therapi.runtimejavadoc.CommentFormatter;
+import com.google.common.collect.Streams;
+import org.jspecify.annotations.Nullable;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (23.08.26)
+ */
+public class VarcondDoc {
+    // region
+    public static void main(String[] args) {
+        var config = new ParserConfiguration();
+        config.setLanguageLevel(ParserConfiguration.LanguageLevel.JAVA_21);
+        StaticJavaParser.setConfiguration(config);
+
+        Function<String, String> normalizeCmdName =
+            (String it) -> it.startsWith("\\") ? it.replace("\\\\", "\\") : "\\" + it;
+        Function<TacletBuilderCommandInfo, String> getTriggerName = TacletBuilderCommandInfo::name;
+
+        var g = TacletBuilderManipulators.getConditionBuilders().stream()
+                .map(TacletBuilderCommand::getInformation)
+                .collect(Collectors.groupingBy(getTriggerName.andThen(normalizeCmdName)));
+        Comparator<TacletBuilderCommandInfo> reversed =
+            Comparator.comparing((TacletBuilderCommandInfo it) -> it.argumentTypes().length)
+                    .reversed();
+
+        var conds = g.keySet().stream().sorted().toList();
+
+        for (var name : conds) {
+            var cmds = g.get(name);
+            System.out.println();
+            System.out.println();
+            System.out.format("### `%s`\n\n", name);
+            cmds.sort(reversed);
+
+            final var generalDocumentation = cmds.getFirst().getGeneralDocumentation();
+            System.out.println(
+                cleanJavadoc(new CommentFormatter().format(generalDocumentation.getComment())));
+
+            System.out.format("\n**Signatures**\n\n");
+            for (TacletBuilderCommandInfo cmd : cmds) {
+
+                final var arguments = Streams.zip(
+                    Arrays.stream(cmd.argNames()),
+                    Arrays.stream(cmd.argumentTypes()).map(Enum::toString),
+                    "%s: %s"::formatted)
+                        .collect(Collectors.joining(", "));
+                System.out.printf("* `%s(%s)`\n", name, arguments);
+
+                if (cmd.isNegationSupported()) {
+                    System.out.printf("* `\\not%s(%s)`\n", name, arguments);
+                }
+
+                System.out.println();
+                final var argumentInformation = cmd.getArgumentInformation();
+
+                System.out.println(
+                    indent("   ", cleanJavadoc(argumentInformation.getComment().toString())));
+                System.out.println();
+                argumentInformation.getParams().stream()
+                        .map(tag -> "   * `%s` %s".formatted(tag.getName(), tag.getComment()))
+                        .forEach(System.out::println);
+                System.out.println();
+            }
+        }
+    }
+
+    private static String indent(String spaces, String it) {
+        return spaces + it.replace("\n", "\n" + spaces);
+    }
+
+    private static String cleanJavadoc(@Nullable String it) {
+        if (it == null)
+            it = "";
+        return it.replace("<tt>", "`")
+                .replace("<ul>", "\n")
+                .replace("</ul>", "\n")
+                .replace("<ul>", "\n")
+                .replace("<li>", "* ")
+                .replace("</li>", "")
+                .replace("{@link", "`")
+                .replace("}", "`")
+                .replace("<code>", "`")
+                .replace("</tt>", "`")
+                .replace("</code>", "`")
+                .replace("<b>", "**")
+                .replace("</b>", "**");
+    }
+    // endregion
+}

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java

@@ -800,7 +800,7 @@ public Object visitVarexp(JavaKeYParser.VarexpContext ctx) {
         }
         if (!applied) {
             LOGGER.warn("Found name-matching conditions with following type signature:");
-            suitableManipulators.forEach(it -> LOGGER.warn(Arrays.toString(it.getArgumentTypes())));
+            suitableManipulators.forEach(it -> LOGGER.warn(it.getArgumentTypes().toString()));
             LOGGER.warn("But you gave {} arguments.\n", arguments.size());
             semanticError(ctx, "Could not apply the given variable condition: %s", ctx.getText());
         }

key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractConditionBuilder.java

@@ -3,16 +3,20 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.nparser.varexp;
 
-import org.jspecify.annotations.NonNull;
+import org.key_project.prover.rules.VariableCondition;
 
 /**
  * @author Alexander Weigl
  * @version 1 (12/9/19)
  */
 public abstract class AbstractConditionBuilder extends AbstractTacletBuilderCommand
         implements ConditionBuilder {
-    protected AbstractConditionBuilder(@NonNull String triggerName,
-            @NonNull ArgumentType... argumentsTypes) {
-        super(triggerName, argumentsTypes);
+    protected AbstractConditionBuilder(TacletBuilderCommandInfo info) {
+        super(info);
+    }
+
+    public AbstractConditionBuilder(String name, Class<? extends VariableCondition> clazz,
+            boolean negationSupported, ArgumentType... types) {
+        super(TacletBuilderCommandInfo.createVarcondInfo(name, clazz, negationSupported, types));
     }
 }

key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractTacletBuilderCommand.java

@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.nparser.varexp;
 
-import org.jspecify.annotations.NonNull;
 
 /**
  * Simple default implementation for {@link TacletBuilderCommand}.
@@ -12,36 +11,26 @@
  * @version 1 (12/9/19)
  */
 public abstract class AbstractTacletBuilderCommand implements TacletBuilderCommand {
-    private final @NonNull String triggerName;
-    private final @NonNull ArgumentType[] argumentsTypes;
+    protected final TacletBuilderCommandInfo info;
 
-    /**
-     * Construct this class with the parameters for {@link #isSuitableFor(String)} and
-     * {@link #getArgumentTypes()}.
-     *
-     * @param triggerName the name of this command.
-     * @param argumentsTypes the argument type of this command.
-     */
-    protected AbstractTacletBuilderCommand(@NonNull String triggerName,
-            @NonNull ArgumentType... argumentsTypes) {
-        this.triggerName = triggerName;
-        this.argumentsTypes = argumentsTypes;
+    protected AbstractTacletBuilderCommand(TacletBuilderCommandInfo info) {
+        this.info = info;
     }
 
     @Override
-    public boolean isSuitableFor(@NonNull String name) {
-        if (triggerName.equalsIgnoreCase(name)) {
+    public boolean isSuitableFor(String name) {
+        if (info.name().equalsIgnoreCase(name)) {
             return true;
         }
-        if (name.startsWith("\\")) // handling leading backslashes
-        {
+        // handling leading backslashes
+        if (name.startsWith("\\")) {
             return isSuitableFor(name.substring(1));
         }
         return false;
     }
 
     @Override
-    public ArgumentType[] getArgumentTypes() {
-        return argumentsTypes;
+    public TacletBuilderCommandInfo getInformation() {
+        return info;
     }
 }

key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ArgumentType.java

@@ -12,14 +12,19 @@
 
 /**
  * Argument types for {@link TacletBuilderCommand}s.
+ * Each {@link ArgumentType} has an expected class for the type of the argument.
  *
  * @author Alexander Weigl
  * @version 1 (12/9/19)
  * @see TacletBuilderCommand
  */
 public enum ArgumentType {
-    TYPE_RESOLVER(TypeResolver.class), SORT(Sort.class), TERM(JTerm.class),
-    JAVA_TYPE(KeYJavaType.class), VARIABLE(ParsableVariable.class), STRING(String.class);
+    TYPE_RESOLVER(TypeResolver.class),
+    SORT(Sort.class),
+    TERM(JTerm.class),
+    JAVA_TYPE(KeYJavaType.class),
+    VARIABLE(ParsableVariable.class),
+    STRING(String.class);
 
     public final Class<?> clazz;
 

key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java

@@ -12,39 +12,26 @@
 
 public class ConstructorBasedBuilder extends AbstractConditionBuilder {
     private final Class<? extends VariableCondition> clazz;
-    private final boolean negationSupported;
 
     public ConstructorBasedBuilder(String name, Class<? extends VariableCondition> clazz,
             ArgumentType... types) {
-        this(name, lastArgumentOfFirstContructorIsBoolean(clazz), clazz, types);
+        this(TacletBuilderCommandInfo.createVarcondInfo(name, clazz, types), clazz);
     }
 
-    private static boolean lastArgumentOfFirstContructorIsBoolean(
+    public ConstructorBasedBuilder(TacletBuilderCommandInfo info,
             Class<? extends VariableCondition> clazz) {
-        try {
-            Class<?>[] types = clazz.getConstructors()[0].getParameterTypes();
-            return types[types.length - 1] == Boolean.class
-                    || types[types.length - 1] == Boolean.TYPE;
-        } catch (ArrayIndexOutOfBoundsException e) {
-            return false;
-        }
-    }
-
-    public ConstructorBasedBuilder(String name, boolean negationSupported,
-            Class<? extends VariableCondition> clazz, ArgumentType... types) {
-        super(name, types);
+        super(info);
         this.clazz = clazz;
-        this.negationSupported = negationSupported;
     }
 
     @Override
     public VariableCondition build(Object[] arguments, List<String> parameters, boolean negated) {
-        if (negated && !negationSupported) {
+        if (negated && !info.isNegationSupported()) {
             throw new RuntimeException(clazz.getName() + " does not support negation.");
         }
 
         Object[] args = arguments;
-        if (negationSupported) {
+        if (info.isNegationSupported()) {
             args = Arrays.copyOf(arguments, arguments.length + 1);
             args[args.length - 1] = negated;
         }
@@ -58,4 +45,9 @@ public VariableCondition build(Object[] arguments, List<String> parameters, bool
         }
         throw new RuntimeException();
     }
+
+    @Override
+    public TacletBuilderCommandInfoImpl getInformation() {
+        return (TacletBuilderCommandInfoImpl) super.getInformation();
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommand.java

@@ -27,6 +27,9 @@ public interface TacletBuilderCommand {
      */
     boolean isSuitableFor(@NonNull String name);
 
+    /// Returns information about this command.
+    TacletBuilderCommandInfo getInformation();
+
     /**
      * Defines the amount and type of expected arguments. For example, if you want describe a
      * sub-type test (instanceOf) you would need two sorts {@code new ArgumentType[]{SORT,SORT} } as
@@ -38,7 +41,9 @@ public interface TacletBuilderCommand {
      *
      * @see ArgumentType
      */
-    ArgumentType[] getArgumentTypes();
+    default ArgumentType[] getArgumentTypes() {
+        return getInformation().argumentTypes();
+    }
 
     /**
      * Applying this command on the given taclet builder.