assignment.h

Go to the documentation of this file.

// Author(s): Jeroen Keiren
// 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_ASSIGNMENT_H
#define MCRL2_DATA_ASSIGNMENT_H
 
#include "mcrl2/data/undefined.h"
#include "mcrl2/data/untyped_identifier.h"
 
namespace mcrl2
{
 
namespace data
{
 
//--- start generated classes ---//
class assignment_expression: public atermpp::aterm
{
  public:
    assignment_expression()
      : atermpp::aterm(core::detail::default_values::WhrDecl)
    {}
 
    explicit assignment_expression(const atermpp::aterm& term)
      : atermpp::aterm(term)
    {
      assert(core::detail::check_rule_WhrDecl(*this));
    }
 
    assignment_expression(const assignment_expression&) noexcept = default;
    assignment_expression(assignment_expression&&) noexcept = default;
    assignment_expression& operator=(const assignment_expression&) noexcept = default;
    assignment_expression& operator=(assignment_expression&&) noexcept = default;
};
 
typedef atermpp::term_list<assignment_expression> assignment_expression_list;
 
typedef std::vector<assignment_expression>    assignment_expression_vector;
 
// prototypes
inline bool is_assignment(const atermpp::aterm& x);
inline bool is_untyped_identifier_assignment(const atermpp::aterm& x);
 
inline
bool is_assignment_expression(const atermpp::aterm& x)
{
  return data::is_assignment(x) ||
         data::is_untyped_identifier_assignment(x);
}
 
// prototype declaration
std::string pp(const assignment_expression& x);
 
inline
std::ostream& operator<<(std::ostream& out, const assignment_expression& x)
{
  return out << data::pp(x);
}
 
inline void swap(assignment_expression& t1, assignment_expression& t2)
{
  t1.swap(t2);
}
 
 
class assignment: public assignment_expression
{
  public:
    assignment()
      : assignment_expression(core::detail::default_values::DataVarIdInit)
    {}
 
    explicit assignment(const atermpp::aterm& term)
      : assignment_expression(term)
    {
      assert(core::detail::check_term_DataVarIdInit(*this));
    }
 
    assignment(const variable& lhs, const data_expression& rhs)
      : assignment_expression(atermpp::aterm(core::detail::function_symbol_DataVarIdInit(), lhs, rhs))
    {}
 
    assignment(const assignment&) noexcept = default;
    assignment(assignment&&) noexcept = default;
    assignment& operator=(const assignment&) noexcept = default;
    assignment& operator=(assignment&&) noexcept = default;
 
    const variable& lhs() const
    {
      return atermpp::down_cast<variable>((*this)[0]);
    }
 
    const data_expression& rhs() const
    {
      return atermpp::down_cast<data_expression>((*this)[1]);
    }
//--- start user section assignment ---//
    const data_expression& operator()(const variable& x) const
    {
      return x == lhs() ? rhs() : x;
    }
//--- end user section assignment ---//
};
 
template <class... ARGUMENTS>
inline void make_assignment(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_DataVarIdInit(), args...);
}
 
typedef atermpp::term_list<assignment> assignment_list;
 
typedef std::vector<assignment>    assignment_vector;
 
inline
bool is_assignment(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::DataVarIdInit;
}
 
// prototype declaration
std::string pp(const assignment& x);
 
inline
std::ostream& operator<<(std::ostream& out, const assignment& x)
{
  return out << data::pp(x);
}
 
inline void swap(assignment& t1, assignment& t2)
{
  t1.swap(t2);
}
 
 
class untyped_identifier_assignment: public assignment_expression
{
  public:
    untyped_identifier_assignment()
      : assignment_expression(core::detail::default_values::UntypedIdentifierAssignment)
    {}
 
    explicit untyped_identifier_assignment(const atermpp::aterm& term)
      : assignment_expression(term)
    {
      assert(core::detail::check_term_UntypedIdentifierAssignment(*this));
    }
 
    untyped_identifier_assignment(const core::identifier_string& lhs, const data_expression& rhs)
      : assignment_expression(atermpp::aterm(core::detail::function_symbol_UntypedIdentifierAssignment(), lhs, rhs))
    {}
 
    untyped_identifier_assignment(const std::string& lhs, const data_expression& rhs)
      : assignment_expression(atermpp::aterm(core::detail::function_symbol_UntypedIdentifierAssignment(), core::identifier_string(lhs), rhs))
    {}
 
    untyped_identifier_assignment(const untyped_identifier_assignment&) noexcept = default;
    untyped_identifier_assignment(untyped_identifier_assignment&&) noexcept = default;
    untyped_identifier_assignment& operator=(const untyped_identifier_assignment&) noexcept = default;
    untyped_identifier_assignment& operator=(untyped_identifier_assignment&&) noexcept = default;
 
    const core::identifier_string& lhs() const
    {
      return atermpp::down_cast<core::identifier_string>((*this)[0]);
    }
 
    const data_expression& rhs() const
    {
      return atermpp::down_cast<data_expression>((*this)[1]);
    }
//--- start user section untyped_identifier_assignment ---//
    data_expression operator()(const untyped_identifier& x) const
    {
      return x == lhs() ? rhs() : data_expression(x);
    }
//--- end user section untyped_identifier_assignment ---//
};
 
template <class... ARGUMENTS>
inline void make_untyped_identifier_assignment(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_UntypedIdentifierAssignment(), args...);
}
 
typedef atermpp::term_list<untyped_identifier_assignment> untyped_identifier_assignment_list;
 
typedef std::vector<untyped_identifier_assignment>    untyped_identifier_assignment_vector;
 
inline
bool is_untyped_identifier_assignment(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::UntypedIdentifierAssignment;
}
 
// prototype declaration
std::string pp(const untyped_identifier_assignment& x);
 
inline
std::ostream& operator<<(std::ostream& out, const untyped_identifier_assignment& x)
{
  return out << data::pp(x);
}
 
inline void swap(untyped_identifier_assignment& t1, untyped_identifier_assignment& t2)
{
  t1.swap(t2);
}
//--- end generated classes ---//
 
template < typename VariableSequence, typename ExpressionSequence >
assignment_vector make_assignment_vector(VariableSequence const& variables, ExpressionSequence const& expressions)
{
  std::vector<assignment> result;
  typename ExpressionSequence::const_iterator j=expressions.begin();
  for(typename VariableSequence::const_iterator i=variables.begin(); i!=variables.end(); ++i, ++j)
  {
    assert(j!=expressions.end());
    result.push_back(assignment(*i,*j));
  }
  assert(j==expressions.end());
  return result;
}
 
template < typename VariableSequence, typename ExpressionSequence >
assignment_list make_assignment_list(const VariableSequence& variables, const ExpressionSequence& expressions)
{
  std::vector<assignment> result(make_assignment_vector(variables,expressions));
  return assignment_list(result.begin(),result.end());
}
 
inline
variable_list left_hand_sides(const assignment_list& x)
{
  return variable_list(x.begin(), x.end(), [](const assignment& a) { return a.lhs(); });
}
 
inline
data_expression_list right_hand_sides(const assignment_list& x)
{
  return data_expression_list(x.begin(), x.end(), [](const assignment& a) { return a.rhs(); });
}
 
// template function overloads
std::string pp(const assignment_list& x);
std::string pp(const assignment_vector& x);
 
} // namespace data
 
} // namespace mcrl2
 
#endif // MCRL2_DATA_ASSIGNMENT_H