parser grammar RParser;
module
: ( proof_module
| theory_module
| conceptual_module
| realization_body_module
| enhancement_module
| facility_module
)
EOF!
;
theory_module
: THEORY^ id1=ident
(module_formal_param_section)? SEMICOLON!
(uses_list)?
(math_item_sequence)?
END! (id2=ident! )?
SEMICOLON!
;
math_item_sequence
: (math_item)+
;
math_item
: formal_type_declaration
| math_type_declaration
| definition_declaration
| math_assertion_declaration
| subtype_declaration
;
conceptual_module
: MODULE_CONCEPT^ id1=ident
(module_formal_param_section)? SEMICOLON!
(uses_list)?
(requires_clause)?
(concept_item_sequence)?
END! (id2=ident! )?
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
| defines_declaration
;
enhancement_module
: MODULE_ENHANCEMENT^ id1=ident
(module_formal_param_section)?
FOR! (CONCEPT!)? ident SEMICOLON!
(uses_list)?
(requires_clause)?
(enhancement_item_sequence)?
END! (id2=ident! )?
SEMICOLON!
;
enhancement_item_sequence
: (enhancement_item)+
;
enhancement_item
: concept_state_variable_declaration
| type_declaration
| operation_declaration
| definition_declaration
| defines_declaration
;
realization_body_module
: MODULE_REALIZATION^ id1=ident
(module_formal_param_section)? FOR!
( (ident OF)=> body_enhancement_section
| body_concept_section
) SEMICOLON!
(uses_list)?
(requires_clause)?
(body_item_sequence)?
END! (id2=ident! )?
SEMICOLON!
;
body_concept_section
: ident
(ENHANCED_BY ident)* -> ^(CONCEPT ident (ident)*)
;
body_enhancement_section
: ident
OF ident
(added_enhancement_section)* -> ^(ENHANCEMENT ident ident (added_enhancement_section)*)
;
added_enhancement_section
: ENHANCED_BY^ ident
(module_argument_section)?
REALIZED_BY! ident
(module_argument_section)?
;
body_item_sequence
: (body_item)+
;
body_item
: state_variable_declaration
| module_body_init_declaration
| module_body_final_declaration
| type_representation_declaration
| aux_operation_declaration
| operation_procedure_declaration
| procedure_declaration
| recursive_procedure_declaration
| definition_declaration
| facility_declaration
;
facility_module
: FACILITY^ id1=ident
( short_facility_section (uses_list)?
| SEMICOLON! (uses_list)?
(facility_item_sequence)?
END! (id2=ident! )?
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_item
: state_variable_declaration
| module_facility_init_declaration
| module_facility_final_declaration
| facility_type_declaration
| operation_procedure_declaration
| definition_declaration
| facility_declaration
;
module_formal_param_section
: LPAREN module_parameter
(SEMICOLON module_parameter)* RPAREN
-> ^(PARAMS module_parameter (module_parameter)*)
;
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
;
uses_list
: (uses_clause)+
;
uses_clause
: USES^ ident (COMMA! ident)* SEMICOLON!
;
formal_type_declaration
: LOCAL_MATH_TYPE^ ident SEMICOLON!
;
subtype_declaration
: MATH_SUBTYPE^ ((ident DOT) => qualified_type | ident) COLON!
((ident DOT) => qualified_type | ident) SEMICOLON!
;
qualified_type
: ident DOT^ ident
;
math_type_declaration
: MATH_TYPE^ ident
COLON! math_type_expression SEMICOLON!
;
confirm_math_type_declaration
: CONFIRM MATH_TYPE math_variable_declaration SEMICOLON
-> ^(CONFIRM_TYPE math_variable_declaration)
;
sset_type_expression
: sset_function_type_expression -> ^(TYPEX sset_function_type_expression)
;
sset_function_type_expression
: (sset_domain_expression FUNCARROW^) =>
sset_domain_expression FUNCARROW^ SSET
| SSET
;
sset_domain_expression
: (SSET (IDENTIFIER|TIMES)) =>
(SSET ((id=IDENTIFIER|id=TIMES) SSET)*)
-> ^(TIMES SSET+)
| SSET
;
math_assertion_declaration
: ( AXIOM^
| THEOREM^
| PROPERTY^
| LEMMA^
| COROLLARY^
| (COMMUTATIVITY) THEOREM!
)
(math_theorem_ident)? COLON!
math_expression SEMICOLON!
;
constraint_clause
: CONSTRAINT^ math_expression SEMICOLON!
;
correspondence_clause
: CORR^ math_expression SEMICOLON!
;
convention_clause
: CONVENTION^ math_expression SEMICOLON!
;
concept_state_variable_declaration
: VAR^ math_variable_declaration_group SEMICOLON!
;
state_variable_declaration
: VAR^ variable_declaration_group SEMICOLON!
;
state_aux_variable_declaration
: AUXVAR^ variable_declaration_group SEMICOLON!
;
facility_declaration
: FACILITY^ ident
IS! ident
(module_argument_section)?
(facility_enhancement)*
REALIZED_BY! ident
(module_argument_section)?
(facility_body_enhancement)*
SEMICOLON!
;
facility_enhancement
: ENHANCED_BY^ ident
(module_argument_section)?
;
facility_body_enhancement
: ENHANCED_BY^ ident
(module_argument_section)?
REALIZED_BY! ident
(module_argument_section)?
;
module_argument_section
: LPAREN module_argument (COMMA module_argument)* RPAREN
-> ^(PARAMS module_argument+)
;
module_argument
: (qualified_ident)=> qualified_ident
| program_expression
;
defines_declaration
: DEFINES^ definition_signature SEMICOLON!
;
definition_declaration
: implicit_definition_declaration
| inductive_definition_declaration
| standard_definition_declaration
;
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!
;
definition_signature
: ( infix_definition_construct
| outfix_definition_construct
| standard_definition_construct
)
COLON! math_type_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)?
;
indexed_expression
: LPAREN! id=ident! RPAREN! math_expression
;
singleton_definition_parameter
: LPAREN math_variable_declaration RPAREN
-> ^(PARAMS math_variable_declaration)
;
definition_formal_param_section
: LPAREN math_variable_declaration_group
(COMMA math_variable_declaration_group)* RPAREN
-> ^(PARAMS math_variable_declaration_group+)
;
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
;
operation_procedure_declaration
: OPERATION^ id1=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! (id2=ident! )?
SEMICOLON!
;
operation_recursive_procedure_declaration
: OPERATION^ id1=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! (id2=ident! )?
SEMICOLON!
;
operation_declaration
: OPERATION^ ident
(operation_formal_param_section)
(COLON! program_type_expression)? SEMICOLON!
(affects_clause)*
(requires_clause)?
(ensures_clause)?
;
aux_operation_declaration
: AUX_OPERATION^ ident
(operation_formal_param_section)
(COLON! program_type_expression)? SEMICOLON!
(affects_clause)*
(requires_clause)?
(ensures_clause)?
;
procedure_declaration
: PROCEDURE^ id1=ident
(operation_formal_param_section)
(COLON! program_type_expression)? SEMICOLON!
(affects_clause)*
(decreasing_clause)?
(facility_declaration)*
(variable_declaration)*
(aux_variable_declaration)*
statement_sequence
END! (id2=ident! )?
SEMICOLON!
;
recursive_procedure_declaration
: RECURSIVE_PROCEDURE^ id1=ident
(operation_formal_param_section)
(COLON! program_type_expression)? SEMICOLON!
(affects_clause)*
decreasing_clause
(facility_declaration)*
(variable_declaration)*
(aux_variable_declaration)*
statement_sequence
END! (id2=ident! )?
SEMICOLON!
;
operation_formal_param_section
: LPAREN
( operation_formal_param_group
(SEMICOLON operation_formal_param_group)*
)? RPAREN
-> ^(PARAMS operation_formal_param_group*)
;
operation_formal_param_group
: abstract_mode variable_declaration_group
-> ^(VAR abstract_mode variable_declaration_group)
;
variable_declaration
: VAR^ variable_declaration_group SEMICOLON!
;
aux_variable_declaration
: AUXVAR^ aux_variable_declaration_group SEMICOLON!
;
affects_clause
: abstract_mode qualified_ident (COMMA qualified_ident)* SEMICOLON
-> ^(AFFECTS abstract_mode qualified_ident (COMMA qualified_ident)*)
;
abstract_mode
: ALTERS
| CLEARS
| EVALUATES
| PRESERVES
| REPLACES
| RESTORES
| UPDATES
| REASSIGNS
;
requires_clause
: REQUIRES^ math_expression SEMICOLON!
;
ensures_clause
: ENSURES^ math_expression SEMICOLON!
;
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)?
;
type_representation_declaration
: TYPE^ ident (EQL! | REPRESENTED!)
structural_program_type_expression SEMICOLON!
(convention_clause)?
(correspondence_clause)?
(type_body_init_declaration)?
(type_body_final_declaration)?
;
facility_type_declaration
: TYPE^ ident (EQL! | REPRESENTED!)
structural_program_type_expression SEMICOLON!
(convention_clause)?
(type_facility_init_declaration)?
(type_facility_final_declaration)?
;
module_concept_init_declaration
: fac=FAC_INIT^ concept_init_final_section
;
module_concept_final_declaration
: fac=FAC_FINAL^ concept_init_final_section
;
module_body_init_declaration
: fac=FAC_INIT^ body_init_final_section
;
module_body_final_declaration
: fac=FAC_FINAL^ body_init_final_section
;
module_facility_init_declaration
: fac=FAC_INIT^ facility_init_final_section
;
module_facility_final_declaration
: fac=FAC_FINAL^ facility_init_final_section
;
type_concept_init_declaration
: INITIALIZATION^ concept_init_final_section
;
type_concept_final_declaration
: FINALIZATION^ concept_init_final_section
;
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 -> ^(STATEMENT if_statement)
| selection_statement -> ^(STATEMENT selection_statement)
| while_loop_statement -> ^(STATEMENT while_loop_statement)
| iterate_loop_statement -> ^(STATEMENT iterate_loop_statement)
| (program_dot_expression SWAP_OP)=> swap_statement -> ^(STATEMENT swap_statement)
| (program_dot_expression ASSIGN_OP)=> function_assignment -> ^(STATEMENT function_assignment)
| (qualified_ident LPAREN)=> procedure_operation_call -> ^(STATEMENT procedure_operation_call)
| remember_statement -> ^(STATEMENT remember_statement)
| forget_statement -> ^(STATEMENT forget_statement)
| confirm_statement -> ^(STATEMENT confirm_statement)
| assume_statement -> ^(STATEMENT assume_statement)
| aux_code_statement -> ^(STATEMENT aux_code_statement)
)
;
in_aux_statement
: ( if_statement -> ^(STATEMENT if_statement)
| selection_statement -> ^(STATEMENT selection_statement)
| while_loop_statement -> ^(STATEMENT while_loop_statement)
| iterate_loop_statement -> ^(STATEMENT iterate_loop_statement)
| (program_dot_expression SWAP_OP)=> swap_statement -> ^(STATEMENT swap_statement)
| (program_dot_expression ASSIGN_OP)=> function_assignment -> ^(STATEMENT function_assignment)
| (qualified_ident LPAREN)=> procedure_operation_call -> ^(STATEMENT procedure_operation_call)
| remember_statement -> ^(STATEMENT remember_statement)
| forget_statement -> ^(STATEMENT forget_statement)
| confirm_statement -> ^(STATEMENT confirm_statement)
| assume_statement -> ^(STATEMENT assume_statement)
| aux_code_statement -> ^(STATEMENT aux_code_statement)
)
;
statement_sequence
: (statement SEMICOLON)* -> ^(STATEMENT_SEQUENCE statement*)
;
in_aux_statement_sequence
: (in_aux_statement SEMICOLON)* -> ^(STATEMENT_SEQUENCE in_aux_statement*)
;
function_assignment
: program_dot_expression ASSIGN_OP^ program_expression
;
forget_statement
: FORGET
;
remember_statement
: REMEMBER
;
if_statement
: IF^ condition
THEN! statement_sequence
(elsif_item)*
(else_part)? END!
;
elsif_item
: ELSIF^ condition
THEN! statement_sequence
;
else_part
: ELSE^ statement_sequence
;
condition
: program_expression
;
aux_code_statement
: AUXCODE^
in_aux_statement_sequence END!
;
iterate_loop_statement
: ITERATE^
(changing_clause)?
maintaining_clause
(decreasing_clause)?
iterate_item_sequence REPEAT!
;
iterate_item_sequence
: (iterate_item SEMICOLON!)+
;
iterate_item
: statement
| iterate_exit_statement
;
iterate_exit_statement
: WHEN^ condition
DO! statement_sequence EXIT!
;
procedure_operation_call
: qualified_ident operation_argument_section
-> ^(FUNCTION qualified_ident operation_argument_section)
;
operation_argument_section
: LPAREN
( program_expression
(COMMA program_expression)*
)? RPAREN -> ^(PARAMS program_expression*)
;
selection_statement
: CASE^ program_expression
OF! selection_alternative_sequence
(default_alternative)? END!
;
selection_alternative_sequence
: (selection_alternative)+
;
selection_alternative
: WHEN^ choices
DO! statement_sequence
;
default_alternative
: DEFAULT^ statement_sequence
;
choice
: program_expression
;
choices
: choice
(DBL_BAR choice)* -> ^(CHOICES choice+)
;
swap_statement
: program_dot_expression SWAP_OP^ program_dot_expression
;
confirm_statement
: CONFIRM^ math_expression
;
assume_statement
: ASSUME^ math_expression
;
while_loop_statement
: WHILE^ condition
(changing_clause)?
maintaining_clause
(decreasing_clause)?
DO! statement_sequence END!
;
maintaining_clause
: MAINTAINING^ math_expression SEMICOLON!
;
decreasing_clause
: DECREASING^ adding_expression SEMICOLON!
;
changing_clause
: CHANGING^ program_dot_expression
(COMMA! program_dot_expression)* SEMICOLON!
;
program_type_expression
: ( (qualified_ident -> ^(TYPEX qualified_ident))
| (ARRAY array_range
OF program_type_expression
-> ^(ARRAY array_range program_type_expression))
)
;
structural_program_type_expression
: RECORD^
(record_variable_declaration_group SEMICOLON!)+
END!
| program_type_expression
;
record_variable_declaration_group
: variable_id_list COLON program_type_expression
-> ^(VAR variable_id_list program_type_expression)
;
array_range
: program_expression RANGE^ program_expression
;
variable_declaration_group
: variable_id_list COLON! program_type_expression
;
aux_variable_declaration_group
: variable_id_list COLON! program_type_expression
;
variable_id_list
: ident (COMMA! ident)*
;
math_type_expression
: function_type_expression? -> ^(TYPEX function_type_expression?)
;
function_type_expression
: structural_math_type_expression
(FUNCARROW^ structural_math_type_expression)*
;
structural_math_type_expression
: CARTPROD^
(cartprod_variable_declaration_group SEMICOLON!)+
END!
| product_type_expression
;
product_type_expression
: (primitive_type_expression (IDENTIFIER|TIMES)) =>
( primitive_type_expression
((id=IDENTIFIER | id=TIMES)
primitive_type_expression
)*
) -> ^(TIMES[$id] primitive_type_expression primitive_type_expression*)
| primitive_type_expression
;
primitive_type_expression
: (SSET) => SSET
| (BOOLEAN) => BOOLEAN
| (POWERSET) => powerset_expression
| nested_type_expression
| (qualified_ident -> ^(qualified_ident))
( type_expression_argument_list
-> ^(FUNCTION 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 -> ^(PARAMS math_type_expression math_type_expression*)
;
cartprod_variable_declaration_group
: math_variable_declaration_group -> ^(VAR math_variable_declaration_group)
;
structural_math_variable_declaration_group
: variable_id_list COLON! structural_math_type_expression
;
math_variable_declaration_group
: variable_id_list COLON! math_type_expression
;
math_variable_declaration
: ident COLON! math_type_expression
;
math_expression
: ( ((ident ident COLON) => iterated_construct) -> ^(EXPR iterated_construct)
| quantified_expression -> ^(EXPR quantified_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
)
;
logical_expression
: relational_expression
( ( AND^
| OR^
)
relational_expression
)*
;
relational_expression
: (infix_expression (LT|LT_EQL) infix_expression (LT|LT_EQL)) =>
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
)?
;
between_expression
: e1=infix_expression
( ( id=LT
| id=LT_EQL
)
e2=infix_expression
)+ -> ^(BETWEEN_EXPR infix_expression ($id infix_expression)+)
;
infix_expression returns [ColsAST ast = null]
:
(adding_expression
( ( RANGE^
| FREE_OPERATOR^
)
adding_expression
)?)
| BOOLEAN
;
adding_expression
: multiplying_expression
( ( PLUS^
| MINUS^
| CAT^
| UNION^
| INTERSECT^
| WITHOUT^
)
multiplying_expression
)*
;
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
| (ident DOT NUMERIC_LITERAL) => qualified_numeric_literal
| dot_expression
| lambda_expression
| literal_expression
| outfix_expression
| set_constructor
| (LPAREN math_expression COMMA) => tuple_expression
| nested_expression
;
dot_expression
: (function_expression DOT) =>
function_expression (DOT clean_function_expression)*
-> ^(DOT function_expression clean_function_expression*)
| function_expression
;
function_expression
: HASH^ clean_function_expression
| clean_function_expression
;
clean_function_expression
: (ident -> ^(ident))
( (hat_expression)?
(function_argument_list)+ -> ^(FUNCTION ident hat_expression? function_argument_list+)
)?
;
hat_expression
: CARAT^ (qualified_ident | nested_expression)
;
function_argument_list
: LPAREN math_expression (COMMA math_expression)* RPAREN -> ^(PARAMS math_expression+)
;
alternative_expression
:
DBL_LBRACE^
(alternative_expression_item)+
DBL_RBRACE!
;
alternative_expression_item
: exp=adding_expression
( IF^ relational_expression
| OTHERWISE^
)
SEMICOLON!
;
iterated_construct
: id=ident
ident
COLON math_type_expression
(where_clause)?
(COMMA | OF) math_expression
-> ^(ITERATION ident ident math_type_expression (where_clause)? math_expression)
;
lambda_expression
: LAMBDA^ ident COLON!
( (ident DOT ident DOT) => certain_qualified_ident
| ident
)
DOT! LPAREN! math_expression RPAREN!
;
literal_expression
: NUMERIC_LITERAL
| CHARACTER_LITERAL
| STRING_LITERAL
;
program_literal_expression
: NUMERIC_LITERAL
| CHARACTER_LITERAL
| STRING_LITERAL
;
qualified_numeric_literal
: ident DOT NUMERIC_LITERAL -> ^(QUALNUM ident NUMERIC_LITERAL)
;
nested_expression
: LPAREN math_expression RPAREN -> ^(NESTED math_expression)
;
outfix_expression
: (lt=LT infix_expression GT)-> ^(ANGLE[$lt] infix_expression)
| (ll=LL math_expression GG) -> ^(DBL_ANGLE[$ll] math_expression)
| BAR^ math_expression BAR!
| DBL_BAR^ math_expression DBL_BAR!
;
parenthesized_expression
: LPAREN! math_expression RPAREN!
;
set_constructor
: LBRACE^ ident
COLON! math_type_expression
(where_clause)? COMMA!
math_expression RBRACE!
;
tuple_expression
: LPAREN math_expression (COMMA math_expression)* RPAREN -> ^(TUPLE math_expression+)
;
where_clause
: WHERE^ math_expression
;
program_expression
: program_logical_expression -> ^(EXPR program_logical_expression)
;
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
| m=MINUS program_unary_expression -> ^(UNARY_MINUS[$m] program_unary_expression)
;
program_primitive_expression
: program_literal_expression
| program_dot_expression
| program_nested_expression
;
program_dot_expression
: (program_function_expression DOT) =>
program_function_expression
(DOT program_function_expression)* -> ^(DOT program_function_expression+)
| program_function_expression
;
program_function_expression
: (ident -> ^(ident))
( program_function_argument_list -> ^(FUNCTION ident program_function_argument_list)
)?
;
program_function_argument_list
: LPAREN (program_expression (COMMA program_expression)*)? RPAREN
-> ^(PARAMS program_expression*)
;
program_nested_expression
: LPAREN program_expression RPAREN -> ^(NESTED program_expression)
;
variable_expression
: (variable_array_expression DOT) =>
variable_array_expression
(DOT variable_array_expression)* -> ^(DOT variable_array_expression+)
| variable_array_expression
;
variable_array_expression
: ident
( variable_array_argument_list -> ^(FUNCTION ident variable_array_argument_list)
)?
;
variable_array_argument_list
: LPAREN (program_expression)? RPAREN -> ^(PARAMS program_expression?)
;
certain_qualified_ident
: ident DOT ident -> ^(IDENTIFIER ident ident)
;
qualified_ident
: ident (DOT ident)? -> ^(IDENTIFIER ident ident?)
;
ident
: IDENTIFIER
;
math_theorem_ident
: ident
| NUMERIC_LITERAL
;
proof_module
: PROOFS_FOR^ id1=ident SEMICOLON!
(module_formal_param_section)?
(uses_list)?
SEMICOLON!
;
proof_module_body
: (math_item_sequence -> ^(PROOFBODY math_item_sequence)
| proof -> ^(PROOFBODY proof))
;
proof
: PROOF^ OF!
math_item_reference
COLON!
( (LSQBRACK IDENTIFIER RSQBRACK LPAREN BASECASE) => base_case_statement_head
| (LPAREN BASECASE) => base_case_statement_body
| (LSQBRACK IDENTIFIER RSQBRACK LPAREN INDUCTIVECASE) => inductive_case_statement_head
| (LPAREN INDUCTIVECASE) => inductive_case_statement_body
| (LSQBRACK IDENTIFIER RSQBRACK) => headed_proof_expression
| proof_expression )*
QED!
;
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
;
math_item_reference
:
( theorem_name -> ^(MATHITEMREF theorem_name)
| lemma_name -> ^(MATHITEMREF lemma_name)
| property_name -> ^(MATHITEMREF property_name)
| corollary_name -> ^(MATHITEMREF corollary_name)
)
;
theorem_name
: THEOREM^ ident
;
lemma_name
: LEMMA^ ident
;
property_name
: PROPERTY^ ident
;
corollary_name
: COROLLARY^ math_theorem_ident
;
proof_expression_list
: ( (LSQBRACK IDENTIFIER RSQBRACK DEDUCTION) => ()
| (DEDUCTION) => ()
| (LSQBRACK IDENTIFIER RSQBRACK) => headed_proof_expression -> ^(PROOFEXPRLIST headed_proof_expression)
| proof_expression -> ^(PROOFEXPRLIST proof_expression)
)*
;
headed_proof_expression
: LSQBRACK! IDENTIFIER^ RSQBRACK! proof_expression
;
proof_expression
:
( goal_declaration
| standard_definition_declaration
| supposition_deduction_pair
| justification_declaration
)
;
goal_declaration
: GOAL^ math_expression SEMICOLON!
;
supposition_deduction_pair
: supposition_declaration SEMICOLON
proof_expression_list
(LSQBRACK IDENTIFIER RSQBRACK)?
deduction_declaration SEMICOLON
-> ^(SUPDEDUC supposition_declaration proof_expression_list IDENTIFIER? deduction_declaration)
;
supposition_declaration
: SUPPOSITION^
(
((ident COLON) => (math_variable_declarations (AND! math_expression)?))
| ((ident COMMA ident) => (math_variable_declarations (AND! math_expression)?))
)
;
math_variable_declarations
: math_variable_declaration_group (COMMA math_variable_declaration_group)*
-> ^(DECLARATIONS math_variable_declaration_group+)
;
deduction_declaration
: DEDUCTION^ math_expression
;
justification_declaration
: math_expression justification SEMICOLON -> ^(SIMPLIFICATION math_expression justification)
;
justification
: BY^
( (hyp_desig COMMA) => double_hyp_rule_justification
| (hyp_desig AMPERSAND) => single_hyp_rule_justification
| (hyp_desig) => hyp_desig
| simple_justification
| (DEFINITION) => def_justification )
;
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)
;
def_justification
:
( DEFINITION ((UNIQUE) => (UNIQUE) | (fn_name))
| LPAREN ident RPAREN OF DEFINITION fn_name (FROM ident)? -> ^(INDEXED_DEFINITION ident fn_name ident?)
)
;
simple_justification
: rules_set_2 | rules_set_3
;
rules_set_1
:
( MODUS_PONENS -> ^(RULE1 MODUS_PONENS)
| AND_RULE -> ^(RULE1 AND_RULE)
| CONTRADICTION -> ^(RULE1 CONTRADICTION)
| EQUALITY -> ^(RULE1 EQUALITY)
| ALTERNATIVE_ELIMINATION -> ^(RULE1 ALTERNATIVE_ELIMINATION)
| COMMON_CONCLUSION -> ^(RULE1 COMMON_CONCLUSION)
)
;
rules_set_2
:
( REDUCTIO_AD_ABSURDUM -> ^(RULE2 REDUCTIO_AD_ABSURDUM)
| UNIVERSAL_GENERALIZATION -> ^(RULE2 UNIVERSAL_GENERALIZATION)
| EXISTENTIAL_GENERALIZATION -> ^(RULE2 EXISTENTIAL_GENERALIZATION)
| OR_RULE -> ^(RULE2 OR_RULE)
| CONJUNCT_ELIMINATION -> ^(RULE2 CONJUNCT_ELIMINATION)
| QUANTIFIER_DISTRIBUTION -> ^(RULE2 QUANTIFIER_DISTRIBUTION)
| UNIVERSAL_INSTANTIATION -> ^(RULE2 UNIVERSAL_INSTANTIATION)
| EXISTENTIAL_INSTANTIATION -> ^(RULE2 EXISTENTIAL_INSTANTIATION)
)
;
rules_set_3
: EXCLUDED_MIDDLE -> ^(RULE3 EXCLUDED_MIDDLE)
;
hyp_desig
:
( SELF -> ^(HYPDESIG SELF)
| lemma_call -> ^(HYPDESIG lemma_call)
| theorem_call -> ^(HYPDESIG theorem_call)
| corollary_name -> ^(HYPDESIG corollary_name)
| supposition_call -> ^(HYPDESIG supposition_call)
| definition_call -> ^(HYPDESIG definition_call)
| reference_marker_call -> ^(HYPDESIG reference_marker_call)
)
;
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 -> ^(REFCALL ident)
;
fn_name
: infix_symbol | prefix_symbol | ident
;;