diff options
author | 2024-01-01 19:14:51 +0100 | |
---|---|---|
committer | 2024-01-01 19:14:51 +0100 | |
commit | a496f9ae10b1c7d0fd0a876f9dae48923075d8b3 (patch) | |
tree | 49569b5df82308a3572ce486dd4e5f6e45d1fd46 /subprojects/language-web/src/main | |
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/language-web/src/main')
3 files changed, 50 insertions, 17 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 @@ | |||
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); |