/**** * * Saber CC grammar for FMSL V4, derived from the operational yacc grammar. * */ /** * Package */ Package parser; /** * Helpers */ Helpers letter = ['A' .. 'Z'] + ['a' .. 'z']; letter_or_underscore = ['_' + [['a' .. 'z'] + ['A' .. 'Z']]]; digit = ['0' .. '9']; alphanumeric = letter | digit; other_id_char = '_'; prime = '''; /* ' */ quesmrk = '$'; all = [0 .. 127]; non_star = [all - '*']; non_star_slash = [non_star - '/']; non_newline = all; paren_star_comment = '(*' non_star* '*'+ (non_star_slash non_star* '*'+)* ')'; dash_dash_comment = '--' non_newline*; dot_dot_dot = '...'; integer_helper = digit+; /** * Tokens */ Tokens actions_token = 'actions'; all = 'all'; and = 'and'; attribute = 'attribute'; ax = 'ax'; axiom = 'axiom'; begin = 'begin'; components = 'components'; dataflow_token = 'dataflow'; define = 'define'; else = 'else'; end = 'end'; eqn = 'eq'; equations = 'equations'; except = 'except'; exists_token = 'exists'; export_token = 'export'; extends = 'extends'; forall_token = 'forall'; foreach = 'foreach'; from = 'from'; func = 'func'; function = 'function'; if = 'if'; iff = 'iff'; implies = 'implies' | '=>'; import_token = 'import'; in = 'in'; inherits = 'inherits'; inputs_token = 'inputs'; is_token = 'is'; ques_mark = '?'; isa = 'isa'; lambda_token = 'lambda'; let_token = 'let'; mod = 'mod'; module = 'module'; not = 'not'; obj = 'obj'; object = 'object'; op_token = 'op'; operation = 'operation'; operations = 'operations'; ops_token = 'ops'; or = 'or'; out = 'out'; outputs_token = 'outputs'; parts_token = 'parts'; post = 'post'; postcondition = 'postcondition'; pre = 'pre'; precondition = 'precondition'; return_token = 'return'; then = 'then'; theorem = 'theorem'; thm = 'thm'; val = 'val'; value = 'value'; var = 'var'; variable = 'variable'; where_token = 'where'; while_token = 'while'; xor = 'xor'; neq = '!=' |'<>'; aeq = '~='; pound = '#'; pound_pound = '##'; ampersand = '&'; l_paren = '('; l_paren_two = '('; r_paren = ')'; r_paren_two = ')'; star = '*'; plus = '+'; comma = ','; minus = '-'; rt_arrow = '->' | '::='; ques_rt_arrow = '?->'; dot = '.'; attr_select = '.-' | '.:'; dot_less = '.<'; dot_gtr = '.>'; divide = '/'; colon = ':'; colon_eq = ':='; semi_colon = ';'; semi_colon_two = ';'; semi_colon_three = ';'; less = '<'; less_eq = '<='; equiv = '<=>'; eq = '='; eq_eq = '=='; gtr = '>'; gtr_eq = '>='; ques_less = '?<'; l_bkt = '['; r_bkt = ']'; caret = '^'; l_brace = '{'; bar = '|'; r_brace = '}'; dot_dot = '..'; nil = 'nil'; ident = (quesmrk? letter_or_underscore ( alphanumeric | other_id_char)* prime*) | dot_dot_dot; symlit = ''' all* '''; number = integer_helper '.' integer_helper; real = integer_helper '.' integer_helper; integer = integer_helper; string = '\"' all* '\"'; comment = paren_star_comment | dash_dash_comment; whitespace = ' ' | '\n' | '\t' | '\r'; /** * Ignored */ Ignored Tokens comment, whitespace; /** * Productions */ Productions top_level_def = spec_unit ; spec_unit = {module_def_no_attrs} module_heading entity_spec_list end module_name_ender semi_colon | {module_def_with_attrs} module_heading attr_defs semi_colon entity_spec_list end module_name_ender semi_colon_two | {module_def_empty_body} module_heading end module_name_ender semi_colon | {module_def_attrs_only} module_heading attr_defs semi_colon end module_name_ender semi_colon_three | {entity_spec_list} entity_spec_list | {attr_def} attr_def semi_colon ; module_heading = {module_name} module module_name semi_colon | {module_name_imports} module module_name semi_colon imports | {module_name_exports} module module_name semi_colon exports | {module_name_imports_exports} module module_name semi_colon imports exports ; imports = {import} import_token | {import_imports} import_token imports ; import = {from_import} from name import name_list semi_colon | {from_import_all} from name import all semi_colon | {from_import_all_except} from name import all except name_list semi_colon | {import} import name_list semi_colon ; exports = {export} export_token | {export_exports} export_token exports ; export = {export} export name_list semi_colon | {export_all} export all semi_colon ; entity_spec_list = {entity_spec} entity_spec | {entity_spec_list_entity_spec} entity_spec_list entity_spec ; entity_spec = {object_spec} object_spec semi_colon | {operation_spec} operation_spec semi_colon | {value_spec} value_spec semi_colon | {formal_decl} formal_decl ; object_spec = {obj_heading_parts_body} obj_heading is parts_spec obj_body | {obj_heading_body} obj_heading obj_body ; is = {is} is_token | {rt_arrow} rt_arrow ; obj_heading = {name} name | {obj_sym_name} obj_symbol name | {obj_sym_name_inherits} obj_symbol name inheritsfrom_symbol class_name_list ; operation_spec = {op_heading_body} op_heading op_body | {op_heading_expr_body} op_heading eq expr op_body | {op_heading_begin_block_body} op_heading eq begin_block op_body ; obj_body = {empty} /* empty */ | {end} end name_ender | {obj_attrs_end} obj_attributes end name_ender ; op_heading = {op_sym_name_parms} op_symbol op_name_enter op_parms | {op_sym_name_parms_inherits} op_symbol op_name_enter op_parms inheritsfrom_symbol class_name_list | {op_sym_name} op_symbol op_name_enter | {op_sym_name_inherits} op_symbol op_name_enter inheritsfrom_symbol class_name_list | {op_sym_name_parms_inherits_parms} op_symbol op_name_enter inheritsfrom_symbol class_name_list op_parms ; op_body = {empty} /* empty */ | {end} end op_name_ender | {op_attrs_end} op_attributes end op_name_ender ; begin_block = {begin_exprs} begin executable_exprs end | {begin_decls_exprs} begin var_decls semi_colon executable_exprs end | {exprs_expr} executable_exprs semi_colon executable_expr ; executable_exprs = {executable_expr} executable_expr | {executable_exprs} executable_exprs semi_colon executable_expr ; executable_expr = {empty} /* empty */ | {assmnt_expr} assmnt_expr | {if_then_stmt} if_then_stmt | {foreach} foreach | {while} while | {functional_expr} functional_expr | {return} return ; assmnt_expr = designator colon_eq assmnt_or_expr // %prec colon_eq ; designator = {selector_expr} selector_expr | {index_expr} index_expr | {obj_name} obj_name ; if_then_stmt = if expr then executable_exprs end ; while = while_token l_paren assmnt_or_expr r_paren executable_exprs end ; return = return_token expr ; assmnt_or_expr = {assmnt_expr} assmnt_expr | {expr} expr ; parts_spec = {parts_spec_one} parts_spec_one | {parts_spec_one_embedded} parts_spec_one embedded_action_decls ; parts_spec_one = {parts_spec_two} parts_spec_two | {parts_spec_one_or} parts_spec_one or_op parts_spec_two // %prec or | {parts_spec_one_embedded} parts_spec_one embedded_action_decls or_op parts_spec_two // %prec or ; parts_spec_two = {empty} /* empty */ | {parts_spec_two_and} parts_spec_two and_op parts_spec_two_x // %prec and | {parts_spec_two_list} parts_spec_two postfix_list_op // %prec unyplus | {op} op l_paren sig_args_list r_paren // %prec rt_arrow | {op_arrow_two} op l_paren_two sig_args_list r_paren rt_arrow l_paren sig_args_list_out r_paren_two // %prec rt_arrow | {name} name colon l_paren parts_spec_one r_paren | {l_paren} l_paren parts_spec_one r_paren | {name_type_opt_pair_list} name_type_opt_pair_list | {string} string | {integer} integer | {real} real | {nil} nil ; parts_spec_two_x = parts_spec_two; op = {op} op_token | {func} func ; name_type_opt_pair_list = {name_type_opt_pair_possibly_starred} name_type_opt_pair_possibly_starred | {name_type_opt_pair_possibly_starred_list} name_type_opt_pair_possibly_starred name_type_opt_pair_list ; embedded_action_decls = {l_brace} l_brace action_decls r_brace | {l_brace_semi} l_brace action_decls semi_colon r_brace ; and_op = {and} and | {comma} comma ; or_op = {or} or | {bar} bar ; postfix_list_op = star ; value_spec = val_symbol name_type_pair eq expr obj_body ; where = where_symbol colon where_list semi_colon ; where_list = {empty} /* empty */ | {where_item} where_item | {where_list} where_list semi_or_comma where_item ; where_item = where_eq ; where_eq = name eq name_two ; name_two = name; ops = ops_symbol colon op_signatures semi_colon ; inputs = in_symbol colon inputs_list ; outputs = out_symbol colon outputs_list ; op_signatures = {empty} /* empty */ | {op_signature} op_signature | {op_signatures} op_signatures semi_or_comma op_signature ; semi_or_comma = {comma} comma | {semi_colon} semi_colon ; op_signature = {op_name} op_name | {op_sig_name} op_sig_name op_parms | {op_sig_name_colon} op_sig_name colon op_parms ; op_sig_name = op_name ; op_parms = {is} is | {l_paren_arrow_args} l_paren_two sig_args_list r_paren rt_arrow l_paren sig_args_list_out r_paren_two | {l_paren_arrow_arg} l_paren sig_args_list r_paren rt_arrow sig_arg | {l_paren_args} l_paren sig_args_list r_paren ; name_obj_list = {empty} /* empty */ | {name_obj_pair} name_obj_pair | {name_obj_list} name_obj_list comma name_obj_pair ; inputs_list = ins_parts_spec ; outputs_list = outs_parts_spec ; parts = parts_symbol colon parts_spec ; ins_parts_spec = {empty} /* empty */ | {ins_parts_spec} ins_parts_spec and_op ins_parts_spec_two // %prec and | {init_name_type_pair_list} init_name_type_pair postfix_list_op // %prec unyplus | {init_name_type_pair} init_name_type_pair ; ins_parts_spec_two = ins_parts_spec; outs_parts_spec = {empty} /* empty */ | {outs_parts_spec} outs_parts_spec and_op outs_parts_spec_two // %prec and | {init_name_type_pair_list} init_name_type_pair postfix_list_op // %prec unyplus | {init_name_type_pair} init_name_type_pair ; outs_parts_spec_two = outs_parts_spec; obj_attributes = {obj_attribute} obj_attribute | {obj_attributes} obj_attributes obj_attribute ; obj_attribute = {parts} parts semi_colon | {where} where | {ops} ops | {eqns} eqns | {actions} actions | {attr_name} attr_name attr_colon semi_colon | {attr_name_text} attr_name attr_colon text semi_colon | {attr_names} attr_name colon name_list semi_colon | {attr_expr} attr_name colon expr semi_colon | {attr_begin} attr_name colon begin_block semi_colon ; text = string; attr = string; attr_colon = colon ; attr_name = attr ; op_attributes = {op_attribute} op_attribute | {op_attributes} op_attributes op_attribute ; op_attribute = {parts} parts semi_colon | {inputs} inputs semi_colon | {outputs} outputs semi_colon | {precond} precond semi_colon | {postcond} postcond semi_colon | {dataflow} dataflow semi_colon | {attr_name} attr_name attr_colon semi_colon | {attr_name_text} attr_name colon text semi_colon | {attr_name_list} attr_name colon name_list semi_colon | {attr_name_expr} attr_name colon expr semi_colon | {attr_name_begin} attr_name colon begin_block semi_colon ; name_type_pair = {obj_name} obj_name | {name} name colon obj_name ; name_type_opt_pair_possibly_starred = {name_type_opt_pair} name_type_opt_pair | {name_type_opt_pair_list} name_type_opt_pair postfix_list_op // %prec unyplus ; name_type_opt_pair = {obj_name} obj_name | {obj_name_expr} obj_name eq expr | {name_colon} name colon obj_name | {name_colon_expr} name colon obj_name eq expr ; name_obj_pair = name_list colon name ; init_name_type_pair = {name_type_pair} name_type_pair | {name_type_pair_colon} name_type_pair colon_eq obj_expr ; module_name = name ; module_name_ender = {empty} /* empty */ | {name} name ; class_name_list = {class_name} class_name | {class_name_list} class_name_list comma class_name ; class_name = qualident ; obj_name = {qualident} qualident | {symlit} symlit ; qualident = {name} name | {name_dot} name dot qualident ; name_ender = {empty} /* empty */ | {name} name ; op_name = {name} name | {string} string ; op_name_enter = {name} name | {string} string ; op_name_ender = {empty} /* empty */ | {op_name} op_name ; formal_decl = {var_decl} var_decl semi_colon | {ax_decl} ax_decl semi_colon | {thm_decl} thm_decl semi_colon ; var_decls = {var_decl} var_decl | {var_decls} var_decls semi_colon var_decl ; var_decl = {var_symbol} var_symbol name_list colon obj_name | {var_symbol_name} var_symbol name_list colon name eq expr ; precond = {pre_symbol} pre_symbol colon | {pre_symbol_expr} pre_symbol colon expr ; postcond = {post_symbol} post_symbol colon | {post_symbol_expr} post_symbol colon expr ; dataflow = dataflow_symbol colon connection_list ; connection_list = {connection} connection | {connection_list} connection_list comma connection ; connection = connection_designator rt_arrow connection_designator_two ; connection_designator = {expr} expr | {isa} isa ; connection_designator_two = connection_designator; expr = {let} let | {lambda} lambda | {and} expr and expr_and // %prec and | {or} expr or expr_or // %prec or | {xor} expr xor expr_xor // %prec xor | {implies} expr implies expr_implies // %prec implies | {equiv} expr equiv expr_equiv // %prec equiv | {not} not expr // %prec not | {if} if expr then expr_if // %prec if | {if_else} if expr then expr_then else expr_else // %prec if | {forall} forall l_paren name_obj_list r_paren expr // %prec forall | {forall_in} forall l_paren name in expr_in r_paren expr // %prec forall | {forall_bar} forall l_paren name_obj_list bar expr_bar r_paren expr // %prec forall | {exists} exists l_paren name_obj_list r_paren expr // %prec exists | {exists_in} exists l_paren name in expr_ein r_paren expr // %prec exists | {exists_bar} exists l_paren name_obj_list bar expr_ebar r_paren expr // %prec exists | {rel_expr} rel_expr ; expr_and = expr; expr_or = expr; expr_xor = expr; expr_implies = expr; expr_equiv = expr; expr_if = expr; expr_then = expr; expr_else = expr; expr_in = expr; expr_bar = expr; expr_ein = expr; expr_ebar = expr; expr_let = expr; expr_lambda = expr; expr_rel = expr; let = {let} let_token name_list eq expr | {let_colon} let_token name colon name_two eq expr_let ; expr_list = {empty} /* empty */ | {exprlelem} exprlelem | {expr_list} expr_list comma exprlelem ; exprlelem = expr ; expr_list_with_empties = {exprlelem_possibly_empty} exprlelem_possibly_empty | {expr_list} expr_list comma exprlelem_possibly_empty ; exprlelem_possibly_empty = {empty} /* empty */ | {expr} expr ; expr_seq = {expr_seq_elem} expr_seq_elem | {expr_seq} expr_seq semi_colon expr_seq_elem ; expr_seq_elem = {empty} /* empty */ | {expr} expr ; lambda = /* empty for now */ // lambda_token l_paren sig_args_list_two r_paren_two rt_arrow l_paren sig_args_list r_paren_two expr_lambda ; sig_args_list_two = sig_args_list; forall = forall_token ; exists = exists_symbol ; rel_expr = {expr} expr rel_bin_op expr_rel // %prec eq | {name} name almost_eq_op expr except except_item | {name_list} name almost_eq_op expr except l_paren except_list r_paren | {arith_expr} arith_expr ; except_list = {except_item} except_item | {except_list} except_list comma except_item ; except_item = selector_expr eq expr // %prec eq ; arith_expr = {add} arith_expr arith_add_op arith_expr_add // %prec plus | {mult} arith_expr arith_mult_op arith_expr_mult // %prec star | {exp} arith_expr arith_exp_op arith_expr_exp // %prec caret | {length_pre_op} length_pre_op arith_expr_length // %prec pound | {arith_pre_op} arith_pre_op arith_expr // %prec unyplus | {selector_expr} selector_expr | {index_expr} index_expr | {functional_expr} functional_expr | {obj_atom} obj_atom | {dot_dot} l_bkt expr dot_dot expr_dot_dot r_bkt | {expr_list} l_bkt expr_list r_bkt | {expr_list_with_empties} l_brace expr_list_with_empties r_brace | {expr_seq} l_paren expr_seq r_paren ; arith_expr_add = arith_expr; arith_expr_mult = arith_expr; arith_expr_exp = arith_expr; arith_expr_length = arith_expr; arith_expr_dot_dot = arith_expr; selector_expr = arith_expr select_op name // %prec dot /* * 16jan06 Update: Enabled this and extant regression tests pass. Still need * to add some new testing. */ | {select_const} arith_expr select_op const_val // %prec dot | {select_name} arith_expr select_op name pound integer | {select_name_pound} arith_expr select_op const_val pound integer | {pound_int} arith_expr pound integer | {pound_pound} arith_expr pound_pound | {pound_int_dot_dot} arith_expr pound integer dot_dot integer_dot_dot // %prec dot_dot | {pound_int_dot_dot_pound_pound} arith_expr pound integer dot_dot pound_pound | {pound_attr_select} arith_expr attr_select attr_name ; integer_dot_dot = integer; const_val = {string} string | {integer} integer | {real} real ; index_expr = {expr} arith_expr l_bkt expr r_bkt // %prec l_bkt | {expr_dot_dot} arith_expr l_bkt expr dot_dot expr_dot_dot r_bkt // %prec l_bkt | {expr_colon} arith_expr l_bkt expr colon expr_colon r_bkt // %prec l_bkt ; expr_dot_dot = expr; expr_colon = expr; functional_expr = {op_args} arith_expr l_paren op_args r_paren | {op_args_arrow} arith_expr l_paren_two op_args r_paren_two ques_rt_arrow // Remainder gone for now: l_paren op_args r_paren ; op_args = /* empty */ | {op_arg} op_arg | {op_args} op_arg comma op_args ; sig_args_list = ins_parts_spec ; sig_args_list_out = outs_parts_spec ; sig_arg = {init_name_type_pair} init_name_type_pair | {init_name_type_pair_postfix} init_name_type_pair postfix_list_op // %prec unyplus ; op_arg = expr ; rel_bin_op = {eq} eq | {less} less | {gtr} gtr | {neq} neq | {less_eq} less_eq | {gtr_eq} gtr_eq | {in} in ; almost_eq_op = aeq ; arith_add_op = {plus} plus | {minus} minus ; arith_mult_op = {star} star | {divide} divide | {mod} mod ; arith_exp_op = caret ; length_pre_op = pound ; arith_pre_op = {plus} plus | {minus} minus ; select_op = {dot} dot | {isa} isa // %prec dot | {dot_less} dot_less | {ques_less} ques_less ; eqns = {eqns_symbol} eqns_symbol colon eqn_decls semi_colon | {eqns_symbol_semi} eqns_symbol colon_two var_decls // Remainder gone: semi_colon eqn_decls semi_colon ; colon_two = colon; eqn_decls = {empty} /* empty */ | {eqn_decl} eqn_decl | {eqn_decls} eqn_decls semi_colon eqn_decl ; eqn_decl = lhs eq_eq rhs ; lhs = functional_expr ; rhs = expr ; actions = actions_symbol colon action_decls semi_colon ; action_decls = {empty} /* empty */ | {action_decl} action_decl | {action_decls} action_decls semi_colon action_decl ; action_decl = action_lhs eq_eq action_rhs ; action_lhs = {name_attr_select} name attr_select attr_name | {name_dot} name dot attr_name | {name} name ; action_rhs = expr ; ax_decl = {ax_symbol} ax_symbol expr | {ax_symbol_ident} ax_symbol ident colon expr ; thm_decl = thm_symbol expr ; obj_expr = {obj_atom} obj_atom | {l_bkt} l_bkt r_bkt | {l_bkt_obj_expr} l_bkt obj_expr_list r_bkt ; obj_expr_list = {obj_expr} obj_expr | {obj_expr_list} obj_expr_list comma obj_expr ; obj_atom = {string} string | {integer} integer | {real} real | {symlit} symlit | {nil} nil | {name} name ; name_list = {name} name | {name_list} name_list comma name ; name = ident ; attr_defs = {attr_def} attr_def | {attr_defs} attr_defs semi_colon attr_def ; attr_def = {attr_def_one_parts_spec} attr_def_one colon parts_spec | {attr_def_one} attr_def_one ; attr_def_one = {define_obj} define obj_symbol attribute name_list | {define_op} define op_symbol attribute name_list | {define} define attribute name_list ; obj_symbol = {object} object | {obj} obj ; val_symbol = {value} value | {val} val ; inheritsfrom_symbol = {inherits} inherits from | {extends} extends | {less} less ; op_symbol = {operation} operation | {op} op | {function} function | {func} func ; parts_symbol = {components} components | {parts} parts_token ; ops_symbol = {operations} operations | {ops} ops_token ; in_symbol = {inputs} inputs_token | {in} in ; out_symbol = {outputs} outputs_token | {out} out ; var_symbol = {variable} variable | {var} var ; eqns_symbol = equations ; actions_symbol = actions_token ; ax_symbol = {axiom} axiom | {ax} ax ; thm_symbol = {theorem} theorem | {thm} thm ; pre_symbol = {precondition} precondition | {pre} pre ; post_symbol = {postcondition} postcondition | {post} post ; dataflow_symbol = dataflow_token ; exists_symbol = exists_token ; where_symbol = where_token ;