/**** * * 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; #define YYERROR_VERBOSE 1 %} /* * 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 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 YREF '#' '(' ')' '*' '+' ',' '-' '.' '/' ':' ';' '<' '=' '>' '[' ']' '^' '{' '|' '}' '?' '@' /* * 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 '@' %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_obj_component const_val dataflow dataflow_symbol deref_pre_op 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: /* * 16oct07: The following keywordless alt for op_heading is possible with the * removal of YIS as a RHS for op_parms. */ op_name_enter op_parms { $$ = NewNode(DECL_NODE, YOP, $1->header.loc); $$->components.decl.kind.obj.name = $1; $$->components.decl.kind.obj.flags = 0; $$->components.decl.kind.obj.inheritsfrom = null; if ($2) { $$->components.decl.kind.op.ins = $2->components.decl.kind.opsig.ins; $$->components.decl.kind.op.outs = $2->components.decl.kind.opsig.outs; } } | /* */ 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; } | prefix_ref_op name %prec YUNYPLUS {$$ = $2;} | 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; } } | /* * Rethink as of 25oct07: Reasons to allow: (a) UML compat; (b) with the * re-enabling of consts in obj exprs, it makes some sense; (c) re. the 31mar04 * conclusion -- just because I've never used it doesn't mean that someone else * might not want it; in particular, I have had some 205/308 students ask about * it, on, as I recal, a number of occasions; (d) if it doesn't cause any * syntactic or semantic harm, preceding reasons (a) - (c) are good enough. * * 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 */ ; 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);} | '+' {$$ = 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; } /* */ /* */ | const_obj_component { $$ = 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 ':' const_obj_component { $$ = 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_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; } ; /* * * For now, the RHS subtrees built for each of these is of the type of the * literal. To be type-accurate, it needs to be "the T X", for T = the type of * the literal value X. * * Some history of allowing constants as obj components follows. The reference * to "It" and "this" in the history refer to the chunk of grammar that's now * the RHS of const_obj_component. * * 25-27oct07 Update: Moved RHS ref of const_obj_component into * name_type_opt_pair rule. Having it ref'd from the RHS of parts_spec_2 * caused a few problems which need not be fully expounded here, since they're * to do largely with vagaries of Yacc. Bottom line, const's as obj components * are now finally here to stay, though as of this writing, they're not yet * type checked as fully as they should be. * * 11nov06 Update: It blows type checker on Intell Mac, in both MacOS and * CYGWIN. Therefore, it's out again, until we get the semantics fully fixed. * * 16jan06 Update: Enabled this and did a quick 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. * * 25oct07: The following causes shift/reduce that is NOT OK: | Yident ':' const_obj_component { $$ = $3; } So the equivalent has been been moved to the name_type_opt_pair rule, q.v. */ const_obj_component: Ystring { $$ = NewNode(ATOM_NODE, Yident, $1.loc); $$->components.atom.val.text = hashsave("string"); $$->components.atom.next = null; } | Yinteger { $$ = NewNode(ATOM_NODE, Yident, $1.loc); $$->components.atom.val.text = hashsave("integer"); $$->components.atom.next = null; } | Yreal { $$ = NewNode(ATOM_NODE, Yident, $1.loc); $$->components.atom.val.text = hashsave("real"); $$->components.atom.next = null; } | Ynil { $$ = NewNode(ATOM_NODE, Yident, $1.loc); $$->components.atom.val.text = hashsave("nilType"); $$->components.atom.next = null; } ; 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 | '?' {$$ = 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_list YIN expr ')' expr %prec YFORALL { nodep n; $$->components.decl.kind.quant.vars = FixAtomList($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_list YAND 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; } | deref_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);} ; deref_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 YASSMNT action_rhs { $$=NewNode(DECL_NODE, YEQEQ, $2.loc); $$->components.decl.kind.eqn.lhs = $1; $$->components.decl.kind.eqn.rhs = $3; } | 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; } | thm_symbol Yident '=' expr { $$ = NewNode(DECL_NODE, YTHM, $4->header.loc); $$->components.decl.kind.formaldef.expr = $4; } ; 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 sparse. */ CurSymtab = Level0Symtab; }