Definition of parser RParser, which is a subclass of LLkParser.


module
	:	(	proof_module 
		|	theory_module 
		|	conceptual_module 
		|	realization_body_module 
		|	enhancement_module 
		|	facility_module 
		) 
		EOF 
	;


proof_module
	:	PROOFS_FOR ident SEMICOLON 
		(	module_formal_param_section 
		|	
		) 
		(	uses_list 
		|	
		) 
		(	proof_module_body 
		|	
		) 
		END ident SEMICOLON 
	;


theory_module
	:	THEORY ident 
		(	module_formal_param_section 
		|	
		) 
		SEMICOLON 
		(	uses_list 
		|	
		) 
		(	math_item_sequence 
		|	
		) 
		END 
		(	ident 
		|	
		) 
		SEMICOLON 
	;


conceptual_module
	:	MODULE_CONCEPT ident 
		(	module_formal_param_section 
		|	
		) 
		SEMICOLON 
		(	uses_list 
		|	
		) 
		(	requires_clause 
		|	
		) 
		(	concept_item_sequence 
		|	
		) 
		END 
		(	ident 
		|	
		) 
		SEMICOLON 
	;


realization_body_module
	:	MODULE_REALIZATION ident 
		(	module_formal_param_section 
		|	
		) 
		FOR 
		(	body_enhancement_section 
		|	body_concept_section 
		) 
		SEMICOLON 
		(	uses_list 
		|	
		) 
		(	requires_clause 
		|	
		) 
		(	body_item_sequence 
		|	
		) 
		END 
		(	ident 
		|	
		) 
		SEMICOLON 
	;


enhancement_module
	:	MODULE_ENHANCEMENT ident 
		(	module_formal_param_section 
		|	
		) 
		FOR 
		(	CONCEPT 
		|	
		) 
		ident SEMICOLON 
		(	uses_list 
		|	
		) 
		(	requires_clause 
		|	
		) 
		(	enhancement_item_sequence 
		|	
		) 
		END 
		(	ident 
		|	
		) 
		SEMICOLON 
	;


facility_module
	:	FACILITY ident 
		(	short_facility_section 
			(	uses_list 
			|	
			) 
		|	SEMICOLON 
			(	uses_list 
			|	
			) 
			(	facility_item_sequence 
			|	
			) 
			END 
			(	ident 
			|	
			) 
			SEMICOLON 
		) 
	;


ident
	:	IDENTIFIER 
	;


module_formal_param_section
	:	LPAREN module_parameter ( SEMICOLON module_parameter )* RPAREN 
	;


uses_list
	:	( uses_clause )+ 
	;


math_item_sequence
	:	( math_item )+ 
	;


math_item
	:	formal_type_declaration 
	|	math_type_declaration 
	|	definition_declaration 
	|	math_assertion_declaration 
	|	subtype_declaration 
	;


formal_type_declaration
	:	LOCAL_MATH_TYPE ident SEMICOLON 
	;


math_type_declaration
	:	MATH_TYPE ident COLON math_type_expression SEMICOLON 
	;


definition_declaration
	:	implicit_definition_declaration 
	|	inductive_definition_declaration 
	|	standard_definition_declaration 
	;


math_assertion_declaration
	:	(	AXIOM 
		|	THEOREM 
		|	PROPERTY 
		|	LEMMA 
		|	COROLLARY 
		|	( COMMUTATIVITY ) THEOREM 
		) 
		(	math_theorem_ident 
		|	
		) 
		COLON math_expression SEMICOLON 
	;


subtype_declaration
	:	MATH_SUBTYPE 
		(	qualified_type 
		|	ident 
		) 
		COLON 
		(	qualified_type 
		|	ident 
		) 
		SEMICOLON 
	;


requires_clause
	:	REQUIRES math_expression SEMICOLON 
	;


concept_item_sequence
	:	( concept_item )+ 
	;


concept_item
	:	confirm_math_type_declaration 
	|	concept_state_variable_declaration 
	|	constraint_clause 
	|	module_concept_init_declaration 
	|	module_concept_final_declaration 
	|	type_declaration 
	|	operation_declaration 
	|	definition_declaration 
	;


confirm_math_type_declaration
	:	CONFIRM MATH_TYPE math_variable_declaration SEMICOLON 
	;


concept_state_variable_declaration
	:	VAR math_variable_declaration_group SEMICOLON 
	;


