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 | |
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
8 files changed, 198 insertions, 16 deletions
diff --git a/subprojects/frontend/src/language/problem.grammar b/subprojects/frontend/src/language/problem.grammar index b08a9c36..ac451e7a 100644 --- a/subprojects/frontend/src/language/problem.grammar +++ b/subprojects/frontend/src/language/problem.grammar | |||
@@ -57,10 +57,10 @@ statement { | |||
57 | // RuleBody { ":" sep<OrOp, Conjunction> "==>" sep<OrOp, Consequent> "." } | 57 | // RuleBody { ":" sep<OrOp, Conjunction> "==>" sep<OrOp, Consequent> "." } |
58 | //} | | 58 | //} | |
59 | AtomDeclaration { | 59 | AtomDeclaration { |
60 | ckw<"atom"> sep<",", AtomNodeName> "." | 60 | kw<"declare">? ckw<"atom"> sep<",", AtomNodeName> "." |
61 | } | | 61 | } | |
62 | NodeDeclaration { | 62 | NodeDeclaration { |
63 | (ckw<"node"> | ckw<"multi">) sep<",", NodeName> "." | 63 | (kw<"declare"> | kw<"declare">? ckw<"multi">) sep<",", NodeName> "." |
64 | } | | 64 | } | |
65 | ScopeDeclaration { | 65 | ScopeDeclaration { |
66 | kw<"scope"> sep<",", ScopeElement> "." | 66 | kw<"scope"> sep<",", ScopeElement> "." |
diff --git a/subprojects/frontend/src/language/problemLanguageSupport.ts b/subprojects/frontend/src/language/problemLanguageSupport.ts index 3847fdd8..2483c2e3 100644 --- a/subprojects/frontend/src/language/problemLanguageSupport.ts +++ b/subprojects/frontend/src/language/problemLanguageSupport.ts | |||
@@ -28,7 +28,7 @@ const parserWithMetadata = parser.configure({ | |||
28 | LineComment: t.lineComment, | 28 | LineComment: t.lineComment, |
29 | BlockComment: t.blockComment, | 29 | BlockComment: t.blockComment, |
30 | 'module problem class enum pred fn scope': t.definitionKeyword, | 30 | 'module problem class enum pred fn scope': t.definitionKeyword, |
31 | 'node atom multi': t.definitionKeyword, | 31 | 'declare atom multi': t.definitionKeyword, |
32 | 'abstract extends refers contains container opposite': t.modifier, | 32 | 'abstract extends refers contains container opposite': t.modifier, |
33 | 'default error contained containment': t.modifier, | 33 | 'default error contained containment': t.modifier, |
34 | 'true false unknown error': t.keyword, | 34 | 'true false unknown error': t.keyword, |
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 | } |
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java index 82dea31b..1fb08845 100644 --- a/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java +++ b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java | |||
@@ -82,7 +82,6 @@ class AssertionValidationTest { | |||
82 | "exists(n).", | 82 | "exists(n).", |
83 | "?exists(n).", | 83 | "?exists(n).", |
84 | "!exists(n).", | 84 | "!exists(n).", |
85 | "exists(*).", | ||
86 | "?exists(*).", | 85 | "?exists(*).", |
87 | "exists(Foo::new).", | 86 | "exists(Foo::new).", |
88 | "?exists(Foo::new).", | 87 | "?exists(Foo::new).", |
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/validation/ModuleValidationTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/ModuleValidationTest.java new file mode 100644 index 00000000..00ad051b --- /dev/null +++ b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/ModuleValidationTest.java | |||
@@ -0,0 +1,145 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.language.tests.validation; | ||
7 | |||
8 | import com.google.inject.Inject; | ||
9 | import org.eclipse.xtext.testing.InjectWith; | ||
10 | import org.eclipse.xtext.testing.extensions.InjectionExtension; | ||
11 | import org.junit.jupiter.api.Test; | ||
12 | import org.junit.jupiter.api.extension.ExtendWith; | ||
13 | import org.junit.jupiter.params.ParameterizedTest; | ||
14 | import org.junit.jupiter.params.provider.Arguments; | ||
15 | import org.junit.jupiter.params.provider.MethodSource; | ||
16 | import tools.refinery.language.model.tests.utils.ProblemParseHelper; | ||
17 | import tools.refinery.language.tests.ProblemInjectorProvider; | ||
18 | import tools.refinery.language.validation.ProblemValidator; | ||
19 | |||
20 | import java.util.stream.Stream; | ||
21 | |||
22 | import static org.hamcrest.MatcherAssert.assertThat; | ||
23 | import static org.hamcrest.Matchers.*; | ||
24 | |||
25 | @ExtendWith(InjectionExtension.class) | ||
26 | @InjectWith(ProblemInjectorProvider.class) | ||
27 | class ModuleValidationTest { | ||
28 | @Inject | ||
29 | private ProblemParseHelper parseHelper; | ||
30 | |||
31 | @ParameterizedTest | ||
32 | @MethodSource | ||
33 | void invalidMultiObjectExistsTest(String invalidDeclaration) { | ||
34 | var problem = parseHelper.parse(""" | ||
35 | module. | ||
36 | |||
37 | %s | ||
38 | """.formatted(invalidDeclaration)); | ||
39 | var issues = problem.validate(); | ||
40 | assertThat(issues, hasItem(hasProperty("issueCode", | ||
41 | is(ProblemValidator.UNSUPPORTED_ASSERTION_ISSUE)))); | ||
42 | } | ||
43 | |||
44 | static Stream<Arguments> invalidMultiObjectExistsTest() { | ||
45 | return Stream.of( | ||
46 | Arguments.of(""" | ||
47 | class Foo. | ||
48 | exists(Foo::new). | ||
49 | """), | ||
50 | Arguments.of(""" | ||
51 | multi m. | ||
52 | exists(m). | ||
53 | """)); | ||
54 | } | ||
55 | |||
56 | @Test | ||
57 | void invalidScopeTest() { | ||
58 | var problem = parseHelper.parse(""" | ||
59 | module. | ||
60 | |||
61 | class Foo. | ||
62 | scope Foo += 1. | ||
63 | """); | ||
64 | var issues = problem.validate(); | ||
65 | assertThat(issues, hasItem(hasProperty("issueCode", | ||
66 | is(ProblemValidator.INVALID_MULTIPLICITY_ISSUE)))); | ||
67 | } | ||
68 | |||
69 | @Test | ||
70 | void invalidAssertionArgumentTest() { | ||
71 | var problem = parseHelper.parse(""" | ||
72 | module. | ||
73 | |||
74 | class Foo. | ||
75 | Foo(foo1). | ||
76 | """); | ||
77 | var issues = problem.validate(); | ||
78 | assertThat(issues, hasItem(allOf( | ||
79 | hasProperty("issueCode", is(ProblemValidator.UNSUPPORTED_ASSERTION_ISSUE)), | ||
80 | hasProperty("message", containsString("foo1"))))); | ||
81 | } | ||
82 | |||
83 | @ParameterizedTest | ||
84 | @MethodSource | ||
85 | void validDeclarationTest(String validDeclaration) { | ||
86 | var problem = parseHelper.parse(validDeclaration); | ||
87 | var issues = problem.validate(); | ||
88 | assertThat(issues, hasSize(0)); | ||
89 | } | ||
90 | |||
91 | static Stream<Arguments> validDeclarationTest() { | ||
92 | return Stream.concat( | ||
93 | invalidMultiObjectExistsTest(), | ||
94 | Stream.of( | ||
95 | Arguments.of(""" | ||
96 | class Foo. | ||
97 | scope Foo += 1. | ||
98 | """), | ||
99 | Arguments.of(""" | ||
100 | module. | ||
101 | |||
102 | class Foo. | ||
103 | scope Foo = 1. | ||
104 | """), | ||
105 | Arguments.of(""" | ||
106 | class Foo. | ||
107 | Foo(foo1). | ||
108 | """), | ||
109 | Arguments.of(""" | ||
110 | module. | ||
111 | |||
112 | class Foo. | ||
113 | multi foo1. | ||
114 | Foo(foo1). | ||
115 | """), | ||
116 | Arguments.of(""" | ||
117 | module. | ||
118 | |||
119 | class Foo. | ||
120 | atom foo1. | ||
121 | Foo(foo1). | ||
122 | """), | ||
123 | Arguments.of(""" | ||
124 | module. | ||
125 | |||
126 | class Foo. | ||
127 | declare foo1. | ||
128 | Foo(foo1). | ||
129 | """), | ||
130 | Arguments.of(""" | ||
131 | module. | ||
132 | |||
133 | enum Foo { foo1 } | ||
134 | Foo(foo1). | ||
135 | """), | ||
136 | Arguments.of(""" | ||
137 | module. | ||
138 | |||
139 | class Foo. | ||
140 | Foo(Foo::new). | ||
141 | """) | ||
142 | ) | ||
143 | ); | ||
144 | } | ||
145 | } | ||