aboutsummaryrefslogtreecommitdiffstats
path: root/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language
diff options
context:
space:
mode:
Diffstat (limited to 'org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language')
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/GenerateProblem.mwe254
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext88
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/ProblemRuntimeModule.java86
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/ProblemStandaloneSetup.java26
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/conversion/ProblemValueConverterService.java17
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/conversion/UpperBoundValueConverter.java35
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/generator/ProblemGenerator.xtend25
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/naming/ProblemQualifiedNameConverter.java13
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/naming/ProblemQualifiedNameProvider.java15
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemDerivedStateComputer.java218
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemLocationInFileProvider.java130
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemResourceDescriptionStrategy.java39
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/scoping/ProblemGlobalScopeProvider.java19
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/scoping/ProblemScopeProvider.java74
-rw-r--r--org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/validation/ProblemValidator.java25
15 files changed, 864 insertions, 0 deletions
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/GenerateProblem.mwe2 b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/GenerateProblem.mwe2
new file mode 100644
index 00000000..46812355
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/GenerateProblem.mwe2
@@ -0,0 +1,54 @@
1module org.eclipse.viatra.solver.language.GenerateProblem
2
3import org.eclipse.xtext.xtext.generator.*
4import org.eclipse.xtext.xtext.generator.model.project.*
5
6var rootPath = ".."
7
8Workflow {
9 component = XtextGenerator {
10 configuration = {
11 project = StandardProjectConfig {
12 baseName = "org.eclipse.viatra.solver.language"
13 rootPath = rootPath
14 runtimeTest = {
15 enabled = true
16 }
17 web = {
18 enabled = true
19 }
20 mavenLayout = true
21 }
22 code = {
23 encoding = "UTF-8"
24 lineDelimiter = "\n"
25 fileHeader = "/*\n * generated by Xtext \${version}\n */"
26 preferXtendStubs = false
27 }
28 }
29
30 language = StandardLanguage {
31 name = "org.eclipse.viatra.solver.language.Problem"
32 fileExtensions = "problem"
33 referencedResource = "platform:/resource/org.eclipse.viatra.solver.language.model/model/problem.genmodel"
34
35 serializer = {
36 generateStub = false
37 }
38 validator = {
39 // composedCheck = "org.eclipse.xtext.validation.NamesAreUniqueValidator"
40 // Generates checks for @Deprecated grammar annotations, an IssueProvider and a corresponding PropertyPage
41 generateDeprecationValidation = true
42 }
43 generator = {
44 generateXtendStub = true
45 }
46 junitSupport = {
47 junitVersion = "5"
48 }
49 webSupport = {
50 framework = "CodeMirror"
51 }
52 }
53 }
54}
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext
new file mode 100644
index 00000000..81c18d0d
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext
@@ -0,0 +1,88 @@
1grammar org.eclipse.viatra.solver.language.Problem with org.eclipse.xtext.common.Terminals
2
3import "http://www.eclipse.org/emf/2002/Ecore" as ecore
4import "http://www.eclipse.org/viatra/solver/language/model/Problem"
5
6Problem:
7 statements+=Statement*;
8
9Statement:
10 ClassDeclaration | PredicateDefinition | Assertion | ScopeDeclaration;
11
12ClassDeclaration:
13 abstract?="abstract"? "class"
14 name=ID
15 ("extends" (superTypes+=[ClassDeclaration] |
16 "[" (superTypes+=[ClassDeclaration] ("," superTypes+=[ClassDeclaration])*)? "]") |
17 referenceDeclarations+=ReferenceDeclaration)?
18 ("," referenceDeclarations+=ReferenceDeclaration)*
19 ".";
20
21ReferenceDeclaration:
22 (containment?="contains" | "refers")
23 referenceType=[ClassDeclaration]
24 "[" multiplicity=Multiplicity "]"
25 name=ID
26 ("opposite" opposite=[ReferenceDeclaration|QualifiedName])?;
27
28PredicateDefinition:
29 (error?="error" "pred"? | "pred")
30 name=ID
31 "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")"
32 (":=" bodies+=Conjunction (";" bodies+=Conjunction)*)?
33 ".";
34
35Parameter:
36 parameterType=[ClassDeclaration] name=ID;
37
38Conjunction:
39 literals+=Literal ("," literals+=Literal)*;
40
41Literal:
42 Atom | NegativeLiteral;
43
44NegativeLiteral:
45 "!" atom=Atom;
46
47Atom:
48 relation=[Relation|QualifiedName]
49 transitiveClosure?="+"?
50 "(" (arguments+=[Variable] ("," arguments+=[Variable])*)? ")";
51
52Assertion:
53 (relation=[Relation|QualifiedName]
54 "(" (arguments+=[Node|QualifiedName] ("," arguments+=[Node|QualifiedName])*)? ")"
55 ":" value=LogicValue |
56 value=ShortLogicValue?
57 relation=[Relation|QualifiedName]
58 "(" (arguments+=[Node|QualifiedName] ("," arguments+=[Node|QualifiedName])*)? ")")
59 ".";
60
61enum LogicValue:
62 TRUE="true" | FALSE="false" | UNKNOWN="unknown";
63
64enum ShortLogicValue returns LogicValue:
65 FALSE="!" | UNKNOWN="?";
66
67ScopeDeclaration:
68 "scope" typeScopes+=TypeScope ("," typeScopes+=TypeScope)* ".";
69
70TypeScope:
71 targetType=[ClassDeclaration]
72 (increment?="+=" | "=")
73 multiplicity=Multiplicity;
74
75Multiplicity:
76 RangeMultiplicity | ExactMultiplicity;
77
78RangeMultiplicity:
79 lowerBound=INT ".." upperBound=UpperBound;
80
81ExactMultiplicity:
82 exactValue=INT;
83
84UpperBound returns ecore::EInt:
85 INT | "*";
86
87QualifiedName:
88 ID ("::" ID)*;
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/ProblemRuntimeModule.java b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/ProblemRuntimeModule.java
new file mode 100644
index 00000000..b2a3218c
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/ProblemRuntimeModule.java
@@ -0,0 +1,86 @@
1/*
2 * generated by Xtext 2.25.0
3 */
4package org.eclipse.viatra.solver.language;
5
6import org.eclipse.viatra.solver.language.conversion.ProblemValueConverterService;
7import org.eclipse.viatra.solver.language.naming.ProblemQualifiedNameConverter;
8import org.eclipse.viatra.solver.language.naming.ProblemQualifiedNameProvider;
9import org.eclipse.viatra.solver.language.resource.ProblemDerivedStateComputer;
10import org.eclipse.viatra.solver.language.resource.ProblemLocationInFileProvider;
11import org.eclipse.viatra.solver.language.resource.ProblemResourceDescriptionStrategy;
12import org.eclipse.viatra.solver.language.scoping.ProblemGlobalScopeProvider;
13import org.eclipse.xtext.conversion.IValueConverterService;
14import org.eclipse.xtext.naming.IQualifiedNameConverter;
15import org.eclipse.xtext.naming.IQualifiedNameProvider;
16import org.eclipse.xtext.resource.DerivedStateAwareResource;
17import org.eclipse.xtext.resource.DerivedStateAwareResourceDescriptionManager;
18import org.eclipse.xtext.resource.IDefaultResourceDescriptionStrategy;
19import org.eclipse.xtext.resource.IDerivedStateComputer;
20import org.eclipse.xtext.resource.ILocationInFileProvider;
21import org.eclipse.xtext.resource.IResourceDescription;
22import org.eclipse.xtext.resource.XtextResource;
23import org.eclipse.xtext.scoping.IGlobalScopeProvider;
24import org.eclipse.xtext.scoping.IScopeProvider;
25import org.eclipse.xtext.scoping.impl.AbstractDeclarativeScopeProvider;
26import org.eclipse.xtext.scoping.impl.SimpleLocalScopeProvider;
27import org.eclipse.xtext.validation.IResourceValidator;
28import org.eclipse.xtext.xbase.annotations.validation.DerivedStateAwareResourceValidator;
29
30import com.google.inject.Binder;
31import com.google.inject.name.Names;
32
33/**
34 * Use this class to register components to be used at runtime / without the
35 * Equinox extension registry.
36 */
37public class ProblemRuntimeModule extends AbstractProblemRuntimeModule {
38 public Class<? extends IQualifiedNameConverter> bindIQualifiedNameConverter() {
39 return ProblemQualifiedNameConverter.class;
40 }
41
42 public Class<? extends IQualifiedNameProvider> bindIQualifiedNameProvider() {
43 return ProblemQualifiedNameProvider.class;
44 }
45
46 public Class<? extends IDefaultResourceDescriptionStrategy> bindIDefaultResourceDescriptionStrategy() {
47 return ProblemResourceDescriptionStrategy.class;
48 }
49
50 @Override
51 public Class<? extends IValueConverterService> bindIValueConverterService() {
52 return ProblemValueConverterService.class;
53 }
54
55 @Override
56 public void configureIScopeProviderDelegate(Binder binder) {
57 binder.bind(IScopeProvider.class).annotatedWith(Names.named(AbstractDeclarativeScopeProvider.NAMED_DELEGATE))
58 .to(SimpleLocalScopeProvider.class);
59 }
60
61 @Override
62 public Class<? extends IGlobalScopeProvider> bindIGlobalScopeProvider() {
63 return ProblemGlobalScopeProvider.class;
64 }
65
66 @Override
67 public Class<? extends XtextResource> bindXtextResource() {
68 return DerivedStateAwareResource.class;
69 }
70
71 public Class<? extends IResourceDescription.Manager> bindIResourceDescription$Manager() {
72 return DerivedStateAwareResourceDescriptionManager.class;
73 }
74
75 public Class<? extends IResourceValidator> bindIResourceValidator() {
76 return DerivedStateAwareResourceValidator.class;
77 }
78
79 public Class<? extends IDerivedStateComputer> bindIDerivedStateComputer() {
80 return ProblemDerivedStateComputer.class;
81 }
82
83 public Class<? extends ILocationInFileProvider> bindILocationInFileProvider() {
84 return ProblemLocationInFileProvider.class;
85 }
86}
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/ProblemStandaloneSetup.java b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/ProblemStandaloneSetup.java
new file mode 100644
index 00000000..5652f859
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/ProblemStandaloneSetup.java
@@ -0,0 +1,26 @@
1/*
2 * generated by Xtext 2.25.0
3 */
4package org.eclipse.viatra.solver.language;
5
6import org.eclipse.emf.ecore.EPackage;
7import org.eclipse.viatra.solver.language.model.problem.ProblemPackage;
8
9import com.google.inject.Injector;
10
11/**
12 * Initialization support for running Xtext languages without Equinox extension registry.
13 */
14public class ProblemStandaloneSetup extends ProblemStandaloneSetupGenerated {
15
16 public static void doSetup() {
17 new ProblemStandaloneSetup().createInjectorAndDoEMFRegistration();
18 }
19
20 @Override
21 public Injector createInjectorAndDoEMFRegistration() {
22 if (!EPackage.Registry.INSTANCE.containsKey(ProblemPackage.eNS_URI))
23 EPackage.Registry.INSTANCE.put(ProblemPackage.eNS_URI, ProblemPackage.eINSTANCE);
24 return super.createInjectorAndDoEMFRegistration();
25 }
26}
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/conversion/ProblemValueConverterService.java b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/conversion/ProblemValueConverterService.java
new file mode 100644
index 00000000..4f5fd069
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/conversion/ProblemValueConverterService.java
@@ -0,0 +1,17 @@
1package org.eclipse.viatra.solver.language.conversion;
2
3import org.eclipse.xtext.common.services.DefaultTerminalConverters;
4import org.eclipse.xtext.conversion.IValueConverter;
5import org.eclipse.xtext.conversion.ValueConverter;
6
7import com.google.inject.Inject;
8
9public class ProblemValueConverterService extends DefaultTerminalConverters {
10 @Inject
11 private UpperBoundValueConverter upperBoundValueConverter;
12
13 @ValueConverter(rule = "UpperBound")
14 public IValueConverter<Integer> UpperBound() {
15 return upperBoundValueConverter;
16 }
17}
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/conversion/UpperBoundValueConverter.java b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/conversion/UpperBoundValueConverter.java
new file mode 100644
index 00000000..3111b69b
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/conversion/UpperBoundValueConverter.java
@@ -0,0 +1,35 @@
1package org.eclipse.viatra.solver.language.conversion;
2
3import org.eclipse.xtext.conversion.ValueConverterException;
4import org.eclipse.xtext.conversion.impl.AbstractValueConverter;
5import org.eclipse.xtext.conversion.impl.INTValueConverter;
6import org.eclipse.xtext.nodemodel.INode;
7
8import com.google.inject.Inject;
9import com.google.inject.Singleton;
10
11@Singleton
12public class UpperBoundValueConverter extends AbstractValueConverter<Integer> {
13 public static final String INFINITY = "*";
14
15 @Inject
16 private INTValueConverter intValueConverter;
17
18 @Override
19 public Integer toValue(String string, INode node) throws ValueConverterException {
20 if (INFINITY.equals(string)) {
21 return -1;
22 } else {
23 return intValueConverter.toValue(string, node);
24 }
25 }
26
27 @Override
28 public String toString(Integer value) throws ValueConverterException {
29 if (value < 0) {
30 return INFINITY;
31 } else {
32 return intValueConverter.toString(value);
33 }
34 }
35}
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/generator/ProblemGenerator.xtend b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/generator/ProblemGenerator.xtend
new file mode 100644
index 00000000..0930f244
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/generator/ProblemGenerator.xtend
@@ -0,0 +1,25 @@
1/*
2 * generated by Xtext 2.25.0
3 */
4package org.eclipse.viatra.solver.language.generator
5
6import org.eclipse.emf.ecore.resource.Resource
7import org.eclipse.xtext.generator.AbstractGenerator
8import org.eclipse.xtext.generator.IFileSystemAccess2
9import org.eclipse.xtext.generator.IGeneratorContext
10
11/**
12 * Generates code from your model files on save.
13 *
14 * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#code-generation
15 */
16class ProblemGenerator extends AbstractGenerator {
17
18 override void doGenerate(Resource resource, IFileSystemAccess2 fsa, IGeneratorContext context) {
19// fsa.generateFile('greetings.txt', 'People to greet: ' +
20// resource.allContents
21// .filter(Greeting)
22// .map[name]
23// .join(', '))
24 }
25}
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/naming/ProblemQualifiedNameConverter.java b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/naming/ProblemQualifiedNameConverter.java
new file mode 100644
index 00000000..ebb7e7b4
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/naming/ProblemQualifiedNameConverter.java
@@ -0,0 +1,13 @@
1package org.eclipse.viatra.solver.language.naming;
2
3import org.eclipse.xtext.naming.IQualifiedNameConverter;
4
5import com.google.inject.Singleton;
6
7@Singleton
8public class ProblemQualifiedNameConverter extends IQualifiedNameConverter.DefaultImpl {
9 @Override
10 public String getDelimiter() {
11 return "::";
12 }
13}
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/naming/ProblemQualifiedNameProvider.java b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/naming/ProblemQualifiedNameProvider.java
new file mode 100644
index 00000000..81365724
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/naming/ProblemQualifiedNameProvider.java
@@ -0,0 +1,15 @@
1package org.eclipse.viatra.solver.language.naming;
2
3import org.eclipse.viatra.solver.language.model.problem.Node;
4import org.eclipse.xtext.naming.DefaultDeclarativeQualifiedNameProvider;
5import org.eclipse.xtext.naming.QualifiedName;
6
7public class ProblemQualifiedNameProvider extends DefaultDeclarativeQualifiedNameProvider {
8 public QualifiedName qualifiedName(Node node) {
9 String name = node.getName();
10 if (name == null || name.isEmpty()) {
11 return null;
12 }
13 return getConverter().toQualifiedName(name);
14 }
15}
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemDerivedStateComputer.java b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemDerivedStateComputer.java
new file mode 100644
index 00000000..571b5745
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemDerivedStateComputer.java
@@ -0,0 +1,218 @@
1package org.eclipse.viatra.solver.language.resource;
2
3import java.util.HashSet;
4import java.util.List;
5import java.util.Set;
6import java.util.regex.Pattern;
7
8import org.eclipse.emf.ecore.EObject;
9import org.eclipse.viatra.solver.language.model.problem.Assertion;
10import org.eclipse.viatra.solver.language.model.problem.Atom;
11import org.eclipse.viatra.solver.language.model.problem.ClassDeclaration;
12import org.eclipse.viatra.solver.language.model.problem.Conjunction;
13import org.eclipse.viatra.solver.language.model.problem.ExistentialQuantifier;
14import org.eclipse.viatra.solver.language.model.problem.ImplicitVariable;
15import org.eclipse.viatra.solver.language.model.problem.Literal;
16import org.eclipse.viatra.solver.language.model.problem.NegativeLiteral;
17import org.eclipse.viatra.solver.language.model.problem.Node;
18import org.eclipse.viatra.solver.language.model.problem.Parameter;
19import org.eclipse.viatra.solver.language.model.problem.PredicateDefinition;
20import org.eclipse.viatra.solver.language.model.problem.Problem;
21import org.eclipse.viatra.solver.language.model.problem.ProblemFactory;
22import org.eclipse.viatra.solver.language.model.problem.ProblemPackage;
23import org.eclipse.viatra.solver.language.model.problem.Statement;
24import org.eclipse.xtext.linking.impl.LinkingHelper;
25import org.eclipse.xtext.naming.IQualifiedNameConverter;
26import org.eclipse.xtext.naming.QualifiedName;
27import org.eclipse.xtext.nodemodel.INode;
28import org.eclipse.xtext.nodemodel.util.NodeModelUtils;
29import org.eclipse.xtext.resource.DerivedStateAwareResource;
30import org.eclipse.xtext.resource.IDerivedStateComputer;
31import org.eclipse.xtext.scoping.IGlobalScopeProvider;
32import org.eclipse.xtext.scoping.IScope;
33
34import com.google.common.base.Predicates;
35import com.google.inject.Inject;
36import com.google.inject.Singleton;
37
38@Singleton
39public class ProblemDerivedStateComputer implements IDerivedStateComputer {
40 public static final String NEW_NODE = "new";
41
42 private static final String ID_REGEX_STRING = "[_a-zA-Z][_0-9a-zA-Z]*";
43
44 private static final Pattern ID_REGEX = Pattern.compile(ID_REGEX_STRING);
45
46 private static final Pattern QUALIFIED_NAME_REGEX = Pattern
47 .compile(ID_REGEX_STRING + "(::" + ID_REGEX_STRING + ")*");
48
49 @Inject
50 private LinkingHelper linkingHelper;
51
52 @Inject
53 private IQualifiedNameConverter qualifiedNameConverter;
54
55 @Inject
56 private IGlobalScopeProvider scopeProvider;
57
58 @Override
59 public void installDerivedState(DerivedStateAwareResource resource, boolean preLinkingPhase) {
60 for (EObject object : resource.getContents()) {
61 if (object instanceof Problem) {
62 installDerivedProblemState((Problem) object, preLinkingPhase);
63 }
64 }
65 }
66
67 protected void installDerivedProblemState(Problem problem, boolean preLinkingPhase) {
68 Set<String> nodeNames = new HashSet<>();
69 if (!preLinkingPhase) {
70 installDerivedNodes(problem);
71 }
72 for (Statement statement : problem.getStatements()) {
73 if (statement instanceof PredicateDefinition) {
74 PredicateDefinition definition = (PredicateDefinition) statement;
75 installDerivedPredicateDefinitionState(definition);
76 }
77 }
78 List<Node> grapNodes = problem.getNodes();
79 for (String nodeName : nodeNames) {
80 Node graphNode = ProblemFactory.eINSTANCE.createNode();
81 graphNode.setName(nodeName);
82 grapNodes.add(graphNode);
83 }
84 }
85
86 protected void installDerivedNodes(Problem problem) {
87 IScope nodeScope = scopeProvider.getScope(problem.eResource(), ProblemPackage.Literals.ASSERTION__ARGUMENTS,
88 Predicates.alwaysTrue());
89 Set<String> nodeNames = new HashSet<>();
90 for (Statement statement : problem.getStatements()) {
91 if (statement instanceof ClassDeclaration) {
92 ClassDeclaration declaration = (ClassDeclaration) statement;
93 if (!declaration.isAbstract()) {
94 String className = declaration.getName();
95 if (validId(className)) {
96 QualifiedName qualifiedName = QualifiedName.create(className, NEW_NODE);
97 String nodeName = qualifiedNameConverter.toString(qualifiedName);
98 nodeNames.add(nodeName);
99 }
100 }
101 }
102 }
103 for (Statement statement : problem.getStatements()) {
104 if (statement instanceof Assertion) {
105 Assertion assertion = (Assertion) statement;
106 List<INode> nodes = NodeModelUtils.findNodesForFeature(assertion,
107 ProblemPackage.Literals.ASSERTION__ARGUMENTS);
108 for (INode node : nodes) {
109 String nodeName = linkingHelper.getCrossRefNodeAsString(node, true);
110 if (validQualifiedName(nodeName)) {
111 QualifiedName qualifiedName = qualifiedNameConverter.toQualifiedName(nodeName);
112 if (nodeScope.getSingleElement(qualifiedName) == null) {
113 nodeNames.add(nodeName);
114 }
115 }
116 }
117 }
118 }
119 List<Node> grapNodes = problem.getNodes();
120 for (String nodeName : nodeNames) {
121 Node graphNode = ProblemFactory.eINSTANCE.createNode();
122 graphNode.setName(nodeName);
123 grapNodes.add(graphNode);
124 }
125 }
126
127 protected void installDerivedPredicateDefinitionState(PredicateDefinition definition) {
128 Set<String> parameterNames = new HashSet<>();
129 for (Parameter parameter : definition.getParameters()) {
130 String name = parameter.getName();
131 if (name != null) {
132 parameterNames.add(name);
133 }
134 }
135 for (Conjunction body : definition.getBodies()) {
136 installDeriveConjunctionState(body, parameterNames);
137 }
138 }
139
140 protected void installDeriveConjunctionState(Conjunction conjunction, Set<String> knownVariables) {
141 Set<String> newVariables = new HashSet<>();
142 for (Literal literal : conjunction.getLiterals()) {
143 if (literal instanceof Atom) {
144 Atom atom = (Atom) literal;
145 collectVariables(atom, knownVariables, newVariables);
146 }
147 }
148 createVariables(conjunction, newVariables);
149 newVariables.addAll(knownVariables);
150 for (Literal literal : conjunction.getLiterals()) {
151 if (literal instanceof NegativeLiteral) {
152 NegativeLiteral negativeLiteral = (NegativeLiteral) literal;
153 installDeriveNegativeLiteralState(negativeLiteral, newVariables);
154 }
155 }
156 }
157
158 protected void installDeriveNegativeLiteralState(NegativeLiteral negativeLiteral, Set<String> knownVariables) {
159 Set<String> newVariables = new HashSet<>();
160 collectVariables(negativeLiteral.getAtom(), knownVariables, newVariables);
161 createVariables(negativeLiteral, newVariables);
162 }
163
164 protected void collectVariables(Atom atom, Set<String> knownVariables, Set<String> newVariables) {
165 List<INode> nodes = NodeModelUtils.findNodesForFeature(atom, ProblemPackage.Literals.ATOM__ARGUMENTS);
166 for (INode node : nodes) {
167 String variableName = linkingHelper.getCrossRefNodeAsString(node, true);
168 if (!knownVariables.contains(variableName)) {
169 newVariables.add(variableName);
170 }
171 }
172 }
173
174 protected void createVariables(ExistentialQuantifier quantifier, Set<String> newVariables) {
175 for (String variableName : newVariables) {
176 if (validId(variableName)) {
177 ImplicitVariable variable = ProblemFactory.eINSTANCE.createImplicitVariable();
178 variable.setName(variableName);
179 quantifier.getImplicitVariables().add(variable);
180 }
181 }
182 }
183
184 @Override
185 public void discardDerivedState(DerivedStateAwareResource resource) {
186 for (EObject object : resource.getContents()) {
187 if (object instanceof Problem) {
188 discardDerivedProblemState((Problem) object);
189 }
190 }
191 }
192
193 protected void discardDerivedProblemState(Problem problem) {
194 problem.getNodes().clear();
195 for (Statement statement : problem.getStatements()) {
196 if (statement instanceof PredicateDefinition) {
197 PredicateDefinition definition = (PredicateDefinition) statement;
198 for (Conjunction body : definition.getBodies()) {
199 body.getImplicitVariables().clear();
200 for (Literal literal : body.getLiterals()) {
201 if (literal instanceof NegativeLiteral) {
202 NegativeLiteral negativeLiteral = (NegativeLiteral) literal;
203 negativeLiteral.getImplicitVariables().clear();
204 }
205 }
206 }
207 }
208 }
209 }
210
211 protected static boolean validId(String name) {
212 return name != null && ID_REGEX.matcher(name).matches();
213 }
214
215 protected static boolean validQualifiedName(String name) {
216 return name != null && QUALIFIED_NAME_REGEX.matcher(name).matches();
217 }
218}
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemLocationInFileProvider.java b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemLocationInFileProvider.java
new file mode 100644
index 00000000..dfffc7ef
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemLocationInFileProvider.java
@@ -0,0 +1,130 @@
1package org.eclipse.viatra.solver.language.resource;
2
3import java.util.Iterator;
4
5import org.eclipse.emf.ecore.EObject;
6import org.eclipse.viatra.solver.language.model.problem.Assertion;
7import org.eclipse.viatra.solver.language.model.problem.Atom;
8import org.eclipse.viatra.solver.language.model.problem.Conjunction;
9import org.eclipse.viatra.solver.language.model.problem.ImplicitVariable;
10import org.eclipse.viatra.solver.language.model.problem.Literal;
11import org.eclipse.viatra.solver.language.model.problem.NegativeLiteral;
12import org.eclipse.viatra.solver.language.model.problem.Node;
13import org.eclipse.viatra.solver.language.model.problem.Problem;
14import org.eclipse.viatra.solver.language.model.problem.ProblemPackage;
15import org.eclipse.viatra.solver.language.model.problem.Statement;
16import org.eclipse.xtext.EcoreUtil2;
17import org.eclipse.xtext.naming.IQualifiedNameProvider;
18import org.eclipse.xtext.naming.QualifiedName;
19import org.eclipse.xtext.resource.DefaultLocationInFileProvider;
20import org.eclipse.xtext.resource.IEObjectDescription;
21import org.eclipse.xtext.scoping.IScope;
22import org.eclipse.xtext.scoping.IScopeProvider;
23import org.eclipse.xtext.util.ITextRegion;
24
25import com.google.inject.Inject;
26
27public class ProblemLocationInFileProvider extends DefaultLocationInFileProvider {
28 @Inject
29 private IQualifiedNameProvider qualifiedNameProvider;
30
31 @Inject
32 private IScopeProvider scopeProvider;
33
34 @Override
35 protected ITextRegion doGetTextRegion(EObject obj, RegionDescription query) {
36 if (obj instanceof Node) {
37 return getNodeTextRegion((Node) obj, query);
38 }
39 if (obj instanceof ImplicitVariable) {
40 return getVariableTextRegion((ImplicitVariable) obj, query);
41 }
42 return super.doGetTextRegion(obj, query);
43 }
44
45 protected ITextRegion getNodeTextRegion(Node node, RegionDescription query) {
46 ITextRegion newNodeRegion = getNewNodeTextRegion(node, query);
47 if (newNodeRegion != null) {
48 return newNodeRegion;
49 }
50 return getNodeFirstReferenceTextRegion(node, query);
51 }
52
53 protected ITextRegion getNewNodeTextRegion(Node node, RegionDescription query) {
54 QualifiedName nodeName = qualifiedNameProvider.getFullyQualifiedName(node);
55 if (nodeName == null || nodeName.getSegmentCount() <= 1) {
56 return null;
57 }
58 if (ProblemDerivedStateComputer.NEW_NODE.equals(nodeName.getLastSegment())) {
59 QualifiedName className = nodeName.skipLast(1);
60 IScope classScope = scopeProvider.getScope(node, ProblemPackage.Literals.ASSERTION__RELATION);
61 IEObjectDescription description = classScope.getSingleElement(className);
62 if (description == null) {
63 return null;
64 }
65 EObject classDeclaration = description.getEObjectOrProxy();
66 if (!classDeclaration.eIsProxy()) {
67 return doGetTextRegion(classDeclaration, query);
68 }
69 }
70 return null;
71 }
72
73 protected ITextRegion getNodeFirstReferenceTextRegion(Node node, RegionDescription query) {
74 Problem problem = EcoreUtil2.getContainerOfType(node, Problem.class);
75 if (problem == null) {
76 return ITextRegion.EMPTY_REGION;
77 }
78 for (Statement statement : problem.getStatements()) {
79 if (statement instanceof Assertion) {
80 Assertion assertion = (Assertion) statement;
81 int index = assertion.getArguments().indexOf(node);
82 if (index >= 0) {
83 return doGetLocationOfFeature(assertion, ProblemPackage.Literals.ASSERTION__ARGUMENTS, index,
84 query);
85 }
86 }
87 }
88 return ITextRegion.EMPTY_REGION;
89 }
90
91 protected ITextRegion getVariableTextRegion(ImplicitVariable variable, RegionDescription query) {
92 EObject container = variable.eContainer();
93 if (container instanceof Conjunction) {
94 return getFirstReferenceToVariableInConjunction(variable, (Conjunction) container, query);
95 }
96 if (container instanceof NegativeLiteral) {
97 return getFirstReferenceToVariableInNegativeLiteral(variable, (NegativeLiteral) container, query);
98 }
99 return ITextRegion.EMPTY_REGION;
100 }
101
102 protected ITextRegion getFirstReferenceToVariableInConjunction(ImplicitVariable variable, Conjunction conjunction,
103 RegionDescription query) {
104 Iterator<Literal> iterator = conjunction.getLiterals().iterator();
105 ITextRegion found = ITextRegion.EMPTY_REGION;
106 while (found == ITextRegion.EMPTY_REGION && iterator.hasNext()) {
107 Literal literal = iterator.next();
108 if (literal instanceof Atom) {
109 found = getFirstReferenceToVariableInAtom(variable, (Atom) literal, query);
110 } else if (literal instanceof NegativeLiteral) {
111 found = getFirstReferenceToVariableInNegativeLiteral(variable, (NegativeLiteral) literal, query);
112 }
113 }
114 return found;
115 }
116
117 protected ITextRegion getFirstReferenceToVariableInNegativeLiteral(ImplicitVariable variable,
118 NegativeLiteral literal, RegionDescription query) {
119 return getFirstReferenceToVariableInAtom(variable, literal.getAtom(), query);
120 }
121
122 protected ITextRegion getFirstReferenceToVariableInAtom(ImplicitVariable variable, Atom atom,
123 RegionDescription query) {
124 int index = atom.getArguments().indexOf(variable);
125 if (index >= 0) {
126 return doGetLocationOfFeature(atom, ProblemPackage.Literals.ATOM__ARGUMENTS, index, query);
127 }
128 return ITextRegion.EMPTY_REGION;
129 }
130}
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemResourceDescriptionStrategy.java b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemResourceDescriptionStrategy.java
new file mode 100644
index 00000000..7b37ffd6
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemResourceDescriptionStrategy.java
@@ -0,0 +1,39 @@
1package org.eclipse.viatra.solver.language.resource;
2
3import org.eclipse.emf.ecore.EObject;
4import org.eclipse.viatra.solver.language.model.problem.ReferenceDeclaration;
5import org.eclipse.viatra.solver.language.model.problem.Variable;
6import org.eclipse.xtext.naming.QualifiedName;
7import org.eclipse.xtext.resource.IEObjectDescription;
8import org.eclipse.xtext.resource.impl.AliasedEObjectDescription;
9import org.eclipse.xtext.resource.impl.DefaultResourceDescriptionStrategy;
10import org.eclipse.xtext.util.IAcceptor;
11
12import com.google.inject.Singleton;
13
14@Singleton
15public class ProblemResourceDescriptionStrategy extends DefaultResourceDescriptionStrategy {
16 @Override
17 public boolean createEObjectDescriptions(EObject eObject, IAcceptor<IEObjectDescription> acceptor) {
18 IAcceptor<IEObjectDescription> wrappedAcceptor;
19 if (eObject instanceof Variable) {
20 return false;
21 }
22 if (eObject instanceof ReferenceDeclaration) {
23 wrappedAcceptor = new IAcceptor<IEObjectDescription>() {
24 public void accept(IEObjectDescription description) {
25 acceptor.accept(description);
26 QualifiedName qualifiedName = description.getQualifiedName();
27 if (qualifiedName.getSegmentCount() >= 2) {
28 QualifiedName simpleName = QualifiedName.create(qualifiedName.getLastSegment());
29 IEObjectDescription aliasedDescription = new AliasedEObjectDescription(simpleName, description);
30 acceptor.accept(aliasedDescription);
31 }
32 };
33 };
34 } else {
35 wrappedAcceptor = acceptor;
36 }
37 return super.createEObjectDescriptions(eObject, wrappedAcceptor);
38 }
39}
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/scoping/ProblemGlobalScopeProvider.java b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/scoping/ProblemGlobalScopeProvider.java
new file mode 100644
index 00000000..cf01999a
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/scoping/ProblemGlobalScopeProvider.java
@@ -0,0 +1,19 @@
1package org.eclipse.viatra.solver.language.scoping;
2
3import java.util.LinkedHashSet;
4
5import org.eclipse.emf.common.util.URI;
6import org.eclipse.emf.ecore.resource.Resource;
7import org.eclipse.xtext.scoping.impl.ImportUriGlobalScopeProvider;
8
9public class ProblemGlobalScopeProvider extends ImportUriGlobalScopeProvider {
10 public static final URI LIBRARY_URI = URI.createURI(ProblemGlobalScopeProvider.class.getClassLoader()
11 .getResource("org/eclipse/viatra/solver/language/library.problem").toString());
12
13 @Override
14 protected LinkedHashSet<URI> getImportedUris(Resource resource) {
15 LinkedHashSet<URI> importedUris = super.getImportedUris(resource);
16 importedUris.add(LIBRARY_URI);
17 return importedUris;
18 }
19}
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/scoping/ProblemScopeProvider.java b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/scoping/ProblemScopeProvider.java
new file mode 100644
index 00000000..254284a8
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/scoping/ProblemScopeProvider.java
@@ -0,0 +1,74 @@
1/*
2 * generated by Xtext 2.25.0
3 */
4package org.eclipse.viatra.solver.language.scoping;
5
6import java.util.ArrayList;
7import java.util.List;
8
9import org.eclipse.emf.ecore.EObject;
10import org.eclipse.emf.ecore.EReference;
11import org.eclipse.viatra.solver.language.model.problem.ClassDeclaration;
12import org.eclipse.viatra.solver.language.model.problem.ExistentialQuantifier;
13import org.eclipse.viatra.solver.language.model.problem.PredicateDefinition;
14import org.eclipse.viatra.solver.language.model.problem.Problem;
15import org.eclipse.viatra.solver.language.model.problem.ProblemPackage;
16import org.eclipse.viatra.solver.language.model.problem.ReferenceDeclaration;
17import org.eclipse.viatra.solver.language.model.problem.Statement;
18import org.eclipse.viatra.solver.language.model.problem.Variable;
19import org.eclipse.xtext.EcoreUtil2;
20import org.eclipse.xtext.naming.QualifiedName;
21import org.eclipse.xtext.scoping.IScope;
22import org.eclipse.xtext.scoping.Scopes;
23
24import com.google.common.collect.ImmutableList;
25
26/**
27 * This class contains custom scoping description.
28 *
29 * See
30 * https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#scoping
31 * on how and when to use it.
32 */
33public class ProblemScopeProvider extends AbstractProblemScopeProvider {
34
35 @Override
36 public IScope getScope(EObject context, EReference reference) {
37 IScope scope = super.getScope(context, reference);
38 if (reference == ProblemPackage.Literals.ATOM__ARGUMENTS) {
39 return getVariableScope(context, scope);
40 } else if (EcoreUtil2.isAssignableFrom(reference.getEReferenceType(),
41 ProblemPackage.Literals.REFERENCE_DECLARATION)) {
42 Problem problem = EcoreUtil2.getContainerOfType(context, Problem.class);
43 if (problem == null) {
44 return scope;
45 }
46 ImmutableList.Builder<ReferenceDeclaration> builder = ImmutableList.builder();
47 for (Statement statement : problem.getStatements()) {
48 if (statement instanceof ClassDeclaration) {
49 ClassDeclaration classDeclaration = (ClassDeclaration) statement;
50 builder.addAll(classDeclaration.getReferenceDeclarations());
51 }
52 }
53 return Scopes.scopeFor(builder.build(), scope);
54 }
55 return scope;
56 }
57
58 protected IScope getVariableScope(EObject context, IScope delegateScope) {
59 List<Variable> variables = new ArrayList<>();
60 EObject currentContext = context;
61 while (currentContext != null && !(currentContext instanceof PredicateDefinition)) {
62 if (currentContext instanceof ExistentialQuantifier) {
63 ExistentialQuantifier quantifier = (ExistentialQuantifier) currentContext;
64 variables.addAll(quantifier.getImplicitVariables());
65 }
66 currentContext = currentContext.eContainer();
67 }
68 if (currentContext instanceof PredicateDefinition) {
69 PredicateDefinition definition = (PredicateDefinition) currentContext;
70 variables.addAll(definition.getParameters());
71 }
72 return Scopes.scopeFor(variables);
73 }
74}
diff --git a/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/validation/ProblemValidator.java b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/validation/ProblemValidator.java
new file mode 100644
index 00000000..2b17e222
--- /dev/null
+++ b/org.eclipse.viatra.solver.language.parent/org.eclipse.viatra.solver.language/src/main/java/org/eclipse/viatra/solver/language/validation/ProblemValidator.java
@@ -0,0 +1,25 @@
1/*
2 * generated by Xtext 2.25.0
3 */
4package org.eclipse.viatra.solver.language.validation;
5
6
7/**
8 * This class contains custom validation rules.
9 *
10 * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#validation
11 */
12public class ProblemValidator extends AbstractProblemValidator {
13
14// public static final String INVALID_NAME = "invalidName";
15//
16// @Check
17// public void checkGreetingStartsWithCapital(Greeting greeting) {
18// if (!Character.isUpperCase(greeting.getName().charAt(0))) {
19// warning("Name should start with a capital",
20// ProblemPackage.Literals.GREETING__NAME,
21// INVALID_NAME);
22// }
23// }
24
25}
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-09-12 09:36:50 +0000