6 files changed, 80 insertions, 42 deletions

diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
index a49e0625..8c157187 100644
--- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
@@ -2,13 +2,14 @@ package tools.refinery.store.partial.literal;
 
 import tools.refinery.store.query.Dnf;
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.literal.DnfCallLiteral;
 import tools.refinery.store.query.literal.LiteralReduction;
 import tools.refinery.store.query.literal.PolarLiteral;
+import tools.refinery.store.query.substitution.Substitution;
 
 import java.util.List;
-import java.util.Map;
 
 public class ModalDnfCallLiteral extends ModalLiteral<Dnf> implements PolarLiteral<ModalDnfCallLiteral> {
         public ModalDnfCallLiteral(CallPolarity polarity, Modality modality, Dnf target, List<Variable> arguments) {
@@ -20,7 +21,17 @@ public class ModalDnfCallLiteral extends ModalLiteral<Dnf> implements PolarLiter
         }
 
         @Override
-        public ModalDnfCallLiteral substitute(Map<Variable, Variable> substitution) {
+        public Class<Dnf> getTargetType() {
+                return Dnf.class;
+        }
+
+        @Override
+        protected boolean targetEquals(LiteralEqualityHelper helper, Dnf otherTarget) {
+                return helper.dnfEqual(getTarget(), otherTarget);
+        }
+
+        @Override
+        public ModalDnfCallLiteral substitute(Substitution substitution) {
                 return new ModalDnfCallLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution));
         }
 
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
index a1b6c83e..cebe9c9d 100644
--- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
@@ -2,8 +2,10 @@ package tools.refinery.store.partial.literal;
 
 import tools.refinery.store.query.RelationLike;
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.literal.CallLiteral;
 import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.Literal;
 
 import java.util.List;
 import java.util.Objects;
@@ -26,6 +28,22 @@ public abstract class ModalLiteral<T extends RelationLike> extends CallLiteral<T
         }
 
         @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                // If {@link CallLiteral#equalsWithSubstitution(LiteralEqualityHelper, Literal)} has returned {@code true},
+                // we must have the same dynamic type as {@code other}.
+                var otherModalLiteral = (ModalLiteral<?>) other;
+                return modality == otherModalLiteral.modality;
+        }
+
+        @Override
+        protected String targetToString() {
+                return "%s %s".formatted(modality, super.targetToString());
+        }
+
+        @Override
         public boolean equals(Object o) {
                 if (this == o) return true;
                 if (o == null || getClass() != o.getClass()) return false;
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
index dbaa524f..39054f22 100644
--- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
@@ -4,9 +4,9 @@ import tools.refinery.store.partial.representation.PartialRelation;
 import tools.refinery.store.query.Variable;
 import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.literal.PolarLiteral;
+import tools.refinery.store.query.substitution.Substitution;
 
 import java.util.List;
-import java.util.Map;
 
 public final class ModalRelationLiteral extends ModalLiteral<PartialRelation>
                 implements PolarLiteral<ModalRelationLiteral> {
@@ -15,12 +15,18 @@ public final class ModalRelationLiteral extends ModalLiteral<PartialRelation>
                 super(polarity, modality, target, arguments);
         }
 
+
         public ModalRelationLiteral(Modality modality, PartialRelationLiteral baseLiteral) {
                 super(modality, baseLiteral);
         }
 
         @Override
-        public ModalRelationLiteral substitute(Map<Variable, Variable> substitution) {
+        public Class<PartialRelation> getTargetType() {
+                return PartialRelation.class;
+        }
+
+        @Override
+        public ModalRelationLiteral substitute(Substitution substitution) {
                 return new ModalRelationLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution));
         }
 
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
index dc1a1da3..b81d9a3d 100644
--- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
@@ -5,9 +5,9 @@ import tools.refinery.store.query.Variable;
 import tools.refinery.store.query.literal.CallLiteral;
 import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.literal.PolarLiteral;
+import tools.refinery.store.query.substitution.Substitution;
 
 import java.util.List;
-import java.util.Map;
 
 public final class PartialRelationLiteral extends CallLiteral<PartialRelation>
                 implements PolarLiteral<PartialRelationLiteral> {
@@ -16,7 +16,12 @@ public final class PartialRelationLiteral extends CallLiteral<PartialRelation>
         }
 
         @Override
-        public PartialRelationLiteral substitute(Map<Variable, Variable> substitution) {
+        public Class<PartialRelation> getTargetType() {
+                return PartialRelation.class;
+        }
+
+        @Override
+        public PartialRelationLiteral substitute(Substitution substitution) {
                 return new PartialRelationLiteral(getPolarity(), getTarget(), substituteArguments(substitution));
         }
 
diff --git a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java
index ad81e28f..5f528328 100644
--- a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java
+++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java
@@ -1,6 +1,5 @@
 package tools.refinery.store.partial.translator.typehierarchy;
 
-import org.hamcrest.Matchers;
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
 import tools.refinery.store.partial.representation.PartialRelation;
@@ -61,16 +60,16 @@ class TypeAnalyzerExampleHierarchyTest {
         @Test
         void inferredTypesTest() {
                 assertAll(
-                                () -> assertThat(sut.getUnknownType(), Matchers.is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))),
-                                () -> assertThat(tester.getInferredType(a1), Matchers.is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))),
-                                () -> assertThat(tester.getInferredType(a3), Matchers.is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))),
-                                () -> assertThat(tester.getInferredType(a4), Matchers.is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))),
-                                () -> assertThat(tester.getInferredType(a5), Matchers.is(new InferredType(Set.of(a5), Set.of(), null))),
-                                () -> assertThat(tester.getInferredType(c1), Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))),
+                                () -> assertThat(sut.getUnknownType(), is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))),
+                                () -> assertThat(tester.getInferredType(a1), is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))),
+                                () -> assertThat(tester.getInferredType(a3), is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))),
+                                () -> assertThat(tester.getInferredType(a4), is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))),
+                                () -> assertThat(tester.getInferredType(a5), is(new InferredType(Set.of(a5), Set.of(), null))),
+                                () -> assertThat(tester.getInferredType(c1), is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))),
                                 () -> assertThat(tester.getInferredType(c2),
-                                                Matchers.is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))),
-                                () -> assertThat(tester.getInferredType(c3), Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
-                                () -> assertThat(tester.getInferredType(c4), Matchers.is(new InferredType(Set.of(a4, c4), Set.of(c4), c4)))
+                                                is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))),
+                                () -> assertThat(tester.getInferredType(c3), is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
+                                () -> assertThat(tester.getInferredType(c4), is(new InferredType(Set.of(a4, c4), Set.of(c4), c4)))
                 );
         }
 
