replace_capture_avoiding.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// 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_MODAL_FORMULA_REPLACE_CAPTURE_AVOIDING_H
#define MCRL2_MODAL_FORMULA_REPLACE_CAPTURE_AVOIDING_H
 
#include "mcrl2/lps/replace_capture_avoiding.h"
#include "mcrl2/modal_formula/builder.h"
#include "mcrl2/modal_formula/find.h"
 
namespace mcrl2 {
 
namespace action_formulas {
 
namespace detail {
 
template <template <class> class Builder, class Derived, class Substitution>
struct add_capture_avoiding_replacement: public lps::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution>
{
  typedef lps::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution> super;
  using super::enter;
  using super::leave;
  using super::update;
  using super::apply;
  using super::sigma;
 
  explicit add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater<Substitution>& sigma)
    : super(sigma)
  { }
 
  template <class T>
  void apply(T& result, const forall& x)
  {
    data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
    action_formula body;
    apply(body, x.body());
    action_formulas::make_forall(result, v1, body);
    sigma.remove_fresh_variable_assignments(x.variables());
  }
 
  template <class T>
  void apply(T& result, const exists& x)
  {
    data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
    action_formula body;
    apply(body, x.body());
    action_formulas::make_exists(result, v1, body);
    sigma.remove_fresh_variable_assignments(x.variables());
  }
};
 
} // namespace detail
 
//--- start generated action_formulas replace_capture_avoiding code ---//
template <typename T, typename Substitution>
void replace_variables_capture_avoiding(T& x,
                                        Substitution& sigma,
                                        data::set_identifier_generator& id_generator,
                                        typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
)
{
  data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
  data::detail::apply_replace_capture_avoiding_variables_builder<action_formulas::data_expression_builder, action_formulas::detail::add_capture_avoiding_replacement>(sigma1).update(x);
}
 
template <typename T, typename Substitution>
T replace_variables_capture_avoiding(const T& x,
                                     Substitution& sigma,
                                     data::set_identifier_generator& id_generator,
                                     typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
)
{
  data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
  T result;
  data::detail::apply_replace_capture_avoiding_variables_builder<action_formulas::data_expression_builder, action_formulas::detail::add_capture_avoiding_replacement>(sigma1).apply(result, x);
  return result;
}
 
template <typename T, typename Substitution>
void replace_variables_capture_avoiding(T& x,
                                        Substitution& sigma,
                                        typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
)
{
  data::set_identifier_generator id_generator;
  id_generator.add_identifiers(action_formulas::find_identifiers(x));
  for (const data::variable& v: substitution_variables(sigma))
  {
    id_generator.add_identifier(v.name());
  }
  action_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
}
 
template <typename T, typename Substitution>
T replace_variables_capture_avoiding(const T& x,
                                     Substitution& sigma,
                                     typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
)
{
  data::set_identifier_generator id_generator;
  id_generator.add_identifiers(action_formulas::find_identifiers(x));
  for (const data::variable& v: substitution_variables(sigma))
  {
    id_generator.add_identifier(v.name());
  }
  return action_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
}
//--- end generated action_formulas replace_capture_avoiding code ---//
 
} // namespace action_formulas
 
} // namespace mcrl2
 
namespace mcrl2 {
 
namespace regular_formulas {
 
namespace detail {
 
template <template <class> class Builder, class Derived, class Substitution>
struct add_capture_avoiding_replacement: public action_formulas::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution>
{
  typedef action_formulas::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution> super;
  using super::enter;
  using super::leave;
  using super::update;
  using super::apply;
  using super::sigma;
 
