diff options
author | Kristóf Marussy <kristof@marussy.com> | 2024-01-31 17:10:28 +0100 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2024-01-31 18:45:13 +0100 |
commit | a2a92561f7b612b472b5b7e49a2d5ca86802092f (patch) | |
tree | b5124c3936cfaba4d046cfc3f4676af5b940d19c /subprojects/language/src/main | |
parent | refactor(language): module and node declarations (diff) | |
download | refinery-a2a92561f7b612b472b5b7e49a2d5ca86802092f.tar.gz refinery-a2a92561f7b612b472b5b7e49a2d5ca86802092f.tar.zst refinery-a2a92561f7b612b472b5b7e49a2d5ca86802092f.zip |
feat(language): validate module isolation
Diffstat (limited to 'subprojects/language/src/main')
4 files changed, 50 insertions, 12 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 c5c42ebe..4ce3fae1 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext +++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext | |||
@@ -256,10 +256,11 @@ ExactMultiplicity: | |||
256 | exactValue=INT; | 256 | exactValue=INT; |
257 | 257 | ||
258 | NodeDeclaration: | 258 | NodeDeclaration: |
259 | kind=NodeKind nodes+=EnumLiteral ("," nodes+=EnumLiteral)* "."; | 259 | ("declare" | "declare"? kind=NodeKind) |
260 | nodes+=EnumLiteral ("," nodes+=EnumLiteral)* "."; | ||
260 | 261 | ||
261 | enum NodeKind: | 262 | enum NodeKind: |
262 | NODE="node" | ATOM="atom" | MULTI="multi"; | 263 | ATOM="atom" | MULTI="multi"; |
263 | 264 | ||
264 | UpperBound returns ecore::EInt: | 265 | UpperBound returns ecore::EInt: |
265 | INT | "*"; | 266 | INT | "*"; |
@@ -274,7 +275,7 @@ Identifier: | |||
274 | NonContainmentIdentifier | "contains" | "container"; | 275 | NonContainmentIdentifier | "contains" | "container"; |
275 | 276 | ||
276 | NonContainmentIdentifier: | 277 | NonContainmentIdentifier: |
277 | ID | "node" | "atom" | "multi" | "contained" | | 278 | ID | "atom" | "multi" | "contained" | |
278 | "sum" | "prod" | "min" | "max" | "problem" | "module"; | 279 | "sum" | "prod" | "min" | "max" | "problem" | "module"; |
279 | 280 | ||
280 | Real returns ecore::EDouble: | 281 | Real returns ecore::EDouble: |
diff --git a/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java b/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java index 0b87e8bb..d6ece1ea 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java +++ b/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java | |||
@@ -23,7 +23,7 @@ public class ProblemFormatter extends AbstractJavaFormatter { | |||
23 | protected void format(Problem problem, IFormattableDocument doc) { | 23 | protected void format(Problem problem, IFormattableDocument doc) { |
24 | doc.prepend(problem, this::noSpace); | 24 | doc.prepend(problem, this::noSpace); |
25 | var region = regionFor(problem); | 25 | var region = regionFor(problem); |
26 | doc.append(region.feature(ProblemPackage.Literals.PROBLEM__KIND), this::oneSpace); | 26 | doc.prepend(region.feature(ProblemPackage.Literals.NAMED_ELEMENT__NAME), this::oneSpace); |
27 | doc.prepend(region.keyword("."), this::noSpace); | 27 | doc.prepend(region.keyword("."), this::noSpace); |
28 | appendNewLines(doc, region.keyword("."), this::twoNewLines); | 28 | appendNewLines(doc, region.keyword("."), this::twoNewLines); |
29 | for (var statement : problem.getStatements()) { | 29 | for (var statement : problem.getStatements()) { |
@@ -135,6 +135,7 @@ public class ProblemFormatter extends AbstractJavaFormatter { | |||
135 | protected void format(NodeDeclaration nodeDeclaration, IFormattableDocument doc) { | 135 | protected void format(NodeDeclaration nodeDeclaration, IFormattableDocument doc) { |
136 | surroundNewLines(doc, nodeDeclaration, this::singleNewLine); | 136 | surroundNewLines(doc, nodeDeclaration, this::singleNewLine); |
137 | var region = regionFor(nodeDeclaration); | 137 | var region = regionFor(nodeDeclaration); |
138 | doc.append(region.keyword("declare"), this::oneSpace); | ||
138 | doc.append(region.feature(ProblemPackage.Literals.NODE_DECLARATION__KIND), this::oneSpace); | 139 | doc.append(region.feature(ProblemPackage.Literals.NODE_DECLARATION__KIND), this::oneSpace); |
139 | formatList(region, ",", doc); | 140 | formatList(region, ",", doc); |
140 | doc.prepend(region.keyword("."), this::noSpace); | 141 | doc.prepend(region.keyword("."), this::noSpace); |
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 ee0e141d..0f87c04b 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 | |||
@@ -8,6 +8,7 @@ package tools.refinery.language.utils; | |||
8 | import org.eclipse.emf.common.util.URI; | 8 | import org.eclipse.emf.common.util.URI; |
9 | import org.eclipse.emf.ecore.EObject; | 9 | import org.eclipse.emf.ecore.EObject; |
10 | import org.eclipse.emf.ecore.util.EcoreUtil; | 10 | import org.eclipse.emf.ecore.util.EcoreUtil; |
11 | import org.eclipse.xtext.EcoreUtil2; | ||
11 | import tools.refinery.language.model.problem.*; | 12 | import tools.refinery.language.model.problem.*; |
12 | 13 | ||
13 | public final class ProblemUtil { | 14 | public final class ProblemUtil { |
@@ -126,6 +127,11 @@ public final class ProblemUtil { | |||
126 | }; | 127 | }; |
127 | } | 128 | } |
128 | 129 | ||
130 | public static boolean isInModule(EObject eObject) { | ||
131 | var problem = EcoreUtil2.getContainerOfType(eObject, Problem.class); | ||
132 | return problem != null && problem.getKind() == ModuleKind.MODULE; | ||
133 | } | ||
134 | |||
129 | private static URI getLibraryUri() { | 135 | private static URI getLibraryUri() { |
130 | var libraryResource = ProblemUtil.class.getClassLoader() | 136 | var libraryResource = ProblemUtil.class.getClassLoader() |
131 | .getResource("tools/refinery/language/%s.problem".formatted(BUILTIN_LIBRARY_NAME)); | 137 | .getResource("tools/refinery/language/%s.problem".formatted(BUILTIN_LIBRARY_NAME)); |
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 a95e8b3c..4cbb02c2 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 | |||
@@ -86,8 +86,8 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
86 | var variableOrNode = expr.getVariableOrNode(); | 86 | var variableOrNode = expr.getVariableOrNode(); |
87 | if (variableOrNode instanceof Node node && !ProblemUtil.isAtomNode(node)) { | 87 | if (variableOrNode instanceof Node node && !ProblemUtil.isAtomNode(node)) { |
88 | var name = node.getName(); | 88 | var name = node.getName(); |
89 | var message = ("Only individuals can be referenced in predicates. " + | 89 | var message = ("Only atoms can be referenced in predicates. " + |
90 | "Mark '%s' as individual with the declaration 'indiv %s.'").formatted(name, name); | 90 | "Mark '%s' as an atom with the declaration 'atom %s.'").formatted(name, name); |
91 | error(message, expr, ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE, | 91 | error(message, expr, ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE, |
92 | INSIGNIFICANT_INDEX, NODE_CONSTANT_ISSUE); | 92 | INSIGNIFICANT_INDEX, NODE_CONSTANT_ISSUE); |
93 | } | 93 | } |
@@ -302,6 +302,10 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
302 | @Check | 302 | @Check |
303 | public void checkTypeScope(TypeScope typeScope) { | 303 | public void checkTypeScope(TypeScope typeScope) { |
304 | checkArity(typeScope, ProblemPackage.Literals.TYPE_SCOPE__TARGET_TYPE, 1); | 304 | checkArity(typeScope, ProblemPackage.Literals.TYPE_SCOPE__TARGET_TYPE, 1); |
305 | if (typeScope.isIncrement() && ProblemUtil.isInModule(typeScope)) { | ||
306 | acceptError("Incremental type scopes are not supported in modules", typeScope, null, 0, | ||
307 | INVALID_MULTIPLICITY_ISSUE); | ||
308 | } | ||
305 | } | 309 | } |
306 | 310 | ||
307 | private void checkArity(EObject eObject, EReference reference, int expectedArity) { | 311 | private void checkArity(EObject eObject, EReference reference, int expectedArity) { |
@@ -351,9 +355,9 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
351 | } | 355 | } |
352 | 356 | ||
353 | private void checkExistsAssertion(Assertion assertion, LogicValue value) { | 357 | private void checkExistsAssertion(Assertion assertion, LogicValue value) { |
354 | if (value == LogicValue.TRUE || value == LogicValue.UNKNOWN) { | 358 | if (value == LogicValue.UNKNOWN) { |
355 | // {@code true} is always a valid value for {@code exists}, while {@code unknown} values may always be | 359 | // {@code unknown} values may always be refined to {@code true} of {@code false} if necessary (e.g., for |
356 | // refined to {@code true} if necessary (e.g., for individual nodes). | 360 | // atom nodes or removed multi-objects). |
357 | return; | 361 | return; |
358 | } | 362 | } |
359 | var arguments = assertion.getArguments(); | 363 | var arguments = assertion.getArguments(); |
@@ -361,9 +365,16 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
361 | // We already report an error on invalid arity. | 365 | // We already report an error on invalid arity. |
362 | return; | 366 | return; |
363 | } | 367 | } |
364 | var node = getNodeArgumentForMultiObjectAssertion(arguments.get(0)); | 368 | var node = getNodeArgumentForMultiObjectAssertion(arguments.getFirst()); |
365 | if (node != null && !node.eIsProxy() && ProblemUtil.isAtomNode(node)) { | 369 | if (node == null || node.eIsProxy()) { |
366 | acceptError("Individual nodes must exist.", assertion, null, 0, UNSUPPORTED_ASSERTION_ISSUE); | 370 | return; |
371 | } | ||
372 | if (ProblemUtil.isAtomNode(node) && value != LogicValue.TRUE) { | ||
373 | acceptError("Atom nodes must exist.", assertion, null, 0, UNSUPPORTED_ASSERTION_ISSUE); | ||
374 | } | ||
375 | if (ProblemUtil.isMultiNode(node) && value != LogicValue.FALSE && ProblemUtil.isInModule(node)) { | ||
376 | acceptError("Multi-objects in modules cannot be required to exist.", assertion, null, 0, | ||
377 | UNSUPPORTED_ASSERTION_ISSUE); | ||
367 | } | 378 | } |
368 | } | 379 | } |
369 | 380 | ||
@@ -403,4 +414,23 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
403 | } | 414 | } |
404 | throw new IllegalArgumentException("Unknown assertion argument: " + argument); | 415 | throw new IllegalArgumentException("Unknown assertion argument: " + argument); |
405 | } | 416 | } |
417 | |||
418 | @Check | ||
419 | private void checkImplicitNodeInModule(Assertion assertion) { | ||
420 | if (!ProblemUtil.isInModule(assertion)) { | ||
421 | return; | ||
422 | } | ||
423 | for (var argument : assertion.getArguments()) { | ||
424 | if (argument instanceof NodeAssertionArgument nodeAssertionArgument) { | ||
425 | var node = nodeAssertionArgument.getNode(); | ||
426 | if (node != null && !node.eIsProxy() && ProblemUtil.isImplicitNode(node)) { | ||
427 | var name = node.getName(); | ||
428 | var message = ("Implicit nodes are not allowed in modules. Explicitly declare '%s' as a node " + | ||
429 | "with the declaration 'declare %s.'").formatted(name, name); | ||
430 | acceptError(message, nodeAssertionArgument, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE, | ||
431 | 0, UNSUPPORTED_ASSERTION_ISSUE); | ||
432 | } | ||
433 | } | ||
434 | } | ||
435 | } | ||
406 | } | 436 | } |