constraint_clause
	:	CONSTRAINT math_expression SEMICOLON 
	;


module_concept_init_declaration
	:	FAC_INIT concept_init_final_section 
	;


module_concept_final_declaration
	:	FAC_FINAL concept_init_final_section 
	;


type_declaration
	:	TYPE_FAMILY ident 
		(	SUBSET 
		|	MODELED 
		) 
		structural_math_type_expression SEMICOLON EXEMPLAR ident SEMICOLON 
		(	constraint_clause 
		|	
		) 
		(	type_concept_init_declaration 
		|	
		) 
		(	type_concept_final_declaration 
		|	
		) 
	;


operation_declaration
	:	OPERATION ident ( operation_formal_param_section ) 
		(	COLON program_type_expression 
		|	
		) 
		SEMICOLON ( affects_clause )* 
		(	requires_clause 
		|	
		) 
		(	ensures_clause 
		|	
		) 
	;


enhancement_item_sequence
	:	( enhancement_item )+ 
	;


enhancement_item
	:	concept_state_variable_declaration 
	|	type_declaration 
	|	operation_declaration 
	|	definition_declaration 
	|	defines_declaration 
	;


defines_declaration
	:	DEFINES definition_signature SEMICOLON 
	;


body_enhancement_section
	:	ident OF ident ( added_enhancement_section )* 
	;


body_concept_section
	:	ident ( ENHANCED_BY ident )* 
	;


body_item_sequence
	:	( body_item )+ 
	;


added_enhancement_section
	:	ENHANCED_BY ident 
		(	module_argument_section 
		|	
		) 
		REALIZED_BY ident 
		(	module_argument_section 
		|	
		) 
	;


module_argument_section
	:	LPAREN module_argument ( COMMA module_argument )* RPAREN 
	;


body_item
	:	state_variable_declaration 
	|	correspondence_clause 
	|	convention_clause 
	|	module_body_init_declaration 
	|	module_body_final_declaration 
	|	type_representation_declaration 
	|	aux_operation_declaration 
	|	operation_procedure_declaration 
	|	operation_recursive_procedure_declaration 
	|	procedure_declaration 
	|	recursive_procedure_declaration 
	|	definition_declaration 
	|	facility_declaration 
	;


state_variable_declaration
	:	VAR variable_declaration_group SEMICOLON 
	;


correspondence_clause
	:	CORR math_expression SEMICOLON 
	;


convention_clause
	:	CONVENTION math_expression SEMICOLON 
	;


module_body_init_declaration
	:	FAC_INIT body_init_final_section 
	;


module_body_final_declaration
	:	FAC_FINAL body_init_final_section 
	;


type_representation_declaration
	:	TYPE ident 
		(	EQL 
		|	REPRESENTED 
		) 
		structural_program_type_expression SEMICOLON 
		(	convention_clause 
		|	
		) 
		(	correspondence_clause 
		|	
		) 
		(	type_body_init_declaration 
		|	
		) 
		(	type_body_final_declaration 
		|	
		) 
	;


aux_operation_declaration
	:	AUX_OPERATION ident ( operation_formal_param_section ) 
		(	COLON program_type_expression 
		|	
		) 
		SEMICOLON ( affects_clause )* 
		(	requires_clause 
		|	
		) 
		(	ensures_clause 
		|	
		) 
	;


operation_procedure_declaration
	:	OPERATION ident ( operation_formal_param_section ) 
		(	COLON program_type_expression 
		|	
		) 
		SEMICOLON ( affects_clause )* 
		(	requires_clause 
		|	
		) 
		(	ensures_clause 
		|	
		) 
		PROCEDURE 
		(	decreasing_clause 
		|	
		) 
		( facility_declaration )* ( variable_declaration )* ( aux_variable_declaration )* statement_sequence END 
		(	ident 
		|	
		) 
		SEMICOLON 
	;


operation_recursive_procedure_declaration
	:	OPERATION ident ( operation_formal_param_section ) 
		(	COLON program_type_expression 
		|	
		) 
		SEMICOLON ( affects_clause )* 
		(	requires_clause 
		|	
		) 
		(	ensures_clause 
		|	
		) 
		RECURSIVE_PROCEDURE decreasing_clause ( facility_declaration )* ( variable_declaration )* ( aux_variable_declaration )* statement_sequence END 
		(	ident 
		|	
		) 
		SEMICOLON 
	;


