Synthetic tokens for solver language

5 files changed, 189 insertions, 14 deletions

diff --git a/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/SolverLanguage.xtext b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/SolverLanguage.xtext
index 5abeb891..1306b626 100644
--- a/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/SolverLanguage.xtext
+++ b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/SolverLanguage.xtext
@@ -9,7 +9,7 @@ Statement:
         (

                 AssertionOrDefinition | PredicateDefinition | UnnamedErrorPrediateDefinition | DefaultDefinition | ExternPredicateDefinition |

                 MetricDefinition | ExternMetricDefinition | ClassDefinition | ScopeDefinition | ObjectiveDefinition

-        ) DOT;

+        ) FULL_STOP;

 

 AssertionOrDefinition returns Statement:

         Expression (

@@ -28,7 +28,7 @@ DefaultDefinition:
         "default" head=Call ":" range=Expression;

 

 ExternPredicateDefinition:

-        "extern" head=Call ".";

+        "extern" head=Call;

 

 enum MetricType:

         INT="int" | REAL="real";

@@ -103,10 +103,10 @@ Aggregation:
         op=AggregationOp "{" body=Expression "|" condition=Expression "}";

 

 AtomicExpression returns Expression:

-        Reference ({Call.functor=current} -> argumentList=ArgumentList)? | Interval | Literal | "(" Expression ")";

+        Reference | Call | Interval | Literal | "(" Expression ")";

 

 Call:

-        functor=Reference (transitiveClosure?=STAR | reflexiveTransitiveClosure?=PLUS)? argumentList=ArgumentList;

+        functor=Reference (transitiveClosure?=TRANSITIVE_CLOSURE | reflexiveTransitiveClosure?=REFLEXIVE_TRANSITIVE_CLOSURE)? argumentList=ArgumentList;

 

 ArgumentList:

         {ArgumentList} "(" (arguments+=Argument ("," arguments+=Argument)*)? ")";

@@ -153,7 +153,7 @@ EmptyIntervalLiteral:
 StringLiteral:

         value=STRING;

 

-ClassDefinition returns Statement:

+ClassDefinition:

         abstract?="abstract"? "class" name=ID ("extends" superclasses+=[NamedElement|QualifiedName] ("," superclasses+=[NamedElement|QualifiedName])*)?

         "{" members+=MemberDefinition* "}";

 

@@ -182,13 +182,13 @@ BoundedScopeDefinition:
         "scope" (

                 (lowerBound=INT "<=")? type=[NamedElement|QualifiedName] "<=" upperBound=INT |

                 upperBound=INT ">=" type=[NamedElement|QualifiedName] (">=" lowerBound=INT)?

-        ) ".";

+        );

 

 LowerBoundedScopeDefinition:

         "scope" (

                 lowerBound=INT "<=" type=[NamedElement|QualifiedName] |

                 type=[NamedElement|QualifiedName] ">=" lowerBound=INT

-        ) ".";

+        );

 

 enum ObjectiveKind:

         MINIMIZE="minimize" | MAXIMIZE="maximize";

@@ -209,17 +209,21 @@ QualifiedName hidden():
 terminal STRING returns ecore::EString:

         '"' ( '\\' . /* 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' */ | !('\\'|'"') )* '"';

 

-terminal QUOTED_ID returns ecore::EString:

+terminal QUOTED_ID:

         '\'' ( '\\' . /* 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' */ | !('\\'|'\'') )* '\'';

 

-terminal PLUS:

-        "synthetic::plus";

+@Override

+terminal SL_COMMENT:

+        ('%' | '//') !('\n'|'\r')* ('\r'? '\n')?;

+

+terminal TRANSITIVE_CLOSURE:

+        "synthetic:TRANSITIVE_CLOSURE";

 

-terminal STAR:

-        "synthetic::star";

+terminal REFLEXIVE_TRANSITIVE_CLOSURE:

+        "synthetic:REFLEXIVE_TRANSITIVE_CLOSURE";

 

-terminal DOT:

-        "synthetic::dot";

+terminal FULL_STOP:

+        "synthetic:FULL_STOP";

 

 NamedElement:

         name=QualifiedName;

