/**** * * Yacc grammar for SpecL version 1.0. * */ /*** * 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" #include "token-mapping.h" int inAttribute; /* exported to lexer.l, q.v. */ int inParts; /* ditto */ int anonopnum; /* counter for anonymous op types */ int anonaxnum; /* counter for anonymous axioms */ int anonthmnum; /* counter for anonymous theorems */ bool input_parm; /* inherited attr, true if processing in parm */ char* name; /* inherited attr for axiom name */ 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; nodep dp; #define YYERROR_VERBOSE 1 %} /* * Start Symbol */ %start start /* * Terminal Symbols */ %token YEOF 0 %token AEQ AND ARROW ATTRIBUTE ATTRIBUTE_SELECT AX AXIOM BODY CHECK_INSTANCE CHECK_UNION COMPONENTS DATAFLOW DEFINE DESCRIPTION DIV DOTDOT ELSE END EQ EQEQ EQUATIONS EXCEPT EXISTS EXPORT EXTENDS FORALL FUNC FUNCTION GEQ GET_INSTANCE IF IFF IMPLIES IMPORT IN INCLUDE INPUTS IS LAMBDA LEQ LET MOD MODULE NEQ NOT OBJ OBJECT OP OPERATION OPERATIONS OPS OR OUT OUTPUTS PARENTS PARTS POST POSTCONDITION PRE PRECONDITION QARROW QUESTION_MARK_IDENTIFIER REF RULE SET THEN THEOREM THM UNYPLUS VAL VALUE VAR VARIABLE XOR '#' '(' ')' '*' '+' ',' '-' '.' '/' ':' ';' '<' '=' '>' '?' '[' ']' '^' '{' '|' '}' '@' /* * The following tokens are not used in the rules, but are used in the tree * or as parameters to tree-building functions. (Well, WHERE currently is * used, but is planned to be replaced with the proper implementation of * parameterized objects.) */ ACTIONS ARRAY CONST LIST RECORD TYPE WHERE /* * Non-Terminal cum Terminal Symbols */ %token IDENTIFIER %token ATTRIBUTE_IDENTIFIER %token INTEGER_LITERAL %token REAL_LITERAL %token STRING_LITERAL %token ATTRIBUTE_TEXT %token NIL_LITERAL /* * Operator Precedences */ %left ')' %left ']' %right SET %left LET %left FORALL EXISTS %left IF IFF IMPLIES %left OR XOR '|' /* or ops */ %left AND ',' /* and ops */ %left AEQ EXCEPT %left '=' NEQ '<' '>' LEQ GEQ /* relational ops */ %left IN %left DOTDOT %left '+' '-' /* add ops */ %left ';' /* expr seq op */ %left '*' '/' DIV MOD /* mult ops */ %left '^' /* exponentiation op */ %left '#' %left QRTARROW %left POUNDPOUND %left '.' CHECK_UNION GET_INSTANCE CHECK_INSTANCE ATTRIBUTE_SELECT /* selector ops */ %right '[' '{' %left UNARY_PLUS UNARY_MINUS NOT /* unary ops */ %right '(' /* * Non-Terminal Symbols */ %type action action_lhs action_rhs actions actual_parameter actual_parameters add_op almost_eq_op arithmetic_expression arithmetic_prefix_op attribute attribute_colon attribute_name axiom // axiom_expression_anonymous // axiom_heading axiom_name axiom_symbol boolean_expression callable_expression component_and_op component_or_op component_list_op component_operation_heading component_ref_op component_type_designator components components_base_element components_expression components_symbol condition connection connection_expression connections constructor_expression declaration declarations dereference_expression equation equations equations_symbol except_item except_items exists_symbol equation_sequence exp_op export exports expression expression_list expression_list_element expression_list_with_empties expression_possibly_empty expression_sequence expression_sequence_element extends_symbol forall_symbol import import_item import_items imports include index_expression in_paren inputs_symbol invocation lambda length_op let literal module module_heading mult_op name names object object_attribute object_attributes object_heading object_parameter object_parameters object_symbol operation operation_attribute operation_attributes operation_heading operation_name operation_name_optional_signature operation_names_optional_signatures operation_output operation_outputs operation_parameter operation_parameters operation_signature operation_symbol operations operations_symbol optional_attributes optional_name optional_semicolon out_paren outputs_symbol parents postcondition_symbol precondition_symbol qualified_name qualified_names quantifier_expression question_mark_name relational_expression relational_op rule rule_alternative rule_element rule_heading rule_rhs rule_terminal select_op selector_expression semicolon_or_comma semicolon_or_comma_or_and set simple_object_declaration simple_operation_declaration simple_variable simple_variables storage_designator theorem // theorem_expression_anonymous // theorem_heading theorem_name theorem_symbol top_level_expression top_level_item top_level_items type_designator type_name type_name_or_variable type_names type_names_or_variables untyped_attribute user_defined_attributes user_defined_attribute validation_invocation value value_symbol variable variable_symbol variable_type_designator where where_eq where_item where_list /* * Rules */ %% start: top_level_items { /* The follow-on processing is expecting an unfixed decl list, so we oblige here, and in the other top_level_item RHS elements. */ // parsetree = InitDeclList($1); parsetree = $1; YYACCEPT; } | YEOF { parsetree = null; YYACCEPT; } ; top_level_items: top_level_item { $$ = InitDeclList($1); } | top_level_items top_level_item { $$ = AddToDeclList($1, $2); } | top_level_item error { $$ = null; } ; top_level_item: declaration | top_level_expression ; declaration: /* empty { $$ = null; } | */ module | object ';' { $$ = $1; if (not PARSE_ERROR) { EnterObject($$); } } | operation ';' { $$ = $1; if (not PARSE_ERROR) { EnterOperation($$); } } | value ';' { $$ = $1; if (not PARSE_ERROR) { EnterObject($$); } } | variable ';' | axiom ';' | theorem ';' | attribute ';' | rule ';' { $$ = $1; if (not PARSE_ERROR) { EnterObject($$); } } | include ';' | error {$$ = null;} ; module: module_heading declarations END optional_name ';' { parsetree = $1; SetSpecUnitBody($$, $2); ExitModule($1); ChkEnder(GetModuleName($1), $4); } | module_heading END optional_name ';' { nodep n; $1->components.module.priority = null; /* * $1->components.module.imports = null; $1->components.module.exports = null; * */ $1->components.module.body = (n = NewNode(SPEC_NODE, null, loc($1))); n->components.spec.entities = null; parsetree = $1; ExitModule($1); ChkEnder($1->components.module.name, $3); } ; module_heading: MODULE name optional_semicolon { $$ = NewNode(MODULE_NODE, YOBJ, $1.loc); $$->components.module.name = $2; $$->components.module.imports = null; $$->components.module.exports = null; EnterModule($2, YMODULE); } | MODULE name optional_semicolon imports { $$ = NewNode(MODULE_NODE, YOBJ, $1.loc); $$->components.module.name = $2; $$->components.module.imports = $4; $$->components.module.exports = null; EnterModule($2, YMODULE); } | MODULE name optional_semicolon exports { $$ = NewNode(MODULE_NODE, YOBJ, $1.loc); $$->components.module.name = $2; $$->components.module.imports = null; $$->components.module.exports = $4; EnterModule($2, YMODULE); } | MODULE name optional_semicolon 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: IMPORT import_items ';' { $$ = NewNode(DECL_NODE, YIMPORT, $1.loc); $$->components.decl.kind.import.items = FixAtomList2($2); $$->components.decl.kind.import.isall = false; $$->components.decl.kind.import.except = null; } | IMPORT qualified_name '.' '*' ';' { $$ = NewNode(DECL_NODE, YIMPORT, $1.loc); $$->components.decl.kind.import.items = FixAtomList($2); $$->components.decl.kind.import.isall = true; $$->components.decl.kind.import.except = null; } | IMPORT qualified_name '.' '*' EXCEPT names ';' { $$ = NewNode(DECL_NODE, YIMPORT, $1.loc); $$->components.decl.kind.import.items = FixAtomList($2); $$->components.decl.kind.import.isall = true; $$->components.decl.kind.import.except = FixAtomList($6); } ; import_items: import_item {$$ = InitAtomList2($1);} | import_items ',' import_item {$$ = AddToAtomList2($1, $3);} ; import_item: qualified_name {$$ = FixAtomList($1);} ; exports: export { $$->components.decl.next = null; $$ = $1; } | export exports { $1->components.decl.next = $2; $$ = $1; } ; export: EXPORT names ';' { $$ = NewNode(DECL_NODE, YEXPORT, $1.loc); $$->components.decl.kind.export_.names = FixAtomList($2); $$->components.decl.kind.export_.isall = false; $$->components.decl.kind.export_.except = null; /*EnterExports($2, null);*/ } | EXPORT '*' ';' { $$ = NewNode(DECL_NODE, YEXPORT, $1.loc); $$->components.decl.kind.export_.names = null; $$->components.decl.kind.export_.isall = true; $$->components.decl.kind.export_.except = null; /*EnterExports($2, null);*/ } | EXPORT '*' EXCEPT names ';' { $$ = NewNode(DECL_NODE, YEXPORT, $1.loc); $$->components.decl.kind.export_.names = null; $$->components.decl.kind.export_.isall = true; $$->components.decl.kind.export_.except = FixAtomList($4); /*EnterExports($2, null);*/ } ; declarations: declaration { $$ = InitDeclList($1); } | declarations declaration { $$ = AddToDeclList($1, $2); } ; object: simple_object_declaration { $$ = $1; $$->components.decl.kind.obj.ops = null; $$->components.decl.kind.obj.eqns = null; $$->components.decl.kind.obj.attrs = null; ProcessAbsObjAttrs($$, $1->components.decl.kind.obj.parts, null); ExitObject($$, startp, endp); } | simple_object_declaration END optional_name { $$ = $1; $$->components.decl.kind.obj.ops = null; $$->components.decl.kind.obj.eqns = null; $$->components.decl.kind.obj.attrs = null; ExitObject($$, startp, endp); } | simple_object_declaration object_attributes END optional_name { $$ = $1; $2 = FixDeclList($2); $$->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; ProcessAbsObjAttrs($$, $1->components.decl.kind.obj.parts, $2); ExitObject($$, startp, endp); } | simple_object_declaration error {$$ = null;} ; simple_object_declaration: object_heading { $$ = $1; } | object_heading '=' components_expression { $$ = $1; $$->components.decl.kind.obj.parts = $3; } | object_heading extends_symbol qualified_names { $$ = $1; $$->components.decl.kind.obj.inheritsfrom = FixAtomList2($3); } | object_heading extends_symbol qualified_names '=' components_expression { $$ = $1; $$->components.decl.kind.obj.parts = $5; $$->components.decl.kind.obj.inheritsfrom = FixAtomList2($3); } | object_heading '=' components_expression extends_symbol qualified_names { $$ = $1; $$->components.decl.kind.obj.parts = $5; $$->components.decl.kind.obj.inheritsfrom = FixAtomList2($3); } ; object_heading: object_symbol name { $$ = $1; $$->components.decl.kind.obj.name = $2; $$->components.decl.kind.obj.parts = null; $$->components.decl.kind.obj.flags = 0; $$->components.decl.kind.obj.parms = null; $$->components.decl.kind.obj.ops = null; $$->components.decl.kind.obj.eqns = null; $$->components.decl.kind.obj.attrs = null; $$->components.decl.kind.obj.inheritsfrom = null; EnterObjectName($$, $2); } | object_symbol name '(' object_parameters ')' { $$ = $1; $$->components.decl.kind.obj.name = $2; $$->components.decl.kind.obj.parts = null; $$->components.decl.kind.obj.flags = 0; $$->components.decl.kind.obj.parms = FixAtomList2($4); $$->components.decl.kind.obj.ops = null; $$->components.decl.kind.obj.eqns = null; $$->components.decl.kind.obj.attrs = null; $$->components.decl.kind.obj.inheritsfrom = null; EnterObjectName($$, $2); } | object_symbol name '(' object_parameters ')' error {$$ = null;} ; object_symbol: OBJECT {$$ = NewNode(DECL_NODE, YOBJ, $1.loc);} | OBJ {$$ = NewNode(DECL_NODE, YOBJ, $1.loc);} ; object_parameters: object_parameter {$$ = InitAtomList2($1);} | object_parameters ',' object_parameter {$$ = AddToAtomList2($1, $3);} ; object_parameter: name {$$ = $1;} | question_mark_name {$$ = $1;} ; object_attributes: object_attribute {$$ = InitDeclList($1);} | object_attributes object_attribute {$$ = AddToDeclList($1, $2);} ; object_attribute: components ';' | components error ';' {$$ = null;} | parents | /* * To be replaced with parameterized objects. */ where | operations | equations | user_defined_attribute ; components: components_symbol ':' components_expression { ExitRecord($1); $$ = NewNode(DECL_NODE, YPARTS, $2.loc); $$->components.decl.kind.parts = $3; inParts = false; } ; parents: PARENTS ':' qualified_names ';' { $$ = NewNode(DECL_NODE, YPARENTS, $2.loc); $$->components.decl.kind.parents = $3; } ; components_symbol: COMPONENTS {EnterRecord(); $$ = NewNode(TYPE_NODE, YRECORD, $1.loc);} | PARTS {EnterRecord(); $$ = NewNode(TYPE_NODE, YRECORD, $1.loc);} ; extends_symbol: EXTENDS {$$ = null;} | '<' {$$ = null;} ; components_expression: /* empty */ {$$ = null;} | components_expression component_and_op components_expression %prec AND { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | components_expression component_or_op components_expression %prec OR { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | components_expression component_list_op %prec UNARY_PLUS { 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; } } | component_operation_heading operation_signature { $$ = $1; $$->components.trinop.left_operand = $2->components.decl.kind.opsig.ins; $$->components.trinop.middle_operand = $2->components.decl.kind.opsig.outs; $$->components.trinop.right_operand = (nodep) CurSymtab->ParentEntry; ExitOperation(null, null, startp, endp); } | component_ref_op component_type_designator %prec UNARY_PLUS { if (isFullNameTypePair($2)) { $$ = $2; $1->components.unop.operand = $2->components.decl.kind.attr.value; $$->components.decl.kind.attr.value = $1; } else { $$ = $1; $$->components.unop.operand = $2; } } | components_base_element ; components_base_element: component_type_designator { if ($1 == null) { $$ = null; } else { $$ = NewNode(DECL_NODE, ':', loc($1)); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = null; $$->components.decl.kind.attr.initvalue = null; } } | component_type_designator '=' expression { $$ = NewNode(DECL_NODE, ':', loc($1)); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = null; $$->components.decl.kind.attr.initvalue = $3; } | literal { $$ = NewNode(DECL_NODE, ':', loc($1)); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = null; } | '(' components_expression ')' { $$ = $2; } | name ':' component_type_designator { $$ = NewNode(DECL_NODE, ':', loc($1)); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = $3; $$->components.decl.kind.attr.initvalue = null; } | name ':' component_type_designator '=' expression { $$ = NewNode(DECL_NODE, ':', loc($1)); $$->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 ':' literal { $$ = NewNode(DECL_NODE, ':', loc($1)); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = $3; } | name ':' '(' components_expression ')' { $$ = NewNode(DECL_NODE, ':', $2.loc); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = ':'; $$->components.decl.kind.attr.value = $4; } | component_type_designator error { $$ = null; } ; component_and_op: AND {$$ = NewNode(BINOP_NODE, YAND, $1.loc);} | ',' {$$ = NewNode(BINOP_NODE, YAND, $1.loc);} ; component_or_op: OR {$$ = NewNode(BINOP_NODE, YOR, $1.loc);} | '|' {$$ = NewNode(BINOP_NODE, YOR, $1.loc);} ; component_list_op: '*' {$$ = NewNode(UNOP_NODE, YLIST, $1.loc);} ; component_ref_op: REF {$$ = NewNode(UNOP_NODE, YREF, $1.loc);} ; component_operation_heading: operation_symbol { $$ = NewNode(TRINOP_NODE, YRTARROW, loc($1)); EnterAnonOpName(anonopnum++); } ; /* * Parts of the more involved version of where, which includes both op sig * requirements and requirement satisfaction equations, have been commented * out. */ where: WHERE ':' where_list ';' { $$ = NewNode(DECL_NODE, YWHERE, $2.loc); $$->components.decl.kind.where = FixDeclList($3); } ; where_list: /* empty */ {$$ = NIL;} | where_item {$$ = InitDeclList($1);} | where_list semicolon_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; } ; operations: operations_symbol ':' operation_names_optional_signatures ';' { $$ = NewNode(DECL_NODE, YOPS, $2.loc); $$->components.decl.kind.opsig.list = FixDeclList($3); } ; operations_symbol: OPERATIONS {$$ = NULL;} | OPS {$$ = NULL;} ; operation_names_optional_signatures: /* empty */ {$$ = null;} | operation_name_optional_signature {$$ = InitDeclList($1);} | operation_names_optional_signatures semicolon_or_comma_or_and operation_name_optional_signature {$$ = AddToDeclList($1, $3);} ; operation_name_optional_signature: name { $$ = NewNode(DECL_NODE, YOPS, loc($1)); $$->components.decl.kind.opsig.name = $1; $$->components.decl.kind.opsig.ins = null; $$->components.decl.kind.opsig.outs = null; } | operation_name operation_signature { $$ = $2; $$->components.decl.kind.opsig.name = $1; ExitOperation(null, null, startp, endp); } ; operation_name: name { EnterOpName($1); } ; equations: equations_symbol ':' equation_sequence ';' { $$ = $1; $$->components.decl.kind.eqns.vars = FixDeclList($3); $$->components.decl.kind.eqns.eqns = null; ExitEqns($$); } | equations_symbol ':' simple_variables ';' equation_sequence ';' { $$ = $1; $$->components.decl.kind.eqns.vars = FixDeclList($3); $$->components.decl.kind.eqns.eqns = FixDeclList($5); ExitEqns($$); } | equations_symbol error {$$ = null;} ; equations_symbol: EQUATIONS { $$ = NewNode(DECL_NODE, YEQUATIONS, $1.loc); EnterEqns(); } ; simple_variables: simple_variable {$$ = InitDeclList($1);} | simple_variables ';' simple_variable {$$ = AddToDeclList($1, $3);} ; simple_variable: variable_symbol names ':' type_designator { $$ = NewNode(DECL_NODE, YVAR, $3.loc); $$->components.decl.kind.var.vars = FixAtomList($2); $$->components.decl.kind.var.type = $4; $$->components.decl.kind.var.init = null; $$->components.decl.kind.var.attrs = null; EnterVars($$->components.decl.kind.var.vars, BuildCompType1($$->components.decl.kind.var.type)); } | variable_symbol names ':' type_designator '=' expression { $$ = NewNode(DECL_NODE, YVAR, $3.loc); $$->components.decl.kind.var.vars = FixAtomList($2); $$->components.decl.kind.var.type = $4; $$->components.decl.kind.var.init = $6; $$->components.decl.kind.var.attrs = null; EnterVars($$->components.decl.kind.var.vars, BuildCompType1($$->components.decl.kind.var.type)); } ; variable_symbol: VARIABLE {$$ = NULL;} | VAR {$$ = NULL;} ; equation_sequence: /* empty */ {$$ = NIL;} | equation {$$ = InitDeclList($1);} | equation_sequence ';' equation {$$ = AddToDeclList($1, $3);} ; equation: invocation EQEQ expression { $$=NewNode(DECL_NODE, YEQEQ, $2.loc); $$->components.decl.kind.eqn.lhs = $1; $$->components.decl.kind.eqn.rhs = $3; } ; user_defined_attribute: attribute_name attribute_colon ';' { nodep n; $$ = NewNode(DECL_NODE, ':', loc($1)); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = (n = NewNode(ATOM_NODE,Ytext, loc($2))); n->components.atom.val.string = GetLastComment(); n->components.atom.next = null; inAttribute = false; } | attribute_name attribute_colon ATTRIBUTE_TEXT ';' { nodep n; $$ = NewNode(DECL_NODE, ':', loc($1)); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = (n = NewNode(ATOM_NODE,Ytext,$3.loc)); n->components.atom.val.string = $3.val; n->components.atom.next = null; inAttribute = false; } | attribute_name ':' qualified_names ';' { nodep n; $$ = NewNode(DECL_NODE, ':', loc($1)); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = FixAtomList2($3); inAttribute = false; } | attribute_name ':' expression ';' { nodep n; $$ = NewNode(DECL_NODE, ':', loc($1)); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = $3; inAttribute = false; } ; attribute_colon: ':' { inAttribute = true; /* ClearComment(); -- now done in lex.l:SetIdent */ $$ = NewNode(ATOM_NODE, ':', $1.loc); $$->components.atom.next = null; } ; operation: simple_operation_declaration { $$ = $1; if (not $1->components.decl.kind.op.ins) { $$->components.decl.kind.op.ins = null; } if (not $1->components.decl.kind.op.outs) { $$->components.decl.kind.op.outs = null; } $$->components.decl.kind.op.precond = null; $$->components.decl.kind.op.postcond = null; $$->components.decl.kind.op.attrs = null; ProcessOpAttrs($$,null,null,null); ExitOperation($$, null, startp, endp); } | simple_operation_declaration END optional_name { $$ = $1; if (not $1->components.decl.kind.op.ins) { $$->components.decl.kind.op.ins = null; } if (not $1->components.decl.kind.op.outs) { $$->components.decl.kind.op.outs = null; } $$->components.decl.kind.op.precond = null; $$->components.decl.kind.op.postcond = null; $$->components.decl.kind.op.attrs = null; ExitOperation($$, null, startp, endp); } | simple_operation_declaration operation_attributes END optional_name { $$ = $1; $2 = FixDeclList($2); 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); } if (not $$->components.decl.kind.obj.parts) { $$->components.decl.kind.obj.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); } ; simple_operation_declaration: operation_symbol operation_heading { $$ = $2; } | operation_symbol operation_heading '=' expression { $$ = $2; $$->components.decl.kind.op.parts = $4; $$->components.decl.kind.op.flags = isDef; } | operation_symbol operation_heading '=' { $$ = $2; $$->components.decl.kind.op.parts = null; $$->components.decl.kind.op.flags = isDef; } ; ; operation_symbol: OPERATION {$$ = NewNode(DECL_NODE, YOP, $1.loc);} | OP {$$ = NewNode(DECL_NODE, YOP, $1.loc);} | FUNCTION {$$ = NewNode(DECL_NODE, YOP, $1.loc);} | FUNC {$$ = NewNode(DECL_NODE, YOP, $1.loc);} ; operation_heading: operation_name { $$ = NewNode(DECL_NODE, YOP, loc($1)); $$->components.decl.kind.obj.name = $1; $$->components.decl.kind.obj.flags = 0; $$->components.decl.kind.obj.inheritsfrom = null; $$->components.decl.kind.op.ins = null; $$->components.decl.kind.op.outs = null; } | operation_name operation_signature { $$ = NewNode(DECL_NODE, YOP, loc($1)); $$->components.decl.kind.op.name = $1; $$->components.decl.kind.op.flags = 0; $$->components.decl.kind.op.ins = $2->components.decl.kind.opsig.ins; $$->components.decl.kind.op.outs = $2->components.decl.kind.opsig.outs; } /* * This does not work syntactically: | operation_name operation_signature precondition_symbol ':' condition ';' postcondition_symbol ':' condition ';' { $$ = NewNode(DECL_NODE, YOP, loc($1)); $$->components.decl.kind.op.name = $1; $$->components.decl.kind.op.flags = 0; $$->components.decl.kind.op.ins = $2->components.decl.kind.opsig.ins; $$->components.decl.kind.op.outs = $2->components.decl.kind.opsig.outs; } */ ; operation_signature: in_paren operation_parameters ')' { $$ = NewNode(DECL_NODE, YRTARROW, loc($1)); $$->components.decl.kind.opsig.ins = $2; $$->components.decl.kind.opsig.outs = null; input_parm = false; } | in_paren operation_parameters ')' ARROW operation_output { $$ = NewNode(DECL_NODE, YRTARROW, loc($1)); $$->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); input_parm = false; } | in_paren operation_parameters ')' ARROW out_paren operation_outputs ')' { $$ = NewNode(DECL_NODE, YRTARROW, loc($1)); $$->components.decl.kind.opsig.ins = $2; $$->components.decl.kind.opsig.outs = $6; } ; in_paren: '(' { input_parm = true; $$ = NewNode(ATOM_NODE, '(', $1.loc); } ; out_paren: '(' { input_parm = false; $$ = NewNode(ATOM_NODE, '(', $1.loc); } ; operation_parameters: /* empty */ { $$ = null; } | operation_parameter { $$ = $1; $$->components.decl.next = null; if (input_parm) { EnterOpInParm( $$->components.decl.kind.initdecl.decl, $$->components.decl.kind.initdecl.islist); } else { EnterOpOutParm( $$->components.decl.kind.initdecl.decl, $$->components.decl.kind.initdecl.islist); } } | operation_parameters component_and_op operation_parameters %prec AND { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } ; operation_outputs: /* empty */ { $$ = null; } | operation_output { $$ = $1; $$->components.decl.next = null; if (input_parm) { EnterOpInParm( $$->components.decl.kind.initdecl.decl, $$->components.decl.kind.initdecl.islist); } else { EnterOpOutParm( $$->components.decl.kind.initdecl.decl, $$->components.decl.kind.initdecl.islist); } } | operation_outputs component_and_op operation_outputs %prec AND { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } ; operation_parameter: variable_type_designator { nodep n; n = NewNode(DECL_NODE, ':', loc($1)); n->components.decl.kind.attr.name = $1; n->components.decl.kind.attr.colon = null; n->components.decl.kind.attr.value = null; $$ = NewNode(DECL_NODE, YASSMNT, loc($1)); $$->components.decl.kind.initdecl.decl = n; $$->components.decl.kind.initdecl.init = null; $$->components.decl.kind.initdecl.islist = IsListTypeDesig($1); } | variable_type_designator '=' expression { nodep n; n = NewNode(DECL_NODE, ':', loc($1)); n->components.decl.kind.attr.name = $1; n->components.decl.kind.attr.colon = null; n->components.decl.kind.attr.value = null; $$ = NewNode(DECL_NODE, YASSMNT, loc($1)); $$->components.decl.kind.initdecl.decl = n; $$->components.decl.kind.initdecl.init = $3; $$->components.decl.kind.initdecl.islist = IsListTypeDesig($1); } | name ':' variable_type_designator { nodep n; n = NewNode(DECL_NODE, ':', loc($1)); n->components.decl.kind.attr.name = $1; n->components.decl.kind.attr.colon = null; n->components.decl.kind.attr.value = $3; $$ = NewNode(DECL_NODE, YASSMNT, loc($1)); $$->components.decl.kind.initdecl.decl = n; $$->components.decl.kind.initdecl.init = null; $$->components.decl.kind.initdecl.islist = IsListTypeDesig($3); } | name ':' variable_type_designator '=' expression { nodep n; n = NewNode(DECL_NODE, ':', loc($1)); n->components.decl.kind.attr.name = $1; n->components.decl.kind.attr.colon = null; n->components.decl.kind.attr.value = $3; $$ = NewNode(DECL_NODE, YASSMNT, loc($1)); $$->components.decl.kind.initdecl.decl = n; $$->components.decl.kind.initdecl.init = $5; $$->components.decl.kind.initdecl.islist = IsListTypeDesig($3); } ; operation_output: variable_type_designator { nodep n; n = NewNode(DECL_NODE, ':', loc($1)); n->components.decl.kind.attr.name = $1; n->components.decl.kind.attr.colon = null; n->components.decl.kind.attr.value = null; $$ = NewNode(DECL_NODE, YASSMNT, loc($1)); $$->components.decl.kind.initdecl.decl = n; $$->components.decl.kind.initdecl.init = null; $$->components.decl.kind.initdecl.islist = IsListTypeDesig($1); } | name ':' variable_type_designator { nodep n; n = NewNode(DECL_NODE, ':', loc($1)); n->components.decl.kind.attr.name = $1; n->components.decl.kind.attr.colon = null; n->components.decl.kind.attr.value = $3; $$ = NewNode(DECL_NODE, YASSMNT, loc($1)); $$->components.decl.kind.initdecl.decl = n; $$->components.decl.kind.initdecl.init = null; $$->components.decl.kind.initdecl.islist = IsListTypeDesig($3); } ; operation_attributes: operation_attribute {$$ = InitDeclList($1);} | operation_attributes operation_attribute {$$ = AddToDeclList($1, $2);} ; operation_attribute: components ';' | inputs_symbol ':' operation_parameters ';' { $$ = NewNode(DECL_NODE, YINPUTS, $2.loc); $$->components.decl.kind.ins = $3; } | outputs_symbol ':' operation_parameters ';' { $$ = NewNode(DECL_NODE, YOUTPUTS, $2.loc); $$->components.decl.kind.outs = $3; } | precondition_symbol ':' condition ';' { $$ = NewNode(DECL_NODE, YPRE, $2.loc); $$->components.decl.kind.pre.expr = $3; ExitPrecond($$); $$->header.end_loc = $2.loc; } | postcondition_symbol ':' condition ';' { $$ = NewNode(DECL_NODE, YPOST, $2.loc); $$->components.decl.kind.post.expr = $3; ExitPostcond($$); } | DATAFLOW ':' connections ';' { $$ = null; } | BODY ':' expression ';' { $$ = null; } | user_defined_attribute ; inputs_symbol: INPUTS { input_parm = true; $$ = NULL; } | IN { input_parm = true; $$ = NULL; } ; outputs_symbol: OUTPUTS { input_parm = false; $$ = NULL; } | OUT { input_parm = false; $$ = NULL; } ; precondition_symbol: PRECONDITION {$$ = NULL; EnterPrecond();} | PRE {$$ = NULL; EnterPrecond();} ; postcondition_symbol: POSTCONDITION {$$ = NULL; EnterPostcond();} | POST {$$ = NULL; EnterPostcond();} ; condition: /* empty */ {$$ = null;} | expression ; connections: connection {$$ = InitDeclList($1);} | connections ',' connection {$$ = AddToDeclList($1, $3);} ; connection: connection_expression ARROW connection_expression { $$ = NewNode(BINOP_NODE, ARROW, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } ; connection_expression: expression | '?' { $$ = NewNode(UNOP_NODE, '?', $1.loc); } ; value: value_symbol name '=' expression optional_attributes { $$ = $1; $$->components.decl.kind.obj.name = $2; $$->components.decl.kind.obj.type = null; /* NOTE: isDef must be set before calling * EnterObjectName, since the function relies on it. * This was the source of some consternation during * the conversion to the new parser. */ $$->components.decl.kind.obj.flags = isDef; EnterObjectName($$,$2); $$->components.decl.kind.obj.parts = $4; $$->components.decl.kind.obj.attrs = $5; ProcessConcObjAttrs($$,$4,null); ExitObject($$, startp, endp); } | value_symbol name ':' type_designator '=' expression optional_attributes { $$ = $1; $$->components.decl.kind.obj.name = $2; $$->components.decl.kind.obj.type = BuildCompType1($4); $$->components.decl.kind.obj.flags = isDef; EnterObjectName($$,$2); $$->components.decl.kind.obj.parts = $6; $$->components.decl.kind.obj.attrs = $7; ProcessConcObjAttrs($$,$6,null); ExitObject($$, startp, endp); } ; value_symbol: VALUE {$$ = NewNode(DECL_NODE, YOBJ, $1.loc);} | VAL {$$ = NewNode(DECL_NODE, YOBJ, $1.loc);} ; variable: variable_symbol names ':' type_designator optional_attributes { $$ = NewNode(DECL_NODE, YVAR, $3.loc); $$->components.decl.kind.var.vars = FixAtomList($2); $$->components.decl.kind.var.type = $4; $$->components.decl.kind.var.init = null; $$->components.decl.kind.var.attrs = $5; EnterVars($$->components.decl.kind.var.vars, BuildCompType1($$->components.decl.kind.var.type)); } | variable_symbol names ':' type_designator '=' expression optional_attributes { $$ = NewNode(DECL_NODE, YVAR, $3.loc); $$->components.decl.kind.var.vars = FixAtomList($2); $$->components.decl.kind.var.type = $4; $$->components.decl.kind.var.init = $6; $$->components.decl.kind.var.attrs = $7; EnterVars($$->components.decl.kind.var.vars, BuildCompType1($$->components.decl.kind.var.type)); } | variable_symbol names '=' expression optional_attributes { $$ = NewNode(DECL_NODE, YVAR, $3.loc); $$->components.decl.kind.var.vars = FixAtomList($2); $$->components.decl.kind.var.type = null; $$->components.decl.kind.var.init = $4; $$->components.decl.kind.var.attrs = $5; EnterVars($$->components.decl.kind.var.vars, BuildAtomType($$->components.decl.kind.var.type)); } ; axiom: axiom_symbol axiom_name '=' expression optional_attributes { $$ = $1; $$->header.loc = loc($4); $$->components.decl.kind.formaldef.name = $2; $$->components.decl.kind.formaldef.expr = $4; $$->components.decl.kind.formaldef.attrs = $5; ExitFormalDecl($$); } /* axiom_symbol axiom_expression_anonymous optional_attributes { $$ = $1; $$->header.loc = loc($2); $$->components.decl.kind.formaldef.name = null; $$->components.decl.kind.formaldef.expr = $2; $$->components.decl.kind.formaldef.attrs = $3; ExitFormalDecl($$); } | axiom_symbol axiom_name '=' expression optional_attributes { $$ = $1; $$->header.loc = loc($2); $$->components.decl.kind.formaldef.expr = $4; $$->components.decl.kind.formaldef.attrs = $5; ExitFormalDecl($$); } | axiom_symbol axiom_name ':' expression optional_attributes { $$ = $1; $$->header.loc = loc($2); $$->components.decl.kind.formaldef.expr = $4; $$->components.decl.kind.formaldef.attrs = $5; ExitFormalDecl($$); } */ ; /* */ axiom_name: name { $$ = $1; $$->components.decl.kind.formaldef.name = $1; EnterAxiom($1, 0); } ; /* */ /* axiom_expression_anonymous: expression { $$ = $1; EnterAxiom(null, anonaxnum++); } ; */ axiom_symbol: AXIOM { $$ = NewNode(DECL_NODE, YAX, $1.loc); // EnterAxiom(null, anonaxnum++); } | AX { $$ = NewNode(DECL_NODE, YAX, $1.loc); // EnterAxiom(null, anonaxnum++); } ; theorem: theorem_symbol theorem_name '=' expression optional_attributes { $$ = $1; $$->header.loc = loc($4); $$->components.decl.kind.formaldef.name = $2; $$->components.decl.kind.formaldef.expr = $4; $$->components.decl.kind.formaldef.attrs = $5; ExitFormalDecl($$); } /* theorem_symbol theorem_expression_anonymous optional_attributes { $$ = $1; $$->header.loc = loc($2); $$->components.decl.kind.formaldef.name = null; $$->components.decl.kind.formaldef.expr = $2; $$->components.decl.kind.formaldef.attrs = $3; ExitFormalDecl($$); } | theorem_heading expression optional_attributes { $$ = $1; $$->header.loc = loc($2); $$->components.decl.kind.formaldef.expr = $2; $$->components.decl.kind.formaldef.attrs = $3; ExitFormalDecl($$); } */ ; /* */ theorem_name: name { $$ = $1; $$->components.decl.kind.formaldef.name = $1; EnterTheorem($1, 0); } ; /* */ /* theorem_expression_anonymous: expression { $$ = $1; EnterTheorem(null, anonaxnum++); } ; */ theorem_symbol: THEOREM { $$ = NewNode(DECL_NODE, YTHM, $1.loc); // EnterTheorem(null, anonaxnum++); } | THM { $$ = NewNode(DECL_NODE, YTHM, $1.loc); // EnterTheorem(null, anonaxnum++); } ; attribute: untyped_attribute | untyped_attribute ':' {inParts = true;} components_expression {$$ = $1; inParts = false;} ; untyped_attribute: DEFINE OBJECT ATTRIBUTE names { DefineAttrNames(FixAtomList($4)); $$ = null; } | DEFINE OPERATION ATTRIBUTE names { DefineAttrNames(FixAtomList($4)); $$ = null; } | DEFINE ATTRIBUTE names { DefineAttrNames(FixAtomList($3)); $$ = null; } ; rule: rule_heading '=' rule_rhs optional_attributes { $$ = $1; $$->components.decl.kind.obj.parts = $3; $$->components.decl.kind.obj.attrs = FixDeclList($4); ExitObject($$, startp, endp); } | rule_heading '=' optional_attributes { $$ = $1; $$->components.decl.kind.obj.attrs = FixDeclList($3); ExitObject($$, startp, endp); } | rule_heading { $$ = $1; $$->components.decl.kind.obj.attrs = null; ExitObject($$, startp, endp); } ; rule_heading: RULE name { SymtabEntry* sym; $$ = NewNode(DECL_NODE, YOBJ, $1.loc); $$->components.decl.kind.obj.name = $2; $$->components.decl.kind.obj.parts = null; $$->components.decl.kind.obj.flags = isRule; $$->components.decl.kind.obj.parms = null; $$->components.decl.kind.obj.ops = null; $$->components.decl.kind.obj.eqns = null; $$->components.decl.kind.obj.attrs = null; $$->components.decl.kind.obj.inheritsfrom = null; sym = EnterObjectName($$, $2); SetSymFlag(sym, isRule); } ; rule_rhs: rule_alternative | rule_alternative '{' actions '}' ; rule_alternative: /* empty */ {$$ = null;} | rule_element | rule_rhs '|' rule_rhs { $$ = NewNode(BINOP_NODE, YOR, loc($1)); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } /* | rule_alternative '{' actions '}' '|' rule_rhs { $$ = NewNode(BINOP_NODE, YOR, loc($1)); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $6; } */ ; rule_element: rule_terminal | rule_terminal component_list_op %prec UNARY_PLUS { 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; } } | rule_element rule_element %prec AND { $$ = NewNode(BINOP_NODE, YAND, loc($1)); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $2; } ; rule_terminal: name { $$ = NewNode(DECL_NODE, ':', loc($1)); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = null; } | name ':' name { $$ = NewNode(DECL_NODE, ':', loc($1)); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = $3; } | STRING_LITERAL { nodep n = NewNode(ATOM_NODE, Ystring, $1.loc); n->components.atom.val.string = $1.val; n->components.atom.next = null; $$ = NewNode(DECL_NODE, ':', $1.loc); $$->components.decl.kind.attr.name = n; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = null; } | name ':' STRING_LITERAL { nodep n = NewNode(ATOM_NODE, Ystring, $3.loc); n->components.atom.val.string = $3.val; n->components.atom.next = null; $$ = NewNode(DECL_NODE, ':', loc($1)); $$->components.decl.kind.attr.name = $1; $$->components.decl.kind.attr.colon = null; $$->components.decl.kind.attr.value = n; } ; actions: action {$$ = InitDeclList($1);} | actions ';' action {$$ = AddToDeclList($1, $3);} ; action: /* empty */ { $$ = null; } | action_lhs '=' action_rhs { $$=NewNode(DECL_NODE, YEQEQ, $2.loc); $$->components.decl.kind.eqn.lhs = $1; $$->components.decl.kind.eqn.rhs = $3; } ; action_lhs: name ATTRIBUTE_SELECT attribute_name { $$=NewNode(BINOP_NODE, YATTRSELECT, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | name '.' attribute_name { $$=NewNode(BINOP_NODE, YATTRSELECT, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | name '.' name { $$=NewNode(BINOP_NODE, YATTRSELECT, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | name /* For global attributes */ { $$=NewNode(BINOP_NODE, YATTRSELECT, loc($1)); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = null; } ; action_rhs: expression ; optional_attributes: /* empty */ { $$ = null; } | END optional_name { $$ = null; } | user_defined_attributes END optional_name { $$ = FixDeclList($1); } ; user_defined_attributes: user_defined_attribute {$$ = InitDeclList($1);} | user_defined_attributes user_defined_attribute {$$ = AddToDeclList($1, $2);} ; include: INCLUDE STRING_LITERAL { $$ = null; } ; top_level_expression: expression ';' { if (PARSE_ERROR) { $$ = null; } else { $$ = NewNode(DECL_NODE, '>', loc($1)); $$->components.decl.kind.expr = $1; } } | '>' expression ';' { if (PARSE_ERROR) { $$ = null; } else { $$ = NewNode(DECL_NODE, '>', loc($2)); $$->components.decl.kind.expr = $2; } } /* | expression ';' error {$$ = null;} */ ; expression: boolean_expression | arithmetic_expression | callable_expression ; boolean_expression: expression AND expression %prec AND { $$ = NewNode(BINOP_NODE, YAND, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | expression OR expression %prec OR { $$ = NewNode(BINOP_NODE, YOR, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | NOT expression %prec NOT { $$ = NewNode(UNOP_NODE, YNOT, $1.loc); $$->components.unop.operand = $2; } | expression XOR expression { $$ = NewNode(BINOP_NODE, YXOR, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | expression IMPLIES expression %prec IMPLIES { $$ = NewNode(BINOP_NODE, YIMPLIES, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | expression IFF expression %prec IFF { $$ = NewNode(BINOP_NODE, YIFF, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | IF expression THEN expression %prec IF { $$ = NewNode(TRINOP_NODE, YIF, $1.loc); $$->components.trinop.left_operand = $2; $$->components.trinop.middle_operand = $4; $$->components.trinop.right_operand = null; } | IF expression THEN expression ELSE expression %prec IF { $$ = NewNode(TRINOP_NODE, YIF, $1.loc); $$->components.trinop.left_operand = $2; $$->components.trinop.middle_operand = $4; $$->components.trinop.right_operand = $6; } | relational_expression %prec '=' | quantifier_expression %prec FORALL ; relational_expression: expression relational_op expression %prec '=' { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | name almost_eq_op expression EXCEPT except_item %prec AEQ { nodep newnd; $$ = $2; $$->components.trinop.left_operand = $1; $$->components.trinop.middle_operand = $3; /* Make an expr list node out of the single item so this one-item case can be treated uniformly with the multi-item case. */ newnd = $$->components.trinop.right_operand = NewNode(EXPR_LIST_NODE, null, loc($1)); newnd->components.exprlist.expr = $5; newnd->components.exprlist.next = null; } | name almost_eq_op expression EXCEPT '(' except_items ')' %prec AEQ { $$ = $2; $$->components.trinop.left_operand = $1; $$->components.trinop.middle_operand = $3; $$->components.trinop.right_operand = FixExprList($6); } ; quantifier_expression: forall_symbol '(' names ':' type_name ')' expression %prec FORALL { nodep n; $$ = $1; n = NewNode(DECL_NODE, ':', $4.loc); n->components.decl.kind.attr.name = FixAtomList($3); n->components.decl.kind.attr.colon = null; n->components.decl.kind.attr.value = $5; EnterVars(n->components.decl.kind.attr.name, BuildCompType1($5)); $$->components.decl.kind.quant.vars = n; $$->components.decl.kind.quant.expr = $7; ExitQuant($$); } | forall_symbol '(' names IN expression ')' expression %prec FORALL { nodep n; $$ = $1; $$->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_symbol '(' names ':' type_name '|' expression ')' expression %prec FORALL { nodep n; $$ = $1; n = NewNode(DECL_NODE, ':', $4.loc); n->components.decl.kind.attr.name = FixAtomList($3); n->components.decl.kind.attr.colon = null; n->components.decl.kind.attr.value = $5; EnterVars(n->components.decl.kind.attr.name, BuildCompType1($5)); $$->components.decl.kind.quant.vars = n; $$->components.decl.kind.quant.in = n = NewNode(UNOP_NODE, '|', $6.loc); n->components.unop.operand = $7; $$->components.decl.kind.quant.expr = $9; ExitQuant($$); } | exists_symbol '(' names ':' type_name ')' expression %prec FORALL { nodep n; $$ = $1; n = NewNode(DECL_NODE, ':', $4.loc); n->components.decl.kind.attr.name = FixAtomList($3); n->components.decl.kind.attr.colon = null; n->components.decl.kind.attr.value = $5; EnterVars(n->components.decl.kind.attr.name, BuildCompType1($5)); $$->components.decl.kind.quant.vars = n; $$->components.decl.kind.quant.expr = $7; ExitQuant($$); } | exists_symbol '(' names IN expression ')' expression %prec FORALL { nodep n; $$ = $1; $$->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($$); } | exists_symbol '(' names ':' type_name '|' expression ')' expression %prec FORALL { nodep n; $$ = $1; n = NewNode(DECL_NODE, ':', $4.loc); n->components.decl.kind.attr.name = FixAtomList($3); n->components.decl.kind.attr.colon = null; n->components.decl.kind.attr.value = $5; EnterVars(n->components.decl.kind.attr.name, BuildCompType1($5)); $$->components.decl.kind.quant.vars = n; $$->components.decl.kind.quant.in = n = NewNode(UNOP_NODE, '|', $6.loc); n->components.unop.operand = $7; $$->components.decl.kind.quant.expr = $9; ExitQuant($$); } ; forall_symbol: FORALL { $$ = NewNode(DECL_NODE, YFORALL, $1.loc); EnterQuant(); } ; exists_symbol: EXISTS { $$ = NewNode(DECL_NODE, YEXISTS, $1.loc); EnterQuant(); } ; arithmetic_expression: expression add_op expression %prec '+' { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | expression mult_op expression %prec '*' { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | expression exp_op expression %prec '^' { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | arithmetic_prefix_op expression %prec UNARY_PLUS { $$ = $1; $$->components.unop.operand = $2; } | length_op expression %prec '#' { $$ = $1; $$->components.unop.operand = $2; } ; relational_op: '=' {$$ = NewNode(BINOP_NODE, '=', $1.loc);} | '<' {$$ = NewNode(BINOP_NODE, '<', $1.loc);} | '>' {$$ = NewNode(BINOP_NODE, '>', $1.loc);} | NEQ {$$ = NewNode(BINOP_NODE, YNEQ, $1.loc);} | LEQ {$$ = NewNode(BINOP_NODE, YLEQ, $1.loc);} | GEQ {$$ = NewNode(BINOP_NODE, YGEQ, $1.loc);} | IN {$$ = NewNode(BINOP_NODE, YIN, $1.loc);} ; almost_eq_op: AEQ {$$ = NewNode(TRINOP_NODE, YAEQ, $1.loc);} ; except_items: except_item { $$ = NewNode(EXPR_LIST_NODE, null, loc($1)); $$->components.exprlist.expr = $1; $$ = InitExprList($$); } | except_items ',' except_item { $$ = NewNode(EXPR_LIST_NODE, null, loc($3)); $$->components.exprlist.expr = $3; $$ = AddToExprList($1,$$); } | except_items AND except_item { $$ = NewNode(EXPR_LIST_NODE, null, loc($3)); $$->components.exprlist.expr = $3; $$ = AddToExprList($1,$$);} ; except_item: name '.' name '=' expression { nodep n; n = NewNode(BINOP_NODE, '.', $2.loc); n->components.binop.left_operand = $1; n->components.binop.right_operand = $3; $$ = NewNode(BINOP_NODE, '=', loc($1)); $$->components.binop.left_operand = n; $$->components.binop.right_operand = $5; } | name '.' INTEGER_LITERAL '=' expression { nodep n1, n2; n1 = NewNode(BINOP_NODE, '.', $2.loc); n1->components.binop.left_operand = $1; n2 = NewNode(ATOM_NODE,Yinteger, $3.loc); n2->components.atom.val.integer = $3.val; n2->components.atom.next = null; n1->components.binop.right_operand = n2; $$ = NewNode(BINOP_NODE, '=', loc($1)); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = n1; } ; add_op: '+' {$$ = NewNode(BINOP_NODE, '+', $1.loc);} | '-' {$$ = NewNode(BINOP_NODE, '-', $1.loc);} ; mult_op: '*' {$$ = NewNode(BINOP_NODE, '*', $1.loc);} | '/' {$$ = NewNode(BINOP_NODE, '/', $1.loc);} | DIV {$$ = NewNode(BINOP_NODE, YDIV, $1.loc);} | MOD {$$ = NewNode(BINOP_NODE, YMOD, $1.loc);} ; exp_op: '^' {$$ = NewNode(BINOP_NODE, '^', $1.loc);} ; length_op: '#' {$$ = NewNode(UNOP_NODE, '#', $1.loc);} ; arithmetic_prefix_op: '+' {$$ = NewNode(UNOP_NODE, YUNYPLUS, $1.loc);} | '-' {$$ = NewNode(UNOP_NODE, YUNYMINUS, $1.loc);} ; callable_expression: constructor_expression | selector_expression %prec '.' | index_expression %prec '[' | let %prec LET | set %prec SET | invocation %prec '(' | validation_invocation %prec '(' | lambda %prec LAMBDA | name %prec IDENTIFIER | literal %prec NIL_LITERAL | '(' expression_sequence ')' %prec '(' { $$ = FixExprList($2); } ; constructor_expression: '[' expression DOTDOT expression ']' { $$ = NewNode(BINOP_NODE, YDOTDOT, $1.loc); $$->components.binop.left_operand = $2; $$->components.binop.right_operand = $4; } | '[' expression_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); } | '{' expression_list_with_empties '}' { $$ = NewNode(UNOP_NODE, '}', $1.loc); $$->components.unop.operand = FixExprList($2); } ; selector_expression: callable_expression select_op name %prec '.' { $$ = $2; $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | callable_expression '.' INTEGER_LITERAL %prec '.' { nodep n; $$ = NewNode(BINOP_NODE, '.', $2.loc); $$->components.binop.left_operand = $1; n = NewNode(ATOM_NODE,Yinteger, $3.loc); n->components.atom.val.integer = $3.val; n->components.atom.next = null; $$->components.binop.right_operand = n; } | callable_expression ATTRIBUTE_SELECT attribute_name %prec '.' { $$ = NewNode(BINOP_NODE, YATTRSELECT, $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; inAttribute = false; } ; /* selectable_expression: constructor_expression | callable_expression ; */ select_op: '.' {$$ = NewNode(BINOP_NODE, '.', $1.loc);} | CHECK_UNION {$$ = NewNode(BINOP_NODE, YISA, $1.loc);} | GET_INSTANCE {$$ = NewNode(BINOP_NODE, YGETINSTANCE, $1.loc);} | CHECK_INSTANCE {$$ = NewNode(BINOP_NODE, YCHKINSTANCE, $1.loc);} ; index_expression: callable_expression '[' expression ']' %prec '[' { $$ = NewNode(BINOP_NODE, '[', $2.loc); $$->components.binop.left_operand = $1; $$->components.binop.right_operand = $3; } | callable_expression '[' expression DOTDOT expression ']' %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. */ | callable_expression '[' expression ':' expression ']' %prec '[' { $$ = NewNode(TRINOP_NODE, '[', $2.loc); $$->components.trinop.left_operand = $1; $$->components.trinop.middle_operand = $3; $$->components.trinop.right_operand = $5; } ; let: LET names '=' expression { $$ = 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; } | LET names ':' type_designator '=' expression { $$ = NewNode(DECL_NODE, YLET, $1.loc); $$->components.decl.kind.let.names = FixAtomList($2); $$->components.decl.kind.let.expr = $6; $$->components.decl.kind.let.type = BuildCompType1($4); } ; set: SET storage_designator '=' expression %prec SET { $$ = NewNode(BINOP_NODE, YASSMNT, $1.loc); $$->components.binop.left_operand = $2; $$->components.binop.right_operand = $4; } ; storage_designator: name | selector_expression %prec '.' | index_expression %prec '[' | dereference_expression %prec '@' ; dereference_expression: '@' callable_expression %prec '@' { $$ = NewNode(UNOP_NODE, '@', $1.loc); $$->components.unop.operand = $2; } ; invocation: callable_expression '(' actual_parameters ')' %prec '(' { $$ = NewNode(PROC_CALL_NODE, null, loc($1)); $$->components.proccall.desig = $1; $$->components.proccall.actuals = FixExprList($3); $$->components.proccall.returns = null; } ; validation_invocation: /* NOTE: the following RHS element causes 19 benign s/r conflicts */ callable_expression '(' actual_parameters ')' QARROW actual_parameter { $$ = NewNode(PROC_CALL_NODE, YQRTARROW, loc($1)); $$->components.trinop.left_operand = $1; $$->components.trinop.middle_operand = FixExprList($3); $$->components.trinop.right_operand = $6; } | callable_expression '(' actual_parameters ')' QARROW '(' actual_parameters ')' { $$ = NewNode(PROC_CALL_NODE, YQRTARROW, loc($1)); $$->components.proccall.desig = $1; $$->components.proccall.actuals = FixExprList($3); $$->components.proccall.returns = FixExprList($7); } ; actual_parameters: /* empty */ {$$ = NIL;} | actual_parameter { $$ = InitExprList($$); } | actual_parameters ',' actual_parameter { $$ = AddToExprList($1,$3); } ; actual_parameter: expression { $$ = NewNode(EXPR_LIST_NODE, null, loc($1)); $$->components.exprlist.expr = $1; $$->components.exprlist.next = null; } | '?' { $$ = NewNode(EXPR_LIST_NODE, null, $1.loc); $$->components.exprlist.expr = NewNode(UNOP_NODE, '?', $1.loc);; $$->components.exprlist.next = null; } ; lambda: /* Note that allowing unparenthesize coarity in this rule causes a * boatload of s/r conflicts, that appear to be benign. */ LAMBDA operation_signature expression { $$ = NewNode(TRINOP_NODE, YLAMBDA, $1.loc); $$->components.trinop.left_operand = $2->components.decl.kind.opsig.ins; $$->components.trinop.middle_operand = $2->components.decl.kind.opsig.outs; $$->components.trinop.right_operand = $3; } ; expression_list: /* empty */ {$$ = null;} | expression_list_element {$$ = InitExprList($1);} | expression_list ',' expression_list_element {$$ = AddToExprList($1,$3);} ; expression_list_element: expression { $$ = NewNode(EXPR_LIST_NODE, null, loc($1)); $$->components.exprlist.expr = $1; $$->components.exprlist.next = null; } ; expression_list_with_empties: expression_possibly_empty {$$ = InitExprList($1);} | expression_list_with_empties ',' expression_possibly_empty {$$ = AddToExprList($1,$3);} ; expression_possibly_empty: /* empty */ { $$ = null; } | expression { $$ = NewNode(EXPR_LIST_NODE, null, loc($1)); $$->components.exprlist.expr = $1; $$->components.exprlist.next = null; } ; expression_sequence: /* empty {$$ = null;} | */ expression_sequence_element {$$ = InitExprList($1);} | expression_sequence ';' expression_sequence_element {$$ = AddToExprList($1,$3);} ; expression_sequence_element: /* empty */ {$$ = null;} | expression { if ($1 == null) $$ = null; else { $$ = NewNode(EXPR_LIST_NODE, YLIST, loc($1)); $$->components.exprlist.expr = $1; $$->components.exprlist.next = null; } } | simple_variable { if ($1 == null) $$ = null; else { $$ = NewNode(EXPR_LIST_NODE, YLIST, loc($1)); $$->components.exprlist.expr = $1; $$->components.exprlist.next = null; } } ; qualified_names: qualified_name { $$ = InitAtomList2(FixAtomList($1)); } | qualified_names ',' qualified_name { $$ = AddToAtomList2($1, FixAtomList($3)); } ; qualified_name: name { $$ = InitAtomList($1); } | qualified_name '.' name { $$ = AddToAtomList($1, $3); } ; names: name {$$ = InitAtomList($1);} | names ',' name {$$ = AddToAtomList($1, $3);} ; name: IDENTIFIER { $$ = NewNode(ATOM_NODE, Yident, $1.loc); $$->components.atom.val.text = $1.text; $$->components.atom.next = null; } ; attribute_name: ATTRIBUTE_IDENTIFIER { /* 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; } ; optional_name: /* empty */ { $$ = null; } | name ; component_type_designator: type_name_or_variable | type_name_or_variable '(' type_names ')' { if (PARSE_ERROR) { $$ = null; } else { $$ = $1; $$->components.atom.parms = $3; } } ; variable_type_designator: type_name_or_variable { // $$ = BuildAtomType($1); $$ = $1; if ($$) { $$->components.atom.parms = null; } } | type_name_or_variable component_list_op { $$ = $2; $$->header.loc = loc($1); if ($$ and $1) { $$->components.unop.operand = $1; $1->components.atom.parms = null; } } | type_name_or_variable '(' type_names_or_variables ')' { // $$ = BuildAtomType($1); $$ = $1; if ($$) { $$->components.atom.parms = FixAtomList2($3); } } | type_name_or_variable '(' type_names_or_variables ')' component_list_op { $$ = $5; if ($$ and $1) { $$->components.unop.operand = $1; $1->components.atom.parms = FixAtomList2($3); } } ; type_designator: type_name { // $$ = BuildAtomType($1); $$ = $1; if ($$ != null) { $$->components.atom.parms = null; } } | type_name component_list_op { $$ = $2; $$->components.unop.operand = $1; $$->components.atom.parms = null; } | type_name '(' type_names ')' { // $$ = BuildAtomType($1); $$ = $1; $$->components.atom.parms = FixAtomList2($3); } | type_name '(' type_names ')' component_list_op { $$ = $5; $$->components.unop.operand = $1; $1->components.atom.parms = FixAtomList2($3); } ; type_names: type_name {$$ = InitAtomList2($1);} | type_names ',' type_name {$$ = AddToAtomList2($1, $3);} ; type_name: qualified_name { $$ = FixAtomList($1); } ; type_name_or_variable: qualified_name { $$ = FixAtomList($1); } | question_mark_name { $$ = $1; } ; type_names_or_variables: type_name_or_variable {$$ = InitAtomList2($1);} | type_names_or_variables ',' type_name_or_variable {$$ = AddToAtomList2($1, $3);} ; question_mark_name: QUESTION_MARK_IDENTIFIER { $$ = NewNode(ATOM_NODE, Yident, $1.loc); $$->components.atom.val.text = $1.text; $$->components.atom.next = null; } ; literal: STRING_LITERAL { $$ = NewNode(ATOM_NODE, Ystring, $1.loc); $$->components.atom.val.string = $1.val; $$->components.atom.next = null; } | INTEGER_LITERAL { $$ = NewNode(ATOM_NODE,Yinteger, $1.loc); $$->components.atom.val.integer = $1.val; $$->components.atom.next = null; } | REAL_LITERAL { $$ = NewNode(ATOM_NODE,Yreal, $1.loc); $$->components.atom.val.real = $1.val; $$->components.atom.next = null; } | NIL_LITERAL { $$ = NewNode(ATOM_NODE,Ynil, $1.loc); $$->components.atom.val.nilval = 0; $$->components.atom.next = null; } ; semicolon_or_comma: /* */ ';' {$$ = null;} | /* */ ',' {$$ = null;} /* | AND {$$ = null;} */ ; semicolon_or_comma_or_and: /* */ ';' {$$ = null;} | /* */ ',' {$$ = null;} | AND {$$ = null;} ; optional_semicolon: /* * empty */ { $$ = null; } | ';' { $$ = null; } ; %% /*** * Functions */ /* set debugging flags (if you like); call yyparse(); return parse tree */ nodep parser() { #ifdef YYDEBUG yydebug = 0; #endif parsetree = null; 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; anonaxnum = 0; anonthmnum = 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; }