From 378d97f41ab9bf1a3dc2136f340bb57d263ea474 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Fri, 17 May 2024 17:13:21 +0200 Subject: feat: rule parsing --- .../java/tools/refinery/language/Problem.xtext | 72 +++++++++++++--------- .../language/scoping/ProblemScopeProvider.java | 15 ++--- .../language/validation/ProblemValidator.java | 11 +++- .../language/tests/rules/RuleParsingTest.java | 54 +--------------- .../language/model/tests/utils/WrappedAction.java | 16 ----- .../tests/utils/WrappedAssertionArgument.java | 2 +- 6 files changed, 58 insertions(+), 112 deletions(-) (limited to 'subprojects/language') 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(); } } -- cgit v1.2.3-54-g00ecf