fix TestProofScriptCommand.java

Author: wadoon

key.core/src/test/java/de/uka/ilkd/key/scripts/TestProofScriptCommand.java

@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.scripts;
 
-import java.io.File;
 import java.io.IOException;
 import java.net.URISyntaxException;
 import java.nio.file.Files;
@@ -36,24 +35,27 @@
  * see {@link MasterHandlerTest} from where I copied quite a bit.
  */
 public class TestProofScriptCommand {
-    public record TestInstance(String key, String script, @Nullable String exception,
+    public record TestInstance(
+            String name,
+            String key, String script, @Nullable String exception,
             String[] goals, Integer selectedGoal) {
     }
 
     public static List<Arguments> data() throws IOException, URISyntaxException {
-        var folder = Paths.get("src/test/resources/de/uka/ilkd/key/macros/scripts");
+        var folder = Paths.get("src/test/resources/de/uka/ilkd/key/scripts/cases")
+                .toAbsolutePath();
         try (var walker = Files.walk(folder)) {
             List<Path> files =
                 walker.filter(it -> it.getFileName().toString().endsWith(".yml")).toList();
             var objectMapper = new ObjectMapper(new YAMLFactory());
             objectMapper.findAndRegisterModules();
 
-            List<Arguments> args = new ArrayList(files.size());
+            List<Arguments> args = new ArrayList<>(files.size());
             for (Path path : files) {
                 try {
                     TestInstance instance =
                         objectMapper.readValue(path.toFile(), TestInstance.class);
-                    args.add(Arguments.of(path.toFile(), instance));
+                    args.add(Arguments.of(instance));
                 } catch (Exception e) {
                     System.out.println(path);
                     e.printStackTrace();
@@ -66,8 +68,8 @@ public static List<Arguments> data() throws IOException, URISyntaxException {
 
     @ParameterizedTest
     @MethodSource("data")
-    void testProofScript(File file, TestInstance data) throws Exception {
-        var name = file.getName().replace(".yml", "");
+    void testProofScript(TestInstance data) throws Exception {
+        var name = data.name();
         Path tmpKey = Files.createTempFile("proofscript_key_" + name, ".key");
         Files.writeString(tmpKey, data.key());
 

key.core/src/test/resources/de/uka/ilkd/key/scripts/cases/andRight.yml

@@ -0,0 +1,9 @@
+name: andRight
+key: |
+  \predicates { a; b; }
+  \problem { a & b }
+script: |
+  rule andRight;
+goals:
+  - ==> b
+  - ==> a

key.core/src/test/resources/de/uka/ilkd/key/scripts/cases/hide.exec.yml

@@ -0,0 +1,14 @@
+name: hide.exec
+key: |
+  \predicates { a; b; c; d; e; f; }
+  \problem { a -> b }
+
+script: |
+  macro "split-prop";
+  hide "b ==>";
+
+exception: |
+
+  Error while executing script: This formula is not on the sequent: b
+  
+  Command: hide "b ==>";

key.core/src/test/resources/de/uka/ilkd/key/scripts/cases/hide.yml

@@ -0,0 +1,12 @@
+name: hide
+key: |
+  \predicates { a; b; c; d; e; f; }
+
+  \problem { a & b & c -> d | e | f }
+
+script: |
+  macro "split-prop";
+  hide "a ==> d, e";
+
+goals:
+  - "b, c ==> f"

key.core/src/test/resources/de/uka/ilkd/key/scripts/cases/rule.exc.yml

@@ -0,0 +1,12 @@
+name: "rule.exc"
+key: |
+  \predicates { a; b; }
+  \problem { a & b }
+
+script: |
+  rule andLeft;
+
+exception: |
+  Error while executing script: No matching applications.
+
+  Command: rule andLeft;

key.core/src/test/resources/de/uka/ilkd/key/scripts/cases/selectFormula.yml

@@ -0,0 +1,15 @@
+name: "selectFormula"
+key: |
+  \predicates { a; b; c; }
+  \problem { a & b & c}
+
+script: |
+  macro "split-prop";
+  select formula="b";
+
+goals:
+  - "==> b"
+  - "==> a"
+  - "==> c"
+
+selectedGoal: 0

key.core/src/test/resources/de/uka/ilkd/key/scripts/cases/unhide.yml

@@ -0,0 +1,13 @@
+name: "unhide"
+key: |
+
+  \problem { 2=3 -> 3=4 }
+
+script: |
+  rule impRight;
+  hide   "2=3 ==> 3=4";
+  unhide "2=3 ==>";
+  unhide "==> 3=4";
+
+goals:
+  - "2 = 3 ==> 3 = 4"

key.core/src/test/resources/de/uka/ilkd/key/scripts/cases/unhide2.yml

@@ -0,0 +1,12 @@
+name: unhide2
+key: |
+
+  \problem { 2=3 -> 3=4 }
+
+script: |
+  rule impRight;
+  hide "2=3 ==> 3=4";
+  unhide "2=3 ==> 3=4";
+
+goals:
+  - 2 = 3 ==> 3 = 4