Single files instead of one large files

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,5 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.12-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.12.1-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

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

@@ -3,14 +3,13 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.macros.scripts;
 
-import java.io.FileNotFoundException;
+import java.io.File;
 import java.io.IOException;
-import java.net.URI;
 import java.net.URISyntaxException;
-import java.net.URL;
 import java.nio.file.Files;
 import java.nio.file.Path;
-import java.util.Arrays;
+import java.nio.file.Paths;
+import java.util.ArrayList;
 import java.util.List;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
@@ -33,32 +32,42 @@
 import static org.assertj.core.api.Assertions.assertThat;
 import static org.junit.jupiter.api.Assertions.assertTrue;
 
-
 /**
  * see {@link MasterHandlerTest} from where I copied quite a bit.
  */
 public class TestProofScriptCommand {
-    public record TestInstance(String name, String key, String script, String exception,
+    public record TestInstance(String key, String script, String exception,
             String[] goals, Integer selectedGoal) {
     }
 
-
     public static List<Arguments> data() throws IOException, URISyntaxException {
-        URL url = TestProofScriptCommand.class.getResource("cases.yml");
-        if (url == null) {
-            throw new FileNotFoundException("Cannot find resource 'cases'.");
+        var folder = Paths.get("src/test/resources/de/uka/ilkd/key/macros/scripts");
+        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());
+            for (Path path : files) {
+                try {
+                    TestInstance instance =
+                        objectMapper.readValue(path.toFile(), TestInstance.class);
+                    args.add(Arguments.of(path.toFile(), instance));
+                } catch (Exception e) {
+                    System.out.println(path);
+                    e.printStackTrace();
+                    throw e;
+                }
+            }
+            return args;
         }
-
-        var objectMapper = new ObjectMapper(new YAMLFactory());
-        objectMapper.findAndRegisterModules();
-        TestInstance[] instances = objectMapper.readValue(url, TestInstance[].class);
-        return Arrays.stream(instances).map(Arguments::of).toList();
     }
 
     @ParameterizedTest
     @MethodSource("data")
-    void testProofScript(TestInstance data) throws Exception {
-        var name = data.name();
+    void testProofScript(File file, TestInstance data) throws Exception {
+        var name = file.getName().replace(".yml", "");
         Path tmpKey = Files.createTempFile("proofscript_key_" + name, ".key");
         Files.writeString(tmpKey, data.key());
 
@@ -67,7 +76,7 @@ void testProofScript(TestInstance data) throws Exception {
         Proof proof = env.getLoadedProof();
 
         ProofScriptEngine pse = new ProofScriptEngine(data.script(),
-                new Location(URI.create("file:/"+data.name), Position.newOneBased(1, 1)));
+            new Location(file.toURI(), Position.newOneBased(1, 1)));
 
         boolean hasException = data.exception() != null;
         try {

key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java

@@ -9,6 +9,7 @@
 import java.nio.charset.StandardCharsets;
 import java.nio.file.Files;
 import java.nio.file.Path;
+import java.nio.file.Paths;
 import java.util.*;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
@@ -25,7 +26,6 @@
 
 import org.key_project.util.Streams;
 
-import com.fasterxml.jackson.core.type.TypeReference;
 import com.fasterxml.jackson.databind.ObjectMapper;
 import com.fasterxml.jackson.dataformat.yaml.YAMLFactory;
 import org.assertj.core.api.Assertions;
@@ -67,43 +67,50 @@ public class MasterHandlerTest {
 
     public static List<Arguments> data()
             throws IOException, URISyntaxException, ProblemLoaderException {
-        try (var input = MasterHandlerTest.class.getResourceAsStream("cases.yml")) {
-            var om = new ObjectMapper(new YAMLFactory());
-            TypeReference<HashMap<String, TestData>> typeRef = new TypeReference<>() {
-            };
-            Map<String, TestData> preData = om.readValue(input, typeRef);
-            var result = new ArrayList<Arguments>(preData.size());
-            for (var entry : preData.entrySet()) {
-                final var value = entry.getValue();
+        var om = new ObjectMapper(new YAMLFactory());
+        var path = Paths.get("src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/");
+        try (var walker = Files.walk(path)) {
+            var files = walker.filter(it -> it.getFileName().endsWith("yml")).toList();
+            var result = new ArrayList<Arguments>(files.size());
+            for (Path pFile : files) {
+                var file = pFile.toFile();
+
+                TestData value = om.readValue(file, TestData.class);
 
                 if (value.state == TestDataState.IGNORE) {
-                    LOGGER.info("Test {} case has been marked ignore", entry.getKey());
+                    LOGGER.info("Test {} case has been marked ignore", file);
                     continue;
                 }
-
-                final var testData = value.load(entry.getKey());
+                final var testData = value.load(file.getName().replace(".yml", ""));
                 result.add(Arguments.of(testData));
             }
             return result;
         }
     }
 
+    /**
+     * Describes the state of a test instance.
+     */
     public enum TestDataState {
         EMPTY, EXTENDED, IGNORE
     }
 
+    /**
+     * Expected outcome of a test instance.
+     */
     public enum Expectation {
         VALID, FAIL, IRRELEVANT
     }
 
     /**
      * This class contains the information about the test fixtures that is loaded via the YAML.
-     * @param contains a list of strings that are expected in the SMT translation
+     *
+     * @param contains    a list of strings that are expected in the SMT translation
      * @param smtSettings required key/values in the smt settings.
-     * @param expected expected output of Z3
-     * @param state    state of the test
-     * @param javaSrc  path to necessary java sources
-     * @param keySrc   contents of the key file to be loaded.
+     * @param expected    expected output of Z3
+     * @param state       state of the test
+     * @param javaSrc     path to necessary java sources
+     * @param keySrc      contents of the key file to be loaded.
      */
     public record TestData(List<String> contains,
                            Properties smtSettings,
@@ -119,7 +126,7 @@ private LoadedTestData load(String name) throws IOException, ProblemLoaderExcept
                 Path srcDir = Files.createTempDirectory("SMT_key_" + name);
                 Path tmpSrc = srcDir.resolve("src.java");
                 Files.writeString(tmpSrc, javaSrc);
-                keySrc += "\n\\javaSource \"%s\";\n".formatted(srcDir);
+                keySrc += "\n/javaSource \"%s\";\n".formatted(srcDir);
             }
 
             Path tmpKey = Files.createTempFile("SMT_key_%s".formatted(name), ".key");

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

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

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

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

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

@@ -0,0 +1,9 @@
+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/macros/scripts/rule.exc.yml

@@ -0,0 +1,9 @@
+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/macros/scripts/selectFormula.yml

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

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

@@ -0,0 +1,9 @@
+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/macros/scripts/unhide2.yml

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