diff options
author | Kristóf Marussy <kristof@marussy.com> | 2024-02-03 01:39:11 +0100 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2024-02-03 03:38:59 +0100 |
commit | d5654f1ae03bec95c08e69a19a116c9825a27098 (patch) | |
tree | a12b59bbf54352cc51d1ae9bafef0eb10b8d28b4 /subprojects/language-semantics | |
parent | refactor(language): name disambiguation (diff) | |
download | refinery-d5654f1ae03bec95c08e69a19a116c9825a27098.tar.gz refinery-d5654f1ae03bec95c08e69a19a116c9825a27098.tar.zst refinery-d5654f1ae03bec95c08e69a19a116c9825a27098.zip |
feat(language): import resolution
Diffstat (limited to 'subprojects/language-semantics')
-rw-r--r-- | subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java | 230 |
1 files changed, 138 insertions, 92 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 7c649232..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 NodeDeclaration nodeDeclaration) { | 204 | for (var statement : importedProblem.getStatements()) { |
173 | for (var node : nodeDeclaration.getNodes()) { | 205 | if (statement instanceof NodeDeclaration nodeDeclaration) { |
174 | collectNode(node); | 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 | } |
@@ -251,11 +287,13 @@ public class ModelInitializer { | |||
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,15 +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 NodeDeclaration nodeDeclaration) { | 396 | collectEnumAssertions(enumDeclaration); |
359 | collectNodeDeclarationAssertions(nodeDeclaration); | 397 | } else if (statement instanceof NodeDeclaration nodeDeclaration) { |
360 | } else if (statement instanceof Assertion assertion) { | 398 | collectNodeDeclarationAssertions(nodeDeclaration); |
361 | collectAssertion(assertion); | 399 | } else if (statement instanceof Assertion assertion) { |
400 | collectAssertion(assertion); | ||
401 | } | ||
362 | } | 402 | } |
363 | } | 403 | } |
364 | } | 404 | } |
@@ -429,9 +469,11 @@ public class ModelInitializer { | |||
429 | } | 469 | } |
430 | 470 | ||
431 | private void fixClassDeclarationAssertions() { | 471 | private void fixClassDeclarationAssertions() { |
432 | for (var statement : problem.getStatements()) { | 472 | for (var importedProblem : importedProblems) { |
433 | if (statement instanceof ClassDeclaration classDeclaration) { | 473 | for (var statement : importedProblem.getStatements()) { |
434 | fixClassDeclarationAssertions(classDeclaration); | 474 | if (statement instanceof ClassDeclaration classDeclaration) { |
475 | fixClassDeclarationAssertions(classDeclaration); | ||
476 | } | ||
435 | } | 477 | } |
436 | } | 478 | } |
437 | } | 479 | } |
@@ -499,9 +541,11 @@ public class ModelInitializer { | |||
499 | } | 541 | } |
500 | 542 | ||
501 | private void collectPredicates(ModelStoreBuilder storeBuilder) { | 543 | private void collectPredicates(ModelStoreBuilder storeBuilder) { |
502 | for (var statement : problem.getStatements()) { | 544 | for (var importedProblem : importedProblems) { |
503 | if (statement instanceof PredicateDefinition predicateDefinition) { | 545 | for (var statement : importedProblem.getStatements()) { |
504 | collectPredicateDefinitionTraced(predicateDefinition, storeBuilder); | 546 | if (statement instanceof PredicateDefinition predicateDefinition) { |
547 | collectPredicateDefinitionTraced(predicateDefinition, storeBuilder); | ||
548 | } | ||
505 | } | 549 | } |
506 | } | 550 | } |
507 | } | 551 | } |
@@ -601,51 +645,51 @@ public class ModelInitializer { | |||
601 | 645 | ||
602 | 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, |
603 | List<Literal> literals) { | 647 | List<Literal> literals) { |
604 | switch (expr) { | 648 | switch (expr) { |
605 | case LogicConstant logicConstant -> { | 649 | case LogicConstant logicConstant -> { |
606 | switch (logicConstant.getLogicValue()) { | 650 | switch (logicConstant.getLogicValue()) { |
607 | case TRUE -> literals.add(BooleanLiteral.TRUE); | 651 | case TRUE -> literals.add(BooleanLiteral.TRUE); |
608 | case FALSE -> literals.add(BooleanLiteral.FALSE); | 652 | case FALSE -> literals.add(BooleanLiteral.FALSE); |
609 | default -> throw new TracedException(logicConstant, "Unsupported literal"); | 653 | default -> throw new TracedException(logicConstant, "Unsupported literal"); |
610 | } | 654 | } |
611 | } | 655 | } |
612 | case Atom atom -> { | 656 | case Atom atom -> { |
613 | var target = getPartialRelation(atom.getRelation()); | 657 | var target = getPartialRelation(atom.getRelation()); |
614 | var polarity = atom.isTransitiveClosure() ? CallPolarity.TRANSITIVE : CallPolarity.POSITIVE; | 658 | var polarity = atom.isTransitiveClosure() ? CallPolarity.TRANSITIVE : CallPolarity.POSITIVE; |
615 | var argumentList = toArgumentList(atom.getArguments(), localScope, literals); | 659 | var argumentList = toArgumentList(atom.getArguments(), localScope, literals); |
616 | literals.add(target.call(polarity, argumentList)); | 660 | literals.add(target.call(polarity, argumentList)); |
617 | } | 661 | } |
618 | case NegationExpr negationExpr -> { | 662 | case NegationExpr negationExpr -> { |
619 | var body = negationExpr.getBody(); | 663 | var body = negationExpr.getBody(); |
620 | if (!(body instanceof Atom atom)) { | 664 | if (!(body instanceof Atom atom)) { |
621 | throw new TracedException(body, "Cannot negate literal"); | 665 | throw new TracedException(body, "Cannot negate literal"); |
622 | } | 666 | } |
623 | var target = getPartialRelation(atom.getRelation()); | 667 | var target = getPartialRelation(atom.getRelation()); |
624 | Constraint constraint; | 668 | Constraint constraint; |
625 | if (atom.isTransitiveClosure()) { | 669 | if (atom.isTransitiveClosure()) { |
626 | constraint = Query.of(target.name() + "#transitive", (builder, p1, p2) -> builder.clause( | 670 | constraint = Query.of(target.name() + "#transitive", (builder, p1, p2) -> builder.clause( |
627 | target.callTransitive(p1, p2) | 671 | target.callTransitive(p1, p2) |
628 | )).getDnf(); | 672 | )).getDnf(); |
629 | } else { | 673 | } else { |
630 | constraint = target; | 674 | constraint = target; |
631 | } | 675 | } |
632 | var negatedScope = extendScope(localScope, negationExpr.getImplicitVariables()); | 676 | var negatedScope = extendScope(localScope, negationExpr.getImplicitVariables()); |
633 | var argumentList = toArgumentList(atom.getArguments(), negatedScope, literals); | 677 | var argumentList = toArgumentList(atom.getArguments(), negatedScope, literals); |
634 | literals.add(constraint.call(CallPolarity.NEGATIVE, argumentList)); | 678 | literals.add(constraint.call(CallPolarity.NEGATIVE, argumentList)); |
635 | } | 679 | } |
636 | case ComparisonExpr comparisonExpr -> { | 680 | case ComparisonExpr comparisonExpr -> { |
637 | var argumentList = toArgumentList(List.of(comparisonExpr.getLeft(), comparisonExpr.getRight()), | 681 | var argumentList = toArgumentList(List.of(comparisonExpr.getLeft(), comparisonExpr.getRight()), |
638 | localScope, literals); | 682 | localScope, literals); |
639 | boolean positive = switch (comparisonExpr.getOp()) { | 683 | boolean positive = switch (comparisonExpr.getOp()) { |
640 | case EQ -> true; | 684 | case EQ -> true; |
641 | case NOT_EQ -> false; | 685 | case NOT_EQ -> false; |
642 | default -> throw new TracedException( | 686 | default -> throw new TracedException( |
643 | comparisonExpr, "Unsupported operator"); | 687 | comparisonExpr, "Unsupported operator"); |
644 | }; | 688 | }; |
645 | literals.add(new EquivalenceLiteral(positive, argumentList.get(0), argumentList.get(1))); | 689 | literals.add(new EquivalenceLiteral(positive, argumentList.get(0), argumentList.get(1))); |
646 | } | 690 | } |
647 | default -> throw new TracedException(expr, "Unsupported literal"); | 691 | default -> throw new TracedException(expr, "Unsupported literal"); |
648 | } | 692 | } |
649 | } | 693 | } |
650 | 694 | ||
651 | private List<Variable> toArgumentList( | 695 | private List<Variable> toArgumentList( |
@@ -680,13 +724,15 @@ public class ModelInitializer { | |||
680 | } | 724 | } |
681 | 725 | ||
682 | private void collectScopes() { | 726 | private void collectScopes() { |
683 | for (var statement : problem.getStatements()) { | 727 | for (var importedProblem : importedProblems) { |
684 | if (statement instanceof ScopeDeclaration scopeDeclaration) { | 728 | for (var statement : importedProblem.getStatements()) { |
685 | for (var typeScope : scopeDeclaration.getTypeScopes()) { | 729 | if (statement instanceof ScopeDeclaration scopeDeclaration) { |
686 | if (typeScope.isIncrement()) { | 730 | for (var typeScope : scopeDeclaration.getTypeScopes()) { |
687 | collectTypeScopeIncrement(typeScope); | 731 | if (typeScope.isIncrement()) { |
688 | } else { | 732 | collectTypeScopeIncrement(typeScope); |
689 | collectTypeScope(typeScope); | 733 | } else { |
734 | collectTypeScope(typeScope); | ||
735 | } | ||
690 | } | 736 | } |
691 | } | 737 | } |
692 | } | 738 | } |