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

Problem:
	(statements+=Statement)*;

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

AssertionOrDefinition returns Statement:
	Expression (
		{Interpretation.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;

MetricDefinition:
	type=[NamedElement|QualifiedName] head=Call "=" body=Expression;

ExternPredicateDefinition:
	"extern" name=QualifiedName argumentList=ArgumentList;

ExternMetricDefinition:
	"extern" type=[NamedElement|QualifiedName] name=QualifiedName argumentList=ArgumentList;

ExternAggregatorDefinition:
	"extern" type=[NamedElement|QualifiedName] name=QualifiedName "{" inputType=[NamedElement|QualifiedName] "..." "}";

ExternDatatypeDefinition:
	"extern" "datatype" name=QualifiedName ("extends" supertypes+=[NamedElement|QualifiedName] ("," supertypes+=[NamedElement|QualifiedName])*);

Variable:
	type=[NamedElement|QualifiedName]? name=ID;

Expression:
	IfElse | Let | ImplicationExpression;

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

Let:
	"let" bindings+=LetBinding ("," bindings+=LetBinding)* "in" body=Expression;

LetBinding:
	variable=Variable "=" value=AdditiveExpression;

enum ImplicationOperator returns BinaryOperator:
	IMPLIES = "=>";

ImplicationExpression returns Expression:
	DisjunctiveExpression ({BinaryExpression.left=current} op=ImplicationOperator right=ImplicationExpression)?;

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 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:
	CastExpression ({BinaryExpression.left=current} op=ExponentialOp right=CastExpression)?;

CastExpression returns Expression:
	UnaryExpression ({CastExpression.body=current} "as" type=[NamedElement|QualifiedName])?;

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

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

AggregationExpression returns Expression:
	AtomicExpression | QuantifiedExpression | Aggregation;

LocalVariables:
	{LocalVariables} "[" (variables+=Variable ("," variables+=Variable)*)? "]";

enum Quantifier:
	EXISTS="exists" | FORALL="forall" | COUNT="count";

QuantifiedExpression:
	quantifier=Quantifier localVariables=LocalVariables? "{" body=Expression "}";

Aggregation:
	op=[NamedElement|QualifiedName] localVariables=LocalVariables? "{" body=Expression ("|" condition=Expression)? "}";

AtomicExpression returns Expression:
	Reference | Call | Interval | Literal | "(" Expression ")";

Call:
	functor=Reference (transitiveClosure?=TRANSITIVE_CLOSURE | reflexiveTransitiveClosure?=REFLEXIVE_TRANSITIVE_CLOSURE)? 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:
	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:
	'\'' ( '\\' . /* 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' */ | !('\\'|'\'') )* '\'';

@Override
terminal SL_COMMENT:
	('%' | '//') !('\n'|'\r')* ('\r'? '\n')?;

terminal TRANSITIVE_CLOSURE:
	"synthetic:TRANSITIVE_CLOSURE";

terminal REFLEXIVE_TRANSITIVE_CLOSURE:
	"synthetic:REFLEXIVE_TRANSITIVE_CLOSURE";

terminal FULL_STOP:
	"synthetic:FULL_STOP";