procedure_declaration
	:	PROCEDURE ident ( operation_formal_param_section ) 
		(	COLON program_type_expression 
		|	
		) 
		SEMICOLON ( affects_clause )* 
		(	decreasing_clause 
		|	
		) 
		( facility_declaration )* ( variable_declaration )* ( aux_variable_declaration )* statement_sequence END 
		(	ident 
		|	
		) 
		SEMICOLON 
	;


recursive_procedure_declaration
	:	RECURSIVE_PROCEDURE ident ( operation_formal_param_section ) 
		(	COLON program_type_expression 
		|	
		) 
		SEMICOLON ( affects_clause )* decreasing_clause ( facility_declaration )* ( variable_declaration )* ( aux_variable_declaration )* statement_sequence END 
		(	ident 
		|	
		) 
		SEMICOLON 
	;


facility_declaration
	:	FACILITY ident IS ident 
		(	module_argument_section 
		|	
		) 
		( facility_enhancement )* REALIZED_BY ident 
		(	module_argument_section 
		|	
		) 
		( facility_body_enhancement )* SEMICOLON 
	;


short_facility_section
	:	IS ident 
		(	module_argument_section 
		|	
		) 
		( facility_enhancement )* REALIZED_BY ident 
		(	module_argument_section 
		|	
		) 
		( facility_body_enhancement )* SEMICOLON 
	;


facility_item_sequence
	:	( facility_item )+ 
	;


facility_enhancement
	:	ENHANCED_BY ident 
		(	module_argument_section 
		|	
		) 
	;


facility_body_enhancement
	:	ENHANCED_BY ident 
		(	module_argument_section 
		|	
		) 
		REALIZED_BY ident 
		(	module_argument_section 
		|	
		) 
	;


facility_item
	:	state_variable_declaration 
	|	module_facility_init_declaration 
	|	module_facility_final_declaration 
	|	facility_type_declaration 
	|	operation_procedure_declaration 
	|	operation_recursive_procedure_declaration 
	|	definition_declaration 
	|	facility_declaration 
	;


module_facility_init_declaration
	:	FAC_INIT facility_init_final_section 
	;


module_facility_final_declaration
	:	FAC_FINAL facility_init_final_section 
	;


facility_type_declaration
	:	TYPE ident 
		(	EQL 
		|	REPRESENTED 
		) 
		structural_program_type_expression SEMICOLON 
		(	convention_clause 
		|	
		) 
		(	type_facility_init_declaration 
		|	
		) 
		(	type_facility_final_declaration 
		|	
		) 
	;


module_parameter
	:	definition_parameter 
	|	constant_parameter 
	|	concept_type_parameter 
	|	operation_parameter 
	|	concept_realization_parameter 
	;


definition_parameter
	:	DEFINITION definition_signature 
	;


constant_parameter
	:	EVALUATES variable_declaration_group 
	;


concept_type_parameter
	:	TYPE ident 
	;


operation_parameter
	:	operation_declaration 
	;


concept_realization_parameter
	:	REALIZATION ident FOR 
		(	CONCEPT 
		|	
		) 
		ident 
	;


definition_signature
	:	(	infix_definition_construct 
		|	outfix_definition_construct 
		|	standard_definition_construct 
		) 
		COLON math_type_expression 
	;


variable_declaration_group
	:	variable_id_list COLON program_type_expression 
	;


uses_clause
	:	USES ident ( COMMA ident )* SEMICOLON 
	;


qualified_type
	:	ident DOT ident 
	;


math_type_expression
	:	function_type_expression 
	;


math_variable_declaration
	:	ident COLON math_type_expression 
	;


sset_type_expression
	:	sset_function_type_expression 
	;


sset_function_type_expression
	:	sset_domain_expression FUNCARROW SSET 
	|	SSET 
	;


sset_domain_expression
	:	( SSET ( (	IDENTIFIER 
				|	TIMES 
				) 
				SSET )* ) 
	|	SSET 
	;


math_theorem_ident
	:	ident 
	|	NUMERIC_LITERAL 
	;


math_expression
	:	(	iterated_construct 
		|	quantified_expression 
		) 
		
	;


math_variable_declaration_group
	:	variable_id_list COLON math_type_expression 
	;


state_aux_variable_declaration
	:	AUXVAR variable_declaration_group SEMICOLON 
	;


module_argument
	:	qualified_ident 
	|	program_expression 
	;


