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/lps/parse_impl.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_PARSE_IMPL_H
      13             : #define MCRL2_LPS_PARSE_IMPL_H
      14             : 
      15             : #include "mcrl2/lps/detail/linear_process_conversion_traverser.h"
      16             : #include "mcrl2/lps/typecheck.h"
      17             : #include "mcrl2/process/parse.h"
      18             : #include "mcrl2/process/parse_impl.h"
      19             : 
      20             : namespace mcrl2 {
      21             : 
      22             : namespace lps {
      23             : 
      24             : namespace detail
      25             : {
      26             : 
      27             : struct multi_action_actions: public process::detail::action_actions
      28             : {
      29         201 :   explicit multi_action_actions(const core::parser& parser_)
      30         201 :     : process::detail::action_actions(parser_)
      31         201 :   {}
      32             : 
      33          22 :   process::untyped_multi_action parse_MultAct(const core::parse_node& node) const
      34             :   {
      35          22 :     if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "tau")) { return process::untyped_multi_action(); }
      36          18 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "ActionList"))
      37             :     {
      38          36 :       return process::untyped_multi_action(parse_ActionList(node.child(0)));
      39             :     }
      40           0 :     throw core::parse_node_unexpected_exception(m_parser, node);
      41             :   }
      42             : };
      43             : 
      44             : struct action_rename_actions: public process::detail::action_actions
      45             : {
      46           6 :   explicit action_rename_actions(const core::parser& parser_)
      47           6 :     : process::detail::action_actions(parser_)
      48           6 :   {}
      49             : 
      50             :   // create an action with an incomplete action label
      51          16 :   process::action parse_Action_as_action(const core::parse_node& node) const
      52             :   {
      53          32 :     process::action_label label(parse_Id(node.child(0)), {});
      54          48 :     return process::action(label, parse_DataExprList(node.child(1)));
      55          16 :   }
      56             : 
      57          10 :   process::process_expression parse_ActionRenameRuleRHS(const core::parse_node& node) const
      58             :   {
      59          10 :     if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "Action")) { return parse_Action_as_action(node.child(0)); }
      60           4 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "tau")) { return process::tau(); }
      61           3 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "delta")) { return process::delta(); }
      62           0 :     throw core::parse_node_unexpected_exception(m_parser, node);
      63             :   }
      64             : 
      65          10 :   lps::action_rename_rule parse_ActionRenameRule(const core::parse_node& node) const
      66             :   {
      67          10 :     data::data_expression condition = data::sort_bool::true_();
      68          10 :     if (node.child(0).child(0))
      69             :     {
      70           4 :       condition = parse_DataExpr(node.child(0).child(0).child(0));
      71             :     }
      72          30 :     return action_rename_rule(data::variable_list(), condition, parse_Action_as_action(node.child(1)), parse_ActionRenameRuleRHS(node.child(3)));
      73          10 :   }
      74             : 
      75           7 :   std::vector<lps::action_rename_rule> parse_ActionRenameRuleList(const core::parse_node& node) const
      76             :   {
      77          17 :     return parse_vector<lps::action_rename_rule>(node, "ActionRenameRule", [&](const core::parse_node& node) { return parse_ActionRenameRule(node); });
      78             :   }
      79             : 
      80           7 :   std::vector<lps::action_rename_rule> parse_ActionRenameRuleSpec(const core::parse_node& node) const
      81             :   {
      82           7 :     data::variable_list variables = parse_VarSpec(node.child(0));
      83           7 :     std::vector<lps::action_rename_rule> rules = parse_ActionRenameRuleList(node.child(2));
      84          17 :     for (lps::action_rename_rule& rule: rules)
      85             :     {
      86          10 :       rule.variables() = variables;
      87             :     }
      88          14 :     return rules;
      89           7 :   }
      90             : 
      91          38 :   bool callback_ActionRenameSpec(const core::parse_node& node, data::untyped_data_specification& dataspec_result, lps::action_rename_specification& result) const
      92             :   {
      93          38 :     if (symbol_name(node) == "SortSpec")
      94             :     {
      95           0 :       return callback_DataSpecElement(node, dataspec_result);
      96             :     }
      97          38 :     else if (symbol_name(node) == "ConsSpec")
      98             :     {
      99           0 :       return callback_DataSpecElement(node, dataspec_result);
     100             :     }
     101          38 :     else if (symbol_name(node) == "MapSpec")
     102             :     {
     103           1 :       return callback_DataSpecElement(node, dataspec_result);
     104             :     }
     105          37 :     else if (symbol_name(node) == "EqnSpec")
     106             :     {
     107           1 :       return callback_DataSpecElement(node, dataspec_result);
     108             :     }
     109          36 :     else if (symbol_name(node) == "ActSpec")
     110             :     {
     111           4 :       result.action_labels() = result.action_labels() + parse_ActSpec(node);
     112           4 :       return true;
     113             :     }
     114          32 :     else if (symbol_name(node) == "ActionRenameRuleSpec")
     115             :     {
     116           7 :       std::vector<lps::action_rename_rule> rules = parse_ActionRenameRuleSpec(node);
     117           7 :       result.rules().insert(result.rules().end(), rules.begin(), rules.end());
     118           7 :       return true;
     119           7 :     }
     120          25 :     return false;
     121             :   }
     122             : 
     123           6 :   lps::action_rename_specification parse_ActionRenameSpec(const core::parse_node& node) const
     124             :   {
     125           6 :     data::untyped_data_specification dataspec_result;
     126           6 :     lps::action_rename_specification result;
     127          44 :     traverse(node, [&](const core::parse_node& node) { return callback_ActionRenameSpec(node, dataspec_result, result); });
     128           6 :     result.data() = dataspec_result.construct_data_specification();
     129          12 :     return result;
     130           6 :   }
     131             : };
     132             : 
     133             : } // namespace detail
     134             : 
     135             : } // namespace lps
     136             : 
     137             : } // namespace mcrl2
     138             : 
     139             : #endif // MCRL2_LPS_PARSE_IMPL_H