diff options
Diffstat (limited to 'subprojects/language-semantics/src/main/java/tools')
4 files changed, 252 insertions, 111 deletions
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java index 38bf5a61..c2bca2a5 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java | |||
@@ -6,7 +6,9 @@ | |||
6 | package tools.refinery.language.semantics; | 6 | package tools.refinery.language.semantics; |
7 | 7 | ||
8 | import com.google.inject.Inject; | 8 | import com.google.inject.Inject; |
9 | import tools.refinery.language.library.BuiltinLibrary; | ||
9 | import tools.refinery.language.model.problem.*; | 10 | import tools.refinery.language.model.problem.*; |
11 | import tools.refinery.language.scoping.imports.ImportCollector; | ||
10 | import tools.refinery.language.semantics.internal.MutableSeed; | 12 | import tools.refinery.language.semantics.internal.MutableSeed; |
11 | import tools.refinery.language.utils.BuiltinSymbols; | 13 | import tools.refinery.language.utils.BuiltinSymbols; |
12 | import tools.refinery.language.utils.ProblemDesugarer; | 14 | import tools.refinery.language.utils.ProblemDesugarer; |
@@ -51,8 +53,13 @@ public class ModelInitializer { | |||
51 | @Inject | 53 | @Inject |
52 | private ProblemTraceImpl problemTrace; | 54 | private ProblemTraceImpl problemTrace; |
53 | 55 | ||
56 | @Inject | ||
57 | private ImportCollector importCollector; | ||
58 | |||
54 | private Problem problem; | 59 | private Problem problem; |
55 | 60 | ||
61 | private final Set<Problem> importedProblems = new HashSet<>(); | ||
62 | |||
56 | private BuiltinSymbols builtinSymbols; | 63 | private BuiltinSymbols builtinSymbols; |
57 | 64 | ||
58 | private PartialRelation nodeRelation; | 65 | private PartialRelation nodeRelation; |
@@ -82,6 +89,8 @@ public class ModelInitializer { | |||
82 | throw new IllegalArgumentException("Problem was already set"); | 89 | throw new IllegalArgumentException("Problem was already set"); |
83 | } | 90 | } |
84 | this.problem = problem; | 91 | this.problem = problem; |
92 | loadImportedProblems(); | ||
93 | importedProblems.add(problem); | ||
85 | problemTrace.setProblem(problem); | 94 | problemTrace.setProblem(problem); |
86 | try { | 95 | try { |
87 | builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException( | 96 | builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalArgumentException( |
@@ -128,6 +137,29 @@ public class ModelInitializer { | |||
128 | } | 137 | } |
129 | } | 138 | } |
130 | 139 | ||
140 | private void loadImportedProblems() { | ||
141 | var resource = problem.eResource(); | ||
142 | if (resource == null) { | ||
143 | return; | ||
144 | } | ||
145 | var resourceSet = resource.getResourceSet(); | ||
146 | if (resourceSet == null) { | ||
147 | return; | ||
148 | } | ||
149 | var importedUris = importCollector.getAllImports(resource).toUriSet(); | ||
150 | for (var uri : importedUris) { | ||
151 | if (BuiltinLibrary.BUILTIN_LIBRARY_URI.equals(uri)) { | ||
152 | // We hard-code the behavior of the builtin library. | ||
153 | continue; | ||
154 | } | ||
155 | var importedResource = resourceSet.getResource(uri, false); | ||
156 | if (importedResource != null && !importedResource.getContents().isEmpty() && | ||
157 | importedResource.getContents().getFirst() instanceof Problem importedProblem) { | ||
158 | importedProblems.add(importedProblem); | ||
159 | } | ||
160 | } | ||
161 | } | ||
162 | |||
131 | public void configureStoreBuilder(ModelStoreBuilder storeBuilder) { | 163 | public void configureStoreBuilder(ModelStoreBuilder storeBuilder) { |
132 | checkProblem(); | 164 | checkProblem(); |
133 | try { | 165 | try { |
@@ -168,19 +200,21 @@ public class ModelInitializer { | |||
168 | } | 200 | } |
169 | 201 | ||
170 | private void collectNodes() { | 202 | private void collectNodes() { |
171 | for (var statement : problem.getStatements()) { | 203 | for (var importedProblem : importedProblems) { |
172 | if (statement instanceof IndividualDeclaration individualDeclaration) { | 204 | for (var statement : importedProblem.getStatements()) { |
173 | for (var individual : individualDeclaration.getNodes()) { | 205 | if (statement instanceof NodeDeclaration nodeDeclaration) { |
174 | collectNode(individual); | 206 | for (var node : nodeDeclaration.getNodes()) { |
175 | } | 207 | collectNode(node); |
176 | } else if (statement instanceof ClassDeclaration classDeclaration) { | 208 | } |
177 | var newNode = classDeclaration.getNewNode(); | 209 | } else if (statement instanceof ClassDeclaration classDeclaration) { |
178 | if (newNode != null) { | 210 | var newNode = classDeclaration.getNewNode(); |
179 | collectNode(newNode); | 211 | if (newNode != null) { |
180 | } | 212 | collectNode(newNode); |
181 | } else if (statement instanceof EnumDeclaration enumDeclaration) { | 213 | } |
182 | for (var literal : enumDeclaration.getLiterals()) { | 214 | } else if (statement instanceof EnumDeclaration enumDeclaration) { |
183 | collectNode(literal); | 215 | for (var literal : enumDeclaration.getLiterals()) { |
216 | collectNode(literal); | ||
217 | } | ||
184 | } | 218 | } |
185 | } | 219 | } |
186 | } | 220 | } |
@@ -194,13 +228,15 @@ public class ModelInitializer { | |||
194 | } | 228 | } |
195 | 229 | ||
196 | private void collectPartialSymbols() { | 230 | private void collectPartialSymbols() { |
197 | for (var statement : problem.getStatements()) { | 231 | for (var importedProblem : importedProblems) { |
198 | if (statement instanceof ClassDeclaration classDeclaration) { | 232 | for (var statement : importedProblem.getStatements()) { |
199 | collectClassDeclarationSymbols(classDeclaration); | 233 | if (statement instanceof ClassDeclaration classDeclaration) { |
200 | } else if (statement instanceof EnumDeclaration enumDeclaration) { | 234 | collectClassDeclarationSymbols(classDeclaration); |
201 | collectPartialRelation(enumDeclaration, 1, TruthValue.FALSE, TruthValue.FALSE); | 235 | } else if (statement instanceof EnumDeclaration enumDeclaration) { |
202 | } else if (statement instanceof PredicateDefinition predicateDefinition) { | 236 | collectPartialRelation(enumDeclaration, 1, TruthValue.FALSE, TruthValue.FALSE); |
203 | collectPredicateDefinitionSymbol(predicateDefinition); | 237 | } else if (statement instanceof PredicateDefinition predicateDefinition) { |
238 | collectPredicateDefinitionSymbol(predicateDefinition); | ||
239 | } | ||
204 | } | 240 | } |
205 | } | 241 | } |
206 | } | 242 | } |
@@ -247,15 +283,17 @@ public class ModelInitializer { | |||
247 | } | 283 | } |
248 | 284 | ||
249 | private String getName(Relation relation) { | 285 | private String getName(Relation relation) { |
250 | return semanticsUtils.getName(relation).orElseGet(() -> "::" + relationInfoMap.size()); | 286 | return semanticsUtils.getNameWithoutRootPrefix(relation).orElseGet(() -> "::" + relationInfoMap.size()); |
251 | } | 287 | } |
252 | 288 | ||
253 | private void collectMetamodel() { | 289 | private void collectMetamodel() { |
254 | for (var statement : problem.getStatements()) { | 290 | for (var importedProblem : importedProblems) { |
255 | if (statement instanceof ClassDeclaration classDeclaration) { | 291 | for (var statement : importedProblem.getStatements()) { |
256 | collectClassDeclarationMetamodel(classDeclaration); | 292 | if (statement instanceof ClassDeclaration classDeclaration) { |
257 | } else if (statement instanceof EnumDeclaration enumDeclaration) { | 293 | collectClassDeclarationMetamodel(classDeclaration); |
258 | collectEnumMetamodel(enumDeclaration); | 294 | } else if (statement instanceof EnumDeclaration enumDeclaration) { |
295 | collectEnumMetamodel(enumDeclaration); | ||
296 | } | ||
259 | } | 297 | } |
260 | } | 298 | } |
261 | } | 299 | } |
@@ -350,17 +388,17 @@ public class ModelInitializer { | |||
350 | } | 388 | } |
351 | 389 | ||
352 | private void collectAssertions() { | 390 | private void collectAssertions() { |
353 | for (var statement : problem.getStatements()) { | 391 | for (var importedProblem : importedProblems) { |
354 | if (statement instanceof ClassDeclaration classDeclaration) { | 392 | for (var statement : importedProblem.getStatements()) { |
355 | collectClassDeclarationAssertions(classDeclaration); | 393 | if (statement instanceof ClassDeclaration classDeclaration) { |
356 | } else if (statement instanceof EnumDeclaration enumDeclaration) { | 394 | collectClassDeclarationAssertions(classDeclaration); |
357 | collectEnumAssertions(enumDeclaration); | 395 | } else if (statement instanceof EnumDeclaration enumDeclaration) { |
358 | } else if (statement instanceof IndividualDeclaration individualDeclaration) { | 396 | collectEnumAssertions(enumDeclaration); |
359 | for (var individual : individualDeclaration.getNodes()) { | 397 | } else if (statement instanceof NodeDeclaration nodeDeclaration) { |
360 | collectIndividualAssertions(individual); | 398 | collectNodeDeclarationAssertions(nodeDeclaration); |
399 | } else if (statement instanceof Assertion assertion) { | ||
400 | collectAssertion(assertion); | ||
361 | } | 401 | } |
362 | } else if (statement instanceof Assertion assertion) { | ||
363 | collectAssertion(assertion); | ||
364 | } | 402 | } |
365 | } | 403 | } |
366 | } | 404 | } |
@@ -379,7 +417,7 @@ public class ModelInitializer { | |||
379 | private void collectEnumAssertions(EnumDeclaration enumDeclaration) { | 417 | private void collectEnumAssertions(EnumDeclaration enumDeclaration) { |
380 | var overlay = MutableSeed.of(1, null); | 418 | var overlay = MutableSeed.of(1, null); |
381 | for (var literal : enumDeclaration.getLiterals()) { | 419 | for (var literal : enumDeclaration.getLiterals()) { |
382 | collectIndividualAssertions(literal); | 420 | collectCardinalityAssertions(literal, TruthValue.TRUE); |
383 | var nodeId = getNodeId(literal); | 421 | var nodeId = getNodeId(literal); |
384 | overlay.mergeValue(Tuple.of(nodeId), TruthValue.TRUE); | 422 | overlay.mergeValue(Tuple.of(nodeId), TruthValue.TRUE); |
385 | } | 423 | } |
@@ -387,9 +425,25 @@ public class ModelInitializer { | |||
387 | info.assertions().overwriteValues(overlay); | 425 | info.assertions().overwriteValues(overlay); |
388 | } | 426 | } |
389 | 427 | ||
390 | private void collectIndividualAssertions(Node node) { | 428 | private void collectNodeDeclarationAssertions(NodeDeclaration nodeDeclaration) { |
429 | var kind = nodeDeclaration.getKind(); | ||
430 | TruthValue value; | ||
431 | switch (kind) { | ||
432 | case ATOM -> value = TruthValue.TRUE; | ||
433 | case MULTI -> value = TruthValue.UNKNOWN; | ||
434 | case NODE -> { | ||
435 | return; | ||
436 | } | ||
437 | default -> throw new IllegalArgumentException("Unknown node kind: " + kind); | ||
438 | } | ||
439 | for (var node : nodeDeclaration.getNodes()) { | ||
440 | collectCardinalityAssertions(node, value); | ||
441 | } | ||
442 | } | ||
443 | |||
444 | private void collectCardinalityAssertions(Node node, TruthValue value) { | ||
391 | var nodeId = getNodeId(node); | 445 | var nodeId = getNodeId(node); |
392 | collectCardinalityAssertions(nodeId, TruthValue.TRUE); | 446 | collectCardinalityAssertions(nodeId, value); |
393 | } | 447 | } |
394 | 448 | ||
395 | private void collectCardinalityAssertions(int nodeId, TruthValue value) { | 449 | private void collectCardinalityAssertions(int nodeId, TruthValue value) { |
@@ -415,9 +469,11 @@ public class ModelInitializer { | |||
415 | } | 469 | } |
416 | 470 | ||
417 | private void fixClassDeclarationAssertions() { | 471 | private void fixClassDeclarationAssertions() { |
418 | for (var statement : problem.getStatements()) { | 472 | for (var importedProblem : importedProblems) { |
419 | if (statement instanceof ClassDeclaration classDeclaration) { | 473 | for (var statement : importedProblem.getStatements()) { |
420 | fixClassDeclarationAssertions(classDeclaration); | 474 | if (statement instanceof ClassDeclaration classDeclaration) { |
475 | fixClassDeclarationAssertions(classDeclaration); | ||
476 | } | ||
421 | } | 477 | } |
422 | } | 478 | } |
423 | } | 479 | } |
@@ -485,9 +541,11 @@ public class ModelInitializer { | |||
485 | } | 541 | } |
486 | 542 | ||
487 | private void collectPredicates(ModelStoreBuilder storeBuilder) { | 543 | private void collectPredicates(ModelStoreBuilder storeBuilder) { |
488 | for (var statement : problem.getStatements()) { | 544 | for (var importedProblem : importedProblems) { |
489 | if (statement instanceof PredicateDefinition predicateDefinition) { | 545 | for (var statement : importedProblem.getStatements()) { |
490 | collectPredicateDefinitionTraced(predicateDefinition, storeBuilder); | 546 | if (statement instanceof PredicateDefinition predicateDefinition) { |
547 | collectPredicateDefinitionTraced(predicateDefinition, storeBuilder); | ||
548 | } | ||
491 | } | 549 | } |
492 | } | 550 | } |
493 | } | 551 | } |
@@ -587,18 +645,21 @@ public class ModelInitializer { | |||
587 | 645 | ||
588 | private void toLiterals(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope, | 646 | private void toLiterals(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope, |
589 | List<Literal> literals) { | 647 | List<Literal> literals) { |
590 | if (expr instanceof LogicConstant logicConstant) { | 648 | switch (expr) { |
649 | case LogicConstant logicConstant -> { | ||
591 | switch (logicConstant.getLogicValue()) { | 650 | switch (logicConstant.getLogicValue()) { |
592 | case TRUE -> literals.add(BooleanLiteral.TRUE); | 651 | case TRUE -> literals.add(BooleanLiteral.TRUE); |
593 | case FALSE -> literals.add(BooleanLiteral.FALSE); | 652 | case FALSE -> literals.add(BooleanLiteral.FALSE); |
594 | default -> throw new TracedException(logicConstant, "Unsupported literal"); | 653 | default -> throw new TracedException(logicConstant, "Unsupported literal"); |
595 | } | 654 | } |
596 | } else if (expr instanceof Atom atom) { | 655 | } |
656 | case Atom atom -> { | ||
597 | var target = getPartialRelation(atom.getRelation()); | 657 | var target = getPartialRelation(atom.getRelation()); |
598 | var polarity = atom.isTransitiveClosure() ? CallPolarity.TRANSITIVE : CallPolarity.POSITIVE; | 658 | var polarity = atom.isTransitiveClosure() ? CallPolarity.TRANSITIVE : CallPolarity.POSITIVE; |
599 | var argumentList = toArgumentList(atom.getArguments(), localScope, literals); | 659 | var argumentList = toArgumentList(atom.getArguments(), localScope, literals); |
600 | literals.add(target.call(polarity, argumentList)); | 660 | literals.add(target.call(polarity, argumentList)); |
601 | } else if (expr instanceof NegationExpr negationExpr) { | 661 | } |
662 | case NegationExpr negationExpr -> { | ||
602 | var body = negationExpr.getBody(); | 663 | var body = negationExpr.getBody(); |
603 | if (!(body instanceof Atom atom)) { | 664 | if (!(body instanceof Atom atom)) { |
604 | throw new TracedException(body, "Cannot negate literal"); | 665 | throw new TracedException(body, "Cannot negate literal"); |
@@ -615,7 +676,8 @@ public class ModelInitializer { | |||
615 | var negatedScope = extendScope(localScope, negationExpr.getImplicitVariables()); | 676 | var negatedScope = extendScope(localScope, negationExpr.getImplicitVariables()); |
616 | var argumentList = toArgumentList(atom.getArguments(), negatedScope, literals); | 677 | var argumentList = toArgumentList(atom.getArguments(), negatedScope, literals); |
617 | literals.add(constraint.call(CallPolarity.NEGATIVE, argumentList)); | 678 | literals.add(constraint.call(CallPolarity.NEGATIVE, argumentList)); |
618 | } else if (expr instanceof ComparisonExpr comparisonExpr) { | 679 | } |
680 | case ComparisonExpr comparisonExpr -> { | ||
619 | var argumentList = toArgumentList(List.of(comparisonExpr.getLeft(), comparisonExpr.getRight()), | 681 | var argumentList = toArgumentList(List.of(comparisonExpr.getLeft(), comparisonExpr.getRight()), |
620 | localScope, literals); | 682 | localScope, literals); |
621 | boolean positive = switch (comparisonExpr.getOp()) { | 683 | boolean positive = switch (comparisonExpr.getOp()) { |
@@ -625,8 +687,8 @@ public class ModelInitializer { | |||
625 | comparisonExpr, "Unsupported operator"); | 687 | comparisonExpr, "Unsupported operator"); |
626 | }; | 688 | }; |
627 | literals.add(new EquivalenceLiteral(positive, argumentList.get(0), argumentList.get(1))); | 689 | literals.add(new EquivalenceLiteral(positive, argumentList.get(0), argumentList.get(1))); |
628 | } else { | 690 | } |
629 | throw new TracedException(expr, "Unsupported literal"); | 691 | default -> throw new TracedException(expr, "Unsupported literal"); |
630 | } | 692 | } |
631 | } | 693 | } |
632 | 694 | ||
@@ -641,7 +703,7 @@ public class ModelInitializer { | |||
641 | var variableOrNode = variableOrNodeExpr.getVariableOrNode(); | 703 | var variableOrNode = variableOrNodeExpr.getVariableOrNode(); |
642 | if (variableOrNode instanceof Node node) { | 704 | if (variableOrNode instanceof Node node) { |
643 | int nodeId = getNodeId(node); | 705 | int nodeId = getNodeId(node); |
644 | var tempVariable = Variable.of(semanticsUtils.getName(node).orElse("_" + nodeId)); | 706 | var tempVariable = Variable.of(semanticsUtils.getNameWithoutRootPrefix(node).orElse("_" + nodeId)); |
645 | literals.add(new ConstantLiteral(tempVariable, nodeId)); | 707 | literals.add(new ConstantLiteral(tempVariable, nodeId)); |
646 | argumentList.add(tempVariable); | 708 | argumentList.add(tempVariable); |
647 | } else if (variableOrNode instanceof tools.refinery.language.model.problem.Variable problemVariable) { | 709 | } else if (variableOrNode instanceof tools.refinery.language.model.problem.Variable problemVariable) { |
@@ -662,13 +724,15 @@ public class ModelInitializer { | |||
662 | } | 724 | } |
663 | 725 | ||
664 | private void collectScopes() { | 726 | private void collectScopes() { |
665 | for (var statement : problem.getStatements()) { | 727 | for (var importedProblem : importedProblems) { |
666 | if (statement instanceof ScopeDeclaration scopeDeclaration) { | 728 | for (var statement : importedProblem.getStatements()) { |
667 | for (var typeScope : scopeDeclaration.getTypeScopes()) { | 729 | if (statement instanceof ScopeDeclaration scopeDeclaration) { |
668 | if (typeScope.isIncrement()) { | 730 | for (var typeScope : scopeDeclaration.getTypeScopes()) { |
669 | collectTypeScopeIncrement(typeScope); | 731 | if (typeScope.isIncrement()) { |
670 | } else { | 732 | collectTypeScopeIncrement(typeScope); |
671 | collectTypeScope(typeScope); | 733 | } else { |
734 | collectTypeScope(typeScope); | ||
735 | } | ||
672 | } | 736 | } |
673 | } | 737 | } |
674 | } | 738 | } |
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ProblemTraceImpl.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ProblemTraceImpl.java index f686e980..aef0fd89 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ProblemTraceImpl.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ProblemTraceImpl.java | |||
@@ -79,7 +79,7 @@ class ProblemTraceImpl implements ProblemTrace { | |||
79 | try { | 79 | try { |
80 | return nodeTrace.getOrThrow(node); | 80 | return nodeTrace.getOrThrow(node); |
81 | } catch (IllegalStateException e) { | 81 | } catch (IllegalStateException e) { |
82 | var qualifiedName = semanticsUtils.getName(node); | 82 | var qualifiedName = semanticsUtils.getNameWithoutRootPrefix(node); |
83 | throw new TracedException(node, "No node ID for " + qualifiedName, e); | 83 | throw new TracedException(node, "No node ID for " + qualifiedName, e); |
84 | } | 84 | } |
85 | } | 85 | } |
@@ -144,7 +144,7 @@ class ProblemTraceImpl implements ProblemTrace { | |||
144 | public PartialRelation getPartialRelation(Relation relation) { | 144 | public PartialRelation getPartialRelation(Relation relation) { |
145 | var partialRelation = mutableRelationTrace.get(relation); | 145 | var partialRelation = mutableRelationTrace.get(relation); |
146 | if (partialRelation == null) { | 146 | if (partialRelation == null) { |
147 | var qualifiedName = semanticsUtils.getName(relation); | 147 | var qualifiedName = semanticsUtils.getNameWithoutRootPrefix(relation); |
148 | throw new TracedException(relation, "No partial relation for " + qualifiedName); | 148 | throw new TracedException(relation, "No partial relation for " + qualifiedName); |
149 | } | 149 | } |
150 | return partialRelation; | 150 | return partialRelation; |
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java index b72ba697..9c40e6df 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.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 | */ |
@@ -7,15 +7,20 @@ package tools.refinery.language.semantics; | |||
7 | 7 | ||
8 | import com.google.inject.Inject; | 8 | import com.google.inject.Inject; |
9 | import com.google.inject.Singleton; | 9 | import com.google.inject.Singleton; |
10 | import com.google.inject.name.Named; | ||
11 | import org.eclipse.emf.ecore.EClass; | ||
10 | import org.eclipse.emf.ecore.EObject; | 12 | import org.eclipse.emf.ecore.EObject; |
11 | import org.eclipse.emf.ecore.util.EcoreUtil; | 13 | import org.eclipse.emf.ecore.util.EcoreUtil; |
12 | import org.eclipse.xtext.naming.IQualifiedNameConverter; | 14 | import org.eclipse.xtext.naming.IQualifiedNameConverter; |
13 | import org.eclipse.xtext.naming.IQualifiedNameProvider; | 15 | import org.eclipse.xtext.naming.IQualifiedNameProvider; |
14 | import org.eclipse.xtext.naming.QualifiedName; | 16 | import org.eclipse.xtext.naming.QualifiedName; |
17 | import org.eclipse.xtext.resource.IEObjectDescription; | ||
18 | import org.eclipse.xtext.resource.IResourceDescriptionsProvider; | ||
15 | import org.eclipse.xtext.scoping.IScope; | 19 | import org.eclipse.xtext.scoping.IScope; |
16 | import org.jetbrains.annotations.NotNull; | 20 | import org.jetbrains.annotations.NotNull; |
17 | import org.jetbrains.annotations.Nullable; | 21 | import org.jetbrains.annotations.Nullable; |
18 | import tools.refinery.language.model.problem.Problem; | 22 | import tools.refinery.language.model.problem.Problem; |
23 | import tools.refinery.language.naming.ProblemQualifiedNameProvider; | ||
19 | 24 | ||
20 | import java.util.Optional; | 25 | import java.util.Optional; |
21 | 26 | ||
@@ -25,10 +30,17 @@ public class SemanticsUtils { | |||
25 | private IQualifiedNameProvider qualifiedNameProvider; | 30 | private IQualifiedNameProvider qualifiedNameProvider; |
26 | 31 | ||
27 | @Inject | 32 | @Inject |
33 | @Named(ProblemQualifiedNameProvider.NAMED_DELEGATE) | ||
34 | private IQualifiedNameProvider delegateQualifiedNameProvider; | ||
35 | |||
36 | @Inject | ||
28 | private IQualifiedNameConverter qualifiedNameConverter; | 37 | private IQualifiedNameConverter qualifiedNameConverter; |
29 | 38 | ||
30 | public Optional<String> getName(EObject eObject) { | 39 | @Inject |
31 | var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(eObject); | 40 | private IResourceDescriptionsProvider resourceDescriptionsProvider; |
41 | |||
42 | public Optional<String> getNameWithoutRootPrefix(EObject eObject) { | ||
43 | var qualifiedName = delegateQualifiedNameProvider.getFullyQualifiedName(eObject); | ||
32 | if (qualifiedName == null) { | 44 | if (qualifiedName == null) { |
33 | return Optional.empty(); | 45 | return Optional.empty(); |
34 | } | 46 | } |
@@ -36,11 +48,31 @@ public class SemanticsUtils { | |||
36 | } | 48 | } |
37 | 49 | ||
38 | @Nullable | 50 | @Nullable |
51 | public <T> T maybeGetLocalElement(Problem problem, QualifiedName qualifiedName, Class<T> type, EClass eClass) { | ||
52 | var resource = problem.eResource(); | ||
53 | var resourceSet = resource.getResourceSet(); | ||
54 | var resourceDescriptions = resourceDescriptionsProvider.getResourceDescriptions(resourceSet); | ||
55 | var resourceDescription = resourceDescriptions.getResourceDescription(resource.getURI()); | ||
56 | if (resourceDescription == null) { | ||
57 | return null; | ||
58 | } | ||
59 | var eObjectDescriptions = resourceDescription.getExportedObjects(eClass, qualifiedName, false); | ||
60 | return maybeGet(problem, eObjectDescriptions, qualifiedName, type); | ||
61 | } | ||
62 | |||
63 | @Nullable | ||
39 | public <T> T maybeGetElement(Problem problem, IScope scope, QualifiedName qualifiedName, Class<T> type) { | 64 | public <T> T maybeGetElement(Problem problem, IScope scope, QualifiedName qualifiedName, Class<T> type) { |
40 | if (qualifiedName == null) { | 65 | if (qualifiedName == null) { |
41 | throw new IllegalArgumentException("Element name must not be null"); | 66 | throw new IllegalArgumentException("Element name must not be null"); |
42 | } | 67 | } |
43 | var iterator = scope.getElements(qualifiedName).iterator(); | 68 | var eObjectDescriptions = scope.getElements(qualifiedName); |
69 | return maybeGet(problem, eObjectDescriptions, qualifiedName, type); | ||
70 | } | ||
71 | |||
72 | @Nullable | ||
73 | private <T> T maybeGet(Problem problem, Iterable<IEObjectDescription> eObjectDescriptions, | ||
74 | QualifiedName qualifiedName, Class<T> type) { | ||
75 | var iterator = eObjectDescriptions.iterator(); | ||
44 | if (!iterator.hasNext()) { | 76 | if (!iterator.hasNext()) { |
45 | return null; | 77 | return null; |
46 | } | 78 | } |
@@ -60,8 +92,19 @@ public class SemanticsUtils { | |||
60 | } | 92 | } |
61 | 93 | ||
62 | @NotNull | 94 | @NotNull |
95 | public <T> T getLocalElement(Problem problem, QualifiedName qualifiedName, Class<T> type, EClass eClass) { | ||
96 | var element = maybeGetLocalElement(problem, qualifiedName, type, eClass); | ||
97 | return getOrThrow(element, qualifiedName, type); | ||
98 | } | ||
99 | |||
100 | @NotNull | ||
63 | public <T> T getElement(Problem problem, IScope scope, QualifiedName qualifiedName, Class<T> type) { | 101 | public <T> T getElement(Problem problem, IScope scope, QualifiedName qualifiedName, Class<T> type) { |
64 | var element = maybeGetElement(problem, scope, qualifiedName, type); | 102 | var element = maybeGetElement(problem, scope, qualifiedName, type); |
103 | return getOrThrow(element, qualifiedName, type); | ||
104 | } | ||
105 | |||
106 | @NotNull | ||
107 | private <T> T getOrThrow(@Nullable T element, QualifiedName qualifiedName, Class<T> type) { | ||
65 | if (element == null) { | 108 | if (element == null) { |
66 | var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName); | 109 | var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName); |
67 | throw new IllegalArgumentException("No such %s: %s" | 110 | throw new IllegalArgumentException("No such %s: %s" |
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 09ba34fc..377a66f3 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 | |||
@@ -10,15 +10,17 @@ 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.map.primitive.MutableIntObjectMap; | 11 | import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; |
12 | import org.eclipse.emf.common.util.URI; | 12 | import org.eclipse.emf.common.util.URI; |
13 | import org.eclipse.emf.ecore.EObject; | ||
14 | import org.eclipse.emf.ecore.resource.Resource; | ||
13 | import org.eclipse.emf.ecore.util.EcoreUtil; | 15 | import org.eclipse.emf.ecore.util.EcoreUtil; |
14 | import org.eclipse.xtext.naming.IQualifiedNameProvider; | 16 | import org.eclipse.xtext.naming.IQualifiedNameProvider; |
15 | import org.eclipse.xtext.naming.QualifiedName; | 17 | import org.eclipse.xtext.naming.QualifiedName; |
16 | import org.eclipse.xtext.resource.FileExtensionProvider; | ||
17 | import org.eclipse.xtext.resource.IResourceFactory; | 18 | import org.eclipse.xtext.resource.IResourceFactory; |
18 | import org.eclipse.xtext.resource.XtextResource; | 19 | import org.eclipse.xtext.resource.XtextResource; |
19 | import org.eclipse.xtext.resource.XtextResourceSet; | 20 | import org.eclipse.xtext.resource.XtextResourceSet; |
20 | import org.eclipse.xtext.scoping.IScopeProvider; | 21 | import org.eclipse.xtext.scoping.IScopeProvider; |
21 | import tools.refinery.language.model.problem.*; | 22 | import tools.refinery.language.model.problem.*; |
23 | import tools.refinery.language.naming.NamingUtil; | ||
22 | import tools.refinery.language.utils.ProblemDesugarer; | 24 | import tools.refinery.language.utils.ProblemDesugarer; |
23 | import tools.refinery.language.utils.ProblemUtil; | 25 | import tools.refinery.language.utils.ProblemUtil; |
24 | import tools.refinery.store.model.Model; | 26 | import tools.refinery.store.model.Model; |
@@ -34,15 +36,11 @@ import tools.refinery.store.tuple.Tuple; | |||
34 | import java.io.ByteArrayInputStream; | 36 | import java.io.ByteArrayInputStream; |
35 | import java.io.ByteArrayOutputStream; | 37 | import java.io.ByteArrayOutputStream; |
36 | import java.io.IOException; | 38 | import java.io.IOException; |
37 | import java.util.Map; | 39 | import java.util.*; |
38 | import java.util.TreeMap; | ||
39 | import java.util.TreeSet; | ||
40 | import java.util.function.Function; | 40 | import java.util.function.Function; |
41 | import java.util.stream.Collectors; | 41 | import java.util.stream.Collectors; |
42 | 42 | ||
43 | public class SolutionSerializer { | 43 | public class SolutionSerializer { |
44 | private String fileExtension; | ||
45 | |||
46 | @Inject | 44 | @Inject |
47 | private Provider<XtextResourceSet> resourceSetProvider; | 45 | private Provider<XtextResourceSet> resourceSetProvider; |
48 | 46 | ||
@@ -68,16 +66,17 @@ public class SolutionSerializer { | |||
68 | private Model model; | 66 | private Model model; |
69 | private ReasoningAdapter reasoningAdapter; | 67 | private ReasoningAdapter reasoningAdapter; |
70 | private PartialInterpretation<TruthValue, Boolean> existsInterpretation; | 68 | private PartialInterpretation<TruthValue, Boolean> existsInterpretation; |
69 | private Resource originalResource; | ||
70 | private Problem originalProblem; | ||
71 | private QualifiedName originalProblemName; | ||
71 | private Problem problem; | 72 | private Problem problem; |
73 | private QualifiedName newProblemName; | ||
74 | private NodeDeclaration nodeDeclaration; | ||
72 | private final MutableIntObjectMap<Node> nodes = IntObjectMaps.mutable.empty(); | 75 | private final MutableIntObjectMap<Node> nodes = IntObjectMaps.mutable.empty(); |
73 | 76 | ||
74 | @Inject | ||
75 | public void setFileExtensionProvider(FileExtensionProvider fileExtensionProvider) { | ||
76 | this.fileExtension = fileExtensionProvider.getPrimaryFileExtension(); | ||
77 | } | ||
78 | |||
79 | public Problem serializeSolution(ProblemTrace trace, Model model) { | 77 | public Problem serializeSolution(ProblemTrace trace, Model model) { |
80 | var uri = URI.createFileURI("__synthetic" + fileExtension); | 78 | var uri = URI.createURI("__solution_%s.%s".formatted(UUID.randomUUID().toString().replace('-', '_'), |
79 | ProblemUtil.MODULE_EXTENSION)); | ||
81 | return serializeSolution(trace, model, uri); | 80 | return serializeSolution(trace, model, uri); |
82 | } | 81 | } |
83 | 82 | ||
@@ -87,14 +86,26 @@ public class SolutionSerializer { | |||
87 | reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | 86 | reasoningAdapter = model.getAdapter(ReasoningAdapter.class); |
88 | existsInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, | 87 | existsInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, |
89 | ReasoningAdapter.EXISTS_SYMBOL); | 88 | ReasoningAdapter.EXISTS_SYMBOL); |
90 | var originalProblem = trace.getProblem(); | 89 | originalProblem = trace.getProblem(); |
90 | originalProblemName = qualifiedNameProvider.getFullyQualifiedName(originalProblem); | ||
91 | problem = copyProblem(originalProblem, uri); | 91 | problem = copyProblem(originalProblem, uri); |
92 | problem.setKind(ProblemUtil.getDefaultModuleKind(uri)); | ||
93 | problem.setExplicitKind(false); | ||
94 | problem.setName(null); | ||
95 | newProblemName = qualifiedNameProvider.getFullyQualifiedName(originalProblem); | ||
92 | problem.getStatements().removeIf(SolutionSerializer::shouldRemoveStatement); | 96 | problem.getStatements().removeIf(SolutionSerializer::shouldRemoveStatement); |
93 | problem.getNodes().removeIf(this::shouldRemoveNode); | 97 | removeNonExistentImplicitNodes(); |
98 | nodeDeclaration = ProblemFactory.eINSTANCE.createNodeDeclaration(); | ||
99 | nodeDeclaration.setKind(NodeKind.NODE); | ||
100 | nodeDeclaration.getNodes().addAll(problem.getNodes()); | ||
101 | problem.getStatements().add(nodeDeclaration); | ||
94 | nameProvider.setProblem(problem); | 102 | nameProvider.setProblem(problem); |
95 | addExistsAssertions(); | 103 | addExistsAssertions(); |
96 | addClassAssertions(); | 104 | addClassAssertions(); |
97 | addReferenceAssertions(); | 105 | addReferenceAssertions(); |
106 | if (nodeDeclaration.getNodes().isEmpty()) { | ||
107 | problem.getStatements().remove(nodeDeclaration); | ||
108 | } | ||
98 | return problem; | 109 | return problem; |
99 | } | 110 | } |
100 | 111 | ||
@@ -102,15 +113,28 @@ public class SolutionSerializer { | |||
102 | return statement instanceof Assertion || statement instanceof ScopeDeclaration; | 113 | return statement instanceof Assertion || statement instanceof ScopeDeclaration; |
103 | } | 114 | } |
104 | 115 | ||
105 | private boolean shouldRemoveNode(Node newNode) { | 116 | private void removeNonExistentImplicitNodes() { |
106 | var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(newNode); | 117 | var originalImplicitNodes = originalProblem.getNodes(); |
107 | var scope = scopeProvider.getScope(trace.getProblem(), ProblemPackage.Literals.ASSERTION__RELATION); | 118 | var newImplicitNodes = problem.getNodes(); |
108 | var originalNode = semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class); | 119 | if (newImplicitNodes.size() != originalImplicitNodes.size()) { |
109 | if (originalNode == null) { | 120 | throw new IllegalStateException("Expected %d implicit nodes in problem, but got %d after copying" |
110 | return false; | 121 | .formatted(originalImplicitNodes.size(), newImplicitNodes.size())); |
122 | } | ||
123 | var iterator = newImplicitNodes.iterator(); | ||
124 | for (var originalNode : originalImplicitNodes) { | ||
125 | if (!iterator.hasNext()) { | ||
126 | throw new AssertionError("Unexpected end of copied implicit node list"); | ||
127 | } | ||
128 | var newNode = iterator.next(); | ||
129 | if (!Objects.equals(originalNode.getName(), newNode.getName())) { | ||
130 | throw new IllegalStateException("Expected copy of '%s' to have the same name, got '%s' instead" | ||
131 | .formatted(originalNode.getName(), newNode.getName())); | ||
132 | } | ||
133 | int nodeId = trace.getNodeId(originalNode); | ||
134 | if (!isExistingNode(nodeId)) { | ||
135 | iterator.remove(); | ||
136 | } | ||
111 | } | 137 | } |
112 | int nodeId = trace.getNodeId(originalNode); | ||
113 | return !isExistingNode(nodeId); | ||
114 | } | 138 | } |
115 | 139 | ||
116 | private boolean isExistingNode(int nodeId) { | 140 | private boolean isExistingNode(int nodeId) { |
@@ -122,13 +146,10 @@ public class SolutionSerializer { | |||
122 | } | 146 | } |
123 | 147 | ||
124 | private Problem copyProblem(Problem originalProblem, URI uri) { | 148 | private Problem copyProblem(Problem originalProblem, URI uri) { |
125 | var newResourceSet = resourceSetProvider.get(); | 149 | originalResource = originalProblem.eResource(); |
126 | if (!fileExtension.equals(uri.fileExtension())) { | 150 | var resourceSet = originalResource.getResourceSet(); |
127 | uri = uri.appendFileExtension(fileExtension); | ||
128 | } | ||
129 | var newResource = resourceFactory.createResource(uri); | 151 | var newResource = resourceFactory.createResource(uri); |
130 | newResourceSet.getResources().add(newResource); | 152 | resourceSet.getResources().add(newResource); |
131 | var originalResource = originalProblem.eResource(); | ||
132 | if (originalResource instanceof XtextResource) { | 153 | if (originalResource instanceof XtextResource) { |
133 | byte[] bytes; | 154 | byte[] bytes; |
134 | try { | 155 | try { |
@@ -143,6 +164,7 @@ public class SolutionSerializer { | |||
143 | throw new IllegalStateException("Failed to copy problem", e); | 164 | throw new IllegalStateException("Failed to copy problem", e); |
144 | } | 165 | } |
145 | var contents = newResource.getContents(); | 166 | var contents = newResource.getContents(); |
167 | EcoreUtil.resolveAll(newResource); | ||
146 | if (!contents.isEmpty() && contents.getFirst() instanceof Problem newProblem) { | 168 | if (!contents.isEmpty() && contents.getFirst() instanceof Problem newProblem) { |
147 | return newProblem; | 169 | return newProblem; |
148 | } | 170 | } |
@@ -154,10 +176,24 @@ public class SolutionSerializer { | |||
154 | } | 176 | } |
155 | } | 177 | } |
156 | 178 | ||
179 | private QualifiedName getConvertedName(EObject original) { | ||
180 | var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(original); | ||
181 | if (originalProblemName != null && qualifiedName.startsWith(originalProblemName)) { | ||
182 | qualifiedName = qualifiedName.skipFirst(originalProblemName.getSegmentCount()); | ||
183 | } | ||
184 | if (newProblemName != null) { | ||
185 | qualifiedName = newProblemName.append(qualifiedName); | ||
186 | } | ||
187 | return NamingUtil.addRootPrefix(qualifiedName); | ||
188 | } | ||
189 | |||
157 | private Relation findRelation(Relation originalRelation) { | 190 | private Relation findRelation(Relation originalRelation) { |
158 | var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(originalRelation); | 191 | if (originalRelation.eResource() != originalResource) { |
159 | var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.ASSERTION__RELATION); | 192 | return originalRelation; |
160 | return semanticsUtils.getElement(problem, scope, qualifiedName, Relation.class); | 193 | } |
194 | var qualifiedName = getConvertedName(originalRelation); | ||
195 | return semanticsUtils.getLocalElement(problem, qualifiedName, Relation.class, | ||
196 | ProblemPackage.Literals.RELATION); | ||
161 | } | 197 | } |
162 | 198 | ||
163 | private Relation findPartialRelation(PartialRelation partialRelation) { | 199 | private Relation findPartialRelation(PartialRelation partialRelation) { |
@@ -165,13 +201,11 @@ public class SolutionSerializer { | |||
165 | } | 201 | } |
166 | 202 | ||
167 | private Node findNode(Node originalNode) { | 203 | private Node findNode(Node originalNode) { |
168 | var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(originalNode); | 204 | if (originalNode.eResource() != originalResource) { |
169 | return findNode(qualifiedName); | 205 | return originalNode; |
170 | } | 206 | } |
171 | 207 | var qualifiedName = getConvertedName(originalNode); | |
172 | private Node findNode(QualifiedName qualifiedName) { | 208 | return semanticsUtils.maybeGetLocalElement(problem, qualifiedName, Node.class, ProblemPackage.Literals.NODE); |
173 | var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE); | ||
174 | return semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class); | ||
175 | } | 209 | } |
176 | 210 | ||
177 | private void addAssertion(Relation relation, LogicValue value, Node... arguments) { | 211 | private void addAssertion(Relation relation, LogicValue value, Node... arguments) { |
@@ -189,17 +223,17 @@ public class SolutionSerializer { | |||
189 | } | 223 | } |
190 | 224 | ||
191 | private void addExistsAssertions() { | 225 | private void addExistsAssertions() { |
192 | var builtinSymbols = desugarer.getBuiltinSymbols(problem) | 226 | var builtinSymbols = desugarer.getBuiltinSymbols(problem).orElseThrow(() -> new IllegalStateException("No " + |
193 | .orElseThrow(() -> new IllegalStateException("No builtin library in copied problem")); | 227 | "builtin library in copied problem")); |
194 | // Make sure to output exists assertions in a deterministic order. | 228 | // Make sure to output exists assertions in a deterministic order. |
195 | var sortedNewNodes = new TreeMap<Integer, Node>(); | 229 | var sortedNewNodes = new TreeMap<Integer, Node>(); |
196 | for (var pair : trace.getNodeTrace().keyValuesView()) { | 230 | for (var pair : trace.getNodeTrace().keyValuesView()) { |
197 | var originalNode = pair.getOne(); | 231 | var originalNode = pair.getOne(); |
198 | int nodeId = pair.getTwo(); | 232 | int nodeId = pair.getTwo(); |
199 | var newNode = findNode(originalNode); | 233 | var newNode = findNode(originalNode); |
200 | // Since all implicit nodes that do not exist has already been remove in serializeSolution, | 234 | // Since all implicit nodes that do not exist has already been removed in serializeSolution, |
201 | // we only need to add !exists assertions to ::new nodes (nodes marked as an individual must always exist). | 235 | // we only need to add !exists assertions to ::new nodes and explicitly declared nodes that do not exist. |
202 | if (ProblemUtil.isNewNode(originalNode)) { | 236 | if (ProblemUtil.isMultiNode(originalNode) || (ProblemUtil.isDeclaredNode(originalNode) && !isExistingNode(nodeId))) { |
203 | sortedNewNodes.put(nodeId, newNode); | 237 | sortedNewNodes.put(nodeId, newNode); |
204 | } else { | 238 | } else { |
205 | nodes.put(nodeId, newNode); | 239 | nodes.put(nodeId, newNode); |
@@ -212,8 +246,8 @@ public class SolutionSerializer { | |||
212 | } | 246 | } |
213 | 247 | ||
214 | private void addClassAssertions() { | 248 | private void addClassAssertions() { |
215 | var types = trace.getMetamodel().typeHierarchy().getPreservedTypes().keySet().stream() | 249 | var types = |
216 | .collect(Collectors.toMap(Function.identity(), this::findPartialRelation)); | 250 | trace.getMetamodel().typeHierarchy().getPreservedTypes().keySet().stream().collect(Collectors.toMap(Function.identity(), this::findPartialRelation)); |
217 | var cursor = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL).getAll(); | 251 | var cursor = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL).getAll(); |
218 | while (cursor.move()) { | 252 | while (cursor.move()) { |
219 | var key = cursor.getKey(); | 253 | var key = cursor.getKey(); |
@@ -237,7 +271,7 @@ public class SolutionSerializer { | |||
237 | var nodeName = nameProvider.getNextName(typeName); | 271 | var nodeName = nameProvider.getNextName(typeName); |
238 | node = ProblemFactory.eINSTANCE.createNode(); | 272 | node = ProblemFactory.eINSTANCE.createNode(); |
239 | node.setName(nodeName); | 273 | node.setName(nodeName); |
240 | problem.getNodes().add(node); | 274 | nodeDeclaration.getNodes().add(node); |
241 | nodes.put(nodeId, node); | 275 | nodes.put(nodeId, node); |
242 | } | 276 | } |
243 | addAssertion(candidateRelation, LogicValue.TRUE, node); | 277 | addAssertion(candidateRelation, LogicValue.TRUE, node); |