parse.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink, Jeroen Keiren, Jan Friso Groote
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_DATA_PARSE_H
#define MCRL2_DATA_PARSE_H
 
#include "mcrl2/data/typecheck.h"
 
namespace mcrl2
{
 
namespace data
{
 
namespace detail {
 
sort_expression parse_sort_expression(const std::string& text);
variable_list parse_variables(const std::string& text);
data_expression parse_data_expression(const std::string& text);
data_specification parse_data_specification_new(const std::string& text);
variable_list parse_variable_declaration_list(const std::string& text);
 
inline static data_specification const& default_specification()
{
  static data_specification specification;
  return specification;
}
 
} // namespace detail
 
std::pair<basic_sort_vector, alias_vector> parse_sort_specification(const std::string& text);
 
inline
data_specification parse_data_specification(std::istream& in)
{
  std::string text = utilities::read_text(in);
  data_specification result = detail::parse_data_specification_new(text);
  typecheck_data_specification(result);
  result.translate_user_notation();
  return result;
}
 
inline
data_specification parse_data_specification(const std::string& text)
{
  // handle empty data specification
  if (utilities::trim_copy(text).empty())
  {
    return data_specification();
  }
  std::istringstream spec_stream(text);
  return parse_data_specification(spec_stream);
}
 
 
template <typename OutputIterator, typename VariableIterator>
void parse_variables(std::istream& in,
                     OutputIterator o,
                     VariableIterator begin,
                     VariableIterator end,
                     const data_specification& data_spec = detail::default_specification())
{
  std::string text = utilities::read_text(in);
  utilities::trim(text);
  variable_list data_vars;
 
  if (!text.empty())
  {
    data_vars = detail::parse_variables(text);
    data_type_checker type_checker(data_spec);
    // Check the variable in an empty variable context.
    type_checker(data_vars,detail::variable_context());
 
    // Undo sort renamings for compatibility with type checker
    // data_vars = data::detail::undo_compatibility_renamings(data_spec, data_vars);
    data_vars = atermpp::reverse(data_vars);
    data_vars = normalize_sorts(data_vars, data_spec);
 
    // Check that variables do not have equal names.
    for (const variable& v: data_vars)
    {
      for (VariableIterator i = begin; i != end; ++i)
      {
        if (v.name()==i->name())
        {
          throw mcrl2::runtime_error("Name conflict of variables " + data::pp(*i) + " and " + data::pp(v) + ".");
        }
      }
      for (const variable& v1: data_vars)
      {
        if ((v1 != v) && (v1.name() == v.name()))
        {
          throw mcrl2::runtime_error("Name conflict of variables " + data::pp(v1) + " and " + data::pp(v) + ".");
        }
      }
    }
  }
 
  // Output the variables read via the Output iterator.
  std::copy(data_vars.begin(), data_vars.end(), o);
}
 
 
template <typename OutputIterator, typename VariableIterator>
void parse_variables(const std::string& text,
                     OutputIterator i,
                     VariableIterator begin,
                     VariableIterator end,
                     const data_specification& data_spec = detail::default_specification())
{
  std::istringstream spec_stream(text);
  parse_variables(spec_stream, i, begin, end, data_spec);
}
 
 
template <typename OutputIterator>
void parse_variables(std::istream& text,
                     OutputIterator i,
                     const data_specification& data_spec = detail::default_specification())
{
  variable_list v_list;
  parse_variables(text,i,v_list.begin(),v_list.end(),data_spec);
}
 
 
template <typename OutputIterator>
void parse_variables(const std::string& text,
                     OutputIterator i,
                     const data_specification& data_spec = detail::default_specification())
{
  variable_list v_list;
  parse_variables(text, i, v_list.begin(), v_list.end(), data_spec);
}
 
inline
variable parse_variable(const std::string& text,
                        const data_specification& data_spec = detail::default_specification())
{
  std::vector<variable> v;
 
  parse_variables(text + ";", std::back_inserter(v),data_spec);
 
  if (v.empty())
  {
    throw mcrl2::runtime_error("Input does not contain a variable declaration.");
  }
  if (v.size() > 1)
  {
    throw mcrl2::runtime_error("Input contains more than one variable declaration.");
  }
 
  return v.front();
}
 
inline
variable parse_variable(std::istream& text,
                        const data_specification& data_spec = detail::default_specification())
{
  std::ostringstream input;
  input << text.rdbuf();
  return parse_variable(input.str(),data_spec);
}
 
template <typename VariableContainer>
data_expression parse_data_expression(std::istream& in,
                                      const VariableContainer& variables,
                                      const data_specification& dataspec = detail::default_specification(),
                                      bool type_check = true,
                                      bool translate_user_notation = true,
                                      bool normalize_sorts = true
                                     )
{
  std::string text = utilities::read_text(in);
  data_expression x = detail::parse_data_expression(text);
  if (type_check)
  {
    x = data::typecheck_data_expression(x, variables, dataspec);
  }
  if (translate_user_notation)
  {
    x = data::translate_user_notation(x);
  }
  if (normalize_sorts)
  {
    x = data::normalize_sorts(x, dataspec);
  }
  return x;
}
 
template <typename VariableContainer>
data_expression parse_data_expression(const std::string& text,
                                      const VariableContainer& variables,
                                      const data_specification& data_spec = detail::default_specification(),
                                      bool type_check = true,
                                      bool translate_user_notation = true,
                                      bool normalize_sorts = true
                                     )
{
  std::istringstream spec_stream(text);
  return parse_data_expression(spec_stream, variables, data_spec, type_check, translate_user_notation, normalize_sorts);
}
 
inline
data_expression parse_data_expression(std::istream& text,
                                      const data_specification& data_spec = detail::default_specification(),
                                      bool type_check = true,
                                      bool translate_user_notation = true,
                                      bool normalize_sorts = true
                                     )
{
  return parse_data_expression(text, variable_list(), data_spec, type_check, translate_user_notation, normalize_sorts);
}
 
inline
data_expression parse_data_expression(const std::string& text,
                                      const data_specification& data_spec = detail::default_specification(),
                                      bool type_check = true,
                                      bool translate_user_notation = true,
                                      bool normalize_sorts = true
                                     )
{
  return parse_data_expression(text, variable_list(), data_spec, type_check, translate_user_notation, normalize_sorts);
}
 
inline
variable_list parse_variables(const std::string& text)
{
  std::vector<variable> result;
  if (!text.empty())
  {
    parse_variables(text, std::back_inserter(result));
  }
  return variable_list(result.begin(), result.end());
}
 
inline
sort_expression parse_sort_expression(std::istream& in,
                                      const data_specification& data_spec = detail::default_specification())
{
  std::string text = utilities::read_text(in);
  sort_expression x = detail::parse_sort_expression(text);
  typecheck_sort_expression(x, data_spec);
  x = normalize_sorts(x, data_spec);
  return x;
}
 
inline
sort_expression parse_sort_expression(const std::string& text,
                                      const data_specification& data_spec = detail::default_specification())
{
  std::istringstream spec_stream(text);
  return parse_sort_expression(spec_stream, data_spec);
}
 
// parse a string like 'tail: List(D) -> List(D)'
//
// TODO: replace this by a proper parse function once the current parser and type checker have been replaced
inline
data::function_symbol parse_function_symbol(const std::string& text, const std::string& dataspec_text = "")
{
  const std::string prefix = "UNIQUE_FUNCTION_SYMBOL_PREFIX";
  std::string s = utilities::trim_copy(text);
  std::string::size_type pos = s.find_first_of(':');
  std::string name = utilities::trim_copy(s.substr(0, pos));
  std::string type = prefix + s.substr(pos);
  std::string spec_text = dataspec_text + "\nmap " + prefix + type + ";\n";
  data::data_specification dataspec = data::parse_data_specification(spec_text);
  data::function_symbol f = dataspec.user_defined_mappings().back();
  data::function_symbol result = data::function_symbol(name, f.sort());
  return result;
}
 
inline
variable_list parse_variable_declaration_list(const std::string& text, const data_specification& dataspec = detail::default_specification())
{
  variable_list variables = detail::parse_variable_declaration_list(text);
  variables = normalize_sorts(variables, dataspec);
  return variables;
}
 
namespace detail
{
 
inline
std::pair<std::string, data_expression_list> parse_variable(std::string const& text)
{
  std::string name;
  data_expression_vector variables;
 
  std::string::size_type idx = text.find('(');
  if (idx == std::string::npos)
  {
    name = text;
  }
  else
  {
    name = text.substr(0, idx);
    assert(*text.rbegin() == ')');
    std::string w = text.substr(idx + 1, text.size() - idx - 2);
    std::vector<std::string> v = utilities::split(w, ",");
    for (const std::string& s: v)
    {
      variables.push_back(data::parse_variable(s));
    }
  }
  return std::make_pair(name, data_expression_list(variables.begin(), variables.end()));
}
 
} // namespace detail
 
} // namespace data
 
} // namespace mcrl2
 
#endif // MCRL2_DATA_PARSE_H