  explicit add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater<Substitution>& sigma)
    : super(sigma)
  { }
};
 
} // namespace detail
 
//--- start generated regular_formulas replace_capture_avoiding code ---//
template <typename T, typename Substitution>
void replace_variables_capture_avoiding(T& x,
                                        Substitution& sigma,
                                        data::set_identifier_generator& id_generator,
                                        typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
)
{
  data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
  data::detail::apply_replace_capture_avoiding_variables_builder<regular_formulas::data_expression_builder, regular_formulas::detail::add_capture_avoiding_replacement>(sigma1).update(x);
}
 
template <typename T, typename Substitution>
T replace_variables_capture_avoiding(const T& x,
                                     Substitution& sigma,
                                     data::set_identifier_generator& id_generator,
                                     typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
)
{
  data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
  T result;
  data::detail::apply_replace_capture_avoiding_variables_builder<regular_formulas::data_expression_builder, regular_formulas::detail::add_capture_avoiding_replacement>(sigma1).apply(result, x);
  return result;
}
 
template <typename T, typename Substitution>
void replace_variables_capture_avoiding(T& x,
                                        Substitution& sigma,
                                        typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
)
{
  data::set_identifier_generator id_generator;
  id_generator.add_identifiers(regular_formulas::find_identifiers(x));
  for (const data::variable& v: substitution_variables(sigma))
  {
    id_generator.add_identifier(v.name());
  }
  regular_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
}
 
template <typename T, typename Substitution>
T replace_variables_capture_avoiding(const T& x,
                                     Substitution& sigma,
                                     typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
)
{
  data::set_identifier_generator id_generator;
  id_generator.add_identifiers(regular_formulas::find_identifiers(x));
  for (const data::variable& v: substitution_variables(sigma))
  {
    id_generator.add_identifier(v.name());
  }
  return regular_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
}
//--- end generated regular_formulas replace_capture_avoiding code ---//
 
} // namespace regular_formulas
 
} // namespace mcrl2
 
namespace mcrl2 {
 
namespace state_formulas {
 
namespace detail {
 
template <template <class> class Builder, class Derived, class Substitution>
struct add_capture_avoiding_replacement: public data::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution>
{
  typedef data::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution> super;
  using super::enter;
  using super::leave;
  using super::update;
  using super::apply;
  using super::sigma;
 
  explicit add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater<Substitution>& sigma)
    : super(sigma)
  { }
 
  state_formula operator()(const forall& x)
  {
    data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
    state_formula result = forall(v1, (*this)(x.body()));
    sigma.remove_fresh_variable_assignments(x.variables());
    return result;
  }
 
  state_formula operator()(const exists& x)
  {
    data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
    state_formula result = exists(v1, (*this)(x.body()));
    sigma.remove_fresh_variable_assignments(x.variables());
    return result;
  }
};
 
} // namespace detail
 
//--- start generated state_formulas replace_capture_avoiding code ---//
template <typename T, typename Substitution>
void replace_variables_capture_avoiding(T& x,
                                        Substitution& sigma,
                                        data::set_identifier_generator& id_generator,
                                        typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
)
{
  data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
  data::detail::apply_replace_capture_avoiding_variables_builder<state_formulas::data_expression_builder, state_formulas::detail::add_capture_avoiding_replacement>(sigma1).update(x);
}
 
template <typename T, typename Substitution>
T replace_variables_capture_avoiding(const T& x,
                                     Substitution& sigma,
                                     data::set_identifier_generator& id_generator,
                                     typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
)
{
  data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
  T result;
  data::detail::apply_replace_capture_avoiding_variables_builder<state_formulas::data_expression_builder, state_formulas::detail::add_capture_avoiding_replacement>(sigma1).apply(result, x);
  return result;
}
 
template <typename T, typename Substitution>
void replace_variables_capture_avoiding(T& x,
                                        Substitution& sigma,
                                        typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
)
{
  data::set_identifier_generator id_generator;
  id_generator.add_identifiers(state_formulas::find_identifiers(x));
  for (const data::variable& v: substitution_variables(sigma))
  {
    id_generator.add_identifier(v.name());
  }
  state_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
}
 
template <typename T, typename Substitution>
T replace_variables_capture_avoiding(const T& x,
                                     Substitution& sigma,
                                     typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
)
{
  data::set_identifier_generator id_generator;
  id_generator.add_identifiers(state_formulas::find_identifiers(x));
  for (const data::variable& v: substitution_variables(sigma))
  {
    id_generator.add_identifier(v.name());
  }
  return state_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
}
//--- end generated state_formulas replace_capture_avoiding code ---//
 
} // namespace state_formulas
 
} // namespace mcrl2
 
#endif // MCRL2_MODAL_FORMULA_REPLACE_CAPTURE_AVOIDING_H