/*
* SPDX-FileCopyrightText: 2021-2024 The Refinery Authors
*
* SPDX-License-Identifier: EPL-2.0
*/
@detectDelim
@external prop implicitCompletion from './props'
@precedence {
cast,
prefix,
range @left,
exponential @right,
multiplicative @left,
additive @left,
lattice @left,
comparison @left,
boolean @left,
assignment,
feature @cut
}
@top Problem { statement* }
statement {
ImportStatement {
kw<"import"> ModuleName (kw<"as"> ModuleName)? "."
} |
Assertion {
kw<"default">? (NotOp | UnknownOp)? RelationName
ParameterList
(":" Expr)? "."
} |
ProblemDeclaration {
(ckw<"module"> | kw<"problem">) ModuleName "."
} |
ClassDefinition {
kw<"abstract">? kw<"class"> RelationName
(kw<"extends"> sep<",", RelationName>)?
(ClassBody { "{" FeatureDeclaration* "}" } | ".")
} |
EnumDefinition {
kw<"enum"> RelationName
(EnumBody { "{" sep<",", AtomNodeName> "}" } | ".")
} |
DatatypeDeclaration {
kw<"extern"> ckw<"datatype"> DatatypeName "."
} |
AggregatorDeclaration {
kw<"extern"> ckw<"aggregator"> AggregatorName "."
} |
PredicateDefinition {
(
(kw<"error"> | ckw<"contained"> | kw<"containment">)? kw<"pred"> |
kw<"error">
)
RelationName ParameterList?
PredicateBody { ("<->" sep)? "." }
} |
// FunctionDefinition {
// kw<"fn"> RelationName RelationName ParameterList?
// FunctionBody { ("=" sep)? "." }
// } |
//RuleDefinition {
// kw<"rule">
// RuleName ParameterList?
// RuleBody { ":" sep "==>" sep "." }
//} |
AtomDeclaration {
kw<"declare">? ckw<"atom"> sep<",", AtomNodeName> "."
} |
NodeDeclaration {
(kw<"declare"> | kw<"declare">? ckw<"multi">) sep<",", NodeName> "."
} |
ScopeDeclaration {
kw<"scope"> sep<",", ScopeElement> "."
}
}
FeatureDeclaration {
// Prefer parsing `contains` as a contextual keyword.
(
FeatureDeclarationHeadWithKind[@dynamicPrecedence=1] {
ReferenceKind !feature ~featureHead
} |
FeatureDeclarationHeadWithoutKind {
~featureHead
}
)
RelationName
("[" Multiplicity? "]")?
RelationName
(kw<"opposite"> RelationName)?
";"?
}
Parameter { RelationName? VariableName }
// Use @dynamicPrecedence to prevent a(b) from being parsed as Expr { a } Expr { b }
// instead of Atom { a(b) }
// Being looser with token sequencing enables more consistent syntactic highlighting.
Conjunction { ("," | NextConjunction[@dynamicPrecedence=-10] { Expr })+ }
// Case { Conjunction ("->" Expr)? }
OrOp { ";" }
Expr {
AssignmentExpr | UnaryExpr | BinaryExpr | CastExpr | Aggregation |
VariableName | Atom | Constant | "(" Expr ")"
}
AssignmentExpr { !assignment VariableName kw<"is"> Expr }
BinaryExpr {
Expr !boolean ("&&" | "||" | "^^") Expr |
Expr !comparison ComparisonOp Expr |
Expr !lattice (LatticeMeet | "\\/") Expr |
Expr !additive ("+" | "-") Expr |
Expr !multiplicative (Star | Divide) Expr |
Expr !exponential "**" Expr |
Expr !range ".." Expr
}
UnaryExpr {
!prefix ("+" | "-" | "!" | kw<"count">) Expr
}
CastExpr { !cast Expr kw<"as"> DatatypeName }
Aggregation {
AggregatorName "{" Expr "|" Expr "}"
}
Atom { RelationName "+"? ParameterList }
//Consequent { ("," | Action)+ }
//Action {
// ckw<"new"> VariableName ("<:" VariableName)? |
// kw<"delete"> VariableName |
// Literal
//}
AssertionArgument { NodeName | StarArgument }
Constant { Real | String | StarMult | LogicValue }
ReferenceKind {
kw<"refers"> | ckw<"contains"> | kw<"container">
}
LogicValue {
kw<"true"> | kw<"false"> | kw<"unknown"> | kw<"error">
}
ComparisonOp { SymbolicComparisonOp | kw<"in"> }
ScopeElement { RelationName ("=" | "+=") Multiplicity }
Multiplicity { (IntMult "..")? (IntMult | StarMult)}
// The ~name handles the ambiguity between transitve closure a+(b, c) and addition a+(b)
// in the grammar. We prefer the addition interpretation by applying @dynamicPrecedence=1
// to the VariableName rule,
// but will go with the transtive closure (and highlight `a` as a relation) if forced.
RelationName { QualifiedName ~name }
DatatypeName { QualifiedName }
//RuleName { QualifiedName }
AtomNodeName { QualifiedName }
VariableName[@dynamicPrecedence=10] { QualifiedName ~name }
NodeName { QualifiedName }
ModuleName { QualifiedName }
AggregatorName { QualifiedName }
QualifiedName[implicitCompletion=true] { "::"? identifier (QualifiedNameSeparator "::" identifier)* }
StarMult { Star }
kw { @specialize[@name={term},implicitCompletion=true] }
ckw { @extend[@name={term},implicitCompletion=true] }
ParameterList { "(" sep<",", content> ")" }
sep { sep1? }
sep1 { content (separator content)* }
@skip { LineComment | BlockComment | whitespace }
@external tokens qualifiedNameSeparator from "./tokens" {
QualifiedNameSeparator
}
@tokens {
whitespace { std.whitespace+ }
LineComment { ("//" | "%") ![\n]* }
BlockComment { "/*" blockCommentRest }
blockCommentRest { ![*] blockCommentRest | "*" blockCommentAfterStar }
blockCommentAfterStar { "/" | "*" blockCommentAfterStar | ![/*] blockCommentRest }
Divide { "/" }
LatticeMeet { "/\\" }
@precedence { BlockComment, LineComment, LatticeMeet, Divide }
identifier { $[A-Za-z_] $[a-zA-Z0-9_]* }
int { $[0-9]+ }
IntMult { int }
Star { "*" }
Real { (exponential | int ("." (int | exponential))?) }
exponential { int ("e" | "E") ("+" | "-")? int }
String {
"'" (![\\'\n] | "\\" ![\n] | "\\\n")+ "'" |
"\"" (![\\"\n] | "\\" (![\n] | "\n"))* "\""
}
SymbolicComparisonOp {
">" | ">=" | "<" | "<=" | "==" | "!=" |
"===" | "!=="
}
NotOp { "!" }
UnknownOp { "?" }
StarArgument { "*" }
"{" "}" "(" ")" "[" "]" "." ".." "," ":" "->" "<->" "+" "-" "**" "=" "+="
}