@@ -80,8 +79,8 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a3Result = tester.getPreservedType(a3);
                 var expected = new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2);
                 assertAll(
-                                () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), Matchers.is(expected)),
-                                () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), Matchers.is(expected)),
+                                () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), is(expected)),
+                                () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), is(expected)),
                                 () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a1Result.asInferredType())),
                                 () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a3Result.asInferredType())),
                                 () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.TRUE),
@@ -96,19 +95,19 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a4Result = tester.getPreservedType(a4);
                 assertAll(
                                 () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
+                                                is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
                                 () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))),
+                                                is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))),
                                 () -> assertThat(a4Result.merge(a3Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
+                                                is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
                                 () -> assertThat(a3Result.merge(a4Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))),
+                                                is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))),
                                 () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(), Set.of(c3, c4), null))),
+                                                is(new InferredType(Set.of(), Set.of(c3, c4), null))),
                                 () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(), Set.of(c1, c4), null))),
+                                                is(new InferredType(Set.of(), Set.of(c1, c4), null))),
                                 () -> assertThat(a4Result.merge(sut.getUnknownType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(), Set.of(c3), null)))
+                                                is(new InferredType(Set.of(), Set.of(c3), null)))
                 );
         }
 
@@ -118,8 +117,8 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a4Result = tester.getPreservedType(a4);
                 var expected = new InferredType(Set.of(c1, a1, a4), Set.of(), null);
                 assertAll(
-                                () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), Matchers.is(expected)),
-                                () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), Matchers.is(expected))
+                                () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), is(expected)),
+                                () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), is(expected))
                 );
         }
 
@@ -141,9 +140,9 @@ class TypeAnalyzerExampleHierarchyTest {
                 var c3Result = tester.getPreservedType(c3);
                 assertAll(
                                 () -> assertThat(a1Result.merge(c3Result.asInferredType(), TruthValue.TRUE),
-                                                Matchers.is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))),
+                                                is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))),
                                 () -> assertThat(c3Result.merge(a1Result.asInferredType(), TruthValue.TRUE),
-                                                Matchers.is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null)))
+                                                is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null)))
                 );
         }
 
@@ -154,13 +153,13 @@ class TypeAnalyzerExampleHierarchyTest {
                 var c1Result = tester.getPreservedType(c1);
                 assertAll(
                                 () -> assertThat(a4Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a1, a4), Set.of(), null))),
+                                                is(new InferredType(Set.of(a1, a4), Set.of(), null))),
                                 () -> assertThat(a1Result.merge(c1Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))),
+                                                is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))),
                                 () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))),
+                                                is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))),
                                 () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a1, a4), Set.of(), null)))
+                                                is(new InferredType(Set.of(a1, a4), Set.of(), null)))
                 );
         }
 
@@ -170,9 +169,9 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a5Result = tester.getPreservedType(a5);
                 assertAll(
                                 () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.TRUE),
-                                                Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
+                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
                                 () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.TRUE),
-                                                Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null)))
+                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null)))
                 );
         }
 
@@ -194,9 +193,9 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a5Result = tester.getPreservedType(a5);
                 assertAll(
                                 () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.ERROR),
-                                                Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
+                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
                                 () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.ERROR),
-                                                Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
+                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
                                 () -> assertThat(a5Result.merge(a5Result.asInferredType(), TruthValue.ERROR),
                                                 is(a5Result.asInferredType()))
                 );
diff --git a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java
index 1aab75bb..02903026 100644
--- a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java
+++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java
@@ -1,6 +1,5 @@
 package tools.refinery.store.partial.translator.typehierarchy;
 
-import org.hamcrest.Matchers;
 import org.junit.jupiter.api.Test;
 import tools.refinery.store.partial.representation.PartialRelation;
 import tools.refinery.store.representation.TruthValue;
@@ -137,8 +136,8 @@ class TypeAnalyzerTest {
 
                 var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3);
                 assertAll(
-                                () -> assertThat(tester.getInferredType(c3), Matchers.is(expected)),
-                                () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), Matchers.is(expected))
+                                () -> assertThat(tester.getInferredType(c3), is(expected)),
+                                () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(expected))
                 );
         }
 
@@ -162,7 +161,7 @@ class TypeAnalyzerTest {
                 var a1Result = tester.getPreservedType(a1);
 
                 assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                Matchers.is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2)));
+                                is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2)));
         }
 
         @Test
@@ -185,7 +184,7 @@ class TypeAnalyzerTest {
                 var a1Result = tester.getPreservedType(a1);
 
                 assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                Matchers.is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3)));
+                                is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3)));
         }
 
         @Test