diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-08-20 19:41:32 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-08-20 20:29:02 +0200 |
commit | a3f1e6872f4f768d14899a1e70bbdc14f32e478d (patch) | |
tree | b2daf0c81724f31ee190f5d63eb42988086dabf2 /subprojects/language-semantics/src | |
parent | fix: nullary model initialization (diff) | |
download | refinery-a3f1e6872f4f768d14899a1e70bbdc14f32e478d.tar.gz refinery-a3f1e6872f4f768d14899a1e70bbdc14f32e478d.tar.zst refinery-a3f1e6872f4f768d14899a1e70bbdc14f32e478d.zip |
feat: improve semantics error reporting
Also makes model seeds cancellable to reduce server load during semantic
analysis.
Diffstat (limited to 'subprojects/language-semantics/src')
2 files changed, 139 insertions, 33 deletions
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java index 5f854ac3..5ed65e04 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java | |||
@@ -15,12 +15,14 @@ import tools.refinery.language.utils.ProblemDesugarer; | |||
15 | import tools.refinery.language.utils.ProblemUtil; | 15 | import tools.refinery.language.utils.ProblemUtil; |
16 | import tools.refinery.store.model.ModelStoreBuilder; | 16 | import tools.refinery.store.model.ModelStoreBuilder; |
17 | import tools.refinery.store.query.Constraint; | 17 | import tools.refinery.store.query.Constraint; |
18 | import tools.refinery.store.query.dnf.InvalidClauseException; | ||
18 | import tools.refinery.store.query.dnf.Query; | 19 | import tools.refinery.store.query.dnf.Query; |
19 | import tools.refinery.store.query.dnf.RelationalQuery; | 20 | import tools.refinery.store.query.dnf.RelationalQuery; |
20 | import tools.refinery.store.query.literal.*; | 21 | import tools.refinery.store.query.literal.*; |
21 | import tools.refinery.store.query.term.NodeVariable; | 22 | import tools.refinery.store.query.term.NodeVariable; |
22 | import tools.refinery.store.query.term.Variable; | 23 | import tools.refinery.store.query.term.Variable; |
23 | import tools.refinery.store.reasoning.ReasoningAdapter; | 24 | import tools.refinery.store.reasoning.ReasoningAdapter; |
25 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
24 | import tools.refinery.store.reasoning.representation.PartialRelation; | 26 | import tools.refinery.store.reasoning.representation.PartialRelation; |
25 | import tools.refinery.store.reasoning.seed.ModelSeed; | 27 | import tools.refinery.store.reasoning.seed.ModelSeed; |
26 | import tools.refinery.store.reasoning.seed.Seed; | 28 | import tools.refinery.store.reasoning.seed.Seed; |
@@ -60,7 +62,9 @@ public class ModelInitializer { | |||
60 | 62 | ||
61 | private final Map<Relation, RelationInfo> relationInfoMap = new LinkedHashMap<>(); | 63 | private final Map<Relation, RelationInfo> relationInfoMap = new LinkedHashMap<>(); |
62 | 64 | ||
63 | private final Map<PartialRelation, RelationInfo> partialRelationInfoMap = new LinkedHashMap<>(); | 65 | private final Map<PartialRelation, RelationInfo> partialRelationInfoMap = new HashMap<>(); |
66 | |||
67 | private Map<AnyPartialSymbol, Relation> inverseTrace = new HashMap<>(); | ||
64 | 68 | ||
65 | private Map<Relation, PartialRelation> relationTrace; | 69 | private Map<Relation, PartialRelation> relationTrace; |
66 | 70 | ||
@@ -82,6 +86,10 @@ public class ModelInitializer { | |||
82 | return relationTrace; | 86 | return relationTrace; |
83 | } | 87 | } |
84 | 88 | ||
89 | public Relation getInverseTrace(AnyPartialSymbol partialRelation) { | ||
90 | return inverseTrace.get(partialRelation); | ||
91 | } | ||
92 | |||
85 | public ModelSeed createModel(Problem problem, ModelStoreBuilder storeBuilder) { | 93 | public ModelSeed createModel(Problem problem, ModelStoreBuilder storeBuilder) { |
86 | this.problem = problem; | 94 | this.problem = problem; |
87 | this.storeBuilder = storeBuilder; | 95 | this.storeBuilder = storeBuilder; |
@@ -172,7 +180,7 @@ public class ModelInitializer { | |||
172 | collectPartialRelation(invalidMultiplicityConstraint, 1, TruthValue.FALSE, TruthValue.FALSE); | 180 | collectPartialRelation(invalidMultiplicityConstraint, 1, TruthValue.FALSE, TruthValue.FALSE); |
173 | } | 181 | } |
174 | } else { | 182 | } else { |
175 | throw new IllegalArgumentException("Unknown feature declaration: " + featureDeclaration); | 183 | throw new TracedException(featureDeclaration, "Unknown feature declaration"); |
176 | } | 184 | } |
177 | } | 185 | } |
178 | } | 186 | } |
@@ -189,6 +197,7 @@ public class ModelInitializer { | |||
189 | private void putRelationInfo(Relation relation, RelationInfo info) { | 197 | private void putRelationInfo(Relation relation, RelationInfo info) { |
190 | relationInfoMap.put(relation, info); | 198 | relationInfoMap.put(relation, info); |
191 | partialRelationInfoMap.put(info.partialRelation(), info); | 199 | partialRelationInfoMap.put(info.partialRelation(), info); |
200 | inverseTrace.put(info.partialRelation(), relation); | ||
192 | } | 201 | } |
193 | 202 | ||
194 | private RelationInfo collectPartialRelation(Relation relation, int arity, TruthValue value, | 203 | private RelationInfo collectPartialRelation(Relation relation, int arity, TruthValue value, |
@@ -197,6 +206,7 @@ public class ModelInitializer { | |||
197 | var name = getName(relation); | 206 | var name = getName(relation); |
198 | var info = new RelationInfo(name, arity, value, defaultValue); | 207 | var info = new RelationInfo(name, arity, value, defaultValue); |
199 | partialRelationInfoMap.put(info.partialRelation(), info); | 208 | partialRelationInfoMap.put(info.partialRelation(), info); |
209 | inverseTrace.put(info.partialRelation(), relation); | ||
200 | return info; | 210 | return info; |
201 | }); | 211 | }); |
202 | } | 212 | } |
@@ -216,7 +226,11 @@ public class ModelInitializer { | |||
216 | } | 226 | } |
217 | 227 | ||
218 | private void collectEnumMetamodel(EnumDeclaration enumDeclaration) { | 228 | private void collectEnumMetamodel(EnumDeclaration enumDeclaration) { |
219 | metamodelBuilder.type(getPartialRelation(enumDeclaration), nodeRelation); | 229 | try { |
230 | metamodelBuilder.type(getPartialRelation(enumDeclaration), nodeRelation); | ||
231 | } catch (RuntimeException e) { | ||
232 | throw TracedException.addTrace(enumDeclaration, e); | ||
233 | } | ||
220 | } | 234 | } |
221 | 235 | ||
222 | private void collectClassDeclarationMetamodel(ClassDeclaration classDeclaration) { | 236 | private void collectClassDeclarationMetamodel(ClassDeclaration classDeclaration) { |
@@ -226,13 +240,15 @@ public class ModelInitializer { | |||
226 | for (var superType : superTypes) { | 240 | for (var superType : superTypes) { |
227 | partialSuperTypes.add(getPartialRelation(superType)); | 241 | partialSuperTypes.add(getPartialRelation(superType)); |
228 | } | 242 | } |
229 | metamodelBuilder.type(getPartialRelation(classDeclaration), classDeclaration.isAbstract(), | 243 | try { |
230 | partialSuperTypes); | 244 | metamodelBuilder.type(getPartialRelation(classDeclaration), classDeclaration.isAbstract(), |
245 | partialSuperTypes); | ||
246 | } catch (RuntimeException e) { | ||
247 | throw TracedException.addTrace(classDeclaration, e); | ||
248 | } | ||
231 | for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) { | 249 | for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) { |
232 | if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) { | 250 | if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) { |
233 | collectReferenceDeclarationMetamodel(classDeclaration, referenceDeclaration); | 251 | collectReferenceDeclarationMetamodel(classDeclaration, referenceDeclaration); |
234 | } else { | ||
235 | throw new IllegalArgumentException("Unknown feature declaration: " + featureDeclaration); | ||
236 | } | 252 | } |
237 | } | 253 | } |
238 | } | 254 | } |
@@ -249,7 +265,11 @@ public class ModelInitializer { | |||
249 | oppositeRelation = getPartialRelation(opposite); | 265 | oppositeRelation = getPartialRelation(opposite); |
250 | } | 266 | } |
251 | var multiplicity = getMultiplicityConstraint(referenceDeclaration); | 267 | var multiplicity = getMultiplicityConstraint(referenceDeclaration); |
252 | metamodelBuilder.reference(relation, source, containment, multiplicity, target, oppositeRelation); | 268 | try { |
269 | metamodelBuilder.reference(relation, source, containment, multiplicity, target, oppositeRelation); | ||
270 | } catch (RuntimeException e) { | ||
271 | throw TracedException.addTrace(classDeclaration, e); | ||
272 | } | ||
253 | } | 273 | } |
254 | 274 | ||
255 | private Multiplicity getMultiplicityConstraint(ReferenceDeclaration referenceDeclaration) { | 275 | private Multiplicity getMultiplicityConstraint(ReferenceDeclaration referenceDeclaration) { |
@@ -267,7 +287,7 @@ public class ModelInitializer { | |||
267 | interval = CardinalityIntervals.between(rangeMultiplicity.getLowerBound(), | 287 | interval = CardinalityIntervals.between(rangeMultiplicity.getLowerBound(), |
268 | upperBound < 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.atMost(upperBound)); | 288 | upperBound < 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.atMost(upperBound)); |
269 | } else { | 289 | } else { |
270 | throw new IllegalArgumentException("Unknown multiplicity: " + problemMultiplicity); | 290 | throw new TracedException(problemMultiplicity, "Unknown multiplicity"); |
271 | } | 291 | } |
272 | var constraint = getRelationInfo(referenceDeclaration.getInvalidMultiplicity()).partialRelation(); | 292 | var constraint = getRelationInfo(referenceDeclaration.getInvalidMultiplicity()).partialRelation(); |
273 | return ConstrainedMultiplicity.of(interval, constraint); | 293 | return ConstrainedMultiplicity.of(interval, constraint); |
@@ -327,13 +347,19 @@ public class ModelInitializer { | |||
327 | } | 347 | } |
328 | 348 | ||
329 | private void collectAssertion(Assertion assertion) { | 349 | private void collectAssertion(Assertion assertion) { |
330 | var relation = assertion.getRelation(); | ||
331 | var tuple = getTuple(assertion); | 350 | var tuple = getTuple(assertion); |
332 | var value = getTruthValue(assertion.getValue()); | 351 | var value = getTruthValue(assertion.getValue()); |
352 | var relation = assertion.getRelation(); | ||
353 | var info = getRelationInfo(relation); | ||
354 | var partialRelation = info.partialRelation(); | ||
355 | if (partialRelation.arity() != tuple.getSize()) { | ||
356 | throw new TracedException(assertion, "Expected %d arguments for %s, got %d instead" | ||
357 | .formatted(partialRelation.arity(), partialRelation, tuple.getSize())); | ||
358 | } | ||
333 | if (assertion.isDefault()) { | 359 | if (assertion.isDefault()) { |
334 | mergeDefaultValue(relation, tuple, value); | 360 | info.defaultAssertions().mergeValue(tuple, value); |
335 | } else { | 361 | } else { |
336 | mergeValue(relation, tuple, value); | 362 | info.assertions().mergeValue(tuple, value); |
337 | } | 363 | } |
338 | } | 364 | } |
339 | 365 | ||
@@ -341,10 +367,6 @@ public class ModelInitializer { | |||
341 | getRelationInfo(relation).assertions().mergeValue(key, value); | 367 | getRelationInfo(relation).assertions().mergeValue(key, value); |
342 | } | 368 | } |
343 | 369 | ||
344 | private void mergeDefaultValue(Relation relation, Tuple key, TruthValue value) { | ||
345 | getRelationInfo(relation).defaultAssertions().mergeValue(key, value); | ||
346 | } | ||
347 | |||
348 | private RelationInfo getRelationInfo(Relation relation) { | 370 | private RelationInfo getRelationInfo(Relation relation) { |
349 | var info = relationInfoMap.get(relation); | 371 | var info = relationInfoMap.get(relation); |
350 | if (info == null) { | 372 | if (info == null) { |
@@ -372,7 +394,7 @@ public class ModelInitializer { | |||
372 | } else if (argument instanceof WildcardAssertionArgument) { | 394 | } else if (argument instanceof WildcardAssertionArgument) { |
373 | nodes[i] = -1; | 395 | nodes[i] = -1; |
374 | } else { | 396 | } else { |
375 | throw new IllegalArgumentException("Unknown assertion argument: " + argument); | 397 | throw new TracedException(argument, "Unsupported assertion argument"); |
376 | } | 398 | } |
377 | } | 399 | } |
378 | return Tuple.of(nodes); | 400 | return Tuple.of(nodes); |
@@ -393,8 +415,24 @@ public class ModelInitializer { | |||
393 | private void collectPredicates() { | 415 | private void collectPredicates() { |
394 | for (var statement : problem.getStatements()) { | 416 | for (var statement : problem.getStatements()) { |
395 | if (statement instanceof PredicateDefinition predicateDefinition) { | 417 | if (statement instanceof PredicateDefinition predicateDefinition) { |
396 | collectPredicateDefinition(predicateDefinition); | 418 | collectPredicateDefinitionTraced(predicateDefinition); |
419 | } | ||
420 | } | ||
421 | } | ||
422 | |||
423 | private void collectPredicateDefinitionTraced(PredicateDefinition predicateDefinition) { | ||
424 | try { | ||
425 | collectPredicateDefinition(predicateDefinition); | ||
426 | } catch (InvalidClauseException e) { | ||
427 | int clauseIndex = e.getClauseIndex(); | ||
428 | var bodies = predicateDefinition.getBodies(); | ||
429 | if (clauseIndex < bodies.size()) { | ||
430 | throw new TracedException(bodies.get(clauseIndex), e); | ||
431 | } else { | ||
432 | throw new TracedException(predicateDefinition, e); | ||
397 | } | 433 | } |
434 | } catch (RuntimeException e) { | ||
435 | throw TracedException.addTrace(predicateDefinition, e); | ||
398 | } | 436 | } |
399 | } | 437 | } |
400 | 438 | ||
@@ -436,13 +474,17 @@ public class ModelInitializer { | |||
436 | } | 474 | } |
437 | var builder = Query.builder(name).parameters(parameters); | 475 | var builder = Query.builder(name).parameters(parameters); |
438 | for (var body : predicateDefinition.getBodies()) { | 476 | for (var body : predicateDefinition.getBodies()) { |
439 | var localScope = extendScope(parameterMap, body.getImplicitVariables()); | 477 | try { |
440 | var problemLiterals = body.getLiterals(); | 478 | var localScope = extendScope(parameterMap, body.getImplicitVariables()); |
441 | var literals = new ArrayList<Literal>(commonLiterals); | 479 | var problemLiterals = body.getLiterals(); |
442 | for (var problemLiteral : problemLiterals) { | 480 | var literals = new ArrayList<>(commonLiterals); |
443 | toLiterals(problemLiteral, localScope, literals); | 481 | for (var problemLiteral : problemLiterals) { |
482 | toLiteralsTraced(problemLiteral, localScope, literals); | ||
483 | } | ||
484 | builder.clause(literals); | ||
485 | } catch (RuntimeException e) { | ||
486 | throw TracedException.addTrace(body, e); | ||
444 | } | 487 | } |
445 | builder.clause(literals); | ||
446 | } | 488 | } |
447 | return builder.build(); | 489 | return builder.build(); |
448 | } | 490 | } |
@@ -462,13 +504,23 @@ public class ModelInitializer { | |||
462 | return localScope; | 504 | return localScope; |
463 | } | 505 | } |
464 | 506 | ||
465 | private void toLiterals(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope, | 507 | private void toLiteralsTraced(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope, |
508 | List<Literal> literals) { | ||
509 | try { | ||
510 | toLiterals(expr, localScope, literals); | ||
511 | } catch (RuntimeException e) { | ||
512 | throw TracedException.addTrace(expr, e); | ||
513 | } | ||
514 | } | ||
515 | |||
516 | private void toLiterals(Expr expr, Map<tools.refinery.language.model.problem.Variable, | ||
517 | Variable> localScope, | ||
466 | List<Literal> literals) { | 518 | List<Literal> literals) { |
467 | if (expr instanceof LogicConstant logicConstant) { | 519 | if (expr instanceof LogicConstant logicConstant) { |
468 | switch (logicConstant.getLogicValue()) { | 520 | switch (logicConstant.getLogicValue()) { |
469 | case TRUE -> literals.add(BooleanLiteral.TRUE); | 521 | case TRUE -> literals.add(BooleanLiteral.TRUE); |
470 | case FALSE -> literals.add(BooleanLiteral.FALSE); | 522 | case FALSE -> literals.add(BooleanLiteral.FALSE); |
471 | default -> throw new IllegalArgumentException("Unsupported literal: " + expr); | 523 | default -> throw new TracedException(logicConstant, "Unsupported literal"); |
472 | } | 524 | } |
473 | } else if (expr instanceof Atom atom) { | 525 | } else if (expr instanceof Atom atom) { |
474 | var target = getPartialRelation(atom.getRelation()); | 526 | var target = getPartialRelation(atom.getRelation()); |
@@ -478,7 +530,7 @@ public class ModelInitializer { | |||
478 | } else if (expr instanceof NegationExpr negationExpr) { | 530 | } else if (expr instanceof NegationExpr negationExpr) { |
479 | var body = negationExpr.getBody(); | 531 | var body = negationExpr.getBody(); |
480 | if (!(body instanceof Atom atom)) { | 532 | if (!(body instanceof Atom atom)) { |
481 | throw new IllegalArgumentException("Cannot negate literal: " + body); | 533 | throw new TracedException(body, "Cannot negate literal"); |
482 | } | 534 | } |
483 | var target = getPartialRelation(atom.getRelation()); | 535 | var target = getPartialRelation(atom.getRelation()); |
484 | Constraint constraint; | 536 | Constraint constraint; |
@@ -498,11 +550,12 @@ public class ModelInitializer { | |||
498 | boolean positive = switch (comparisonExpr.getOp()) { | 550 | boolean positive = switch (comparisonExpr.getOp()) { |
499 | case EQ -> true; | 551 | case EQ -> true; |
500 | case NOT_EQ -> false; | 552 | case NOT_EQ -> false; |
501 | default -> throw new IllegalArgumentException("Unsupported operator: " + comparisonExpr.getOp()); | 553 | default -> throw new TracedException( |
554 | comparisonExpr, "Unsupported operator"); | ||
502 | }; | 555 | }; |
503 | literals.add(new EquivalenceLiteral(positive, argumentList.get(0), argumentList.get(1))); | 556 | literals.add(new EquivalenceLiteral(positive, argumentList.get(0), argumentList.get(1))); |
504 | } else { | 557 | } else { |
505 | throw new IllegalArgumentException("Unsupported literal: " + expr); | 558 | throw new TracedException(expr, "Unsupported literal"); |
506 | } | 559 | } |
507 | } | 560 | } |
508 | 561 | ||
@@ -512,7 +565,7 @@ public class ModelInitializer { | |||
512 | var argumentList = new ArrayList<Variable>(expressions.size()); | 565 | var argumentList = new ArrayList<Variable>(expressions.size()); |
513 | for (var expr : expressions) { | 566 | for (var expr : expressions) { |
514 | if (!(expr instanceof VariableOrNodeExpr variableOrNodeExpr)) { | 567 | if (!(expr instanceof VariableOrNodeExpr variableOrNodeExpr)) { |
515 | throw new IllegalArgumentException("Unsupported argument: " + expr); | 568 | throw new TracedException(expr, "Unsupported argument"); |
516 | } | 569 | } |
517 | var variableOrNode = variableOrNodeExpr.getVariableOrNode(); | 570 | var variableOrNode = variableOrNodeExpr.getVariableOrNode(); |
518 | if (variableOrNode instanceof Node node) { | 571 | if (variableOrNode instanceof Node node) { |
@@ -526,10 +579,12 @@ public class ModelInitializer { | |||
526 | } else { | 579 | } else { |
527 | var variable = localScope.get(problemVariable); | 580 | var variable = localScope.get(problemVariable); |
528 | if (variable == null) { | 581 | if (variable == null) { |
529 | throw new IllegalArgumentException("Unknown variable: " + problemVariable.getName()); | 582 | throw new TracedException(variableOrNode, "Unknown variable: " + problemVariable.getName()); |
530 | } | 583 | } |
531 | argumentList.add(variable); | 584 | argumentList.add(variable); |
532 | } | 585 | } |
586 | } else { | ||
587 | throw new TracedException(variableOrNode, "Unknown argument"); | ||
533 | } | 588 | } |
534 | } | 589 | } |
535 | return argumentList; | 590 | return argumentList; |
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/TracedException.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/TracedException.java new file mode 100644 index 00000000..38fd8a67 --- /dev/null +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/TracedException.java | |||
@@ -0,0 +1,51 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.language.semantics.model; | ||
7 | |||
8 | import org.eclipse.emf.ecore.EObject; | ||
9 | |||
10 | public class TracedException extends RuntimeException { | ||
11 | private final transient EObject sourceElement; | ||
12 | |||
13 | public TracedException(EObject sourceElement) { | ||
14 | this.sourceElement = sourceElement; | ||
15 | } | ||
16 | |||
17 | public TracedException(EObject sourceElement, String message) { | ||
18 | super(message); | ||
19 | this.sourceElement = sourceElement; | ||
20 | } | ||
21 | |||
22 | public TracedException(EObject sourceElement, String message, Throwable cause) { | ||
23 | super(message, cause); | ||
24 | this.sourceElement = sourceElement; | ||
25 | } | ||
26 | |||
27 | public TracedException(EObject sourceElement, Throwable cause) { | ||
28 | super(cause); | ||
29 | this.sourceElement = sourceElement; | ||
30 | } | ||
31 | |||
32 | public EObject getSourceElement() { | ||
33 | return sourceElement; | ||
34 | } | ||
35 | |||
36 | @Override | ||
37 | public String getMessage() { | ||
38 | var message = super.getMessage(); | ||
39 | if (message == null) { | ||
40 | return "Internal error"; | ||
41 | } | ||
42 | return message; | ||
43 | } | ||
44 | |||
45 | public static TracedException addTrace(EObject sourceElement, Throwable cause) { | ||
46 | if (cause instanceof TracedException tracedException && tracedException.sourceElement != null) { | ||
47 | return tracedException; | ||
48 | } | ||
49 | return new TracedException(sourceElement, cause); | ||
50 | } | ||
51 | } | ||