feat: partial interpretation for type hierarchy

15 files changed, 565 insertions, 209 deletions

diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/proxy/PartialRelationTranslatorProxy.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/proxy/PartialRelationTranslatorProxy.java
new file mode 100644
index 00000000..45dc5bd2
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/proxy/PartialRelationTranslatorProxy.java
@@ -0,0 +1,52 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.proxy;
+
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
+import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.literal.ModalConstraint;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
+
+import java.util.List;
+import java.util.Set;
+
+public class PartialRelationTranslatorProxy implements ModelStoreConfiguration, PartialRelationRewriter {
+        private final PartialRelation partialRelation;
+        private final PartialRelation targetRelation;
+        private final boolean mutable;
+
+        public PartialRelationTranslatorProxy(PartialRelation partialRelation, PartialRelation targetRelation,
+                                                                                  boolean mutable) {
+                this.partialRelation = partialRelation;
+                this.targetRelation = targetRelation;
+                this.mutable = mutable;
+        }
+
+        @Override
+        public void apply(ModelStoreBuilder storeBuilder) {
+                var translator = PartialRelationTranslator.of(partialRelation)
+                                .interpretation(((adapter, concreteness, partialSymbol) ->
+                                                adapter.getPartialInterpretation(concreteness, targetRelation)))
+                                .rewriter(this);
+                if (mutable) {
+                        translator.refiner((adapter, partialSymbol) -> adapter.getRefiner(targetRelation));
+                }
+                storeBuilder.with(translator);
+        }
+
+        @Override
+        public List<Literal> rewriteLiteral(Set<Variable> positiveVariables, AbstractCallLiteral literal,
+                                                                                Modality modality, Concreteness concreteness) {
+                return List.of(literal.withTarget(ModalConstraint.of(modality, concreteness, targetRelation)));
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/CandidateTypeView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/CandidateTypeView.java
new file mode 100644
index 00000000..faf1b958
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/CandidateTypeView.java
@@ -0,0 +1,21 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+
+class CandidateTypeView extends InferredTypeView {
+        public CandidateTypeView(Symbol<InferredType> symbol, PartialRelation type) {
+                super(symbol, "candidate", type);
+        }
+
+        @Override
+        protected boolean doFilter(Tuple key, InferredType value) {
+                return type.equals(value.candidateType());
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/EliminatedType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/EliminatedType.java
deleted file mode 100644
index 6e4728db..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/EliminatedType.java
+++ /dev/null
@@ -1,11 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.translator.typehierarchy;
-
-import tools.refinery.store.reasoning.representation.PartialRelation;
-
-record EliminatedType(PartialRelation replacement) implements TypeAnalysisResult {
-}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java
index fd05158b..1ae94ae1 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java
@@ -11,18 +11,18 @@ import java.util.Collections;
 import java.util.Set;
 
 record InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes,
-                                        PartialRelation currentType) {
+                                        PartialRelation candidateType) {
         public static final InferredType UNTYPED = new InferredType(Set.of(), Set.of(), null);
 
         public InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes,
-                                                PartialRelation currentType) {
+                                                PartialRelation candidateType) {
                 this.mustTypes = Collections.unmodifiableSet(mustTypes);
                 this.mayConcreteTypes = Collections.unmodifiableSet(mayConcreteTypes);
-                this.currentType = currentType;
+                this.candidateType = candidateType;
         }
 
         public boolean isConsistent() {
-                return currentType != null || mustTypes.isEmpty();
+                return candidateType != null || mustTypes.isEmpty();
         }
 
         public boolean isMust(PartialRelation partialRelation) {
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeRefiner.java
new file mode 100644
index 00000000..40a7b3fa
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeRefiner.java
@@ -0,0 +1,38 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.model.Interpretation;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+class InferredTypeRefiner extends AbstractPartialInterpretationRefiner<TruthValue, Boolean> {
+        private final Interpretation<InferredType> interpretation;
+        private final TypeAnalysisResult result;
+
+        private InferredTypeRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol,
+                                                                Symbol<InferredType> symbol, TypeAnalysisResult result) {
+                super(adapter, partialSymbol);
+                interpretation = adapter.getModel().getInterpretation(symbol);
+                this.result = result;
+        }
+
+        @Override
+        public boolean merge(Tuple key, TruthValue value) {
+                var currentType = interpretation.get(key);
+                var newType = result.merge(currentType, value);
+                interpretation.put(key, newType);
+                return true;
+        }
+
+        public static Factory<TruthValue, Boolean> of(Symbol<InferredType> symbol, TypeAnalysisResult result) {
+                return (adapter, partialSymbol) -> new InferredTypeRefiner(adapter, partialSymbol, symbol, result);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeView.java
new file mode 100644
index 00000000..3c074df5
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeView.java
@@ -0,0 +1,35 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.query.view.TuplePreservingView;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.Symbol;
+
+import java.util.Objects;
+
+abstract class InferredTypeView extends TuplePreservingView<InferredType> {
+        protected final PartialRelation type;
+
+        protected InferredTypeView(Symbol<InferredType> symbol, String name, PartialRelation type) {
+                super(symbol, type.name() + "#" + name);
+                this.type = type;
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                if (!super.equals(o)) return false;
+                InferredTypeView that = (InferredTypeView) o;
+                return Objects.equals(type, that.type);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), type);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/MayTypeView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/MayTypeView.java
new file mode 100644
index 00000000..dcaf61c5
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/MayTypeView.java
@@ -0,0 +1,21 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+
+class MayTypeView extends InferredTypeView {
+        public MayTypeView(Symbol<InferredType> symbol, PartialRelation type) {
+                super(symbol, "may", type);
+        }
+
+        @Override
+        protected boolean doFilter(Tuple key, InferredType value) {
+                return value.mayConcreteTypes().contains(type);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/MustTypeView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/MustTypeView.java
new file mode 100644
index 00000000..833e1594
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/MustTypeView.java
@@ -0,0 +1,21 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+
+class MustTypeView extends InferredTypeView {
+        public MustTypeView(Symbol<InferredType> symbol, PartialRelation type) {
+                super(symbol, "must", type);
+        }
+
+        @Override
+        protected boolean doFilter(Tuple key, InferredType value) {
+                return value.mustTypes().contains(type);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/PreservedType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/PreservedType.java
deleted file mode 100644
index 0696f4c3..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/PreservedType.java
+++ /dev/null
@@ -1,141 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.translator.typehierarchy;
-
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.representation.TruthValue;
-
-import java.util.*;
-
-final class PreservedType implements TypeAnalysisResult {
-        private final ExtendedTypeInfo extendedTypeInfo;
-        private final List<PartialRelation> directSubtypes;
-        private final List<ExtendedTypeInfo> allExternalTypeInfoList;
-        private final InferredType inferredType;
-
-        public PreservedType(ExtendedTypeInfo extendedTypeInfo, List<ExtendedTypeInfo> allExternalTypeInfoList) {
-                this.extendedTypeInfo = extendedTypeInfo;
-                directSubtypes = List.copyOf(extendedTypeInfo.getDirectSubtypes());
-                this.allExternalTypeInfoList = allExternalTypeInfoList;
-                inferredType = propagateMust(extendedTypeInfo.getAllSupertypesAndSelf(),
-                                extendedTypeInfo.getConcreteSubtypesAndSelf());
-        }
-
-        public PartialRelation type() {
-                return extendedTypeInfo.getType();
-        }
-
-        public List<PartialRelation> getDirectSubtypes() {
-                return directSubtypes;
-        }
-
-        public boolean isAbstractType() {
-                return extendedTypeInfo.isAbstractType();
-        }
-
-        public boolean isVacuous() {
-                return isAbstractType() && directSubtypes.isEmpty();
-        }
-
-        public InferredType asInferredType() {
-                return inferredType;
-        }
-
-        public InferredType merge(InferredType inferredType, TruthValue value) {
-                return switch (value) {
-                        case UNKNOWN -> inferredType;
-                        case TRUE -> addMust(inferredType);
-                        case FALSE -> removeMay(inferredType);
-                        case ERROR -> addError(inferredType);
-                };
-        }
-
-        private InferredType addMust(InferredType inferredType) {
-                var originalMustTypes = inferredType.mustTypes();
-                if (originalMustTypes.contains(type())) {
-                        return inferredType;
-                }
-                var mustTypes = new HashSet<>(originalMustTypes);
-                extendedTypeInfo.addMust(mustTypes);
-                var originalMayConcreteTypes = inferredType.mayConcreteTypes();
-                var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes);
-                Set<PartialRelation> mayConcreteTypesResult;
-                if (mayConcreteTypes.retainAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) {
-                        mayConcreteTypesResult = mayConcreteTypes;
-                } else {
-                        mayConcreteTypesResult = originalMayConcreteTypes;
-                }
-                return propagateMust(mustTypes, mayConcreteTypesResult);
-        }
-
-        private InferredType removeMay(InferredType inferredType) {
-                var originalMayConcreteTypes = inferredType.mayConcreteTypes();
-                var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes);
-                if (!mayConcreteTypes.removeAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) {
-                        return inferredType;
-                }
-                return propagateMust(inferredType.mustTypes(), mayConcreteTypes);
-        }
-
-        private InferredType addError(InferredType inferredType) {
-                var originalMustTypes = inferredType.mustTypes();
-                if (originalMustTypes.contains(type())) {
-                        if (inferredType.mayConcreteTypes().isEmpty()) {
-                                return inferredType;
-                        }
-                        return new InferredType(originalMustTypes, Set.of(), null);
-                }
-                var mustTypes = new HashSet<>(originalMustTypes);
-                extendedTypeInfo.addMust(mustTypes);
-                return new InferredType(mustTypes, Set.of(), null);
-        }
-
-        private InferredType propagateMust(Set<PartialRelation> originalMustTypes,
-                                                                           Set<PartialRelation> mayConcreteTypes) {
-                // It is possible that there is not type at all, do not force one by propagation.
-                var maybeUntyped = originalMustTypes.isEmpty();
-                // Para-consistent case, do not propagate must types to avoid logical explosion.
-                var paraConsistentOrSurelyUntyped = mayConcreteTypes.isEmpty();
-                if (maybeUntyped || paraConsistentOrSurelyUntyped) {
-                        return new InferredType(originalMustTypes, mayConcreteTypes, null);
-                }
-                var currentType = computeCurrentType(mayConcreteTypes);
-                var mustTypes = new HashSet<>(originalMustTypes);
-                boolean changed = false;
-                for (var newMustExtendedTypeInfo : allExternalTypeInfoList) {
-                        var newMustType = newMustExtendedTypeInfo.getType();
-                        if (mustTypes.contains(newMustType)) {
-                                continue;
-                        }
-                        if (newMustExtendedTypeInfo.allowsAllConcreteTypes(mayConcreteTypes)) {
-                                newMustExtendedTypeInfo.addMust(mustTypes);
-                                changed = true;
-                        }
-                }
-                if (!changed) {
-                        return new InferredType(originalMustTypes, mayConcreteTypes, currentType);
-                }
-                return new InferredType(mustTypes, mayConcreteTypes, currentType);
-        }
-
-        /**
-         * Returns a concrete type that is allowed by a (consistent, i.e., nonempty) set of <b>may</b> concrete types.
-         *
-         * @param mayConcreteTypes The set of allowed concrete types. Must not be empty.
-         * @return The first concrete type that is allowed by {@code matConcreteTypes}.
-         */
-        private PartialRelation computeCurrentType(Set<PartialRelation> mayConcreteTypes) {
-                for (var concreteExtendedTypeInfo : allExternalTypeInfoList) {
-                        var concreteType = concreteExtendedTypeInfo.getType();
-                        if (!concreteExtendedTypeInfo.isAbstractType() && mayConcreteTypes.contains(concreteType)) {
-                                return concreteType;
-                        }
-                }
-                // We have already filtered out the para-consistent case in {@link #propagateMust(Set<PartialRelation>,
-                // Set<PartialRelation>}.
-                throw new AssertionError("No concrete type in %s".formatted(mayConcreteTypes));
-        }
-}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java
index fbf8a7c9..39a76745 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java
@@ -5,5 +5,137 @@
  */
 package tools.refinery.store.reasoning.translator.typehierarchy;
 
-sealed interface TypeAnalysisResult permits EliminatedType, PreservedType {
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.TruthValue;
+
+import java.util.*;
+
+final class TypeAnalysisResult {
+        private final ExtendedTypeInfo extendedTypeInfo;
+        private final List<PartialRelation> directSubtypes;
+        private final List<ExtendedTypeInfo> allExternalTypeInfoList;
+        private final InferredType inferredType;
+
+        public TypeAnalysisResult(ExtendedTypeInfo extendedTypeInfo, List<ExtendedTypeInfo> allExternalTypeInfoList) {
+                this.extendedTypeInfo = extendedTypeInfo;
+                directSubtypes = List.copyOf(extendedTypeInfo.getDirectSubtypes());
+                this.allExternalTypeInfoList = allExternalTypeInfoList;
+                inferredType = propagateMust(extendedTypeInfo.getAllSupertypesAndSelf(),
+                                extendedTypeInfo.getConcreteSubtypesAndSelf());
+        }
+
+        public PartialRelation type() {
+                return extendedTypeInfo.getType();
+        }
+
+        public List<PartialRelation> getDirectSubtypes() {
+                return directSubtypes;
+        }
+
+        public boolean isAbstractType() {
+                return extendedTypeInfo.isAbstractType();
+        }
+
+        public boolean isVacuous() {
+                return isAbstractType() && directSubtypes.isEmpty();
+        }
+
+        public InferredType asInferredType() {
+                return inferredType;
+        }
+
+        public InferredType merge(InferredType inferredType, TruthValue value) {
+                return switch (value) {
+                        case UNKNOWN -> inferredType;
+                        case TRUE -> addMust(inferredType);
+                        case FALSE -> removeMay(inferredType);
+                        case ERROR -> addError(inferredType);
+                };
+        }
+
+        private InferredType addMust(InferredType inferredType) {
+                var originalMustTypes = inferredType.mustTypes();
+                if (originalMustTypes.contains(type())) {
+                        return inferredType;
+                }
+                var mustTypes = new HashSet<>(originalMustTypes);
+                extendedTypeInfo.addMust(mustTypes);
+                var originalMayConcreteTypes = inferredType.mayConcreteTypes();
+                var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes);
+                Set<PartialRelation> mayConcreteTypesResult;
+                if (mayConcreteTypes.retainAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) {
+                        mayConcreteTypesResult = mayConcreteTypes;
+                } else {
+                        mayConcreteTypesResult = originalMayConcreteTypes;
+                }
+                return propagateMust(mustTypes, mayConcreteTypesResult);
+        }
+
+        private InferredType removeMay(InferredType inferredType) {
+                var originalMayConcreteTypes = inferredType.mayConcreteTypes();
+                var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes);
+                if (!mayConcreteTypes.removeAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) {
+                        return inferredType;
+                }
+                return propagateMust(inferredType.mustTypes(), mayConcreteTypes);
+        }
+
+        private InferredType addError(InferredType inferredType) {
+                var originalMustTypes = inferredType.mustTypes();
+                if (originalMustTypes.contains(type())) {
+                        if (inferredType.mayConcreteTypes().isEmpty()) {
+                                return inferredType;
+                        }
+                        return new InferredType(originalMustTypes, Set.of(), null);
+                }
+                var mustTypes = new HashSet<>(originalMustTypes);
+                extendedTypeInfo.addMust(mustTypes);
+                return new InferredType(mustTypes, Set.of(), null);
+        }
+
+        private InferredType propagateMust(Set<PartialRelation> originalMustTypes,
+                                                                           Set<PartialRelation> mayConcreteTypes) {
+                // It is possible that there is not type at all, do not force one by propagation.
+                var maybeUntyped = originalMustTypes.isEmpty();
+                // Para-consistent case, do not propagate must types to avoid logical explosion.
+                var paraConsistentOrSurelyUntyped = mayConcreteTypes.isEmpty();
+                if (maybeUntyped || paraConsistentOrSurelyUntyped) {
+                        return new InferredType(originalMustTypes, mayConcreteTypes, null);
+                }
+                var currentType = computeCurrentType(mayConcreteTypes);
+                var mustTypes = new HashSet<>(originalMustTypes);
+                boolean changed = false;
+                for (var newMustExtendedTypeInfo : allExternalTypeInfoList) {
+                        var newMustType = newMustExtendedTypeInfo.getType();
+                        if (mustTypes.contains(newMustType)) {
+                                continue;
+                        }
+                        if (newMustExtendedTypeInfo.allowsAllConcreteTypes(mayConcreteTypes)) {
+                                newMustExtendedTypeInfo.addMust(mustTypes);
+                                changed = true;
+                        }
+                }
+                if (!changed) {
+                        return new InferredType(originalMustTypes, mayConcreteTypes, currentType);
+                }
+                return new InferredType(mustTypes, mayConcreteTypes, currentType);
+        }
+
+        /**
+         * Returns a concrete type that is allowed by a (consistent, i.e., nonempty) set of <b>may</b> concrete types.
+         *
+         * @param mayConcreteTypes The set of allowed concrete types. Must not be empty.
+         * @return The first concrete type that is allowed by {@code matConcreteTypes}.
+         */
+        private PartialRelation computeCurrentType(Set<PartialRelation> mayConcreteTypes) {
+                for (var concreteExtendedTypeInfo : allExternalTypeInfoList) {
+                        var concreteType = concreteExtendedTypeInfo.getType();
+                        if (!concreteExtendedTypeInfo.isAbstractType() && mayConcreteTypes.contains(concreteType)) {
+                                return concreteType;
+                        }
+                }
+                // We have already filtered out the para-consistent case in {@link #propagateMust(Set<PartialRelation>,
+                // Set<PartialRelation>}.
+                throw new AssertionError("No concrete type in %s".formatted(mayConcreteTypes));
+        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java
index e97ce954..99069ab9 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzer.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java
@@ -9,14 +9,16 @@ import tools.refinery.store.reasoning.representation.PartialRelation;
 
 import java.util.*;
 
-class TypeAnalyzer {
+public class TypeHierarchy {
+        private final Set<PartialRelation> allTypes;
         private final Map<PartialRelation, ExtendedTypeInfo> extendedTypeInfoMap;
         private final Map<PartialRelation, PartialRelation> replacements = new LinkedHashMap<>();
         private final InferredType unknownType;
-        private final Map<PartialRelation, TypeAnalysisResult> analysisResults;
+        private final Map<PartialRelation, TypeAnalysisResult> preservedTypes;
 
-        public TypeAnalyzer(Map<PartialRelation, TypeInfo> typeInfoMap) {
+        TypeHierarchy(Map<PartialRelation, TypeInfo> typeInfoMap) {
                 int size = typeInfoMap.size();
+                allTypes = Collections.unmodifiableSet(new LinkedHashSet<>(typeInfoMap.keySet()));
                 extendedTypeInfoMap = new LinkedHashMap<>(size);
                 var concreteTypes = new LinkedHashSet<PartialRelation>();
                 int index = 0;
@@ -34,15 +36,39 @@ class TypeAnalyzer {
                 computeAllAndConcreteSubtypes();
                 computeDirectSubtypes();
                 eliminateTrivialSupertypes();
-                analysisResults = computeAnalysisResults();
+                preservedTypes = computeAnalysisResults();
+        }
+
+        public boolean isEmpty() {
+                return extendedTypeInfoMap.isEmpty();
         }
 
         public InferredType getUnknownType() {
                 return unknownType;
         }
 
-        public Map<PartialRelation, TypeAnalysisResult> getAnalysisResults() {
-                return analysisResults;
+        public Set<PartialRelation> getAllTypes() {
+                return allTypes;
+        }
+
+        public Map<PartialRelation, TypeAnalysisResult> getPreservedTypes() {
+                return preservedTypes;
+        }
+
+        public Map<PartialRelation, PartialRelation> getEliminatedTypes() {
+                return Collections.unmodifiableMap(replacements);
+        }
+
+        public TypeAnalysisResult getAnalysisResult(PartialRelation type) {
+                var preservedResult = preservedTypes.get(type);
+                if (preservedResult != null) {
+                        return preservedResult;
+                }
+                var eliminatedResult = replacements.get(type);
+                if (eliminatedResult != null) {
+                        return preservedTypes.get(eliminatedResult);
+                }
+                throw new IllegalArgumentException("Unknown type: " + type);
         }
 
         private void computeAllSupertypes() {
@@ -156,17 +182,13 @@ class TypeAnalyzer {
 
         private Map<PartialRelation, TypeAnalysisResult> computeAnalysisResults() {
                 var allExtendedTypeInfoList = sortTypes();
-                var results = new LinkedHashMap<PartialRelation, TypeAnalysisResult>(
-                                allExtendedTypeInfoList.size() + replacements.size());
+                var preservedResults = new LinkedHashMap<PartialRelation, TypeAnalysisResult>(
+                                allExtendedTypeInfoList.size());
                 for (var extendedTypeInfo : allExtendedTypeInfoList) {
                         var type = extendedTypeInfo.getType();
-                        results.put(type, new PreservedType(extendedTypeInfo, allExtendedTypeInfoList));
+                        preservedResults.put(type, new TypeAnalysisResult(extendedTypeInfo, allExtendedTypeInfoList));
                 }
-                for (var entry : replacements.entrySet()) {
-                        var type = entry.getKey();
-                        results.put(type, new EliminatedType(entry.getValue()));
-                }
-                return Collections.unmodifiableMap(results);
+                return Collections.unmodifiableMap(preservedResults);
         }
 
         private List<ExtendedTypeInfo> sortTypes() {
@@ -204,4 +226,8 @@ class TypeAnalyzer {
                 }
                 return Collections.unmodifiableList(sorted);
         }
+
+        public static TypeHierarchyBuilder builder() {
+                return new TypeHierarchyBuilder();
+        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java
new file mode 100644
index 00000000..0fca4810
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java
@@ -0,0 +1,62 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+import java.util.Collection;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
+
+public class TypeHierarchyBuilder {
+        private final Map<PartialRelation, TypeInfo> typeInfoMap = new LinkedHashMap<>();
+
+        public TypeHierarchyBuilder type(PartialRelation partialRelation, TypeInfo typeInfo) {
+                if (partialRelation.arity() != 1) {
+                        throw new IllegalArgumentException("Only types of arity 1 are supported, hot %d instead"
+                                        .formatted(partialRelation.arity()));
+                }
+                var putResult = typeInfoMap.put(partialRelation, typeInfo);
+                if (putResult != null && !putResult.equals(typeInfo)) {
+                        throw new IllegalArgumentException("Duplicate type info for partial relation: " + partialRelation);
+                }
+                return this;
+        }
+
+        public TypeHierarchyBuilder type(PartialRelation partialRelation, boolean abstractType,
+                                                                         PartialRelation... supertypes) {
+                return type(partialRelation, abstractType, List.of(supertypes));
+        }
+
+        public TypeHierarchyBuilder type(PartialRelation partialRelation, boolean abstractType,
+                                                                         Collection<PartialRelation> supertypes) {
+                return type(partialRelation, new TypeInfo(supertypes, abstractType));
+        }
+
+        public TypeHierarchyBuilder type(PartialRelation partialRelation, PartialRelation... supertypes) {
+                return type(partialRelation, List.of(supertypes));
+        }
+
+        public TypeHierarchyBuilder type(PartialRelation partialRelation, Collection<PartialRelation> supertypes) {
+                return type(partialRelation, false, supertypes);
+        }
+
+        public TypeHierarchyBuilder types(Collection<Map.Entry<PartialRelation, TypeInfo>> entries) {
+                for (var entry : entries) {
+                        type(entry.getKey(), entry.getValue());
+                }
+                return this;
+        }
+
+        public TypeHierarchyBuilder types(Map<PartialRelation, TypeInfo> map) {
+                return types(map.entrySet());
+        }
+
+        public TypeHierarchy build() {
+                return new TypeHierarchy(typeInfoMap);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyInitializer.java
new file mode 100644
index 00000000..6648a454
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyInitializer.java
@@ -0,0 +1,57 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.seed.ModelSeed;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.Arrays;
+
+public class TypeHierarchyInitializer implements PartialModelInitializer {
+        private final TypeHierarchy typeHierarchy;
+        private final Symbol<InferredType> typeSymbol;
+
+        public TypeHierarchyInitializer(TypeHierarchy typeHierarchy, Symbol<InferredType> typeSymbol) {
+                this.typeHierarchy = typeHierarchy;
+                this.typeSymbol = typeSymbol;
+        }
+
+        @Override
+        public void initialize(Model model, ModelSeed modelSeed) {
+                var inferredTypes = new InferredType[modelSeed.getNodeCount()];
+                Arrays.fill(inferredTypes, typeHierarchy.getUnknownType());
+                for (var type : typeHierarchy.getAllTypes()) {
+                        initializeType(type, inferredTypes, modelSeed);
+                }
+                var typeInterpretation = model.getInterpretation(typeSymbol);
+                for (int i = 0; i < inferredTypes.length; i++) {
+                        typeInterpretation.put(Tuple.of(i), inferredTypes[i]);
+                }
+        }
+
+        private void initializeType(PartialRelation type, InferredType[] inferredTypes, ModelSeed modelSeed) {
+                var cursor = modelSeed.getCursor(type, TruthValue.UNKNOWN);
+                var analysisResult = typeHierarchy.getAnalysisResult(type);
+                while (cursor.move()) {
+                        var i = cursor.getKey().get(0);
+                        checkNodeId(inferredTypes, i);
+                        var value = cursor.getValue();
+                        inferredTypes[i] = analysisResult.merge(inferredTypes[i], value);
+                }
+        }
+
+        private void checkNodeId(InferredType[] inferredTypes, int nodeId) {
+                if (nodeId < 0 || nodeId >= inferredTypes.length) {
+                        throw new IllegalArgumentException("Expected node id %d to be lower than model size %d"
+                                        .formatted(nodeId, inferredTypes.length));
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java
new file mode 100644
index 00000000..6a45acd3
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java
@@ -0,0 +1,81 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.reasoning.ReasoningBuilder;
+import tools.refinery.store.reasoning.literal.PartialLiterals;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
+import tools.refinery.store.reasoning.translator.proxy.PartialRelationTranslatorProxy;
+import tools.refinery.store.representation.Symbol;
+
+public class TypeHierarchyTranslator implements ModelStoreConfiguration {
+        private final Symbol<InferredType> typeSymbol = Symbol.of("TYPE", 1, InferredType.class, InferredType.UNTYPED);
+        private final TypeHierarchy typeHierarchy;
+
+        public TypeHierarchyTranslator(TypeHierarchy typeHierarchy) {
+                this.typeHierarchy = typeHierarchy;
+        }
+
+        @Override
+        public void apply(ModelStoreBuilder storeBuilder) {
+                if (typeHierarchy.isEmpty()) {
+                        return;
+                }
+
+                storeBuilder.symbol(typeSymbol);
+
+                for (var entry : typeHierarchy.getPreservedTypes().entrySet()) {
+                        storeBuilder.with(createPreservedTypeTranslator(entry.getKey(), entry.getValue()));
+                }
+
+                for (var entry : typeHierarchy.getEliminatedTypes().entrySet()) {
+                        storeBuilder.with(createEliminatedTypeTranslator(entry.getKey(), entry.getValue()));
+                }
+
+                var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class);
+                reasoningBuilder.initializer(new TypeHierarchyInitializer(typeHierarchy, typeSymbol));
+        }
+
+        private ModelStoreConfiguration createPreservedTypeTranslator(PartialRelation type, TypeAnalysisResult result) {
+                var may = Query.of(type.name() + "#may", (builder, p1) -> {
+                        if (result.isAbstractType()) {
+                                for (var subtype : result.getDirectSubtypes()) {
+                                        builder.clause(PartialLiterals.may(subtype.call(p1)));
+                                }
+                        } else {
+                                builder.clause(new MayTypeView(typeSymbol, type).call(p1));
+                        }
+                });
+
+                var must = Query.of(type.name() + "#must", (builder, p1) -> builder.clause(
+                                new MustTypeView(typeSymbol, type).call(p1)
+                ));
+
+                var candidate = Query.of(type.name() + "#candidate", (builder, p1) -> {
+                        if (!result.isAbstractType()) {
+                                builder.clause(new CandidateTypeView(typeSymbol, type).call(p1));
+                        }
+                        for (var subtype : result.getDirectSubtypes()) {
+                                builder.clause(PartialLiterals.candidateMust(subtype.call(p1)));
+                        }
+                });
+
+                return PartialRelationTranslator.of(type)
+                                .may(may)
+                                .must(must)
+                                .candidate(candidate)
+                                .refiner(InferredTypeRefiner.of(typeSymbol, result));
+        }
+
+        private ModelStoreConfiguration createEliminatedTypeTranslator(
+                        PartialRelation type, PartialRelation replacement) {
+                return new PartialRelationTranslatorProxy(type, replacement, true);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java
index 9f897e46..68ed4089 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java
@@ -10,42 +10,4 @@ import tools.refinery.store.reasoning.representation.PartialRelation;
 import java.util.*;
 
 public record TypeInfo(Collection<PartialRelation> supertypes, boolean abstractType) {
-        public static Builder builder() {
-                return new Builder();
-        }
-
-        public static class Builder {
-                private final Set<PartialRelation> supertypes = new LinkedHashSet<>();
-                private boolean abstractType;
-
-                private Builder() {
-                }
-
-                public Builder supertypes(Collection<PartialRelation> supertypes) {
-                        this.supertypes.addAll(supertypes);
-                        return this;
-                }
-
-                public Builder supertypes(PartialRelation... supertypes) {
-                        return supertypes(List.of(supertypes));
-                }
-
-                public Builder supertype(PartialRelation supertype) {
-                        supertypes.add(supertype);
-                        return this;
-                }
-
-                public Builder abstractType(boolean abstractType) {
-                        this.abstractType = abstractType;
-                        return this;
-                }
-
-                public Builder abstractType() {
-                        return abstractType(true);
-                }
-
-                public TypeInfo build() {
-                        return new TypeInfo(Collections.unmodifiableSet(supertypes), abstractType);
-                }
-        }
 }