/*
 * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors <https://refinery.tools/>
 *
 * SPDX-License-Identifier: EPL-2.0
 */
grammar tools.refinery.language.Problem with org.eclipse.xtext.common.Terminals

import "http://www.eclipse.org/emf/2002/Ecore" as ecore
import "https://refinery.tools/emf/2021/Problem"

Problem:
	(kind=ModuleKind name=QualifiedName? ".")?
	statements+=Statement*;

enum ModuleKind:
	PROBLEM="problem" | MODULE="module";

Statement:
	ImportStatement | Assertion | ClassDeclaration | EnumDeclaration |
	PredicateDefinition | /* FunctionDefinition | RuleDefinition | */
	ScopeDeclaration | NodeDeclaration;

ImportStatement:
	"import" importedModule=[Problem|QualifiedName] ("as" alias=ID)? ".";

ClassDeclaration:
	abstract?="abstract"? "class"
	name=Identifier
	("extends" superTypes+=[Relation|QualifiedName] ("," superTypes+=[Relation|QualifiedName])*)?
	("{" (featureDeclarations+=FeatureDeclaration ";"?)* "}" | ".");

EnumDeclaration:
	"enum"
	name=Identifier
	("{" (literals+=EnumLiteral ("," literals+=EnumLiteral)* ("," | ";")?)? "}" | ".");

EnumLiteral returns Node:
	name=Identifier;

FeatureDeclaration:
	ReferenceDeclaration /* | AttributeDeclaration | FlagDeclaration */;

enum ReferenceKind:
	REFERENCE="refers" | CONTAINMENT="contains" | CONTAINER="container";

ReferenceDeclaration:
	(referenceType=[Relation|NonContainmentQualifiedName] |
	kind=ReferenceKind referenceType=[Relation|QualifiedName])
	(multiplicity=ReferenceMultiplicity)?
	name=Identifier
	("opposite" opposite=[ReferenceDeclaration|QualifiedName])?;

ReferenceMultiplicity returns Multiplicity:
	"[" Multiplicity "]";

//enum PrimitiveType:
//	INT="int" | REAL="real" | STRING="string";
//
//AttributeDeclaration:
//	attributeType=PrimitiveType name=Identifier;
//
//FlagDeclaration:
//	"bool" name=Identifier;

PredicateDefinition:
	("pred" | error?="error" "pred"?)
	name=Identifier
	"(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")"
	("<->" bodies+=Conjunction (";" bodies+=Conjunction)*)?
	".";

Conjunction:
	literals+=Expr ("," literals+=Expr)*;

//FunctionDefinition:
//	"fn" functionType=PrimitiveType name=Identifier
//	"(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")"
//	("=" cases+=Case (";" cases+=Case)*)?
//	".";
//
//Case:
//	Conjunction ({Match.condition=current} "->" value=Expr)?;

//RuleDefinition:
//	"rule"
//	name=Identifier
//	"(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")"
//	(":" preconditions+=Conjunction (";" preconditions+=Conjunction)*)?
//	"==>" consequents+=Consequent (";" consequents+=Consequent)*)?
//	".";

Parameter:
	parameterType=[Relation|QualifiedName]? name=Identifier;

//Consequent:
//	actions+=Action ("," actions+=Action)*;
//
//Action:
//	AssertionAction | DeleteAction | NewAction;
//
//AssertionAction:
//	value=ShortLogicValue? atom=Atom |
//	atom=Atom (overwrite?=":=" | "<:") value=LogicValue;
//
//DeleteAction:
//	"delete" variableOrNode=[VariableOrNode|QualifiedName];
//
//NewAction:
//	"new" variable=NewVariable ("<:" parent=[VariableOrNode|QualifiedName])?;
//
//NewVariable:
//	name=Identifier;

Expr:
	ComparisonExpr;

enum ComparisonOp:
	LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | EQ="==" | NOT_EQ="!=" |
	IN="in" | SUBSUMES=":>" | SUBSUMED_BY="<:" | ABS_EQ="===" | ABS_NOT_EQ="!==";

ComparisonExpr returns Expr:
	LatticeExpr ({ComparisonExpr.left=current}
	op=ComparisonOp right=LatticeExpr)*;

enum LatticeOp returns BinaryOp:
	MEET="/\\" | JOIN="\\/";

LatticeExpr returns Expr:
	RangeExpr ({ArithmeticBinaryExpr.left=current}
	op=LatticeOp right=RangeExpr)*;

RangeExpr returns Expr:
	AdditiveExpr ({RangeExpr.left=current} ".." right=AdditiveExpr)*;

enum AdditiveOp returns BinaryOp:
	ADD="+" | SUB="-";

AdditiveExpr returns Expr:
	MultiplicativeExpr ({ArithmeticBinaryExpr.left=current}
	op=AdditiveOp right=MultiplicativeExpr)*;

