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: Interpretation | Predicate;

@Override terminal STRING returns ecore::EString: '"' ( '\\' . /* 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' */ | !('\\'|'"') )* '"';
REALLiteral returns ecore::EBigDecimal: '-'? INT '.' INT;
INTLiteral returns ecore::EInt: '-'? INT;
BooleanValue: {BooleanTrue} 'true' | 'false' {BooleanFalse};
TruthValue: {True} 'true'  | {False} 'false'  | {Unknown} 'unknown' |  {Error} 'error' ;


///////////////////
// Core grammar
///////////////////
Interpretation: BasicInterpretation | DefaultInterpretation | CDInterpretation;

BasicInterpretation: symbol=Symbol ('(' (objects+=ComplexObject (',' objects+=ComplexObject)*)? ')')? ':' value = TruthValue;

Symbol: ModelSymbol | PartialitySymbol | DataSymbol;

ModelSymbol: name = ID;

PartialitySymbol: ExistSymbol | EqualsSymbol;
ExistSymbol:'exists'{ExistSymbol};
EqualsSymbol:'equals' {EqualsSymbol};

DataSymbol: BooleanSymbol | IntegerSymbol | RealSymbol | StringSymbol;
BooleanSymbol:'bool' {BooleanSymbol};
IntegerSymbol:'int' {IntegerSymbol};
RealSymbol: 'real' {RealSymbol};
StringSymbol:'string' {StringSymbol};

ComplexObject: Object | AllInstances | AllObjects;

Object: NamedObject | UnnamedObject | DataObject;
NamedObject: "'" name = ID "'";
UnnamedObject: name = ID;
DataObject: BooleanObject | IntObject | RealObject | StringObject;
BooleanObject: value = BooleanValue;
IntObject: value = INTLiteral;
RealObject: value = REALLiteral;
StringObject: value = STRING;

///////////////////
// Predicte grammar
///////////////////

Predicate:
	(isError?='error')? symbol = ModelSymbol ('(' (parameters += Parameter (',' parameters += Parameter)*)? ')')? ':-' ('false' | (bodies += PatternBody ('|' bodies += PatternBody)*)) '.'
;

Parameter: variable = Variable (':' type = Symbol)?;
PatternBody: {PatternBody} ('true' | constraints += Constraint*) ;
Polarity: {Positive} '+' | {Negative} '-';
Constraint: (polarity = Polarity)?  symbol = ModelSymbol 
	(('(' params += Literal? (',' params += Literal)* ')')?)
	|
	(closureType=ClosureType '(' params += Literal? (',' params += Literal)* ')');
ClosureType: {ReflexiveClosure} '*' | {IrreflexiveClosure} '+';
Literal: Variable | DataObject | NamedObject;
Variable: name = ID;

///////////////////
// Complex Interpretation grammar
///////////////////

AllInstances: ':' symbol = Symbol;
AllObjects: {AllObjects} '*';

///////////////////
// Defaul Interpretation grammar
///////////////////
DefaultInterpretation: 'default' interpretation = BasicInterpretation;

///////////////////
// Advanced Class-Diagram interpretations
///////////////////
CDInterpretation: ClassInterpretation | EnumInterpretation| GlobalRelationInterpretation;
ClassInterpretation:
	(abstract?='abstract')? 'class' symbol = ModelSymbol ('extends' supertypes += ModelSymbol+)?'{'
	fielt += FieldRelationInterpretation*
	'}'
;
EnumInterpretation: 'enum' Symbol = ModelSymbol '{' objects+=NamedObject+ '}';
FieldRelationInterpretation: (containment ?= 'containment')? symbol = ModelSymbol ':' multiplicity = MultiplicityDefinition? target = Symbol;
GlobalRelationInterpretation: (containment ?= 'containment')? 'relation' symbol = ModelSymbol ':' sourceMultiplicity = MultiplicityDefinition? source = Symbol targetMultiplicity = MultiplicityDefinition? target = Symbol;
MultiplicityDefinition: lower = INT '..' (upper = INT | unlimitedUpper?='*');

////SymbolIntroduction : Type | GlobalRelation | Predicate;
////Symbol: Type | Relation | Predicate | Variable | Element;
//
//////////////////////
//// Types
//////////////////////
//
//Type: TypeDeclaration | /*TypeDefinition |*/ TypeEnumeration;
//
//TypeDeclaration:
//	abstract?= 'abstract' 'class' name = ID ('extends' supertypes += [Type] (',' supertypes += [Type])) '{'
//		fieldDeclarations += FieldRelationDeclaration*
//	'}'
//;
//TypeEnumeration:
//	'enum' name = ID 'extends' supertypes += [Type] (',' supertypes += [Type]) '{'
//		(elements += Element)*
//	'}'
//;
//Element:
//	name = ID
//;
//
//////////////////////
//// Relations
//////////////////////
//
//Relation: FieldRelationDeclaration | GlobalRelationDeclaration | RelationEnumeration;
//GlobalRelation returns Relation: GlobalRelationDeclaration | /*RelationDefinition |*/ RelationEnumeration;
//
//FieldRelationDeclaration:
//	containment?='containment' target = [Type] name = ID
//;
//
//GlobalRelationDeclaration:
//	containment?='containment' 'relation' name = ID '(' source = [Type] ',' target = [Type] ')'
//;
//
//RelationEnumeration:
//	'relation' name = ID '{' links += Link* '}'
//;
//
//Link: '(' source = Element ',' target = Element ')';
//
//
//
//
//
//
//Model:
//	'model' '{'
//		atoms += Atom (',' atoms += Atom )
//	'}'
//;
//Atom: referredSymbol = [Symbol] '(' (params += Element (',' params += Element)*)? ')';
//
//ScopeDeclaration:
//	'scope'
//;
//