Merge pull request #51 from kris7t/color-identifiers

Color identifiers

5 files changed, 114 insertions, 22 deletions

diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java
index a3b6ca82..7febce7d 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java
@@ -1,5 +1,5 @@
 /*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/>
  *
  * SPDX-License-Identifier: EPL-2.0
  */
@@ -17,6 +17,7 @@ import tools.refinery.generator.ValidationErrorsException;
 import tools.refinery.language.web.semantics.PartialInterpretation2Json;
 import tools.refinery.language.web.xtext.server.ThreadPoolExecutorServiceProvider;
 import tools.refinery.language.web.xtext.server.push.PushWebDocument;
+import tools.refinery.store.reasoning.literal.Concreteness;
 import tools.refinery.store.util.CancellationToken;
 
 import java.io.IOException;
@@ -142,7 +143,7 @@ public class ModelGenerationWorker implements Runnable {
                 } catch (ValidationErrorsException e) {
                         var errors = e.getErrors();
                         if (errors != null && !errors.isEmpty()) {
-                                return new ModelGenerationErrorResult(uuid, "Validation error: " + errors.get(0).getMessage());
+                                return new ModelGenerationErrorResult(uuid, "Validation error: " + errors.getFirst().getMessage());
                         }
                         throw e;
                 }
@@ -154,7 +155,7 @@ public class ModelGenerationWorker implements Runnable {
                 notifyResult(new ModelGenerationStatusResult(uuid, "Saving generated model"));
                 cancellationToken.checkCancelled();
                 metadataCreator.setProblemTrace(generator.getProblemTrace());
-                var nodesMetadata = metadataCreator.getNodesMetadata(generator.getModel(), false);
+                var nodesMetadata = metadataCreator.getNodesMetadata(generator.getModel(), Concreteness.CANDIDATE);
                 cancellationToken.checkCancelled();
                 var relationsMetadata = metadataCreator.getRelationsMetadata();
                 cancellationToken.checkCancelled();
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java
index 44974869..fed3c8a3 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java
@@ -1,5 +1,5 @@
 /*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/>
  *
  * SPDX-License-Identifier: EPL-2.0
  */
@@ -20,6 +20,7 @@ import tools.refinery.generator.ModelSemanticsFactory;
 import tools.refinery.language.model.problem.Problem;
 import tools.refinery.language.web.semantics.metadata.MetadataCreator;
 import tools.refinery.language.semantics.TracedException;
+import tools.refinery.store.reasoning.literal.Concreteness;
 import tools.refinery.store.reasoning.translator.TranslationException;
 import tools.refinery.store.util.CancellationToken;
 
@@ -73,7 +74,7 @@ class SemanticsWorker implements Callable<SemanticsResult> {
                 }
                 cancellationToken.checkCancelled();
                 metadataCreator.setProblemTrace(semantics.getProblemTrace());
-                var nodesMetadata = metadataCreator.getNodesMetadata(semantics.getModel(), true);
+                var nodesMetadata = metadataCreator.getNodesMetadata(semantics.getModel(), Concreteness.PARTIAL);
                 cancellationToken.checkCancelled();
                 var relationsMetadata = metadataCreator.getRelationsMetadata();
                 cancellationToken.checkCancelled();
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/MetadataCreator.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/MetadataCreator.java
index 3fbc5d2d..f05abc45 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/MetadataCreator.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/MetadataCreator.java
@@ -1,11 +1,12 @@
 /*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/>
  *
  * SPDX-License-Identifier: EPL-2.0
  */
 package tools.refinery.language.web.semantics.metadata;
 
 import com.google.inject.Inject;
+import com.google.inject.Provider;
 import org.eclipse.emf.ecore.EObject;
 import org.eclipse.xtext.naming.IQualifiedNameConverter;
 import org.eclipse.xtext.naming.IQualifiedNameProvider;
@@ -18,6 +19,7 @@ import tools.refinery.language.semantics.TracedException;
 import tools.refinery.language.utils.ProblemUtil;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.literal.Concreteness;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 
 import java.util.ArrayList;
@@ -35,10 +37,11 @@ public class MetadataCreator {
         @Inject
         private IQualifiedNameConverter qualifiedNameConverter;
 
-        private ProblemTrace problemTrace;
+        @Inject
+        private Provider<NodeMetadataFactory> nodeMetadataFactoryProvider;
 
+        private ProblemTrace problemTrace;
         private IScope nodeScope;
-
         private IScope relationScope;
 
         public void setProblemTrace(ProblemTrace problemTrace) {
@@ -51,37 +54,35 @@ public class MetadataCreator {
                 relationScope = scopeProvider.getScope(problem, ProblemPackage.Literals.ASSERTION__RELATION);
         }
 
-        public static String unnamedNode(int nodeId) {
-                return "::" + nodeId;
-        }
-
-        public List<NodeMetadata> getNodesMetadata(Model model, boolean preserveNewNodes) {
+        public List<NodeMetadata> getNodesMetadata(Model model, Concreteness concreteness) {
                 int nodeCount = model.getAdapter(ReasoningAdapter.class).getNodeCount();
                 var nodeTrace = problemTrace.getNodeTrace();
                 var nodes = new NodeMetadata[Math.max(nodeTrace.size(), nodeCount)];
+                var nodeMetadataFactory = nodeMetadataFactoryProvider.get();
+                nodeMetadataFactory.initialize(problemTrace, concreteness, model);
+                boolean preserveNewNodes = concreteness == Concreteness.PARTIAL;
                 for (var entry : nodeTrace.keyValuesView()) {
                         var node = entry.getOne();
                         var id = entry.getTwo();
-                        nodes[id] = getNodeMetadata(id, node, preserveNewNodes);
+                        nodes[id] = getNodeMetadata(id, node, preserveNewNodes, nodeMetadataFactory);
                 }
                 for (int i = 0; i < nodes.length; i++) {
                         if (nodes[i] == null) {
-                                var nodeName = unnamedNode(i);
-                                nodes[i] = new NodeMetadata(nodeName, nodeName, NodeKind.IMPLICIT);
+                                nodes[i] = nodeMetadataFactory.createFreshlyNamedMetadata(i);
                         }
                 }
                 return List.of(nodes);
         }
 
-        private NodeMetadata getNodeMetadata(int nodeId, Node node, boolean preserveNewNodes) {
+        private NodeMetadata getNodeMetadata(int nodeId, Node node, boolean preserveNewNodes,
+                                                                                 NodeMetadataFactory nodeMetadataFactory) {
                 var kind = getNodeKind(node);
                 if (!preserveNewNodes && kind == NodeKind.NEW) {
-                        var nodeName = unnamedNode(nodeId);
-                        return new NodeMetadata(nodeName, nodeName, NodeKind.IMPLICIT);
+                        return nodeMetadataFactory.createFreshlyNamedMetadata(nodeId);
                 }
                 var qualifiedName = getQualifiedName(node);
                 var simpleName = getSimpleName(node, qualifiedName, nodeScope);
-                return new NodeMetadata(qualifiedNameConverter.toString(qualifiedName),
+                return nodeMetadataFactory.doCreateMetadata(nodeId, qualifiedNameConverter.toString(qualifiedName),
                                 qualifiedNameConverter.toString(simpleName), getNodeKind(node));
         }
 
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/NodeMetadata.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/NodeMetadata.java
index 5da28acf..f3347eac 100644
--- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/NodeMetadata.java
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/NodeMetadata.java
@@ -1,9 +1,9 @@
 /*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2023-2023 The Refinery Authors <https://refinery.tools/>
  *
  * SPDX-License-Identifier: EPL-2.0
  */
 package tools.refinery.language.web.semantics.metadata;
 
-public record NodeMetadata(String name, String simpleName, NodeKind kind) implements Metadata {
+public record NodeMetadata(String name, String simpleName, String typeHash, NodeKind kind) implements Metadata {
 }
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/NodeMetadataFactory.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/NodeMetadataFactory.java
new file mode 100644
index 00000000..ce0e50c1
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/NodeMetadataFactory.java
@@ -0,0 +1,89 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.web.semantics.metadata;
+
+import com.google.inject.Inject;
+import tools.refinery.language.ide.syntaxcoloring.TypeHashProvider;
+import tools.refinery.language.semantics.NodeNameProvider;
+import tools.refinery.language.semantics.ProblemTrace;
+import tools.refinery.store.model.Interpretation;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.typehierarchy.InferredType;
+import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+public class NodeMetadataFactory {
+        @Inject
+        private NodeNameProvider nodeNameProvider;
+
+        @Inject
+        private TypeHashProvider typeHashProvider;
+
+        private ProblemTrace problemTrace;
+        private Concreteness concreteness;
+        private Interpretation<InferredType> typeInterpretation;
+        private PartialInterpretation<TruthValue, Boolean> existsInterpretation;
+
+        public void initialize(ProblemTrace problemTrace, Concreteness concreteness, Model model) {
+                this.problemTrace = problemTrace;
+                this.concreteness = concreteness;
+                typeInterpretation = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL);
+                existsInterpretation = model.getAdapter(ReasoningAdapter.class).getPartialInterpretation(concreteness,
+                                ReasoningAdapter.EXISTS_SYMBOL);
+                nodeNameProvider.setProblem(problemTrace.getProblem());
+        }
+
+        public NodeMetadata doCreateMetadata(int nodeId, String name, String simpleName, NodeKind kind) {
+                var type = getType(nodeId);
+                return doCreateMetadata(name, simpleName, type, kind);
+        }
+
+        public NodeMetadata createFreshlyNamedMetadata(int nodeId) {
+                var type = getType(nodeId);
+                var name = getName(type, nodeId);
+                return doCreateMetadata(name, name, type, NodeKind.IMPLICIT);
+        }
+
+        private PartialRelation getType(int nodeId) {
+                var inferredType = typeInterpretation.get(Tuple.of(nodeId));
+                if (inferredType == null) {
+                        return null;
+                }
+                return inferredType.candidateType();
+        }
+
+        private String getName(PartialRelation type, int nodeId) {
+                if (concreteness == Concreteness.CANDIDATE && !existsInterpretation.get(Tuple.of(nodeId)).may()) {
+                        // Do not increment the node name counter for non-existent nodes in the candidate interpretation.
+                        // While non-existent nodes may appear in the partial interpretation, they are never displayed in the
+                        // candidate interpretation.
+                        return "::" + nodeId;
+                }
+                if (type == null) {
+                        return nodeNameProvider.getNextName(null);
+                }
+                var relation = problemTrace.getRelation(type);
+                return nodeNameProvider.getNextName(relation.getName());
+        }
+
+        private NodeMetadata doCreateMetadata(String name, String simpleName, PartialRelation type, NodeKind kind) {
+                var typeHash = getTypeHash(type);
+                return new NodeMetadata(name, simpleName, typeHash, kind);
+        }
+
+        private String getTypeHash(PartialRelation type) {
+                if (type == null) {
+                        return null;
+                }
+                var relation = problemTrace.getRelation(type);
+                return typeHashProvider.getTypeHash(relation);
+        }
+}