diff options
Diffstat (limited to 'Application/org.eclipse.viatra.solver.language/src')
2 files changed, 46 insertions, 26 deletions
diff --git a/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/GenerateSolverLanguage.mwe2 b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/GenerateSolverLanguage.mwe2 index 7f95e737..50072f0d 100644 --- a/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/GenerateSolverLanguage.mwe2 +++ b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/GenerateSolverLanguage.mwe2 | |||
@@ -32,6 +32,7 @@ Workflow { | |||
32 | language = StandardLanguage { | 32 | language = StandardLanguage { |
33 | name = "org.eclipse.viatra.solver.language.SolverLanguage" | 33 | name = "org.eclipse.viatra.solver.language.SolverLanguage" |
34 | fileExtensions = "vsc" | 34 | fileExtensions = "vsc" |
35 | referencedResource = "platform:/resource/org.eclipse.viatra.solver.language/model/SolverLanguage.genmodel" | ||
35 | 36 | ||
36 | serializer = { | 37 | serializer = { |
37 | generateStub = false | 38 | generateStub = false |
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 1306b626..d0578d78 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 | |||
@@ -1,22 +1,23 @@ | |||
1 | grammar org.eclipse.viatra.solver.language.SolverLanguage with org.eclipse.xtext.common.Terminals | 1 | grammar org.eclipse.viatra.solver.language.SolverLanguage with org.eclipse.xtext.common.Terminals |
2 | import "http://www.eclipse.org/emf/2002/Ecore" as ecore | 2 | import "http://www.eclipse.org/emf/2002/Ecore" as ecore |
3 | generate solverLanguage "http://www.eclipse.org/viatra/solver/language/SolverLanguage" | 3 | import "http://www.eclipse.org/viatra/solver/language/SolverLanguage" |
4 | 4 | ||
5 | Problem: | 5 | Problem: |
6 | (statements+=Statement)*; | 6 | (statements+=Statement)*; |
7 | 7 | ||
8 | Statement: | 8 | Statement: |
9 | ( | 9 | ( |
10 | AssertionOrDefinition | PredicateDefinition | UnnamedErrorPrediateDefinition | DefaultDefinition | ExternPredicateDefinition | | 10 | AssertionOrDefinition | PredicateDefinition | UnnamedErrorPrediateDefinition | DefaultDefinition | MetricDefinition | |
11 | MetricDefinition | ExternMetricDefinition | ClassDefinition | ScopeDefinition | ObjectiveDefinition | 11 | ExternPredicateDefinition | ExternMetricDefinition | ExternAggregatorDefinition | ExternDatatypeDefinition | |
12 | ClassDefinition | ScopeDefinition | ObjectiveDefinition | ||
12 | ) FULL_STOP; | 13 | ) FULL_STOP; |
13 | 14 | ||
14 | AssertionOrDefinition returns Statement: | 15 | AssertionOrDefinition returns Statement: |
15 | Expression ( | 16 | Expression ( |
16 | {Assertion.body=current} (":" range=Expression)? | | 17 | {Interpretation.body=current} ":" range=Expression | |
17 | {PredicateDefinition.head=current} ":-" body=Expression | | 18 | {PredicateDefinition.head=current} ":-" body=Expression | |
18 | {MetricDefinition.head=current} "=" body=Expression | 19 | {MetricDefinition.head=current} "=" body=Expression |
19 | ); | 20 | )?; |
20 | 21 | ||
21 | PredicateDefinition: | 22 | PredicateDefinition: |
22 | (functional?="functional" error?="error"? | error?="error" functional?="functional"?) head=Call ":-" body=Expression; | 23 | (functional?="functional" error?="error"? | error?="error" functional?="functional"?) head=Call ":-" body=Expression; |
@@ -27,24 +28,42 @@ UnnamedErrorPrediateDefinition: | |||
27 | DefaultDefinition: | 28 | DefaultDefinition: |
28 | "default" head=Call ":" range=Expression; | 29 | "default" head=Call ":" range=Expression; |
29 | 30 | ||
31 | MetricDefinition: | ||
32 | type=[NamedElement|QualifiedName] head=Call "=" body=Expression; | ||
33 | |||
30 | ExternPredicateDefinition: | 34 | ExternPredicateDefinition: |
31 | "extern" head=Call; | 35 | "extern" name=QualifiedName argumentList=ArgumentList; |
32 | 36 | ||
33 | enum MetricType: | 37 | ExternMetricDefinition: |
34 | INT="int" | REAL="real"; | 38 | "extern" type=[NamedElement|QualifiedName] name=QualifiedName argumentList=ArgumentList; |
35 | 39 | ||
36 | MetricDefinition: | 40 | ExternAggregatorDefinition: |
37 | type=MetricType head=Expression "=" body=Expression; | 41 | "extern" type=[NamedElement|QualifiedName] name=QualifiedName "{" inputType=[NamedElement|QualifiedName] "..." "}"; |
38 | 42 | ||
39 | ExternMetricDefinition: | 43 | ExternDatatypeDefinition: |
40 | "extern" type=MetricType head=Call; | 44 | "extern" "datatype" name=QualifiedName ("extends" supertypes+=[NamedElement|QualifiedName] ("," supertypes+=[NamedElement|QualifiedName])*); |
45 | |||
46 | Variable: | ||
47 | type=[NamedElement|QualifiedName]? name=ID; | ||
41 | 48 | ||
42 | Expression: | 49 | Expression: |
43 | IfElse | DisjunctiveExpression; | 50 | IfElse | Let | ImplicationExpression; |
44 | 51 | ||
45 | IfElse: | 52 | IfElse: |
46 | "if" condition=Expression "then" then=Expression "else" else=Expression; | 53 | "if" condition=Expression "then" then=Expression "else" else=Expression; |
47 | 54 | ||
55 | Let: | ||
56 | "let" bindings+=LetBinding ("," bindings+=LetBinding)* "in" body=Expression; | ||
57 | |||
58 | LetBinding: | ||
59 | variable=Variable "=" value=AdditiveExpression; | ||
60 | |||
61 | enum ImplicationOperator returns BinaryOperator: | ||
62 | IMPLIES = "=>"; | ||
63 | |||
64 | ImplicationExpression returns Expression: | ||
65 | DisjunctiveExpression ({BinaryExpression.left=current} op=ImplicationOperator right=ImplicationExpression)?; | ||
66 | |||
48 | DisjunctiveExpression returns Expression: | 67 | DisjunctiveExpression returns Expression: |
49 | ConjunctiveExpression ( | 68 | ConjunctiveExpression ( |
50 | {Disjunction.children+=current} (";" children+=ConjunctiveExpression)+ | | 69 | {Disjunction.children+=current} (";" children+=ConjunctiveExpression)+ | |
@@ -57,9 +76,6 @@ Case: | |||
57 | ConjunctiveExpression returns Expression: | 76 | ConjunctiveExpression returns Expression: |
58 | ComparisonExpression ({Conjunction.children+=current} ("," children+=ComparisonExpression)+)?; | 77 | ComparisonExpression ({Conjunction.children+=current} ("," children+=ComparisonExpression)+)?; |
59 | 78 | ||
60 | enum BinaryOperator: | ||
61 | EQ | NOT_EQ | LESS | LESS_EQ | GREATER | GREATER_EQ | IN | ADD | SUB | MUL | DIV | POW; | ||
62 | |||
63 | enum ComparisonOperator returns BinaryOperator: | 79 | enum ComparisonOperator returns BinaryOperator: |
64 | EQ="==" | NOT_EQ="!=" | LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | IN="in"; | 80 | EQ="==" | NOT_EQ="!=" | LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | IN="in"; |
65 | 81 | ||
@@ -82,7 +98,10 @@ enum ExponentialOp returns BinaryOperator: | |||
82 | POW="^"; | 98 | POW="^"; |
83 | 99 | ||
84 | ExponentialExpression returns Expression: | 100 | ExponentialExpression returns Expression: |
85 | UnaryExpression ({BinaryExpression.left=current} op=ExponentialOp right=ExponentialExpression)?; | 101 | CastExpression ({BinaryExpression.left=current} op=ExponentialOp right=CastExpression)?; |
102 | |||
103 | CastExpression returns Expression: | ||
104 | UnaryExpression ({CastExpression.body=current} "as" type=[NamedElement|QualifiedName])?; | ||
86 | 105 | ||
87 | enum UnaryOp: | 106 | enum UnaryOp: |
88 | NEG="!" | PLUS="+" | MINUS="-" | MAY="may" | MUST="must" | CURRENT="current"; | 107 | NEG="!" | PLUS="+" | MINUS="-" | MAY="may" | MUST="must" | CURRENT="current"; |
@@ -91,16 +110,19 @@ UnaryExpression returns Expression: | |||
91 | AggregationExpression | {UnaryExpression} op=UnaryOp body=AggregationExpression; | 110 | AggregationExpression | {UnaryExpression} op=UnaryOp body=AggregationExpression; |
92 | 111 | ||
93 | AggregationExpression returns Expression: | 112 | AggregationExpression returns Expression: |
94 | AtomicExpression | Count | Aggregation; | 113 | AtomicExpression | QuantifiedExpression | Aggregation; |
95 | 114 | ||
96 | Count: | 115 | LocalVariables: |
97 | "count" "{" body=Expression "}"; | 116 | {LocalVariables} "[" (variables+=Variable ("," variables+=Variable)*)? "]"; |
98 | 117 | ||
99 | enum AggregationOp: | 118 | enum Quantifier: |
100 | ONLY="only" | SUM="sum" | PROD="prod" | AVG="avg" | MIN="min" | MAX="max"; | 119 | EXISTS="exists" | FORALL="forall" | COUNT="count"; |
120 | |||
121 | QuantifiedExpression: | ||
122 | quantifier=Quantifier localVariables=LocalVariables? "{" body=Expression "}"; | ||
101 | 123 | ||
102 | Aggregation: | 124 | Aggregation: |
103 | op=AggregationOp "{" body=Expression "|" condition=Expression "}"; | 125 | op=[NamedElement|QualifiedName] localVariables=LocalVariables? "{" body=Expression ("|" condition=Expression)? "}"; |
104 | 126 | ||
105 | AtomicExpression returns Expression: | 127 | AtomicExpression returns Expression: |
106 | Reference | Call | Interval | Literal | "(" Expression ")"; | 128 | Reference | Call | Interval | Literal | "(" Expression ")"; |
@@ -224,7 +246,4 @@ terminal REFLEXIVE_TRANSITIVE_CLOSURE: | |||
224 | 246 | ||
225 | terminal FULL_STOP: | 247 | terminal FULL_STOP: |
226 | "synthetic:FULL_STOP"; | 248 | "synthetic:FULL_STOP"; |
227 | |||
228 | NamedElement: | ||
229 | name=QualifiedName; | ||
230 | 249 | ||