diff options
Diffstat (limited to 'subprojects/language/src/main')
4 files changed, 50 insertions, 56 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 c94d40ab..ba885e3c 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext +++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext | |||
@@ -33,25 +33,19 @@ ReferenceDeclaration: | |||
33 | name=Identifier | 33 | name=Identifier |
34 | ("opposite" opposite=[ReferenceDeclaration|QualifiedName])?; | 34 | ("opposite" opposite=[ReferenceDeclaration|QualifiedName])?; |
35 | 35 | ||
36 | enum PredicateKind: | ||
37 | DIRECT="direct"; | ||
38 | |||
39 | PredicateDefinition: | 36 | PredicateDefinition: |
40 | (error?="error" "pred"? | kind=PredicateKind? "pred") | 37 | (error?="error" "pred"? | "pred") |
41 | name=Identifier | 38 | name=Identifier |
42 | "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")" | 39 | "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")" |
43 | ("<->" bodies+=Conjunction (";" bodies+=Conjunction)*)? | 40 | ("<->" bodies+=Conjunction (";" bodies+=Conjunction)*)? |
44 | "."; | 41 | "."; |
45 | 42 | ||
46 | enum RuleKind: | ||
47 | DIRECT="direct"; | ||
48 | |||
49 | RuleDefinition: | 43 | RuleDefinition: |
50 | kind=RuleKind "rule" | 44 | "rule" |
51 | name=Identifier | 45 | name=Identifier |
52 | "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")" | 46 | "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")" |
53 | (":" bodies+=Conjunction (";" bodies+=Conjunction)* | 47 | (":" bodies+=Conjunction (";" bodies+=Conjunction)* |
54 | "~>" action=Action)? | 48 | "==>" consequents+=Consequent (";" consequents+=Consequent)*)? |
55 | "."; | 49 | "."; |
56 | 50 | ||
57 | Parameter: | 51 | Parameter: |
@@ -60,45 +54,40 @@ Parameter: | |||
60 | Conjunction: | 54 | Conjunction: |
61 | literals+=Literal ("," literals+=Literal)*; | 55 | literals+=Literal ("," literals+=Literal)*; |
62 | 56 | ||
63 | Action: | 57 | Consequent: |
64 | actionLiterals+=ActionLiteral ("," actionLiterals+=ActionLiteral)*; | 58 | actions+=Action ("," actions+=Action)*; |
65 | 59 | ||
66 | Literal: | 60 | Literal: |
67 | Atom | ValueLiteral | NegativeLiteral; | 61 | Atom | NegativeLiteral; |
68 | |||
69 | ValueLiteral: | ||
70 | atom=Atom | ||
71 | (refinement?=":" | "=") | ||
72 | values+=LogicConstant ("|" values+=LogicConstant)*; | ||
73 | 62 | ||
74 | NegativeLiteral: | 63 | NegativeLiteral: |
75 | "!" atom=Atom; | 64 | modality=Modality? "!" atom=Atom; |
76 | 65 | ||
77 | ActionLiteral: | 66 | Action: |
78 | ValueActionLiteral | DeleteActionLiteral | NewActionLiteral; | 67 | AssertionAction | DeleteAction | NewAction; |
79 | 68 | ||
80 | ValueActionLiteral: | 69 | AssertionAction: |
81 | atom=Atom | 70 | value=ShortLogicValue? atom=Atom | |
82 | (refinement?=":" | "=") | 71 | atom=Atom (overwrite?="=" | ":") value=LogicValue; |
83 | value=LogicValue; | ||
84 | 72 | ||
85 | DeleteActionLiteral: | 73 | DeleteAction: |
86 | "delete" variableOrNode=[VariableOrNode|QualifiedName]; | 74 | "delete" variableOrNode=[VariableOrNode|QualifiedName]; |
87 | 75 | ||
88 | NewActionLiteral: | 76 | NewAction: |
89 | "new" variable=NewVariable; | 77 | "new" variable=NewVariable (":" parent=[VariableOrNode|QualifiedName])?; |
90 | 78 | ||
91 | NewVariable: | 79 | NewVariable: |
92 | name=Identifier; | 80 | name=Identifier; |
93 | 81 | ||
82 | enum Modality: | ||
83 | MAY="may" | MUST="must" | CURRENT="current"; | ||
84 | |||
94 | Atom: | 85 | Atom: |
86 | modality=Modality? | ||
95 | relation=[Relation|QualifiedName] | 87 | relation=[Relation|QualifiedName] |
96 | transitiveClosure?="+"? | 88 | transitiveClosure?="+"? |
97 | "(" (arguments+=Argument ("," arguments+=Argument)*)? ")"; | 89 | "(" (arguments+=Argument ("," arguments+=Argument)*)? ")"; |
98 | 90 | ||
99 | LogicConstant: | ||
100 | value=LogicValue; | ||
101 | |||
102 | Argument: | 91 | Argument: |
103 | VariableOrNodeArgument | ConstantArgument; | 92 | VariableOrNodeArgument | ConstantArgument; |
104 | 93 | ||
@@ -185,7 +174,7 @@ QualifiedName hidden(): | |||
185 | 174 | ||
186 | Identifier: | 175 | Identifier: |
187 | ID | "true" | "false" | "unknown" | "error" | "class" | "abstract" | "extends" | "enum" | "pred" | | 176 | ID | "true" | "false" | "unknown" | "error" | "class" | "abstract" | "extends" | "enum" | "pred" | |
188 | "indiv" | "problem" | "new" | "delete" | "direct" | "rule"; | 177 | "indiv" | "problem" | "new" | "delete" | "rule" | "may" | "must" | "current"; |
189 | 178 | ||
190 | Integer returns ecore::EInt hidden(): | 179 | Integer returns ecore::EInt hidden(): |
191 | "-"? INT; | 180 | "-"? INT; |
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 903347f7..df5d2090 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 | |||
@@ -49,7 +49,7 @@ public class ProblemFormatter extends AbstractJavaFormatter { | |||
49 | doc.format(argument); | 49 | doc.format(argument); |
50 | } | 50 | } |
51 | } | 51 | } |
52 | 52 | ||
53 | protected void format(ClassDeclaration classDeclaration, IFormattableDocument doc) { | 53 | protected void format(ClassDeclaration classDeclaration, IFormattableDocument doc) { |
54 | surroundNewLines(doc, classDeclaration, this::twoNewLines); | 54 | surroundNewLines(doc, classDeclaration, this::twoNewLines); |
55 | var region = regionFor(classDeclaration); | 55 | var region = regionFor(classDeclaration); |
@@ -69,7 +69,6 @@ public class ProblemFormatter extends AbstractJavaFormatter { | |||
69 | protected void format(PredicateDefinition predicateDefinition, IFormattableDocument doc) { | 69 | protected void format(PredicateDefinition predicateDefinition, IFormattableDocument doc) { |
70 | surroundNewLines(doc, predicateDefinition, this::twoNewLines); | 70 | surroundNewLines(doc, predicateDefinition, this::twoNewLines); |
71 | var region = regionFor(predicateDefinition); | 71 | var region = regionFor(predicateDefinition); |
72 | doc.append(region.feature(ProblemPackage.Literals.PREDICATE_DEFINITION__KIND), this::oneSpace); | ||
73 | doc.append(region.keyword("pred"), this::oneSpace); | 72 | doc.append(region.keyword("pred"), this::oneSpace); |
74 | doc.append(region.feature(ProblemPackage.Literals.NAMED_ELEMENT__NAME), this::noSpace); | 73 | doc.append(region.feature(ProblemPackage.Literals.NAMED_ELEMENT__NAME), this::noSpace); |
75 | formatParenthesizedList(region, doc); | 74 | formatParenthesizedList(region, doc); |
@@ -98,12 +97,14 @@ public class ProblemFormatter extends AbstractJavaFormatter { | |||
98 | 97 | ||
99 | protected void format(NegativeLiteral literal, IFormattableDocument doc) { | 98 | protected void format(NegativeLiteral literal, IFormattableDocument doc) { |
100 | var region = regionFor(literal); | 99 | var region = regionFor(literal); |
100 | doc.append(region.feature(ProblemPackage.Literals.LITERAL__MODALITY), this::oneSpace); | ||
101 | doc.append(region.keyword("!"), this::noSpace); | 101 | doc.append(region.keyword("!"), this::noSpace); |
102 | doc.format(literal.getAtom()); | 102 | doc.format(literal.getAtom()); |
103 | } | 103 | } |
104 | 104 | ||
105 | protected void format(Atom atom, IFormattableDocument doc) { | 105 | protected void format(Atom atom, IFormattableDocument doc) { |
106 | var region = regionFor(atom); | 106 | var region = regionFor(atom); |
107 | doc.append(region.feature(ProblemPackage.Literals.LITERAL__MODALITY), this::oneSpace); | ||
107 | doc.append(region.feature(ProblemPackage.Literals.ATOM__RELATION), this::noSpace); | 108 | doc.append(region.feature(ProblemPackage.Literals.ATOM__RELATION), this::noSpace); |
108 | doc.append(region.feature(ProblemPackage.Literals.ATOM__TRANSITIVE_CLOSURE), this::noSpace); | 109 | doc.append(region.feature(ProblemPackage.Literals.ATOM__TRANSITIVE_CLOSURE), this::noSpace); |
109 | formatParenthesizedList(region, doc); | 110 | formatParenthesizedList(region, doc); |
diff --git a/subprojects/language/src/main/java/tools/refinery/language/resource/DerivedVariableComputer.java b/subprojects/language/src/main/java/tools/refinery/language/resource/DerivedVariableComputer.java index bb1226c4..4d19006f 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/resource/DerivedVariableComputer.java +++ b/subprojects/language/src/main/java/tools/refinery/language/resource/DerivedVariableComputer.java | |||
@@ -29,7 +29,6 @@ import tools.refinery.language.model.problem.Problem; | |||
29 | import tools.refinery.language.model.problem.ProblemFactory; | 29 | import tools.refinery.language.model.problem.ProblemFactory; |
30 | import tools.refinery.language.model.problem.ProblemPackage; | 30 | import tools.refinery.language.model.problem.ProblemPackage; |
31 | import tools.refinery.language.model.problem.Statement; | 31 | import tools.refinery.language.model.problem.Statement; |
32 | import tools.refinery.language.model.problem.ValueLiteral; | ||
33 | import tools.refinery.language.model.problem.VariableOrNodeArgument; | 32 | import tools.refinery.language.model.problem.VariableOrNodeArgument; |
34 | import tools.refinery.language.naming.NamingUtil; | 33 | import tools.refinery.language.naming.NamingUtil; |
35 | 34 | ||
@@ -72,9 +71,6 @@ public class DerivedVariableComputer { | |||
72 | for (Literal literal : conjunction.getLiterals()) { | 71 | for (Literal literal : conjunction.getLiterals()) { |
73 | if (literal instanceof Atom atom) { | 72 | if (literal instanceof Atom atom) { |
74 | createSigletonVariablesAndCollectVariables(atom, knownVariables, newVariables); | 73 | createSigletonVariablesAndCollectVariables(atom, knownVariables, newVariables); |
75 | } else | ||
76 | if (literal instanceof ValueLiteral valueLiteral) { | ||
77 | createSigletonVariablesAndCollectVariables(valueLiteral.getAtom(), knownVariables, newVariables); | ||
78 | } | 74 | } |
79 | } | 75 | } |
80 | createVariables(conjunction, newVariables); | 76 | createVariables(conjunction, newVariables); |
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 7a3e77a4..925ac3a5 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 | |||
@@ -13,10 +13,10 @@ import org.eclipse.xtext.scoping.IScope; | |||
13 | import org.eclipse.xtext.scoping.Scopes; | 13 | import org.eclipse.xtext.scoping.Scopes; |
14 | 14 | ||
15 | import tools.refinery.language.ProblemUtil; | 15 | import tools.refinery.language.ProblemUtil; |
16 | import tools.refinery.language.model.problem.Action; | ||
17 | import tools.refinery.language.model.problem.ClassDeclaration; | 16 | import tools.refinery.language.model.problem.ClassDeclaration; |
17 | import tools.refinery.language.model.problem.Consequent; | ||
18 | import tools.refinery.language.model.problem.ExistentialQuantifier; | 18 | import tools.refinery.language.model.problem.ExistentialQuantifier; |
19 | import tools.refinery.language.model.problem.NewActionLiteral; | 19 | import tools.refinery.language.model.problem.NewAction; |
20 | import tools.refinery.language.model.problem.ParametricDefinition; | 20 | import tools.refinery.language.model.problem.ParametricDefinition; |
21 | import tools.refinery.language.model.problem.Problem; | 21 | import tools.refinery.language.model.problem.Problem; |
22 | import tools.refinery.language.model.problem.ProblemPackage; | 22 | import tools.refinery.language.model.problem.ProblemPackage; |
@@ -41,7 +41,8 @@ public class ProblemScopeProvider extends AbstractProblemScopeProvider { | |||
41 | return getNodesScope(context, scope); | 41 | return getNodesScope(context, scope); |
42 | } | 42 | } |
43 | if (reference == ProblemPackage.Literals.VARIABLE_OR_NODE_ARGUMENT__VARIABLE_OR_NODE | 43 | if (reference == ProblemPackage.Literals.VARIABLE_OR_NODE_ARGUMENT__VARIABLE_OR_NODE |
44 | || reference == ProblemPackage.Literals.DELETE_ACTION_LITERAL__VARIABLE_OR_NODE) { | 44 | || reference == ProblemPackage.Literals.NEW_ACTION__PARENT |
45 | || reference == ProblemPackage.Literals.DELETE_ACTION__VARIABLE_OR_NODE) { | ||
45 | return getVariableScope(context, scope); | 46 | return getVariableScope(context, scope); |
46 | } | 47 | } |
47 | if (reference == ProblemPackage.Literals.REFERENCE_DECLARATION__OPPOSITE) { | 48 | if (reference == ProblemPackage.Literals.REFERENCE_DECLARATION__OPPOSITE) { |
@@ -60,32 +61,39 @@ public class ProblemScopeProvider extends AbstractProblemScopeProvider { | |||
60 | 61 | ||
61 | protected IScope getVariableScope(EObject context, IScope delegateScope) { | 62 | protected IScope getVariableScope(EObject context, IScope delegateScope) { |
62 | List<Variable> variables = new ArrayList<>(); | 63 | List<Variable> variables = new ArrayList<>(); |
64 | addSingletonVariableToScope(context, variables); | ||
63 | EObject currentContext = context; | 65 | EObject currentContext = context; |
66 | while (currentContext != null && !(currentContext instanceof ParametricDefinition)) { | ||
67 | addExistentiallyQualifiedVariableToScope(currentContext, variables); | ||
68 | currentContext = currentContext.eContainer(); | ||
69 | } | ||
70 | IScope parentScope = getNodesScope(context, delegateScope); | ||
71 | if (currentContext != null) { | ||
72 | ParametricDefinition definition = (ParametricDefinition) currentContext; | ||
73 | parentScope = Scopes.scopeFor(definition.getParameters(), parentScope); | ||
74 | } | ||
75 | return Scopes.scopeFor(variables, parentScope); | ||
76 | } | ||
77 | |||
78 | protected void addSingletonVariableToScope(EObject context, List<Variable> variables) { | ||
64 | if (context instanceof VariableOrNodeArgument argument) { | 79 | if (context instanceof VariableOrNodeArgument argument) { |
65 | Variable singletonVariable = argument.getSingletonVariable(); | 80 | Variable singletonVariable = argument.getSingletonVariable(); |
66 | if (singletonVariable != null) { | 81 | if (singletonVariable != null) { |
67 | variables.add(singletonVariable); | 82 | variables.add(singletonVariable); |
68 | } | 83 | } |
69 | } | 84 | } |
70 | while (currentContext != null && !(currentContext instanceof ParametricDefinition)) { | 85 | } |
71 | if (currentContext instanceof ExistentialQuantifier quantifier) { | 86 | |
72 | variables.addAll(quantifier.getImplicitVariables()); | 87 | protected void addExistentiallyQualifiedVariableToScope(EObject currentContext, List<Variable> variables) { |
73 | } else | 88 | if (currentContext instanceof ExistentialQuantifier quantifier) { |
74 | if(currentContext instanceof Action action) { | 89 | variables.addAll(quantifier.getImplicitVariables()); |
75 | for (var literal : action.getActionLiterals()) { | 90 | } else if (currentContext instanceof Consequent consequent) { |
76 | if(literal instanceof NewActionLiteral newActionLiteral && newActionLiteral.getVariable() != null) { | 91 | for (var literal : consequent.getActions()) { |
77 | variables.add(newActionLiteral.getVariable()); | 92 | if (literal instanceof NewAction newAction && newAction.getVariable() != null) { |
78 | } | 93 | variables.add(newAction.getVariable()); |
79 | } | 94 | } |
80 | } | 95 | } |
81 | currentContext = currentContext.eContainer(); | ||
82 | } | ||
83 | IScope parentScope = getNodesScope(context, delegateScope); | ||
84 | if (currentContext != null) { | ||
85 | ParametricDefinition definition = (ParametricDefinition) currentContext; | ||
86 | parentScope = Scopes.scopeFor(definition.getParameters(),parentScope); | ||
87 | } | 96 | } |
88 | return Scopes.scopeFor(variables,parentScope); | ||
89 | } | 97 | } |
90 | 98 | ||
91 | protected IScope getOppositeScope(EObject context, IScope delegateScope) { | 99 | protected IScope getOppositeScope(EObject context, IScope delegateScope) { |