Higher Order Proof Scripts (#3654)

Author: wadoon

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

@@ -859,13 +859,12 @@ proofScriptEntry
     | LBRACE proofScript RBRACE
     )
 ;
+
 proofScriptEOF: proofScript EOF;
-proofScript: proofScriptCommand+;
-proofScriptCommand: cmd=IDENT proofScriptParameters?
-	( LBRACE sub=proofScript RBRACE SEMI?
-	| SEMI);
+proofScript: proofScriptCommand*;
+proofScriptCommand: cmd=IDENT proofScriptParameters SEMI;
 
-proofScriptParameters: proofScriptParameter+;
+proofScriptParameters: proofScriptParameter*;
 proofScriptParameter :  ((pname=proofScriptParameterName (COLON|EQUALS))? expr=proofScriptExpression);
 proofScriptParameterName: AT? IDENT; // someone thought, that the let-command parameters should have a leading "@"
 proofScriptExpression:
@@ -878,8 +877,10 @@ proofScriptExpression:
   | simple_ident
   | abbreviation
   | literals
+  | proofScriptCodeBlock
   ;
 
+proofScriptCodeBlock: LBRACE proofScript RBRACE;
 
 // PROOF
 proof: PROOF EOF;

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

@@ -17,6 +17,7 @@
 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.ScriptBlock;
 import de.uka.ilkd.key.scripts.ScriptCommandAst;
 import de.uka.ilkd.key.settings.Configuration;
 import de.uka.ilkd.key.settings.ProofSettings;
