diff options
author | Kristóf Marussy <kristof@marussy.com> | 2024-01-01 19:14:51 +0100 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2024-01-01 19:14:51 +0100 |
commit | a496f9ae10b1c7d0fd0a876f9dae48923075d8b3 (patch) | |
tree | 49569b5df82308a3572ce486dd4e5f6e45d1fd46 /subprojects | |
parent | Merge pull request #50 from kris7t/generator-roundtrip (diff) | |
download | refinery-a496f9ae10b1c7d0fd0a876f9dae48923075d8b3.tar.gz refinery-a496f9ae10b1c7d0fd0a876f9dae48923075d8b3.tar.zst refinery-a496f9ae10b1c7d0fd0a876f9dae48923075d8b3.zip |
refactor: matching node names in CLI and web
Diffstat (limited to 'subprojects')
5 files changed, 121 insertions, 46 deletions
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/NodeNameProvider.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/NodeNameProvider.java new file mode 100644 index 00000000..517b8604 --- /dev/null +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/NodeNameProvider.java | |||
@@ -0,0 +1,62 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.language.semantics; | ||
7 | |||
8 | import com.google.inject.Inject; | ||
9 | import org.eclipse.collections.api.factory.primitive.ObjectIntMaps; | ||
10 | import org.eclipse.collections.api.map.primitive.MutableObjectIntMap; | ||
11 | import org.eclipse.xtext.naming.IQualifiedNameConverter; | ||
12 | import org.eclipse.xtext.naming.QualifiedName; | ||
13 | import org.eclipse.xtext.scoping.IScopeProvider; | ||
14 | import tools.refinery.language.model.problem.Node; | ||
15 | import tools.refinery.language.model.problem.Problem; | ||
16 | import tools.refinery.language.model.problem.ProblemPackage; | ||
17 | |||
18 | import java.util.Locale; | ||
19 | |||
20 | public class NodeNameProvider { | ||
21 | @Inject | ||
22 | private IQualifiedNameConverter qualifiedNameConverter; | ||
23 | |||
24 | @Inject | ||
25 | private SemanticsUtils semanticsUtils; | ||
26 | |||
27 | @Inject | ||
28 | private IScopeProvider scopeProvider; | ||
29 | |||
30 | private Problem problem; | ||
31 | private final MutableObjectIntMap<String> indexMap = ObjectIntMaps.mutable.empty(); | ||
32 | |||
33 | public void setProblem(Problem problem) { | ||
34 | if (this.problem != null) { | ||
35 | throw new IllegalStateException("Problem was already set"); | ||
36 | } | ||
37 | this.problem = problem; | ||
38 | } | ||
39 | |||
40 | public String getNextName(String typeName) { | ||
41 | if (problem == null) { | ||
42 | throw new IllegalStateException("Problem was not set"); | ||
43 | } | ||
44 | String namePrefix; | ||
45 | if (typeName == null || typeName.isEmpty()) { | ||
46 | namePrefix = "node"; | ||
47 | } else { | ||
48 | namePrefix = typeName.substring(0, 1).toLowerCase(Locale.ROOT) + typeName.substring(1); | ||
49 | } | ||
50 | int index = indexMap.getIfAbsent(namePrefix, 0); | ||
51 | String nodeName; | ||
52 | QualifiedName qualifiedName; | ||
53 | var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE); | ||
54 | do { | ||
55 | index++; | ||
56 | nodeName = namePrefix + index; | ||
57 | qualifiedName = qualifiedNameConverter.toQualifiedName(nodeName); | ||
58 | } while (semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class) != null); | ||
59 | indexMap.put(namePrefix, index); | ||
60 | return nodeName; | ||
61 | } | ||
62 | } | ||
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java index 57af599e..09ba34fc 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java | |||
@@ -1,5 +1,5 @@ | |||
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 | */ |
@@ -8,12 +8,9 @@ package tools.refinery.language.semantics; | |||
8 | import com.google.inject.Inject; | 8 | import com.google.inject.Inject; |
9 | import com.google.inject.Provider; | 9 | import com.google.inject.Provider; |
10 | import org.eclipse.collections.api.factory.primitive.IntObjectMaps; | 10 | import org.eclipse.collections.api.factory.primitive.IntObjectMaps; |
11 | import org.eclipse.collections.api.factory.primitive.ObjectIntMaps; | ||
12 | import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; | 11 | import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; |
13 | import org.eclipse.collections.api.map.primitive.MutableObjectIntMap; | ||
14 | import org.eclipse.emf.common.util.URI; | 12 | import org.eclipse.emf.common.util.URI; |
15 | import org.eclipse.emf.ecore.util.EcoreUtil; | 13 | import org.eclipse.emf.ecore.util.EcoreUtil; |
16 | import org.eclipse.xtext.naming.IQualifiedNameConverter; | ||
17 | import org.eclipse.xtext.naming.IQualifiedNameProvider; | 14 | import org.eclipse.xtext.naming.IQualifiedNameProvider; |
18 | import org.eclipse.xtext.naming.QualifiedName; | 15 | import org.eclipse.xtext.naming.QualifiedName; |
19 | import org.eclipse.xtext.resource.FileExtensionProvider; | 16 | import org.eclipse.xtext.resource.FileExtensionProvider; |
@@ -37,7 +34,6 @@ import tools.refinery.store.tuple.Tuple; | |||
37 | import java.io.ByteArrayInputStream; | 34 | import java.io.ByteArrayInputStream; |
38 | import java.io.ByteArrayOutputStream; | 35 | import java.io.ByteArrayOutputStream; |
39 | import java.io.IOException; | 36 | import java.io.IOException; |
40 | import java.util.Locale; | ||
41 | import java.util.Map; | 37 | import java.util.Map; |
42 | import java.util.TreeMap; | 38 | import java.util.TreeMap; |
43 | import java.util.TreeSet; | 39 | import java.util.TreeSet; |
@@ -57,9 +53,6 @@ public class SolutionSerializer { | |||
57 | private IQualifiedNameProvider qualifiedNameProvider; | 53 | private IQualifiedNameProvider qualifiedNameProvider; |
58 | 54 | ||
59 | @Inject | 55 | @Inject |
60 | private IQualifiedNameConverter qualifiedNameConverter; | ||
61 | |||
62 | @Inject | ||
63 | private SemanticsUtils semanticsUtils; | 56 | private SemanticsUtils semanticsUtils; |
64 | 57 | ||
65 | @Inject | 58 | @Inject |
@@ -68,6 +61,9 @@ public class SolutionSerializer { | |||
68 | @Inject | 61 | @Inject |
69 | private ProblemDesugarer desugarer; | 62 | private ProblemDesugarer desugarer; |
70 | 63 | ||
64 | @Inject | ||
65 | private NodeNameProvider nameProvider; | ||
66 | |||
71 | private ProblemTrace trace; | 67 | private ProblemTrace trace; |
72 | private Model model; | 68 | private Model model; |
73 | private ReasoningAdapter reasoningAdapter; | 69 | private ReasoningAdapter reasoningAdapter; |
@@ -95,6 +91,7 @@ public class SolutionSerializer { | |||
95 | problem = copyProblem(originalProblem, uri); | 91 | problem = copyProblem(originalProblem, uri); |
96 | problem.getStatements().removeIf(SolutionSerializer::shouldRemoveStatement); | 92 | problem.getStatements().removeIf(SolutionSerializer::shouldRemoveStatement); |
97 | problem.getNodes().removeIf(this::shouldRemoveNode); | 93 | problem.getNodes().removeIf(this::shouldRemoveNode); |
94 | nameProvider.setProblem(problem); | ||
98 | addExistsAssertions(); | 95 | addExistsAssertions(); |
99 | addClassAssertions(); | 96 | addClassAssertions(); |
100 | addReferenceAssertions(); | 97 | addReferenceAssertions(); |
@@ -172,11 +169,6 @@ public class SolutionSerializer { | |||
172 | return findNode(qualifiedName); | 169 | return findNode(qualifiedName); |
173 | } | 170 | } |
174 | 171 | ||
175 | private Node findNode(String name) { | ||
176 | var qualifiedName = qualifiedNameConverter.toQualifiedName(name); | ||
177 | return findNode(qualifiedName); | ||
178 | } | ||
179 | |||
180 | private Node findNode(QualifiedName qualifiedName) { | 172 | private Node findNode(QualifiedName qualifiedName) { |
181 | var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE); | 173 | var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE); |
182 | return semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class); | 174 | return semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class); |
@@ -222,19 +214,17 @@ public class SolutionSerializer { | |||
222 | private void addClassAssertions() { | 214 | private void addClassAssertions() { |
223 | var types = trace.getMetamodel().typeHierarchy().getPreservedTypes().keySet().stream() | 215 | var types = trace.getMetamodel().typeHierarchy().getPreservedTypes().keySet().stream() |
224 | .collect(Collectors.toMap(Function.identity(), this::findPartialRelation)); | 216 | .collect(Collectors.toMap(Function.identity(), this::findPartialRelation)); |
225 | var indexMap = ObjectIntMaps.mutable.empty(); | ||
226 | var cursor = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL).getAll(); | 217 | var cursor = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL).getAll(); |
227 | while (cursor.move()) { | 218 | while (cursor.move()) { |
228 | var key = cursor.getKey(); | 219 | var key = cursor.getKey(); |
229 | var nodeId = key.get(0); | 220 | var nodeId = key.get(0); |
230 | if (isExistingNode(nodeId)) { | 221 | if (isExistingNode(nodeId)) { |
231 | createNodeAndAssertType(nodeId, cursor.getValue(), types, indexMap); | 222 | createNodeAndAssertType(nodeId, cursor.getValue(), types); |
232 | } | 223 | } |
233 | } | 224 | } |
234 | } | 225 | } |
235 | 226 | ||
236 | private void createNodeAndAssertType(int nodeId, InferredType inferredType, Map<PartialRelation, Relation> types, | 227 | private void createNodeAndAssertType(int nodeId, InferredType inferredType, Map<PartialRelation, Relation> types) { |
237 | MutableObjectIntMap<Object> indexMap) { | ||
238 | var candidateTypeSymbol = inferredType.candidateType(); | 228 | var candidateTypeSymbol = inferredType.candidateType(); |
239 | var candidateRelation = types.get(candidateTypeSymbol); | 229 | var candidateRelation = types.get(candidateTypeSymbol); |
240 | if (candidateRelation instanceof EnumDeclaration) { | 230 | if (candidateRelation instanceof EnumDeclaration) { |
@@ -243,18 +233,8 @@ public class SolutionSerializer { | |||
243 | } | 233 | } |
244 | Node node = nodes.get(nodeId); | 234 | Node node = nodes.get(nodeId); |
245 | if (node == null) { | 235 | if (node == null) { |
246 | String typeName = candidateRelation.getName(); | 236 | var typeName = candidateRelation.getName(); |
247 | if (typeName == null || typeName.isEmpty()) { | 237 | var nodeName = nameProvider.getNextName(typeName); |
248 | typeName = "node"; | ||
249 | } else { | ||
250 | typeName = typeName.substring(0, 1).toLowerCase(Locale.ROOT) + typeName.substring(1); | ||
251 | } | ||
252 | int index = indexMap.getIfAbsent(typeName, 0); | ||
253 | String nodeName; | ||
254 | do { | ||
255 | index++; | ||
256 | nodeName = typeName + index; | ||
257 | } while (findNode(nodeName) != null); | ||
258 | node = ProblemFactory.eINSTANCE.createNode(); | 238 | node = ProblemFactory.eINSTANCE.createNode(); |
259 | node.setName(nodeName); | 239 | node.setName(nodeName); |
260 | problem.getNodes().add(node); | 240 | problem.getNodes().add(node); |
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 @@ | |||
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 | */ |
@@ -17,6 +17,7 @@ import tools.refinery.generator.ValidationErrorsException; | |||
17 | import tools.refinery.language.web.semantics.PartialInterpretation2Json; | 17 | import tools.refinery.language.web.semantics.PartialInterpretation2Json; |
18 | import tools.refinery.language.web.xtext.server.ThreadPoolExecutorServiceProvider; | 18 | import tools.refinery.language.web.xtext.server.ThreadPoolExecutorServiceProvider; |
19 | import tools.refinery.language.web.xtext.server.push.PushWebDocument; | 19 | import tools.refinery.language.web.xtext.server.push.PushWebDocument; |
20 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
20 | import tools.refinery.store.util.CancellationToken; | 21 | import tools.refinery.store.util.CancellationToken; |
21 | 22 | ||
22 | import java.io.IOException; | 23 | import java.io.IOException; |
@@ -142,7 +143,7 @@ public class ModelGenerationWorker implements Runnable { | |||
142 | } catch (ValidationErrorsException e) { | 143 | } catch (ValidationErrorsException e) { |
143 | var errors = e.getErrors(); | 144 | var errors = e.getErrors(); |
144 | if (errors != null && !errors.isEmpty()) { | 145 | if (errors != null && !errors.isEmpty()) { |
145 | return new ModelGenerationErrorResult(uuid, "Validation error: " + errors.get(0).getMessage()); | 146 | return new ModelGenerationErrorResult(uuid, "Validation error: " + errors.getFirst().getMessage()); |
146 | } | 147 | } |
147 | throw e; | 148 | throw e; |
148 | } | 149 | } |
@@ -154,7 +155,7 @@ public class ModelGenerationWorker implements Runnable { | |||
154 | notifyResult(new ModelGenerationStatusResult(uuid, "Saving generated model")); | 155 | notifyResult(new ModelGenerationStatusResult(uuid, "Saving generated model")); |
155 | cancellationToken.checkCancelled(); | 156 | cancellationToken.checkCancelled(); |
156 | metadataCreator.setProblemTrace(generator.getProblemTrace()); | 157 | metadataCreator.setProblemTrace(generator.getProblemTrace()); |
157 | var nodesMetadata = metadataCreator.getNodesMetadata(generator.getModel(), false); | 158 | var nodesMetadata = metadataCreator.getNodesMetadata(generator.getModel(), Concreteness.CANDIDATE); |
158 | cancellationToken.checkCancelled(); | 159 | cancellationToken.checkCancelled(); |
159 | var relationsMetadata = metadataCreator.getRelationsMetadata(); | 160 | var relationsMetadata = metadataCreator.getRelationsMetadata(); |
160 | cancellationToken.checkCancelled(); | 161 | 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 @@ | |||
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 | */ |
@@ -20,6 +20,7 @@ import tools.refinery.generator.ModelSemanticsFactory; | |||
20 | import tools.refinery.language.model.problem.Problem; | 20 | import tools.refinery.language.model.problem.Problem; |
21 | import tools.refinery.language.web.semantics.metadata.MetadataCreator; | 21 | import tools.refinery.language.web.semantics.metadata.MetadataCreator; |
22 | import tools.refinery.language.semantics.TracedException; | 22 | import tools.refinery.language.semantics.TracedException; |
23 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
23 | import tools.refinery.store.reasoning.translator.TranslationException; | 24 | import tools.refinery.store.reasoning.translator.TranslationException; |
24 | import tools.refinery.store.util.CancellationToken; | 25 | import tools.refinery.store.util.CancellationToken; |
25 | 26 | ||
@@ -73,7 +74,7 @@ class SemanticsWorker implements Callable<SemanticsResult> { | |||
73 | } | 74 | } |
74 | cancellationToken.checkCancelled(); | 75 | cancellationToken.checkCancelled(); |
75 | metadataCreator.setProblemTrace(semantics.getProblemTrace()); | 76 | metadataCreator.setProblemTrace(semantics.getProblemTrace()); |
76 | var nodesMetadata = metadataCreator.getNodesMetadata(semantics.getModel(), true); | 77 | var nodesMetadata = metadataCreator.getNodesMetadata(semantics.getModel(), Concreteness.PARTIAL); |
77 | cancellationToken.checkCancelled(); | 78 | cancellationToken.checkCancelled(); |
78 | var relationsMetadata = metadataCreator.getRelationsMetadata(); | 79 | var relationsMetadata = metadataCreator.getRelationsMetadata(); |
79 | cancellationToken.checkCancelled(); | 80 | 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..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); |