feat: rule parsing

6 files changed, 58 insertions, 112 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 08f7a585..64998cd0 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
+++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
@@ -18,7 +18,7 @@ enum ModuleKind:
 Statement:
         ImportStatement | Assertion | ClassDeclaration | EnumDeclaration |
         DatatypeDeclaration | AggregatorDeclaration | PredicateDefinition |
-        /* FunctionDefinition | RuleDefinition | */
+        /* FunctionDefinition | */ RuleDefinition |
         ScopeDeclaration | NodeDeclaration;
 
 ImportStatement:
@@ -75,35 +75,40 @@ Conjunction:
 //
 //Case:
 //      Conjunction ({Match.condition=current} "->" value=Expr)?;
-//RuleDefinition:
-//      "rule"
-//      name=Identifier
-//      "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")"
-//      (":" preconditions+=Conjunction (";" preconditions+=Conjunction)*)?
-//      "==>" consequents+=Consequent (";" consequents+=Consequent)*)?
-//      ".";
+
+enum RuleKind:
+        DECISION="decision" | PROPAGATION="propagation";
+
+RuleDefinition:
+        kind=RuleKind? "rule"
+        name=Identifier
+        "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")"
+        (":" preconditions+=Conjunction (";" preconditions+=Conjunction)*)?
+        ("==>" consequents+=Consequent (";" consequents+=Consequent)*)?
+        ".";
+
+enum ParameterBinding:
+        FOCUS="&" | MULTI="*";
 
 Parameter:
-        parameterType=[Relation|QualifiedName]? name=Identifier;
+        (
+                (concreteness=Concreteness? modality=Modality)?
+                parameterType=[Relation|QualifiedName]
+        )? binding=ParameterBinding? name=Identifier;
 
-//Consequent:
-//      actions+=Action ("," actions+=Action)*;
-//
-//Action:
-//      AssertionAction | DeleteAction | NewAction;
-//
-//AssertionAction:
-//      value=ShortLogicValue? atom=Atom |
-//      atom=Atom (overwrite?=":=" | "<:") value=LogicValue;
-//
-//DeleteAction:
-//      "delete" variableOrNode=[VariableOrNode|QualifiedName];
-//
-//NewAction:
-//      "new" variable=NewVariable ("<:" parent=[VariableOrNode|QualifiedName])?;
-//
-//NewVariable:
-//      name=Identifier;
+Consequent:
+        actions+=Action ("," actions+=Action)*;
+
+Action:
+        AssertionAction;
+
+AssertionAction:
+        relation=[Relation|QualifiedName]
+        "(" (arguments+=AssertionArgument ("," arguments+=AssertionArgument)*)? ")"
+        ":" value=Expr |
+        value=ShortLogicConstant
+        relation=[Relation|QualifiedName]
+        "(" (arguments+=AssertionArgument ("," arguments+=AssertionArgument)*)? ")";
 
 Expr:
         AssignmentExpr;
@@ -159,7 +164,7 @@ RangeExpr returns Expr:
 
 UnaryExpr returns Expr:
         ArithmeticUnaryExpr | NegationExpr |
-        CountExpr | AggregationExpr | CastExpr;
+        CountExpr | AggregationExpr | ModalExpr | CastExpr;
 
 enum UnaryOp:
         PLUS="+" | MINUS="-";
@@ -177,6 +182,15 @@ AggregationExpr:
         aggregator=[AggregatorDeclaration|QualifiedName]
         "{" value=Expr "|" condition=ComparisonExpr "}";
 
+enum Concreteness:
+        CANDIDATE="candidate";
+
+enum Modality:
+        MUST="must" | MAY="may";
+
+ModalExpr:
+        concreteness=Concreteness? modality=Modality body=UnaryExpr;
+
 CastExpr returns Expr:
         CastExprBody ({CastExpr.body=current} "as" targetType=[Relation|QualifiedName])?;
 
@@ -281,7 +295,7 @@ Identifier:
 
 NonContainmentIdentifier:
         ID | "atom" | "multi" | "contained" | "problem" | "module" |
-        "datatype" | "aggregator";
+        "datatype" | "aggregator" | "decision" | "propagation";
 
 Real returns ecore::EDouble:
         EXPONENTIAL | INT "." (INT | EXPONENTIAL);
