Introduce ScriptCommandAst to keep the ProofEngine separated from ANTLR's parse tree

Author: wadoon

build.gradle

@@ -101,6 +101,7 @@ subprojects {
         testImplementation ("org.junit.jupiter:junit-jupiter-params")
         testRuntimeOnly ("org.junit.jupiter:junit-jupiter-engine")
         testRuntimeOnly ("org.junit.platform:junit-platform-launcher")
+        testImplementation ("org.assertj:assertj-core:3.26.3")
         testImplementation project(':key.util')
 
         // test fixtures

key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java

@@ -6,14 +6,18 @@
 import java.net.URI;
 import java.net.URISyntaxException;
 import java.net.URL;
+import java.util.ArrayList;
+import java.util.HashMap;
 import java.util.List;
 
+import de.uka.ilkd.key.java.Position;
 import de.uka.ilkd.key.nparser.builder.BuilderHelpers;
 import de.uka.ilkd.key.nparser.builder.ChoiceFinder;
 import de.uka.ilkd.key.nparser.builder.FindProblemInformation;
 import de.uka.ilkd.key.nparser.builder.IncludeFinder;
 import de.uka.ilkd.key.parser.Location;
 import de.uka.ilkd.key.proof.init.Includes;
+import de.uka.ilkd.key.scripts.ScriptCommandAst;
 import de.uka.ilkd.key.settings.Configuration;
 import de.uka.ilkd.key.settings.ProofSettings;
 import de.uka.ilkd.key.speclang.njml.JmlParser;
@@ -48,7 +52,8 @@ protected KeyAst(@NonNull T ctx) {
         this.ctx = ctx;
     }
 
-    public <T> T accept(ParseTreeVisitor<T> visitor) {
+    /// Apply the given `visitor` to the underlying ANTLR4 parse tree.
+    public <R> R accept(ParseTreeVisitor<R> visitor) {
         return ctx.accept(visitor);
     }
 
@@ -57,22 +62,27 @@ public String toString() {
         return getClass().getName() + ": " + BuilderHelpers.getPosition(ctx);
     }
 
+    /// Returns the start location of the first character of the first token of the underlying parse
+    /// tree.
     public Location getStartLocation() {
         return Location.fromToken(ctx.start);
     }
 
+    /// Get the text of the parse tree as a cut out of the original input stream.
+    /// Hence, Spaces and comments should be preserved.
     public String getText() {
         var interval = new Interval(ctx.start.getStartIndex(), ctx.stop.getStopIndex() + 1);
         return ctx.start.getInputStream().getText(interval);
     }
 
+    /// An AST representing a complete KeY file.
     public static class File extends KeyAst<KeYParser.FileContext> {
         File(KeYParser.FileContext ctx) {
             super(ctx);
         }
 
-        @Nullable
-        public ProofSettings findProofSettings() {
+        /// Returns proof settings (aka `\settings`) if found in the parse tree.
+        public @Nullable ProofSettings findProofSettings() {
             ProofSettings settings = new ProofSettings(ProofSettings.DEFAULT_SETTINGS);
 
             if (ctx.preferences() != null && ctx.preferences().s != null) {
@@ -100,7 +110,6 @@ public ProofSettings findProofSettings() {
             if (ctx.problem() != null && ctx.problem().proofScriptEntry() != null) {
                 KeYParser.ProofScriptEntryContext pctx = ctx.problem().proofScriptEntry();
 
-                KeYParser.ProofScriptContext ps;
                 if (pctx.STRING_LITERAL() != null) {
                     var ctx = pctx.STRING_LITERAL().getSymbol();
                     String text = pctx.STRING_LITERAL().getText();
@@ -117,25 +126,34 @@ public ProofSettings findProofSettings() {
             return null;
         }
 
+        /// Returns the includes (possible empty but not null) computed from the underlying parse
+        /// tree.
         public Includes getIncludes(URL base) {
             IncludeFinder finder = new IncludeFinder(base);
             accept(finder);
             return finder.getIncludes();
         }
 
+        /// Returns the information on choices from the underlying parse tree.
         public ChoiceInformation getChoices() {
             ChoiceFinder finder = new ChoiceFinder();
             accept(finder);
             return finder.getChoiceInformation();
         }
 
+        /// Returns information on `\problem`, `\proofObligation` or `\chooseContract` using the
+        /// underlying
+        /// parse tree.
         public ProblemInformation getProblemInformation() {
             FindProblemInformation fpi = new FindProblemInformation();
             ctx.accept(fpi);
             return fpi.getProblemInformation();
         }
 
-        public Token findProof() {
+        /// Returns the token `\proof` in the underlying parse tree.`
+        /// This token also marks the end of the parse tree (EOF) but not the end of the file.
+        /// Positional information of the token is used to set up the proof replayer.
+        public @Nullable Token findProof() {
             KeYParser.ProofContext a = ctx.proof();
             if (a != null) {
                 return a.PROOF().getSymbol();
@@ -177,7 +195,7 @@ public Configuration asConfiguration() {
             final var cfg = new ConfigurationBuilder();
             List<Object> res = cfg.visitCfile(ctx);
             if (!res.isEmpty())
-                return (Configuration) res.get(0);
+                return (Configuration) res.getFirst();
             else
                 throw new RuntimeException("Error in configuration. Source: "
                     + ctx.start.getTokenSource().getSourceName());
@@ -234,7 +252,7 @@ public static class ProofScript extends KeyAst<KeYParser.ProofScriptContext> {
             super(ctx);
         }
 
-        public URI getUrl() {
+        public URI getUri() {
             final var sourceName = ctx.start.getTokenSource().getSourceName();
             try {
                 if (sourceName.startsWith("file:") || sourceName.startsWith("http:")
@@ -244,5 +262,42 @@ public URI getUrl() {
             }
             return new java.io.File(sourceName).toURI();
         }
+
+        /// Translates this parse tree into an AST usable for the proof script engine.
+        /// The current representation of a proof script is a list of commands. Each command
+        /// can hold a list of sub-commands.
+        ///
+        /// @return a non-null list of the parsed commands.
+        public List<ScriptCommandAst> asAst() {
+            var fileUri = getUri();
+            return asAst(fileUri, ctx.proofScriptCommand());
+        }
+
+        private List<ScriptCommandAst> asAst(URI file,
+                List<KeYParser.ProofScriptCommandContext> cmds) {
+            return cmds.stream().map(it -> asAst(file, it)).toList();
+        }
+
+        private @NonNull ScriptCommandAst asAst(URI file, KeYParser.ProofScriptCommandContext it) {
+            var loc = new Location(file, Position.fromToken(it.start));
+            var sub = it.sub != null
+                    ? asAst(file, it.sub.proofScriptCommand())
+                    : null;
+
+            var nargs = new HashMap<String, Object>();
+            var pargs = new ArrayList<>();
+
+            if (it.proofScriptParameters() != null) {
+                for (var param : it.proofScriptParameters().proofScriptParameter()) {
+                    if (param.pname != null) {
+                        nargs.put(param.pname.getText(), param.expr);
+                    } else {
+                        pargs.add(param.expr);
+                    }
+                }
+            }
+
+            return new ScriptCommandAst(it.cmd.getText(), nargs, pargs, sub, loc);
+        }
     }
 }

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

@@ -5,7 +5,7 @@
 
 import java.util.ArrayList;
 import java.util.List;
-import java.util.Map;
+import java.util.Objects;
 
 import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
 import de.uka.ilkd.key.java.Services;
@@ -26,10 +26,9 @@
 /// {@link AbstractCommand}. You need to override [AbstractCommand#execute(Object)] to implement the
 /// command logic.
 ///
-/// @param <T> the expected parameter class
 /// @author Alexander Weigl
 @NullMarked
-public abstract class AbstractCommand<T> implements ProofScriptCommand<T> {
+public abstract class AbstractCommand implements ProofScriptCommand {
     protected @Nullable Proof proof;
     protected @Nullable Services service;
     protected @Nullable EngineState state;
@@ -40,34 +39,30 @@ public abstract class AbstractCommand<T> implements ProofScriptCommand<T> {
      */
     protected @Nullable String documentation = null;
 
+    protected final EngineState state() {
+        return Objects.requireNonNull(state);
+    }
+
     /**
      * ...
      */
-    private final Class<T> parameterClazz;
+    private final @Nullable Class<?> parameterClazz;
 
-    protected AbstractCommand(Class<T> clazz) {
+    protected AbstractCommand(@Nullable Class<?> clazz) {
         this.parameterClazz = clazz;
     }
 
-    public List<ProofScriptArgument<T>> getArguments() {
+    public List<ProofScriptArgument> getArguments() {
         if (parameterClazz == null) {
             return new ArrayList<>();
         }
-        return ArgumentsLifter.inferScriptArguments(parameterClazz, this);
+        return ArgumentsLifter.inferScriptArguments(parameterClazz);
     }
 
 
     @Override
-    public T evaluateArguments(EngineState state, Map<String, Object> arguments) throws Exception {
-        if (parameterClazz != null) {
-            T obj = parameterClazz.getDeclaredConstructor().newInstance();
-            return state.getValueInjector().inject(this, obj, arguments);
-        }
-        return null;
-    }
-
-    @Override
-    public void execute(AbstractUserInterfaceControl uiControl, T args, EngineState stateMap)
+    public final void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
+            EngineState stateMap)
             throws ScriptException, InterruptedException {
         proof = stateMap.getProof();
         service = proof.getServices();
@@ -89,11 +84,16 @@ public void execute(AbstractUserInterfaceControl uiControl, T args, EngineState
     /// @param args an instance of the parameters
     /// @throws ScriptException if something happened during execution
     /// @throws InterruptedException if thread was interrupted during execution
-    protected void execute(T args) throws ScriptException, InterruptedException {
+    public void execute(ScriptCommandAst args) throws ScriptException, InterruptedException {
     }
 
     @Override
     public String getDocumentation() {
-        return "";
+        if (documentation == null && parameterClazz != null) {
+            documentation =
+                ArgumentsLifter.extractDocumentation(getName(), getClass(), parameterClazz);
+        }
+        return Objects.requireNonNullElse(documentation, "");
     }
+
 }

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

@@ -25,7 +25,8 @@ public String getDocumentation() {
     }
 
     @Override
-    public void execute(AbstractUserInterfaceControl uiControl, Void args, EngineState state)
+    public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
+            EngineState state)
             throws ScriptException, InterruptedException {
         Goal goal = state.getFirstOpenGoal(false);
         goal.setEnabled(true);

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

@@ -4,30 +4,23 @@
 package de.uka.ilkd.key.scripts;
 
 import java.util.List;
-import java.util.Map;
 
 import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
-import de.uka.ilkd.key.nparser.KeYParser;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.scripts.meta.ProofScriptArgument;
 
-public class AllCommand implements ProofScriptCommand<Map<String, Object>> {
+public class AllCommand implements ProofScriptCommand {
     private String documentation;
 
     @Override
-    public List<ProofScriptArgument<Map<String, Object>>> getArguments() {
+    public List<ProofScriptArgument> getArguments() {
         return List.of();
     }
 
     @Override
-    public Map<String, Object> evaluateArguments(EngineState state, Map<String, Object> arguments) {
-        return arguments;
-    }
-
-    @Override
-    public void execute(AbstractUserInterfaceControl uiControl, Map<String, Object> args,
+    public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
             EngineState stateMap) throws ScriptException, InterruptedException {
-        var block = (KeYParser.ProofScriptContext) args.get(ProofScriptEngine.KEY_SUB_SCRIPT);
+        var block = args.commands();
 
         if (block == null) {
             throw new ScriptException("Missing command to apply onAll to");
@@ -38,7 +31,7 @@ public void execute(AbstractUserInterfaceControl uiControl, Map<String, Object>
         for (Goal g : proof.openGoals()) {
             // if (isBelow(g, selectedNode)) {
             stateMap.setGoal(g);
-            stateMap.getEngine().execute(uiControl, block.proofScriptCommand());
+            stateMap.getEngine().execute(uiControl, block);
             // }
         }
         // state.setGoal(selectedNode);

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

@@ -3,16 +3,18 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.scripts;
 
-import java.util.Map;
 
+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
  */
-public class AssertCommand extends AbstractCommand<AssertCommand.Parameters> {
+public class AssertCommand extends AbstractCommand {
 
     /**
      * Instantiates a new assert command.
@@ -22,21 +24,16 @@ public AssertCommand() {
     }
 
     @Override
-    public Parameters evaluateArguments(EngineState state,
-            Map<String, Object> arguments) throws Exception {
-        return state.getValueInjector().inject(this, new Parameters(),
-            arguments);
-    }
+    public void execute(ScriptCommandAst arguments) throws ScriptException, InterruptedException {
+        var args = state().getValueInjector().inject(new Parameters(), arguments);
 
-    @Override
-    public void execute(Parameters args) throws ScriptException, InterruptedException {
         if (args.goals == null) {
             throw new ScriptException("No parameter specified!");
         }
 
-        if (state.getProof().openEnabledGoals().size() != args.goals) {
+        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);
         }
     }
 
@@ -48,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.