/**** * * Yacc grammar for RSL V4. * */ /** * Declarations */ /* * Includes for definition files */ %{ #include "std-macros.h" #include #include "parse-tree.h" #include "parser.h" #include "sym.h" #include "translator.h" #include "parser-aux.h" #include "sym-aux.h" #include "lex.h" int inAttribute; /* exported to lexer.l, q.v. */ int inParts; /* ditto */ int anonopnum; /* counter for anonymous op types */ extern int yydebug; /* imported from lexer.l */ extern int yylineno; /* ibid. */ extern int yycharno; /* ibid. */ extern char* yyfilename; /* ibid. */ /* Browser hooks */ int startp,endp; /* start and end position of a NAME */ int startp2,endp2; /* start and end position of a NAME */ extern int bm_startpos,bm_endpos; %} /* * Start Symbol */ %start top_level_def /* * Terminal Symbols */ %token YEOF 0 %token YACTIONS YAEQ YALL YAND YATTRIBUTE YAX YAXIOM YBEGIN YCOMPONENTS YDATAFLOW YDEFINE YELSE YEND YEQ YEQUATIONS YEXCEPT YEXISTS YEXPORT YEXTENDS YFORALL YFOREACH YFROM YFUNC YFUNCTION YIF YIFF YIMPLIES YIMPORT YIN YINHERITS YINPUTS YIS YISA YLAMBDA YLET YMOD YMODULE YNOT YOBJ YOBJECT YOF YOP YOPERATION YOPERATIONS YOPS YOR YOUT YOUTPUTS YPARTS YPOST YPOSTCONDITION YPOUNDPOUND YPRE YPRECONDITION YRETURN YTHEN YTHEOREM YTHM YVAL YVALUE YVAR YVARIABLE YWHERE YWHILE YXOR YLIST /* not used in rules, but in list nodes */ YCONST /* not used in rules, but in InstallConst in sym-aux.c */ YARRAY /* not used in rules, but in BuildOpenArrayType */ YRECORD /* not used in rules, but in tree */ YASSMNT YATTRSELECT YCHKINSTANCE YEQEQ YGEQ YGETINSTANCE YLEQ YNEQ YQRTARROW YRETRACT YRTARROW '#' '(' ')' '*' '+' ',' '-' '.' '/' ':' ';' '<' '=' '>' '[' ']' '^' '{' '|' '}' '?' /* * Non-Terminal cum Terminal Symbols */ %token Yident %token Yattr %token Yinteger %token Yoctal %token Yhex %token Yreal %token Ynumber %token Ychar %token Ystring %token Ytext %token Ysymlit %token Ynil /* * Operator Precedences */ %left ')' %left ']' %right YASSMNT /* := */ %left YLET %left YFORALL YEXISTS %left YIF YIFF YIMPLIES %left '|' YOR YXOR %left YAND ',' %left YAEQ YEXCEPT %left '=' YNEQ '<' '>' YLEQ YGEQ /* relational ops */ %left YIN %left YDOTDOT %left '+' '-' /* '|' YOR YXOR */ /* add ops */ /* %left YAND ',' */ /* and ops */ %left ';' /* expr seq op */ %left '*' '/' YDIV YMOD /* mult ops */ %left '^' /* exponentiation op */ %left '#' %left YPOUNDPOUND %left '.' YIS YISA YGETINSTANCE YCHKINSTANCE YATTRSELECT /* selector ops */ %right '[' '{' %left YUNYPLUS YUNYMINUS YNOT /* unary ops */ %right '(' /* * Non-Terminal Symbols */ %type action_decl action_decls action_lhs action_rhs actions actions_symbol almost_eq_op and_op arith_add_op arith_exp_op arith_expr arith_mult_op arith_pre_op assmnt_expr assmnt_or_expr attr_colon attr_def attr_def1 attr_defs attr_name ax_decl ax_symbol begin_block class_name class_name_list connection connection_designator connection_list const_val dataflow dataflow_symbol designator embedded_action_decls entity_spec entity_spec_list eqn_decl eqn_decls eqns eqns_symbol except_list except_item executable_expr executable_exprs exists exists_symbol export exports expr expr_list expr_seq expr_list_with_empties expr_seq_elem exprlelem exprlelem_possibly_empty forall foreach formal_decl functional_expr if_then_stmt import imports in_symbol index_expr init_name_type_pair inputs inputs_list ins_parts_spec inheritsfrom_symbol is lambda length_pre_op let lhs module_heading module_name module_name_ender name name_ender name_list name_obj_list name_obj_pair name_type_opt_pair name_type_opt_pair_list name_type_opt_pair_possibly_starred name_type_pair obj_atom obj_attribute obj_attributes obj_expr obj_expr_list obj_heading obj_name obj_symbol obj_body object_spec op op_arg op_args op_attribute op_attributes op_heading op_name op_name_ender op_name_enter op_parms op_sig_name op_signature op_signatures op_symbol op_body operation_spec ops ops_symbol or_op out_symbol outputs outputs_list outs_parts_spec parts parts_spec parts_spec_1 parts_spec_2 parts_symbol post_symbol postcond postfix_list_op pre_symbol precond qualident rel_bin_op rel_expr return rhs select_op selector_expr semi_or_comma sig_arg sig_args_list sig_args_list_out spec_unit thm_decl thm_symbol val_symbol value_spec var_decl var_decls var_symbol where where_eq where_item where_list where_symbol while /** * Rules */ %% top_level_def: spec_unit ; spec_unit: module_heading entity_spec_list YEND module_name_ender ';' { parsetree = $1; SetSpecUnitBody($$, $2); ExitModule($1); ChkEnder(GetModuleName($1), $4); YYACCEPT; } | module_heading attr_defs ';' entity_spec_list YEND module_name_ender ';' { nodep newnd; $1->components.module.priority = null; /* * $1->components.module.imports = null; $1->components.module.exports = null; * */ $1->components.module.body = (newnd = NewNode(SPEC_NODE, null, $1->header.loc)); newnd->components.spec.entities = FixDeclList($4); parsetree = $1; ExitModule($1); ChkEnder($1->components.module.name, $6); YYACCEPT; } | module_heading YEND module_name_ender ';' { nodep newnd; $1->components.module.priority = null; /* * $1->components.module.imports = null; $1->components.module.exports = null; * */ $1->components.module.body = (newnd = NewNode(SPEC_NODE, null, $1->header.loc)); newnd->components.spec.entities = null; parsetree = $1; ExitModule($1); ChkEnder($1->components.module.name, $3); YYACCEPT; } | module_heading attr_defs ';' YEND module_name_ender ';' { nodep newnd; $1->components.module.priority = null; /* * $1->components.module.imports = null; $1->components.module.exports = null; * */ $1->components.module.body = (newnd = NewNode(SPEC_NODE, null, $1->header.loc)); newnd->components.spec.entities = null; parsetree = $1; ExitModule($1); ChkEnder($1->components.module.name, $5); YYACCEPT; } | entity_spec_list { parsetree = $1; YYACCEPT; } | attr_def ';' { parsetree = null; YYACCEPT; } | YEOF { parsetree = null; YYACCEPT; } ; module_heading: YMODULE module_name ';' { $$ = NewNode(MODULE_NODE, YOBJ, $1.loc); $$->components.module.name = $2; $$->components.module.imports = null; $$->components.module.exports = null; EnterModule($2, YMODULE); } | YMODULE module_name ';' imports { $$ = NewNode(MODULE_NODE, YOBJ, $1.loc); $$->components.module.name = $2; $$->components.module.imports = $4; $$->components.module.exports = null; EnterModule($2, YMODULE); } | YMODULE module_name ';' exports { $$ = NewNode(MODULE_NODE, YOBJ, $1.loc); $$->components.module.name = $2; $$->components.module.imports = null; $$->components.module.exports = $4; EnterModule($2, YMODULE); } | YMODULE module_name ';' imports exports { $$ = NewNode(MODULE_NODE, YOBJ, $1.loc); $$->components.module.name = $2; $$->components.module.imports = $4; $$->components.module.exports = $5; EnterModule($2, YMODULE); } ; imports: import { $$->components.decl.next = null; $$ = $1; } | import imports { $1->components.decl.next = $2; $$ = $1; } ; import: YFROM name YIMPORT name_list ';' { $$ = NewNode(DECL_NODE, YIMPORT, $1.loc); $$->components.decl.kind.import.from = $2; $$->components.decl.kind.import.names = FixAtomList($4); $$->components.decl.kind.import.isall = FALSE; /*EnterImports($2, $4);*/ } | YFROM name YIMPORT YALL ';' { $$ = NewNode(DECL_NODE, YIMPORT, $1.loc); $$->components.decl.kind.import.from = $2; $$->components.decl.kind.import.names = null; $$->components.decl.kind.import.isall = TRUE; } | YFROM name YIMPORT YALL YEXCEPT name_list ';' { $$ = NewNode(DECL_NODE, YIMPORT, $1.loc); $$->components.decl.kind.import.from = $2; $$->components.decl.kind.import.names = FixAtomList($6); $$->components.decl.kind.import.isall = TRUE; } | YIMPORT name_list ';' { $$ = NewNode(DECL_NODE, YIMPORT, $1.loc); $$->components.decl.kind.import.from = null; $$->components.decl.kind.import.names = FixAtomList($2); $$->components.decl.kind.import.isall = FALSE; /*EnterImports(null, $2);*/ } ; exports: export { $$->components.decl.next = null; $$ = $1; } | export exports { $1->components.decl.next = $2; $$ = $1; } ; export: YEXPORT name_list ';' { $$ = NewNode(DECL_NODE, YEXPORT, $1.loc); $$->components.decl.kind.export_.isqual = FALSE; $$->components.decl.kind.export_.names = FixAtomList($2); $$->components.decl.kind.export_.isall = FALSE; /*EnterExports($2, null);*/ } | YEXPORT YALL ';' { $$ = NewNode(DECL_NODE, YEXPORT, $1.loc); $$->components.decl.kind.export_.isqual = FALSE; $$->components.decl.kind.export_.names = null; $$->components.decl.kind.export_.isall = TRUE; /*EnterExports($2, null);*/ } ; entity_spec_list: entity_spec { $$ = InitDeclList($1); } | entity_spec_list entity_spec { $$ = AddToDeclList($1, $2); } ; entity_spec: object_spec ';' { EnterObject($1); $$ = $1; } | operation_spec ';' { EnterOperation($1); $$ = $1; } | value_spec ';' { EnterObject($1); $$ = $1; } | formal_decl | error {$$ = null;} ; object_spec: obj_heading is {inParts = true; /*SetGrammarFlag();*/} /* $1 $2 $3 */ parts_spec {inParts = false; /*ClearGrammarFlag();*/} obj_body /* $4 $5 $6 */ { $$ = $1; $$->components.decl.kind.obj.name = $1->components.decl.kind.obj.name; $$->components.decl.kind.obj.flags = null; $$->components.decl.kind.obj.where = FindAttr($6, YWHERE); $$->components.decl.kind.obj.ops = FindAttr($6, YOPS); $$->components.decl.kind.obj.eqns = FindAttr($6, YEQUATIONS); $$->components.decl.kind.obj.attrs = $6; /* Note: built-ins are still there. */ ProcessAbsObjAttrs($$,$4,$6); ExitObject($$, startp, endp); } /* * | val_symbol name_type_pair '=' expr { $$ = $1; $$->components.decl.kind.obj.name = $2->components.decl.kind.attr.name; $$->components.decl.kind.obj.flags = isDef; EnterObjectName($$,$2); $$->components.decl.kind.obj.attrs = $4; -- Note: built-ins are still there. ProcessConcObjAttrs($$,$4,null); ExitObject($$, startp, endp); } * */ | obj_heading obj_body { $$ = $1; if ($$) { $$->components.decl.kind.obj.name = $1->components.decl.kind.obj.name; $$->components.decl.kind.obj.flags = null; $$->components.decl.kind.obj.where = FindAttr($2, YWHERE); $$->components.decl.kind.obj.ops = FindAttr($2, YOPS); $$->components.decl.kind.obj.eqns = FindAttr($2, YEQUATIONS); $$->components.decl.kind.obj.attrs = $2; /* Note: built-ins are still there. */ ProcessAbsObjAttrs($$,null,$2); ExitObject($$, startp, endp); } } | obj_heading error {$$=null;} ; is: '=' {$$=null;} | YIS {$$=null;} | YRTARROW {$$=null;} ; obj_heading: /* * This first RHS alternative allows keywordless obj defs, to provide a * conventional syntax for obj defs as grammar rules. */ name { $$ = NewNode(DECL_NODE, YOBJ, $1->header.loc); $$->components.decl.kind.obj.name = $1; $$->components.decl.kind.obj.flags = 0; $$->components.decl.kind.obj.inheritsfrom = null; EnterObjectName($$,$1); } | name inheritsfrom_symbol class_name_list { $$ = NewNode(DECL_NODE, YOBJ, $1->header.loc); $$->components.decl.kind.obj.name = $1; $$->components.decl.kind.obj.flags = 0; $$->components.decl.kind.obj.inheritsfrom = FixAtomList2($3); EnterObjectName($$,$1); } | obj_symbol name { $$ = $1; $$->components.decl.kind.obj.name = $2; $$->components.decl.kind.obj.flags = 0; $$->components.decl.kind.obj.inheritsfrom = null; EnterObjectName($$,$2); } | obj_symbol name inheritsfrom_symbol class_name_list { $$ = $1; $$->components.decl.kind.obj.name = $2; $$->components.decl.kind.obj.flags = 0; $$->components.decl.kind.obj.inheritsfrom = FixAtomList2($4); EnterObjectName($$,$2); } | obj_symbol name inheritsfrom_symbol class_name_list error {$$ = null;} ; operation_spec: op_heading op_body { $$ = $1; $$->components.decl.kind.op.parts = null; if (not $1->components.decl.kind.op.ins) { $$->components.decl.kind.op.ins = FindAttr($2, YINPUTS); } if (not $1->components.decl.kind.op.outs) { $$->components.decl.kind.op.outs = FindAttr($2, YOUTPUTS); } $$->components.decl.kind.op.parts = FindAttr($2, YPARTS); $$->components.decl.kind.op.precond = FindAttr($2, YPRE); $$->components.decl.kind.op.postcond = FindAttr($2, YPOST); $$->components.decl.kind.op.attrs = $2; ProcessOpAttrs($$,null,null,$2); ExitOperation($$, null, startp, endp); } | op_heading '=' expr op_body { $$ = $1; $$->components.decl.kind.op.parts = null; if (not $1->components.decl.kind.op.ins) { $$->components.decl.kind.op.ins = FindAttr($4, YINPUTS); } if (not $1->components.decl.kind.op.outs) { $$->components.decl.kind.op.outs = FindAttr($4, YOUTPUTS); } if ($3) { $$->components.decl.kind.op.parts = $3; $$->components.decl.kind.op.flags = isDef; } else { $$->components.decl.kind.op.parts = FindAttr($4, YPARTS); } $$->components.decl.kind.op.precond = FindAttr($4, YPRE); $$->components.decl.kind.op.postcond = FindAttr($4, YPOST); $$->components.decl.kind.op.attrs = $4; ProcessOpAttrs($$,null,$3,$4); ExitOperation($$, null, startp, endp); } | op_heading '=' begin_block op_body { $$ = $1; $$->components.decl.kind.op.parts = null; if (not $1->components.decl.kind.op.ins) { $$->components.decl.kind.op.ins = FindAttr($4, YINPUTS); } if (not $1->components.decl.kind.op.outs) { $$->components.decl.kind.op.outs = FindAttr($4, YOUTPUTS); } if ($3) { $$->components.decl.kind.op.parts = $3; $$->components.decl.kind.obj.flags = isDef; } else { $$->components.decl.kind.op.parts = FindAttr($4, YPARTS); } $$->components.decl.kind.op.precond = null; $$->components.decl.kind.op.postcond = null; $$->components.decl.kind.op.attrs = $4; ProcessOpAttrs($$,null,$3,$4); ExitOperation($1, null, startp, endp); } ; obj_body: /* empty */ {$$ = null;} | YEND name_ender {$$ = null;} | obj_attributes YEND name_ender { $$ = FixDeclList($1); } ; op_heading: op_symbol op_name_enter op_parms { $$ = $1; $$->components.decl.kind.obj.name = $2; $$->components.decl.kind.obj.flags = 0; $$->components.decl.kind.obj.inheritsfrom = null; if ($3) { $$->components.decl.kind.op.ins = $3->components.decl.kind.opsig.ins; $$->components.decl.kind.op.outs = $3->components.decl.kind.opsig.outs; } } | op_symbol op_name_enter op_parms inheritsfrom_symbol class_name_list { $$ = $1; $$->components.decl.kind.obj.name = $2; $$->components.decl.kind.obj.flags = 0; $$->components.decl.kind.obj.inheritsfrom = FixAtomList2($5); if ($3) { $$->components.decl.kind.op.ins = $3->components.decl.kind.opsig.ins; $$->components.decl.kind.op.outs = $3->components.decl.kind.opsig.outs; } } | op_symbol op_name_enter { $$ = $1; $$->components.decl.kind.obj.name = $2; $$->components.decl.kind.obj.flags = 0; $$->components.decl.kind.obj.inheritsfrom = null; } | op_symbol op_name_enter inheritsfrom_symbol class_name_list { $$ = $1; $$->components.decl.kind.obj.name = $2; $$->components.decl.kind.obj.flags = 0; $$->components.decl.kind.obj.inheritsfrom = FixAtomList2($4); } | op_symbol op_name_enter inheritsfrom_symbol class_name_list op_parms { $$ = $1; $$->components.decl.kind.obj.name = $2; $$->components.decl.kind.obj.flags = 0; $$->components.decl.kind.obj.inheritsfrom = FixAtomList2($4); if ($5) { $$->components.decl.kind.op.ins = $5->components.decl.kind.opsig.ins; $$->components.decl.kind.op.outs = $5->components.decl.kind.opsig.outs; } } ; op_body: /* empty */ {$$ = null;} | YEND op_name_ender {$$ = null;} | op_attributes YEND op_name_ender { $$ = FixDeclList($1); } ; begin_block: YBEGIN executable_exprs YEND { $$ = NewNode(BINOP_NODE, YBEGIN, $1.loc); $$->components.binop.left_operand = null; $$->components.binop.right_operand = FixExprList($2); } | YBEGIN var_decls ';' executable_exprs YEND { $$ = NewNode(BINOP_NODE, YBEGIN, $1.loc); $$->components.binop.left_operand = FixDeclList($2); $$->components.binop.right_operand = FixExprList($4);} | YBEGIN error YEND {$$ = null;} ; /* Next lines dont work, somewhat obviously. begin_symbol: YBEGIN {} | '{' {} ; end_symbol: YEND {} | '}' {} ; */ executable_exprs: executable_expr { $$ = NewNode(EXPR_LIST_NODE, null, $1 ? $1->header.loc : EmptyLoc); $$->components.exprlist.expr = $1; $$ = InitExprList($$); } | executable_exprs ';' executable_expr { $$ = NewNode(EXPR_LIST_NODE, null, $1 ? $1->header.loc : EmptyLoc); $$->components.exprlist.expr = $3; $$ = AddToExprList($1,$$); } ; executable_expr: /* empty */ {$$ = null;} | assmnt_expr | if_then_stmt | foreach | while | functional_expr | return ; assmnt_expr: designator YASSMNT assmnt_or_expr %prec YASSMNT { $$ = NewNode(BINOP_NODE, YASSMNT, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } ; designator: selector_expr | index_expr | obj_name ; if_then_stmt: YIF expr YTHEN executable_exprs YEND {$$ = null;} | YIF expr YTHEN executable_exprs YELSE executable_exprs YEND {$$ = null;} ; foreach: YFOREACH '(' name_list YIN expr ')' executable_exprs YEND { $$ = NewNode(TRINOP_NODE, YFOREACH, $2.loc); $$->components.trinop.left_operand = $3; $$->components.trinop.middle_operand = $5; $$->components.trinop.right_operand = $7; } ; while: YWHILE '(' assmnt_or_expr ')' executable_exprs YEND {$$ = null;} ; return: YRETURN expr {$$ = null;} ; assmnt_or_expr: assmnt_expr | expr ; /* * NOTE: any changes to parts_spec should be reflected in ins_parts_spec below. */ parts_spec: parts_spec_1 | parts_spec_1 embedded_action_decls ; parts_spec_1: parts_spec_2 | parts_spec_1 or_op parts_spec_2 %prec YOR { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | parts_spec_1 embedded_action_decls or_op parts_spec_2 %prec YOR { $$ = $3; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $4; } ; parts_spec_2: /* empty */ {$$ = NIL;} | parts_spec_2 and_op parts_spec_2 %prec YAND { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | parts_spec_2 postfix_list_op %prec YUNYPLUS { if (isFullNameTypePair($1)) { $$ = $1; $2->components.unop.operand = $1->components.decl.kind.attr.value; $$->components.decl.kind.attr.value = $2; } else { $$ = $2; $$->components.unop.operand = $1; } } | /* * Conclusion as of 31mar04: It might be fine to have this, but I really don't * think it's necessary. The best argument against it is that I have never * really missed having in any spec yet written. * parts_spec_2 '[' Yinteger ']' %prec '[' { if (isFullNameTypePair($1)) { Node* n = NewNode(BINOP_NODE, YLIST, $2.loc); $$ = $1; n->components.binop.left_operand = $1->components.decl.kind.attr.value; n->components.binop.right_operand = $3; $$->components.decl.kind.attr.value = n; } else { $$ = NewNode(BINOP_NODE, YLIST, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } } | parts_spec_2 '[' Yinteger YDOTDOT Yinteger ']' %prec '[' { if (isFullNameTypePair($1)) { Node* n = NewNode(BINOP_NODE, YLIST, $2.loc); $$ = $1; n->components.binop.left_operand = $1->components.decl.kind.attr.value; n->components.binop.right_operand = $3; $$->components.decl.kind.attr.value = n; } else { $$ = NewNode(BINOP_NODE, YLIST, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } } | * */ op '(' sig_args_list ')' %prec YRTARROW { $$ = $1; $$->components.trinop.left_operand = $3; $$->components.trinop.middle_operand = null; $$->components.trinop.right_operand = (nodep) CurSymtab->ParentEntry; ExitOperation(null, null, startp, endp); } | /* op '(' sig_args_list ')' YRTARROW sig_arg %prec YRTARROW { $$ = $1; $$->components.binop.left_operand = $3; $$->components.binop.middle_operand = $6; EnterOpOutParm($6->components.decl.kind.initdecl.decl, $6->components.decl.kind.initdecl.islist); $$->components.binop.right_operand = (nodep) CurSymtab->ParentEntry; ExitOperation(null, null, startp, endp); } | */ op '(' sig_args_list ')' YRTARROW '(' sig_args_list_out ')' %prec YRTARROW { $$ = $1; $$->components.trinop.left_operand = $3; $$->components.trinop.middle_operand = $7; $$->components.trinop.right_operand = (nodep) CurSymtab->ParentEntry; ExitOperation(null, null, startp, endp); } | /* name_type_opt_pair { $$ = $1; $$->components.decl.next = null; } | */ name ':' '(' parts_spec_1 ')' { $$ = NewNode(DECL_NODE, ':', $2.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = ':'; $$->components.decl.kind.attr.value = $4; } | '(' parts_spec_1 ')' { $$ = $2; } /* * The following alternatives are for space-delimited YAND args and * embedded semantic actions. */ /* | parts_spec_2 embedded_action_decls {} */ | name_type_opt_pair_list { $$ = $1; $$->components.decl.next = null; } /* | parts_spec_2 or_op parts_spec_2 '{' action_decls '}' %prec YOR { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } */ /* | obj_atom {} -- Way too many conflicts */ /* * 16jan06 Update: Enabled this and did a key fix to typechk.c; not sure if * more needs to be done. Extant regression tests pass. * * The syntax from here to the end of the rule works fine grammatically, but * leads to semantics problems that need to be fixed before the syntax can be * (re-)enabled. See the 19oct99 entry in the implementation-ideas file for * further info. */ | Ystring { $$ = NewNode(ATOM_NODE, Ystring, $1.loc); $$->components.atom.val.string = $1.val; $$->components.atom.next = null; } | Yinteger { $$ = NewNode(ATOM_NODE,Yinteger, $1.loc); $$->components.atom.val.integer = $1.val; $$->components.atom.next = null; } | Yreal { $$ = NewNode(ATOM_NODE,Yreal, $1.loc); $$->components.atom.val.real = $1.val; $$->components.atom.next = null; } | Ynil { $$ = NewNode(ATOM_NODE,Ynil, $1.loc); $$->components.atom.val.nilval = 0; $$->components.atom.next = null; } ; op: YOP { $$ = NewNode(TRINOP_NODE, YRTARROW, $1.loc); EnterAnonOpName(anonopnum++); } | YFUNC { $$ = NewNode(TRINOP_NODE, YRTARROW, $1.loc); EnterAnonOpName(anonopnum++); } ; name_type_opt_pair_list: name_type_opt_pair_possibly_starred { $$ = $1; $$->components.decl.next = null; } | name_type_opt_pair_possibly_starred name_type_opt_pair_list { $$ = NewNode(BINOP_NODE, YAND, $1->header.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $2; } ; embedded_action_decls: '{' action_decls '}' { $$ = $2; } | '{' action_decls ';' '}' { $$ = $2; } ; and_op: YAND {$$ = NewNode(BINOP_NODE, YAND, $1.loc);} | ',' {$$ = NewNode(BINOP_NODE, YAND, $1.loc);} ; or_op: YOR {$$ = NewNode(BINOP_NODE, YOR, $1.loc);} | '|' {$$ = NewNode(BINOP_NODE, YOR, $1.loc);} ; postfix_list_op: '*' {$$ = NewNode(UNOP_NODE, YLIST, $1.loc);} ; value_spec: val_symbol name_type_pair '=' expr obj_body { $$ = $1; $$->components.decl.kind.obj.name = $2->components.decl.kind.attr.name; $$->components.decl.kind.obj.flags = isDef; EnterObjectName($$,$2); $$->components.decl.kind.obj.attrs = $5; /* Note: only subset of built-ins are valid. */ ProcessConcObjAttrs($$,$4,null); ExitObject($$, startp, endp); } ; /* * Parts of the more involved version of where, which includes both op sig * requirements and requirement satisfaction equations, have been commented * out. */ where: where_symbol ':' where_list ';' { $$ = NewNode(DECL_NODE, YWHERE, $2.loc); $$->components.decl.kind.where = FixDeclList($3); } ; where_list: /* empty */ {$$ = NIL;} | where_item {$$ = InitDeclList($1);} | where_list semi_or_comma where_item {$$ = AddToDeclList($1, $3);} ; where_item: /* op_signature | */ where_eq ; where_eq: name '=' name /* ins_parts_spec would be interesting */ { $$ = NewNode(DECL_NODE, '=', $2.loc); $$->components.decl.kind.eq.left_operand = $1; $$->components.decl.kind.eq.right_operand = $3; } ; ops: ops_symbol ':' op_signatures ';' { $$ = NewNode(DECL_NODE, YOPS, $2.loc); $$->components.decl.kind.opsig.list = FixDeclList($3); } ; inputs: in_symbol ':' inputs_list { $$ = NewNode(DECL_NODE, YINPUTS, $2.loc); $$->components.decl.kind.ins = $3; } ; outputs: out_symbol ':' outputs_list { $$ = NewNode(DECL_NODE, YOUTPUTS, $2.loc); $$->components.decl.kind.outs = $3; } ; op_signatures: /* empty */ {$$ = NIL;} | op_signature {$$ = InitDeclList($1);} | op_signatures semi_or_comma op_signature {$$ = AddToDeclList($1, $3);} ; semi_or_comma: ',' {$$ = null;} | ';' {$$ = null;} /* | YAND {$$ = null;} */ ; op_signature: op_name { $$ = NewNode(DECL_NODE, YOPS, $1->header.loc); $$->components.decl.kind.opsig.name = $1; $$->components.decl.kind.opsig.ins = null; $$->components.decl.kind.opsig.outs = null; } | op_sig_name op_parms { $$ = $2; $$->components.decl.kind.opsig.name = $1; ExitOperation(null, null, startp, endp); } | op_sig_name ':' op_parms { $$ = $3; $$->components.decl.kind.opsig.name = $1; ExitOperation(null, null, startp, endp); } ; op_sig_name: op_name { EnterOpName($1); } ; op_parms: /* */ YIS { $$ = null; } | /* */ '(' sig_args_list ')' YRTARROW '(' sig_args_list_out ')' { $$ = NewNode(DECL_NODE, YRTARROW, $1.loc); $$->components.decl.kind.opsig.ins = $2; $$->components.decl.kind.opsig.outs = $6; } | '(' sig_args_list ')' YRTARROW sig_arg { $$ = NewNode(DECL_NODE, YRTARROW, $1.loc); $$->components.decl.kind.opsig.ins = $2; $$->components.decl.kind.opsig.outs = $5; EnterOpOutParm($5->components.decl.kind.initdecl.decl, $5->components.decl.kind.initdecl.islist); } | '(' sig_args_list ')' { $$ = NewNode(DECL_NODE, YRTARROW, $1.loc); $$->components.decl.kind.opsig.ins = $2; $$->components.decl.kind.opsig.outs = null; } ; name_obj_list: /* empty */ {$$ = NIL;} | name_obj_pair {$$ = InitDeclList($1);} | name_obj_list ',' name_obj_pair {$$ = AddToDeclList($1, $3);} ; inputs_list: {inParts = true;} ins_parts_spec {$$ = $2; inParts = false;} ; outputs_list: {inParts = true;} outs_parts_spec {$$ = $2; inParts = false;} ; parts: parts_symbol ':' {inParts = true;} parts_spec { /* BuildCompType($3); */ ExitRecord($1); /* NOTE -- $1 here must change! */ /* NOTE: the preceding comment appears to be * crap. */ $$ = NewNode(DECL_NODE, YPARTS, $2.loc); $$->components.decl.kind.parts = $4; inParts = false; } /* | parts_symbol ':' error { $$=null; } */ ; /* * The following note is rather out of date, in so far as an ins_parts_spec is * a significantly reduced version of a parts spec. In particular, no ORs or * nesting via parens are allowed in an ins_parts_spec. * * NOTE: any changes to in_parts_spec should be reflected in parts_spec above. * ins_parts_spec is the same as parts_spec, except that name_type_opt_pair is * replaced with init_name_type_pair. */ ins_parts_spec: /* empty */ {$$ = NIL;} | ins_parts_spec and_op ins_parts_spec %prec YAND { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | init_name_type_pair postfix_list_op %prec YUNYPLUS { $$ = $2; $$->components.unop.operand = $1; EnterOpInParm($1->components.decl.kind.initdecl.decl, true); } | init_name_type_pair { $$ = $1; $$->components.decl.next = null; EnterOpInParm($1->components.decl.kind.initdecl.decl, false); } ; /* * Clone of ins_parts_spec. Only diff is call of EnterOpOutParm instead of * EnterOpInParm. Clearly this could be cleaner -- here cum da rewrite. */ outs_parts_spec: /* empty */ {$$ = NIL;} | outs_parts_spec and_op outs_parts_spec %prec YAND { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | init_name_type_pair postfix_list_op %prec YUNYPLUS { $$ = $1; $$->components.decl.kind.initdecl.islist = true; EnterOpOutParm($1->components.decl.kind.initdecl.decl, true); } | init_name_type_pair { $$ = $1; $$->components.decl.next = null; EnterOpOutParm($1->components.decl.kind.initdecl.decl, false); } ; obj_attributes: obj_attribute {$$ = InitDeclList($1);} | obj_attributes obj_attribute {$$ = AddToDeclList($1, $2);} ; obj_attribute: /* ';' {$$ = null;} | */ parts ';' | parts error ';' {$$ = null;} | where | ops | eqns | actions | attr_name attr_colon ';' { nodep newnd; $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = (newnd = NewNode(ATOM_NODE,Ytext, $2->header.loc)); newnd->components.atom.val.string = GetLastComment(); newnd->components.atom.next = null; inAttribute = false; } | attr_name attr_colon Ytext ';' { nodep newnd; $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = (newnd = NewNode(ATOM_NODE,Ytext,$3.loc)); newnd->components.atom.val.string = $3.val; newnd->components.atom.next = null; inAttribute = false; } | attr_name ':' name_list ';' { nodep newnd; $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = FixAtomList($3); inAttribute = false; } | /* * Enable list when we want to deal with rlink and dlink attributes. * attr_name ':' string_list ';' | * */ attr_name ':' expr ';' { nodep newnd; $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = $3; inAttribute = false; } | attr_name ':' begin_block ';' { nodep newnd; $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = $3; inAttribute = false; } ; /* * Enable list when we want to deal with rlink and dlink attributes. * string_list: Ystring | string_list ',' Ystring ; * */ attr_colon: ':' { inAttribute = true; /* ClearComment(); -- now done in lex.l:SetIdent */ $$ = NewNode(ATOM_NODE, ':', $1.loc); $$->components.atom.next = null; } ; attr_name: Yattr { /* inAttribute = true; * See 5dec97 entry LOG for why this is gone now. */ $$ = NewNode(ATOM_NODE, Yattr, $1.loc); $$->components.atom.val.text = stralloc($1.text); $$->components.atom.next = null; } ; op_attributes: op_attribute {$$ = InitDeclList($1);} | op_attributes op_attribute {$$ = AddToDeclList($1, $2);} ; op_attribute: parts ';' | inputs ';' | outputs ';' | precond ';' | postcond ';' | dataflow ';' | attr_name attr_colon ';' { nodep newnd; $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = (newnd = NewNode(ATOM_NODE,Ytext, $2->header.loc)); newnd->components.atom.val.string = GetLastComment(); newnd->components.atom.next = null; inAttribute = false; } | attr_name ':' Ytext ';' { nodep newnd; $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = (newnd = NewNode(ATOM_NODE,Ytext,$3.loc)); newnd->components.atom.val.string = $3.val; newnd->components.atom.next = null; inAttribute = false; } | attr_name ':' name_list ';' { nodep newnd; $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = FixAtomList($3); inAttribute = false; } | attr_name ':' expr ';' { nodep newnd; $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = $3; inAttribute = false; } | attr_name ':' begin_block ';' { nodep newnd; $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = $3; inAttribute = false; } ; name_type_pair: obj_name { $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = null; } | name ':' obj_name { $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = $3; } ; name_type_opt_pair_possibly_starred: name_type_opt_pair | name_type_opt_pair postfix_list_op %prec YUNYPLUS { if (isFullNameTypePair($1)) { $$ = $1; $2->components.unop.operand = $1->components.decl.kind.attr.value; $$->components.decl.kind.attr.value = $2; } else { $$ = $2; $$->components.unop.operand = $1; } } ; name_type_opt_pair: obj_name { $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = null; } | obj_name '=' expr { $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = null; $$->components.decl.kind.attr.initvalue = $3; } /* | name ':' { $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = ':'; $$->components.decl.kind.attr.value = null; } */ | name ':' obj_name { $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = $3; } /**/ | name ':' obj_name '=' expr { $$ = NewNode(DECL_NODE, ':', $1->header.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = $3; $$->components.decl.kind.attr.initvalue = $5; } /* */ ; name_obj_pair: name_list ':' name { $$ = NewNode(DECL_NODE, ':', $2.loc); $$->components.decl.kind.attr.name = FixAtomList($1); $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = $3; EnterVars($$->components.decl.kind.attr.name, BuildCompType1($3)); } ; init_name_type_pair: name_type_pair { $$ = NewNode(DECL_NODE, YASSMNT, $1->header.loc); $$->components.decl.kind.initdecl.decl = $1; $$->components.decl.kind.initdecl.init = null; } | name_type_pair YASSMNT obj_expr { $$ = NewNode(DECL_NODE, YASSMNT, $1->header.loc); $$->components.decl.kind.initdecl.decl = $1; $$->components.decl.kind.initdecl.init = $3; } ; module_name: name ; module_name_ender: /* empty */ { $$ = NULL; /* Browser: */ addSpecToList(); } | name { /* Browser: */ addSpecToList(); } ; class_name_list: class_name {$$ = InitAtomList2($1);} | class_name_list ',' class_name {$$ = AddToAtomList2($1, $3);} ; class_name: qualident ; obj_name: qualident | Ysymlit { $$ = NewNode(ATOM_NODE, Ysymlit, $1.loc); $$->components.atom.val.symlit = $1.val; $$->components.atom.next = null; } ; qualident : name {$$ = $1; } | name '.' qualident {$1->components.atom.next = $3; } ; name_ender: /* empty */ { $$ = NULL; } | name ; op_name: name | Ystring { $$ = NewNode(ATOM_NODE, Yident, $1.loc); $$->components.atom.val.text = $1.val; $$->components.atom.next = null; } ; op_name_enter: name { EnterOpName($1); } | Ystring { $$ = NewNode(ATOM_NODE, Yident, $1.loc); $$->components.atom.val.text = $1.val; $$->components.atom.next = null; EnterOpName($$); } ; op_name_ender: /* empty */ {$$ = NULL;} | op_name ; formal_decl: var_decl ';' {$$ = $1;} | ax_decl ';' {$$ = $1; ExitFormalDecl($$);} | thm_decl ';' {$$ = $1; ExitFormalDecl($$);} ; var_decls: var_decl {$$ = InitDeclList($1);} | var_decls ';' var_decl {$$ = AddToDeclList($1, $3);} ; var_decl: var_symbol name_list ':' obj_name { $$ = NewNode(DECL_NODE, YVAR, $3.loc); $$->components.decl.kind.var.vars = FixAtomList($2); $$->components.decl.kind.var.type = BuildAtomType($4); EnterVars($$->components.decl.kind.var.vars, $$->components.decl.kind.var.type); } /* 19jan06 TODO: Make sure semantics of this is properly type checked. */ | var_symbol name_list ':' name '=' expr { $$ = NewNode(DECL_NODE, YVAR, $3.loc); $$->components.decl.kind.var.vars = FixAtomList($2); $$->components.decl.kind.var.type = BuildAtomType($4); EnterVars($$->components.decl.kind.var.vars, $$->components.decl.kind.var.type); } /* */ ; precond: pre_symbol ':' { $$ = NewNode(DECL_NODE, YPRE, $2.loc); $$->components.decl.kind.pre.expr = null; ExitPostcond(null); } | pre_symbol ':' expr { $$ = NewNode(DECL_NODE, YPRE, $2.loc); $$->components.decl.kind.pre.expr = $3; ExitPrecond($$); } | pre_symbol error {$$ = null;} ; postcond: post_symbol ':' { $$ = NewNode(DECL_NODE, YPOST, $2.loc); $$->components.decl.kind.post.expr = null; ExitPostcond(null); } | post_symbol ':' expr { $$ = NewNode(DECL_NODE, YPOST, $2.loc); $$->components.decl.kind.post.expr = $3; ExitPostcond($$); } | post_symbol error {$$ = null;} ; dataflow: dataflow_symbol ':' connection_list {$$ = null;} ; connection_list: connection | connection_list ',' connection ; connection: connection_designator YRTARROW connection_designator /* OLD: name '.' name YRTARROW name '.' name | name YRTARROW name '.' name | name '.' name YRTARROW name | name YRTARROW name */ ; /* NOTE: this separate rule for connection_designator is defined in addition to * designator because using designator in the connection syntax causes 5 * reduce/reduce errors, stemming from fact that designator appears recursively * within selector_exprs and index_exprs, which in turn leads ultimately to a * conflict in the area of assmnt_or_expr. It's complicated, but this extra * def of connection_designator deals with the problem just fine. * * Well, as it turns out, connection_designator really needs to have more stuff * in it anyway, but the above comment is useful for general grammar debugging * purposes. */ connection_designator: expr | YISA {$$ = NewNode(UNOP_NODE, '?', $1.loc);} /* The following is not necessary syntactically, but left here for historical * understanding: * selector_expr | index_expr | name * */ ; expr: let | lambda | /* * OK, we've decided not to have standard assignments, but always require let. * designator YASSMNT expr %prec YASSMNT { $$ = NewNode(BINOP_NODE, YASSMNT, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | * */ expr YAND expr %prec YAND { $$ = NewNode(BINOP_NODE, YAND, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | expr YOR expr %prec YOR { $$ = NewNode(BINOP_NODE, YOR, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | expr YXOR expr %prec YXOR { $$ = NewNode(BINOP_NODE, YXOR, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | expr YIMPLIES expr %prec YIMPLIES { $$ = NewNode(BINOP_NODE, YIMPLIES, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | expr YIFF expr %prec YIFF { $$ = NewNode(BINOP_NODE, YIFF, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | YNOT expr %prec YNOT { $$ = NewNode(UNOP_NODE, YNOT, $1.loc); $$->components.unop.operand = $2; } | YIF expr YTHEN expr %prec YIF { $$ = NewNode(TRINOP_NODE, YIF, $1.loc); $$->components.trinop.left_operand = $2; $$->components.trinop.middle_operand = $4; $$->components.trinop.right_operand = null; } | YIF expr YTHEN expr YELSE expr %prec YIF { $$ = NewNode(TRINOP_NODE, YIF, $1.loc); $$->components.trinop.left_operand = $2; $$->components.trinop.middle_operand = $4; $$->components.trinop.right_operand = $6; } | forall '(' name_obj_list ')' expr %prec YFORALL { $$->components.decl.kind.quant.vars = FixDeclList($3); $$->components.decl.kind.quant.expr = $5; ExitQuant($$); } | forall '(' name YIN expr ')' expr %prec YFORALL { nodep n; $$->components.decl.kind.quant.vars = $3; $$->components.decl.kind.quant.in = n = NewNode(UNOP_NODE, YIN, $4.loc); n->components.unop.operand = $5; $$->components.decl.kind.quant.expr = $7; ExitQuant($$); } | forall '(' name_obj_list '|' expr ')' expr %prec YFORALL { nodep n; $$->components.decl.kind.quant.vars = FixAtomList($3); $$->components.decl.kind.quant.in = n = NewNode(UNOP_NODE, '|', $4.loc); n->components.unop.operand = $5; $$->components.decl.kind.quant.expr = $7; ExitQuant($$); } | exists '(' name_obj_list ')' expr %prec YEXISTS { $$->components.decl.kind.quant.vars = FixDeclList($3); $$->components.decl.kind.quant.expr = $5; ExitQuant($$); } | exists '(' name YIN expr ')' expr %prec YEXISTS { nodep n; $$->components.decl.kind.quant.vars = $3; $$->components.decl.kind.quant.in = n = NewNode(UNOP_NODE, YIN, $4.loc); n->components.unop.operand = $5; $$->components.decl.kind.quant.expr = $7; ExitQuant($$); } | exists '(' name_obj_list '|' expr ')' expr %prec YEXISTS { nodep n; $$->components.decl.kind.quant.vars = FixAtomList($3); $$->components.decl.kind.quant.in = n = NewNode(UNOP_NODE, '|', $4.loc); n->components.unop.operand = $5; $$->components.decl.kind.quant.expr = $7; ExitQuant($$); } | rel_expr ; let: YLET name_list '=' expr { $$ = NewNode(DECL_NODE, YLET, $1.loc); $$->components.decl.kind.let.names = FixAtomList($2); $$->components.decl.kind.let.expr = $4; $$->components.decl.kind.let.type = null; } | YLET name ':' name '=' expr { $$ = NewNode(DECL_NODE, YLET, $1.loc); $$->components.decl.kind.let.names = $2; $$->components.decl.kind.let.expr = $6; $$->components.decl.kind.let.type = $4; } ; expr_list: /* empty */ {$$ = null;} | exprlelem {$$ = InitExprList($1);} | expr_list ',' exprlelem {$$ = AddToExprList($1,$3);} ; exprlelem: /* empty {$$ = null;} | */ expr { $$ = NewNode(EXPR_LIST_NODE, null, $1->header.loc); $$->components.exprlist.expr = $1; $$->components.exprlist.next = null; } ; expr_list_with_empties: exprlelem_possibly_empty {$$ = InitExprList($1);} | expr_list ',' exprlelem_possibly_empty {$$ = AddToExprList($1,$3);} ; exprlelem_possibly_empty: /* empty */ {$$ = null;} | expr { $$ = NewNode(EXPR_LIST_NODE, null, $1->header.loc); $$->components.exprlist.expr = $1; $$->components.exprlist.next = null; } ; expr_seq: /* empty {$$ = null;} | */ expr_seq_elem {$$ = InitExprList($1);} | expr_seq ';' expr_seq_elem {$$ = AddToExprList($1,$3);} ; expr_seq_elem: /* empty */ {$$ = null;} | expr { if (not $1) $$ = null; else { $$ = NewNode(EXPR_LIST_NODE, null, $1->header.loc); $$->components.exprlist.expr = $1; $$->components.exprlist.next = null; } } ; lambda: YLAMBDA '(' sig_args_list ')' YRTARROW '(' sig_args_list ')' expr { $$ = NewNode(TRINOP_NODE, YLAMBDA, $1.loc); $$->components.trinop.left_operand = $3; $$->components.trinop.middle_operand = $7; $$->components.trinop.right_operand = $9; } /* * Next alternative causes abundant s/r conflicts -- we can live * without it. * | YLAMBDA '(' sig_args_list ')' YRTARROW sig_arg expr * */ ; forall: YFORALL { $$ = NewNode(DECL_NODE, YFORALL, $1.loc); EnterQuant(); } ; exists: exists_symbol { EnterQuant(); } ; rel_expr: expr rel_bin_op expr %prec '=' { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | name almost_eq_op expr YEXCEPT except_item { nodep newnd; $$ = $2; $$->components.trinop.left_operand = $1; $$->components.trinop.middle_operand = $3; newnd = $$->components.trinop.right_operand = NewNode(EXPR_LIST_NODE, null, $1 ? $1->header.loc : EmptyLoc); newnd->components.exprlist.expr = $5; newnd->components.exprlist.next = null; } | name almost_eq_op expr YEXCEPT '(' except_list ')' { $$ = $2; $$->components.trinop.left_operand = $1; $$->components.trinop.middle_operand = $3; $$->components.trinop.right_operand = FixExprList($6); } | arith_expr ; except_list: except_item { $$ = NewNode(EXPR_LIST_NODE, null, $1 ? $1->header.loc : EmptyLoc); $$->components.exprlist.expr = $1; $$ = InitExprList($$);} | except_list ',' except_item { $$ = NewNode(EXPR_LIST_NODE, null, $3 ? $3->header.loc : EmptyLoc); $$->components.exprlist.expr = $3; $$ = AddToExprList($1,$$);} ; except_item: selector_expr '=' expr %prec '=' { $$ = NewNode(BINOP_NODE, '=', $1->header.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } ; arith_expr: arith_expr arith_add_op arith_expr %prec '+' { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | arith_expr arith_mult_op arith_expr %prec '*' { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | arith_expr arith_exp_op arith_expr %prec '^' { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | length_pre_op arith_expr %prec '#' { $$ = $1; $$->components.unop.operand = $2; } | arith_pre_op arith_expr %prec YUNYPLUS { $$ = $1; $$->components.unop.operand = $2; } | selector_expr | index_expr | functional_expr | obj_atom | '[' expr YDOTDOT expr ']' { $$ = NewNode(BINOP_NODE, YDOTDOT, $1.loc); $$->components.binop.left_operand = $2; $$->components.binop.right_operand = $4; } | '[' expr_list ']' { /* Note use of ']'. It's the name for list constructor /* node wherease '[' is name for list ref node */ $$ = NewNode(UNOP_NODE, ']', $1.loc); $$->components.unop.operand = FixExprList($2); } | '{' expr_list_with_empties '}' { $$ = NewNode(UNOP_NODE, '}', $1.loc); $$->components.unop.operand = FixExprList($2); } | '(' expr_seq ')' {$$ = FixExprList($2);} ; selector_expr: arith_expr select_op name %prec '.' { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } /* * 16jan06 Update: Enabled this and extant regression tests pass. Still need * to add some new testing. */ | arith_expr select_op const_val %prec '.' { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | arith_expr select_op name '#' Yinteger {} | arith_expr select_op const_val '#' Yinteger {} | arith_expr '#' Yinteger {} | arith_expr YPOUNDPOUND {} | arith_expr '#' Yinteger YDOTDOT Yinteger %prec YDOTDOT {} | arith_expr '#' Yinteger YDOTDOT YPOUNDPOUND {} | arith_expr YATTRSELECT attr_name { $$ = NewNode(BINOP_NODE, YATTRSELECT, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; inAttribute = false; } ; /* * Same here. Hmm, to be clean, should we put symlit in here and remove it as * a RHS element of obj_name and obj_atom? Or should we put symlit here, but * not remove it as a RHS element elsewhere? Good questions, these. */ const_val: Ystring { $$ = NewNode(ATOM_NODE, Ystring, $1.loc); $$->components.atom.val.string = $1.val; $$->components.atom.next = null; } | Yinteger { $$ = NewNode(ATOM_NODE,Yinteger, $1.loc); $$->components.atom.val.integer = $1.val; $$->components.atom.next = null; } | Yreal { $$ = NewNode(ATOM_NODE,Yreal, $1.loc); $$->components.atom.val.real = $1.val; $$->components.atom.next = null; } ; index_expr: arith_expr '[' expr ']' %prec '[' { $$ = NewNode(BINOP_NODE, '[', $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | arith_expr '[' expr YDOTDOT expr ']' %prec '[' { $$ = NewNode(TRINOP_NODE, '[', $2.loc); $$->components.trinop.left_operand = $1; $$->components.trinop.middle_operand = $3; $$->components.trinop.right_operand = $5; } /* IMPORTANT NOTE: Phase out the next RHS alt; it's just here now for backwards compat. */ | arith_expr '[' expr ':' expr ']' %prec '[' { $$ = NewNode(TRINOP_NODE, '[', $2.loc); $$->components.trinop.left_operand = $1; $$->components.trinop.middle_operand = $3; $$->components.trinop.right_operand = $5; } ; functional_expr: arith_expr '(' op_args ')' { $$ = NewNode(PROC_CALL_NODE, null, $1 ? $1->header.loc : EmptyLoc); $$->components.proccall.desig = $1; $$->components.proccall.actuals = $3; } | arith_expr '(' op_args ')' YQRTARROW '(' op_args ')' { $$ = NewNode(TRINOP_NODE, YQRTARROW, $1 ? $1->header.loc : EmptyLoc); $$->components.trinop.left_operand = $1; $$->components.trinop.middle_operand = $3; $$->components.trinop.right_operand = $7; } /* * Oh well | Yattr '(' op_args ')' { $$ = null; } * */ ; op_args: /* empty */ {$$ = NIL;} | op_arg {$$ = $1;} | op_arg ',' op_args { $1->components.exprlist.next = $3; $$ = $1; } ; sig_args_list: {inParts = true;} ins_parts_spec {$$ = $2; inParts = false;} ; sig_args_list_out: {inParts = true;} outs_parts_spec {$$ = $2; inParts = false;} ; sig_arg: init_name_type_pair { $$ = $1; $$->components.decl.next = null; } | init_name_type_pair postfix_list_op %prec YUNYPLUS { $$ = $1; $$->components.decl.kind.initdecl.islist = true; $$->components.decl.next = null; } ; op_arg: expr { $$ = NewNode(EXPR_LIST_NODE, null, $1 ? $1->header.loc : EmptyLoc); $$->components.exprlist.expr = $1; $$->components.exprlist.next = null; } ; rel_bin_op: '=' {$$ = NewNode(BINOP_NODE, '=', $1.loc);} | '<' {$$ = NewNode(BINOP_NODE, '<', $1.loc);} | '>' {$$ = NewNode(BINOP_NODE, '>', $1.loc);} | YNEQ {$$ = NewNode(BINOP_NODE, YNEQ, $1.loc);} | YLEQ {$$ = NewNode(BINOP_NODE, YLEQ, $1.loc);} | YGEQ {$$ = NewNode(BINOP_NODE, YGEQ, $1.loc);} | YIN {$$ = NewNode(BINOP_NODE, YIN, $1.loc);} ; almost_eq_op: YAEQ {$$ = NewNode(BINOP_NODE, YAEQ, $1.loc);} ; arith_add_op: '+' {$$ = NewNode(BINOP_NODE, '+', $1.loc);} | '-' {$$ = NewNode(BINOP_NODE, '-', $1.loc);} ; arith_mult_op: '*' {$$ = NewNode(BINOP_NODE, '*', $1.loc);} | '/' {$$ = NewNode(BINOP_NODE, '/', $1.loc);} | YMOD {$$ = NewNode(BINOP_NODE, YMOD, $1.loc);} ; arith_exp_op: '^' {$$ = NewNode(BINOP_NODE, '^', $1.loc);} ; length_pre_op: '#' {$$ = NewNode(UNOP_NODE, '#', $1.loc);} ; arith_pre_op: '+' {$$ = NewNode(UNOP_NODE, YUNYPLUS, $1.loc);} | '-' {$$ = NewNode(UNOP_NODE, YUNYMINUS, $1.loc);} ; select_op: '.' {$$ = NewNode(BINOP_NODE, '.', $1.loc);} | YISA %prec '.' {$$ = NewNode(BINOP_NODE, YISA, $1.loc);} | YGETINSTANCE {$$ = NewNode(BINOP_NODE, YGETINSTANCE, $1.loc);} | YCHKINSTANCE {$$ = NewNode(BINOP_NODE, YCHKINSTANCE, $1.loc);} ; eqns: eqns_symbol ':' eqn_decls ';' { $$ = NewNode(DECL_NODE, YEQUATIONS, $2.loc); $$->components.decl.kind.eqns.vars = null; $$->components.decl.kind.eqns.eqns = FixDeclList($3); $$->components.decl.kind.eqns.symtab = null; } | eqns_symbol ':' {EnterEqns();} var_decls ';' eqn_decls ';' { $$ = $1; $$->components.decl.kind.eqns.vars = FixDeclList($4); $$->components.decl.kind.eqns.eqns = FixDeclList($6); ExitEqns($$); } | eqns_symbol error {$$ = null;} ; eqn_decls: /* empty */ {$$ = NIL;} | eqn_decl {$$ = InitDeclList($1);} | eqn_decls ';' eqn_decl {$$ = AddToDeclList($1, $3);} ; eqn_decl: lhs YEQEQ rhs { $$=NewNode(DECL_NODE, YEQEQ, $2.loc); $$->components.decl.kind.eqn.lhs = $1; $$->components.decl.kind.eqn.rhs = $3; } ; lhs: functional_expr ; rhs: expr ; actions: actions_symbol ':' action_decls ';' { $$ = NewNode(DECL_NODE, YACTIONS, $2.loc); $$->components.decl.kind.actions = FixDeclList($3); } | actions_symbol error {$$ = null;} ; action_decls: /* empty */ {$$ = NIL;} | action_decl {$$ = InitDeclList($1);} | action_decls ';' action_decl {$$ = AddToDeclList($1, $3);} ; action_decl: action_lhs YEQEQ action_rhs { $$=NewNode(DECL_NODE, YEQEQ, $2.loc); $$->components.decl.kind.eqn.lhs = $1; $$->components.decl.kind.eqn.rhs = $3; } ; action_lhs: name YATTRSELECT attr_name { $$=NewNode(BINOP_NODE, YATTRSELECT, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.left_operand = $3; } | name '.' attr_name { $$=NewNode(BINOP_NODE, YATTRSELECT, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.left_operand = $3; } | name /* For global attributes */ { $$=NewNode(BINOP_NODE, YATTRSELECT, $1->header.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = null; } ; action_rhs: expr ; /* * Removed this def altogether to allow keywordless obj decls. * ax_decls: ax_decl {$$ = InitDeclList($1);} | ax_decls ';' ax_decl {$$ = AddToDeclList($1, $3);} ; */ ax_decl: ax_symbol expr { $$ = NewNode(DECL_NODE, YAX, $2->header.loc); $$->components.decl.kind.formaldef.expr = $2; } /* */ | ax_symbol Yident ':' expr { $$ = NewNode(DECL_NODE, YAX, $4->header.loc); $$->components.decl.kind.formaldef.expr = $4; } /* */ ; /* * Removed this def altogether to allow keywordless obj decls. * thm_decls: thm_decl {$$ = InitDeclList($1);} | thm_decls ';' thm_decl {$$ = AddToDeclList($1, $3);} ; */ thm_decl: thm_symbol expr { $$ = NewNode(DECL_NODE, YTHM, $2->header.loc); $$->components.decl.kind.formaldef.expr = $2; } ; obj_expr: /* expr*/ /* name | */ obj_atom | '[' ']' { $$ = NewNode(ATOM_NODE, Ynil, $1.loc); $$->components.atom.next = null; } | '[' obj_expr_list ']' {$$ = FixObjList($2);} ; obj_expr_list: obj_expr { nodep head; head = InitObjList(NewNode(ATOM_NODE,YLIST, $1->header.loc)); $$ = AddToObjList(head, $1); } | obj_expr_list ',' obj_expr {$$ = AddToObjList($1, $3); } ; obj_atom: Ystring { $$ = NewNode(ATOM_NODE, Ystring, $1.loc); $$->components.atom.val.string = $1.val; $$->components.atom.next = null; } | Yinteger { $$ = NewNode(ATOM_NODE,Yinteger, $1.loc); $$->components.atom.val.integer = $1.val; $$->components.atom.next = null; } | Yreal { $$ = NewNode(ATOM_NODE,Yreal, $1.loc); $$->components.atom.val.real = $1.val; $$->components.atom.next = null; } | Ysymlit { $$ = NewNode(ATOM_NODE,Ysymlit, $1.loc); $$->components.atom.val.symlit = $1.val; $$->components.atom.next = null; } | Ynil { $$ = NewNode(ATOM_NODE,Ynil, $1.loc); $$->components.atom.val.nilval = 0; $$->components.atom.next = null; } | name /* if (identis($1, PROC)) $$ = NewNode(T_PCALL, yyline, $1, NIL); else $$ = setupvar($1, NIL); */ ; name_list: name {$$ = InitAtomList($1);} | name_list ',' name {$$ = AddToAtomList($1, $3);} /* | '(' name_list ',' name ')' {$$ = AddToAtomList($2, $4);} */ ; /* * Phase 1 ANTLR translation of the preceding rule (still uses recursion): name_list: n:name {#name_list = InitAtomList(#n);} | nl:name_list "," n:name {#name_list = AddToAtomList(#nl, #n);} | "(" nl:name_list "," n:name ")" {#name_list = AddToAtomList(#nl, #n);} ; * * Phase 2 ANTLR translation of the preceding rule (recursion removed): * name_list: n1:name ( "," n2:name )* {-- Figure out ANTLR's list-building action idiom --} ; * */ name: Yident { $$ = NewNode(ATOM_NODE, Yident, $1.loc); $$->components.atom.val.text = $1.text; $$->components.atom.next = null; } /* | Yident '.' name { $$ = NewNode(ATOM_NODE, Yident, $1.loc); $$->components.atom.val.text = $1.text; $$->components.atom.next = $3; } */ ; attr_defs: attr_def {$$ = null;} | attr_defs ';' attr_def {$$ = null;} ; attr_def: attr_def1 ':' {inParts = true;} parts_spec {$$ = $1; inParts = false;} | attr_def1 ; attr_def1: YDEFINE obj_symbol YATTRIBUTE name_list { DefineAttrNames(FixAtomList($4)); $$ = null; } | YDEFINE op_symbol YATTRIBUTE name_list { DefineAttrNames(FixAtomList($4)); $$ = null; } | YDEFINE YATTRIBUTE name_list { DefineAttrNames(FixAtomList($3)); $$ = null; } ; obj_symbol: YOBJECT {$$ = NewNode(DECL_NODE, YOBJ, $1.loc);} | YOBJ {$$ = NewNode(DECL_NODE, YOBJ, $1.loc);} ; /* * */ val_symbol: YVALUE {$$ = NewNode(DECL_NODE, YOBJ, $1.loc);} | YVAL {$$ = NewNode(DECL_NODE, YOBJ, $1.loc);} ; /* * */ inheritsfrom_symbol: YINHERITS YFROM {$$ = null;} | YEXTENDS {$$ = null;} | '<' {$$ = null;} ; op_symbol: YOPERATION {$$ = NewNode(DECL_NODE, YOP, $1.loc);} | YOP {$$ = NewNode(DECL_NODE, YOP, $1.loc);} | YFUNCTION {$$ = NewNode(DECL_NODE, YOP, $1.loc);} | YFUNC {$$ = NewNode(DECL_NODE, YOP, $1.loc);} ; parts_symbol: YCOMPONENTS {EnterRecord(); $$ = NewNode(TYPE_NODE, YRECORD, $1.loc);} | YPARTS {EnterRecord(); $$ = NewNode(TYPE_NODE, YRECORD, $1.loc);} ; ops_symbol: YOPERATIONS {$$ = NULL;} | YOPS {$$ = NULL;} ; in_symbol: YINPUTS {$$ = NULL;} | YIN {$$ = NULL;} ; out_symbol: YOUTPUTS {$$ = NULL;} | YOUT {$$ = NULL;} ; var_symbol: YVARIABLE {$$ = NULL;} | YVAR {$$ = NULL;} ; eqns_symbol: YEQUATIONS {$$ = NewNode(DECL_NODE, YEQUATIONS, $1.loc);} ; actions_symbol: YACTIONS {$$ = NewNode(DECL_NODE, YACTIONS, $1.loc);} ; ax_symbol: YAXIOM {$$ = NULL; EnterFormalDecl("An Axiom");} | YAX {$$ = NULL; EnterFormalDecl("An Axiom");} ; thm_symbol: YTHEOREM {$$ = NULL; EnterFormalDecl("A Theorem");} | YTHM {$$ = NULL; EnterFormalDecl("A Theorem");} ; pre_symbol: YPRECONDITION {$$ = NULL; EnterPrecond();} | YPRE {$$ = NULL; EnterPrecond();} ; post_symbol: YPOSTCONDITION {$$ = NULL; EnterPostcond();} | YPOST {$$ = NULL; EnterPostcond();} ; dataflow_symbol: YDATAFLOW {$$ = NULL;} ; exists_symbol: YEXISTS {$$ = NewNode(DECL_NODE, YEXISTS, $1.loc);} ; where_symbol: YWHERE {$$ = null;} ; /* Piece of crap to get over ';' problems, temporarily, if not forever. */ /* Apparently not. */ /*semi_list:*/ /* empty */ /* {$$ = NULL;} | semi_list ';' {$$ = NULL;} ; */ %% /***********************/ /**** FUNCTIONS ****/ /***********************/ /* set debugging flags (if you like); call yyparse(); return parse tree */ nodep parser() { #ifdef YYDEBUG yydebug = 0; #endif PARSE_ERROR = false; inAttribute = false; inParts = false; if ((not yyparse()) and (not PARSE_ERROR)) return parsetree; else return null; } /* use default version in yacc paper, or fancy later */ yyerror(s) char *s; { SrcLoc loc; nodep t; anonopnum = 0; loc.line = yylineno; loc.col = yycharno; loc.file = yyfilename ? stralloc(yyfilename) : stralloc("stdin"); t = NewNode(null, null, loc); lerror(t, "\tsyntax error.\n"); PARSE_ERROR = true; /* * Hmm, this'll probably fix any nasty symtab problems, particularly if we * get stuck in a record symtab, which is a bit sparce. */ CurSymtab = Level0Symtab; }