Line data    Source code

       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/process/parse_impl.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_PARSE_IMPL_H
      13             : #define MCRL2_PROCESS_PARSE_IMPL_H
      14             : 
      15             : #include "mcrl2/data/parse_impl.h"
      16             : #include "mcrl2/process/typecheck.h"
      17             : #include "mcrl2/utilities/detail/separate_keyword_section.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace process {
      22             : 
      23             : struct untyped_process_specification: public data::untyped_data_specification
      24             : {
      25             :   data::variable_list global_variables;
      26             :   action_label_list action_labels;
      27             :   std::vector<process::process_equation> equations;
      28             :   process_expression init;
      29             : 
      30        1152 :   process_specification construct_process_specification()
      31             :   {
      32        1152 :     process_specification result;
      33        1152 :     result.data() = construct_data_specification();
      34        1152 :     result.global_variables() = std::set<data::variable>(global_variables.begin(), global_variables.end());
      35        1152 :     result.action_labels() = action_labels;
      36        1152 :     result.equations() = equations;
      37        1152 :     result.init() = init;
      38        1152 :     return result;
      39           0 :   }
      40             : };
      41             : 
      42             : namespace detail
      43             : {
      44             : 
      45             : struct action_actions: public data::detail::data_specification_actions
      46             : {
      47        1366 :   action_actions(const core::parser& parser_)
      48        1366 :     : data::detail::data_specification_actions(parser_)
      49        1366 :   {}
      50             : 
      51         189 :   data::untyped_data_parameter parse_Action(const core::parse_node& node) const
      52             :   {
      53         378 :     return data::untyped_data_parameter(parse_Id(node.child(0)), parse_DataExprList(node.child(1)));
      54             :   }
      55             : 
      56         197 :   data::untyped_data_parameter_list parse_ActionList(const core::parse_node& node) const
      57             :   {
      58         386 :     return parse_list<data::untyped_data_parameter>(node, "Action", [&](const core::parse_node& node) { return parse_Action(node); });
      59             :   }
      60             : 
      61        2378 :   bool callback_ActDecl(const core::parse_node& node, action_label_vector& result) const
      62             :   {
      63        2378 :     if (symbol_name(node) == "ActDecl")
      64             :     {
      65        1362 :       core::identifier_string_list ids = parse_IdList(node.child(0));
      66        1362 :       data::sort_expression_list sorts;
      67        1362 :       if (node.child(1).child(0))
      68             :       {
      69         754 :         sorts = parse_SortProduct(node.child(1).child(0).child(1));
      70             :       }
      71        3914 :       for (const core::identifier_string& id: ids)
      72             :       {
      73        2552 :         result.push_back(action_label(id, sorts));
      74             :       }
      75        1362 :       return true;
      76        1362 :     }
      77        1016 :     return false;
      78             :   };
      79             : 
      80        1016 :   action_label_list parse_ActDeclList(const core::parse_node& node) const
      81             :   {
      82        1016 :     action_label_vector result;
      83        3390 :     traverse(node, [&](const core::parse_node& node) { return callback_ActDecl(node, result); });
      84        2032 :     return process::action_label_list(result.begin(), result.end());
      85        1016 :   }
      86             : 
      87        1016 :   action_label_list parse_ActSpec(const core::parse_node& node) const
      88             :   {
      89        2032 :     return parse_ActDeclList(node.child(1));
      90             :   }
      91             : };
      92             : 
      93             : struct process_actions: public process::detail::action_actions
      94             : {
      95        1155 :   explicit process_actions(const core::parser& parser_)
      96        1155 :     : process::detail::action_actions(parser_)
      97        1155 :   {}
      98             : 
      99          24 :   core::identifier_string_list parse_ActIdSet(const core::parse_node& node) const
     100             :   {
     101          48 :     return parse_IdList(node.child(1));
     102             :   }
     103             : 
     104         182 :   process::action_name_multiset parse_MultActId(const core::parse_node& node) const
     105             :   {
     106         364 :     return action_name_multiset(parse_IdList(node));
     107             :   }
     108             : 
     109          70 :   process::action_name_multiset_list parse_MultActIdList(const core::parse_node& node) const
     110             :   {
     111         252 :     return parse_list<process::action_name_multiset>(node, "MultActId", [&](const core::parse_node& node) { return parse_MultActId(node); });
     112             :   }
     113             : 
     114          70 :   process::action_name_multiset_list parse_MultActIdSet(const core::parse_node& node) const
     115             :   {
     116         140 :     return parse_MultActIdList(node.child(1));
     117             :   }
     118             : 
     119         195 :   process::communication_expression parse_CommExpr(const core::parse_node& node) const
     120             :   {
     121         195 :     core::identifier_string id = parse_Id(node.child(0));
     122         195 :     core::identifier_string_list ids = parse_IdList(node.child(2));
     123         195 :     ids.push_front(id);
     124         195 :     action_name_multiset lhs(ids);
     125         195 :     core::identifier_string rhs = parse_Id(node.child(4));
     126         390 :     return process::communication_expression(lhs, rhs);
     127         195 :   }
     128             : 
     129         122 :   process::communication_expression_list parse_CommExprList(const core::parse_node& node) const
     130             :   {
     131         317 :     return parse_list<process::communication_expression>(node, "CommExpr", [&](const core::parse_node& node) { return parse_CommExpr(node); });
     132             :   }
     133             : 
     134         122 :   process::communication_expression_list parse_CommExprSet(const core::parse_node& node) const
     135             :   {
     136         244 :     return parse_CommExprList(node.child(1));
     137             :   }
     138             : 
     139           0 :   process::rename_expression parse_RenExpr(const core::parse_node& node) const
     140             :   {
     141           0 :     return process::rename_expression(parse_Id(node.child(0)), parse_Id(node.child(2)));
     142             :   }
     143             : 
     144           0 :   process::rename_expression_list parse_RenExprList(const core::parse_node& node) const
     145             :   {
     146           0 :     return parse_list<process::rename_expression>(node, "RenExpr", [&](const core::parse_node& node) { return parse_RenExpr(node); });
     147             :   }
     148             : 
     149           0 :   process::rename_expression_list parse_RenExprSet(const core::parse_node& node) const
     150             :   {
     151           0 :     return parse_RenExprList(node.child(1));
     152             :   }
     153             : 
     154         754 :   bool is_proc_expr_sum(const core::parse_node& node) const
     155             :   {
     156         754 :     return (symbol_name(node).find("ProcExpr") == 0) && (node.child_count() == 3) && (symbol_name(node.child(0)) == "sum") && (symbol_name(node.child(1)) == "VarsDeclList") && (symbol_name(node.child(2)) == ".");
     157             :   }
     158             : 
     159        2295 :   bool is_proc_expr_if(const core::parse_node& node) const
     160             :   {
     161        2295 :     return (symbol_name(node).find("ProcExpr") == 0) && (node.child_count() == 2) && (symbol_name(node.child(0)) == "DataExprUnit") && (node.child(1).string() == "->");
     162             :   }
     163             : 
     164         879 :   bool is_proc_expr_else(const core::parse_node& node) const
     165             :   {
     166         879 :     return (symbol_name(node).find("ProcExpr") == 0) && (node.child_count() == 3) && is_proc_expr_if(node.child(0)) && (symbol_name(node.child(1)) == "ProcExpr") && (node.child(2).string() == "<>");
     167             :   }
     168             : 
     169         136 :   bool is_proc_expr_stochastic_operator(const core::parse_node& node) const
     170             :   {
     171         408 :     return (symbol_name(node).find("ProcExpr") == 0) && (node.child_count() == 6) && (symbol_name(node.child(0)) == "dist") && (symbol_name(node.child(1)) == "VarsDeclList") &&
     172         544 :            (symbol_name(node.child(2)) == "[") && (symbol_name(node.child(3)) == "DataExpr") && (symbol_name(node.child(4)) == "]") && (symbol_name(node.child(5)) == ".");
     173             :   }
     174             : 
     175             :   // override
     176        5013 :   data::untyped_data_parameter parse_Action(const core::parse_node& node) const
     177             :   {
     178       10026 :     return data::untyped_data_parameter(parse_Id(node.child(0)), parse_DataExprList(node.child(1)));
     179             :   }
     180             : 
     181       12514 :   process::process_expression parse_ProcExpr(const core::parse_node& node) const
     182             :   {
     183       12514 :     if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "Action")) { return parse_Action(node.child(0)); }
     184        7501 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "Id") && (symbol_name(node.child(1)) == "(") && (symbol_name(node.child(3)) == ")")) { return untyped_process_assignment(parse_Id(node.child(0)), parse_AssignmentList(node.child(2))); }
     185        7060 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "delta")) { return delta(); }
     186        6549 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "tau")) { return tau(); }
     187        6388 :     else if ((node.child_count() == 6) && (symbol_name(node.child(0)) == "block") && (symbol_name(node.child(1)) == "(") && (symbol_name(node.child(2)) == "ActIdSet") && (symbol_name(node.child(3)) == ",") && (symbol_name(node.child(4)) == "ProcExpr") && (symbol_name(node.child(5)) == ")")) { return process::block(parse_ActIdSet(node.child(2)), parse_ProcExpr(node.child(4))); }
     188        6388 :     else if ((node.child_count() == 6) && (symbol_name(node.child(0)) == "allow") && (symbol_name(node.child(1)) == "(") && (symbol_name(node.child(2)) == "MultActIdSet") && (symbol_name(node.child(3)) == ",") && (symbol_name(node.child(4)) == "ProcExpr") && (symbol_name(node.child(5)) == ")")) { return process::allow(parse_MultActIdSet(node.child(2)), parse_ProcExpr(node.child(4))); }
     189        6318 :     else if ((node.child_count() == 6) && (symbol_name(node.child(0)) == "hide") && (symbol_name(node.child(1)) == "(") && (symbol_name(node.child(2)) == "ActIdSet") && (symbol_name(node.child(3)) == ",") && (symbol_name(node.child(4)) == "ProcExpr") && (symbol_name(node.child(5)) == ")")) { return process::hide(parse_ActIdSet(node.child(2)), parse_ProcExpr(node.child(4))); }
     190        6294 :     else if ((node.child_count() == 6) && (symbol_name(node.child(0)) == "rename") && (symbol_name(node.child(1)) == "(") && (symbol_name(node.child(2)) == "RenExprSet") && (symbol_name(node.child(3)) == ",") && (symbol_name(node.child(4)) == "ProcExpr") && (symbol_name(node.child(5)) == ")")) { return process::rename(parse_RenExprSet(node.child(2)), parse_ProcExpr(node.child(4))); }
     191        6294 :     else if ((node.child_count() == 6) && (symbol_name(node.child(0)) == "comm") && (symbol_name(node.child(1)) == "(") && (symbol_name(node.child(2)) == "CommExprSet") && (symbol_name(node.child(3)) == ",") && (symbol_name(node.child(4)) == "ProcExpr") && (symbol_name(node.child(5)) == ")")) { return process::comm(parse_CommExprSet(node.child(2)), parse_ProcExpr(node.child(4))); }
     192        6750 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "(") && (symbol_name(node.child(1)) == "ProcExpr") && (symbol_name(node.child(2)) == ")")) { return parse_ProcExpr(node.child(1)); }
     193        5594 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "ProcExpr") && (node.child(1).string() == "+") && (symbol_name(node.child(2)) == "ProcExpr")) { return choice(parse_ProcExpr(node.child(0)), parse_ProcExpr(node.child(2))); }
     194        4782 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "ProcExpr") && (node.child(1).string() == "||") && (symbol_name(node.child(2)) == "ProcExpr")) { return merge(parse_ProcExpr(node.child(0)), parse_ProcExpr(node.child(2))); }
     195        4438 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "ProcExpr") && (node.child(1).string() == "||_") && (symbol_name(node.child(2)) == "ProcExpr")) { return left_merge(parse_ProcExpr(node.child(0)), parse_ProcExpr(node.child(2))); }
     196        4438 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "ProcExpr") && (node.child(1).string() == ".") && (symbol_name(node.child(2)) == "ProcExpr")) { return seq(parse_ProcExpr(node.child(0)), parse_ProcExpr(node.child(2))); }
     197        2219 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "ProcExpr") && (node.child(1).string() == "<<") && (symbol_name(node.child(2)) == "ProcExpr")) { return bounded_init(parse_ProcExpr(node.child(0)), parse_ProcExpr(node.child(2))); }
     198        2219 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "ProcExpr") && (node.child(1).string() == "@") && (symbol_name(node.child(2)) == "DataExprUnit")) { return at(parse_ProcExpr(node.child(0)), parse_DataExprUnit(node.child(2))); }
     199        1877 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "ProcExpr") && (node.child(1).string() == "|") && (symbol_name(node.child(2)) == "ProcExpr")) { return sync(parse_ProcExpr(node.child(0)), parse_ProcExpr(node.child(2))); }
     200        1552 :     else if ((node.child_count() == 2) && is_proc_expr_if(node.child(0)) && (symbol_name(node.child(1)) == "ProcExpr")) { return if_then(parse_DataExprUnit(node.child(0).child(0)), parse_ProcExpr(node.child(1))); }
     201         879 :     else if ((node.child_count() == 2) && is_proc_expr_else(node.child(0)) && (symbol_name(node.child(1)) == "ProcExpr")) { return if_then_else(parse_DataExprUnit(node.child(0).child(0).child(0)), parse_ProcExpr(node.child(0).child(1)), parse_ProcExpr(node.child(1))); }
     202         754 :     else if ((node.child_count() == 2) && is_proc_expr_sum(node.child(0)) && (symbol_name(node.child(1)) == "ProcExpr")) { return sum(parse_VarsDeclList(node.child(0).child(1)), parse_ProcExpr(node.child(1))); }
     203         136 :     else if ((node.child_count() == 2) && is_proc_expr_stochastic_operator(node.child(0)) && (symbol_name(node.child(1)) == "ProcExpr")) { return stochastic_operator(parse_VarsDeclList(node.child(0).child(1)), parse_DataExpr(node.child(0).child(3)), parse_ProcExpr(node.child(1))); }
     204           0 :     throw core::parse_node_unexpected_exception(m_parser, node);
     205             :   }
     206             : 
     207        1146 :   process::process_equation parse_ProcDecl(const core::parse_node& node) const
     208             :   {
     209        1146 :     core::identifier_string name = parse_Id(node.child(0));
     210        1146 :     data::variable_list variables = parse_VarsDeclList(node.child(1));
     211        1146 :     process_identifier id(name, variables);
     212        3438 :     return process::process_equation(id, variables, parse_ProcExpr(node.child(3)));
     213        1146 :   }
     214             : 
     215         893 :   std::vector<process::process_equation> parse_ProcDeclList(const core::parse_node& node) const
     216             :   {
     217        2039 :     return parse_vector<process::process_equation>(node, "ProcDecl", [&](const core::parse_node& node) { return parse_ProcDecl(node); });
     218             :   }
     219             : 
     220         893 :   std::vector<process::process_equation> parse_ProcSpec(const core::parse_node& node) const
     221             :   {
     222        1786 :     return parse_ProcDeclList(node.child(1));
     223             :   }
     224             : 
     225        1152 :   process::process_expression parse_Init(const core::parse_node& node) const
     226             :   {
     227        2304 :     return parse_ProcExpr(node.child(1));
     228             :   }
     229             : 
     230       40589 :   bool callback_mCRL2Spec(const core::parse_node& node, untyped_process_specification& result) const
     231             :   {
     232       40589 :     if (symbol_name(node) == "SortSpec")
     233             :     {
     234         242 :       return callback_DataSpecElement(node, result);
     235             :     }
     236       40347 :     else if (symbol_name(node) == "ConsSpec")
     237             :     {
     238           7 :       return callback_DataSpecElement(node, result);
     239             :     }
     240       40340 :     else if (symbol_name(node) == "MapSpec")
     241             :     {
     242         138 :       return callback_DataSpecElement(node, result);
     243             :     }
     244       40202 :     else if (symbol_name(node) == "EqnSpec")
     245             :     {
     246         110 :       return callback_DataSpecElement(node, result);
     247             :     }
     248       40092 :     else if (symbol_name(node) == "GlobVarSpec")
     249             :     {
     250          38 :       result.global_variables = parse_GlobVarSpec(node);
     251          38 :       return true;
     252             :     }
     253       40054 :     else if (symbol_name(node) == "ActSpec")
     254             :     {
     255        1008 :       result.action_labels = result.action_labels + parse_ActSpec(node);
     256        1008 :       return true;
     257             :     }
     258       39046 :     else if (symbol_name(node) == "ProcSpec")
     259             :     {
     260         893 :       std::vector<process::process_equation> eqn = parse_ProcSpec(node);
     261         893 :       result.equations.insert(result.equations.end(), eqn.begin(), eqn.end());
     262         893 :       return true;
     263         893 :     }
     264       38153 :     else if (symbol_name(node) == "Init")
     265             :     {
     266        1152 :       result.init = parse_Init(node);
     267             :     }
     268       38153 :     return false;
     269             :   }
     270             : 
     271        1152 :   untyped_process_specification parse_mCRL2Spec(const core::parse_node& node) const
     272             :   {
     273        1152 :     untyped_process_specification result;
     274       41741 :     traverse(node, [&](const core::parse_node& node) { return callback_mCRL2Spec(node, result); });
     275        1152 :     return result;
     276           0 :   }
     277             : };
     278             : 
     279             : } // namespace detail
     280             : 
     281             : } // namespace process
     282             : 
     283             : } // namespace mcrl2
     284             : 
     285             : #endif // MCRL2_PROCESS_PARSE_IMPL_H