remove description in xml files for proof script commands

KeYProject · Jan 20, 2025 · e84c44a · e84c44a
1 parent 7c05a63
commit e84c44a
Show file tree

Hide file tree

Showing 17 changed files with 126 additions and 237 deletions.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java b/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java
@@ -11,6 +11,7 @@
 import de.uka.ilkd.key.java.JavaInfo;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.nparser.KeyAst;
+import de.uka.ilkd.key.nparser.KeyAst.ProofScript;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.Profile;
@@ -48,7 +49,7 @@ public class KeYEnvironment<U extends UserInterfaceControl> {
     /**
      * An optional field denoting a script contained in the proof file.
      */
-    private final KeyAst.@Nullable ProofScript proofScript;
+    private final @Nullable ProofScript proofScript;
 
     /**
      * Indicates that this {@link KeYEnvironment} is disposed.
@@ -78,7 +79,7 @@ public KeYEnvironment(U ui, InitConfig initConfig) {
      * @param proofScript add an optional proof script
      */
     public KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof,
-            KeyAst.@Nullable ProofScript proofScript, ReplayResult replayResult) {
+                          @Nullable ProofScript proofScript, ReplayResult replayResult) {
         this.ui = ui;
         this.initConfig = initConfig;
         this.loadedProof = loadedProof;
@@ -322,7 +323,7 @@ public boolean isDisposed() {
         return disposed;
     }
 
-    public KeyAst.@Nullable ProofScript getProofScript() {
+    public @Nullable ProofScript getProofScript() {
         return proofScript;
     }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AbstractCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AbstractCommand.java
@@ -10,7 +10,6 @@
 import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.macros.scripts.meta.ArgumentsLifter;
-import de.uka.ilkd.key.macros.scripts.meta.DescriptionFacade;
 import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument;
 import de.uka.ilkd.key.proof.Proof;
 
@@ -82,18 +81,10 @@ public void execute(AbstractUserInterfaceControl uiControl, T args, EngineState
      * @throws ScriptException
      * @throws InterruptedException
      */
-    protected void execute(T args) throws ScriptException, InterruptedException {
+    protected void execute(T args) throws ScriptException, InterruptedException {}
 
-    }
-
-    /**
-     * {@inheritDoc}
-     */
     @Override
     public String getDocumentation() {
-        if (documentation == null) {
-            documentation = DescriptionFacade.getDocumentation(this);
-        }
-        return documentation;
+        return "";
     }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ActivateCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ActivateCommand.java
@@ -19,6 +19,11 @@ public String getName() {
         return "activate";
     }
 
+    @Override
+    public String getDocumentation() {
+        return "";
+    }
+
     @Override
     public void execute(AbstractUserInterfaceControl uiControl, Void args, EngineState state)
             throws ScriptException, InterruptedException {

diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AllCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AllCommand.java
@@ -7,7 +7,6 @@
 import java.util.Map;
 
 import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
-import de.uka.ilkd.key.macros.scripts.meta.DescriptionFacade;
 import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument;
 import de.uka.ilkd.key.nparser.KeYParser;
 import de.uka.ilkd.key.proof.Goal;
@@ -56,9 +55,7 @@ public String getName() {
      */
     @Override
     public String getDocumentation() {
-        if (documentation == null) {
-            documentation = DescriptionFacade.getDocumentation(this);
-        }
-        return documentation;
+        return """
+                Applies the given command to all the open goals.""";
     }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssumeCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssumeCommand.java
@@ -3,17 +3,16 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.macros.scripts;
 
-import java.util.Map;
-
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.SchemaVariable;
 import de.uka.ilkd.key.macros.scripts.meta.Option;
 import de.uka.ilkd.key.rule.NoPosTacletApp;
 import de.uka.ilkd.key.rule.Taclet;
 import de.uka.ilkd.key.rule.TacletApp;
-
 import org.key_project.logic.Name;
 
+import java.util.Map;
+
 /**
  * The assume command takes one argument: * a formula to which the command is applied
  */
@@ -26,7 +25,7 @@ public AssumeCommand() {
 
     @Override
     public FormulaParameter evaluateArguments(EngineState state,
-            Map<String, Object> arguments)
+                                              Map<String, Object> arguments)
             throws Exception {
         return state.getValueInjector().inject(this, new FormulaParameter(), arguments);
     }
@@ -36,15 +35,24 @@ public String getName() {
         return "assume";
     }
 
+    @Override
+    public String getDocumentation() {
+        return """
+                The assume command is an unsound taclet rule and takes one argument:
+                
+                The command adds the formula passed as argument to the antecedent
+                a formula #2 to which the command is applied""";
+    }
+
     @Override
     public void execute(FormulaParameter parameter) throws ScriptException, InterruptedException {
         Taclet cut =
-            state.getProof().getEnv().getInitConfigForEnvironment().lookupActiveTaclet(TACLET_NAME);
+                state.getProof().getEnv().getInitConfigForEnvironment().lookupActiveTaclet(TACLET_NAME);
         TacletApp app = NoPosTacletApp.createNoPosTacletApp(cut);
         SchemaVariable sv = app.uninstantiatedVars().iterator().next();
 
         app = app.addCheckedInstantiation(sv, parameter.formula, state.getProof().getServices(),
-            true);
+                true);
         state.getFirstOpenAutomaticGoal().apply(app);
     }
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java
@@ -38,6 +38,11 @@ public String getName() {
         return "auto";
     }
 
+    @Override
+    public String getDocumentation() {
+        return "The AutoCommand invokes the automatic strategy \"Auto\"";
+    }
+
     @Override
     public Parameters evaluateArguments(EngineState state, Map<String, Object> arguments)
             throws ConversionException, ArgumentRequiredException, InjectionReflectionException,

diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/CutCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/CutCommand.java
@@ -3,18 +3,17 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.macros.scripts;
 
-import java.util.Map;
-
 import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.SchemaVariable;
 import de.uka.ilkd.key.macros.scripts.meta.Option;
 import de.uka.ilkd.key.rule.NoPosTacletApp;
 import de.uka.ilkd.key.rule.Taclet;
 import de.uka.ilkd.key.rule.TacletApp;
-
 import org.key_project.logic.Name;
 
+import java.util.Map;
+
 /**
  * The command object CutCommand has as scriptcommand name "cut" As parameters: a formula with the
  * id "#2"
@@ -31,15 +30,23 @@ public String getName() {
         return "cut";
     }
 
+    @Override
+    public String getDocumentation() {
+        return """
+                CutCommand has as script command name "cut"
+                
+                As parameters:
+                * a formula with the id "#2""";
+    }
+
     @Override
     public Parameters evaluateArguments(EngineState state,
-            Map<String, Object> arguments)
+                                        Map<String, Object> arguments)
             throws Exception {
         return state.getValueInjector().inject(this, new Parameters(), arguments);
     }
 
     /**
-     *
      * @param uiControl
      * @param args
      * @param state

diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ExitCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ExitCommand.java
@@ -18,4 +18,9 @@ public void execute(AbstractUserInterfaceControl uiControl, Void args, EngineSta
     public String getName() {
         return "exit";
     }
+
+    @Override
+    public String getDocumentation() {
+        return "Kills the script execution.";
+    }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/InstantiateCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/InstantiateCommand.java
@@ -3,8 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.macros.scripts;
 
-import java.util.Map;
-
 import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.*;
@@ -20,11 +18,12 @@
 import de.uka.ilkd.key.rule.PosTacletApp;
 import de.uka.ilkd.key.rule.Taclet;
 import de.uka.ilkd.key.rule.TacletApp;
-
 import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 
+import java.util.Map;
+
 import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY;
 
 /**
@@ -42,14 +41,14 @@ public InstantiateCommand() {
 
     @Override
     public Parameters evaluateArguments(EngineState state,
-            Map<String, Object> arguments)
+                                        Map<String, Object> arguments)
             throws Exception {
         return state.getValueInjector().inject(this, new Parameters(), arguments);
     }
 
     @Override
     public void execute(AbstractUserInterfaceControl uiControl, Parameters params,
-            EngineState state) throws ScriptException, InterruptedException {
+                        EngineState state) throws ScriptException, InterruptedException {
 
         Goal goal = state.getFirstOpenAutomaticGoal();
 
@@ -71,7 +70,7 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters params,
         SchemaVariable sv = theApp.uninstantiatedVars().iterator().next();
 
         theApp = theApp.addInstantiation(sv, params.with, true /* ??? */,
-            state.getProof().getServices());
+                state.getProof().getServices());
 
         theApp = theApp.tryToInstantiate(state.getProof().getServices());
 
@@ -116,7 +115,7 @@ private ImmutableList<TacletApp> findAllTacletApps(Parameters p, EngineState sta
                 continue;
             }
             allApps = allApps.append(index.getTacletAppAtAndBelow(filter,
-                new PosInOccurrence(sf, PosInTerm.getTopLevel(), true), services));
+                    new PosInOccurrence(sf, PosInTerm.getTopLevel(), true), services));
         }
 
         for (SequentFormula sf : g.node().sequent().succedent()) {
@@ -125,7 +124,7 @@ private ImmutableList<TacletApp> findAllTacletApps(Parameters p, EngineState sta
                 continue;
             }
             allApps = allApps.append(index.getTacletAppAtAndBelow(filter,
-                new PosInOccurrence(sf, PosInTerm.getTopLevel(), false), services));
+                    new PosInOccurrence(sf, PosInTerm.getTopLevel(), false), services));
         }
 
         return allApps;