qualified_ident
	:	ident 
		(	DOT ident 
		|	
		) 
		
	;


program_expression
	:	program_logical_expression 
	;


implicit_definition_declaration
	:	IMPLICIT_DEF definition_signature 
		(	SEMICOLON 
		|	
		) 
		IS math_expression SEMICOLON 
	;


inductive_definition_declaration
	:	INDUCTIVE_DEF definition_signature 
		(	SEMICOLON 
		|	
		) 
		IS indexed_expression SEMICOLON indexed_expression SEMICOLON 
	;


standard_definition_declaration
	:	DEFINITION definition_signature 
		(	EQL math_expression 
		|	
		) 
		SEMICOLON 
	;


indexed_expression
	:	LPAREN ident RPAREN math_expression 
	;


infix_definition_construct
	:	singleton_definition_parameter 
		(	ident 
		|	infix_symbol 
		) 
		singleton_definition_parameter 
	;


outfix_definition_construct
	:	BAR singleton_definition_parameter BAR 
	|	DBL_BAR singleton_definition_parameter DBL_BAR 
	|	LT singleton_definition_parameter GT 
	|	LL singleton_definition_parameter GG 
	;


standard_definition_construct
	:	(	ident 
		|	prefix_symbol 
		|	quant_symbol 
		|	NUMERIC_LITERAL 
		) 
		(	definition_formal_param_section 
		|	
		) 
	;


singleton_definition_parameter
	:	LPAREN math_variable_declaration RPAREN 
	;


infix_symbol
	:	EQL 
	|	NOT_EQL 
	|	LT 
	|	GT 
	|	LT_EQL 
	|	GT_EQL 
	|	PLUS 
	|	MINUS 
	|	MULTIPLY 
	|	DIVIDE 
	|	EXP 
	|	MOD 
	|	REM 
	|	DIV 
	|	IMPLIES 
	|	IFF 
	|	AND 
	|	OR 
	|	XOR 
	|	ANDTHEN 
	|	ORELSE 
	|	COMPLEMENT 
	|	IN 
	|	NOT_IN 
	|	RANGE 
	|	UNION 
	|	INTERSECT 
	|	WITHOUT 
	|	SUBSET 
	|	PROP_SUBSET 
	|	NOT_SUBSET 
	|	NOT_PROP_SUBSET 
	|	CAT 
	|	SUBSTR 
	|	NOT_SUBSTR 
	;


prefix_symbol
	:	PLUS 
	|	MINUS 
	|	NOT 
	|	ABS 
	|	COMPLEMENT 
	;


quant_symbol
	:	BIG_UNION 
	|	BIG_INTERSECT 
	|	BIG_SUM 
	|	BIG_PRODUCT 
	|	BIG_CONCAT 
	;


definition_formal_param_section
	:	LPAREN math_variable_declaration_group ( COMMA math_variable_declaration_group )* RPAREN 
	;


operation_formal_param_section
	:	LPAREN 
		(	operation_formal_param_group ( SEMICOLON operation_formal_param_group )* 
		|	
		) 
		RPAREN 
	;


program_type_expression
	:	(	qualified_ident 
		|	ARRAY array_range OF program_type_expression 
		) 
		
	;


affects_clause
	:	abstract_mode qualified_ident ( COMMA qualified_ident )* SEMICOLON 
	;


ensures_clause
	:	ENSURES math_expression SEMICOLON 
	;


decreasing_clause
	:	DECREASING adding_expression SEMICOLON 
	;


variable_declaration
	:	VAR variable_declaration_group SEMICOLON 
	;


aux_variable_declaration
	:	AUXVAR aux_variable_declaration_group SEMICOLON 
	;


statement_sequence
	:	( statement SEMICOLON )* 
	;


operation_formal_param_group
	:	abstract_mode variable_declaration_group 
	;


abstract_mode
	:	ALTERS 
	|	CLEARS 
	|	EVALUATES 
	|	PRESERVES 
	|	REPLACES 
	|	RESTORES 
	|	UPDATES 
	|	REASSIGNS 
	;


aux_variable_declaration_group
	:	variable_id_list COLON program_type_expression 
	;


structural_math_type_expression
	:	CARTPROD ( cartprod_variable_declaration_group SEMICOLON )+ END 
	|	product_type_expression 
	;


type_concept_init_declaration
	:	INITIALIZATION concept_init_final_section 
	;


