feat: basic partial interpretation infrastructure

16 files changed, 176 insertions, 60 deletions

diff --git a/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java b/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java
index 1080a248..5e69e7af 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java
@@ -5,6 +5,9 @@
  */
 package tools.refinery.store.map;
 
+import java.util.Iterator;
+import java.util.Map;
+
 public final class Cursors {
     private Cursors() {
         throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
@@ -18,6 +21,14 @@ public final class Cursors {
                 return new Singleton<>(key, value);
         }
 
+        public static <K, V> Cursor<K, V> of(Iterator<Map.Entry<K, V>> iterator) {
+                return new IteratorBasedCursor<>(iterator);
+        }
+
+        public static <K, V> Cursor<K, V> of(Map<K, V> map) {
+                return of(map.entrySet().iterator());
+        }
+
     private static class Empty<K, V> implements Cursor<K, V> {
         private boolean terminated = false;
 
diff --git a/subprojects/store/src/main/java/tools/refinery/store/map/IteratorBasedCursor.java b/subprojects/store/src/main/java/tools/refinery/store/map/IteratorBasedCursor.java
new file mode 100644
index 00000000..0ed9b730
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/map/IteratorBasedCursor.java
@@ -0,0 +1,44 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.map;
+
+import java.util.Iterator;
+import java.util.Map;
+
+public class IteratorBasedCursor<K, V> implements Cursor<K, V> {
+        private final Iterator<Map.Entry<K, V>> iterator;
+        private Map.Entry<K, V> entry;
+        private boolean terminated;
+
+        public IteratorBasedCursor(Iterator<Map.Entry<K, V>> iterator) {
+                this.iterator = iterator;
+        }
+
+        @Override
+        public K getKey() {
+                return entry.getKey();
+        }
+
+        @Override
+        public V getValue() {
+                return entry.getValue();
+        }
+
+        @Override
+        public boolean isTerminated() {
+                return terminated;
+        }
+
+        @Override
+        public boolean move() {
+                if (!terminated && iterator.hasNext()) {
+                        entry = iterator.next();
+                        return true;
+                }
+                terminated = true;
+                return false;
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java
index 3a4024b5..8f652762 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java
@@ -29,7 +29,9 @@ public interface ModelStoreBuilder {
 
         <T> ModelStoreBuilder symbol(Symbol<T> symbol);
 
-        <T extends ModelAdapterBuilder> ModelStoreBuilder with(T adapterBuilder);
+        ModelStoreBuilder with(ModelAdapterBuilder adapterBuilder);
+
+        ModelStoreBuilder with(ModelStoreConfiguration configuration);
 
         <T extends ModelAdapterBuilder> Optional<T> tryGetAdapter(Class<? extends T> adapterType);
 
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreConfiguration.java b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreConfiguration.java
new file mode 100644
index 00000000..e94af5f8
--- /dev/null
+++ b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreConfiguration.java
@@ -0,0 +1,11 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.model;
+
+@FunctionalInterface
+public interface ModelStoreConfiguration {
+        void apply(ModelStoreBuilder storeBuilder);
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java b/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java
index d9245c1d..3d7f59d7 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java
@@ -9,14 +9,9 @@ import org.eclipse.collections.api.factory.Maps;
 import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
 import org.eclipse.collections.api.map.MutableMap;
 import org.eclipse.collections.api.map.primitive.MutableIntObjectMap;
-import tools.refinery.store.map.AnyVersionedMap;
-import tools.refinery.store.map.Cursor;
-import tools.refinery.store.map.Cursors;
-import tools.refinery.store.map.VersionedMap;
+import tools.refinery.store.map.*;
 import tools.refinery.store.tuple.Tuple;
 
-import java.util.Iterator;
-import java.util.Map;
 import java.util.Set;
 
 class BaseIndexer<T> {
@@ -91,40 +86,12 @@ class BaseIndexer<T> {
                 return new IndexCursor<>(adjacentTuples, versionedMap);
         }
 
-        private static class IndexCursor<T> implements Cursor<Tuple, T> {
+        private static class IndexCursor<T> extends IteratorBasedCursor<Tuple, T> {
                 private final Set<AnyVersionedMap> dependingMaps;
-                private final Iterator<Map.Entry<Tuple, T>> iterator;
-                private Map.Entry<Tuple, T> entry;
-                private boolean terminated;
 
-                public IndexCursor(MutableMap<Tuple, T> adjacentTuples, VersionedMap<Tuple, T> versionedMap) {
+                public IndexCursor(MutableMap<Tuple, T> map, VersionedMap<Tuple, T> versionedMap) {
+                        super(map.entrySet().iterator());
                         dependingMaps = versionedMap == null ? Set.of() : Set.of(versionedMap);
-                        iterator = adjacentTuples.entrySet().iterator();
-                }
-
-                @Override
-                public Tuple getKey() {
-                        return entry.getKey();
-                }
-
-                @Override
-                public T getValue() {
-                        return entry.getValue();
-                }
-
-                @Override
-                public boolean isTerminated() {
-                        return terminated;
-                }
-
-                @Override
-                public boolean move() {
-                        if (!terminated && iterator.hasNext()) {
-                                entry = iterator.next();
-                                return true;
-                        }
-                        terminated = true;
-                        return false;
                 }
 
                 @Override
diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java b/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java
index aafbe130..5c688178 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java
@@ -11,6 +11,7 @@ import tools.refinery.store.map.VersionedMapStore;
 import tools.refinery.store.map.VersionedMapStoreImpl;
 import tools.refinery.store.model.ModelStore;
 import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
 import tools.refinery.store.model.TupleHashProvider;
 import tools.refinery.store.representation.AnySymbol;
 import tools.refinery.store.representation.Symbol;
@@ -26,7 +27,8 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder {
         @Override
         public <T> ModelStoreBuilder symbol(Symbol<T> symbol) {
                 if (!allSymbols.add(symbol)) {
-                        throw new IllegalArgumentException("Symbol %s already added".formatted(symbol));
+                        // No need to add symbol twice.
+                        return this;
                 }
                 var equivalenceClass = new SymbolEquivalenceClass<>(symbol);
                 var symbolsInEquivalenceClass = equivalenceClasses.computeIfAbsent(equivalenceClass,
@@ -36,7 +38,7 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder {
         }
 
         @Override
-        public <T extends ModelAdapterBuilder> ModelStoreBuilder with(T adapterBuilder) {
+        public ModelStoreBuilder with(ModelAdapterBuilder adapterBuilder) {
                 for (var existingAdapter : adapters) {
                         if (existingAdapter.getClass().equals(adapterBuilder.getClass())) {
                                 throw new IllegalArgumentException("%s adapter was already configured for store builder"
@@ -48,6 +50,12 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder {
         }
 
         @Override
+        public ModelStoreBuilder with(ModelStoreConfiguration configuration) {
+                configuration.apply(this);
+                return this;
+        }
+
+        @Override
         public <T extends ModelAdapterBuilder> Optional<T> tryGetAdapter(Class<? extends T> adapterType) {
                 return AdapterUtils.tryGetAdapter(adapters, adapterType);
         }
@@ -59,13 +67,14 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder {
 
         @Override
         public ModelStore build() {
+                // First configure adapters and let them register any symbols we don't know about yet.
+                for (int i = adapters.size() - 1; i >= 0; i--) {
+                        adapters.get(i).configure(this);
+                }
                 var stores = new HashMap<AnySymbol, VersionedMapStore<Tuple, ?>>(allSymbols.size());
                 for (var entry : equivalenceClasses.entrySet()) {
                         createStores(stores, entry.getKey(), entry.getValue());
                 }
-                for (int i = adapters.size() - 1; i >= 0; i--) {
-                        adapters.get(i).configure(this);
-                }
                 var modelStore = new ModelStoreImpl(stores, adapters.size());
                 for (var adapterBuilder : adapters) {
                         var storeAdapter = adapterBuilder.build(modelStore);
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java
index 52c740e8..dfdb43bd 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java
@@ -5,6 +5,7 @@
  */
 package tools.refinery.store.representation;
 
+import java.util.Objects;
 import java.util.Optional;
 
 public non-sealed interface AbstractDomain<A, C> extends AnyAbstractDomain {
@@ -22,7 +23,9 @@ public non-sealed interface AbstractDomain<A, C> extends AnyAbstractDomain {
                 return toConcrete(abstractValue).isPresent();
         }
 
-        boolean isRefinement(A originalValue, A refinedValue);
+        default boolean isRefinement(A originalValue, A refinedValue) {
+                return Objects.equals(commonRefinement(originalValue, refinedValue), refinedValue);
+        }
 
         A commonRefinement(A leftValue, A rightValue);
 
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java
index 40baf9a5..f81ee9a4 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java
@@ -36,6 +36,10 @@ public enum TruthValue {
                 return this != UNKNOWN;
         }
 
+        public boolean isConcrete() {
+                return this == TRUE || this == FALSE;
+        }
+
         public boolean must() {
                 return this == TRUE || this == ERROR;
         }
@@ -55,9 +59,18 @@ public enum TruthValue {
         public TruthValue merge(TruthValue other) {
                 return switch (this) {
                         case TRUE -> other == UNKNOWN || other == TRUE ? TRUE : ERROR;
-                        case FALSE -> other == TruthValue.UNKNOWN || other == TruthValue.FALSE ? FALSE : ERROR;
+                        case FALSE -> other == UNKNOWN || other == FALSE ? FALSE : ERROR;
                         case UNKNOWN -> other;
-                        default -> ERROR;
+                        case ERROR -> ERROR;
+                };
+        }
+
+        public TruthValue join(TruthValue other) {
+                return switch (this) {
+                        case TRUE -> other == ERROR || other == TRUE ? TRUE : UNKNOWN;
+                        case FALSE -> other == ERROR || other == FALSE ? FALSE : UNKNOWN;
+                        case UNKNOWN -> UNKNOWN;
+                        case ERROR -> other;
                 };
         }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java
index 89f8dd19..61696dca 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java
@@ -7,6 +7,8 @@ package tools.refinery.store.representation;
 
 import java.util.Optional;
 
+// Singleton pattern, because there is only one domain for truth values.
+@SuppressWarnings("squid:S6548")
 public final class TruthValueDomain implements AbstractDomain<TruthValue, Boolean> {
         public static final TruthValueDomain INSTANCE = new TruthValueDomain();
 
@@ -15,51 +17,50 @@ public final class TruthValueDomain implements AbstractDomain<TruthValue, Boolea
 
         @Override
         public Class<TruthValue> abstractType() {
-                return null;
+                return TruthValue.class;
         }
 
         @Override
         public Class<Boolean> concreteType() {
-                return null;
+                return Boolean.class;
         }
 
         @Override
         public TruthValue toAbstract(Boolean concreteValue) {
-                return null;
+                return TruthValue.toTruthValue(concreteValue);
         }
 
         @Override
         public Optional<Boolean> toConcrete(TruthValue abstractValue) {
-                return Optional.empty();
+                return switch (abstractValue) {
+                        case TRUE -> Optional.of(true);
+                        case FALSE -> Optional.of(false);
+                        default -> Optional.empty();
+                };
         }
 
         @Override
         public boolean isConcrete(TruthValue abstractValue) {
-                return AbstractDomain.super.isConcrete(abstractValue);
-        }
-
-        @Override
-        public boolean isRefinement(TruthValue originalValue, TruthValue refinedValue) {
-                return false;
+                return abstractValue.isConcrete();
         }
 
         @Override
         public TruthValue commonRefinement(TruthValue leftValue, TruthValue rightValue) {
-                return null;
+                return leftValue.merge(rightValue);
         }
 
         @Override
         public TruthValue commonAncestor(TruthValue leftValue, TruthValue rightValue) {
-                return null;
+                return leftValue.join(rightValue);
         }
 
         @Override
         public TruthValue unknown() {
-                return null;
+                return TruthValue.UNKNOWN;
         }
 
         @Override
         public boolean isError(TruthValue abstractValue) {
-                return false;
+                return !abstractValue.isConsistent();
         }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java
index aae7b344..e9761763 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java
@@ -12,6 +12,8 @@ public sealed interface Tuple extends Comparable<Tuple> permits Tuple0, Tuple1,
 
         int get(int element);
 
+        Tuple set(int element, int value);
+
         @Override
         default int compareTo(@NotNull Tuple other) {
                 int size = getSize();
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java
index a9aa9bf2..5f525798 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java
@@ -29,6 +29,11 @@ public final class Tuple0 implements Tuple {
         }
 
         @Override
+        public Tuple set(int element, int value) {
+                throw new IndexOutOfBoundsException(element);
+        }
+
+        @Override
         public String toString() {
                 return TUPLE_BEGIN + TUPLE_END;
         }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java
index 388ee3a9..fb9497d2 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java
@@ -38,6 +38,14 @@ public final class Tuple1 implements Tuple {
         }
 
         @Override
+        public Tuple set(int element, int value) {
+                if (element == 0) {
+                        return Tuple.of(value);
+                }
+                throw new IndexOutOfBoundsException(element);
+        }
+
+        @Override
         public String toString() {
                 return TUPLE_BEGIN + value0 + TUPLE_END;
         }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java
index 6d886fd3..2213df97 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java
@@ -25,6 +25,15 @@ public record Tuple2(int value0, int value1) implements Tuple {
         }
 
         @Override
+        public Tuple set(int element, int value) {
+                return switch (element) {
+                        case 0 -> Tuple.of(value, value1);
+                        case 1 -> Tuple.of(value0, value);
+                        default -> throw new ArrayIndexOutOfBoundsException(element);
+                };
+        }
+
+        @Override
         public String toString() {
                 return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_END;
         }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java
index 734e45c2..417770e8 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java
@@ -26,6 +26,16 @@ public record Tuple3(int value0, int value1, int value2) implements Tuple {
         }
 
         @Override
+        public Tuple set(int element, int value) {
+                return switch (element) {
+                        case 0 -> Tuple.of(value, value1, value2);
+                        case 1 -> Tuple.of(value0, value, value2);
+                        case 2 -> Tuple.of(value0, value1, value);
+                        default -> throw new ArrayIndexOutOfBoundsException(element);
+                };
+        }
+
+        @Override
         public String toString() {
                 return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_SEPARATOR + value2 + TUPLE_END;
         }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java
index e1b93e7b..c4915198 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java
@@ -27,6 +27,17 @@ public record Tuple4(int value0, int value1, int value2, int value3) implements
         }
 
         @Override
+        public Tuple set(int element, int value) {
+                return switch (element) {
+                        case 0 -> Tuple.of(value, value1, value2, value3);
+                        case 1 -> Tuple.of(value0, value, value2, value3);
+                        case 2 -> Tuple.of(value0, value1, value, value3);
+                        case 3 -> Tuple.of(value0, value1, value2, value);
+                        default -> throw new ArrayIndexOutOfBoundsException(element);
+                };
+        }
+
+        @Override
         public String toString() {
                 return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_SEPARATOR + value2 + TUPLE_SEPARATOR + value3 +
                                 TUPLE_END;
diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java
index b66af491..b42b4b6a 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java
@@ -32,6 +32,16 @@ public final class TupleN implements Tuple {
         }
 
         @Override
+        public Tuple set(int element, int value) {
+                int size = getSize();
+                var newValues = new int[size];
+                for (int i = 0; i < size; i++) {
+                        newValues[i] = element == i ? value : values[i];
+                }
+                return Tuple.of(newValues);
+        }
+
+        @Override
         public String toString() {
                 var valuesString = Arrays.stream(values)
                                 .mapToObj(Integer::toString)