Higher Order Proof Scripts

Author: wadoon

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

@@ -5,6 +5,7 @@ parser grammar KeYParser;
 }
 
 @members {
+private boolean lastPosArgWasCodeBlock=false;
 private SyntaxErrorReporter errorReporter = new SyntaxErrorReporter(getClass());
 public SyntaxErrorReporter getErrorReporter() { return errorReporter;}
 }
@@ -859,16 +860,18 @@ proofScriptEntry
     | LBRACE proofScript RBRACE
     )
 ;
+
 proofScriptEOF: proofScript EOF;
 proofScript: proofScriptCommand+;
-proofScriptCommand: cmd=IDENT proofScriptParameters?
-	( LBRACE sub=proofScript RBRACE SEMI?
-	| SEMI);
+proofScriptCommand: cmd=IDENT proofScriptParameters? SEMI;
+//	( {lastPosArgWasCodeBlock}? SEMI?
+//	| SEMI);
 
 proofScriptParameters: proofScriptParameter+;
 proofScriptParameter :  ((pname=proofScriptParameterName (COLON|EQUALS))? expr=proofScriptExpression);
 proofScriptParameterName: AT? IDENT; // someone thought, that the let-command parameters should have a leading "@"
 proofScriptExpression:
+//  {lastPosArgWasCodeBlock=false;}
     boolean_literal
   | char_literal
   | integer
@@ -878,8 +881,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,41 @@ 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));
+            return new ScriptBlock(
+                    ctx.proofScript().proofScriptCommand().stream()
+                    .map(it -> asAst(file, it))
+                    .toList(), 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

@@ -3,38 +3,35 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.scripts;
 
-import java.util.List;
-
 import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.scripts.meta.ProofScriptArgument;
 
-public class AllCommand implements ProofScriptCommand {
-    private String documentation;
+import java.util.List;
 
+public class AllCommand implements ProofScriptCommand {
     @Override
     public List<ProofScriptArgument> getArguments() {
         return List.of();
     }
 
     @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");
+                        EngineState stateMap) throws ScriptException, InterruptedException {
+        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

@@ -6,6 +6,7 @@
 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;
@@ -14,6 +15,8 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+import java.net.URI;
+
 import static org.key_project.util.java.StringUtil.trim;
 
 /// Evaluates expression inside of proof script to their appropriate type.
@@ -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,25 @@
+/* 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 de.uka.ilkd.key.parser.Location;
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+
+import java.util.List;
+
+import static java.util.stream.Collectors.joining;
+
+/// This class represents is the AST of a proof script command.
+@NullMarked
+public record ScriptBlock(
+        List<ScriptCommandAst> commands,
+        @Nullable Location location) {
+
+    public String asCommandLine() {
+        return " {"
+                + 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;
@@ -22,31 +23,27 @@
 /// ```
 /// <commandName> key_1:value_1 ... key_m:value_m positionalArgs_1 ... positionalArgs_n {
 /// commands_0; ...; commands_k;
-/// }
-/// ```
+///}
+///```
 ///
-/// @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 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);
+                            List<Object> positionalArgs) {
+        this(commandName, namedArgs, positionalArgs, null);
     }
 
     /// Renders this command a parsable string representation. The order of the arguments is as
@@ -62,18 +59,35 @@ public String asCommandLine() {
                 + ' '
                 + positionalArgs.stream().map(ScriptCommandAst::asReadableString)
                         .collect(joining(" "))
-                + (commands != null
-                        ? " {"
-                            + commands.stream().map(ScriptCommandAst::asCommandLine)
-                                    .collect(joining("\n"))
-                            + "\n}"
-                        : ";");
+                + ";";
     }
 
     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);
+    }
 }