type_concept_final_declaration
	:	FINALIZATION concept_init_final_section 
	;


structural_program_type_expression
	:	RECORD ( record_variable_declaration_group SEMICOLON )+ END 
	|	program_type_expression 
	;


type_body_init_declaration
	:	INITIALIZATION body_init_final_section 
	;


type_body_final_declaration
	:	FINALIZATION body_init_final_section 
	;


type_facility_init_declaration
	:	INITIALIZATION facility_init_final_section 
	;


type_facility_final_declaration
	:	FINALIZATION facility_init_final_section 
	;


concept_init_final_section
	:	( affects_clause )* 
		(	requires_clause 
		|	
		) 
		(	ensures_clause 
		|	
		) 
	;


body_init_final_section
	:	( affects_clause )* ( facility_declaration )* ( variable_declaration )* ( aux_variable_declaration )* statement_sequence END SEMICOLON 
	;


facility_init_final_section
	:	( affects_clause )* 
		(	requires_clause 
		|	
		) 
		(	ensures_clause 
		|	
		) 
		( facility_declaration )* ( variable_declaration )* ( aux_variable_declaration )* statement_sequence END SEMICOLON 
	;


statement
	:	(	if_statement 
		|	selection_statement 
		|	while_loop_statement 
		|	iterate_loop_statement 
		|	swap_statement 
		|	function_assignment 
		|	procedure_operation_call 
		|	remember_statement 
		|	forget_statement 
		|	confirm_statement 
		|	assume_statement 
		|	aux_code_statement 
		) 
		
	;


if_statement
	:	IF condition THEN statement_sequence ( elsif_item )* 
		(	else_part 
		|	
		) 
		END 
	;


selection_statement
	:	CASE program_expression OF selection_alternative_sequence 
		(	default_alternative 
		|	
		) 
		END 
	;


while_loop_statement
	:	WHILE condition 
		(	changing_clause 
		|	
		) 
		maintaining_clause 
		(	decreasing_clause 
		|	
		) 
		DO statement_sequence END 
	;


iterate_loop_statement
	:	ITERATE 
		(	changing_clause 
		|	
		) 
		maintaining_clause 
		(	decreasing_clause 
		|	
		) 
		iterate_item_sequence REPEAT 
	;


program_dot_expression
	:	program_function_expression ( DOT program_function_expression )* 
	|	program_function_expression 
	;


swap_statement
	:	program_dot_expression SWAP_OP program_dot_expression 
	;


function_assignment
	:	program_dot_expression ASSIGN_OP program_expression 
	;


procedure_operation_call
	:	qualified_ident operation_argument_section 
	;


remember_statement
	:	REMEMBER 
	;


forget_statement
	:	FORGET 
	;


confirm_statement
	:	CONFIRM math_expression 
	;


assume_statement
	:	ASSUME math_expression 
	;


aux_code_statement
	:	AUXCODE in_aux_statement_sequence END 
	;


in_aux_statement
	:	(	if_statement 
		|	selection_statement 
		|	while_loop_statement 
		|	iterate_loop_statement 
		|	swap_statement 
		|	function_assignment 
		|	procedure_operation_call 
		|	remember_statement 
		|	forget_statement 
		|	confirm_statement 
		|	assume_statement 
		) 
		
	;


in_aux_statement_sequence
	:	( in_aux_statement SEMICOLON )* 
	;


condition
	:	program_expression 
	;


elsif_item
	:	ELSIF condition THEN statement_sequence 
	;


else_part
	:	ELSE statement_sequence 
	;


changing_clause
	:	CHANGING program_dot_expression ( COMMA program_dot_expression )* SEMICOLON 
	;


maintaining_clause
	:	MAINTAINING math_expression SEMICOLON 
	;


iterate_item_sequence
	:	( iterate_item SEMICOLON )+ 
	;


iterate_item
	:	statement 
	|	iterate_exit_statement 
	;


iterate_exit_statement
	:	WHEN condition DO statement_sequence EXIT 
	;


operation_argument_section
	:	LPAREN 
		(	program_expression ( COMMA program_expression )* 
		|	
		) 
		RPAREN 
	;


selection_alternative_sequence
	:	( selection_alternative )+ 
	;


default_alternative
	:	DEFAULT statement_sequence 
	;


selection_alternative
	:	WHEN choices DO statement_sequence 
	;


choices
	:	choice ( DBL_BAR choice )* 
	;