diff --git a/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/SolverLanguageRuntimeModule.xtend b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/SolverLanguageRuntimeModule.xtend
index 343bc48a..e882626b 100644
--- a/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/SolverLanguageRuntimeModule.xtend
+++ b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/SolverLanguageRuntimeModule.xtend
@@ -3,9 +3,21 @@
  */

 package org.eclipse.viatra.solver.language

 

+import org.eclipse.viatra.solver.language.parser.antlr.SolverLanguageTokenDefInjectingParser

+import org.eclipse.viatra.solver.language.serializer.SolverLanguageSyntheticTokenSyntacticSequencer

 

 /**

  * Use this class to register components to be used at runtime / without the Equinox extension registry.

  */

 class SolverLanguageRuntimeModule extends AbstractSolverLanguageRuntimeModule {

+        

+        override bindIParser() {

+                SolverLanguageTokenDefInjectingParser

+        }

+        

+        

+        override bindISyntacticSequencer() {

+                SolverLanguageSyntheticTokenSyntacticSequencer

+        }

+        

 }

diff --git a/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/parser/antlr/SolverLanguageTokenDefInjectingParser.xtend b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/parser/antlr/SolverLanguageTokenDefInjectingParser.xtend
new file mode 100644
index 00000000..87efd2b3
--- /dev/null
+++ b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/parser/antlr/SolverLanguageTokenDefInjectingParser.xtend
@@ -0,0 +1,16 @@
+package org.eclipse.viatra.solver.language.parser.antlr
+
+import com.google.inject.Inject
+import org.antlr.runtime.CharStream
+import org.eclipse.xtext.parser.antlr.ITokenDefProvider
+
+class SolverLanguageTokenDefInjectingParser extends SolverLanguageParser {
+        @Inject ITokenDefProvider tokenDefProvider
+
+        override protected createLexer(CharStream stream) {
+                val tokenSource = super.createLexer(stream) as SolverLanguageTokenSource
+                tokenSource.initializeTokenDefsFrom(tokenDefProvider)
+                tokenSource
+        }
+
+}
diff --git a/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/parser/antlr/SolverLanguageTokenSource.java b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/parser/antlr/SolverLanguageTokenSource.java
new file mode 100644
index 00000000..4c1dacd5
--- /dev/null
+++ b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/parser/antlr/SolverLanguageTokenSource.java
@@ -0,0 +1,122 @@
+/*

+ * generated by Xtext 2.21.0

+ */

+package org.eclipse.viatra.solver.language.parser.antlr;

+

+import static org.eclipse.viatra.solver.language.parser.antlr.internal.InternalSolverLanguageParser.RULE_FULL_STOP;

+import static org.eclipse.viatra.solver.language.parser.antlr.internal.InternalSolverLanguageParser.RULE_ID;

+import static org.eclipse.viatra.solver.language.parser.antlr.internal.InternalSolverLanguageParser.RULE_INT;

+import static org.eclipse.viatra.solver.language.parser.antlr.internal.InternalSolverLanguageParser.RULE_ML_COMMENT;

+import static org.eclipse.viatra.solver.language.parser.antlr.internal.InternalSolverLanguageParser.RULE_QUOTED_ID;

+import static org.eclipse.viatra.solver.language.parser.antlr.internal.InternalSolverLanguageParser.RULE_REFLEXIVE_TRANSITIVE_CLOSURE;

+import static org.eclipse.viatra.solver.language.parser.antlr.internal.InternalSolverLanguageParser.RULE_SL_COMMENT;

+import static org.eclipse.viatra.solver.language.parser.antlr.internal.InternalSolverLanguageParser.RULE_TRANSITIVE_CLOSURE;

+import static org.eclipse.viatra.solver.language.parser.antlr.internal.InternalSolverLanguageParser.RULE_WS;

+

+import java.util.Map;

+

+import org.antlr.runtime.Token;

+import org.antlr.runtime.TokenSource;

+import org.eclipse.xtext.parser.antlr.ITokenDefProvider;

+import org.eclipse.xtext.parser.antlr.TokenAcceptor;

+