diff --git a/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemScopeProvider.java b/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemScopeProvider.java
index d94c9a13..21f64236 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemScopeProvider.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemScopeProvider.java
@@ -31,11 +31,11 @@ public class ProblemScopeProvider extends AbstractProblemScopeProvider {
         public IScope getScope(EObject context, EReference reference) {
                 var scope = super.getScope(context, reference);
                 if (reference == ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE) {
-                        return getNodesScope(context, scope);
+                        // On the right side of a rule, assertion arguments may refer to variables.
+                        var rule = EcoreUtil2.getContainerOfType(context, RuleDefinition.class);
+                        return rule == null ? getNodesScope(context, scope) : getVariableScope(context, scope);
                 }
-                if (reference == ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE
-                                || reference == ProblemPackage.Literals.NEW_ACTION__PARENT
-                                || reference == ProblemPackage.Literals.DELETE_ACTION__VARIABLE_OR_NODE) {
+                if (reference == ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE) {
                         return getVariableScope(context, scope);
                 }
                 if (reference == ProblemPackage.Literals.REFERENCE_DECLARATION__OPPOSITE) {
@@ -81,13 +81,6 @@ public class ProblemScopeProvider extends AbstractProblemScopeProvider {
                 switch (currentContext) {
                 case ExistentialQuantifier quantifier -> variables.addAll(quantifier.getImplicitVariables());
                 case Match match -> variables.addAll(match.getCondition().getImplicitVariables());
-                case Consequent consequent -> {
-                        for (var literal : consequent.getActions()) {
-                                if (literal instanceof NewAction newAction && newAction.getVariable() != null) {
-                                        variables.add(newAction.getVariable());
-                                }
-                        }
-                }
                 default -> {
                         // Nothing to add.
                 }
diff --git a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java
index 745e2d2b..c49718ab 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java
@@ -472,7 +472,10 @@ public class ProblemValidator extends AbstractProblemValidator {
                         return null;
                 }
                 if (argument instanceof NodeAssertionArgument nodeAssertionArgument) {
-                        return nodeAssertionArgument.getNode();
+                        var variableOrNode = nodeAssertionArgument.getNode();
+                        if (variableOrNode == null || variableOrNode instanceof Node) {
+                                return (Node) variableOrNode;
+                        }
                 }
                 throw new IllegalArgumentException("Unknown assertion argument: " + argument);
         }
@@ -484,8 +487,10 @@ public class ProblemValidator extends AbstractProblemValidator {
                 }
                 for (var argument : assertion.getArguments()) {
                         if (argument instanceof NodeAssertionArgument nodeAssertionArgument) {
-                                var node = nodeAssertionArgument.getNode();
-                                if (node != null && !node.eIsProxy() && ProblemUtil.isImplicitNode(node)) {
+                                var variableOrNode = nodeAssertionArgument.getNode();
+                                if (variableOrNode instanceof Node node &&
+                                                !variableOrNode.eIsProxy() &&
+                                                ProblemUtil.isImplicitNode(node)) {
                                         var name = node.getName();
                                         var message = ("Implicit nodes are not allowed in modules. Explicitly declare '%s' as a node " +
                                                         "with the declaration 'declare %s.'").formatted(name, name);
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/rules/RuleParsingTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/rules/RuleParsingTest.java
index 56e65550..15636483 100644
--- a/subprojects/language/src/test/java/tools/refinery/language/tests/rules/RuleParsingTest.java
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/rules/RuleParsingTest.java
@@ -9,7 +9,6 @@ import com.google.inject.Inject;
 import org.eclipse.xtext.testing.InjectWith;
 import org.eclipse.xtext.testing.extensions.InjectionExtension;
 import org.junit.jupiter.api.Disabled;
-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.ValueSource;
@@ -17,7 +16,7 @@ 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.*;
+import static org.hamcrest.Matchers.empty;
 
 @Disabled("TODO: Rework transformation rules")
 @ExtendWith(InjectionExtension.class)
@@ -29,62 +28,13 @@ class RuleParsingTest {
         @ParameterizedTest
         @ValueSource(strings = { """
                         pred Person(p).
-                        rule r(p1): must Person(p1) ==> Person(p1) := false.
-                        """, """
-                        pred Person(p).
-                        rule r(p1): must Person(p1) ==> Person(p1) <: false.
+                        rule r(p1): must Person(p1) ==> Person(p1): false.
                         """, """
                         pred Person(p).
                         rule r(p1): must Person(p1) ==> !Person(p1).
-                        """, """
-                        pred Person(p).
-                        rule r(p1): must Person(p1) ==> delete p1.
                         """ })
         void simpleTest(String text) {
                 var problem = parseHelper.parse(text);
                 assertThat(problem.getResourceErrors(), empty());
         }
-
-        @Test
-        void newNodeTest() {
-                var problem = parseHelper.parse("""
-                                pred Person(p).
-                                rule r(p1): must Person(p1) ==> new p2, Person(p2) := unknown.
-                                """);
-                assertThat(problem.getResourceErrors(), empty());
-                assertThat(problem.rule("r").param(0), equalTo(problem.rule("r").conj(0).lit(0).arg(0).variable()));
-                assertThat(problem.rule("r").consequent(0).action(0).newVar(),
-                                equalTo(problem.rule("r").consequent(0).action(1).assertedAtom().arg(0).variable()));
-        }
-
-        @Test
-        void differentScopeTest() {
-                var problem = parseHelper.parse("""
-                                pred Friend(a, b).
-                                rule r(p1): !may Friend(p1, p2) ==> new p2, Friend(p1, p2) := true.
-                                """);
-                assertThat(problem.getResourceErrors(), empty());
-                assertThat(problem.rule("r").conj(0).lit(0).negated().arg(1).variable(),
-                                not(equalTo(problem.rule("r").consequent(0).action(1).assertedAtom().arg(1).variable())));
-        }
-
-        @Test
-        void parameterShadowingTest() {
-                var problem = parseHelper.parse("""
-                                pred Friend(a, b).
-                                rule r(p1, p2): !may Friend(p1, p2) ==> new p2, Friend(p1, p2) := true.
-                                """);
-                assertThat(problem.getResourceErrors(), empty());
-                assertThat(problem.rule("r").param(1),
-                                not(equalTo(problem.rule("r").consequent(0).action(1).assertedAtom().arg(1).variable())));
-        }
-
-        @Test
-        void deleteDifferentScopeNodeTest() {
-                var problem = parseHelper.parse("""
-                                pred Person(p).
-                                rule r(p1): must Friend(p1, p2) ==> delete p2.
-                                """);
-                assertThat(problem.getResourceErrors(), not(empty()));
-        }
 }
diff --git a/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedAction.java b/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedAction.java
index 3a49a0b9..4987cb89 100644
--- a/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedAction.java
+++ b/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedAction.java
@@ -6,25 +6,9 @@
 package tools.refinery.language.model.tests.utils;
 
 import tools.refinery.language.model.problem.Action;
-import tools.refinery.language.model.problem.AssertionAction;
-import tools.refinery.language.model.problem.DeleteAction;
-import tools.refinery.language.model.problem.NewAction;
-import tools.refinery.language.model.problem.VariableOrNode;
 
 public record WrappedAction(Action action) {
         public Action get() {
                 return action;
         }
-        
-        public VariableOrNode newVar() {
-                return ((NewAction) action).getVariable();
-        }
-        
-        public VariableOrNode deleteVar() {
-                return ((DeleteAction) action).getVariableOrNode();
-        }
-        
-        public WrappedAtom assertedAtom() {
-                return new WrappedAtom(((AssertionAction) action).getAtom());
-        }
 }
diff --git a/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedAssertionArgument.java b/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedAssertionArgument.java
index b36f2506..50cb958d 100644
--- a/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedAssertionArgument.java
+++ b/subprojects/language/src/testFixtures/java/tools/refinery/language/model/tests/utils/WrappedAssertionArgument.java
@@ -15,6 +15,6 @@ public record WrappedAssertionArgument(AssertionArgument assertionArgument) {
         }
 
         public Node node() {
-                return ((NodeAssertionArgument) assertionArgument).getNode();
+                return (Node) ((NodeAssertionArgument) assertionArgument).getNode();
         }
 }