diff options
Diffstat (limited to 'subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/MetadataCreator.java')
-rw-r--r-- | subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/metadata/MetadataCreator.java | 55 |
1 files changed, 43 insertions, 12 deletions
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..67ef82ce 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,29 +1,36 @@ | |||
1 | /* | 1 | /* |
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | 2 | * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors <https://refinery.tools/> |
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
6 | package tools.refinery.language.web.semantics.metadata; | 6 | package tools.refinery.language.web.semantics.metadata; |
7 | 7 | ||
8 | import com.google.inject.Inject; | 8 | import com.google.inject.Inject; |
9 | import com.google.inject.Provider; | ||
9 | import org.eclipse.emf.ecore.EObject; | 10 | import org.eclipse.emf.ecore.EObject; |
10 | import org.eclipse.xtext.naming.IQualifiedNameConverter; | 11 | import org.eclipse.xtext.naming.IQualifiedNameConverter; |
11 | import org.eclipse.xtext.naming.IQualifiedNameProvider; | 12 | import org.eclipse.xtext.naming.IQualifiedNameProvider; |
12 | import org.eclipse.xtext.naming.QualifiedName; | 13 | import org.eclipse.xtext.naming.QualifiedName; |
13 | import org.eclipse.xtext.scoping.IScope; | 14 | import org.eclipse.xtext.scoping.IScope; |
14 | import org.eclipse.xtext.scoping.IScopeProvider; | 15 | import org.eclipse.xtext.scoping.IScopeProvider; |
16 | import org.jetbrains.annotations.NotNull; | ||
15 | import tools.refinery.language.model.problem.*; | 17 | import tools.refinery.language.model.problem.*; |
18 | import tools.refinery.language.semantics.NodeNameProvider; | ||
16 | import tools.refinery.language.semantics.ProblemTrace; | 19 | import tools.refinery.language.semantics.ProblemTrace; |
17 | import tools.refinery.language.semantics.TracedException; | 20 | import tools.refinery.language.semantics.TracedException; |
18 | import tools.refinery.language.utils.ProblemUtil; | 21 | import tools.refinery.language.utils.ProblemUtil; |
19 | import tools.refinery.store.model.Model; | 22 | import tools.refinery.store.model.Model; |
20 | import tools.refinery.store.reasoning.ReasoningAdapter; | 23 | import tools.refinery.store.reasoning.ReasoningAdapter; |
24 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
21 | import tools.refinery.store.reasoning.representation.PartialRelation; | 25 | import tools.refinery.store.reasoning.representation.PartialRelation; |
26 | import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator; | ||
27 | import tools.refinery.store.tuple.Tuple; | ||
22 | 28 | ||
23 | import java.util.ArrayList; | 29 | import java.util.ArrayList; |
24 | import java.util.Collections; | 30 | import java.util.Collections; |
25 | import java.util.Comparator; | 31 | import java.util.Comparator; |
26 | import java.util.List; | 32 | import java.util.List; |
33 | import java.util.function.IntFunction; | ||
27 | 34 | ||
28 | public class MetadataCreator { | 35 | public class MetadataCreator { |
29 | @Inject | 36 | @Inject |
@@ -35,10 +42,11 @@ public class MetadataCreator { | |||
35 | @Inject | 42 | @Inject |
36 | private IQualifiedNameConverter qualifiedNameConverter; | 43 | private IQualifiedNameConverter qualifiedNameConverter; |
37 | 44 | ||
38 | private ProblemTrace problemTrace; | 45 | @Inject |
46 | private Provider<NodeNameProvider> nodeNameProviderProvider; | ||
39 | 47 | ||
48 | private ProblemTrace problemTrace; | ||
40 | private IScope nodeScope; | 49 | private IScope nodeScope; |
41 | |||
42 | private IScope relationScope; | 50 | private IScope relationScope; |
43 | 51 | ||
44 | public void setProblemTrace(ProblemTrace problemTrace) { | 52 | public void setProblemTrace(ProblemTrace problemTrace) { |
@@ -51,32 +59,55 @@ public class MetadataCreator { | |||
51 | relationScope = scopeProvider.getScope(problem, ProblemPackage.Literals.ASSERTION__RELATION); | 59 | relationScope = scopeProvider.getScope(problem, ProblemPackage.Literals.ASSERTION__RELATION); |
52 | } | 60 | } |
53 | 61 | ||
54 | public static String unnamedNode(int nodeId) { | 62 | public List<NodeMetadata> getNodesMetadata(Model model, Concreteness concreteness) { |
55 | return "::" + nodeId; | ||
56 | } | ||
57 | |||
58 | public List<NodeMetadata> getNodesMetadata(Model model, boolean preserveNewNodes) { | ||
59 | int nodeCount = model.getAdapter(ReasoningAdapter.class).getNodeCount(); | 63 | int nodeCount = model.getAdapter(ReasoningAdapter.class).getNodeCount(); |
60 | var nodeTrace = problemTrace.getNodeTrace(); | 64 | var nodeTrace = problemTrace.getNodeTrace(); |
61 | var nodes = new NodeMetadata[Math.max(nodeTrace.size(), nodeCount)]; | 65 | var nodes = new NodeMetadata[Math.max(nodeTrace.size(), nodeCount)]; |
66 | var getName = makeGetName(model, concreteness); | ||
67 | boolean preserveNewNodes = concreteness == Concreteness.PARTIAL; | ||
62 | for (var entry : nodeTrace.keyValuesView()) { | 68 | for (var entry : nodeTrace.keyValuesView()) { |
63 | var node = entry.getOne(); | 69 | var node = entry.getOne(); |
64 | var id = entry.getTwo(); | 70 | var id = entry.getTwo(); |
65 | nodes[id] = getNodeMetadata(id, node, preserveNewNodes); | 71 | nodes[id] = getNodeMetadata(id, node, preserveNewNodes, getName); |
66 | } | 72 | } |
67 | for (int i = 0; i < nodes.length; i++) { | 73 | for (int i = 0; i < nodes.length; i++) { |
68 | if (nodes[i] == null) { | 74 | if (nodes[i] == null) { |
69 | var nodeName = unnamedNode(i); | 75 | var nodeName = getName.apply(i); |
70 | nodes[i] = new NodeMetadata(nodeName, nodeName, NodeKind.IMPLICIT); | 76 | nodes[i] = new NodeMetadata(nodeName, nodeName, NodeKind.IMPLICIT); |
71 | } | 77 | } |
72 | } | 78 | } |
73 | return List.of(nodes); | 79 | return List.of(nodes); |
74 | } | 80 | } |
75 | 81 | ||
76 | private NodeMetadata getNodeMetadata(int nodeId, Node node, boolean preserveNewNodes) { | 82 | @NotNull |
83 | private IntFunction<String> makeGetName(Model model, Concreteness concreteness) { | ||
84 | var nodeNameProvider = nodeNameProviderProvider.get(); | ||
85 | nodeNameProvider.setProblem(problemTrace.getProblem()); | ||
86 | var typeInterpretation = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL); | ||
87 | var existsInterpretation = model.getAdapter(ReasoningAdapter.class).getPartialInterpretation(concreteness, | ||
88 | ReasoningAdapter.EXISTS_SYMBOL); | ||
89 | return nodeId -> { | ||
90 | var key = Tuple.of(nodeId); | ||
91 | var inferredType = typeInterpretation.get(key); | ||
92 | if (inferredType == null || inferredType.candidateType() == null) { | ||
93 | return nodeNameProvider.getNextName(null); | ||
94 | } | ||
95 | if (concreteness == Concreteness.CANDIDATE && !existsInterpretation.get(key).may()) { | ||
96 | // Do not increment the node name counter for non-existent nodes in the candidate interpretation. | ||
97 | // While non-existent nodes may appear in the partial interpretation, they are never displayed in the | ||
98 | // candidate interpretation. | ||
99 | return "::" + nodeId; | ||
100 | } | ||
101 | var relation = problemTrace.getRelation(inferredType.candidateType()); | ||
102 | return nodeNameProvider.getNextName(relation.getName()); | ||
103 | }; | ||
104 | } | ||
105 | |||
106 | private NodeMetadata getNodeMetadata(int nodeId, Node node, boolean preserveNewNodes, | ||
107 | IntFunction<String> getName) { | ||
77 | var kind = getNodeKind(node); | 108 | var kind = getNodeKind(node); |
78 | if (!preserveNewNodes && kind == NodeKind.NEW) { | 109 | if (!preserveNewNodes && kind == NodeKind.NEW) { |
79 | var nodeName = unnamedNode(nodeId); | 110 | var nodeName = getName.apply(nodeId); |
80 | return new NodeMetadata(nodeName, nodeName, NodeKind.IMPLICIT); | 111 | return new NodeMetadata(nodeName, nodeName, NodeKind.IMPLICIT); |
81 | } | 112 | } |
82 | var qualifiedName = getQualifiedName(node); | 113 | var qualifiedName = getQualifiedName(node); |