diff options
author | Kristóf Marussy <kristof@marussy.com> | 2024-05-17 17:13:21 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2024-05-26 17:22:31 +0200 |
commit | 378d97f41ab9bf1a3dc2136f340bb57d263ea474 (patch) | |
tree | 55e4002d0bfb00392f4ab9538f804ee241c9d84e /subprojects/language/src | |
parent | chore(deps): bump dependencies (diff) | |
download | refinery-378d97f41ab9bf1a3dc2136f340bb57d263ea474.tar.gz refinery-378d97f41ab9bf1a3dc2136f340bb57d263ea474.tar.zst refinery-378d97f41ab9bf1a3dc2136f340bb57d263ea474.zip |
feat: rule parsing
Diffstat (limited to 'subprojects/language/src')
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: | |||
18 | Statement: | 18 | Statement: |
19 | ImportStatement | Assertion | ClassDeclaration | EnumDeclaration | | 19 | ImportStatement | Assertion | ClassDeclaration | EnumDeclaration | |
20 | DatatypeDeclaration | AggregatorDeclaration | PredicateDefinition | | 20 | DatatypeDeclaration | AggregatorDeclaration | PredicateDefinition | |
21 | /* FunctionDefinition | RuleDefinition | */ | 21 | /* FunctionDefinition | */ RuleDefinition | |
22 | ScopeDeclaration | NodeDeclaration; | 22 | ScopeDeclaration | NodeDeclaration; |
23 | 23 | ||
24 | ImportStatement: | 24 | ImportStatement: |
@@ -75,35 +75,40 @@ Conjunction: | |||
75 | // | 75 | // |
76 | //Case: | 76 | //Case: |
77 | // Conjunction ({Match.condition=current} "->" value=Expr)?; | 77 | // Conjunction ({Match.condition=current} "->" value=Expr)?; |
78 | //RuleDefinition: | 78 | |
79 | // "rule" | 79 | enum RuleKind: |
80 | // name=Identifier | 80 | DECISION="decision" | PROPAGATION="propagation"; |
81 | // "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")" | 81 | |
82 | // (":" preconditions+=Conjunction (";" preconditions+=Conjunction)*)? | 82 | RuleDefinition: |
83 | // "==>" consequents+=Consequent (";" consequents+=Consequent)*)? | 83 | kind=RuleKind? "rule" |
84 | // "."; | 84 | name=Identifier |
85 | "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")" | ||
86 | (":" preconditions+=Conjunction (";" preconditions+=Conjunction)*)? | ||
87 | ("==>" consequents+=Consequent (";" consequents+=Consequent)*)? | ||
88 | "."; | ||
89 | |||
90 | enum ParameterBinding: | ||
91 | FOCUS="&" | MULTI="*"; | ||
85 | 92 | ||
86 | Parameter: | 93 | Parameter: |
87 | parameterType=[Relation|QualifiedName]? name=Identifier; | 94 | ( |
95 | (concreteness=Concreteness? modality=Modality)? | ||
96 | parameterType=[Relation|QualifiedName] | ||
97 | )? binding=ParameterBinding? name=Identifier; | ||
88 | 98 | ||
89 | //Consequent: | 99 | Consequent: |
90 | // actions+=Action ("," actions+=Action)*; | 100 | actions+=Action ("," actions+=Action)*; |
91 | // | 101 | |
92 | //Action: | 102 | Action: |
93 | // AssertionAction | DeleteAction | NewAction; | 103 | AssertionAction; |
94 | // | 104 | |
95 | //AssertionAction: | 105 | AssertionAction: |
96 | // value=ShortLogicValue? atom=Atom | | 106 | relation=[Relation|QualifiedName] |
97 | // atom=Atom (overwrite?=":=" | "<:") value=LogicValue; | 107 | "(" (arguments+=AssertionArgument ("," arguments+=AssertionArgument)*)? ")" |
98 | // | 108 | ":" value=Expr | |
99 | //DeleteAction: | 109 | value=ShortLogicConstant |
100 | // "delete" variableOrNode=[VariableOrNode|QualifiedName]; | 110 | relation=[Relation|QualifiedName] |
101 | // | 111 | "(" (arguments+=AssertionArgument ("," arguments+=AssertionArgument)*)? ")"; |
102 | //NewAction: | ||
103 | // "new" variable=NewVariable ("<:" parent=[VariableOrNode|QualifiedName])?; | ||
104 | // | ||
105 | //NewVariable: | ||
106 | // name=Identifier; | ||
107 | 112 | ||
108 | Expr: | 113 | Expr: |
109 | AssignmentExpr; | 114 | AssignmentExpr; |
@@ -159,7 +164,7 @@ RangeExpr returns Expr: | |||
159 | 164 | ||
160 | UnaryExpr returns Expr: | 165 | UnaryExpr returns Expr: |
161 | ArithmeticUnaryExpr | NegationExpr | | 166 | ArithmeticUnaryExpr | NegationExpr | |
162 | CountExpr | AggregationExpr | CastExpr; | 167 | CountExpr | AggregationExpr | ModalExpr | CastExpr; |
163 | 168 | ||
164 | enum UnaryOp: | 169 | enum UnaryOp: |
165 | PLUS="+" | MINUS="-"; | 170 | PLUS="+" | MINUS="-"; |
@@ -177,6 +182,15 @@ AggregationExpr: | |||
177 | aggregator=[AggregatorDeclaration|QualifiedName] | 182 | aggregator=[AggregatorDeclaration|QualifiedName] |
178 | "{" value=Expr "|" condition=ComparisonExpr "}"; | 183 | "{" value=Expr "|" condition=ComparisonExpr "}"; |
179 | 184 | ||
185 | enum Concreteness: | ||
186 | CANDIDATE="candidate"; | ||
187 | |||
188 | enum Modality: | ||
189 | MUST="must" | MAY="may"; | ||
190 | |||
191 | ModalExpr: | ||
192 | concreteness=Concreteness? modality=Modality body=UnaryExpr; | ||
193 | |||
180 | CastExpr returns Expr: | 194 | CastExpr returns Expr: |
181 | CastExprBody ({CastExpr.body=current} "as" targetType=[Relation|QualifiedName])?; | 195 | CastExprBody ({CastExpr.body=current} "as" targetType=[Relation|QualifiedName])?; |
182 | 196 | ||
@@ -281,7 +295,7 @@ Identifier: | |||
281 | 295 | ||
282 | NonContainmentIdentifier: | 296 | NonContainmentIdentifier: |
283 | ID | "atom" | "multi" | "contained" | "problem" | "module" | | 297 | ID | "atom" | "multi" | "contained" | "problem" | "module" | |
284 | "datatype" | "aggregator"; | 298 | "datatype" | "aggregator" | "decision" | "propagation"; |
285 | 299 | ||
286 | Real returns ecore::EDouble: | 300 | Real returns ecore::EDouble: |
287 | EXPONENTIAL | INT "." (INT | EXPONENTIAL); | 301 | 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 { | |||
31 | public IScope getScope(EObject context, EReference reference) { | 31 | public IScope getScope(EObject context, EReference reference) { |
32 | var scope = super.getScope(context, reference); | 32 | var scope = super.getScope(context, reference); |
33 | if (reference == ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE) { | 33 | if (reference == ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE) { |
34 | return getNodesScope(context, scope); | 34 | // On the right side of a rule, assertion arguments may refer to variables. |
35 | var rule = EcoreUtil2.getContainerOfType(context, RuleDefinition.class); | ||
36 | return rule == null ? getNodesScope(context, scope) : getVariableScope(context, scope); | ||
35 | } | 37 | } |
36 | if (reference == ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE | 38 | if (reference == ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE) { |
37 | || reference == ProblemPackage.Literals.NEW_ACTION__PARENT | ||
38 | || reference == ProblemPackage.Literals.DELETE_ACTION__VARIABLE_OR_NODE) { | ||
39 | return getVariableScope(context, scope); | 39 | return getVariableScope(context, scope); |
40 | } | 40 | } |
41 | if (reference == ProblemPackage.Literals.REFERENCE_DECLARATION__OPPOSITE) { | 41 | if (reference == ProblemPackage.Literals.REFERENCE_DECLARATION__OPPOSITE) { |
@@ -81,13 +81,6 @@ public class ProblemScopeProvider extends AbstractProblemScopeProvider { | |||
81 | switch (currentContext) { | 81 | switch (currentContext) { |
82 | case ExistentialQuantifier quantifier -> variables.addAll(quantifier.getImplicitVariables()); | 82 | case ExistentialQuantifier quantifier -> variables.addAll(quantifier.getImplicitVariables()); |
83 | case Match match -> variables.addAll(match.getCondition().getImplicitVariables()); | 83 | case Match match -> variables.addAll(match.getCondition().getImplicitVariables()); |
84 | case Consequent consequent -> { | ||
85 | for (var literal : consequent.getActions()) { | ||
86 | if (literal instanceof NewAction newAction && newAction.getVariable() != null) { | ||
87 | variables.add(newAction.getVariable()); | ||
88 | } | ||
89 | } | ||
90 | } | ||
91 | default -> { | 84 | default -> { |
92 | // Nothing to add. | 85 | // Nothing to add. |
93 | } | 86 | } |
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 { | |||
472 | return null; | 472 | return null; |
473 | } | 473 | } |
474 | if (argument instanceof NodeAssertionArgument nodeAssertionArgument) { | 474 | if (argument instanceof NodeAssertionArgument nodeAssertionArgument) { |
475 | return nodeAssertionArgument.getNode(); | 475 | var variableOrNode = nodeAssertionArgument.getNode(); |
476 | if (variableOrNode == null || variableOrNode instanceof Node) { | ||
477 | return (Node) variableOrNode; | ||
478 | } | ||
476 | } | 479 | } |
477 | throw new IllegalArgumentException("Unknown assertion argument: " + argument); | 480 | throw new IllegalArgumentException("Unknown assertion argument: " + argument); |
478 | } | 481 | } |
@@ -484,8 +487,10 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
484 | } | 487 | } |
485 | for (var argument : assertion.getArguments()) { | 488 | for (var argument : assertion.getArguments()) { |
486 | if (argument instanceof NodeAssertionArgument nodeAssertionArgument) { | 489 | if (argument instanceof NodeAssertionArgument nodeAssertionArgument) { |
487 | var node = nodeAssertionArgument.getNode(); | 490 | var variableOrNode = nodeAssertionArgument.getNode(); |
488 | if (node != null && !node.eIsProxy() && ProblemUtil.isImplicitNode(node)) { | 491 | if (variableOrNode instanceof Node node && |
492 | !variableOrNode.eIsProxy() && | ||
493 | ProblemUtil.isImplicitNode(node)) { | ||
489 | var name = node.getName(); | 494 | var name = node.getName(); |
490 | var message = ("Implicit nodes are not allowed in modules. Explicitly declare '%s' as a node " + | 495 | var message = ("Implicit nodes are not allowed in modules. Explicitly declare '%s' as a node " + |
491 | "with the declaration 'declare %s.'").formatted(name, name); | 496 | "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; | |||
9 | import org.eclipse.xtext.testing.InjectWith; | 9 | import org.eclipse.xtext.testing.InjectWith; |
10 | import org.eclipse.xtext.testing.extensions.InjectionExtension; | 10 | import org.eclipse.xtext.testing.extensions.InjectionExtension; |
11 | import org.junit.jupiter.api.Disabled; | 11 | import org.junit.jupiter.api.Disabled; |
12 | import org.junit.jupiter.api.Test; | ||
13 | import org.junit.jupiter.api.extension.ExtendWith; | 12 | import org.junit.jupiter.api.extension.ExtendWith; |
14 | import org.junit.jupiter.params.ParameterizedTest; | 13 | import org.junit.jupiter.params.ParameterizedTest; |
15 | import org.junit.jupiter.params.provider.ValueSource; | 14 | import org.junit.jupiter.params.provider.ValueSource; |
@@ -17,7 +16,7 @@ import tools.refinery.language.model.tests.utils.ProblemParseHelper; | |||
17 | import tools.refinery.language.tests.ProblemInjectorProvider; | 16 | import tools.refinery.language.tests.ProblemInjectorProvider; |
18 | 17 | ||
19 | import static org.hamcrest.MatcherAssert.assertThat; | 18 | import static org.hamcrest.MatcherAssert.assertThat; |
20 | import static org.hamcrest.Matchers.*; | 19 | import static org.hamcrest.Matchers.empty; |
21 | 20 | ||
22 | @Disabled("TODO: Rework transformation rules") | 21 | @Disabled("TODO: Rework transformation rules") |
23 | @ExtendWith(InjectionExtension.class) | 22 | @ExtendWith(InjectionExtension.class) |
@@ -29,62 +28,13 @@ class RuleParsingTest { | |||
29 | @ParameterizedTest | 28 | @ParameterizedTest |
30 | @ValueSource(strings = { """ | 29 | @ValueSource(strings = { """ |
31 | pred Person(p). | 30 | pred Person(p). |
32 | rule r(p1): must Person(p1) ==> Person(p1) := false. | 31 | rule r(p1): must Person(p1) ==> Person(p1): false. |
33 | """, """ | ||
34 | pred Person(p). | ||
35 | rule r(p1): must Person(p1) ==> Person(p1) <: false. | ||
36 | """, """ | 32 | """, """ |
37 | pred Person(p). | 33 | pred Person(p). |
38 | rule r(p1): must Person(p1) ==> !Person(p1). | 34 | rule r(p1): must Person(p1) ==> !Person(p1). |
39 | """, """ | ||
40 | pred Person(p). | ||
41 | rule r(p1): must Person(p1) ==> delete p1. | ||
42 | """ }) | 35 | """ }) |
43 | void simpleTest(String text) { | 36 | void simpleTest(String text) { |
44 | var problem = parseHelper.parse(text); | 37 | var problem = parseHelper.parse(text); |
45 | assertThat(problem.getResourceErrors(), empty()); | 38 | assertThat(problem.getResourceErrors(), empty()); |
46 | } | 39 | } |
47 | |||
48 | @Test | ||
49 | void newNodeTest() { | ||
50 | var problem = parseHelper.parse(""" | ||
51 | pred Person(p). | ||
52 | rule r(p1): must Person(p1) ==> new p2, Person(p2) := unknown. | ||
53 | """); | ||
54 | assertThat(problem.getResourceErrors(), empty()); | ||
55 | assertThat(problem.rule("r").param(0), equalTo(problem.rule("r").conj(0).lit(0).arg(0).variable())); | ||
56 | assertThat(problem.rule("r").consequent(0).action(0).newVar(), | ||
57 | equalTo(problem.rule("r").consequent(0).action(1).assertedAtom().arg(0).variable())); | ||
58 | } | ||
59 | |||
60 | @Test | ||
61 | void differentScopeTest() { | ||
62 | var problem = parseHelper.parse(""" | ||
63 | pred Friend(a, b). | ||
64 | rule r(p1): !may Friend(p1, p2) ==> new p2, Friend(p1, p2) := true. | ||
65 | """); | ||
66 | assertThat(problem.getResourceErrors(), empty()); | ||
67 | assertThat(problem.rule("r").conj(0).lit(0).negated().arg(1).variable(), | ||
68 | not(equalTo(problem.rule("r").consequent(0).action(1).assertedAtom().arg(1).variable()))); | ||
69 | } | ||
70 | |||
71 | @Test | ||
72 | void parameterShadowingTest() { | ||
73 | var problem = parseHelper.parse(""" | ||
74 | pred Friend(a, b). | ||
75 | rule r(p1, p2): !may Friend(p1, p2) ==> new p2, Friend(p1, p2) := true. | ||
76 | """); | ||
77 | assertThat(problem.getResourceErrors(), empty()); | ||
78 | assertThat(problem.rule("r").param(1), | ||
79 | not(equalTo(problem.rule("r").consequent(0).action(1).assertedAtom().arg(1).variable()))); | ||
80 | } | ||
81 | |||
82 | @Test | ||
83 | void deleteDifferentScopeNodeTest() { | ||
84 | var problem = parseHelper.parse(""" | ||
85 | pred Person(p). | ||
86 | rule r(p1): must Friend(p1, p2) ==> delete p2. | ||
87 | """); | ||
88 | assertThat(problem.getResourceErrors(), not(empty())); | ||
89 | } | ||
90 | } | 40 | } |
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 @@ | |||
6 | package tools.refinery.language.model.tests.utils; | 6 | package tools.refinery.language.model.tests.utils; |
7 | 7 | ||
8 | import tools.refinery.language.model.problem.Action; | 8 | import tools.refinery.language.model.problem.Action; |
9 | import tools.refinery.language.model.problem.AssertionAction; | ||
10 | import tools.refinery.language.model.problem.DeleteAction; | ||
11 | import tools.refinery.language.model.problem.NewAction; | ||
12 | import tools.refinery.language.model.problem.VariableOrNode; | ||
13 | 9 | ||
14 | public record WrappedAction(Action action) { | 10 | public record WrappedAction(Action action) { |
15 | public Action get() { | 11 | public Action get() { |
16 | return action; | 12 | return action; |
17 | } | 13 | } |
18 | |||
19 | public VariableOrNode newVar() { | ||
20 | return ((NewAction) action).getVariable(); | ||
21 | } | ||
22 | |||
23 | public VariableOrNode deleteVar() { | ||
24 | return ((DeleteAction) action).getVariableOrNode(); | ||
25 | } | ||
26 | |||
27 | public WrappedAtom assertedAtom() { | ||
28 | return new WrappedAtom(((AssertionAction) action).getAtom()); | ||
29 | } | ||
30 | } | 14 | } |
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) { | |||
15 | } | 15 | } |
16 | 16 | ||
17 | public Node node() { | 17 | public Node node() { |
18 | return ((NodeAssertionArgument) assertionArgument).getNode(); | 18 | return (Node) ((NodeAssertionArgument) assertionArgument).getNode(); |
19 | } | 19 | } |
20 | } | 20 | } |