Package de.be4.classicalb.core.parser; /******************************************************************* * Helpers * *******************************************************************/ Helpers underscore = '_'; double_quotation = '"'; lf = 10; cr = 13; comment_start = '/*'; comment_end = '*/'; small_letter = ['a'..'z']; capital_letter = ['A' .. 'Z']; letter = small_letter | capital_letter; digit = ['0' .. '9'] ; all_chars = [0 .. 0xffff]; all_chars_without_quote = [all_chars - double_quotation]; line_break = [lf + cr]; layout_char = [[[[0 .. 32] - line_break] + [127..160]] + [[8206 .. 8207] + [8232 .. 8233]]]; white_space = line_break | layout_char+; /******************************************************************* * States * *******************************************************************/ States normal, string, comment; /******************************************************************* * Tokens * *******************************************************************/ Tokens {normal -> comment, comment} comment = comment_start ; {comment} comment_end = comment_end; // return to state 'normal' is done in Lexer {comment} comment_body = [all_chars - ['*' + '/']]*; {comment} star = '*'; {comment} slash = '/'; {normal -> string, string -> normal} double_quotation = double_quotation; {string} string_body = all_chars_without_quote* ; {normal} for_any = '!' | 0x2200; {normal} exists = '#' | 0x2203; {normal} dollar = '$'; {normal} lambda = '%' | 0x03bb; {normal} conjunction = '&' | 0x2227; {normal} single_quotation = 39; // single quote: ' {normal} left_par = '('; {normal} right_par = ')'; {normal} product = '*' | 0x00d7; {normal} power_of = '**'; {normal} plus = '+' | 0x002b; {normal} partial_function = '+->' | 0x21f8; {normal} partial_surjection = '+->>' | 0x2900; {normal} comma = ','; {normal} minus = '-' | 0x2212; {normal} total_function = '-->' | 0x2192; {normal} total_surjection = '-->>' | 0x21a0; {normal} insert_start_sequence = '->'; {normal} dot = '.'; {normal} interval = '..' | 0x2025; {normal} dot_par = '.' white_space* '(' | 0x00b7 white_space* '(' ; // dot in generalisation expression and other expressions {normal} division = '/'; {normal} not_belonging = '/:' | 0x2209; {normal} non_inclusion = '/<:' | 0x2288; {normal} strict_non_inclusion = '/<<:' | 0x2284; {normal} not_equal = '/=' | 0x2260; {normal} set_subtraction = '\'; {normal} intersection = '/\' | 0x2229; {normal} restrict_head_sequence = '/|\'; {normal} element_of = ':' | 0x2208; {normal} double_colon = '::'; {normal} assign = ':='; {normal} semicolon = ';'; {normal} less = '<'; {normal} overwrite_relation = '<+' | 0xe103; {normal} set_relation = '<->' | 0x2194; {normal} insert_end_sequence = '<-'; {normal} output_parameters = '<--'; {normal} inclusion = '<:' | 0x2286; {normal} strict_inclusion = '<<:' | 0x2282; {normal} domain_subtraction = '<<|' | 0x2a64; {normal} less_equal = '<=' | 0x2264; {normal} equivalence = '<=>' | 0x21d4; {normal} domain_restriction = '<|' | 0x25c1; {normal} equal = '='; {normal} double_equal = '=='; {normal} implies = '=>' | 0x21d2; {normal} greater = '>'; {normal} partial_injection = '>+>' | 0x2914; {normal} total_injection = '>->' | 0x21a3; {normal} partial_bijection = '>+>>'; {normal} total_bijection = '>->>' | 0x2916; {normal} direct_product = '><' | 0x2297; {normal} greater_equal = '>=' | 0x2265; {normal} abstract_constants = 'ABSTRACT_CONSTANTS'; {normal} abstract_variables = 'ABSTRACT_VARIABLES'; {normal} any = 'ANY'; {normal} assert = 'ASSERT'; {normal} assertions = 'ASSERTIONS'; {normal} be = 'BE'; {normal} begin = 'BEGIN'; {normal} bool = 'BOOL'; {normal} bfalse = 'bfalse'; {normal} case = 'CASE'; {normal} choice = 'CHOICE'; {normal} concrete_constants = 'CONCRETE_CONSTANTS'; {normal} concrete_variables = 'CONCRETE_VARIABLES'; {normal} constants = 'CONSTANTS'; {normal} constraints = 'CONSTRAINTS'; {normal} definitions = 'DEFINITIONS'; {normal} do = 'DO'; {normal} either = 'EITHER'; {normal} else = 'ELSE'; {normal} elsif = 'ELSIF'; {normal} end = 'END'; {normal} extends = 'EXTENDS'; {normal} false = 'FALSE' | 0x22a5; {normal} fin = 'FIN'; {normal} fin1 = 'FIN1'; {normal} if = 'IF'; {normal} implementation = 'IMPLEMENTATION'; {normal} imports = 'IMPORTS'; {normal} in = 'IN'; {normal} includes = 'INCLUDES'; {normal} initialisation = 'INITIALISATION' | 'INITIALIZATION'; /* amerikanische Version scheinbar auch erlaubt */ {normal} int = 'INT'; {normal} integer = 'INTEGER' | 0x2124; {normal} quantified_inter = 'INTER' | 0x22c2; {normal} invariant = 'INVARIANT'; {normal} let = 'LET'; {normal} local_operations = 'LOCAL_OPERATIONS'; {normal} machine = 'MACHINE' | 'MODEL' | 'SYSTEM'; /* SYSTEM fuer Event-B */ {normal} max_int = 'MAXINT'; {normal} min_int = 'MININT'; {normal} nat = 'NAT' | 0x2115; {normal} nat1 = 'NAT1' | 0x2115 0x0031; {normal} natural = 'NATURAL' | 0x2115; {normal} natural1 = 'NATURAL1'; {normal} of = 'OF'; {normal} operations = 'OPERATIONS' | 'EVENTS'; /* EVENTS fuer Event-B */ {normal} or = 'OR'; {normal} pi = 'PI'; {normal} pow = 'POW' | 0x2119; {normal} pow1 = 'POW1' | 0x2119 0x0031; {normal} pre = 'PRE'; {normal} promotes = 'PROMOTES'; {normal} properties = 'PROPERTIES'; {normal} refines = 'REFINES'; {normal} refinement = 'REFINEMENT'; {normal} sees = 'SEES'; {normal} select = 'SELECT'; {normal} sets = 'SETS'; {normal} quantified_set = 'SET'; {normal} sigma = 'SIGMA'; {normal} string = 'STRING'; {normal} then = 'THEN'; {normal} true = 'TRUE' | 0x22a4; {normal} quantified_union = 'UNION' | 0x22c3; {normal} uses = 'USES'; {normal} value = 'VALUES'; {normal} var = 'VAR'; {normal} variant = 'VARIANT'; {normal} variables = 'VARIABLES'; {normal} when = 'WHEN'; {normal} where = 'WHERE'; {normal} while = 'WHILE'; {normal} empty_sequence = '[' white_space* ']' | '<' white_space* '>'; {normal} left_bracket = '['; {normal} right_bracket = ']'; {normal} union = '\/' | 0x222a; {normal} restrict_tail_sequence = '\|/'; {normal} concat_sequence = '^'; {normal} arity = 'arity'; {normal} bin = 'bin'; {normal} bool_cast = 'bool'; {normal} btree = 'btree'; {normal} card = 'card'; {normal} closure = 'closure'; {normal} closure1 = 'closure1'; {normal} conc = 'conc'; {normal} const = 'const'; {normal} dom = 'dom'; {normal} father = 'father'; {normal} first = 'first'; {normal} fnc = 'fnc'; {normal} front = 'front'; {normal} id = 'id'; {normal} infix = 'infix'; {normal} generalized_inter = 'inter'; {normal} iseq = 'iseq'; {normal} iseq1 = 'iseq1'; {normal} iterate = 'iterate'; {normal} last = 'last'; {normal} left = 'left'; {normal} max = 'max'; {normal} min = 'min'; {normal} mirror = 'mirror'; {normal} mod = 'mod'; {normal} not = 'not' | 0x00ac; {normal} logical_or = 'or' | 0x2228; {normal} perm = 'perm'; {normal} postfix = 'postfix'; {normal} pred = 'pred'; {normal} prefix = 'prefix'; {normal} prj1 = 'prj1'; {normal} prj2 = 'prj2'; {normal} rank = 'rank'; {normal} ran = 'ran'; {normal} rec = 'rec'; {normal} rel = 'rel'; {normal} rev = 'rev'; {normal} right = 'right'; {normal} seq = 'seq'; {normal} seq1 = 'seq1'; {normal} sizet = 'sizet'; {normal} size = 'size'; {normal} skip = 'skip'; {normal} sons = 'sons'; {normal} son = 'son'; {normal} struct = 'struct'; {normal} subtree = 'subtree'; {normal} succ = 'succ'; {normal} tail = 'tail'; {normal} top = 'top'; {normal} tree = 'tree'; {normal} generalized_union = 'union'; {normal} empty_set = '{' white_space* '}' | 0x2205; {normal} left_brace = '{'; {normal} right_brace = '}'; {normal} vertical_bar = '|'; {normal} double_vertical_bar = '||' | 0x2225; {normal} maplet = '|->' | 0x21a6; {normal} range_restriction = '|>' | 0x25b7; {normal} range_subtraction = '|>>' | 0x2a65; {normal} tilde = '~' | 0x223c; // Extensions {normal} total_relation = '<<->' | 0xe100; {normal} surjection_relation = '<->>' | 0xe101; {normal} total_surjection_relation = '<<->>' | 0xe102; // keywords for special parsing modes {normal} kw_expression = '#EXPRESSION'; {normal} kw_predicate = '#PREDICATE'; {normal} kw_substitution = '#SUBSTITUTION'; {normal} kw_abstract_constants = '#ABSTRACT_CONSTANTS'; {normal} kw_abstract_variables = '#ABSTRACT_VARIABLES'; {normal} kw_assertions = '#ASSERTIONS'; {normal} kw_concrete_constants = '#CONCRETE_CONSTANTS'; {normal} kw_concrete_variables = '#CONCRETE_VARIABLES'; {normal} kw_constants = '#CONSTANTS'; {normal} kw_constraints = '#CONSTRAINTS'; {normal} kw_definitions = '#DEFINITIONS'; {normal} kw_extends = '#EXTENDS'; {normal} kw_imports = '#IMPORTS'; {normal} kw_includes = '#INCLUDES'; {normal} kw_initialisation = '#INITIALISATION'; {normal} kw_invariant = '#INVARIANT'; {normal} kw_local_operations = '#LOCAL_OPERATIONS'; {normal} kw_operations = '#OPERATIONS'; {normal} kw_promotes = '#PROMOTES'; {normal} kw_properties = '#PROPERTIES'; {normal} kw_sees = '#SEES'; {normal} kw_sets = '#SETS'; {normal} kw_uses = '#USES'; {normal} kw_variables = '#VARIABLES'; {normal} kw_values = '#VALUES'; {normal} kw_oppattern = '#OPPATTERN'; {normal} identifier_literal = letter (letter | digit | underscore)*; {normal} def_literal_substitution = letter (letter | digit | underscore)*; {normal} def_literal_predicate = letter (letter | digit | underscore)*; {normal} integer_literal = digit+; {normal} underscore = underscore; white_space = white_space; /******************************************************************* * Ignored Tokens * *******************************************************************/ Ignored Tokens white_space, comment, comment_body, comment_end; /******************************************************************* * Productions * *******************************************************************/ Productions parse_unit {-> parse_unit} = {machine} P.machine {-> machine.parse_unit} | {definition_file} [clause]:definitions_clause {-> New parse_unit.definition_file(clause.machine_clause)} | {predicate} kw_predicate [pred]:predicate_top {-> New parse_unit.predicate(pred.predicate)} | {expression} kw_expression [expr]:expression_top {-> New parse_unit.expression(expr.expression)} | {substitution} kw_substitution [subst]:substitution_l1 {-> New parse_unit.substitution(subst.substitution)} | {abstract_constants} kw_abstract_constants [clause]:abstract_constants_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {abstract_variables} kw_abstract_variables [clause]:variables_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {assertions} kw_assertions [clause]:assertions_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {concrete_constants} kw_concrete_constants [clause]:constants_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {concrete_variables} kw_concrete_variables [clause]:concrete_variables_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {constants} kw_constants [clause]:constants_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {constraints} kw_constraints [clause]:constraints_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {definitions} kw_definitions [clause]:definitions_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {extends} kw_extends [clause]:extends_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {imports} kw_imports [clause]:imports_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {includes} kw_includes [clause]:includes_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {initialisation} kw_initialisation [clause]:initialisation_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {invariant} kw_invariant [clause]:invariant_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {local_operations} kw_local_operations [clause]:operations_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {operations} kw_operations [clause]:operations_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {promotes} kw_promotes [clause]:promotes_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {properties} kw_properties [clause]:properties_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {sees} kw_sees [clause]:sees_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {sets} kw_sets [clause]:sets_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {uses} kw_uses [clause]:uses_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {values} kw_values [clause]:values_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {variables} kw_variables [clause]:variables_clause {-> New parse_unit.machine_clause(clause.machine_clause)} | {oppattern} kw_oppattern [pattern]:operation_pattern {-> pattern.parse_unit} ; machine {-> parse_unit} = {abstract} [type]:T.machine [header]:machine_header [machine_clauses]:machine_clause_list? end {-> New parse_unit.abstract_machine(type,header.machine_header, [machine_clauses.machine_clause])} | {refinement} T.refinement [header]:machine_header refines [ref_machine]:identifier_literal [machine_clauses]:machine_clause_list? end {-> New parse_unit.refinement_machine(header.machine_header, ref_machine, [machine_clauses.machine_clause])} | {implementation} T.implementation [header]:machine_header refines [ref_machine]:identifier_literal [machine_clauses]:machine_clause_list? end {-> New parse_unit.implementation_machine(header.machine_header, ref_machine, [machine_clauses.machine_clause])} ; machine_header {-> machine_header} = [name]:composed_identifier [parameters]:machine_params? {-> New machine_header([name.identifier_literal],[parameters.expression])}; machine_params {-> expression*} = left_par [param_list]:machine_param_list right_par {-> [param_list.expression]}; machine_param_list {-> expression*} = {single} [param]:machine_param {-> [param.expression]} | {multi} [rest]:machine_param_list comma [first]:machine_param {-> [rest.expression, first.expression]} ; machine_param {-> expression} = [parameter]:expression_in_par {-> parameter.expression} ; machine_clause_list {-> machine_clause*} = {single} [clause]:machine_clause {-> [clause.machine_clause]} | {multiple} [rest]:machine_clause_list [clause]:machine_clause {-> [rest.machine_clause, clause.machine_clause]} ; machine_clause {-> machine_clause} = {definitions} [clause]:definitions_clause {-> clause.machine_clause} | {constraints} [clause]:constraints_clause {-> clause.machine_clause} | {sees} [clause]:sees_clause {-> clause.machine_clause} | {promotes} [clause]:promotes_clause {-> clause.machine_clause} | {uses} [clause]:uses_clause {-> clause.machine_clause} | {includes} [clause]:includes_clause {-> clause.machine_clause} | {extends} [clause]:extends_clause {-> clause.machine_clause} | {imports} [clause]:imports_clause {-> clause.machine_clause} | {sets} [clause]:sets_clause {-> clause.machine_clause} | {constants} [clause]:constants_clause {-> clause.machine_clause} | {abstract_constants} [clause]:abstract_constants_clause {-> clause.machine_clause} | {properties} [clause]:properties_clause {-> clause.machine_clause} | {concrete_variables} [clause]:concrete_variables_clause {-> clause.machine_clause} | {variables} [clause]:variables_clause {-> clause.machine_clause} | {assertions} [clause]:assertions_clause {-> clause.machine_clause} | {initialisation} [clause]:initialisation_clause {-> clause.machine_clause} | {local_operations} [clause]:local_operations_clause {-> clause.machine_clause} | {operations} [clause]:operations_clause {-> clause.machine_clause} | {values} [clause]:values_clause {-> clause.machine_clause} | {invariant} [clause]:invariant_clause {-> clause.machine_clause} ; definitions_clause {-> machine_clause} = definitions [definition_list]:definition_list semicolon? {-> New machine_clause.definitions([definition_list.definition])} ; definition_list {-> definition*} = {single} [def]:definition {-> [def.definition]} | {multi} [rest]:definition_list semicolon [def]:definition {-> [rest.definition, def.definition]} ; definition {-> definition} = {predicate} [name]:def_literal_predicate [parameters]:def_parameters? double_equal [rhs]:predicate_top {-> New definition.predicate(name, [parameters.expression], rhs.predicate)} | {substitution} [name]:def_literal_substitution [parameters]:def_parameters? double_equal [rhs]:substitution_l2 {-> New definition.substitution(name, [parameters.expression], rhs.substitution)} | {expression} [name]:identifier_literal [parameters]:def_parameters? double_equal [rhs]:expression_top {-> New definition.expression(name, [parameters.expression], rhs.expression)} | {file} [q1]:double_quotation [filename]:string_body [q2]:double_quotation {-> New definition.file(filename)}; def_parameters {-> expression*} = left_par [parameters]:identifier_list right_par {-> [parameters.expression]} ; sees_clause {-> machine_clause} = sees [machine_names]:identifier_list {-> New machine_clause.sees([machine_names.expression])} ; promotes_clause {-> machine_clause} = promotes [machine_names]:identifier_list {-> New machine_clause.promotes([machine_names.expression])} ; uses_clause {-> machine_clause} = uses [machine_names]:identifier_list {-> New machine_clause.uses([machine_names.expression])} ; includes_clause {-> machine_clause} = includes [machine_references]:machine_ref_list {-> New machine_clause.includes([machine_references.machine_reference])} ; extends_clause {-> machine_clause} = extends [machine_references]:machine_ref_list {-> New machine_clause.extends([machine_references.machine_reference])} ; imports_clause {-> machine_clause} = imports [machine_references]:machine_ref_list {-> New machine_clause.imports([machine_references.machine_reference])} ; machine_ref_list {-> machine_reference*} = {single} [ref]:machine_reference {-> [ref.machine_reference]} | {multi} [rest]:machine_ref_list comma [first]:machine_reference {-> [rest.machine_reference, first.machine_reference]} ; machine_reference {-> machine_reference} = [machine_name]:composed_identifier [parameters]:machine_params? {-> New machine_reference([machine_name.identifier_literal], [parameters.expression])} ; variables_clause {-> machine_clause} = {abstract} abstract_variables [identifiers]:identifier_list {-> New machine_clause.variables([identifiers.expression])} | variables [identifiers]:identifier_list {-> New machine_clause.variables([identifiers.expression])} ; constants_clause {-> machine_clause} = {concrete} concrete_constants [identifiers]:identifier_list {-> New machine_clause.constants([identifiers.expression])} | constants [identifiers]:identifier_list {-> New machine_clause.constants([identifiers.expression])} ; concrete_variables_clause {-> machine_clause} = concrete_variables [identifiers]:identifier_list {-> New machine_clause.concrete_variables([identifiers.expression])} ; abstract_constants_clause {-> machine_clause} = abstract_constants [identifiers]:identifier_list {-> New machine_clause.abstract_constants([identifiers.expression])} ; sets_clause {-> machine_clause} = sets [set_definitions]:set_def_list {-> New machine_clause.sets([set_definitions.set])}; set_def_list {-> set*} = {single} [set]:set {-> [set.set]} | {multi} [rest]:set_def_list semicolon [last]:set {-> [rest.set, last.set]} ; set {-> set} = {deferred} [identifier]:composed_identifier {-> New set.deferred([identifier.identifier_literal])} | {enumerated} [identifier]:composed_identifier equal left_brace [elements]:expression_list right_brace {-> New set.enumerated([identifier.identifier_literal], [elements.expression])} ; properties_clause {-> machine_clause} = properties [predicates]:predicate_top {-> New machine_clause.properties(predicates.predicate)}; initialisation_clause {-> machine_clause} = initialisation [substitutions]:substitution_l1 {-> New machine_clause.initialisation(substitutions.substitution)}; invariant_clause {-> machine_clause} = invariant [predicates]:predicate_top {-> New machine_clause.invariant(predicates.predicate)}; constraints_clause {-> machine_clause} = constraints [predicates]:predicate_top {-> New machine_clause.constraints(predicates.predicate)}; assertions_clause {-> machine_clause} = assertions [predicates]:assertions_pred_list {-> New machine_clause.assertions([predicates.predicate])}; assertions_pred_list {-> predicate*} = {single} [predicate]:predicate_top {-> [predicate.predicate]} | {multi} [rest]:assertions_pred_list semicolon [predicate]:predicate_top {-> [rest.predicate, predicate.predicate]} ; values_clause {-> machine_clause} = value [entries]:values_entries_list {-> New machine_clause.values([entries.values_entry])} ; values_entries_list {-> values_entry*} = {single} [entry]:values_entry {-> [entry.values_entry]} | {multi} [rest]:values_entries_list semicolon [entry]:values_entry {-> [rest.values_entry, entry.values_entry]} ; values_entry = [identifier]:composed_identifier equal [value]:expression_top {-> New values_entry([identifier.identifier_literal], value.expression)} ; local_operations_clause {-> machine_clause} = local_operations [operation_list]:operation_list {-> New machine_clause.local_operations([operation_list.operation])} ; operations_clause {-> machine_clause} = operations [operation_list]:operation_list {-> New machine_clause.operations([operation_list.operation])} ; operation_list {-> operation*} = {single} [operation]:operation {-> [operation.operation]} | {multi} [rest]:operation_list semicolon [operation]:operation {-> [rest.operation, operation.operation]} ; operation {-> operation} = [return_values]:operation_return_values? [op_name]:composed_identifier [parameters]:op_params? equal [operation_body]:substitution_l2 {-> New operation([return_values.expression], [op_name.identifier_literal], [parameters.expression], operation_body.substitution)} ; operation_return_values {-> expression*} = [return_values]:identifier_list output_parameters {-> [return_values.expression]} ; /* Predicates */ predicate_top {-> predicate} = [pred]:predicate_p30 {-> pred.predicate}; predicate_p30 {-> predicate} = {implication} [left]:predicate_p30 implies [right]:predicate_x30 {-> New predicate.implication(left.predicate, right.predicate)} | // rechtsassoziativ? {next_level} [pred]:predicate_x30 {-> pred.predicate}; predicate_x30 {-> predicate} = [pred]:predicate_p40 {-> pred.predicate}; predicate_p40 {-> predicate} = {disjunct} [left]:predicate_p40 logical_or [right]:predicate_x40 {-> New predicate.disjunct(left.predicate, right.predicate)} | {conjunct} [left]:predicate_p40 conjunction [right]:predicate_x40 {-> New predicate.conjunct(left.predicate, right.predicate)} | {next_level} [pred]:predicate_x40 {-> pred.predicate}; predicate_x40 {-> predicate} = [pred]:predicate_p60 {-> pred.predicate}; predicate_p60 {-> predicate} = {equivalence} [left]:predicate_p60 equivalence [right]:predicate_x60 {-> New predicate.equivalence(left.predicate, right.predicate)} | {next_level} [pred]:predicate_x60 {-> pred.predicate}; predicate_x60 {-> predicate} = [pred]:predicate_atomic {-> pred.predicate}; /* The predicates of the following levels have completely moved down to the atomic level: predicate_p110 {-> predicate} = {next_level} [pred]:predicate_x110 {-> pred.predicate}; predicate_x110 {-> predicate} = [pred]:predicate_p160 {-> pred.predicate}; predicate_p160 {-> predicate} = {next_level} [pred]:predicate_x160 {-> pred.predicate}; predicate_x160 {-> predicate} = [pred]:predicate_atomic {-> pred.predicate}; */ predicate_atomic {-> predicate} = /* The following predicates have a priority in the AtelierB manual. But we (in contrast to AtelierB) distinguish between predicates and expression and can put the predicates of the form EXPR*EXPR -> PRED here. Thus sewer parenthesis can be used */ /* Original priority: 60 */ {equal} [left]:expression_top equal [right]:expression_top {-> New predicate.equal(left.expression, right.expression)} | {belong} [left]:expression_top element_of [right]:expression_top {-> New predicate.belong(left.expression, right.expression)} | /* Original priority: 110 */ {include} [left]:expression_top inclusion[right]:expression_top {-> New predicate.include(left.expression, right.expression)} | {include_strictly} [left]:expression_top strict_inclusion [right]:expression_top {-> New predicate.include_strictly(left.expression, right.expression)} | {not_include} [left]:expression_top non_inclusion [right]:expression_top {-> New predicate.not_include(left.expression, right.expression)} | {not_include_strictly} [left]:expression_top strict_non_inclusion [right]:expression_top {-> New predicate.not_include_strictly(left.expression, right.expression)} | /* Original priority: 160 */ {unequal} [left]:expression_top not_equal [right]:expression_top {-> New predicate.unequal(left.expression, right.expression)} | {not_belong} [left]:expression_top not_belonging [right]:expression_top {-> New predicate.not_belong(left.expression, right.expression)} | {less_equal} [left]:expression_top less_equal [right]:expression_top {-> New predicate.less_equal(left.expression, right.expression)} | {less} [left]:expression_top less [right]:expression_top {-> New predicate.less(left.expression, right.expression)} | {greater_equal} [left]:expression_top greater_equal [right]:expression_top {-> New predicate.greater_equal(left.expression, right.expression)} | {greater} [left]:expression_top greater [right]:expression_top {-> New predicate.greater(left.expression, right.expression)} | /* Now we continue with the real atomic predicates: */ {false} bfalse {-> New predicate.false()} | {bracketed} left_par [predicate]:predicate_top right_par {-> predicate.predicate} | {negation} not left_par [predicate]:predicate_top right_par {-> New predicate.negation(predicate.predicate)} | {universal_quantification} for_any [identifiers]:expression_list dot_par [implication]:predicate_top right_par {-> New predicate.universal_quantification([identifiers.expression], implication.predicate)} | // check in typechecker: predicate must be an implication predicate {existential_quantification} exists [identifiers]:expression_list dot_par [predicate]:predicate_top right_par {-> New predicate.existential_quantification([identifiers.expression], predicate.predicate)} | {definition} [def_literal]:def_literal_predicate [parameters]:def_call_params? {-> New predicate.definition(def_literal, [parameters.expression])} ; /* Expressions */ /* expression_in_par contains the priority level 20, it is not considered as expression_top because ; and || should only be used inside parenthesis */ expression_in_par {-> expression} = {composition} [left]:expression_in_par semicolon [right]:expression_top {-> New expression.composition(left.expression, right.expression)} | {parallel_product} [left]:expression_in_par double_vertical_bar [right]:expression_top {-> New expression.parallel_product(left.expression, right.expression)} | {next_level} [expr]:expression_top {-> expr.expression}; expression_top {-> expression} = [expr]:expression_p125 {-> expr.expression}; /*expression_p20 {-> expression} = {parallel_product} left_par [left]:expression_p20 double_vertical_bar [right]:expression_x20 right_par {-> New expression.parallel_product(left.expression, right.expression)} | // zu sehr eingeschränkt?!? {next_level} [expr]:expression_x20 {-> expr.expression} ; expression_x20 {-> expression} = [expr]:expression_p125 {-> expr.expression}; */ expression_p125 {-> expression} = {relations} [left]:expression_p125 set_relation [right]:expression_x125 {-> New expression.relations(left.expression, right.expression)} | {partial_function} [left]:expression_p125 partial_function [right]:expression_x125 {-> New expression.partial_function(left.expression, right.expression)} | {total_function} [left]:expression_p125 total_function [right]:expression_x125 {-> New expression.total_function(left.expression, right.expression)} | {partial_injection} [left]:expression_p125 partial_injection [right]:expression_x125 {-> New expression.partial_injection(left.expression, right.expression)} | {total_injection} [left]:expression_p125 total_injection [right]:expression_x125 {-> New expression.total_injection(left.expression, right.expression)} | {partial_surjection} [left]:expression_p125 partial_surjection [right]:expression_x125 {-> New expression.partial_surjection(left.expression, right.expression)} | {total_surjection} [left]:expression_p125 total_surjection [right]:expression_x125 {-> New expression.total_surjection(left.expression, right.expression)} | {partial_bijection} [left]:expression_p125 partial_bijection [right]:expression_x125 {-> New expression.partial_bijection(left.expression, right.expression)} | {total_bijection} [left]:expression_p125 total_bijection [right]:expression_x125 {-> New expression.total_bijection(left.expression, right.expression)} | {total_relation} [left]:expression_p125 total_relation [right]:expression_x125 {-> New expression.total_relation(left.expression, right.expression)} | {surjection_relation} [left]:expression_p125 surjection_relation [right]:expression_x125 {-> New expression.surjection_relation(left.expression, right.expression)} | {total_surjection_relation} [left]:expression_p125 total_surjection_relation [right]:expression_x125 {-> New expression.total_surjection_relation(left.expression, right.expression)} | {next_level} [expr]:expression_x125 {-> expr.expression} ; expression_x125 {-> expression} = [expr]:expression_p160 {-> expr.expression}; expression_p160 {-> expression} = {overwrite} [left]:expression_p160 overwrite_relation [right]:expression_x160 {-> New expression.overwrite(left.expression, right.expression)} | {direct_product} [left]:expression_p160 direct_product [right]:expression_x160 {-> New expression.direct_product(left.expression, right.expression)} | {concat} [left]:expression_p160 concat_sequence [right]:expression_x160 {-> New expression.concat(left.expression, right.expression)} | {domain_restriction} [left]:expression_p160 domain_restriction [right]:expression_x160 {-> New expression.domain_restriction(left.expression, right.expression)} | {domain_subtraction} [left]:expression_p160 domain_subtraction [right]:expression_x160 {-> New expression.domain_subtraction(left.expression, right.expression)} | {range_restriction} [left]:expression_p160 range_restriction [right]:expression_x160 {-> New expression.range_restriction(left.expression, right.expression)} | {range_subtraction} [left]:expression_p160 range_subtraction [right]:expression_x160 {-> New expression.range_subtraction(left.expression, right.expression)} | {insert_front} [left]:expression_p160 insert_start_sequence [right]:expression_x160 {-> New expression.insert_front(left.expression, right.expression)} | {insert_tail} [left]:expression_p160 insert_end_sequence [right]:expression_x160 {-> New expression.insert_tail(left.expression, right.expression)} | {union} [left]:expression_p160 union [right]:expression_x160 {-> New expression.union(left.expression, right.expression)} | {intersection} [left]:expression_p160 intersection [right]:expression_x160 {-> New expression.intersection(left.expression, right.expression)} | {restrict_front} [left]:expression_p160 restrict_head_sequence [right]:expression_x160 {-> New expression.restrict_front(left.expression, right.expression)} | {restrict_tail} [left]:expression_p160 restrict_tail_sequence [right]:expression_x160 {-> New expression.restrict_tail(left.expression, right.expression)} | {couple1} [left]:expression_p160 maplet [right]:expression_x160 {-> New expression.couple([left.expression, right.expression])} | {next_level} [expr]:expression_x160 {-> expr.expression} ; expression_x160 {-> expression} = [expr]:expression_p170 {-> expr.expression}; expression_p170 {-> expression} = {interval} [left_border]:expression_p170 interval [right_border]:expression_x170 {-> New expression.interval(left_border.expression, right_border.expression)} | {next_level} [expr]:expression_x170 {-> expr.expression} ; expression_x170 {-> expression} = [expr]:expression_p180 {-> expr.expression}; expression_p180 {-> expression} = {minus_or_set_subtract} [left]:expression_p180 minus [right]:expression_x180 {-> New expression.minus_or_set_subtract(left.expression, right.expression)} | {add} [left]:expression_p180 plus [right]:expression_x180 {-> New expression.add(left.expression, right.expression)} | {set_subtraction} [left]:expression_p180 set_subtraction [right]:expression_x180 {-> New expression.set_subtraction(left.expression, right.expression)} | {next_level} [expr]:expression_x180 {-> expr.expression} ; expression_x180 {-> expression} = [expr]:expression_p190 {-> expr.expression}; expression_p190 {-> expression} = {mul} [left]:expression_p190 product [right]:expression_x190 {-> New expression.mult_or_cart(left.expression, right.expression)} | {div} [left]:expression_p190 division [right]:expression_x190 {-> New expression.div(left.expression, right.expression)} | {modulo} [left]:expression_p190 mod [right]:expression_x190 {-> New expression.modulo(left.expression, right.expression)} | {next_level} [expr]:expression_x190 {-> expr.expression} ; expression_x190 {-> expression} = [expr]:expression_p200 {-> expr.expression}; /* Attention: power_of is right-assoziative! */ expression_p200 {-> expression} = {power_of} [left]:expression_x200 power_of [right]:expression_p200 {-> New expression.power_of(left.expression, right.expression)} | // right associative! {next_level} [expr]:expression_x200 {-> expr.expression} ; expression_x200 {-> expression} = [expr]:expression_p210 {-> expr.expression}; expression_p210 {-> expression} = {unary} minus [expression]:expression_x210 {-> New expression.unary(expression.expression)} | {next_level} [expr]:expression_x210 {-> expr.expression} ; expression_x210 {-> expression} = [expr]:expression_p230 {-> expr.expression}; expression_p230 {-> expression} = {reverse} [expression]:expression_x230 tilde {-> New expression.reverse(expression.expression)} | {next_level} [expr]:expression_x230 {-> expr.expression} ; expression_x230 {-> expression} = [expr]:expression_p231 {-> expr.expression}; expression_p231 {-> expression} = {image} [left]:expression_p230 left_bracket [right]:expression_in_par right_bracket {-> New expression.image(left.expression, right.expression)} | {next_level} [expr]:expression_x231 {-> expr.expression} ; expression_x231 {-> expression} = [expr]:expression_keyword {-> expr.expression}; expression_keyword {-> expression} = {convert_bool} bool_cast left_par [predicate]:predicate_top right_par {-> New expression.convert_bool(predicate.predicate)} | {max} max left_par [expression]:expression_in_par right_par {-> New expression.max(expression.expression)} | {min} min left_par [expression]:expression_in_par right_par {-> New expression.min(expression.expression)} | {card} card left_par [expression]:expression_in_par right_par {-> New expression.card(expression.expression)} | {general_sum} sigma [identifiers]:expression_list dot_par [predicates]:predicate_top vertical_bar [expression]:expression_in_par right_par {-> New expression.general_sum([identifiers.expression], predicates.predicate, expression.expression)} | {general_product} pi [identifiers]:expression_list dot_par [predicates]:predicate_top vertical_bar [expression]:expression_in_par right_par {-> New expression.general_product([identifiers.expression], predicates.predicate, expression.expression)} | {pow_subset} pow left_par [expression]:expression_in_par right_par {-> New expression.pow_subset(expression.expression)} | {pow1_subset} pow1 left_par [expression]:expression_in_par right_par {-> New expression.pow1_subset(expression.expression)} | {fin_subset} fin left_par [expression]:expression_in_par right_par {-> New expression.fin_subset(expression.expression)} | {fin1_subset} fin1 left_par [expression]:expression_in_par right_par {-> New expression.fin1_subset(expression.expression)} | {general_union} generalized_union left_par [expression]:expression_in_par right_par {-> New expression.general_union(expression.expression)} | {general_intersection} generalized_inter left_par [expression]:expression_in_par right_par {-> New expression.general_intersection(expression.expression)} | {identity} id left_par [expression]:expression_in_par right_par {-> New expression.identity(expression.expression)} | {reflexive_closure} closure left_par [expression]:expression_in_par right_par {-> New expression.reflexive_closure(expression.expression)} | {closure} closure1 left_par [expression]:expression_in_par right_par {-> New expression.closure(expression.expression)} | {domain} dom left_par [expression]:expression_in_par right_par {-> New expression.domain(expression.expression)} | {range} ran left_par [expression]:expression_in_par right_par {-> New expression.range(expression.expression)} | {lambda} lambda [identifiers]:expression_list dot_par [predicate]:predicate_top vertical_bar [expression]:expression_in_par right_par {-> New expression.lambda([identifiers.expression], predicate.predicate, expression.expression)} | {trans_function} fnc left_par [expression]:expression_in_par right_par {-> New expression.trans_function(expression.expression)} | {trans_relation} rel left_par [expression]:expression_in_par right_par {-> New expression.trans_relation(expression.expression)} | {seq} seq left_par [expression]:expression_in_par right_par {-> New expression.seq(expression.expression)} | {seq1} seq1 left_par [expression]:expression_in_par right_par {-> New expression.seq1(expression.expression)} | {iseq} iseq left_par [expression]:expression_in_par right_par {-> New expression.iseq(expression.expression)} | {iseq1} iseq1 left_par [expression]:expression_in_par right_par {-> New expression.iseq1(expression.expression)} | {perm} perm left_par [expression]:expression_in_par right_par {-> New expression.perm(expression.expression)} | {empty_sequence} empty_sequence {-> New expression.empty_sequence()} | {size} size left_par [expression]:expression_in_par right_par {-> New expression.size(expression.expression)} | {first} first left_par [expression]:expression_in_par right_par {-> New expression.first(expression.expression)} | {last} last left_par [expression]:expression_in_par right_par {-> New expression.last(expression.expression)} | {front} front left_par [expression]:expression_in_par right_par {-> New expression.front(expression.expression)} | {tail} tail left_par [expression]:expression_in_par right_par {-> New expression.tail(expression.expression)} | {rev} rev left_par [expression]:expression_in_par right_par {-> New expression.rev(expression.expression)} | {first_projection} prj1 left_par [exp1]:expression_in_par comma [exp2]:expression_in_par right_par {-> New expression.first_projection(exp1.expression, exp2.expression)} | {second_projection} prj2 left_par [exp1]:expression_in_par comma [exp2]:expression_in_par right_par {-> New expression.second_projection(exp1.expression, exp2.expression)} | {iteration} iterate left_par [left]:expression_in_par comma [right]:expression_in_par right_par {-> New expression.iteration(left.expression, right.expression)} | {comprehension_set} left_brace [identifiers]:expression_list vertical_bar [predicates]:predicate_top right_brace {-> New expression.comprehension_set([identifiers.expression], predicates.predicate)} | {quantified_union} quantified_union [identifiers]:expression_list dot_par [predicates]:predicate_top vertical_bar [expression]:expression_in_par right_par {-> New expression.quantified_union([identifiers.expression], predicates.predicate, expression.expression)} | {quantified_intersection} quantified_inter [identifiers]:expression_list dot_par [predicates]:predicate_top vertical_bar [expression]:expression_in_par right_par {-> New expression.quantified_intersection([identifiers.expression], predicates.predicate, expression.expression)} | {quantified_set} quantified_set [identifiers]:expression_list dot_par [predicates]:predicate_top right_par {-> New expression.prover_comprehension_set([identifiers.expression], predicates.predicate)} | {set_extension} left_brace [expressions]:expression_list right_brace {-> New expression.set_extension([expressions.expression])} | {sequence_extension} left_bracket [expressions]:expression_list right_bracket {-> New expression.sequence_extension([expressions.expression])} | {couple2} left_par [first]:expression_in_par comma [rest]:expression_list right_par {-> New expression.couple([first.expression, rest.expression])} | // Klammern notwendig {general_concat} conc left_par [expression]:expression_in_par right_par {-> New expression.general_concat(expression.expression)} | {tree} tree left_par [expression]:expression_in_par right_par {-> New expression.tree(expression.expression)} | {btree} btree left_par [expression]:expression_in_par right_par {-> New expression.btree(expression.expression)} | {const} const left_par [expr1]:expression_in_par comma [expr2]:expression_in_par right_par {-> New expression.const(expr1.expression, expr2.expression)} | {top} top left_par [expression]:expression_in_par right_par {-> New expression.top(expression.expression)} | {sons} sons left_par [expression]:expression_in_par right_par {-> New expression.sons(expression.expression)} | {prefix} prefix left_par [expression]:expression_in_par right_par {-> New expression.prefix(expression.expression)} | {postfix} postfix left_par [expression]:expression_in_par right_par {-> New expression.postfix(expression.expression)} | {sizet} sizet left_par [expression]:expression_in_par right_par {-> New expression.sizet(expression.expression)} | {mirror} mirror left_par [expression]:expression_in_par right_par {-> New expression.mirror(expression.expression)} | {rank} rank left_par [expression1]:expression_in_par comma [expression2]:expression_in_par right_par {-> New expression.rank(expression1.expression, expression2.expression)} | {father} father left_par [expression1]:expression_in_par comma [expression2]:expression_in_par right_par {-> New expression.father(expression1.expression, expression2.expression)} | {son} son left_par [expression1]:expression_in_par [comma1]:comma [expression2]:expression_in_par [comma2]:comma [expression3]:expression_in_par right_par {-> New expression.son(expression1.expression, expression2.expression, expression3.expression)} | {subtree} subtree left_par [expression1]:expression_in_par comma [expression2]:expression_in_par right_par {-> New expression.subtree(expression1.expression, expression2.expression)} | {arity} arity left_par [expression1]:expression_in_par comma [expression2]:expression_in_par right_par {-> New expression.arity(expression1.expression, expression2.expression)} | {bin1} bin left_par [expression]:expression_in_par right_par {-> New expression.bin(expression.expression, Null, Null)} | {bin2} bin left_par [expression1]:expression_in_par [comma1]:comma [expression2]:expression_in_par [comma2]:comma [expression3]:expression_in_par right_par {-> New expression.bin(expression1.expression, expression2.expression, expression3.expression)} | {left} left left_par [expression]:expression_in_par right_par {-> New expression.left(expression.expression)} | {right} right left_par [expression]:expression_in_par right_par {-> New expression.right(expression.expression)} | {infix} infix left_par [expression]:expression_in_par right_par {-> New expression.infix(expression.expression)} | {struct} struct left_par [entries]:rec_entry_list right_par {-> New expression.struct([entries.rec_entry])} | {rec} rec left_par [entries]:rec_entry_list right_par {-> New expression.rec([entries.rec_entry])} | {record_field} [record]:expression_p231 single_quotation [identifier]:expression_atomic {-> New expression.record_field(record.expression, identifier.expression)} | {next_level} [expr]:expression_func {-> expr.expression} ; rec_entry {-> rec_entry} = [identifier]:expression_top element_of [value]:expression_in_par {-> New rec_entry(identifier.expression, value.expression)} ; rec_entry_list {-> rec_entry*} = {single} [entry]:rec_entry {-> [entry.rec_entry]} | {multi} [rest]:rec_entry_list comma [last]:rec_entry {-> [rest.rec_entry, last.rec_entry]}; expression_func {-> expression} = {function} [function]:expression_p230 left_par [parameters]:expression_list right_par {-> New expression.function(function.expression, [parameters.expression])} | {next_level} expression_atomic {-> expression_atomic.expression} ; expression_atomic {-> expression} = {paren} left_par [expression]:expression_in_par right_par {-> expression.expression} | {identifier} [identifier]:composed_identifier {-> New expression.identifier([identifier.identifier_literal])} | {primed_identifier} [identifier]:composed_identifier dollar [grade]:integer_literal {-> New expression.primed_identifier([identifier.identifier_literal], grade)} | {string} [dq1]:double_quotation [content]:string_body? [dq2]:double_quotation {-> New expression.string(content)} | {true} true {-> New expression.true()} | {false} false {-> New expression.false()} | {successor} succ {-> New expression.successor()} | {predecessor} pred {-> New expression.predecessor()} | {integer} [literal]:integer_literal {-> New expression.integer(literal)} | {max_int} max_int {-> New expression.max_int()} | {min_int} min_int {-> New expression.min_int()} | {empty_set} empty_set {-> New expression.empty_set()} | {integer_set} integer {-> New expression.integer_set()} | {natural_set} natural {-> New expression.natural_set()} | {natural1_set} natural1 {-> New expression.natural1_set()} | {nat_set} nat {-> New expression.nat_set()} | {nat1_set} nat1 {-> New expression.nat1_set()} | {int_set} int {-> New expression.int_set()} | {bool_set} bool {-> New expression.bool_set()} | {string_set} string {-> New expression.string_set()} ; expression_list {-> expression*} = {single} [expression]:expression_top {-> [expression.expression]} | {multiple} [rest]:expression_list comma [last]:expression_top {-> [rest.expression, last.expression]} ; /*expression_list_in_par {-> expression*} = {single} [expression]:expression_in_par {-> [expression.expression]} | {multiple} [rest]:expression_list_in_par comma [last]:expression_in_par {-> [rest.expression, last.expression]} ; */ /* Substitutions */ substitution_l1 {-> substitution} = {sequence} [first]:substitution_l2 semicolon [second]:substitution_l2 [rest]:sequence_subst_tail? {-> New substitution.sequence([first.substitution, second.substitution, rest.substitution])} | {next_level} substitution_l2 {-> substitution_l2.substitution} ; substitution_l2 {-> substitution} = {parallel} [first]:substitution_l3 double_vertical_bar [second]:substitution_l3 [rest]:parallel_subst_tail? {-> New substitution.parallel([first.substitution, second.substitution, rest.substitution])} | {next_level} substitution_l3 {-> substitution_l3.substitution} ; substitution_l3 {-> substitution} = {block} begin [substitution]:substitution_l1 end {-> New substitution.block(substitution.substitution)} | {skip} skip {-> New substitution.skip()} | {assign} [lhs_expression]:expression_list assign [rhs_expressions]:expression_list {-> New substitution.assign([lhs_expression.expression], [rhs_expressions.expression])} | {precondition} pre [predicate]:predicate_top then [substitution]:substitution_l1 end {-> New substitution.precondition(predicate.predicate, substitution.substitution)} | {assertion} assert [predicate]:predicate_top then [substitution]:substitution_l1 end {-> New substitution.assertion(predicate.predicate, substitution.substitution)} | {choice} choice [first]:substitution_l1 [rest]:choice_or* end {-> New substitution.choice([first.substitution, rest.substitution])} | {if} if [condition]:predicate_top then [then_subst]:substitution_l1 [elsifs]:if_elsif* [else]:if_else? end {-> New substitution.if(condition.predicate, then_subst.substitution, [elsifs.substitution], else.substitution)} | {select} select [condition]:predicate_top then [then_subst]:substitution_l1 [whens]:select_when* [else]:select_else? end {-> New substitution.select(condition.predicate, then_subst.substitution, [whens.substitution], else.substitution)} | {case} case [case_expr]:expression_in_par of either [either_expr]:expression_list then [either_subst]:substitution_l1 [or_substitutions]:case_or* [else]:case_else? [end1]:end [end2]:end {-> New substitution.case(case_expr.expression, [either_expr.expression], either_subst.substitution, [or_substitutions.substitution], else.substitution)} | {any} any [identifiers]:expression_list where [where_pred]:predicate_top then [then_subst]:substitution_l1 end {-> New substitution.any([identifiers.expression], where_pred.predicate, then_subst.substitution)} | {becomes_element_of} [identifiers]:expression_list double_colon [set]:expression_top {-> New substitution.becomes_element_of([identifiers.expression], set.expression)} | {becomes_such} [identifiers]:expression_list element_of left_par [predicate]:predicate_top right_par {-> New substitution.becomes_such([identifiers.expression], predicate.predicate)} | {var} var [identifiers]:expression_list in [substitution]:substitution_l1 end {-> New substitution.var([identifiers.expression], substitution.substitution)} | {func_op} [expr]:expression_func {-> New substitution.func_op(expr.expression)} | // check in semantic check if expression is a function {op_with_return} [return_values]:expression_list output_parameters [op_name]:composed_identifier [parameters]:op_params? {-> New substitution.op_with_return([return_values.expression], [op_name.identifier_literal], [parameters.expression])} | {while} while [condition]:predicate_top do [do_subst]:substitution_l1 invariant [invariant_pred]:predicate_top variant [variant_expr]:expression_in_par end {-> New substitution.while(condition.predicate, do_subst.substitution, invariant_pred.predicate, variant_expr.expression)} | {let} let [identifiers]:expression_list be [predicate]:predicate_top in [substitution]:substitution_l1 end {-> New substitution.let([identifiers.expression], predicate.predicate, substitution.substitution)} | {definition} [def_literal]:def_literal_substitution [parameters]:def_call_params? {-> New substitution.definition(def_literal, [parameters.expression])} ; parallel_subst_tail {-> substitution*} = {single} double_vertical_bar [substitution]:substitution_l3 {-> [substitution.substitution]} | {multi} double_vertical_bar [substitution]:substitution_l3 [rest]:parallel_subst_tail {-> [substitution.substitution, rest.substitution]} ; sequence_subst_tail {-> substitution*} = {single} semicolon [substitution]:substitution_l2 {-> [substitution.substitution]} | {multi} semicolon [substitution]:substitution_l2 [rest]:sequence_subst_tail {-> [substitution.substitution, rest.substitution]} ; choice_or {-> substitution} = or [substitution]:substitution_l1 {-> New substitution.choice_or(substitution.substitution)} ; if_elsif {-> substitution} = elsif [condition]:predicate_top then [subst]:substitution_l1 {-> New substitution.if_elsif(condition.predicate, subst.substitution)}; if_else {-> substitution} = else [subst]:substitution_l1 {-> subst.substitution}; select_when {-> substitution} = when [condition]:predicate_top then [subst]:substitution_l1 {-> New substitution.select_when(condition.predicate, subst.substitution)}; select_else {-> substitution} = else [subst]:substitution_l1 {-> subst.substitution}; case_or {-> substitution} = or [expressions]:expression_list then [subst]:substitution_l1 {-> New substitution.case_or([expressions.expression], subst.substitution)}; case_else {-> substitution} = else [subst]:substitution_l1 {-> subst.substitution}; op_params {-> expression*} = left_par [parameters]:expression_list right_par {-> [parameters.expression]} ; /* Basics */ composed_identifier {-> identifier_literal*} = {single} [name]:identifier_literal {-> [name]} | {multi} [rest]:composed_identifier dot [first]:identifier_literal {-> [rest.identifier_literal, first]} ; identifier_list {-> expression*} = {single} [identifier]:composed_identifier_expression {-> [identifier.expression]} | {multi} [rest]:identifier_list comma [identifier]:composed_identifier_expression {-> [rest.expression, identifier.expression]} ; composed_identifier_expression {-> expression} = [identifier]:composed_identifier {-> New expression.identifier([identifier.identifier_literal])} ; def_call_params {-> expression*} = left_par [params]:expression_list right_par {-> [params.expression]} ; /* Patterns for opertions */ operation_pattern {-> parse_unit }= [op_name]:composed_identifier [parameters]:op_pattern_params? {-> New parse_unit.oppattern([op_name.identifier_literal], [parameters.argpattern])} ; op_pattern_params {-> argpattern*} = left_par [parameters]:oppattern_list right_par {-> [parameters.argpattern]} ; oppattern_list {-> argpattern*} = {single} [arg]:op_pattern_param {-> [arg.argpattern]} | {multiple} [rest]:oppattern_list comma [last]:op_pattern_param {-> [rest.argpattern, last.argpattern]} ; op_pattern_param {-> argpattern} = {def} [expression]:expression_in_par {-> New argpattern.def(expression.expression)} | {undef} underscore {-> New argpattern.undef()}; /******************************************************************* * Abstract Syntax Tree * *******************************************************************/ Abstract Syntax Tree parse_unit = {abstract_machine} [type]:T.machine [header]:machine_header [machine_clauses]:machine_clause* | {refinement_machine} [header]:machine_header [ref_machine]:identifier_literal [machine_clauses]:machine_clause* | {implementation_machine} [header]:machine_header [ref_machine]:identifier_literal [machine_clauses]:machine_clause* | {definition_file} [definitions_clauses]:machine_clause | {predicate} predicate | {expression} expression | {substitution} substitution | {machine_clause} machine_clause | {event_b_context} [name]:identifier_literal [context_clauses]:context_clause* | {event_b_model} [name]:identifier_literal [model_clauses]:model_clause* | {oppattern} [name]:identifier_literal* [parameters]:argpattern*; argpattern = {undef} | {def} expression; csppattern = argtype argpattern; argtype = {join} | {in} | {out}; machine_header = [name]:identifier_literal* [parameters]:expression*; context_clause = {extends} [extends]:identifier_literal* | {sets} set* | {constants} [identifiers]:expression* | {axioms} [predicates]:predicate* | {theorems} [predicates]:predicate* ; model_clause = {refines} [refines]:identifier_literal | {sees} [sees]:identifier_literal* | {variables} [identifiers]:expression* | {invariant} [predicates]:predicate* | {theorems} [predicates]:predicate* | {variant} [variant]:expression | {events} event*; machine_clause = {definitions} [definitions]:definition* | {sees} [machine_names]:expression* | {promotes} [machine_names]:expression* | {uses} [machine_names]:expression* | {includes} [machine_references]:machine_reference* | {extends} [machine_references]:machine_reference* | {imports} [machine_references]:machine_reference* | {sets} [set_definitions]:set* | {variables} [identifiers]:expression* | {concrete_variables} [identifiers]:expression* | {abstract_constants} [identifiers]:expression* | {constants} [identifiers]:expression* | {properties} [predicates]:predicate | {constraints} [predicates]:predicate | {initialisation} [substitutions]:substitution | {invariant} [predicates]:predicate | {assertions} [predicates]:predicate* | {values} [entries]:values_entry* | {local_operations} [operations]:operation* | {operations} [operations]:operation* ; machine_reference = [machine_name]:identifier_literal* [parameters]:expression* ; definition = {predicate} [name]:def_literal_predicate [parameters]:expression* [rhs]:predicate | {substitution} [name]:def_literal_substitution [parameters]:expression* [rhs]:substitution | {expression} [name]:identifier_literal [parameters]:expression* [rhs]:expression | {file} [filename]:string_body ; set = {deferred} [identifier]:identifier_literal* | {enumerated} [identifier]:identifier_literal* [elements]:expression* ; values_entry = [identifier]:identifier_literal* [value]:expression ; operation = [return_values]:expression* [op_name]:identifier_literal* [parameters]:expression* [operation_body]:substitution ; event = [event_name]:identifier_literal [status]:eventstatus [refines]:identifier_literal* [variables]:expression* [guards]:predicate* [theorems]:predicate* [assignments]:substitution* [witness]:witness*; witness = [name]:identifier_literal [predicate]:predicate; eventstatus = {ordinary} | {anticipated} | {convergent}; /* Predicates */ predicate = {conjunct} [left]:predicate [right]:predicate | {negation} [predicate]:predicate | {disjunct} [left]:predicate [right]:predicate | {implication} [left]:predicate [right]:predicate | {equivalence} [left]:predicate [right]:predicate | {universal_quantification} [identifiers]:expression* [implication]:predicate | {existential_quantification} [identifiers]:expression* [predicate]:predicate | {equal} [left]:expression [right]:expression | {unequal} [left]:expression [right]:expression | {belong} [left]:expression [right]:expression | {not_belong} [left]:expression [right]:expression | {include} [left]:expression [right]:expression | {include_strictly} [left]:expression [right]:expression | {not_include} [left]:expression [right]:expression | {not_include_strictly} [left]:expression [right]:expression | {less_equal} [left]:expression [right]:expression | {less} [left]:expression [right]:expression | {greater_equal} [left]:expression [right]:expression | {greater} [left]:expression [right]:expression | {true} | {false} | {finite} [set]:expression | {partition} [set]:expression [elements]:expression* | /* Event-B only predicate */ {definition} [def_literal]:def_literal_predicate [parameters]:expression* ; /* Expressions */ expression = {identifier} [identifier]:identifier_literal* | {primed_identifier} [identifier]:identifier_literal* [grade]:integer_literal | {string} [content]:string_body? | {true} | {false} | {integer} [literal]:integer_literal | {max_int} | {min_int} | {empty_set} | {integer_set} | {natural_set} | {natural1_set} | {nat_set} | {nat1_set} | {int_set} | {bool_set} | {string_set} | {convert_bool} [predicate]:predicate | {add} [left]:expression [right]:expression | {minus} [left]:expression [right]:expression | // only used by EventB translator {minus_or_set_subtract} [left]:expression [right]:expression | // used by this parser 'cause we cannot decide which one it is {unary} [expression]:expression | {multiplication} [left]:expression [right]:expression | // only used by EventB translator {cartesian_product} [left]:expression [right]:expression | // only used by EventB translator {mult_or_cart} [left]:expression [right]:expression | // used by this parser 'cause we cannot decide which one it is {div} [left]:expression [right]:expression | {modulo} [left]:expression [right]:expression | {power_of} [left]:expression [right]:expression | {successor} | {predecessor} | {max} [expression]:expression | {min} [expression]:expression | {card} [expression]:expression | {general_sum} [identifiers]:expression* [predicates]:predicate [expression]:expression | {general_product} [identifiers]:expression* [predicates]:predicate [expression]:expression | {couple} [list]:expression* | {comprehension_set} [identifiers]:expression* [predicates]:predicate | {prover_comprehension_set} [identifiers]:expression* [predicates]:predicate | {event_b_comprehension_set} [identifiers]:expression* [expression]:expression [predicates]:predicate | // EventB only {pow_subset} [expression]:expression | {pow1_subset} [expression]:expression | {fin_subset} [expression]:expression | {fin1_subset} [expression]:expression | {set_extension} [expressions]:expression* | {interval} [left_border]:expression [right_border]:expression | {union} [left]:expression [right]:expression | {intersection} [left]:expression [right]:expression | {set_subtraction} [left]:expression [right]:expression | {general_union} [expression]:expression | {general_intersection} [expression]:expression | {quantified_union} [identifiers]:expression* [predicates]:predicate [expression]:expression | {quantified_intersection} [identifiers]:expression* [predicates]:predicate [expression]:expression | {relations} [left]:expression [right]:expression | {identity} [expression]:expression | {event_b_identity} | // EventB v 2.0 language only {reverse} [expression]:expression | {first_projection} [exp1]:expression [exp2]:expression | {event_b_first_projection} [expression]:expression | // EventB only {event_b_first_projection_v2} | // EventB v 2.0 language only {second_projection} [exp1]:expression [exp2]:expression | {event_b_second_projection} [expression]:expression | // EventB only {event_b_second_projection_v2} | // EventB v 2.0 language only {composition} [left]:expression [right]:expression | {ring} [left]:expression [right]:expression | // EventB only {direct_product} [left]:expression [right]:expression | {parallel_product} [left]:expression [right]:expression | {iteration} [left]:expression [right]:expression | {reflexive_closure} [expression]:expression | {closure} [expression]:expression | {domain} [expression]:expression | {range} [expression]:expression | {image} [left]:expression [right]:expression | {domain_restriction} [left]:expression [right]:expression | {domain_subtraction} [left]:expression [right]:expression | {range_restriction} [left]:expression [right]:expression | {range_subtraction} [left]:expression [right]:expression | {overwrite} [left]:expression [right]:expression | {partial_function} [left]:expression [right]:expression | {total_function} [left]:expression [right]:expression | {partial_injection} [left]:expression [right]:expression | {total_injection} [left]:expression [right]:expression | {partial_surjection} [left]:expression [right]:expression | {total_surjection} [left]:expression [right]:expression | {partial_bijection} [left]:expression [right]:expression | {total_bijection} [left]:expression [right]:expression | {total_relation} [left]:expression [right]:expression | // EventB only {surjection_relation} [left]:expression [right]:expression | // EventB only {total_surjection_relation} [left]:expression [right]:expression | // EventB only {lambda} [identifiers]:expression* [predicate]:predicate [expression]:expression | {trans_function} [expression]:expression | {trans_relation} [expression]:expression | {seq} [expression]:expression | {seq1} [expression]:expression | {iseq} [expression]:expression | {iseq1} [expression]:expression | {perm} [expression]:expression | {empty_sequence} | {sequence_extension} [expression]:expression* | {size} [expression]:expression | {first} [expression]:expression | {last} [expression]:expression | {front} [expression]:expression | {tail} [expression]:expression | {rev} [expression]:expression | {concat} [left]:expression [right]:expression | {insert_front} [left]:expression [right]:expression | {insert_tail} [left]:expression [right]:expression | {restrict_front} [left]:expression [right]:expression | {restrict_tail} [left]:expression [right]:expression | {general_concat} [expression]:expression | {definition} [def_literal]:identifier_literal [parameters]:expression* | {function} [identifier]:expression [parameters]:expression* | {tree} [expression]:expression | {btree} [expression]:expression | {const} [expression1]:expression [expression2]:expression | {top} [expression]:expression | {sons} [expression]:expression | {prefix} [expression]:expression | {postfix} [expression]:expression | {sizet} [expression]:expression | {mirror} [expression]:expression | {rank} [expression1]:expression [expression2]:expression | {father} [expression1]:expression [expression2]:expression | {son} [expression1]:expression [expression2]:expression [expression3]:expression | {subtree} [expression1]:expression [expression2]:expression | {arity} [expression1]:expression [expression2]:expression | {bin} [expression1]:expression [expression2]:expression? [expression3]:expression? | {left} [expression]:expression | {right} [expression]:expression | {infix} [expression]:expression | {struct} [entries]:rec_entry* | {rec} [entries]:rec_entry* | {record_field} [record]:expression [identifier]:expression; rec_entry = [identifier]:expression [value]:expression; /* Substitutions */ substitution = {block} [substitution]:substitution | {skip} | {assign} [lhs_expression]:expression* [rhs_expressions]:expression* | {precondition} [predicate]:predicate [substitution]:substitution | {assertion} [predicate]:predicate [substitution]:substitution | {choice} [substitutions]:substitution* | {choice_or} [substitution]:substitution | {if} [condition]:predicate [then]:substitution [elsif_substitutions]:substitution* [else]:substitution? | {if_elsif} [condition]:predicate [then_substitution]:substitution | {select} [condition]:predicate [then]:substitution [when_substitutions]:substitution* [else]:substitution? | {select_when} [condition]:predicate [substitution]:substitution | {case} expression [either_expr]:expression* [either_subst]:substitution [or_substitutions]:substitution* [else]:substitution? | {case_or} [expressions]:expression* [substitution]:substitution | {any} [identifiers]:expression* [where]:predicate [then]:substitution | {let} [identifiers]:expression* [predicate]:predicate [substitution]:substitution | {becomes_element_of} [identifiers]:expression* [set]:expression| {becomes_such} [identifiers]:expression* [predicate]:predicate | {var} [identifiers]:expression* [substitution]:substitution | {sequence} [substitutions]:substitution* | {func_op} [function]:expression | {op} [name]:expression [parameters]:expression* | {op_with_return} [result_identifiers]:expression* [operation]:identifier_literal* [parameters]:expression* | {while} [condition]:predicate [do_subst]:substitution [invariant]:predicate [variant]:expression | {parallel} [substitutions]:substitution* | {definition} [def_literal]:def_literal_substitution [parameters]:expression* ;