+public class SolverLanguageTokenSource implements TokenSource {

+        private TokenSource delegate;

+

+        private final TokenAcceptor acceptor = new TokenAcceptor();

+

+        private int lastTokenId = -1;

+        private int plusTokenId = -1;

+        private int starTokenId = -1;

+        private int dotTokenId = -1;

+        private int openParenTokenId = -1;

+

+        public SolverLanguageTokenSource(TokenSource delegate) {

+                this.delegate = delegate;

+        }

+

+        @Override

+        public String getSourceName() {

+                return "[SolverLanguageSyntheticTokenTokenSource] " + delegate.getSourceName();

+        }

+

+        @Override

+        public Token nextToken() {

+                Token token = internalNextToken();

+                lastTokenId = token.getType();

+                return token;

+        }

+

+        protected Token internalNextToken() {

+                if (acceptor.hasNext()) {

+                        return acceptor.next();

+                }

+                Token token = delegate.nextToken();

+                int type = token.getType();

+                if (type == plusTokenId) {

+                        if ((lastTokenId == RULE_ID || lastTokenId == RULE_QUOTED_ID)

+                                        && peekUntilVisible().getType() == openParenTokenId) {

+                                token.setType(RULE_TRANSITIVE_CLOSURE);

+                        }

+                } else if (type == starTokenId) {

+                        if ((lastTokenId == RULE_ID || lastTokenId == RULE_QUOTED_ID)

+                                        && peekUntilVisible().getType() == openParenTokenId) {

+                                token.setType(RULE_REFLEXIVE_TRANSITIVE_CLOSURE);

+                        }

+                } else if (type == dotTokenId) {

+                        if ((lastTokenId != RULE_ID && lastTokenId != RULE_INT) || peekToken().getType() != lastTokenId) {

+                                token.setType(RULE_FULL_STOP);

+                        }

+                }

+                return token;

+        }

+

+        protected Token peekUntilVisible() {

+                Token followingToken = null;

+                do {

+                        followingToken = peekToken();

+                } while (isHidden(followingToken.getType()));

+                return followingToken;

+        }

+

+        protected Token peekToken() {

+                Token followingToken = delegate.nextToken();

+                acceptor.accept(followingToken);

+                return followingToken;

+        }

+

+        protected boolean isHidden(int tokenType) {

+                return tokenType == RULE_WS || tokenType == RULE_SL_COMMENT || tokenType == RULE_ML_COMMENT;

+        }

+

+        public void initializeTokenDefsFrom(ITokenDefProvider provider) {

+                for (Map.Entry<Integer, String> entry : provider.getTokenDefMap().entrySet()) {

+                        switch (entry.getValue()) {

+                        case "'+'":

+                                plusTokenId = entry.getKey();

+                                break;

+                        case "'*'":

+                                starTokenId = entry.getKey();

+                                break;

+                        case "'.'":

+                                dotTokenId = entry.getKey();

+                                break;

+                        case "'('":

+                                openParenTokenId = entry.getKey();

+                                break;

+                        }

+                }

+                if (plusTokenId == -1) {

+                        throw new IllegalStateException("Token '+' was not found");

+                }

+                if (starTokenId == -1) {

+                        throw new IllegalStateException("Token '*' was not found");

+                }

+                if (dotTokenId == -1) {

+                        throw new IllegalStateException("Token '.' was not found");

+                }

+                if (openParenTokenId == -1) {

+                        throw new IllegalStateException("Token '(' was not found");

+                }

+        }

+}

diff --git a/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/serializer/SolverLanguageSyntheticTokenSyntacticSequencer.xtend b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/serializer/SolverLanguageSyntheticTokenSyntacticSequencer.xtend
new file mode 100644
index 00000000..587ea27b
--- /dev/null
+++ b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/serializer/SolverLanguageSyntheticTokenSyntacticSequencer.xtend
@@ -0,0 +1,21 @@
+package org.eclipse.viatra.solver.language.serializer
+
+import org.eclipse.emf.ecore.EObject
+import org.eclipse.xtext.RuleCall
+import org.eclipse.xtext.nodemodel.INode
+
+class SolverLanguageSyntheticTokenSyntacticSequencer extends SolverLanguageSyntacticSequencer {
+        
+        override protected getTRANSITIVE_CLOSUREToken(EObject semanticObject, RuleCall ruleCall, INode node) {
+                "+"
+        }
+        
+        override protected getREFLEXIVE_TRANSITIVE_CLOSUREToken(EObject semanticObject, RuleCall ruleCall, INode node) {
+                "*"
+        }
+        
+        override protected getFULL_STOPToken(EObject semanticObject, RuleCall ruleCall, INode node) {
+                "."
+        }
+        
+}
\ No newline at end of file