choice
	:	program_expression 
	;


adding_expression
	:	multiplying_expression ( (	PLUS 
			|	MINUS 
			|	CAT 
			|	UNION 
			|	INTERSECT 
			|	WITHOUT 
			) 
			multiplying_expression )* 
	;


array_range
	:	program_expression RANGE program_expression 
	;


record_variable_declaration_group
	:	variable_id_list COLON program_type_expression 
	;


variable_id_list
	:	ident ( COMMA ident )* 
	;


function_type_expression
	:	structural_math_type_expression ( FUNCARROW structural_math_type_expression )* 
	;


cartprod_variable_declaration_group
	:	math_variable_declaration_group 
	;


product_type_expression
	:	( primitive_type_expression ( (	IDENTIFIER 
				|	TIMES 
				) 
				primitive_type_expression )* ) 
	|	primitive_type_expression 
	;


primitive_type_expression
	:	SSET 
	|	powerset_expression 
	|	nested_type_expression 
	|	qualified_ident 
		(	type_expression_argument_list 
		|	
		) 
	;


powerset_expression
	:	POWERSET LPAREN math_type_expression RPAREN 
	;


nested_type_expression
	:	LPAREN math_type_expression RPAREN 
	;


type_expression_argument_list
	:	LPAREN math_type_expression ( COMMA math_type_expression )* RPAREN 
	;


structural_math_variable_declaration_group
	:	variable_id_list COLON structural_math_type_expression 
	;


iterated_construct
	:	ident ident COLON math_type_expression 
		(	where_clause 
		|	
		) 
		(	COMMA 
		|	OF 
		) 
		math_expression 
	;


quantified_expression
	:	implies_expression 
	|	FORALL math_variable_declaration_group 
		(	where_clause 
		|	
		) 
		COMMA quantified_expression 
	|	(	EXISTS 
		|	EXISTS_UNIQUE 
		) 
		math_variable_declaration_group 
		(	where_clause 
		|	
		) 
		(	ST 
		|	COMMA 
		) 
		quantified_expression 
	;


implies_expression
	:	(	logical_expression 
			(	IMPLIES logical_expression 
			|	IFF logical_expression 
			|	
			) 
		|	IF logical_expression THEN logical_expression 
			(	ELSE logical_expression 
			|	
			) 
		) 
	;


where_clause
	:	WHERE math_expression 
	;


logical_expression
	:	relational_expression ( (	AND 
			|	OR 
			) 
			relational_expression )* 
	;


relational_expression
	:	between_expression 
	|	infix_expression 
		(	(	EQL 
			|	NOT_EQL 
			|	LT 
			|	LT_EQL 
			|	GT 
			|	GT_EQL 
			|	IN 
			|	NOT_IN 
			|	SUBSET 
			|	NOT_SUBSET 
			|	PROP_SUBSET 
			|	NOT_PROP_SUBSET 
			|	SUBSTR 
			|	NOT_SUBSTR 
			|	PROP_SUBSTR 
			|	NOT_PROP_SUBSTR 
			) 
			infix_expression 
		|	
		) 
	;


infix_expression
	:	( math_variable_declarations AND math_expression ) 
	|	( adding_expression 
			(	(	RANGE 
				|	FREE_OPERATOR 
				) 
				adding_expression 
			|	
			) ) 
	;


between_expression
	:	infix_expression ( (	LT 
			|	LT_EQL 
			) 
			infix_expression )+ 
	;


math_variable_declarations
	:	math_variable_declaration_group ( COMMA math_variable_declaration_group )* 
	;


multiplying_expression
	:	exponential_expression ( (	MULTIPLY 
			|	DIVIDE 
			|	MOD 
			|	REM 
			|	DIV 
			) 
			exponential_expression )* 
	;


exponential_expression
	:	prefix_expression 
		(	EXP exponential_expression 
		|	
		) 
	;


prefix_expression
	:	unary_expression 
	|	FREE_OPERATOR prefix_expression 
	;


unary_expression
	:	primitive_expression 
	|	NOT unary_expression 
	|	COMPLEMENT unary_expression 
	|	MINUS unary_expression 
	;


primitive_expression
	:	alternative_expression 
	|	qualified_numeric_literal 
	|	dot_expression 
	|	lambda_expression 
	|	literal_expression 
	|	outfix_expression 
	|	set_constructor 
	|	tuple_expression 
	|	nested_expression 
	;


