feat(lang): basic formatting

Adds support for formatting some elements without any indentation.
Mostly for testing model serialization with some human-readable
formatting instead of just space-separating the tokens.

Finishing the formatter to support all language constructs might be a
bit more difficult due to our Prolog-like indentation rules.

5 files changed, 454 insertions, 18 deletions

diff --git a/language/src/main/java/tools/refinery/language/GenerateProblem.mwe2 b/language/src/main/java/tools/refinery/language/GenerateProblem.mwe2
index 58620d6a..0d934b68 100644
--- a/language/src/main/java/tools/refinery/language/GenerateProblem.mwe2
+++ b/language/src/main/java/tools/refinery/language/GenerateProblem.mwe2
@@ -39,6 +39,9 @@ Workflow {
                         serializer = {
                                 generateStub = false
                         }
+                        formatter = {
+                                generateStub = true
+                        }
                         validator = {
                                 generateDeprecationValidation = true
                         }
diff --git a/language/src/main/java/tools/refinery/language/Problem.xtext b/language/src/main/java/tools/refinery/language/Problem.xtext
index 26773047..c94d40ab 100644
--- a/language/src/main/java/tools/refinery/language/Problem.xtext
+++ b/language/src/main/java/tools/refinery/language/Problem.xtext
@@ -8,7 +8,8 @@ Problem:
         statements+=Statement*;
 
 Statement:
-        ClassDeclaration | EnumDeclaration | PredicateDefinition | RuleDefinition | Assertion | NodeValueAssertion | ScopeDeclaration |
+        ClassDeclaration | EnumDeclaration | PredicateDefinition | RuleDefinition | Assertion | NodeValueAssertion |
+        ScopeDeclaration |
         IndividualDeclaration;
 
 ClassDeclaration:
@@ -67,7 +68,7 @@ Literal:
 
 ValueLiteral:
         atom=Atom
-        (refinement?=":"|"=")
+        (refinement?=":" | "=")
         values+=LogicConstant ("|" values+=LogicConstant)*;
 
 NegativeLiteral:
@@ -78,7 +79,7 @@ ActionLiteral:
 
 ValueActionLiteral:
         atom=Atom
-        (refinement?=":"|"=")
+        (refinement?=":" | "=")
         value=LogicValue;
 
 DeleteActionLiteral:
@@ -86,7 +87,7 @@ DeleteActionLiteral:
 
 NewActionLiteral:
         "new" variable=NewVariable;
-        
+
 NewVariable:
         name=Identifier;
 
diff --git a/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java b/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java
new file mode 100644
index 00000000..903347f7
--- /dev/null
+++ b/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java
@@ -0,0 +1,183 @@
+/*
+ * generated by Xtext 2.26.0.M2
+ */
+package tools.refinery.language.formatting2;
+
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.xtext.formatting2.AbstractJavaFormatter;
+import org.eclipse.xtext.formatting2.IFormattableDocument;
+import org.eclipse.xtext.formatting2.IHiddenRegionFormatter;
+import org.eclipse.xtext.formatting2.regionaccess.ISemanticRegionsFinder;
+import org.eclipse.xtext.formatting2.regionaccess.ISequentialRegion;
+import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
+
+import tools.refinery.language.model.problem.Assertion;
+import tools.refinery.language.model.problem.Atom;
+import tools.refinery.language.model.problem.ClassDeclaration;
+import tools.refinery.language.model.problem.Conjunction;
+import tools.refinery.language.model.problem.IndividualDeclaration;
+import tools.refinery.language.model.problem.NegativeLiteral;
+import tools.refinery.language.model.problem.Parameter;
+import tools.refinery.language.model.problem.PredicateDefinition;
+import tools.refinery.language.model.problem.Problem;
+import tools.refinery.language.model.problem.ProblemPackage;
+
+public class ProblemFormatter extends AbstractJavaFormatter {
+
+        protected void format(Problem problem, IFormattableDocument doc) {
+                doc.prepend(problem, this::noSpace);
+                var region = regionFor(problem);
+                doc.append(region.keyword("problem"), this::oneSpace);
+                doc.prepend(region.keyword("."), this::noSpace);
+                appendNewLines(doc, region.keyword("."), this::twoNewLines);
+                for (var statement : problem.getStatements()) {
+                        doc.format(statement);
+                }
+        }
+
+        protected void format(Assertion assertion, IFormattableDocument doc) {
+                surroundNewLines(doc, assertion, this::singleNewLine);
+                var region = regionFor(assertion);
+                doc.append(region.feature(ProblemPackage.Literals.ASSERTION__DEFAULT), this::oneSpace);
+                doc.append(region.feature(ProblemPackage.Literals.ASSERTION__VALUE), this::noSpace);
+                doc.append(region.feature(ProblemPackage.Literals.ASSERTION__RELATION), this::noSpace);
+                formatParenthesizedList(region, doc);
+                doc.prepend(region.keyword(":"), this::noSpace);
+                doc.append(region.keyword(":"), this::oneSpace);
+                doc.prepend(region.keyword("."), this::noSpace);
+                for (var argument : assertion.getArguments()) {
+                        doc.format(argument);
+                }
+        }
+        
+        protected void format(ClassDeclaration classDeclaration, IFormattableDocument doc) {
+                surroundNewLines(doc, classDeclaration, this::twoNewLines);
+                var region = regionFor(classDeclaration);
+                doc.append(region.feature(ProblemPackage.Literals.CLASS_DECLARATION__ABSTRACT), this::oneSpace);
+                doc.append(region.keyword("class"), this::oneSpace);
+                doc.surround(region.keyword("extends"), this::oneSpace);
+                formatList(region, ",", doc);
+                doc.prepend(region.keyword("{"), this::oneSpace);
+                doc.append(region.keyword("{"), it -> it.setNewLines(1, 1, 2));
+                doc.prepend(region.keyword("}"), it -> it.setNewLines(1, 1, 2));
+                doc.prepend(region.keyword("."), this::noSpace);
+                for (var referenceDeclaration : classDeclaration.getReferenceDeclarations()) {
+                        doc.format(referenceDeclaration);
+                }
+        }
+
+        protected void format(PredicateDefinition predicateDefinition, IFormattableDocument doc) {
+                surroundNewLines(doc, predicateDefinition, this::twoNewLines);
+                var region = regionFor(predicateDefinition);
+                doc.append(region.feature(ProblemPackage.Literals.PREDICATE_DEFINITION__KIND), this::oneSpace);
+                doc.append(region.keyword("pred"), this::oneSpace);
+                doc.append(region.feature(ProblemPackage.Literals.NAMED_ELEMENT__NAME), this::noSpace);
+                formatParenthesizedList(region, doc);
+                doc.surround(region.keyword("<->"), this::oneSpace);
+                formatList(region, ";", doc);
+                doc.prepend(region.keyword("."), this::noSpace);
+                for (var parameter : predicateDefinition.getParameters()) {
+                        doc.format(parameter);
+                }
+                for (var body : predicateDefinition.getBodies()) {
+                        doc.format(body);
+                }
+        }
+
+        protected void format(Parameter parameter, IFormattableDocument doc) {
+                doc.append(regionFor(parameter).feature(ProblemPackage.Literals.PARAMETER__PARAMETER_TYPE), this::oneSpace);
+        }
+
+        protected void format(Conjunction conjunction, IFormattableDocument doc) {
+                var region = regionFor(conjunction);
+                formatList(region, ",", doc);
+                for (var literal : conjunction.getLiterals()) {
+                        doc.format(literal);
+                }
+        }
+
+        protected void format(NegativeLiteral literal, IFormattableDocument doc) {
+                var region = regionFor(literal);
+                doc.append(region.keyword("!"), this::noSpace);
+                doc.format(literal.getAtom());
+        }
+
+        protected void format(Atom atom, IFormattableDocument doc) {
+                var region = regionFor(atom);
+                doc.append(region.feature(ProblemPackage.Literals.ATOM__RELATION), this::noSpace);
+                doc.append(region.feature(ProblemPackage.Literals.ATOM__TRANSITIVE_CLOSURE), this::noSpace);
+                formatParenthesizedList(region, doc);
+                for (var argument : atom.getArguments()) {
+                        doc.format(argument);
+                }
+        }
+
+        protected void format(IndividualDeclaration individualDeclaration, IFormattableDocument doc) {
+                surroundNewLines(doc, individualDeclaration, this::singleNewLine);
+                var region = regionFor(individualDeclaration);
+                doc.append(region.keyword("indiv"), this::oneSpace);
+                formatList(region, ",", doc);
+                doc.prepend(region.keyword("."), this::noSpace);
+        }
+
+        protected void formatParenthesizedList(ISemanticRegionsFinder region, IFormattableDocument doc) {
+                doc.append(region.keyword("("), this::noSpace);
+                doc.prepend(region.keyword(")"), this::noSpace);
+                formatList(region, ",", doc);
+        }
+
+        protected void formatList(ISemanticRegionsFinder region, String separator, IFormattableDocument doc) {
+                for (var comma : region.keywords(separator)) {
+                        doc.prepend(comma, this::noSpace);
+                        doc.append(comma, this::oneSpace);
+                }
+        }
+
+        protected void singleNewLine(IHiddenRegionFormatter it) {
+                it.setNewLines(1, 1, 2);
+        }
+
+        protected void twoNewLines(IHiddenRegionFormatter it) {
+                it.highPriority();
+                it.setNewLines(2);
+        }
+
+        protected void surroundNewLines(IFormattableDocument doc, EObject eObject,
+                        Procedure1<? super IHiddenRegionFormatter> init) {
+                var region = doc.getRequest().getTextRegionAccess().regionForEObject(eObject);
+                preprendNewLines(doc, region, init);
+                appendNewLines(doc, region, init);
+        }
+
+        protected void preprendNewLines(IFormattableDocument doc, ISequentialRegion region,
+                        Procedure1<? super IHiddenRegionFormatter> init) {
+                if (region == null) {
+                        return;
+                }
+                var previousHiddenRegion = region.getPreviousHiddenRegion();
+                if (previousHiddenRegion == null) {
+                        return;
+                }
+                if (previousHiddenRegion.getPreviousSequentialRegion() == null) {
+                        doc.set(previousHiddenRegion, it -> it.setNewLines(0));
+                } else {
+                        doc.set(previousHiddenRegion, init);
+                }
+        }
+
+        protected void appendNewLines(IFormattableDocument doc, ISequentialRegion region,
+                        Procedure1<? super IHiddenRegionFormatter> init) {
+                if (region == null) {
+                        return;
+                }
+                var nextHiddenRegion = region.getNextHiddenRegion();
+                if (nextHiddenRegion == null) {
+                        return;
+                }
+                if (nextHiddenRegion.getNextSequentialRegion() == null) {
+                        doc.set(nextHiddenRegion, it -> it.setNewLines(1));
+                } else {
+                        doc.set(nextHiddenRegion, init);
+                }
+        }
+}
diff --git a/language/src/test/java/tools/refinery/language/tests/formatting2/ProblemFormatterTest.java b/language/src/test/java/tools/refinery/language/tests/formatting2/ProblemFormatterTest.java
new file mode 100644
index 00000000..854c3da1
--- /dev/null
+++ b/language/src/test/java/tools/refinery/language/tests/formatting2/ProblemFormatterTest.java
@@ -0,0 +1,235 @@
+package tools.refinery.language.tests.formatting2;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.equalTo;
+
+import java.util.List;
+
+import org.eclipse.xtext.formatting2.FormatterRequest;
+import org.eclipse.xtext.formatting2.IFormatter2;
+import org.eclipse.xtext.formatting2.regionaccess.ITextRegionAccess;
+import org.eclipse.xtext.formatting2.regionaccess.ITextReplacement;
+import org.eclipse.xtext.formatting2.regionaccess.TextRegionAccessBuilder;
+import org.eclipse.xtext.resource.XtextResource;
+import org.eclipse.xtext.testing.InjectWith;
+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;
+
+@ExtendWith(InjectionExtension.class)
+@InjectWith(ProblemInjectorProvider.class)
+class ProblemFormatterTest {
+        @Inject
+        private ParseHelper<Problem> parseHelper;
+
+        @Inject
+        private Provider<FormatterRequest> formatterRequestProvider;
+
+        @Inject
+        private TextRegionAccessBuilder regionBuilder;
+
+        @Inject
+        private IFormatter2 formatter2;
+
+        @Test
+        void problemNameTest() {
+                testFormatter("  problem  problem  .  ", "problem problem.\n");
+        }
+
+        @Test
+        void assertionTest() {
+                testFormatter("  equals (  a  ,  b  ,  *  )  :  true  .  ", "equals(a, b, *): true.\n");
+        }
+
+        @Test
+        void defaultAssertionTest() {
+                testFormatter("  default  equals (  a  ,  b  ,  *  )  :  true  .  ", "default equals(a, b, *): true.\n");
+        }
+
+        @Test
+        void assertionShortTrueTest() {
+                testFormatter("  equals (  a  ,  b  ,  *  )  .  ", "equals(a, b, *).\n");
+        }
+
+        @Test
+        void defaultAssertionShortTrueTest() {
+                testFormatter("  default  equals (  a  ,  b  ,  *  )  .  ", "default equals(a, b, *).\n");
+        }
+
+        @Test
+        void assertionShortFalseTest() {
+                testFormatter("  !  equals (  a  ,  b  ,  *  )  .  ", "!equals(a, b, *).\n");
+        }
+
+        @Test
+        void defaultAssertionShortFalseTest() {
+                testFormatter("  default  !  equals (  a  ,  b  ,  *  )  .  ", "default !equals(a, b, *).\n");
+        }
+
+        @Test
+        void assertionShortUnknownTest() {
+                testFormatter("  ?  equals (  a  ,  b  ,  *  )  .  ", "?equals(a, b, *).\n");
+        }
+
+        @Test
+        void defaultAssertionShortUnknownTest() {
+                testFormatter("  default  ?  equals (  a  ,  b  ,  *  )  .  ", "default ?equals(a, b, *).\n");
+        }
+
+        @Test
+        void multipleAssertionsTest() {
+                testFormatter("  exists (  a  )  .  ?  equals  (  a  ,  a  ).", """
+                                exists(a).
+                                ?equals(a, a).
+                                """);
+        }
+
+        @Test
+        void multipleAssertionsNamedProblemTest() {
+                testFormatter("  problem  foo  .  exists (  a  )  .  ?  equals  (  a  ,  a  ).", """
+                                problem foo.
+
+                                exists(a).
+                                ?equals(a, a).
+                                """);
+        }
+
+        @Test
+        void classWithoutBodyTest() {
+                testFormatter("  class  Foo  .  ", "class Foo.\n");
+        }
+        
+        @Test
+        void abstractClassWithoutBodyTest() {
+                testFormatter("  abstract  class  Foo  .  ", "abstract class Foo.\n");
+        }
+        
+        @Test
+        void classExtendsWithoutBodyTest() {
+                testFormatter("  class  Foo.  class  Bar  .  class  Quux  extends  Foo  ,  Bar  .  ", """
+                                class Foo.
+                                
+                                class Bar.
+                                
+                                class Quux extends Foo, Bar.
+                                """);
+        }
+
+        @Test
+        void classWithEmptyBodyTest() {
+                testFormatter("  class  Foo  {  }  ", """
+                                class Foo {
+                                }
+                                """);
+        }
+
+        @Test
+        void classExtendsWithBodyTest() {
+                testFormatter("  class  Foo.  class  Bar  .  class  Quux  extends  Foo  ,  Bar  {  }  ", """
+                                class Foo.
+                                
+                                class Bar.
+                                
+                                class Quux extends Foo, Bar {
+                                }
+                                """);
+        }
+
+        @Test
+        void predicateWithoutBodyTest() {
+                testFormatter("  pred  foo  (  node  a  ,  b  )  .  ", "pred foo(node a, b).\n");
+        }
+
+        @Test
+        void predicateWithBodyTest() {
+                testFormatter(
+                                "  pred  foo  (  node  a  ,  b  )  <->  equal  (a  ,  _c  )  ,  !  equal  (  a  ,  b  )  ;  equal+(  a  ,  b  )  .  ",
+                                "pred foo(node a, b) <-> equal(a, _c), !equal(a, b); equal+(a, b).\n");
+        }
+
+        @Test
+        void predicatesWithoutBodyTest() {
+                testFormatter("  pred  foo  (  node  a  ,  b  )  .  pred  bar  (  node  c  )  .  ", """
+                                pred foo(node a, b).
+
+                                pred bar(node c).
+                                """);
+        }
+
+        @Test
+        void predicateCommentsTest() {
+                testFormatter("""
+                                  % Some foo
+                                pred  foo  (  node  a  ,  b  )  .
+                                  % Some bar
+                                pred  bar  (  node  c  )  .
+                                """, """
+                                % Some foo
+                                pred foo(node a, b).
+
+                                % Some bar
+                                pred bar(node c).
+                                """);
+        }
+
+        @Test
+        void individualDeclarationTest() {
+                testFormatter("  indiv  a  ,  b  .  ", "indiv a, b.\n");
+        }
+
+        @Test
+        void mixedDeclarationsTest() {
+                testFormatter("""
+                                problem test.
+                                pred foo(node a).
+                                class Foo.
+                                foo(n1, n2).
+                                indiv i1.
+                                !foo(i1, n1).
+                                pred bar(node a, node b).
+                                pred quux().
+                                default !bar(*, *).
+                                """, """
+                                problem test.
+
+                                pred foo(node a).
+                                
+                                class Foo.
+
+                                foo(n1, n2).
+                                indiv i1.
+                                !foo(i1, n1).
+
+                                pred bar(node a, node b).
+
+                                pred quux().
+
+                                default !bar(*, *).
+                                """);
+        }
+
+        private void testFormatter(String toFormat, String expected) {
+                Problem problem;
+                try {
+                        problem = parseHelper.parse(toFormat);
+                } catch (Exception e) {
+                        throw new RuntimeException("Failed to parse document", e);
+                }
+                var resource = (XtextResource) problem.eResource();
+                FormatterRequest request = formatterRequestProvider.get();
+                request.setAllowIdentityEdits(false);
+                request.setFormatUndefinedHiddenRegionsOnly(false);
+                ITextRegionAccess regionAccess = regionBuilder.forNodeModel(resource).create();
+                request.setTextRegionAccess(regionAccess);
+                List<ITextReplacement> replacements = formatter2.format(request);
+                var formattedString = regionAccess.getRewriter().renderToString(replacements);
+                assertThat(formattedString, equalTo(expected));
+        }
+}
diff --git a/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java b/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java
index 22c79a09..ba3aaeb7 100644
--- a/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java
+++ b/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java
@@ -38,16 +38,16 @@ import tools.refinery.language.tests.ProblemInjectorProvider;
 @InjectWith(ProblemInjectorProvider.class)
 class ProblemSerializerTest {
         @Inject
-        ResourceSet resourceSet;
+        private ResourceSet resourceSet;
 
         @Inject
-        ProblemTestUtil testUtil;
+        private ProblemTestUtil testUtil;
 
-        Resource resource;
+        private Resource resource;
 
-        Problem problem;
+        private Problem problem;
 
-        Problem builtin;
+        private Problem builtin;
 
         @BeforeEach
         void beforeEach() {
@@ -68,14 +68,16 @@ class ProblemSerializerTest {
                 problem.getStatements().add(individualDeclaration);
                 createAssertion(pred, node, value);
 
-                assertSerializedResult("pred foo ( node p ) . indiv a . " + serializedAssertion);
+                assertSerializedResult("""
+                                pred foo(node p).
+
+                                indiv a.
+                                """ + serializedAssertion + "\n");
         }
 
         static Stream<Arguments> assertionTest() {
-                return Stream.of(Arguments.of(LogicValue.TRUE, "foo ( a ) ."),
-                                Arguments.of(LogicValue.FALSE, "! foo ( a ) ."),
-                                Arguments.of(LogicValue.UNKNOWN, "? foo ( a ) ."),
-                                Arguments.of(LogicValue.ERROR, "foo ( a ) : error ."));
+                return Stream.of(Arguments.of(LogicValue.TRUE, "foo(a)."), Arguments.of(LogicValue.FALSE, "!foo(a)."),
+                                Arguments.of(LogicValue.UNKNOWN, "?foo(a)."), Arguments.of(LogicValue.ERROR, "foo(a): error."));
         }
 
         @Test
@@ -86,7 +88,11 @@ class ProblemSerializerTest {
                 problem.getNodes().add(node);
                 createAssertion(pred, node);
 
-                assertSerializedResult("pred foo ( node p ) . foo ( a ) .");
+                assertSerializedResult("""
+                                pred foo(node p).
+
+                                foo(a).
+                                """);
         }
 
         private PredicateDefinition createPred() {
@@ -111,7 +117,11 @@ class ProblemSerializerTest {
                 problem.getStatements().add(classDeclaration);
                 createAssertion(classDeclaration, newNode);
 
-                assertSerializedResult("class Foo . Foo ( Foo::new ) .");
+                assertSerializedResult("""
+                                class Foo.
+
+                                Foo(Foo::new).
+                                """);
         }
 
         private void createAssertion(Relation relation, Node node) {
@@ -151,7 +161,9 @@ class ProblemSerializerTest {
                 pred.getBodies().add(conjunction);
                 problem.getStatements().add(pred);
 
-                assertSerializedResult("pred foo ( node p1 , node p2 ) <-> equals ( p1 , q ) , equals ( q , p2 ) .");
+                assertSerializedResult("""
+                                pred foo(node p1, node p2) <-> equals(p1, q), equals(q, p2).
+                                """);
         }
 
         private Atom createAtom(Relation relation, VariableOrNode variable1, VariableOrNode variable2) {
@@ -192,7 +204,9 @@ class ProblemSerializerTest {
                 pred.getBodies().add(conjunction);
                 problem.getStatements().add(pred);
 
-                assertSerializedResult("pred foo ( node p ) <-> equals ( p , _q ) .");
+                assertSerializedResult("""
+                                pred foo(node p) <-> equals(p, _q).
+                                """);
         }
 
         private void assertSerializedResult(String expected) {