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.h
      10             : /// \brief Parse function for process specifications
      11             : 
      12             : #ifndef MCRL2_PROCESS_PARSE_H
      13             : #define MCRL2_PROCESS_PARSE_H
      14             : 
      15             : #include "mcrl2/data/parse.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             : namespace detail {
      24             : 
      25             : process_expression parse_process_expression_new(const std::string& text);
      26             : process_specification parse_process_specification_new(const std::string& text);
      27             : void complete_process_specification(process_specification& x, bool alpha_reduce = false);
      28             : 
      29             : } // namespace detail
      30             : 
      31             : /// \brief Parses an action declaration from a string
      32             : /// \param text A string containing an action declaration
      33             : /// \param[in] data_spec A data specification used for sort normalization
      34             : /// \return A list of action labels
      35             : /// \exception mcrl2::runtime_error when the input does not match the syntax of an action declaration.
      36             : process::action_label_list parse_action_declaration(const std::string& text, const data::data_specification& data_spec = data::detail::default_specification());
      37             : 
      38             : /// \brief Parses a process specification from an input stream
      39             : /// \param in An input stream
      40             : /// \return The parse result
      41             : inline
      42             : process_specification
      43        1147 : parse_process_specification(std::istream& in)
      44             : {
      45        1147 :   std::string text = utilities::read_text(in);
      46        1147 :   process_specification result = detail::parse_process_specification_new(text);
      47        1146 :   detail::complete_process_specification(result);
      48        2258 :   return result;
      49        1164 : }
      50             : 
      51             : /// \brief Parses a process specification from a string
      52             : /// \param spec_string A string
      53             : /// \return The parse result
      54             : inline
      55             : process_specification
      56         977 : parse_process_specification(const std::string& spec_string)
      57             : {
      58         977 :   std::istringstream in(spec_string);
      59        1937 :   return parse_process_specification(in);
      60         977 : }
      61             : 
      62             : /// \brief Parses a process identifier.
      63             : inline
      64             : process_identifier parse_process_identifier(std::string text, const data::data_specification& dataspec)
      65             : {
      66             :   text = utilities::trim_copy(text);
      67             : 
      68             :   // unfortunately there is no grammar element for a process identifier, so parsing has to be done in an ad hoc manner
      69             :   auto pos = text.find('(');
      70             :   if (pos == std::string::npos)
      71             :   {
      72             :     return process_identifier(core::identifier_string(text), {});
      73             :   }
      74             :   std::string name    = text.substr(0, pos);
      75             :   std::string vardecl = utilities::trim_copy(text.substr(pos + 1));
      76             :   vardecl.pop_back();
      77             : 
      78             :   core::identifier_string id(name);
      79             :   data::variable_list variables = data::parse_variable_declaration_list(vardecl, dataspec);
      80             : 
      81             :   return process_identifier(id, variables);
      82             : }
      83             : 
      84             : /// \brief Parses and type checks a process expression.
      85             : /// \param[in] text The input text containing a process expression.
      86             : /// \param[in] data_decl A declaration of data and actions ("glob m:Nat; act a:Nat;").
      87             : /// \param[in] proc_decl A process declaration ("proc P(n: Nat);").
      88             : inline
      89          11 : process_expression parse_process_expression(const std::string& text,
      90             :                                             const std::string& data_decl,
      91             :                                             const std::string& proc_decl
      92             :                                            )
      93             : {
      94          22 :   std::string proc_text = utilities::regex_replace(";", " = delta;", proc_decl);
      95          11 :   std::string init_text = "init\n     " + text + ";\n";
      96          22 :   std::string spec_text = data_decl + "\n" + proc_text + "\n" + init_text;
      97          11 :   process_specification spec = parse_process_specification(spec_text);
      98          22 :   return spec.init();
      99          11 : }
     100             : 
     101             : /// \brief Parses and type checks a process expression.
     102             : /// \param[in] text The input text containing a process expression.
     103             : /// \param[in] procspec_text A textual version of a process specification used as context
     104             : inline
     105             : process_expression parse_process_expression(const std::string& text, const std::string& procspec_text)
     106             : {
     107             :   std::vector<std::string> keywords{"sort", "var", "eqn", "map", "cons", "act", "glob", "proc", "init"};
     108             :   std::pair<std::string, std::string> result = utilities::detail::separate_keyword_section(procspec_text, "init", keywords);
     109             :   std::string init_text = "init\n     " + text + ";\n";
     110             :   std::string ptext = result.second + init_text;
     111             :   process_specification spec = parse_process_specification(ptext);
     112             :   return spec.init();
     113             : }
     114             : 
     115             : /// \brief Parses and type checks a process expression. N.B. Very inefficient!
     116             : template <typename VariableContainer>
     117             : process_expression parse_process_expression(const std::string& text, const VariableContainer& variables, const process_specification& procspec)
     118             : {
     119             :   process_specification procspec1 = procspec;
     120             :   auto& globvars = procspec1.global_variables();
     121             :   globvars.insert(variables.begin(), variables.end());
     122             :   std::string ptext = process::pp(procspec1);
     123             :   ptext = utilities::regex_replace("\\binit.*;", "init " + text + ";", ptext);
     124             :   process_specification procspec2 =
     125             :       parse_process_specification(ptext);
     126             :   return procspec2.init();
     127             : }
     128             : 
     129             : template <typename VariableContainer, typename ActionLabelContainer, typename ProcessIdentifierContainer>
     130           3 : process_expression parse_process_expression(const std::string& text,
     131             :                                             const VariableContainer& variables = VariableContainer(),
     132             :                                             const data::data_specification& dataspec = data::data_specification(),
     133             :                                             const ActionLabelContainer& action_labels = std::vector<action_label>(),
     134             :                                             const ProcessIdentifierContainer& process_identifiers = ProcessIdentifierContainer(),
     135             :                                             const process_identifier* current_equation = nullptr
     136             :                                            )
     137             : {
     138           3 :   process_expression x = detail::parse_process_expression_new(text);
     139           3 :   x = typecheck_process_expression(x, variables, dataspec, action_labels, process_identifiers, current_equation);
     140           3 :   x = translate_user_notation(x);
     141           3 :   return x;
     142           0 : }
     143             : 
     144             : } // namespace process
     145             : 
     146             : } // namespace mcrl2
     147             : 
     148             : #endif // MCRL2_PROCESS_PARSE_H