Merge pull request #53 from kris7t/imports

Module and import resolution support

6 files changed, 191 insertions, 65 deletions

diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/ProblemParsingTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/ProblemParsingTest.java
index 72d57f54..17ae5fbb 100644
--- a/subprojects/language/src/test/java/tools/refinery/language/tests/ProblemParsingTest.java
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/ProblemParsingTest.java
@@ -42,7 +42,7 @@ class ProblemParsingTest {
                                 error invalidTaxStatus(Person p) <->
                                         taxStatus(p, CHILD), children(p, _q).
 
-                                indiv family.
+                                atom family.
                                 Family(family).
                                 members(family, anne): true.
                                 members(family, bob).
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/formatting2/ProblemFormatterTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/formatting2/ProblemFormatterTest.java
index f688d970..4a15f9de 100644
--- a/subprojects/language/src/test/java/tools/refinery/language/tests/formatting2/ProblemFormatterTest.java
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/formatting2/ProblemFormatterTest.java
@@ -183,8 +183,8 @@ class ProblemFormatterTest {
         }
 
         @Test
-        void individualDeclarationTest() {
-                testFormatter("  indiv  a  ,  b  .  ", "indiv a, b.\n");
+        void atomDeclarationTest() {
+                testFormatter("  atom  a  ,  b  .  ", "atom a, b.\n");
         }
 
         @Test
@@ -194,7 +194,7 @@ class ProblemFormatterTest {
                                 pred foo(node a).
                                 class Foo.
                                 foo(n1, n2).
-                                indiv i1.
+                                atom i1.
                                 !foo(i1, n1).
                                 pred bar(node a, node b).
                                 pred quux().
@@ -207,7 +207,7 @@ class ProblemFormatterTest {
                                 class Foo.
 
                                 foo(n1, n2).
-                                indiv i1.
+                                atom i1.
                                 !foo(i1, n1).
 
                                 pred bar(node a, node b).
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/scoping/NodeScopingTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/scoping/NodeScopingTest.java
index e76d2993..0704e026 100644
--- a/subprojects/language/src/test/java/tools/refinery/language/tests/scoping/NodeScopingTest.java
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/scoping/NodeScopingTest.java
@@ -1,5 +1,5 @@
 /*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors <https://refinery.tools/>
  *
  * SPDX-License-Identifier: EPL-2.0
  */
@@ -68,37 +68,31 @@ class NodeScopingTest {
                 assertThat(problem.assertion(0).arg(0).node(), equalTo(problem.node("b")));
         }
 
-        @ParameterizedTest
-        @MethodSource("individualNodeReferenceSource")
-        void individualNodeInAssertionTest(String qualifiedNamePrefix, boolean namedProblem) {
+        @Test
+        void atomNodeInAssertionTest() {
                 var problem = parse("""
-                                indiv a, b.
+                                atom a, b.
                                 pred predicate(node x, node y) <-> node(x).
-                                predicate({PARAM}a, {PARAM}a).
-                                ?predicate({PARAM}a, {PARAM}b).
-                                """, qualifiedNamePrefix, namedProblem);
+                                predicate(a, a).
+                                ?predicate(a, b).
+                                """);
                 assertThat(problem.getResourceErrors(), empty());
                 assertThat(problem.nodeNames(), empty());
-                assertThat(problem.assertion(0).arg(0).node(), equalTo(problem.individualNode("a")));
-                assertThat(problem.assertion(0).arg(1).node(), equalTo(problem.individualNode("a")));
-                assertThat(problem.assertion(1).arg(0).node(), equalTo(problem.individualNode("a")));
-                assertThat(problem.assertion(1).arg(1).node(), equalTo(problem.individualNode("b")));
+                assertThat(problem.assertion(0).arg(0).node(), equalTo(problem.atomNode("a")));
+                assertThat(problem.assertion(0).arg(1).node(), equalTo(problem.atomNode("a")));
+                assertThat(problem.assertion(1).arg(0).node(), equalTo(problem.atomNode("a")));
+                assertThat(problem.assertion(1).arg(1).node(), equalTo(problem.atomNode("b")));
         }
 
-        @ParameterizedTest
-        @MethodSource("individualNodeReferenceSource")
-        void individualNodeInPredicateTest(String qualifiedNamePrefix, boolean namedProblem) {
+        @Test
+        void atomNodeInPredicateTest() {
                 var problem = parse("""
-                                indiv b.
-                                pred predicate(node a) <-> node({PARAM}b).
+                                atom b.
+                                pred predicate(node a) <-> node(b).
                                 """);
                 assertThat(problem.getResourceErrors(), empty());
                 assertThat(problem.nodeNames(), empty());
-                assertThat(problem.pred("predicate").conj(0).lit(0).arg(0).node(), equalTo(problem.individualNode("b")));
-        }
-
-        static Stream<Arguments> individualNodeReferenceSource() {
-                return Stream.of(Arguments.of("", false), Arguments.of("", true), Arguments.of("test::", true));
+                assertThat(problem.pred("predicate").conj(0).lit(0).arg(0).node(), equalTo(problem.atomNode("b")));
         }
 
         @Disabled("No nodes are present in builtin.problem currently")
@@ -131,37 +125,30 @@ class NodeScopingTest {
                 return Stream.of(Arguments.of("int::new"), Arguments.of("builtin::int::new"));
         }
 
-        @ParameterizedTest
-        @MethodSource("classNewNodeReferencesSource")
-        void classNewNodeTest(String qualifiedName, boolean namedProblem) {
+        @Test
+        void classNewNodeTest() {
                 var problem = parse("""
                                 class Foo.
                                 pred predicate(node x) <-> node(x).
-                                predicate({PARAM}).
-                                """, qualifiedName, namedProblem);
+                                predicate(Foo::new).
+                                """);
                 assertThat(problem.getResourceErrors(), empty());
                 assertThat(problem.nodeNames(), empty());
                 assertThat(problem.assertion(0).arg(0).node(), equalTo(problem.findClass("Foo").get().getNewNode()));
         }
 
-        @ParameterizedTest
-        @MethodSource("classNewNodeReferencesSource")
-        void classNewNodeInPredicateTest(String qualifiedName, boolean namedProblem) {
+        @Test
+        void classNewNodeInPredicateTest() {
                 var problem = parse("""
                                 class Foo.
-                                pred predicate(node x) <-> node({PARAM}).
-                                """, qualifiedName, namedProblem);
+                                pred predicate(node x) <-> node(Foo::new).
+                                """);
                 assertThat(problem.getResourceErrors(), empty());
                 assertThat(problem.nodeNames(), empty());
                 assertThat(problem.pred("predicate").conj(0).lit(0).arg(0).node(),
                                 equalTo(problem.findClass("Foo").get().getNewNode()));
         }
 
-        static Stream<Arguments> classNewNodeReferencesSource() {
-                return Stream.of(Arguments.of("Foo::new", false), Arguments.of("Foo::new", true),
-                                Arguments.of("test::Foo::new", true));
-        }
-
         @Test
         void newNodeIsNotSpecial() {
                 var problem = parse("""
@@ -176,12 +163,12 @@ class NodeScopingTest {
 
         @ParameterizedTest
         @MethodSource("enumLiteralReferencesSource")
-        void enumLiteralTest(String qualifiedName, boolean namedProblem) {
+        void enumLiteralTest(String qualifiedName) {
                 var problem = parse("""
                                 enum Foo { alpha, beta }
                                 pred predicate(Foo a) <-> node(a).
                                 predicate({PARAM}).
-                                """, qualifiedName, namedProblem);
+                                """, qualifiedName);
                 assertThat(problem.getResourceErrors(), empty());
                 assertThat(problem.nodeNames(), empty());
                 assertThat(problem.assertion(0).arg(0).node(), equalTo(problem.findEnum("Foo").literal("alpha")));
@@ -189,11 +176,11 @@ class NodeScopingTest {
 
         @ParameterizedTest
         @MethodSource("enumLiteralReferencesSource")
-        void enumLiteralInPredicateTest(String qualifiedName, boolean namedProblem) {
+        void enumLiteralInPredicateTest(String qualifiedName) {
                 var problem = parse("""
                                 enum Foo { alpha, beta }
                                 pred predicate(Foo a) <-> node({PARAM}).
-                                """, qualifiedName, namedProblem);
+                                """, qualifiedName);
                 assertThat(problem.getResourceErrors(), empty());
                 assertThat(problem.nodeNames(), empty());
                 assertThat(problem.pred("predicate").conj(0).lit(0).arg(0).node(),
@@ -201,9 +188,7 @@ class NodeScopingTest {
         }
 
         static Stream<Arguments> enumLiteralReferencesSource() {
-                return Stream.of(Arguments.of("alpha", false), Arguments.of("alpha", true), Arguments.of("Foo::alpha", false),
-                                Arguments.of("Foo::alpha", true), Arguments.of("test::alpha", true),
-                                Arguments.of("test::Foo::alpha", true));
+                return Stream.of(Arguments.of("alpha"), Arguments.of("Foo::alpha"));
         }
 
         @Disabled("No enum literals are present in builtin.problem currently")
@@ -222,7 +207,7 @@ class NodeScopingTest {
         @Disabled("No enum literals are present in builtin.problem currently")
         @ParameterizedTest
         @MethodSource("builtInEnumLiteralReferencesSource")
-        void bultInEnumLiteralInPredicateTest(String qualifiedName) {
+        void builtInEnumLiteralInPredicateTest(String qualifiedName) {
                 var problem = parse("""
                                 pred predicate() <-> node({PARAM}).
                                 """, qualifiedName);
@@ -237,13 +222,8 @@ class NodeScopingTest {
                                 Arguments.of("builtin::bool::true"));
         }
 
-        private WrappedProblem parse(String text, String parameter, boolean namedProblem) {
-                var problemName = namedProblem ? "problem test.\n" : "";
-                return parseHelper.parse(problemName + text.replace("{PARAM}", parameter));
-        }
-
         private WrappedProblem parse(String text, String parameter) {
-                return parse(text, parameter, false);
+                return parseHelper.parse(text.replace("{PARAM}", parameter));
         }
 
         private WrappedProblem parse(String text) {
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java
index 65675b6b..ad583f8e 100644
--- a/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java
@@ -56,15 +56,16 @@ class ProblemSerializerTest {
                 var pred = createPred();
                 var node = ProblemFactory.eINSTANCE.createNode();
                 node.setName("a");
-                var individualDeclaration = ProblemFactory.eINSTANCE.createIndividualDeclaration();
-                individualDeclaration.getNodes().add(node);
-                problem.getStatements().add(individualDeclaration);
+                var atomDeclaration = ProblemFactory.eINSTANCE.createNodeDeclaration();
+                atomDeclaration.setKind(NodeKind.ATOM);
+                atomDeclaration.getNodes().add(node);
+                problem.getStatements().add(atomDeclaration);
                 createAssertion(pred, node, value);
 
                 assertSerializedResult("""
                                 pred foo(node p).
 
-                                indiv a.
+                                atom a.
                                 """ + serializedAssertion + "\n");
         }
 
@@ -79,15 +80,16 @@ class ProblemSerializerTest {
                 var pred = createPred();
                 var node = ProblemFactory.eINSTANCE.createNode();
                 node.setName("a");
-                var individualDeclaration = ProblemFactory.eINSTANCE.createIndividualDeclaration();
-                individualDeclaration.getNodes().add(node);
-                problem.getStatements().add(individualDeclaration);
+                var atomDeclaration = ProblemFactory.eINSTANCE.createNodeDeclaration();
+                atomDeclaration.setKind(NodeKind.ATOM);
+                atomDeclaration.getNodes().add(node);
+                problem.getStatements().add(atomDeclaration);
                 createAssertion(pred, node, value, true);
 
                 assertSerializedResult("""
                                 pred foo(node p).
 
-                                indiv a.
+                                atom a.
                                 default\040""" + serializedAssertion + "\n");
         }
 
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 {
                         "exists(n).",
                         "?exists(n).",
                         "!exists(n).",
-                        "exists(*).",
                         "?exists(*).",
                         "exists(Foo::new).",
                         "?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 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.tests.validation;
+
+import com.google.inject.Inject;
+import org.eclipse.xtext.testing.InjectWith;
+import org.eclipse.xtext.testing.extensions.InjectionExtension;
+import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.extension.ExtendWith;
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.Arguments;
+import org.junit.jupiter.params.provider.MethodSource;
+import tools.refinery.language.model.tests.utils.ProblemParseHelper;
+import tools.refinery.language.tests.ProblemInjectorProvider;
+import tools.refinery.language.validation.ProblemValidator;
+
+import java.util.stream.Stream;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.*;
+
+@ExtendWith(InjectionExtension.class)
+@InjectWith(ProblemInjectorProvider.class)
+class ModuleValidationTest {
+        @Inject
+        private ProblemParseHelper parseHelper;
+
+        @ParameterizedTest
+        @MethodSource
+        void invalidMultiObjectExistsTest(String invalidDeclaration) {
+                var problem = parseHelper.parse("""
+                                module.
+
+                                %s
+                                """.formatted(invalidDeclaration));
+                var issues = problem.validate();
+                assertThat(issues, hasItem(hasProperty("issueCode",
+                                is(ProblemValidator.UNSUPPORTED_ASSERTION_ISSUE))));
+        }
+
+        static Stream<Arguments> invalidMultiObjectExistsTest() {
+                return Stream.of(
+                                Arguments.of("""
+                                                class Foo.
+                                                exists(Foo::new).
+                                                """),
+                                Arguments.of("""
+                                                multi m.
+                                                exists(m).
+                                                """));
+        }
+
+        @Test
+        void invalidScopeTest() {
+                var problem = parseHelper.parse("""
+                                module.
+
+                                class Foo.
+                                scope Foo += 1.
+                                """);
+                var issues = problem.validate();
+                assertThat(issues, hasItem(hasProperty("issueCode",
+                                is(ProblemValidator.INVALID_MULTIPLICITY_ISSUE))));
+        }
+
+        @Test
+        void invalidAssertionArgumentTest() {
+                var problem = parseHelper.parse("""
+                                module.
+
+                                class Foo.
+                                Foo(foo1).
+                                """);
+                var issues = problem.validate();
+                assertThat(issues, hasItem(allOf(
+                                hasProperty("issueCode", is(ProblemValidator.UNSUPPORTED_ASSERTION_ISSUE)),
+                                hasProperty("message", containsString("foo1")))));
+        }
+
+        @ParameterizedTest
+        @MethodSource
+        void validDeclarationTest(String validDeclaration) {
+                var problem = parseHelper.parse(validDeclaration);
+                var issues = problem.validate();
+                assertThat(issues, hasSize(0));
+        }
+
+        static Stream<Arguments> validDeclarationTest() {
+                return Stream.concat(
+                                invalidMultiObjectExistsTest(),
+                                Stream.of(
+                                                Arguments.of("""
+                                                                class Foo.
+                                                                scope Foo += 1.
+                                                                """),
+                                                Arguments.of("""
+                                                                module.
+
+                                                                class Foo.
+                                                                scope Foo = 1.
+                                                                """),
+                                                Arguments.of("""
+                                                                class Foo.
+                                                                Foo(foo1).
+                                                                """),
+                                                Arguments.of("""
+                                                                module.
+
+                                                                class Foo.
+                                                                multi foo1.
+                                                                Foo(foo1).
+                                                                """),
+                                                Arguments.of("""
+                                                                module.
+
+                                                                class Foo.
+                                                                atom foo1.
+                                                                Foo(foo1).
+                                                                """),
+                                                Arguments.of("""
+                                                                module.
+
+                                                                class Foo.
+                                                                declare foo1.
+                                                                Foo(foo1).
+                                                                """),
+                                                Arguments.of("""
+                                                                module.
+
+                                                                enum Foo { foo1 }
+                                                                Foo(foo1).
+                                                                """),
+                                                Arguments.of("""
+                                                                module.
+
+                                                                class Foo.
+                                                                Foo(Foo::new).
+                                                                """)
+                                )
+                );
+        }
+}