@@ -253,7 +254,11 @@ public static class ProofScript extends KeyAst<KeYParser.ProofScriptContext> {
         }
 
         public URI getUri() {
-            final var sourceName = ctx.start.getTokenSource().getSourceName();
+            return getUri(ctx.start);
+        }
+
+        public static URI getUri(Token token) {
+            final var sourceName = token.getTokenSource().getSourceName();
             try {
                 if (sourceName.startsWith("file:") || sourceName.startsWith("http:")
                         || sourceName.startsWith("jar:"))
@@ -273,31 +278,45 @@ public List<ScriptCommandAst> asAst() {
             return asAst(fileUri, ctx.proofScriptCommand());
         }
 
-        private List<ScriptCommandAst> asAst(URI file,
+        private static 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;
+        public static @NonNull ScriptBlock asAst(URI file,
+                KeYParser.ProofScriptCodeBlockContext ctx) {
+            var loc = new Location(file, Position.fromToken(ctx.start));
+            final var proofScriptCommandContexts = ctx.proofScript().proofScriptCommand();
+            final List<ScriptCommandAst> list =
+                proofScriptCommandContexts.stream()
+                        .map(it -> asAst(file, it))
+                        .toList();
+            return new ScriptBlock(list, loc);
+        }
 
+        private static @NonNull ScriptCommandAst asAst(URI file,
+                KeYParser.ProofScriptCommandContext it) {
+            var loc = new Location(file, Position.fromToken(it.start));
             var nargs = new HashMap<String, Object>();
             var pargs = new ArrayList<>();
 
             if (it.proofScriptParameters() != null) {
                 for (var param : it.proofScriptParameters().proofScriptParameter()) {
+                    var expr = param.expr;
+                    Object value = expr;
+                    if (expr.proofScriptCodeBlock() != null) {
+                        value = asAst(file, expr.proofScriptCodeBlock());
+                    }
+
                     if (param.pname != null) {
-                        nargs.put(param.pname.getText(), param.expr);
+                        nargs.put(param.pname.getText(), value);
                     } else {
-                        pargs.add(param.expr);
+                        pargs.add(value);
                     }
                 }
             }
 
-            return new ScriptCommandAst(it.cmd.getText(), nargs, pargs, sub, loc);
+            return new ScriptCommandAst(it.cmd.getText(), nargs, pargs, loc);
         }
     }
 }

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

@@ -10,8 +10,6 @@
 import de.uka.ilkd.key.scripts.meta.ProofScriptArgument;
 
 public class AllCommand implements ProofScriptCommand {
-    private String documentation;
-
     @Override
     public List<ProofScriptArgument> getArguments() {
         return List.of();
@@ -20,21 +18,21 @@ public List<ProofScriptArgument> getArguments() {
     @Override
     public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
             EngineState stateMap) throws ScriptException, InterruptedException {
-        var block = args.commands();
-
-        if (block == null) {
-            throw new ScriptException("Missing command to apply onAll to");
+        if (args.positionalArgs().size() != 1) {
+            throw new ScriptException(
+                "Invalid number of positional arguments to 'onAll'. Pos. arguments: "
+                    + args.positionalArgs().size());
         }
 
+        var block = stateMap.getValueInjector().convert(
+            args.positionalArgs().getFirst(),
+            ScriptBlock.class);
+
         var proof = stateMap.getProof();
-        // Node selectedNode = state.getSelectedNode();
         for (Goal g : proof.openGoals()) {
-            // if (isBelow(g, selectedNode)) {
             stateMap.setGoal(g);
             stateMap.getEngine().execute(uiControl, block);
-            // }
         }
-        // state.setGoal(selectedNode);
     }
 
 

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

@@ -100,6 +100,7 @@ private ValueInjector createDefaultValueInjector() {
         addContextTranslator(v, JTerm.class);
         addContextTranslator(v, Sequent.class);
         addContextTranslator(v, Semisequent.class);
+        addContextTranslator(v, ScriptBlock.class);
         return v;
     }
 

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

@@ -3,9 +3,12 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.scripts;
 
+import java.net.URI;
+
 import de.uka.ilkd.key.nparser.KeYParser;
 import de.uka.ilkd.key.nparser.KeYParser.*;
 import de.uka.ilkd.key.nparser.KeYParserBaseVisitor;
+import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.nparser.builder.ExpressionBuilder;
 
 import org.key_project.prover.sequent.Sequent;
@@ -36,6 +39,12 @@ class ExprEvaluator extends KeYParserBaseVisitor<Object> {
         this.state = engineState;
     }
 
+    @Override
+    public Object visitProofScriptCodeBlock(ProofScriptCodeBlockContext ctx) {
+        URI uri = KeyAst.ProofScript.getUri(ctx.start);
+        return KeyAst.ProofScript.asAst(uri, ctx);
+    }
+
     @Override
     public Object visitBoolean_literal(Boolean_literalContext ctx) {
         return Boolean.parseBoolean(ctx.getText());

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

@@ -22,7 +22,6 @@
 import de.uka.ilkd.key.proof.Proof;
 
 import org.antlr.v4.runtime.RuleContext;
-import org.antlr.v4.runtime.misc.Interval;
 import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
@@ -32,9 +31,6 @@
  * @author Alexander Weigl
  */
 public class ProofScriptEngine {
-    public static final int KEY_START_INDEX_PARAMETER = 2;
-    public static final String KEY_SUB_SCRIPT = "#block";
-    private static final int MAX_CHARS_PER_COMMAND = 80;
     private static final Map<String, ProofScriptCommand> COMMANDS = loadCommands();
     private static final Logger LOGGER = LoggerFactory.getLogger(ProofScriptEngine.class);
 
@@ -117,6 +113,11 @@ public void execute(AbstractUserInterfaceControl uiControl, Proof proof)
         execute(uiControl, script);
     }
 
+    public void execute(AbstractUserInterfaceControl uiControl, ScriptBlock block)
+            throws ScriptException, InterruptedException {
+        execute(uiControl, block.commands());
+    }
+
     public void execute(AbstractUserInterfaceControl uiControl, List<ScriptCommandAst> commands)
             throws InterruptedException, ScriptException {
         if (script.isEmpty()) { // no commands given, no work to do
@@ -199,29 +200,6 @@ public static String prettyPrintCommand(KeYParser.ProofScriptCommandContext ctx)
     }
 
 
-    private Map<String, Object> getArguments(KeYParser.ProofScriptCommandContext commandContext) {
-        var map = new TreeMap<String, Object>();
-        int i = KEY_START_INDEX_PARAMETER;
-
-        if (commandContext.proofScriptParameters() != null) {
-            for (var pc : commandContext.proofScriptParameters().proofScriptParameter()) {
-                String key = pc.pname != null ? pc.pname.getText() : "#" + (i++);
-                map.put(key, pc.expr);
-            }
-        }
-
-        if (commandContext.sub != null) {
-            map.put(KEY_SUB_SCRIPT, commandContext.sub);
-        }
-
-        var in = commandContext.start.getTokenSource().getInputStream();
-        var txt = in.getText(
-            Interval.of(commandContext.start.getStartIndex(), commandContext.stop.getStopIndex()));
-        map.put(ScriptLineParser.LITERAL_KEY, txt);
-        return map;
-    }
-
-
     public EngineState getStateMap() {
         return stateMap;
     }

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

@@ -0,0 +1,38 @@
+/* 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.scripts;
+
+import java.util.List;
+
+import de.uka.ilkd.key.parser.Location;
+
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+
+import static java.util.stream.Collectors.joining;
+
+/// This class represents a block `{ c1; c2; ... ck; }` of proof scripts.
+@NullMarked
+public record ScriptBlock(
+        List<ScriptCommandAst> commands,
+        @Nullable Location location) {
+
+    /// Renders this command a parsable string representation. The order of the arguments is as
+    /// follows:
+    /// key-value arguments, positional arguments and the additional script block.
+    ///
+    /// @see de.uka.ilkd.key.nparser.ParsingFacade#parseScript(org.antlr.v4.runtime.CharStream)
+    public String asCommandLine() {
+        if (commands.isEmpty()) {
+            return " {}";
+        }
+        if (commands.size() == 1) {
+            return " {" + commands.getFirst().asCommandLine() + "}";
+        }
+
+        return " {\n"
+            + commands.stream().map(ScriptCommandAst::asCommandLine).collect(joining("\n"))
+            + "\n}";
+    }
+}

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

@@ -3,11 +3,12 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.scripts;
 
-import java.util.Collections;
 import java.util.List;
 import java.util.Map;
 import java.util.Objects;
 
+import de.uka.ilkd.key.nparser.KeYParser;
+import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.parser.Location;
 
 import org.antlr.v4.runtime.ParserRuleContext;
@@ -20,33 +21,36 @@
 ///
 /// It is an abstraction to the commands of following structure:
 /// ```
-/// <commandName> key_1:value_1 ... key_m:value_m positionalArgs_1 ... positionalArgs_n {
-/// commands_0; ...; commands_k;
-/// }
+/// integer-split
+/// "<0" : { auto; }
+/// "=0" : { instantiate; }
+/// ">0" : { tryclose; }
+/// ;
 /// ```
+/// or
+/// ```
+/// <commandName> key_1:value_1 ... key_m:value_m positionalArgs_1 ... positionalArgs_n;
+/// ```
+/// where `value_X` and `positionalArgs_X` can also be scripts.
 ///
 /// @param commandName the name of the command, e.g., "macro" for `macro auto;`
 /// @param namedArgs a map of the given named arguments and values.
 /// If a named argument is not given, the entry should be missing in the map. Null-values are not
 /// allowed.
 /// @param positionalArgs the list of given positional arguments
-/// @param commands a nullable block of proof script arguments (represents "higher-order proof
-/// scripts").
-/// If null, the block was omitted syntactically in contrast to an empty list.
-/// @param location the location of this command for error reporting.
+/// @param location the location of this command for error reporting. **excluded from equality**
 /// @author Alexander Weigl
 /// @version 1 (14.03.25)
 @NullMarked
 public record ScriptCommandAst(
         String commandName,
         Map<String, Object> namedArgs,
         List<Object> positionalArgs,
-        @Nullable List<ScriptCommandAst> commands,
         @Nullable Location location) {
 
     public ScriptCommandAst(String commandName, Map<String, Object> namedArgs,
             List<Object> positionalArgs) {
-        this(commandName, namedArgs, positionalArgs, Collections.emptyList(), null);
+        this(commandName, namedArgs, positionalArgs, null);
     }
 
     /// Renders this command a parsable string representation. The order of the arguments is as
@@ -56,24 +60,45 @@ public ScriptCommandAst(String commandName, Map<String, Object> namedArgs,
     /// @see de.uka.ilkd.key.nparser.ParsingFacade#parseScript(CharStream)
     public String asCommandLine() {
         return commandName + ' ' +
-                namedArgs.entrySet().stream()
-                        .map(it -> it.getKey() + ": " + asReadableString(it.getValue()))
-                        .collect(joining(" "))
-                + ' '
-                + positionalArgs.stream().map(ScriptCommandAst::asReadableString)
-                        .collect(joining(" "))
-                + (commands != null
-                        ? " {"
-                            + commands.stream().map(ScriptCommandAst::asCommandLine)
-                                    .collect(joining("\n"))
-                            + "\n}"
-                        : ";");
+            namedArgs.entrySet().stream()
+                    .map(it -> it.getKey() + ": " + asReadableString(it.getValue()))
+                    .collect(joining(" "))
+            + ' '
+            + positionalArgs.stream().map(ScriptCommandAst::asReadableString)
+                    .collect(joining(" "))
+            + ";";
     }
 
     public static String asReadableString(Object value) {
+        if (value instanceof ScriptBlock b) {
+            return b.asCommandLine();
+        }
+
+        if (value instanceof KeYParser.ProofScriptCodeBlockContext ctx) {
+            asReadableString(KeyAst.ProofScript.asAst(null, ctx));
+        }
         if (value instanceof ParserRuleContext ctx) {
             return ctx.getText();
         }
         return Objects.toString(value);
     }
+
+    @Override
+    public int hashCode() {
+        return Objects.hash(commandName, namedArgs, positionalArgs);
+    }
+
+    @Override
+    public boolean equals(Object obj) {
+        if (this == obj) {
+            return true;
+        }
+        if (obj == null || getClass() != obj.getClass()) {
+            return false;
+        }
+        ScriptCommandAst other = (ScriptCommandAst) obj;
+        return Objects.equals(commandName, other.commandName)
+                && Objects.equals(positionalArgs, other.positionalArgs)
+                && Objects.equals(namedArgs, other.namedArgs);
+    }
 }