refactor(language): simplify syntax

10 files changed, 64 insertions, 73 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 8b13a693..95a64737 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
+++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
@@ -33,7 +33,8 @@ enum ReferenceKind:
         REFERENCE="refers" | CONTAINMENT="contains" | CONTAINER="container";
 
 ReferenceDeclaration:
-        kind=ReferenceKind referenceType=[Relation|QualifiedName]
+        (referenceType=[Relation|NonContainmentQualifiedName] |
+        kind=ReferenceKind referenceType=[Relation|QualifiedName])
         ("[" multiplicity=Multiplicity "]")?
         name=Identifier
         ("opposite" opposite=[ReferenceDeclaration|QualifiedName])?;
@@ -64,7 +65,7 @@ Conjunction:
         literals+=Expr ("," literals+=Expr)*;
 
 FunctionDefinition:
-        functionType=PrimitiveType name=Identifier
+        "fn" functionType=PrimitiveType name=Identifier
         "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")"
         ("=" cases+=Case (";" cases+=Case)*)?
         ".";
@@ -106,7 +107,8 @@ Expr:
         ComparisonExpr;
 
 enum ComparisonOp:
-        LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | EQ="==" | NOT_EQ="!=" | IN="in";
+        LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | EQ="==" | NOT_EQ="!=" |
+        IN="in" | SUBSUMES=":>" | SUBSUMED_BY="<:" | ABS_EQ="===" | ABS_NOT_EQ="!==";
 
 ComparisonExpr returns Expr:
         LatticeExpr ({ComparisonExpr.left=current}
@@ -163,7 +165,7 @@ NegationExpr:
         "!" body=UnaryExpr;
 
 CountExpr:
-        "#" body=UnaryExpr;
+        "count" body=UnaryExpr;
 
 enum AggregationOp:
         SUM="sum" | PROD="prod" | MIN="min" | MAX="max";
@@ -180,7 +182,7 @@ VariableOrNodeExpr:
         variableOrNode=[VariableOrNode|QualifiedName];
 
 Constant:
-        RealConstant | IntConstant | InfConstant | StringConstant;
+        RealConstant | IntConstant | InfConstant | StringConstant | LogicConstant;
 
 IntConstant:
         intValue=INT;
@@ -194,12 +196,18 @@ InfConstant:
 StringConstant:
         stringValue=STRING;
 
+enum LogicValue:
+        TRUE="true" | FALSE="false" | UNKNOWN="unknown" | ERROR="error";
+
+LogicConstant:
+        logicValue=LogicValue;
+
 Assertion:
         default?="default"?
         (relation=[Relation|QualifiedName]
         "(" (arguments+=AssertionArgument ("," arguments+=AssertionArgument)*)? ")"
-        value=AssertionValue |
-        value=ShortLogicAssertionValue
+        ":" value=Expr |
+        value=ShortLogicConstant
         relation=[Relation|QualifiedName]
         "(" (arguments+=AssertionArgument ("," arguments+=AssertionArgument)*)? ")")
         ".";
@@ -213,23 +221,11 @@ NodeAssertionArgument:
 WildcardAssertionArgument:
         {WildcardAssertionArgument} "*";
 
-AssertionValue:
-        LogicAssertionValue | ExprAssertionValue;
-
-enum LogicValue:
-        TRUE="true" | FALSE="false" | UNKNOWN="unknown" | ERROR="error";
-
-LogicAssertionValue:
-        ":" logicValue=LogicValue;
-
-ExprAssertionValue:
-        (range?="in" | "=") body=Expr;
-
 enum ShortLogicValue returns LogicValue:
         FALSE="!" | UNKNOWN="?";
 
-ShortLogicAssertionValue returns LogicAssertionValue:
-        {LogicAssertionValue} logicValue=ShortLogicValue?;
+ShortLogicConstant returns LogicConstant:
+        {LogicConstant} logicValue=ShortLogicValue?;
 
 ScopeDeclaration:
         "scope" typeScopes+=TypeScope ("," typeScopes+=TypeScope)* ".";
@@ -255,7 +251,7 @@ ExactMultiplicity:
         exactValue=INT;
 
 IndividualDeclaration:
-        "individual" nodes+=EnumLiteral ("," nodes+=EnumLiteral)* ".";
+        "indiv" nodes+=EnumLiteral ("," nodes+=EnumLiteral)* ".";
 
 UpperBound returns ecore::EInt:
         INT | "*";
@@ -263,8 +259,14 @@ UpperBound returns ecore::EInt:
 QualifiedName hidden():
         Identifier ("::" Identifier)*;
 
+NonContainmentQualifiedName hidden():
+        NonContainmentIdentifier ("::" Identifier)*;
+
 Identifier:
-        ID | "contains" | "contained" | "sum" | "prod" | "min" | "max";
+        NonContainmentIdentifier | "contains";
+
+NonContainmentIdentifier:
+        ID | "contained" | "sum" | "prod" | "min" | "max";
 
 Real returns ecore::EDouble:
         EXPONENTIAL | INT "." (INT | EXPONENTIAL);
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 46870edb..797535ea 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
@@ -3,7 +3,6 @@
  */
 package tools.refinery.language.formatting2;
 
-import com.google.inject.Inject;
 import org.eclipse.emf.ecore.EObject;
 import org.eclipse.xtext.formatting2.AbstractJavaFormatter;
 import org.eclipse.xtext.formatting2.IFormattableDocument;
@@ -11,15 +10,10 @@ 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.*;
-import tools.refinery.language.services.ProblemGrammarAccess;
 
 @SuppressWarnings("UnstableApiUsage")
 public class ProblemFormatter extends AbstractJavaFormatter {
-        @Inject
-        private ProblemGrammarAccess problemGrammarAccess;
-
         protected void format(Problem problem, IFormattableDocument doc) {
                 doc.prepend(problem, this::noSpace);
                 var region = regionFor(problem);
@@ -37,31 +31,26 @@ public class ProblemFormatter extends AbstractJavaFormatter {
                 doc.append(region.feature(ProblemPackage.Literals.ASSERTION__DEFAULT), this::oneSpace);
                 doc.append(region.feature(ProblemPackage.Literals.ASSERTION__RELATION), this::noSpace);
                 formatParenthesizedList(region, doc);
+                for (var argument : assertion.getArguments()) {
+                        doc.format(argument);
+                }
+                var colon = region.keyword(":");
+                boolean abbreviated = colon == null;
+                if (!abbreviated) {
+                        doc.prepend(colon, this::noSpace);
+                        doc.append(colon, this::oneSpace);
+                }
                 var value = assertion.getValue();
                 if (value != null) {
-                        doc.append(value, this::noSpace);
+                        var valueRegion = regionForEObject(value);
+                        // Avoid clash between noSpace after ASSERTION_DEFAULT and noSpace after the 0-length region
+                        // for a true LogicAssertionValue if the abbreviated form of assertion (no : operator) is used.
+                        if (abbreviated && valueRegion != null && valueRegion.getLength() > 0) {
+                                doc.append(value, this::noSpace);
+                        }
                         doc.format(value);
                 }
                 doc.prepend(region.keyword("."), this::noSpace);
-                for (var argument : assertion.getArguments()) {
-                        doc.format(argument);
-                }
-        }
-
-        protected void format(LogicAssertionValue assertionValue, IFormattableDocument doc) {
-                var region = regionFor(assertionValue);
-                doc.prepend(region.keyword(":"), this::noSpace);
-                doc.append(region.keyword(":"), this::oneSpace);
-        }
-
-        protected void format(ExprAssertionValue assertionValue, IFormattableDocument doc) {
-                var region = regionFor(assertionValue);
-                doc.surround(region.keyword("="), this::oneSpace);
-                doc.surround(region.keyword("in"), this::oneSpace);
-                var body = assertionValue.getBody();
-                if (body != null) {
-                        doc.format(body);
-                }
         }
 
         protected void format(ClassDeclaration classDeclaration, IFormattableDocument doc) {
@@ -128,7 +117,7 @@ public class ProblemFormatter extends AbstractJavaFormatter {
         protected void format(IndividualDeclaration individualDeclaration, IFormattableDocument doc) {
                 surroundNewLines(doc, individualDeclaration, this::singleNewLine);
                 var region = regionFor(individualDeclaration);
-                doc.append(region.keyword("individual"), this::oneSpace);
+                doc.append(region.keyword("indiv"), this::oneSpace);
                 formatList(region, ",", doc);
                 doc.prepend(region.keyword("."), this::noSpace);
         }
diff --git a/subprojects/language/src/main/java/tools/refinery/language/serializer/PreferShortAssertionsProblemSemanticSequencer.java b/subprojects/language/src/main/java/tools/refinery/language/serializer/PreferShortAssertionsProblemSemanticSequencer.java
index c51a5e28..27ce1521 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/serializer/PreferShortAssertionsProblemSemanticSequencer.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/serializer/PreferShortAssertionsProblemSemanticSequencer.java
@@ -5,7 +5,7 @@ import org.eclipse.xtext.serializer.ISerializationContext;
 import org.eclipse.xtext.serializer.sequencer.ITransientValueService.ListTransient;
 import org.eclipse.xtext.serializer.sequencer.ITransientValueService.ValueTransient;
 import tools.refinery.language.model.problem.Assertion;
-import tools.refinery.language.model.problem.LogicAssertionValue;
+import tools.refinery.language.model.problem.LogicConstant;
 import tools.refinery.language.model.problem.LogicValue;
 import tools.refinery.language.model.problem.ProblemPackage;
 import tools.refinery.language.services.ProblemGrammarAccess;
@@ -17,8 +17,8 @@ public class PreferShortAssertionsProblemSemanticSequencer extends ProblemSemant
         @Override
         protected void sequence_Assertion(ISerializationContext context, Assertion semanticObject) {
                 if (semanticObject.isDefault() ||
-                                !(semanticObject.getValue() instanceof LogicAssertionValue logicAssertionValue) ||
-                                logicAssertionValue.getLogicValue() == LogicValue.ERROR) {
+                                !(semanticObject.getValue() instanceof LogicConstant logicConstant) ||
+                                logicConstant.getLogicValue() == LogicValue.ERROR) {
                         super.sequence_Assertion(context, semanticObject);
                         return;
                 }
@@ -34,7 +34,7 @@ public class PreferShortAssertionsProblemSemanticSequencer extends ProblemSemant
                 }
                 var feeder = createSequencerFeeder(context, semanticObject);
                 var access = grammarAccess.getAssertionAccess();
-                feeder.accept(access.getValueShortLogicAssertionValueParserRuleCall_1_1_0_0(), logicAssertionValue);
+                feeder.accept(access.getValueShortLogicConstantParserRuleCall_1_1_0_0(), logicConstant);
                 feeder.accept(access.getRelationRelationQualifiedNameParserRuleCall_1_1_1_0_1(), semanticObject.getRelation());
                 var iterator = semanticObject.getArguments().iterator();
                 if (iterator.hasNext()) {
diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java b/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java
index 5412f620..65167ed6 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/utils/SymbolCollector.java
@@ -242,7 +242,7 @@ class SymbolCollector {
                         }
                         assertion.getArguments().add(argument);
                 }
-                var value = ProblemFactory.eINSTANCE.createLogicAssertionValue();
+                var value = ProblemFactory.eINSTANCE.createLogicConstant();
                 value.setLogicValue(logicValue);
                 assertion.setValue(value);
                 collectAssertion(assertion);
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 e0dee496..58daa365 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
@@ -24,30 +24,30 @@ class ProblemParsingTest {
                                 }
 
                                 class Person {
-                                        refers Person[0..*] children opposite parent
-                                        refers Person[0..1] parent opposite children
+                                        Person[0..*] children opposite parent
+                                        Person[0..1] parent opposite children
                                         int age
-                                        refers TaxStatus taxStatus
+                                        TaxStatus taxStatus
                                 }
 
                                 enum TaxStatus {
-                                        child, student, adult, retired
+                                        CHILD, STUDENT, ADULT, RETIRED
                                 }
 
                                 % A child cannot have any dependents.
                                 error invalidTaxStatus(Person p) <->
-                                        taxStatus(p, child), children(p, _q).
+                                        taxStatus(p, CHILD), children(p, _q).
 
-                                individual family.
+                                indiv family.
                                 Family(family).
                                 members(family, anne): true.
                                 members(family, bob).
                                 members(family, ciri).
                                 children(anne, ciri).
                                 ?children(bob, ciri).
-                                taxStatus(anne, adult).
-                                age(bob) in 21..35.
-                                age(ciri) = 10.
+                                taxStatus(anne, ADULT).
+                                age(bob): 21..35.
+                                age(ciri): 10.
                                 """);
                 assertThat(problem.errors(), empty());
         }
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 a6e38130..6e0802ca 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
@@ -179,7 +179,7 @@ class ProblemFormatterTest {
 
         @Test
         void individualDeclarationTest() {
-                testFormatter("  individual  a  ,  b  .  ", "individual a, b.\n");
+                testFormatter("  indiv  a  ,  b  .  ", "indiv a, b.\n");
         }
 
         @Test
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
index 6e702720..65ceb45f 100644
--- 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
@@ -24,8 +24,8 @@ class TransitiveClosureParserTest {
         @Test
         void binaryAddOperatorTest() {
                 var problem = parseHelper.parse("""
-                                        int a().
-                                        int b().
+                                        fn int a().
+                                        fn int b().
                                         pred foo() <-> a() + (b()) > 10.
                                 """);
                 assertThat(problem.errors(), empty());
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 2fd647e5..fa462691 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
@@ -67,7 +67,7 @@ class NodeScopingTest {
         @MethodSource("individualNodeReferenceSource")
         void individualNodeInAssertionTest(String qualifiedNamePrefix, boolean namedProblem) {
                 var problem = parse("""
-                                individual a, b.
+                                indiv a, b.
                                 pred predicate(node x, node y) <-> node(x).
                                 predicate({PARAM}a, {PARAM}a).
                                 ?predicate({PARAM}a, {PARAM}b).
@@ -84,7 +84,7 @@ class NodeScopingTest {
         @MethodSource("individualNodeReferenceSource")
         void individualNodeInPredicateTest(String qualifiedNamePrefix, boolean namedProblem) {
                 var problem = parse("""
-                                individual b.
+                                indiv 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 5024fb45..4a18704a 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
@@ -59,7 +59,7 @@ class ProblemSerializerTest {
                 assertSerializedResult("""
                                 pred foo(node p).
 
-                                individual a.
+                                indiv a.
                                 """ + serializedAssertion + "\n");
         }
 
@@ -82,7 +82,7 @@ class ProblemSerializerTest {
                 assertSerializedResult("""
                                 pred foo(node p).
 
-                                individual a.
+                                indiv a.
                                 default foo(a):\040""" + valueAsString + ".\n");
         }
 
@@ -149,7 +149,7 @@ class ProblemSerializerTest {
                 var argument = ProblemFactory.eINSTANCE.createNodeAssertionArgument();
                 argument.setNode(node);
                 assertion.getArguments().add(argument);
-                var value = ProblemFactory.eINSTANCE.createLogicAssertionValue();
+                var value = ProblemFactory.eINSTANCE.createLogicConstant();
                 value.setLogicValue(logicValue);
                 assertion.setValue(value);
                 assertion.setDefault(isDefault);
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 66b7f1ab..af6de37f 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
@@ -45,7 +45,7 @@ class SymbolCollectorTest {
         @Test
         void individualNodeTest() {
                 var problem = parseHelper.parse("""
-                                individual a.
+                                indiv a.
                                 """);
                 var collectedSymbols = desugarer.collectSymbols(problem.get());
                 var node = problem.individualNode("a");