feat(language): numeric expressions

8 files changed, 261 insertions, 57 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 1e8682a3..3a6e015f 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
@@ -1,17 +1,15 @@
 package tools.refinery.language.tests;
 
-import static org.hamcrest.MatcherAssert.assertThat;
-import static org.hamcrest.Matchers.empty;
-
+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 com.google.inject.Inject;
-
 import tools.refinery.language.model.tests.utils.ProblemParseHelper;
 
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.empty;
+
 @ExtendWith(InjectionExtension.class)
 @InjectWith(ProblemInjectorProvider.class)
 class ProblemParsingTest {
@@ -40,7 +38,7 @@ class ProblemParsingTest {
                                 error invalidTaxStatus(Person p) <->
                                         taxStatus(p, child), children(p, _q).
 
-                                indiv family.
+                                individual 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 083c5184..a6e38130 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
@@ -1,10 +1,7 @@
 package tools.refinery.language.tests.formatting2;
 
-import static org.hamcrest.MatcherAssert.assertThat;
-import static org.hamcrest.Matchers.equalTo;
-
-import java.util.List;
-
+import com.google.inject.Inject;
+import com.google.inject.Provider;
 import org.eclipse.xtext.formatting2.FormatterRequest;
 import org.eclipse.xtext.formatting2.IFormatter2;
 import org.eclipse.xtext.formatting2.regionaccess.ITextRegionAccess;
@@ -16,13 +13,14 @@ import org.eclipse.xtext.testing.extensions.InjectionExtension;
 import org.eclipse.xtext.testing.util.ParseHelper;
 import org.junit.jupiter.api.Test;
 import org.junit.jupiter.api.extension.ExtendWith;
-
-import com.google.inject.Inject;
-import com.google.inject.Provider;
-
 import tools.refinery.language.model.problem.Problem;
 import tools.refinery.language.tests.ProblemInjectorProvider;
 
+import java.util.List;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.equalTo;
+
 @ExtendWith(InjectionExtension.class)
 @InjectWith(ProblemInjectorProvider.class)
 class ProblemFormatterTest {
@@ -181,7 +179,7 @@ class ProblemFormatterTest {
 
         @Test
         void individualDeclarationTest() {
-                testFormatter("  indiv  a  ,  b  .  ", "indiv a, b.\n");
+                testFormatter("  individual  a  ,  b  .  ", "individual a, b.\n");
         }
 
         @Test
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/parser/antlr/IdentifierTokenProviderTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/parser/antlr/IdentifierTokenProviderTest.java
new file mode 100644
index 00000000..abff8d9c
--- /dev/null
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/parser/antlr/IdentifierTokenProviderTest.java
@@ -0,0 +1,39 @@
+package tools.refinery.language.tests.parser.antlr;
+
+import com.google.inject.Inject;
+import org.eclipse.xtext.testing.InjectWith;
+import org.eclipse.xtext.testing.extensions.InjectionExtension;
+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.parser.antlr.IdentifierTokenProvider;
+import tools.refinery.language.parser.antlr.internal.InternalProblemParser;
+import tools.refinery.language.tests.ProblemInjectorProvider;
+
+import java.util.stream.Stream;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.equalTo;
+
+@ExtendWith(InjectionExtension.class)
+@InjectWith(ProblemInjectorProvider.class)
+class IdentifierTokenProviderTest {
+        @Inject
+        private IdentifierTokenProvider identifierTokenProvider;
+
+        @ParameterizedTest(name = "{0} is identifier: {2}")
+        @MethodSource
+        void isIdentifierTokenTest(String ignoredTokenName, int tokenId, boolean expected) {
+                assertThat(identifierTokenProvider.isIdentifierToken(tokenId), equalTo(expected));
+        }
+
+        static Stream<Arguments> isIdentifierTokenTest() {
+                return Stream.of(
+                                Arguments.of("RULE_ID", InternalProblemParser.RULE_ID, true),
+                                Arguments.of("contained", InternalProblemParser.Contained, true),
+                                Arguments.of("contains", InternalProblemParser.Contains, true),
+                                Arguments.of("(", InternalProblemParser.LeftParenthesis, false)
+                );
+        }
+}
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/parser/antlr/ProblemTokenSourceTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/parser/antlr/ProblemTokenSourceTest.java
new file mode 100644
index 00000000..cb42d5d0
--- /dev/null
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/parser/antlr/ProblemTokenSourceTest.java
@@ -0,0 +1,134 @@
+package tools.refinery.language.tests.parser.antlr;
+
+import com.google.inject.Inject;
+import com.google.inject.Provider;
+import com.google.inject.name.Named;
+import org.antlr.runtime.ANTLRStringStream;
+import org.antlr.runtime.Token;
+import org.eclipse.xtext.parser.antlr.Lexer;
+import org.eclipse.xtext.parser.antlr.LexerBindings;
+import org.eclipse.xtext.testing.InjectWith;
+import org.eclipse.xtext.testing.extensions.InjectionExtension;
+import org.hamcrest.Matcher;
+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 org.junit.jupiter.params.provider.ValueSource;
+import tools.refinery.language.parser.antlr.IdentifierTokenProvider;
+import tools.refinery.language.parser.antlr.ProblemTokenSource;
+import tools.refinery.language.parser.antlr.internal.InternalProblemParser;
+import tools.refinery.language.tests.ProblemInjectorProvider;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.stream.Stream;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.*;
+
+@ExtendWith(InjectionExtension.class)
+@InjectWith(ProblemInjectorProvider.class)
+class ProblemTokenSourceTest {
+        @Inject
+        @Named(LexerBindings.RUNTIME)
+        private Provider<Lexer> lexerProvider;
+
+        @Inject
+        private IdentifierTokenProvider identifierTokenProvider;
+
+        @ParameterizedTest
+        @ValueSource(strings = {
+                        "a+b",
+                        "a+(b)",
+                        "a+(b(x, y), x)",
+                        "a + (b)",
+                        "a+(b::x)",
+                        "c+(a+(b)",
+                        "a+(1, b)",
+                        // These are never valid expressions, so we do try to peek at the inner plus sign
+                        // to limit recursion depth in the token source:
+                        "c+(equals+(a, b))",
+                        "equals+(equals+(a, b), c)",
+        })
+        void plusSignInTokenStreamTest(String text) {
+                var tokenList = createTokenList(text);
+                assertThat(tokenList, hasTokenOfType(InternalProblemParser.PlusSign));
+                assertThat(tokenList, not(hasTokenOfType(InternalProblemParser.RULE_TRANSITIVE_CLOSURE)));
+        }
+
+        @ParameterizedTest
+        @ValueSource(strings = {
+                        "equals+(a, b)",
+                        "equals + (a, b)",
+                        "equals+(a::x, b)"
+        })
+        void transitiveClosureInTokenStreamTest(String text) {
+                var tokenList = createTokenList(text);
+                assertThat(tokenList, not(hasTokenOfType(InternalProblemParser.PlusSign)));
+                assertThat(tokenList, hasTokenOfType(InternalProblemParser.RULE_TRANSITIVE_CLOSURE));
+        }
+
+        @ParameterizedTest
+        @MethodSource
+        void plusAndTransitiveClosureInSameTokenStreamTest(String text, boolean recursive) {
+                var tokenSource = createTokenSource(text);
+                tokenSource.setRecursive(recursive);
+                Token token;
+                int i = 0;
+                int plusIndex = -1;
+                int transitiveClosureIndex = -1;
+                do {
+                        token = tokenSource.nextToken();
+                        switch (token.getType()) {
+                        case InternalProblemParser.PlusSign -> {
+                                assertThat("multiple plus signs", plusIndex, equalTo(-1));
+                                plusIndex = i;
+                        }
+                        case InternalProblemParser.RULE_TRANSITIVE_CLOSURE -> {
+                                assertThat("multiple transitive closures", transitiveClosureIndex, equalTo(-1));
+                                transitiveClosureIndex = i;
+                        }
+                        }
+                        i++;
+                } while (token.getType() != InternalProblemParser.EOF);
+                assertThat("no plus sign", plusIndex, not(equalTo(-1)));
+                assertThat("no transitive closure", transitiveClosureIndex, not(equalTo(-1)));
+                assertThat("transitive closure before plus", transitiveClosureIndex, greaterThan(plusIndex));
+        }
+
+        static Stream<Arguments> plusAndTransitiveClosureInSameTokenStreamTest() {
+                return Stream.of(
+                                Arguments.of("c+(d), equals+(a, b)", false),
+                                Arguments.of("foo+(bar baz+(a, b))", false),
+                                // Here we can peek at the inner plus sign without recursion:
+                                Arguments.of("c+(1, equals+(a, b))", false),
+                                // But these cases need recursion:
+                                Arguments.of("c+(equals+(a, b))", true),
+                                Arguments.of("equals+(equals+(a, b), c)", true)
+                );
+        }
+
+        private ProblemTokenSource createTokenSource(String text) {
+                var lexer = lexerProvider.get();
+                lexer.setCharStream(new ANTLRStringStream(text));
+                var tokenSource = new ProblemTokenSource(lexer);
+                tokenSource.setIdentifierTokenProvider(identifierTokenProvider);
+                return tokenSource;
+        }
+
+        private List<Token> createTokenList(String text) {
+                var tokenSource = createTokenSource(text);
+                var tokens = new ArrayList<Token>();
+                Token token;
+                do {
+                        token = tokenSource.nextToken();
+                        tokens.add(token);
+                } while (token.getType() != InternalProblemParser.EOF);
+                return tokens;
+        }
+
+        private Matcher<Iterable<? super Token>> hasTokenOfType(int tokenId) {
+                return hasItem(hasProperty("type", equalTo(tokenId)));
+        }
+}
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/parser/antlr/TransitiveClosureParserTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/parser/antlr/TransitiveClosureParserTest.java
new file mode 100644
index 00000000..96d12edf
--- /dev/null
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/parser/antlr/TransitiveClosureParserTest.java
@@ -0,0 +1,49 @@
+package tools.refinery.language.tests.parser.antlr;
+
+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 tools.refinery.language.model.problem.ArithmeticBinaryExpr;
+import tools.refinery.language.model.problem.Atom;
+import tools.refinery.language.model.problem.BinaryOp;
+import tools.refinery.language.model.problem.ComparisonExpr;
+import tools.refinery.language.model.tests.utils.ProblemParseHelper;
+import tools.refinery.language.tests.ProblemInjectorProvider;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.*;
+
+@ExtendWith(InjectionExtension.class)
+@InjectWith(ProblemInjectorProvider.class)
+class TransitiveClosureParserTest {
+        @Inject
+        private ProblemParseHelper parseHelper;
+
+        @Test
+        void binaryAddOperatorTest() {
+                var problem = parseHelper.parse("""
+                                        pred foo(int a, int b) <-> a + (b) > 10.
+                                """);
+                assertThat(problem.errors(), empty());
+                var literal = problem.pred("foo").conj(0).lit(0).get();
+                assertThat(literal, instanceOf(ComparisonExpr.class));
+                var left = ((ComparisonExpr) literal).getLeft();
+                assertThat(left, instanceOf(ArithmeticBinaryExpr.class));
+                var binary = (ArithmeticBinaryExpr) left;
+                assertThat(binary.getOp(), equalTo(BinaryOp.ADD));
+        }
+
+        @Test
+        void transitiveClosureTest() {
+                var problem = parseHelper.parse("""
+                                        pred foo(a, b) <-> equals+(a, b).
+                                """);
+                assertThat(problem.errors(), empty());
+                var literal = problem.pred("foo").conj(0).lit(0).get();
+                assertThat(literal, instanceOf(Atom.class));
+                var atom = (Atom) literal;
+                assertThat(atom.isTransitiveClosure(), equalTo(true));
+        }
+}
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 5c905ede..9049b8ec 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,13 +1,6 @@
 package tools.refinery.language.tests.scoping;
 
-import static org.hamcrest.MatcherAssert.assertThat;
-import static org.hamcrest.Matchers.empty;
-import static org.hamcrest.Matchers.equalTo;
-import static org.hamcrest.Matchers.hasItems;
-import static org.hamcrest.Matchers.not;
-
-import java.util.stream.Stream;
-
+import com.google.inject.Inject;
 import org.eclipse.xtext.testing.InjectWith;
 import org.eclipse.xtext.testing.extensions.InjectionExtension;
 import org.junit.jupiter.api.Test;
@@ -16,13 +9,15 @@ import org.junit.jupiter.params.ParameterizedTest;
 import org.junit.jupiter.params.provider.Arguments;
 import org.junit.jupiter.params.provider.MethodSource;
 import org.junit.jupiter.params.provider.ValueSource;
-
-import com.google.inject.Inject;
-
 import tools.refinery.language.model.tests.utils.ProblemParseHelper;
 import tools.refinery.language.model.tests.utils.WrappedProblem;
 import tools.refinery.language.tests.ProblemInjectorProvider;
 
+import java.util.stream.Stream;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.*;
+
 @ExtendWith(InjectionExtension.class)
 @InjectWith(ProblemInjectorProvider.class)
 class NodeScopingTest {
@@ -85,7 +80,7 @@ class NodeScopingTest {
         @MethodSource("individualNodeReferenceSource")
         void individualNodeInAssertionTest(String qualifiedNamePrefix, boolean namedProblem) {
                 var problem = parse("""
-                                indiv a, b.
+                                individual a, b.
                                 pred predicate(node x, node y) <-> node(x).
                                 predicate({PARAM}a, {PARAM}a).
                                 ?predicate({PARAM}a, {PARAM}b).
@@ -102,7 +97,7 @@ class NodeScopingTest {
         @MethodSource("individualNodeReferenceSource")
         void individualNodeInNodeValueAssertionTest(String qualifiedNamePrefix, boolean namedProblem) {
                 var problem = parse("""
-                                indiv a.
+                                individual a.
                                 {PARAM}a: 16.
                                 """, qualifiedNamePrefix, namedProblem);
                 assertThat(problem.errors(), empty());
@@ -114,7 +109,7 @@ class NodeScopingTest {
         @MethodSource("individualNodeReferenceSource")
         void individualNodeInPredicateTest(String qualifiedNamePrefix, boolean namedProblem) {
                 var problem = parse("""
-                                indiv b.
+                                individual b.
                                 pred predicate(node a) <-> node({PARAM}b).
                                 """);
                 assertThat(problem.errors(), empty());
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 ea858e92..150e47a4 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
@@ -1,13 +1,6 @@
 package tools.refinery.language.tests.serializer;
 
-import static org.hamcrest.MatcherAssert.assertThat;
-import static org.hamcrest.Matchers.equalTo;
-
-import java.io.ByteArrayOutputStream;
-import java.io.IOException;
-import java.util.Map;
-import java.util.stream.Stream;
-
+import com.google.inject.Inject;
 import org.eclipse.emf.common.util.URI;
 import org.eclipse.emf.ecore.resource.Resource;
 import org.eclipse.emf.ecore.resource.ResourceSet;
@@ -19,20 +12,18 @@ 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 com.google.inject.Inject;
-
-import tools.refinery.language.model.problem.Atom;
-import tools.refinery.language.model.problem.LogicValue;
-import tools.refinery.language.model.problem.Node;
-import tools.refinery.language.model.problem.PredicateDefinition;
-import tools.refinery.language.model.problem.Problem;
-import tools.refinery.language.model.problem.ProblemFactory;
-import tools.refinery.language.model.problem.Relation;
-import tools.refinery.language.model.problem.VariableOrNode;
+import tools.refinery.language.model.problem.*;
 import tools.refinery.language.model.tests.utils.WrappedProblem;
 import tools.refinery.language.tests.ProblemInjectorProvider;
 
+import java.io.ByteArrayOutputStream;
+import java.io.IOException;
+import java.util.Map;
+import java.util.stream.Stream;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.equalTo;
+
 @ExtendWith(InjectionExtension.class)
 @InjectWith(ProblemInjectorProvider.class)
 class ProblemSerializerTest {
@@ -68,7 +59,7 @@ class ProblemSerializerTest {
                 assertSerializedResult("""
                                 pred foo(node p).
 
-                                indiv a.
+                                individual a.
                                 """ + serializedAssertion + "\n");
         }
 
@@ -166,10 +157,10 @@ class ProblemSerializerTest {
         private Atom createAtom(Relation relation, VariableOrNode variable1, VariableOrNode variable2) {
                 var atom = ProblemFactory.eINSTANCE.createAtom();
                 atom.setRelation(relation);
-                var arg1 = ProblemFactory.eINSTANCE.createVariableOrNodeArgument();
+                var arg1 = ProblemFactory.eINSTANCE.createVariableOrNodeExpr();
                 arg1.setVariableOrNode(variable1);
                 atom.getArguments().add(arg1);
-                var arg2 = ProblemFactory.eINSTANCE.createVariableOrNodeArgument();
+                var arg2 = ProblemFactory.eINSTANCE.createVariableOrNodeExpr();
                 arg2.setVariableOrNode(variable2);
                 atom.getArguments().add(arg2);
                 return atom;
@@ -188,10 +179,10 @@ class ProblemSerializerTest {
                 var atom = ProblemFactory.eINSTANCE.createAtom();
                 var equals = nodeType.reference("equals");
                 atom.setRelation(equals);
-                var arg1 = ProblemFactory.eINSTANCE.createVariableOrNodeArgument();
+                var arg1 = ProblemFactory.eINSTANCE.createVariableOrNodeExpr();
                 arg1.setVariableOrNode(parameter);
                 atom.getArguments().add(arg1);
-                var arg2 = ProblemFactory.eINSTANCE.createVariableOrNodeArgument();
+                var arg2 = ProblemFactory.eINSTANCE.createVariableOrNodeExpr();
                 var variable = ProblemFactory.eINSTANCE.createImplicitVariable();
                 variable.setName("_q");
                 arg2.setSingletonVariable(variable);
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java
index a05f3335..98c16352 100644
--- a/subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java
@@ -44,7 +44,7 @@ class SymbolCollectorTest {
         @Test
         void individualNodeTest() {
                 var problem = parseHelper.parse("""
-                                indiv a.
+                                individual a.
                                 """);
                 var collectedSymbols = desugarer.collectSymbols(problem.get());
                 var node = problem.individualNode("a");
@@ -161,7 +161,7 @@ class SymbolCollectorTest {
 
         static Stream<Arguments> predicateTest() {
                 return Stream.of(Arguments.of("pred", ContainmentRole.NONE), Arguments.of("error", ContainmentRole.NONE),
-                                Arguments.of("contained", ContainmentRole.CONTAINED), Arguments.of("containment",
+                                Arguments.of("contained pred", ContainmentRole.CONTAINED), Arguments.of("containment pred",
                                                 ContainmentRole.CONTAINMENT));
         }