diff options
author | 2024-07-05 19:54:38 +0200 | |
---|---|---|
committer | 2024-07-05 19:54:38 +0200 | |
commit | c991b64b1839fcf5dcfd29fa1de9d0ceeb90f792 (patch) | |
tree | 672f862efec5b485d12163f9765c1c3efc8ef926 /subprojects/language/src/main/java/tools | |
parent | refactor(reasoning): remove errors when possible (diff) | |
download | refinery-c991b64b1839fcf5dcfd29fa1de9d0ceeb90f792.tar.gz refinery-c991b64b1839fcf5dcfd29fa1de9d0ceeb90f792.tar.zst refinery-c991b64b1839fcf5dcfd29fa1de9d0ceeb90f792.zip |
feat(language): shadow predicate validation and content assist
Diffstat (limited to 'subprojects/language/src/main/java/tools')
3 files changed, 64 insertions, 18 deletions
diff --git a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext index 3a897cc0..7e3b3c83 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext +++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext | |||
@@ -187,7 +187,7 @@ enum Modality: | |||
187 | MUST="must" | MAY="may"; | 187 | MUST="must" | MAY="may"; |
188 | 188 | ||
189 | ModalExpr: | 189 | ModalExpr: |
190 | (concreteness=Concreteness => modality=Modality? | modality=Modality) | 190 | (concreteness=Concreteness => modality=Modality? | modality=Modality => concreteness=Concreteness?) |
191 | body=UnaryExpr; | 191 | body=UnaryExpr; |
192 | 192 | ||
193 | CastExpr returns Expr: | 193 | CastExpr returns Expr: |
diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java index c2c19d74..067e684a 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java | |||
@@ -57,6 +57,15 @@ public final class ProblemUtil { | |||
57 | return eObject instanceof PredicateDefinition predicateDefinition && predicateDefinition.isShadow(); | 57 | return eObject instanceof PredicateDefinition predicateDefinition && predicateDefinition.isShadow(); |
58 | } | 58 | } |
59 | 59 | ||
60 | public static boolean mayReferToShadow(EObject context) { | ||
61 | var definitionContext = EcoreUtil2.getContainerOfType(context, ParametricDefinition.class); | ||
62 | return switch (definitionContext) { | ||
63 | case PredicateDefinition predicateDefinition -> predicateDefinition.isShadow(); | ||
64 | case RuleDefinition ignored -> true; | ||
65 | case null, default -> false; | ||
66 | }; | ||
67 | } | ||
68 | |||
60 | public static boolean isAtomNode(Node node) { | 69 | public static boolean isAtomNode(Node node) { |
61 | var containingFeature = node.eContainingFeature(); | 70 | var containingFeature = node.eContainingFeature(); |
62 | if (containingFeature == ProblemPackage.Literals.NODE_DECLARATION__NODES) { | 71 | if (containingFeature == ProblemPackage.Literals.NODE_DECLARATION__NODES) { |
diff --git a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java index 343340bd..8d64933f 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java +++ b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java | |||
@@ -357,26 +357,46 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
357 | 357 | ||
358 | @Check | 358 | @Check |
359 | public void checkReferenceType(ReferenceDeclaration referenceDeclaration) { | 359 | public void checkReferenceType(ReferenceDeclaration referenceDeclaration) { |
360 | var referenceType = referenceDeclaration.getReferenceType(); | ||
361 | if (referenceType == null || referenceType.eIsProxy()) { | ||
362 | return; | ||
363 | } | ||
360 | boolean isDefaultReference = referenceDeclaration.getKind() == ReferenceKind.DEFAULT && | 364 | boolean isDefaultReference = referenceDeclaration.getKind() == ReferenceKind.DEFAULT && |
361 | !ProblemUtil.isContainerReference(referenceDeclaration); | 365 | !ProblemUtil.isContainerReference(referenceDeclaration); |
362 | if (isDefaultReference || referenceDeclaration.getKind() == ReferenceKind.REFERENCE) { | 366 | if (isDefaultReference || referenceDeclaration.getKind() == ReferenceKind.REFERENCE) { |
363 | checkArity(referenceDeclaration, ProblemPackage.Literals.REFERENCE_DECLARATION__REFERENCE_TYPE, 1); | 367 | checkArity(referenceDeclaration, ProblemPackage.Literals.REFERENCE_DECLARATION__REFERENCE_TYPE, 1); |
364 | return; | 368 | if (ProblemUtil.isShadow(referenceType)) { |
369 | var message = "Shadow relations '%s' is not allowed in reference types." | ||
370 | .formatted(referenceType.getName()); | ||
371 | acceptError(message, referenceDeclaration, | ||
372 | ProblemPackage.Literals.REFERENCE_DECLARATION__REFERENCE_TYPE, 0, SHADOW_RELATION_ISSUE); | ||
373 | } | ||
374 | } else if (!(referenceType instanceof ClassDeclaration)) { | ||
375 | var message = "Reference type '%s' of the containment or container reference '%s' is not a class." | ||
376 | .formatted(referenceType.getName(), referenceDeclaration.getName()); | ||
377 | acceptError(message, referenceDeclaration, ProblemPackage.Literals.REFERENCE_DECLARATION__REFERENCE_TYPE, | ||
378 | 0, INVALID_REFERENCE_TYPE_ISSUE); | ||
365 | } | 379 | } |
366 | var referenceType = referenceDeclaration.getReferenceType(); | 380 | } |
367 | if (referenceType == null || referenceType.eIsProxy() || referenceType instanceof ClassDeclaration) { | 381 | |
368 | // Either correct, or a missing reference type where we are probably already emitting another error. | 382 | @Check |
369 | return; | 383 | public void checkPredicateDefinition(PredicateDefinition predicateDefinition) { |
384 | if (predicateDefinition.isError() && predicateDefinition.isShadow()) { | ||
385 | var message = "Shadow predicates cannot be marked as error predicates."; | ||
386 | acceptError(message, predicateDefinition, ProblemPackage.Literals.PREDICATE_DEFINITION__ERROR, 0, | ||
387 | SHADOW_RELATION_ISSUE); | ||
370 | } | 388 | } |
371 | var message = "Reference type '%s' of the containment or container reference '%s' is not a class." | ||
372 | .formatted(referenceType.getName(), referenceDeclaration.getName()); | ||
373 | acceptError(message, referenceDeclaration, ProblemPackage.Literals.REFERENCE_DECLARATION__REFERENCE_TYPE, 0, | ||
374 | INVALID_REFERENCE_TYPE_ISSUE); | ||
375 | } | 389 | } |
376 | 390 | ||
377 | @Check | 391 | @Check |
378 | public void checkParameter(Parameter parameter) { | 392 | public void checkParameter(Parameter parameter) { |
379 | checkArity(parameter, ProblemPackage.Literals.PARAMETER__PARAMETER_TYPE, 1); | 393 | checkArity(parameter, ProblemPackage.Literals.PARAMETER__PARAMETER_TYPE, 1); |
394 | var type = parameter.getParameterType(); | ||
395 | if (type != null && !type.eIsProxy() && ProblemUtil.isShadow(type)) { | ||
396 | var message = "Shadow relations '%s' is not allowed in parameter types.".formatted(type.getName()); | ||
397 | acceptError(message, parameter, ProblemPackage.Literals.PARAMETER__PARAMETER_TYPE, 0, | ||
398 | SHADOW_RELATION_ISSUE); | ||
399 | } | ||
380 | var parametricDefinition = EcoreUtil2.getContainerOfType(parameter, ParametricDefinition.class); | 400 | var parametricDefinition = EcoreUtil2.getContainerOfType(parameter, ParametricDefinition.class); |
381 | if (parametricDefinition instanceof RuleDefinition rule) { | 401 | if (parametricDefinition instanceof RuleDefinition rule) { |
382 | var kind = rule.getKind(); | 402 | var kind = rule.getKind(); |
@@ -399,7 +419,6 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
399 | @Check | 419 | @Check |
400 | public void checkAtom(Atom atom) { | 420 | public void checkAtom(Atom atom) { |
401 | int argumentCount = atom.getArguments().size(); | 421 | int argumentCount = atom.getArguments().size(); |
402 | checkArity(atom, ProblemPackage.Literals.ATOM__RELATION, argumentCount); | ||
403 | if (atom.isTransitiveClosure() && argumentCount != 2) { | 422 | if (atom.isTransitiveClosure() && argumentCount != 2) { |
404 | var message = "Transitive closure needs exactly 2 arguments, got %d arguments instead." | 423 | var message = "Transitive closure needs exactly 2 arguments, got %d arguments instead." |
405 | .formatted(argumentCount); | 424 | .formatted(argumentCount); |
@@ -407,12 +426,13 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
407 | INVALID_TRANSITIVE_CLOSURE_ISSUE); | 426 | INVALID_TRANSITIVE_CLOSURE_ISSUE); |
408 | } | 427 | } |
409 | var target = atom.getRelation(); | 428 | var target = atom.getRelation(); |
410 | if (target != null && !target.eIsProxy() && ProblemUtil.isShadow(target)) { | 429 | if (target == null || target.eIsProxy()) { |
411 | var definitionContext = EcoreUtil2.getContainerOfType(atom, ParametricDefinition.class); | 430 | return; |
412 | if (!(definitionContext instanceof RuleDefinition)){ | 431 | } |
413 | var message = "Shadow relation '%s' may only appear in rule definitions.".formatted(target.getName()); | 432 | checkArity(atom, ProblemPackage.Literals.ATOM__RELATION, argumentCount); |
414 | acceptError(message, atom, ProblemPackage.Literals.ATOM__RELATION, 0, SHADOW_RELATION_ISSUE); | 433 | if (ProblemUtil.isShadow(target) && !ProblemUtil.mayReferToShadow(atom)) { |
415 | } | 434 | var message = "Shadow relation '%s' is not allowed in a non-shadow context.".formatted(target.getName()); |
435 | acceptError(message, atom, ProblemPackage.Literals.ATOM__RELATION, 0, SHADOW_RELATION_ISSUE); | ||
416 | } | 436 | } |
417 | } | 437 | } |
418 | 438 | ||
@@ -485,23 +505,40 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
485 | @Check | 505 | @Check |
486 | public void checkAssertion(AbstractAssertion assertion) { | 506 | public void checkAssertion(AbstractAssertion assertion) { |
487 | var relation = assertion.getRelation(); | 507 | var relation = assertion.getRelation(); |
508 | if (relation == null || relation.eIsProxy()) { | ||
509 | return; | ||
510 | } | ||
488 | if (relation instanceof DatatypeDeclaration) { | 511 | if (relation instanceof DatatypeDeclaration) { |
489 | var message = "Assertions for data types are not supported."; | 512 | var message = "Assertions for data types are not supported."; |
490 | acceptError(message, assertion, ProblemPackage.Literals.ABSTRACT_ASSERTION__RELATION, 0, | 513 | acceptError(message, assertion, ProblemPackage.Literals.ABSTRACT_ASSERTION__RELATION, 0, |
491 | UNSUPPORTED_ASSERTION_ISSUE); | 514 | UNSUPPORTED_ASSERTION_ISSUE); |
492 | return; | 515 | return; |
493 | } | 516 | } |
517 | if (ProblemUtil.isShadow(relation)) { | ||
518 | var message = "Shadow relation '%s' may not have any assertions.".formatted(relation.getName()); | ||
519 | acceptError(message, assertion, ProblemPackage.Literals.ABSTRACT_ASSERTION__RELATION, 0, | ||
520 | SHADOW_RELATION_ISSUE); | ||
521 | } | ||
494 | int argumentCount = assertion.getArguments().size(); | 522 | int argumentCount = assertion.getArguments().size(); |
495 | checkArity(assertion, ProblemPackage.Literals.ABSTRACT_ASSERTION__RELATION, argumentCount); | 523 | checkArity(assertion, ProblemPackage.Literals.ABSTRACT_ASSERTION__RELATION, argumentCount); |
496 | } | 524 | } |
497 | 525 | ||
498 | @Check | 526 | @Check |
499 | public void checkTypeScope(TypeScope typeScope) { | 527 | public void checkTypeScope(TypeScope typeScope) { |
500 | checkArity(typeScope, ProblemPackage.Literals.TYPE_SCOPE__TARGET_TYPE, 1); | ||
501 | if (typeScope.isIncrement() && ProblemUtil.isInModule(typeScope)) { | 528 | if (typeScope.isIncrement() && ProblemUtil.isInModule(typeScope)) { |
502 | acceptError("Incremental type scopes are not supported in modules", typeScope, null, 0, | 529 | acceptError("Incremental type scopes are not supported in modules", typeScope, null, 0, |
503 | INVALID_MULTIPLICITY_ISSUE); | 530 | INVALID_MULTIPLICITY_ISSUE); |
504 | } | 531 | } |
532 | var type = typeScope.getTargetType(); | ||
533 | if (type == null || type.eIsProxy()) { | ||
534 | return; | ||
535 | } | ||
536 | checkArity(typeScope, ProblemPackage.Literals.TYPE_SCOPE__TARGET_TYPE, 1); | ||
537 | if (ProblemUtil.isShadow(type)) { | ||
538 | var message = "Shadow relations '%s' is not allowed in type scopes.".formatted(type.getName()); | ||
539 | acceptError(message, typeScope, ProblemPackage.Literals.TYPE_SCOPE__TARGET_TYPE, 0, | ||
540 | SHADOW_RELATION_ISSUE); | ||
541 | } | ||
505 | } | 542 | } |
506 | 543 | ||
507 | private void checkArity(EObject eObject, EReference reference, int expectedArity) { | 544 | private void checkArity(EObject eObject, EReference reference, int expectedArity) { |