diff options
author | 2024-02-20 01:27:51 +0100 | |
---|---|---|
committer | 2024-04-07 14:55:46 +0200 | |
commit | 01960723de5ca42e28dc8f162d4fe9e24c23c0b8 (patch) | |
tree | c391738a378d079d4c3b1aa8966c6b66d60ee4c9 /subprojects/language/src/main/java/tools | |
parent | feat: subproject for z3 integration (diff) | |
download | refinery-01960723de5ca42e28dc8f162d4fe9e24c23c0b8.tar.gz refinery-01960723de5ca42e28dc8f162d4fe9e24c23c0b8.tar.zst refinery-01960723de5ca42e28dc8f162d4fe9e24c23c0b8.zip |
feat(language): datatype declarations
Also changes ReferenceDeclaration to declare attributes, since reference and
attributes can only be distinguished at linking time.
Diffstat (limited to 'subprojects/language/src/main/java/tools')
5 files changed, 22 insertions, 33 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 f0d6c38c..a2fea627 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext +++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext | |||
@@ -17,7 +17,7 @@ enum ModuleKind: | |||
17 | 17 | ||
18 | Statement: | 18 | Statement: |
19 | ImportStatement | Assertion | ClassDeclaration | EnumDeclaration | | 19 | ImportStatement | Assertion | ClassDeclaration | EnumDeclaration | |
20 | PredicateDefinition | /* FunctionDefinition | RuleDefinition | */ | 20 | DatatypeDeclaration | PredicateDefinition | /* FunctionDefinition | RuleDefinition | */ |
21 | ScopeDeclaration | NodeDeclaration; | 21 | ScopeDeclaration | NodeDeclaration; |
22 | 22 | ||
23 | ImportStatement: | 23 | ImportStatement: |
@@ -27,7 +27,7 @@ ClassDeclaration: | |||
27 | abstract?="abstract"? "class" | 27 | abstract?="abstract"? "class" |
28 | name=Identifier | 28 | name=Identifier |
29 | ("extends" superTypes+=[Relation|QualifiedName] ("," superTypes+=[Relation|QualifiedName])*)? | 29 | ("extends" superTypes+=[Relation|QualifiedName] ("," superTypes+=[Relation|QualifiedName])*)? |
30 | ("{" (featureDeclarations+=FeatureDeclaration ";"?)* "}" | "."); | 30 | ("{" (featureDeclarations+=ReferenceDeclaration ";"?)* "}" | "."); |
31 | 31 | ||
32 | EnumDeclaration: | 32 | EnumDeclaration: |
33 | "enum" | 33 | "enum" |
@@ -37,8 +37,8 @@ EnumDeclaration: | |||
37 | EnumLiteral returns Node: | 37 | EnumLiteral returns Node: |
38 | name=Identifier; | 38 | name=Identifier; |
39 | 39 | ||
40 | FeatureDeclaration: | 40 | DatatypeDeclaration: |
41 | ReferenceDeclaration /* | AttributeDeclaration | FlagDeclaration */; | 41 | "extern" "datatype" name=Identifier "."; |
42 | 42 | ||
43 | enum ReferenceKind: | 43 | enum ReferenceKind: |
44 | REFERENCE="refers" | CONTAINMENT="contains" | CONTAINER="container"; | 44 | REFERENCE="refers" | CONTAINMENT="contains" | CONTAINER="container"; |
@@ -53,15 +53,6 @@ ReferenceDeclaration: | |||
53 | ReferenceMultiplicity returns Multiplicity: | 53 | ReferenceMultiplicity returns Multiplicity: |
54 | "[" Multiplicity "]"; | 54 | "[" Multiplicity "]"; |
55 | 55 | ||
56 | //enum PrimitiveType: | ||
57 | // INT="int" | REAL="real" | STRING="string"; | ||
58 | // | ||
59 | //AttributeDeclaration: | ||
60 | // attributeType=PrimitiveType name=Identifier; | ||
61 | // | ||
62 | //FlagDeclaration: | ||
63 | // "bool" name=Identifier; | ||
64 | |||
65 | PredicateDefinition: | 56 | PredicateDefinition: |
66 | ("pred" | error?="error" "pred"?) | 57 | ("pred" | error?="error" "pred"?) |
67 | name=Identifier | 58 | name=Identifier |
@@ -73,7 +64,7 @@ Conjunction: | |||
73 | literals+=Expr ("," literals+=Expr)*; | 64 | literals+=Expr ("," literals+=Expr)*; |
74 | 65 | ||
75 | //FunctionDefinition: | 66 | //FunctionDefinition: |
76 | // "fn" functionType=PrimitiveType name=Identifier | 67 | // "fn" functionType=[DatatypeDefinition|QualifiedName] name=Identifier |
77 | // "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")" | 68 | // "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")" |
78 | // ("=" cases+=Case (";" cases+=Case)*)? | 69 | // ("=" cases+=Case (";" cases+=Case)*)? |
79 | // "."; | 70 | // "."; |
diff --git a/subprojects/language/src/main/java/tools/refinery/language/resource/state/ProblemDerivedStateComputer.java b/subprojects/language/src/main/java/tools/refinery/language/resource/state/ProblemDerivedStateComputer.java index d905aa9a..efa77c50 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/resource/state/ProblemDerivedStateComputer.java +++ b/subprojects/language/src/main/java/tools/refinery/language/resource/state/ProblemDerivedStateComputer.java | |||
@@ -1,5 +1,5 @@ | |||
1 | /* | 1 | /* |
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | 2 | * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors <https://refinery.tools/> |
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
@@ -51,7 +51,7 @@ public class ProblemDerivedStateComputer implements IDerivedStateComputer { | |||
51 | if (contents.isEmpty()) { | 51 | if (contents.isEmpty()) { |
52 | return null; | 52 | return null; |
53 | } | 53 | } |
54 | EObject object = contents.get(0); | 54 | EObject object = contents.getFirst(); |
55 | if (object instanceof Problem problem) { | 55 | if (object instanceof Problem problem) { |
56 | return problem; | 56 | return problem; |
57 | } | 57 | } |
@@ -71,10 +71,8 @@ public class ProblemDerivedStateComputer implements IDerivedStateComputer { | |||
71 | for (var statement : problem.getStatements()) { | 71 | for (var statement : problem.getStatements()) { |
72 | if (statement instanceof ClassDeclaration classDeclaration) { | 72 | if (statement instanceof ClassDeclaration classDeclaration) { |
73 | installOrRemoveNewNode(adapter, classDeclaration); | 73 | installOrRemoveNewNode(adapter, classDeclaration); |
74 | for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) { | 74 | for (var referenceDeclaration : classDeclaration.getFeatureDeclarations()) { |
75 | if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) { | 75 | installOrRemoveInvalidMultiplicityPredicate(adapter, classDeclaration, referenceDeclaration); |
76 | installOrRemoveInvalidMultiplicityPredicate(adapter, classDeclaration, referenceDeclaration); | ||
77 | } | ||
78 | } | 76 | } |
79 | } | 77 | } |
80 | } | 78 | } |
@@ -157,9 +155,8 @@ public class ProblemDerivedStateComputer implements IDerivedStateComputer { | |||
157 | if (classDeclaration.isAbstract()) { | 155 | if (classDeclaration.isAbstract()) { |
158 | abstractClassDeclarations.add(classDeclaration); | 156 | abstractClassDeclarations.add(classDeclaration); |
159 | } | 157 | } |
160 | for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) { | 158 | for (var referenceDeclaration : classDeclaration.getFeatureDeclarations()) { |
161 | if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration && | 159 | if (ProblemUtil.hasMultiplicityConstraint(referenceDeclaration)) { |
162 | ProblemUtil.hasMultiplicityConstraint(referenceDeclaration)) { | ||
163 | referenceDeclarationsWithMultiplicity.add(referenceDeclaration); | 160 | referenceDeclarationsWithMultiplicity.add(referenceDeclaration); |
164 | } | 161 | } |
165 | } | 162 | } |
diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemDesugarer.java b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemDesugarer.java index 0bd1e50b..d45c8083 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemDesugarer.java +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemDesugarer.java | |||
@@ -87,11 +87,7 @@ public class ProblemDesugarer { | |||
87 | private Collection<ReferenceDeclaration> doGetAllReferenceDeclarations(ClassDeclaration classDeclaration) { | 87 | private Collection<ReferenceDeclaration> doGetAllReferenceDeclarations(ClassDeclaration classDeclaration) { |
88 | Set<ReferenceDeclaration> referenceDeclarations = new HashSet<>(); | 88 | Set<ReferenceDeclaration> referenceDeclarations = new HashSet<>(); |
89 | for (ClassDeclaration superclass : getSuperclassesAndSelf(classDeclaration)) { | 89 | for (ClassDeclaration superclass : getSuperclassesAndSelf(classDeclaration)) { |
90 | for (FeatureDeclaration featureDeclaration : superclass.getFeatureDeclarations()) { | 90 | referenceDeclarations.addAll(superclass.getFeatureDeclarations()); |
91 | if (featureDeclaration instanceof ReferenceDeclaration referenceDeclaration) { | ||
92 | referenceDeclarations.add(referenceDeclaration); | ||
93 | } | ||
94 | } | ||
95 | } | 91 | } |
96 | return referenceDeclarations; | 92 | return referenceDeclarations; |
97 | } | 93 | } |
diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java index f70893e0..6d6d65da 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java | |||
@@ -1,5 +1,5 @@ | |||
1 | /* | 1 | /* |
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | 2 | * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors <https://refinery.tools/> |
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
@@ -81,6 +81,9 @@ public final class ProblemUtil { | |||
81 | } | 81 | } |
82 | 82 | ||
83 | public static boolean hasMultiplicityConstraint(ReferenceDeclaration referenceDeclaration) { | 83 | public static boolean hasMultiplicityConstraint(ReferenceDeclaration referenceDeclaration) { |
84 | if (referenceDeclaration.getReferenceType() instanceof DatatypeDeclaration) { | ||
85 | return false; | ||
86 | } | ||
84 | var opposite = referenceDeclaration.getOpposite(); | 87 | var opposite = referenceDeclaration.getOpposite(); |
85 | if (opposite != null && opposite.getKind() == ReferenceKind.CONTAINMENT) { | 88 | if (opposite != null && opposite.getKind() == ReferenceKind.CONTAINMENT) { |
86 | return false; | 89 | return false; |
@@ -96,7 +99,8 @@ public final class ProblemUtil { | |||
96 | } | 99 | } |
97 | 100 | ||
98 | public static int getArity(Relation relation) { | 101 | public static int getArity(Relation relation) { |
99 | if (relation instanceof ClassDeclaration || relation instanceof EnumDeclaration) { | 102 | if (relation instanceof ClassDeclaration || relation instanceof EnumDeclaration || |
103 | relation instanceof DatatypeDeclaration) { | ||
100 | return 1; | 104 | return 1; |
101 | } | 105 | } |
102 | if (relation instanceof ReferenceDeclaration) { | 106 | if (relation instanceof ReferenceDeclaration) { |
@@ -116,7 +120,7 @@ public final class ProblemUtil { | |||
116 | return switch (kind) { | 120 | return switch (kind) { |
117 | case CONTAINMENT -> false; | 121 | case CONTAINMENT -> false; |
118 | case CONTAINER -> true; | 122 | case CONTAINER -> true; |
119 | case REFERENCE -> { | 123 | case DEFAULT, REFERENCE -> { |
120 | var opposite = referenceDeclaration.getOpposite(); | 124 | var opposite = referenceDeclaration.getOpposite(); |
121 | if (opposite == null) { | 125 | if (opposite == null) { |
122 | yield false; | 126 | yield false; |
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 d9eb5fd3..560f612a 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 | |||
@@ -315,8 +315,9 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
315 | 315 | ||
316 | @Check | 316 | @Check |
317 | public void checkReferenceType(ReferenceDeclaration referenceDeclaration) { | 317 | public void checkReferenceType(ReferenceDeclaration referenceDeclaration) { |
318 | if (referenceDeclaration.getKind() == ReferenceKind.REFERENCE && | 318 | boolean isDefaultReference = referenceDeclaration.getKind() == ReferenceKind.DEFAULT && |
319 | !ProblemUtil.isContainerReference(referenceDeclaration)) { | 319 | !ProblemUtil.isContainerReference(referenceDeclaration); |
320 | if (isDefaultReference || referenceDeclaration.getKind() == ReferenceKind.REFERENCE) { | ||
320 | checkArity(referenceDeclaration, ProblemPackage.Literals.REFERENCE_DECLARATION__REFERENCE_TYPE, 1); | 321 | checkArity(referenceDeclaration, ProblemPackage.Literals.REFERENCE_DECLARATION__REFERENCE_TYPE, 1); |
321 | return; | 322 | return; |
322 | } | 323 | } |