data_expression.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_DATA_EXPRESSION_H
#define MCRL2_DATA_DATA_EXPRESSION_H
 
#include "mcrl2/data/container_sort.h"
#include "mcrl2/data/function_sort.h"
#include "mcrl2/data/untyped_sort.h"
 
namespace mcrl2
{
 
namespace data
{
 
inline bool is_abstraction(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Binder;
}
 
inline bool is_lambda(const atermpp::aterm& x)
{
  return is_abstraction(x) && x[0].function() == core::detail::function_symbols::Lambda;
}
 
inline bool is_forall(const atermpp::aterm& x)
{
  return is_abstraction(x) && x[0].function() == core::detail::function_symbols::Forall;
}
 
inline bool is_exists(const atermpp::aterm& x)
{
  return is_abstraction(x) && x[0].function() == core::detail::function_symbols::Exists;
}
 
inline bool is_set_comprehension(const atermpp::aterm& x)
{
  return is_abstraction(x) && x[0].function() == core::detail::function_symbols::SetComp;
}
 
inline bool is_bag_comprehension(const atermpp::aterm& x)
{
  return is_abstraction(x) && x[0].function() == core::detail::function_symbols::BagComp;
}
 
inline bool is_untyped_set_or_bag_comprehension(const atermpp::aterm& x)
{
  return is_abstraction(x) && x[0].function() == core::detail::function_symbols::UntypedSetBagComp;
}
 
inline bool is_function_symbol(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::OpId;
}
 
inline bool is_variable(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::DataVarId;
}
 
inline bool is_machine_number(const atermpp::aterm& x)
{
  return x.type_is_int();
}
 
inline bool is_application(const atermpp::aterm& x)
{
  return core::detail::gsIsDataAppl(x);
}
 
inline bool is_application_no_check(const atermpp::aterm& x)
{
  return core::detail::gsIsDataAppl_no_check(x);
}
 
inline bool is_where_clause(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::Whr;
}
 
inline bool is_untyped_identifier(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::UntypedIdentifier;
}
 
class application; // prototype
 
 
//--- start generated class data_expression ---//
class data_expression: public atermpp::aterm
{
  public:
    data_expression()
      : atermpp::aterm(core::detail::default_values::DataExpr)
    {}
 
    explicit data_expression(const atermpp::aterm& term)
      : atermpp::aterm(term)
    {
      assert(core::detail::check_rule_DataExpr(*this));
    }
 
    data_expression(const data_expression&) noexcept = default;
    data_expression(data_expression&&) noexcept = default;
    data_expression& operator=(const data_expression&) noexcept = default;
    data_expression& operator=(data_expression&&) noexcept = default;
//--- start user section data_expression ---//
    bool is_default_data_expression() const
    {
      return *this==core::detail::default_values::DataExpr;
    }
 
    application operator()(const data_expression& e) const;
 
    application operator()(const data_expression& e1,
                           const data_expression& e2) const;
 
    application operator()(const data_expression& e1,
                           const data_expression& e2,
                           const data_expression& e3) const;
 
    application operator()(const data_expression& e1,
                           const data_expression& e2,
                           const data_expression& e3,
                           const data_expression& e4) const;
 
    application operator()(const data_expression& e1,
                           const data_expression& e2,
                           const data_expression& e3,
                           const data_expression& e4,
                           const data_expression& e5) const;
 
    application operator()(const data_expression& e1,
                           const data_expression& e2,
                           const data_expression& e3,
                           const data_expression& e4,
                           const data_expression& e5,
                           const data_expression& e6) const;
 
    sort_expression sort() const;
 