enum MultiplicativeOp returns BinaryOp:
	MUL="*" | DIV="/";

MultiplicativeExpr returns Expr:
	ExponentialExpr ({ArithmeticBinaryExpr.left=current}
	op=MultiplicativeOp right=ExponentialExpr)*;

enum ExponentialOp returns BinaryOp:
	POW="**";

ExponentialExpr returns Expr:
	UnaryExpr ({ArithmeticBinaryExpr.left=current}
	op=ExponentialOp right=ExponentialExpr)?;

UnaryExpr returns Expr:
	ArithmeticUnaryExpr | ModalExpr | NegationExpr | CountExpr | AggregationExpr |
	Atom | VariableOrNodeExpr | Constant | "(" Expr ")";

enum UnaryOp:
	PLUS="+" | MINUS="-";

ArithmeticUnaryExpr:
	op=UnaryOp body=UnaryExpr;

enum Modality:
	MAY="may" | MUST="must" | CURRENT="current";

ModalExpr:
	modality=Modality body=UnaryExpr;

NegationExpr:
	"!" body=UnaryExpr;

CountExpr:
	"count" body=UnaryExpr;

enum AggregationOp:
	SUM="sum" | PROD="prod" | MIN="min" | MAX="max";

AggregationExpr:
	op=AggregationOp "{" value=Expr "|" condition=Expr "}";

Atom:
	relation=[Relation|QualifiedName]
	transitiveClosure?=TRANSITIVE_CLOSURE?
	"(" (arguments+=Expr ("," arguments+=Expr)*)? ")";

VariableOrNodeExpr:
	variableOrNode=[VariableOrNode|QualifiedName];

Constant:
	RealConstant | IntConstant | InfConstant | StringConstant | LogicConstant;

IntConstant:
	intValue=INT;

RealConstant:
	realValue=Real;

InfConstant:
	{InfConstant} "*";

StringConstant:
	stringValue=STRING;

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

LogicConstant:
	logicValue=LogicValue;

Assertion:
	default?="default"?
	(relation=[Relation|QualifiedName]
	"(" (arguments+=AssertionArgument ("," arguments+=AssertionArgument)*)? ")"
	":" value=Expr |
	value=ShortLogicConstant
	relation=[Relation|QualifiedName]
	"(" (arguments+=AssertionArgument ("," arguments+=AssertionArgument)*)? ")")
	".";

AssertionArgument:
	NodeAssertionArgument | WildcardAssertionArgument;

NodeAssertionArgument:
	node=[Node|QualifiedName];

WildcardAssertionArgument:
	{WildcardAssertionArgument} "*";

enum ShortLogicValue returns LogicValue:
	FALSE="!" | UNKNOWN="?";

ShortLogicConstant returns LogicConstant:
	{LogicConstant} logicValue=ShortLogicValue?;

ScopeDeclaration:
	"scope" typeScopes+=TypeScope ("," typeScopes+=TypeScope)* ".";

TypeScope:
	targetType=[Relation|QualifiedName]
	(increment?="+=" | "=")
	multiplicity=DefiniteMultiplicity;

Multiplicity:
	UnboundedMultiplicity | DefiniteMultiplicity;

DefiniteMultiplicity returns Multiplicity:
	RangeMultiplicity | ExactMultiplicity;

UnboundedMultiplicity:
	{UnboundedMultiplicity};

RangeMultiplicity:
	lowerBound=INT ".." upperBound=UpperBound;

ExactMultiplicity:
	exactValue=INT;

NodeDeclaration:
	("declare" | "declare"? kind=NodeKind)
	nodes+=EnumLiteral ("," nodes+=EnumLiteral)* ".";

enum NodeKind:
	ATOM="atom" | MULTI="multi";

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

QualifiedName hidden():
	"::"? Identifier (QUALIFIED_NAME_SEPARATOR Identifier)*;

NonContainmentQualifiedName hidden():
	(NonContainmentIdentifier | "::" Identifier) (QUALIFIED_NAME_SEPARATOR Identifier)*;

Identifier:
	NonContainmentIdentifier | "contains" | "container";

NonContainmentIdentifier:
	ID | "atom" | "multi" | "contained" |
	"sum" | "prod" | "min" | "max" | "problem" | "module";

Real returns ecore::EDouble:
	EXPONENTIAL | INT "." (INT | EXPONENTIAL);

terminal TRANSITIVE_CLOSURE:
	"synthetic:TRANSITIVE_CLOSURE";

terminal QUALIFIED_NAME_SEPARATOR:
	"synthetic::QUALIFIED_NAME_SEPARATOR";

@Override
terminal ID:
	('a'..'z' | 'A'..'Z' | '_') ('a'..'z' | 'A'..'Z' | '_' | '0'..'9')*;

terminal EXPONENTIAL:
	INT ("e" | "E") ("+" | "-")? INT;

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