add matcher

Author: wadoon

key.ncore.java/src/adt/java-ast.java

@@ -3,9 +3,11 @@
 import de.uka.ilkd.key.speclang.jml.pretranslation.*;
 import de.uka.ilkd.key.java.ast.PositionInfo;
 import org.key_project.util.collection.*;
+import de.uka.ilkd.key.rule.MatchConditions;
+
 
 @Root
-abstract class JavaSourceElement implements Visitable {
+abstract class JavaSourceElement implements Visitable, Matchable {
     @EqEx @Nullable PositionInfo positionInfo;
 }
 

key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java

@@ -53,11 +53,12 @@ public Generator() {
         addStep(NodeSteps::addEquals);
         addStep(NodeSteps::ToString);
         addStep(NodeSteps::addHashCode);
+        addStep(NodeSteps::addMatch);
         addStep(NodeSteps::addWiths);
         addStep(NodeSteps::addBuilder);
         addStep(NodeSteps::addOverrideConstructor);
         addStep(NodeSteps::addOverrideConstructor2);
-        addStep(NodeSteps::addGetProperties);
+        //addStep(NodeSteps::addGetProperties);
         addStep(NodeSteps::processFieldsAccessor);
 
         postSteps.add(PostSteps::createVisitor);

key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java

@@ -60,6 +60,34 @@ private static String upperStart(String nameAsString) {
         return c + nameAsString.substring(1);
     }
 
+    static void addMatch(ClassOrInterfaceDeclaration target) {
+        if (target.isAbstract() || target.isInterface()) {
+            return;
+        }
+        MethodDeclaration equals = target.addMethod("match", PUBLIC);
+        equals.addModifier(FINAL);
+        equals.addAnnotation(Override.class);
+        equals.addAnnotation(Nullable.class);
+        equals.setType("MatchConditions");
+        final var o = getNullableObject();
+        equals.getParameters().add(o);
+        equals.addParameter("MatchConditions", "cond");
+
+        BlockStmt body = equals.getBody().get();
+        body.addStatement(parseStatement(
+                "if(!(o instanceof %s other)) return null;".formatted(target.getNameAsString())));
+        var fields = target.getFields().stream()
+                .filter(it -> it.getAnnotationByName("EqEx").isEmpty())
+                .flatMap(it -> it.getVariables().stream())
+                .toList();
+        for (var field : fields) {
+            body.addStatement("cond = MatchHelper.match(%s, other.%s, cond);"
+                    .formatted(field.getNameAsString(), field.getNameAsString()));
+            body.addStatement("if(cond==null) {return null;}");
+        }
+        body.addStatement("return cond;");
+    }
+
     static void addEquals(ClassOrInterfaceDeclaration target) {
         if (target.isAbstract() || target.isInterface()) {
             return;
@@ -208,7 +236,6 @@ static void addAllWoOptFieldsConstructor(ClassOrInterfaceDeclaration target) {
         target.addMember(constr);
     }
 
-
     static void addOverrideConstructor(ClassOrInterfaceDeclaration target) {
         if (target.isInterface()) {
             return;

key.ncore.java/src/main/java/org/key_project/java/ast/MatchHelper.java

@@ -0,0 +1,49 @@
+package org.key_project.java.ast;
+
+import de.uka.ilkd.key.rule.MatchConditions;
+import org.jspecify.annotations.Nullable;
+import org.key_project.util.collection.RoList;
+
+import java.util.Objects;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (25.04.26)
+ */
+public class MatchHelper {
+    public static @Nullable MatchConditions match(Enum<?> e1, Enum<?> e2, MatchConditions cond) {
+        return Objects.equals(e1, e2) ? cond : null;
+    }
+
+    public static @Nullable MatchConditions match(int i1, int i2, MatchConditions cond) {
+        return i1 == i2 ? cond : null;
+    }
+
+    public static @Nullable MatchConditions match(long i1, long i2, MatchConditions cond) {
+        return i1 == i2 ? cond : null;
+    }
+
+    public static @Nullable MatchConditions match(String s1, String s2, MatchConditions cond) {
+        return Objects.equals(s1, s2) ? cond : null;
+    }
+
+    public static @Nullable <T extends Matchable> MatchConditions match(RoList<T> seq1, RoList<T> seq2, MatchConditions cond) {
+        if (seq1.size() != seq2.size()) {
+            return null;
+        }
+        for (int i = 0; i < seq1.size(); i++) {
+            var e1 = seq1.get(i);
+            var e2 = seq2.get(i);
+            cond = e1.match(e2, cond);
+            if (cond == null) {
+                return null;
+            }
+        }
+        return cond;
+    }
+
+    public static @Nullable MatchConditions match(JavaSourceElement e1, JavaSourceElement e2, MatchConditions cond) {
+        return e1.match(e2, cond);
+    }
+}

key.ncore.java/src/main/java/org/key_project/java/ast/Matchable.java

@@ -0,0 +1,13 @@
+package org.key_project.java.ast;
+
+import de.uka.ilkd.key.rule.MatchConditions;
+import org.jspecify.annotations.Nullable;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (25.04.26)
+ */
+public interface Matchable {
+    @Nullable MatchConditions match(Object o, MatchConditions cond);
+}