grammar org.eclipse.viatra.solver.language.SolverLanguage with org.eclipse.xtext.common.Terminals
import "http://www.eclipse.org/emf/2002/Ecore" as ecore
generate solverLanguage "http://www.eclipse.org/viatra/solver/language/SolverLanguage"

Problem:
	(statements+=Statement)*;

Statement: 
	(
		AssertionOrDefinition | PredicateDefinition | UnnamedErrorPrediateDefinition | DefaultDefinition | ExternPredicateDefinition |
		MetricDefinition | ExternMetricDefinition | ClassDefinition | ScopeDefinition | ObjectiveDefinition
	) DOT;

AssertionOrDefinition returns Statement:
	Expression (
		{Assertion.body=current} (":" range=Expression)? |
		{PredicateDefinition.head=current} ":-" body=Expression |
		{MetricDefinition.head=current} "=" body=Expression
	);

PredicateDefinition:
	(functional?="functional" error?="error"? | error?="error" functional?="functional"?) head=Call ":-" body=Expression;

UnnamedErrorPrediateDefinition:
	"error" argumentList=ArgumentList ":-" body=Expression;

DefaultDefinition:
	"default" head=Call ":" range=Expression;

ExternPredicateDefinition:
	"extern" head=Call ".";

enum MetricType:
	INT="int" | REAL="real";

MetricDefinition:
	type=MetricType head=Expression "=" body=Expression;

ExternMetricDefinition:
	"extern" type=MetricType head=Call;

Expression:
	IfElse | DisjunctiveExpression;

IfElse:
	"if" condition=Expression "then" then=Expression "else" else=Expression;

DisjunctiveExpression returns Expression:
	ConjunctiveExpression (
		{Disjunction.children+=current} (";" children+=ConjunctiveExpression)+ |
		{Case.condition=current} "->" body=ConjunctiveExpression {Switch.cases+=current} (";" cases+=Case)*
	)?;

Case:
	condition=ConjunctiveExpression "->" body=ConjunctiveExpression;

ConjunctiveExpression returns Expression:
	ComparisonExpression ({Conjunction.children+=current} ("," children+=ComparisonExpression)+)?;

enum BinaryOperator:
	EQ | NOT_EQ | LESS | LESS_EQ | GREATER | GREATER_EQ | IN | ADD | SUB | MUL | DIV | POW;

enum ComparisonOperator returns BinaryOperator:
	EQ="==" | NOT_EQ="!=" | LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | IN="in";

ComparisonExpression returns Expression:
	AdditiveExpression ({Comparison.left=current} op=ComparisonOperator right=AdditiveExpression)?;

enum AdditiveBinaryOperator returns BinaryOperator:
	ADD="+" | SUB="-";

AdditiveExpression returns Expression:
	MultiplicativeExpression ({BinaryExpression.left=current} op=AdditiveBinaryOperator right=MultiplicativeExpression)*;

enum MultiplicativeBinaryOperator returns BinaryOperator:
	MUL="*" | DIV="/";

MultiplicativeExpression returns Expression:
	ExponentialExpression ({BinaryExpression.left=current} op=MultiplicativeBinaryOperator right=ExponentialExpression)*;

enum ExponentialOp returns BinaryOperator:
	POW="^";

ExponentialExpression returns Expression:
	UnaryExpression ({BinaryExpression.left=current} op=ExponentialOp right=ExponentialExpression)?;

enum UnaryOp:
	NEG="!" | PLUS="+" | MINUS="-" | MAY="may" | MUST="must" | CURRENT="current";

UnaryExpression returns Expression:
	AggregationExpression | {UnaryExpression} op=UnaryOp body=AggregationExpression;

AggregationExpression returns Expression:
	AtomicExpression | Count | Aggregation;

Count:
	"count" "{" body=Expression "}";

enum AggregationOp:
	ONLY="only" | SUM="sum" | PROD="prod" | AVG="avg" | MIN="min" | MAX="max";

Aggregation:
	op=AggregationOp "{" body=Expression "|" condition=Expression "}";

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

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

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

Argument:
	ExpressionArgument | StarArgument | TypedArgument | TypedStarArgument;

ExpressionArgument:
	body=ComparisonExpression;

StarArgument:
	{StarArgument} "*";

TypedArgument:
	type=[NamedElement|QualifiedName] variable=[NamedElement|QualifiedName];

TypedStarArgument:
	type=[NamedElement|QualifiedName] "*";

Reference:
	referred=[NamedElement|QualifiedName];

Interval:
	"[" lowerBound=Expression ".." upperBound=Expression "]";

Literal:
	LogicLiteral | NumericLiteral | InfinityLiteral | EmptyIntervalLiteral | StringLiteral;

enum LogicValue:
	TRUE="true" | FALSE="false" | UNKNOWN="unknown" | ERROR="error";

LogicLiteral:
	value=LogicValue;

NumericLiteral:
	value=Real;

InfinityLiteral:
	{InfinityLiteral} "inf";

EmptyIntervalLiteral:
	{EmptyIntervalLiteral} "empty";

StringLiteral:
	value=STRING;

ClassDefinition returns Statement:
	abstract?="abstract"? "class" name=ID ("extends" superclasses+=[NamedElement|QualifiedName] ("," superclasses+=[NamedElement|QualifiedName])*)?
	"{" members+=MemberDefinition* "}";

MemberDefinition:
	containment?="contains"? type=[NamedElement|QualifiedName] multiplicity=Multiplicity? name=ID ("opposite" opposite=[NamedElement|QualifiedName])? ";"?;

Multiplicity:
	ManyMultiplicity | ExactMultiplicity | BoundedMultiplicity;

ManyMultiplicity:
	{ManyMultiplicity} "[" "]";

ExactMultiplicity:
	"[" multiplicity=UpperMultiplicty "]";

BoundedMultiplicity:
	"[" lowerBound=INT ".." upperBound=UpperMultiplicty "]";

ScopeDefinition:
	ExactScopeDefinition | BoundedScopeDefinition | LowerBoundedScopeDefinition;

ExactScopeDefinition:
	"scope" type=[NamedElement|QualifiedName] "==" exactScope=INT;

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";

ObjectiveDefinition:
	kind=ObjectiveKind objective=Expression;

UpperMultiplicty returns ecore::EInt:
	INT | "*";

Real returns ecore::EBigDecimal hidden():
	INT ("." INT)?;

QualifiedName hidden():
	ID ("." ID)* | QUOTED_ID;

@Override
terminal STRING returns ecore::EString:
	'"' ( '\\' . /* 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' */ | !('\\'|'"') )* '"';

terminal QUOTED_ID returns ecore::EString:
	'\'' ( '\\' . /* 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' */ | !('\\'|'\'') )* '\'';

terminal PLUS:
	"synthetic::plus";

terminal STAR:
	"synthetic::star";

terminal DOT:
	"synthetic::dot";

NamedElement:
	name=QualifiedName;