alternative_expression
	:	DBL_LBRACE ( alternative_expression_item )+ DBL_RBRACE 
	;


qualified_numeric_literal
	:	ident DOT NUMERIC_LITERAL 
	;


dot_expression
	:	function_expression ( DOT clean_function_expression )* 
	|	function_expression 
	;


lambda_expression
	:	LAMBDA ident COLON 
		(	certain_qualified_ident 
		|	ident 
		) 
		DOT LPAREN math_expression RPAREN 
	;


literal_expression
	:	qualified_numeric_literal 
	|	NUMERIC_LITERAL 
	|	CHARACTER_LITERAL 
	|	STRING_LITERAL 
	;


outfix_expression
	:	LT infix_expression GT 
	|	LL math_expression GG 
	|	BAR math_expression BAR 
	|	DBL_BAR math_expression DBL_BAR 
	;


set_constructor
	:	LBRACE ident COLON math_type_expression 
		(	where_clause 
		|	
		) 
		COMMA math_expression RBRACE 
	;


tuple_expression
	:	LPAREN math_expression ( COMMA math_expression )* RPAREN 
	;


nested_expression
	:	LPAREN math_expression RPAREN 
	;


function_expression
	:	HASH clean_function_expression 
	|	clean_function_expression 
	;


clean_function_expression
	:	ident 
		(	(	hat_expression 
			|	
			) 
			( function_argument_list )+ 
		|	
		) 
	;


hat_expression
	:	CARAT 
		(	qualified_ident 
		|	nested_expression 
		) 
	;


function_argument_list
	:	LPAREN math_expression ( COMMA math_expression )* RPAREN 
	;


alternative_expression_item
	:	adding_expression 
		(	IF relational_expression 
		|	OTHERWISE 
		) 
		SEMICOLON 
	;


certain_qualified_ident
	:	ident DOT ident 
	;


program_literal_expression
	:	NUMERIC_LITERAL 
	|	CHARACTER_LITERAL 
	|	STRING_LITERAL 
	;


parenthesized_expression
	:	LPAREN math_expression RPAREN 
	;


program_logical_expression
	:	program_relational_expression ( (	AND 
			|	OR 
			) 
			program_relational_expression )* 
	;


program_relational_expression
	:	program_adding_expression 
		(	(	EQL 
			|	NOT_EQL 
			|	LT 
			|	LT_EQL 
			|	GT 
			|	GT_EQL 
			) 
			program_adding_expression 
		|	
		) 
	;


program_adding_expression
	:	program_multiplying_expression ( (	PLUS 
			|	MINUS 
			) 
			program_multiplying_expression )* 
	;


program_multiplying_expression
	:	program_exponential_expression ( (	MULTIPLY 
			|	DIVIDE 
			|	MOD 
			|	REM 
			|	DIV 
			) 
			program_exponential_expression )* 
	;


program_exponential_expression
	:	program_unary_expression 
		(	EXP program_exponential_expression 
		|	
		) 
	;


program_unary_expression
	:	program_primitive_expression 
	|	NOT program_unary_expression 
	|	MINUS program_unary_expression 
	;


program_primitive_expression
	:	program_literal_expression 
	|	program_dot_expression 
	|	program_nested_expression 
	;


program_nested_expression
	:	LPAREN program_expression RPAREN 
	;


program_function_expression
	:	ident 
		(	program_function_argument_list 
		|	
		) 
	;


program_function_argument_list
	:	LPAREN 
		(	program_expression ( COMMA program_expression )* 
		|	
		) 
		RPAREN 
	;


variable_expression
	:	variable_array_expression ( DOT variable_array_expression )* 
	|	variable_array_expression 
	;


variable_array_expression
	:	ident 
		(	variable_array_argument_list 
		|	
		) 
	;


variable_array_argument_list
	:	LPAREN 
		(	program_expression 
		|	
		) 
		RPAREN 
	;


proof_module_body
	:	(	math_item_sequence 
		|	proof 
		)* 
		
	;


proof
	:	PROOF OF math_item_reference COLON 
		(	base_case_statement_head 
		|	base_case_statement_body 
		|	inductive_case_statement_head 
		|	inductive_case_statement_body 
		|	headed_proof_expression 
		|	proof_expression 
		)* 
		QED 
	;


math_item_reference
	:	(	theorem_name 
		|	lemma_name 
		|	property_name 
		|	corollary_name 
		) 
		
	;