@@ -138,7 +137,7 @@ private TacletApp filterList(Parameters p, ImmutableList<TacletApp> list) {
         for (TacletApp tacletApp : list) {
             if (tacletApp instanceof PosTacletApp pta) {
                 if (pta.posInOccurrence().subTerm().equalsModProperty(p.formula,
-                    RENAMING_TERM_PROPERTY)) {
+                        RENAMING_TERM_PROPERTY)) {
                     return pta;
                 }
             }
@@ -181,7 +180,7 @@ private void computeFormula(Parameters params, Goal goal) throws ScriptException
         }
 
         throw new ScriptException(
-            "Variable '" + params.var + "' has no occurrence no. '" + params.occ + "'.");
+                "Variable '" + params.var + "' has no occurrence no. '" + params.occ + "'.");
     }
 
     private Term stripUpdates(Term term) {
@@ -219,6 +218,15 @@ public String getName() {
         return "instantiate";
     }
 
+    @Override
+    public String getDocumentation() {
+        return """
+                instantiate var=a occ=2 with="a_8" hide
+                  <p>
+                  instantiate formula="\\forall int a; phi(a)" with="a_8\"
+                """;
+    }
+
     /**
      *
      */

diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/LeaveCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/LeaveCommand.java
@@ -17,6 +17,11 @@ public String getName() {
         return "leave";
     }
 
+    @Override
+    public String getDocumentation() {
+        return "Marks the current goal to be ignored by the macros.";
+    }
+
     @Override
     public void execute(AbstractUserInterfaceControl uiControl, Void args, EngineState state)
             throws ScriptException, InterruptedException {

diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/LetCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/LetCommand.java
@@ -38,7 +38,7 @@ public void execute(AbstractUserInterfaceControl uiControl, Map<String, Object>
 
         for (Map.Entry<String, Object> entry : args.entrySet()) {
             String key = entry.getKey();
-            if (key.startsWith("#") && key.equals("force")) {
+            if (key.startsWith("#") || key.equals("force")) {
                 continue;
             }
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/NoArgumentCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/NoArgumentCommand.java
@@ -7,7 +7,6 @@
 import java.util.List;
 import java.util.Map;
 
-import de.uka.ilkd.key.macros.scripts.meta.DescriptionFacade;
 import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument;
 
 /**
@@ -25,9 +24,4 @@ public Void evaluateArguments(EngineState state,
             Map<String, Object> arguments) {
         return null;
     }
-
-    @Override
-    public String getDocumentation() {
-        return DescriptionFacade.getDocumentation(this);
-    }
 }