standard_container_utility.h

Go to the documentation of this file.

// Author(s): Jeroen van der Wulp
// 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_STANDARD_CONTAINER_UTILITY_H
#define MCRL2_DATA_STANDARD_CONTAINER_UTILITY_H
 
#include "mcrl2/utilities/detail/join.h"
 
#include "mcrl2/data/bag.h"
#include "mcrl2/data/list.h"
 
namespace mcrl2
{
 
namespace data
{
 
namespace sort_list
{
//
template < typename Sequence >
inline
application list(const sort_expression& s,
                 Sequence const& range,
                 typename atermpp::enable_if_container< Sequence, data_expression >::type* = nullptr)
{
  data_expression                list_expression(empty(s));
  std::vector< data_expression > elements(range.begin(), range.end());
 
  for (std::vector< data_expression >::reverse_iterator i = elements.rbegin(); i != elements.rend(); ++i)
  {
    list_expression = sort_list::cons_(s, *i, list_expression);
  }
 
  return static_cast< application >(list_expression);
}
 
inline
core::identifier_string const& list_enumeration_name()
{
  static core::identifier_string list_enumeration_name = core::identifier_string("@ListEnum");
  return list_enumeration_name;
}
 
inline
function_symbol list_enumeration(const sort_expression& s)
{
  function_symbol list_enumeration(list_enumeration_name(), s);
  return list_enumeration;
}
 
inline
bool is_list_enumeration_function_symbol(const atermpp::aterm& e)
{
  if (is_function_symbol(e))
  {
    return function_symbol(e).name() == list_enumeration_name();
  }
  return false;
}
 
template <typename Sequence>
inline
data_expression list_enumeration(const sort_expression& s,
                                 Sequence const& range,
                                 typename atermpp::enable_if_container< Sequence, data_expression >::type* = nullptr)
{
  if (range.empty())
  {
    return list_enumeration(s);
  }
  else
  {
    sort_expression_vector v(range.size(), range.begin()->sort());
 
    return application(list_enumeration(function_sort(v,s)), range);
  }
}
 
inline
data_expression list_enumeration(const sort_expression& s, data_expression_list const& range)
{
  if (range.empty())
  {
    return list_enumeration(s);
  }
  else
  {
    sort_expression_vector v(range.size(), range.begin()->sort());
 
    return application(list_enumeration(function_sort(v,s)), range);
  }
}
 
inline
bool is_list_enumeration_application(const atermpp::aterm& e)
{
  if (is_application(e))
  {
    return is_list_enumeration_function_symbol(application(e).head());
  }
  return false;
}
} // namespace sort_list
 
namespace sort_set
{
inline
core::identifier_string const& set_enumeration_name()
{
  static core::identifier_string set_enumeration_name = core::identifier_string("@SetEnum");
  return set_enumeration_name;
}
 
inline
function_symbol set_enumeration(const sort_expression& s)
{
  function_symbol set_enumeration(set_enumeration_name(), s);
  return set_enumeration;
}
 
inline
bool is_set_enumeration_function_symbol(const atermpp::aterm& e)
{
  if (is_function_symbol(e))
  {
    return function_symbol(e).name() == set_enumeration_name();
  }
  return false;
}
 
template <typename Sequence>
inline
data_expression set_enumeration(const sort_expression& s,
                                Sequence const& range,
                                typename atermpp::enable_if_container< Sequence, data_expression >::type* = 0)
{
  if (range.empty())
  {
    return set_enumeration(sort_fset::fset(s));
  }
  else
  {
    sort_expression_vector v(range.size(), range.begin()->sort());
 
    return application(set_enumeration(function_sort(v,sort_fset::fset(s))), range);
  }
}
 
inline
data_expression set_enumeration(const sort_expression& s,
                                data_expression_list const& range)
{
  if (range.empty())
  {
    return set_enumeration(sort_fset::fset(s));
  }
  else
  {
    sort_expression_vector v(range.size(), range.begin()->sort());
 
    return application(set_enumeration(function_sort(v,sort_fset::fset(s))), range);
  }
}
 
inline
bool is_set_enumeration_application(const atermpp::aterm& e)
{
  if (is_application(e))
  {
    return is_set_enumeration_function_symbol(application(e).head());
  }
  return false;
}
} // namespace sort_set
 
namespace sort_fset
{
 
//
template < typename Sequence >
inline
application fset(const sort_expression& s,
                 Sequence const& range,
                 typename atermpp::enable_if_container< Sequence, data_expression >::type* = nullptr)
{
  data_expression fset_expression(sort_fset::empty(s));
 
  // We process the elements in reverse order to have a resulting enumeration
  // in the same order as the input
  for (typename Sequence::const_reverse_iterator i = range.rbegin(); i != range.rend(); ++i)
  {
    fset_expression = sort_fset::insert(s, *i, fset_expression);
  }
 
  return static_cast< application >(fset_expression);
}
 
//
inline
application fset(const sort_expression& s,
                 const data_expression_list& range)
{
  return fset(s, data_expression_vector(range.begin(),range.end()));
}
 
} // namespace sort_fset
 
namespace sort_bag
{
inline
core::identifier_string const& bag_enumeration_name()
{
  static core::identifier_string bag_enumeration_name = core::identifier_string("@BagEnum");
  return bag_enumeration_name;
}
 
inline
function_symbol bag_enumeration(const sort_expression& s)
{
  function_symbol bag_enumeration(bag_enumeration_name(), s);
  return bag_enumeration;
}
 
inline
bool is_bag_enumeration_function_symbol(const atermpp::aterm& e)
{
  if (is_function_symbol(e))
  {
    return function_symbol(e).name() == bag_enumeration_name();
  }
  return false;
}
 
template <typename Sequence>
inline
data_expression bag_enumeration(const sort_expression& s,
                                Sequence const& range,
                                typename atermpp::enable_if_container< Sequence, data_expression >::type* = 0)
{
  if (range.empty())
  {
    return bag_enumeration(sort_fbag::fbag(s));
  }
  else
  {
    assert(range.size() % 2 == 0);
    sort_expression t(range.begin()->sort());
 
    sort_expression_vector v;
 
    for (std::size_t i = 0; i < range.size() / 2; ++i)
    {
      v.push_back(t);
      v.push_back(sort_nat::nat());
    }
 
    return application(bag_enumeration(function_sort(v,sort_fbag::fbag(s))), range);
  }
}
 
inline
data_expression bag_enumeration(const sort_expression& s,
                                data_expression_list const& range)
{
  if (range.empty())
  {
    return bag_enumeration(sort_fbag::fbag(s));
  }
  else
  {
    assert(range.size() % 2 == 0);
    sort_expression t(range.begin()->sort());
    sort_expression_vector v;
 
    for (std::size_t i = 0; i < range.size() / 2; ++i)
    {
      v.push_back(t);
      v.push_back(sort_nat::nat());
    }
 
    return application(bag_enumeration(function_sort(v,sort_fbag::fbag(s))), range);
  }
}
 
inline
bool is_bag_enumeration_application(const atermpp::aterm& e)
{
  if (is_application(e))
  {
    return is_bag_enumeration_function_symbol(application(e).head());
  }
  return false;
}
 
} // namespace sort_bag
 
namespace sort_fbag
{
template < typename Sequence >
inline
application fbag(const sort_expression& s, Sequence const& range,
                 typename atermpp::enable_if_container< Sequence, data_expression >::type* = nullptr)
{
  data_expression fbag_expression(sort_fbag::empty(s));
 
  // The sequence contains element, count, ...
  // As we process the list in reverse, we have count, element, ...
  // We process the elements in reverse order to have a resulting enumeration
  // in the same order as the input
  for (typename Sequence::const_reverse_iterator i = range.rbegin(); i != range.rend(); ++i, ++i)
  {
    fbag_expression = sort_fbag::cinsert(s, *std::next(i, 1), *i, fbag_expression);
  }
 
  return static_cast< application >(fbag_expression);
}
 
inline
application fbag(const sort_expression& s, const data_expression_list& range)
{
  return fbag(s, data_expression_vector(range.begin(),range.end()));
}
} // namespace sort_fbag
 
} // namespace data
 
} // namespace mcrl2
 
#endif