base_case_statement_head
	:	LSQBRACK IDENTIFIER RSQBRACK base_case_statement_body 
	;


base_case_statement_body
	:	LPAREN BASECASE RPAREN proof_expression 
	;


inductive_case_statement_head
	:	LSQBRACK IDENTIFIER RSQBRACK inductive_case_statement_body 
	;


inductive_case_statement_body
	:	LPAREN INDUCTIVECASE RPAREN proof_expression 
	;


headed_proof_expression
	:	LSQBRACK IDENTIFIER RSQBRACK proof_expression 
	;


proof_expression
	:	(	goal_declaration 
		|	standard_definition_declaration 
		|	supposition_deduction_pair 
		|	justification_declaration 
		) 
	;


theorem_name
	:	THEOREM ident 
	;


lemma_name
	:	LEMMA ident 
	;


property_name
	:	PROPERTY ident 
	;


corollary_name
	:	COROLLARY math_theorem_ident 
	;


proof_expression_list
	:	(	( ) 
		|	( ) 
		|	headed_proof_expression 
		|	proof_expression 
		)* 
		
	;


goal_declaration
	:	GOAL math_expression SEMICOLON 
	;


supposition_deduction_pair
	:	supposition_declaration SEMICOLON proof_expression_list 
		(	LSQBRACK IDENTIFIER RSQBRACK 
		|	
		) 
		deduction_declaration SEMICOLON 
	;


justification_declaration
	:	math_expression justification SEMICOLON 
	;


supposition_declaration
	:	SUPPOSITION 
		(	( ( math_variable_declarations 
					(	AND math_expression 
					|	
					) ) ) 
		|	( ( math_variable_declarations 
					(	AND math_expression 
					|	
					) ) ) 
		|	( math_expression ( (	AND math_variable_declarations 
					|	
					) ) ) 
		) 
	;


deduction_declaration
	:	DEDUCTION math_expression 
	;


justification
	:	BY 
		(	double_hyp_rule_justification 
		|	single_hyp_rule_justification 
		|	hyp_desig 
		|	simple_justification 
		|	def_justification 
		) 
	;


hyp_desig
	:	(	SELF 
		|	lemma_call 
		|	theorem_call 
		|	corollary_name 
		|	supposition_call 
		|	definition_call 
		|	reference_marker_call 
		) 
		
	;


double_hyp_rule_justification
	:	hyp_desig COMMA hyp_desig 
		(	AMPERSAND rules_set_1 
		|	
		) 
	;


single_hyp_rule_justification
	:	hyp_desig AMPERSAND 
		(	rules_set_1 
		|	rules_set_2 
		|	def_justification 
		) 
	;


simple_justification
	:	rules_set_2 
	|	rules_set_3 
	;


def_justification
	:	(	DEFINITION 
			(	( UNIQUE ) 
			|	( fn_name ) 
			) 
		|	LPAREN ident RPAREN OF DEFINITION fn_name 
			(	FROM ident 
			|	
			) 
			
		) 
	;


rules_set_1
	:	(	MODUS_PONENS 
		|	AND_RULE 
		|	CONTRADICTION 
		|	EQUALITY 
		|	ALTERNATIVE_ELIMINATION 
		|	COMMON_CONCLUSION 
		) 
		
	;


rules_set_2
	:	(	REDUCTIO_AD_ABSURDUM 
		|	UNIVERSAL_GENERALIZATION 
		|	EXISTENTIAL_GENERALIZATION 
		|	OR_RULE 
		|	CONJUNCT_ELIMINATION 
		|	QUANTIFIER_DISTRIBUTION 
		|	UNIVERSAL_INSTANTIATION 
		|	EXISTENTIAL_INSTANTIATION 
		) 
		
	;


fn_name
	:	infix_symbol 
	|	prefix_symbol 
	|	ident 
	;


rules_set_3
	:	EXCLUDED_MIDDLE 
	;


lemma_call
	:	LEMMA ident 
	;


theorem_call
	:	THEOREM ident 
	;


supposition_call
	:	SUPPOSITION 
	;


definition_call
	:	(	LPAREN ident RPAREN OF 
		|	
		) 
		DEFINITION fn_name 
		(	LPAREN qualified_ident ( COMMA ident ) RPAREN 
		|	
		) 
		(	FROM ident 
		|	
		) 
	;


reference_marker_call
	:	ident 
	;