added psg4-cleaned-continued

Author: mattulbrich

key.core/src/main/antlr4/KeYLexer.g4

@@ -480,6 +480,7 @@ MODAILITYGENERIC:
       -> more, pushMode(modGeneric);
 */
 //BACKSLASH:  '\\';
+
 ERROR_UKNOWN_ESCAPE: '\\' IDENT;
 ERROR_CHAR: .;
 

key.core/src/main/java/de/uka/ilkd/key/scripts/AbstractCommand.java

@@ -60,15 +60,6 @@ public List<ProofScriptArgument> getArguments() {
     }
 
 
-    public @Nullable Object evaluateArguments(EngineState state, ScriptCommandAst arguments)
-            throws Exception {
-        if (parameterClazz != null) {
-            Object obj = parameterClazz.getDeclaredConstructor().newInstance();
-            return state.getValueInjector().inject(this, obj, arguments);
-        }
-        return null;
-    }
-
     @Override
     public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
             EngineState stateMap)
@@ -98,6 +89,10 @@ public void execute(ScriptCommandAst args) throws ScriptException, InterruptedEx
 
     @Override
     public String getDocumentation() {
-        return "";
+        if (documentation == null) {
+            documentation = ArgumentsLifter.extractDocumentation(parameterClazz);
+        }
+        return documentation;
     }
+
 }

key.core/src/main/java/de/uka/ilkd/key/scripts/AssertCommand.java

@@ -4,10 +4,13 @@
 package de.uka.ilkd.key.scripts;
 
 
+import de.uka.ilkd.key.scripts.meta.Documentation;
 import de.uka.ilkd.key.scripts.meta.Option;
 
 /**
  * Halts the script if some condition is not met.
+ * <p>
+ * See exported documentation at {@link Parameters} at the end of this file.
  *
  * @author lanzinger
  */
@@ -30,7 +33,7 @@ public void execute(ScriptCommandAst arguments) throws ScriptException, Interrup
 
         if (state().getProof().openEnabledGoals().size() != args.goals) {
             throw new ScriptException("Assertion failed: number of open goals is "
-                + state.getProof().openGoals().size() + ", but should be " + args.goals);
+                + state().getProof().openGoals().size() + ", but should be " + args.goals);
         }
     }
 
@@ -42,6 +45,15 @@ public String getName() {
     /**
      * The Assigned parameters (currently only the passed goals).
      */
+    @Documentation("""
+            The assert command checks if the number of open and enabled goals is equal to the given number.
+            If not, the script is halted with an error message.
+
+            Deprecated: This command is deprecated and should not be used in new scripts.
+            The name of this command is likely to change since "assert" will
+            be used for a more general purpose. You may find that this is called
+            "failUnless".
+            """)
     public static class Parameters {
         /**
          * The number of open and enabled goals.

key.core/src/main/java/de/uka/ilkd/key/scripts/AssumeCommand.java

@@ -4,40 +4,73 @@
 package de.uka.ilkd.key.scripts;
 
 
+import de.uka.ilkd.key.logic.ChoiceExpr;
+import de.uka.ilkd.key.logic.SequentFormula;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.rule.NoPosTacletApp;
-import de.uka.ilkd.key.rule.Taclet;
-import de.uka.ilkd.key.rule.TacletApp;
+import de.uka.ilkd.key.logic.TermFactory;
+import de.uka.ilkd.key.logic.op.FormulaSV;
+import de.uka.ilkd.key.logic.op.SchemaVariable;
+import de.uka.ilkd.key.logic.op.SchemaVariableFactory;
+import de.uka.ilkd.key.rule.*;
+import de.uka.ilkd.key.rule.tacletbuilder.TacletGoalTemplate;
+import de.uka.ilkd.key.scripts.meta.Documentation;
 import de.uka.ilkd.key.scripts.meta.Option;
-
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
 import org.key_project.logic.Name;
-import org.key_project.logic.op.sv.SchemaVariable;
+import org.key_project.util.collection.DefaultImmutableMap;
+import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.collection.ImmutableSet;
 
 /**
- * The assume command takes one argument: * a formula to which the command is applied
+ * The assume statement for proof debugging purposes
+ * <p>
+ * See exported documentation at @{@link FormulaParameter} at the end of this file.
  */
+@NullMarked
 public class AssumeCommand extends AbstractCommand {
     private static final Name TACLET_NAME = new Name("UNSOUND_ASSUME");
 
+    /**
+     * The taclet that is used to implement the assume command.
+     * <p>
+     * The taclet UNSOUND_ASSUME { \add( b ==> ) } is obviously unsound, but it is used for
+     * debugging
+     * purposes. It is constructed programmatically here, because it should not show up in the
+     * sources
+     * of the key repository.
+     * <p>
+     * (Earlier versions had the unsound axion taclet amongst the axioms in KeY and special-cased
+     * around it.)
+     */
+    private static @Nullable Taclet assumeTaclet;
+
     public AssumeCommand() {
         super(FormulaParameter.class);
     }
 
-    @Override
-    public String getName() {
-        return "assume";
+    private static @NonNull Taclet createAssumeTaclet() {
+        if (assumeTaclet == null) {
+            TacletApplPart applPart = new TacletApplPart(Sequent.EMPTY_SEQUENT, ImmutableList.of(),
+                ImmutableList.of(), ImmutableList.of(), ImmutableList.of());
+            FormulaSV sv = SchemaVariableFactory.createFormulaSV(new Name("b"));
+            Term b = new TermFactory().createTerm(sv);
+            TacletGoalTemplate goal = new TacletGoalTemplate(
+                Sequent.createAnteSequent(new Semisequent(ImmutableList.of(new SequentFormula(b)))),
+                ImmutableList.of());
+            assumeTaclet = new NoFindTaclet(TACLET_NAME, applPart, ImmutableList.of(goal),
+                ImmutableList.of(), new TacletAttributes(),
+                DefaultImmutableMap.nilMap(), ChoiceExpr.TRUE, ImmutableSet.empty());
+        }
+        return assumeTaclet;
     }
 
     @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""";
+    public String getName() {
+        return "assume";
     }
 
-    @Override
     public void execute(ScriptCommandAst arguments) throws ScriptException, InterruptedException {
         var parameter = state().getValueInjector()
                 .inject(this, new FormulaParameter(), arguments);
@@ -52,8 +85,12 @@ public void execute(ScriptCommandAst arguments) throws ScriptException, Interrup
         state().getFirstOpenAutomaticGoal().apply(app);
     }
 
+    @Documentation("""
+            The assume command is an unsound debug command. It takes one argument, a formula,
+            that is added to the antecedent of the current goal. The command is implemented
+            using a local unsound taclet, UNSOUND_ASSUME.""")
     public static class FormulaParameter {
-        @Option("#2")
+        @Option(value = "#2", help = "The formula to be assumed.")
         public Term formula;
     }
 }