BNF for LogicParser.jj

NON-TERMINALS

parseFormulas	::=	"{" expression ( "," expression )* "}" <EOF>
	\|	"{" "}" <EOF>
	\|	parseFormula
parseFormula	::=	expression <EOF>
parseTerm	::=	term <EOF>
parseType	::=	typeUse <EOF>
expression	::=	FreeDeclarationExpression
FreeDeclarationExpression	::=	( <DECLARE_FREE> VariableDeclaration )* EquivalenceExpression
EquivalenceExpression	::=	ImplicationExpression ( <EQUIV> ImplicationExpression )*
ImplicationExpression	::=	InclusiveOrExpression ( <IMPLY> ImplicationExpression )?
InclusiveOrExpression	::=	ExclusiveOrExpression ( <OR> ExclusiveOrExpression )*
ExclusiveOrExpression	::=	AndExpression ( <XOR> AndExpression )*
AndExpression	::=	UnaryExpression ( <AND> UnaryExpression )*
UnaryExpression	::=	<NOT> UnaryExpression
	\|	ModalExpression
	\|	QuantifiedExpression
	\|	PrimaryExpression
QuantifiedExpression	::=	( <FORALL> ( VariableDeclaration \| <LAMBDA> VariableDeclaration "." ) )+ UnaryExpression
	\|	( <EXISTS> ( VariableDeclaration \| <LAMBDA> VariableDeclaration "." ) )+ UnaryExpression
ModalExpression	::=	<BOX> UnaryExpression
	\|	<DIAMOND> UnaryExpression
PrimaryExpression	::=	( Atom \| "(" expression ")" )
Atom	::=	CompoundFormula
	\|	<IDENTIFIER>
	\|	NumberLiteralValue
CompoundFormula	::=	EqualityExpression
	\|	<IDENTIFIER> Arguments
	\|	"[" <IDENTIFIER> ":" typeUse "]" Arguments
	\|	LambdaAbstractionPredicate Arguments
EqualityExpression	::=	"(" term ( ( <EQUAL> \| <UNEQUAL> \| <LESS> \| <GREATER> \| <LESS_EQUAL> \| <GREATER_EQUAL> ) term )+ ")"
LambdaAbstractionPredicate	::=	"(" <LAMBDA> VariableDeclaration "." expression ")"
term	::=	SumTerm
SumTerm	::=	ProductTerm ( ( <PLUS> \| <MINUS> ) ProductTerm )*
ProductTerm	::=	PowerTerm ( ( <TIMES> \| <DIVIDE> ) PowerTerm )*
PowerTerm	::=	UnaryTerm ( <XOR> PowerTerm )?
UnaryTerm	::=	( <PLUS> \| <MINUS> ) UnaryTerm
	\|	PrimaryTerm
PrimaryTerm	::=	( CompoundTerm \| AtomicTerm \| "(" term ")" )
CompoundTerm	::=	<IDENTIFIER> Arguments
	\|	LambdaAbstraction Arguments
LambdaAbstraction	::=	"(" <LAMBDA> VariableDeclaration "." term ")"
AtomicTerm	::=	( LiteralValue \| ConstantOrVariable )
LiteralValue	::=	NumberLiteralValue
	\|	<STRING_LITERAL>
NumberLiteralValue	::=	<INTEGER_LITERAL>
	\|	<FLOATING_POINT_LITERAL>
ConstantOrVariable	::=	<IDENTIFIER>
Variable	::=	<IDENTIFIER>
VariableDeclaration	::=	<IDENTIFIER> ( ":" typeUse )?
typeUse	::=	type
type	::=	MapType
MapType	::=	ProductType ( <IMPLY> ProductType )*
ProductType	::=	PrimaryType ( <PRODUCT> PrimaryType )*
PiAbstractionType	::=	"(" <PI> <IDENTIFIER> "." type ")"
PrimaryType	::=	<IDENTIFIER>
	\|	"[" CompoundType "]"
	\|	PiAbstractionType
	\|	"(" type ")"
CompoundType	::=	<IDENTIFIER> Types
Arguments	::=	"(" ( Argument_list )? ")"
Argument_list	::=	term ( "," term )*
Types	::=	"(" ( Type_list )? ")"
Type_list	::=	type ( "," type )*

BNF for LogicParser.jj Part 2

TERMINALS

<DECLARE_FREE>	::=	"$" \| "free"
<EQUIV>	::=	"↔" \| "⇔" \| "<->" \| "<=>"
<IMPLY>	::=	"→" \| "⇒" \| "⊃" \| "->" \| "=>"
<OR>	::=	"∨" \| "\|" \| "\|\|"
<XOR>	::=	"∨̇" \| "xor" \| "^"
<AND>	::=	"∧" \| "&" \| "&&"
<NOT>	::=	"¬" \| "~" \| "!"
<EXISTS>	::=	"∃" \| "?" \| "some"
<FORALL>	::=	"∀" \| "°" \| "all"
<BOX>	::=	"□" \| "[]"
<DIAMOND>	::=	"◇" \| "<>"
<EQUAL>	::=	"=" \| "=="
<UNEQUAL>	::=	"≠" \| "!="
<LESS>	::=	"<"
<GREATER>	::=	">"
<LESS_EQUAL>	::=	"≤" \| "=<"
<GREATER_EQUAL>	::=	"≥" \| ">="
<PLUS>	::=	"+"
<MINUS>	::=	"-"
<TIMES>	::=	"⋅" \| "*"
<DIVIDE>	::=	"∕" \| "/"
<LAMBDA>	::=	"λ" \| "\"
<PI>	::=	"Π" \| "\\"
<IDENTIFIER>	::=	["A"-"Z","_"] ["A"-"Z","_","0"-"9"]*
<INTEGER_LITERAL>	::=	["0"-"9"]+
<FLOATING_POINT_LITERAL>	::=	["0"-"9"]+ "." ["0"-"9"]+ (["e","E"] ["+","-"]? ["0"-"9"]+)?
<STRING_LITERAL>	::=	"\"" ~["\"","\n",...]* "\""

Quantifiers and modal operators bind strong. The precedence order is thus

↔,⊃,∨,∨̇,∧,¬,∃,∀,□,◇,=,≠,<,≤,>,≥ where ∀ binds stronger than ∧ etc.