    private:
      // The following methods are not to be used in a data_expression.
      // They are restricted to a data_appl. 
      const_iterator begin() const;
      const_iterator end() const;
 
//--- end user section data_expression ---//
};
 
typedef atermpp::term_list<data_expression> data_expression_list;
 
typedef std::vector<data_expression>    data_expression_vector;
 
// prototype declaration
std::string pp(const data_expression& x);
 
inline
std::ostream& operator<<(std::ostream& out, const data_expression& x)
{
  return out << data::pp(x);
}
 
inline void swap(data_expression& t1, data_expression& t2)
{
  t1.swap(t2);
}
//--- end generated class data_expression ---//
 
inline void make_data_expression(data_expression& result)
{
  static_cast<atermpp::aterm&>(result)=core::detail::default_values::DataExpr;
}
 
inline
bool is_data_expression(const atermpp::aterm& x)
{
  return is_machine_number(x)                   ||
         is_lambda(x)                           ||
         is_forall(x)                           ||
         is_exists(x)                           ||
         is_set_comprehension(x)                ||
         is_bag_comprehension(x)                ||
         is_untyped_set_or_bag_comprehension(x) ||
         is_function_symbol(x)                  ||
         is_variable(x)                         ||
         is_application(x)                      ||
         is_where_clause(x)                     ||
         is_untyped_identifier(x);
}
 
template < typename Container >
inline data_expression_list make_data_expression_list(Container const& r, typename atermpp::enable_if_container< Container, data_expression >::type* = nullptr)
{
  return data_expression_list(r.begin(),r.end());
}
 
class variable;
 
// template function overloads
std::string pp(const data_expression_list& x);
std::string pp(const data_expression_vector& x);
data::data_expression translate_user_notation(const data::data_expression& x);
std::set<data::sort_expression> find_sort_expressions(const data::data_expression& x);
std::set<data::variable> find_all_variables(const data::data_expression& x);
std::set<data::variable> find_all_variables(const data::data_expression_list& x);
std::set<data::variable> find_free_variables(const data::data_expression& x);
std::set<data::variable> find_free_variables(const data::data_expression_list& x);
bool search_variable(const data::data_expression& x, const data::variable& v);
 
inline
bool is_constant(const data_expression& x)
{
  return find_free_variables(x).empty();
}
 
typedef atermpp::term_list<variable> variable_list;
variable_list free_variables(const data_expression& x);
 
} // namespace data
 
} // namespace mcrl2
 
// The trick of including application.h only at this point is needed to break
// the circular dependencies between application and data_expression. This
// dependency was introduced to allow the application operator to be defined for
// all data expression types.
#ifndef MCRL2_DATA_APPLICATION_H
#include "mcrl2/data/application.h"
#endif
 
namespace mcrl2
{
namespace data
{
inline bool is_application(const data_expression& t)
{
  return !(is_machine_number(t) ||
           is_function_symbol(t) ||
           is_variable(t) ||
           is_where_clause(t) ||
           is_abstraction(t) ||
           is_untyped_identifier(t));
} 
 
inline 
const data_expression_list& variable_list_to_data_expression_list(const variable_list& l)
{
  return atermpp::down_cast<data_expression_list>(static_cast<const atermpp::aterm&>(l));
}
 
inline
application data_expression::operator()(const data_expression& e) const
{
  return application(*this, e);
}
 
inline
application data_expression::operator()(const data_expression& e1, const data_expression& e2) const
{
  return application(*this, e1, e2);
}
 
inline
application data_expression::operator()(const data_expression& e1, const data_expression& e2, const data_expression& e3) const
{
  return application(*this, e1, e2, e3);
}
 
inline
application data_expression::operator()(const data_expression& e1, const data_expression& e2, const data_expression& e3, const data_expression& e4) const
{
  return application(*this, e1, e2, e3, e4);
}
 
inline
application data_expression::operator()(const data_expression& e1, const data_expression& e2, const data_expression& e3, const data_expression& e4, const data_expression& e5) const
{
  return application(*this, e1, e2, e3, e4, e5);
}
 
inline
application data_expression::operator()(const data_expression& e1, const data_expression& e2, const data_expression& e3, 
                                        const data_expression& e4, const data_expression& e5, const data_expression& e6) const
{
  return application(*this, e1, e2, e3, e4, e5, e6);
}
 
} // namespace data
} // namespace mcrl2
 
 
namespace std
{
 
template<>
struct hash<mcrl2::data::data_expression>
{
    std::size_t operator()(const mcrl2::data::data_expression& v) const
    {
      const hash<atermpp::aterm> hasher;
      return hasher(v);
    }
};
 
} // namespace std
 
 
 
#endif // MCRL2_DATA_DATA_EXPRESSION_H