Line data    Source code

       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/pbes/replace_capture_avoiding.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_REPLACE_CAPTURE_AVOIDING_H
      13             : #define MCRL2_PBES_REPLACE_CAPTURE_AVOIDING_H
      14             : 
      15             : #include "mcrl2/data/replace_capture_avoiding.h"
      16             : #include "mcrl2/pbes/builder.h"
      17             : #include "mcrl2/pbes/find.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace pbes_system {
      22             : 
      23             : namespace detail {
      24             : 
      25             : template<template<class> class Builder, class Derived, class Substitution>
      26             : struct add_capture_avoiding_replacement
      27             :   : public data::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution>
      28             : {
      29             :   typedef data::detail::add_capture_avoiding_replacement <Builder, Derived, Substitution> super;
      30             :   using super::enter;
      31             :   using super::leave;
      32             :   using super::update;
      33             :   using super::apply;
      34             :   using super::sigma;
      35             : 
      36         925 :   explicit add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater<Substitution>& sigma)
      37         925 :     : super(sigma)
      38         925 :   { }
      39             : 
      40             :   template <class T>
      41          30 :   void apply(T& result, const forall& x)
      42             :   {
      43          30 :     data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
      44          30 :     pbes_expression body;
      45          30 :     apply(body, x.body());
      46          30 :     make_forall(result, v1, body);
      47          30 :     sigma.remove_fresh_variable_assignments(x.variables());
      48          30 :   }
      49             : 
      50             :   template <class T>
      51          28 :   void apply(T& result, const exists& x)
      52             :   {
      53          28 :     data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
      54          28 :     pbes_expression body;
      55          28 :     apply(body, x.body());
      56          28 :     make_exists(result, v1, body);
      57          28 :     sigma.remove_fresh_variable_assignments(x.variables());
      58          28 :   }
      59             : 
      60             :   void update(pbes_equation& x)
      61             :   {
      62             :     data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variable().parameters());
      63             :     x.variable() = propositional_variable(x.variable().name(), v1);
      64             :     pbes_expression formula;
      65             :     apply(formula, x.formula());
      66             :     x.formula() = formula;
      67             :     sigma.remove_fresh_variable_assignments(x.variable().parameters());
      68             :   }
      69             : 
      70             :   void update(pbes& x)
      71             :   {
      72             :     data::variable_list v1 = sigma.add_fresh_variable_assignments(x.global_variables());
      73             :     x.global_variables() = std::set<data::variable>(v1.begin(), v1.end());
      74             :     update(x.equations());
      75             :     sigma.remove_fresh_variable_assignments(x.global_variables());
      76             :   }
      77             : };
      78             : 
      79             : } // namespace detail
      80             : 
      81             : //--- start generated pbes_system replace_capture_avoiding code ---//
      82             : /// \\brief Applies sigma as a capture avoiding substitution to x.
      83             : /// \\param x The object to which the subsitution is applied.
      84             : /// \\param sigma A substitution.
      85             : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
      86             : template <typename T, typename Substitution>
      87             : void replace_variables_capture_avoiding(T& x,
      88             :                                         Substitution& sigma,
      89             :                                         data::set_identifier_generator& id_generator,
      90             :                                         typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      91             : )
      92             : {
      93             :   data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
      94             :   data::detail::apply_replace_capture_avoiding_variables_builder<pbes_system::data_expression_builder, pbes_system::detail::add_capture_avoiding_replacement>(sigma1).update(x);
      95             : }
      96             : 
      97             : /// \\brief Applies sigma as a capture avoiding substitution to x.
      98             : /// \\param x The object to which the substiution is applied.
      99             : /// \\param sigma A substitution.
     100             : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
     101             : template <typename T, typename Substitution>
     102         925 : T replace_variables_capture_avoiding(const T& x,
     103             :                                      Substitution& sigma,
     104             :                                      data::set_identifier_generator& id_generator,
     105             :                                      typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     106             : )
     107             : {
     108         925 :   data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
     109         925 :   T result;
     110         925 :   data::detail::apply_replace_capture_avoiding_variables_builder<pbes_system::data_expression_builder, pbes_system::detail::add_capture_avoiding_replacement>(sigma1).apply(result, x);
     111        1850 :   return result;
     112         925 : }
     113             : 
     114             : /// \\brief Applies sigma as a capture avoiding substitution to x.
     115             : /// \\param x The object to which the subsitution is applied.
     116             : /// \\param sigma A substitution.
     117             : template <typename T, typename Substitution>
     118             : void replace_variables_capture_avoiding(T& x,
     119             :                                         Substitution& sigma,
     120             :                                         typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     121             : )
     122             : {
     123             :   data::set_identifier_generator id_generator;
     124             :   id_generator.add_identifiers(pbes_system::find_identifiers(x));
     125             :   for (const data::variable& v: substitution_variables(sigma))
     126             :   {
     127             :     id_generator.add_identifier(v.name());
     128             :   }
     129             :   pbes_system::replace_variables_capture_avoiding(x, sigma, id_generator);
     130             : }
     131             : 
     132             : /// \\brief Applies sigma as a capture avoiding substitution to x.
     133             : /// \\param x The object to which the substiution is applied.
     134             : /// \\param sigma A substitution.
     135             : template <typename T, typename Substitution>
     136         925 : T replace_variables_capture_avoiding(const T& x,
     137             :                                      Substitution& sigma,
     138             :                                      typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     139             : )
     140             : {
     141         925 :   data::set_identifier_generator id_generator;
     142         925 :   id_generator.add_identifiers(pbes_system::find_identifiers(x));
     143        1653 :   for (const data::variable& v: substitution_variables(sigma))
     144             :   {
     145         728 :     id_generator.add_identifier(v.name());
     146             :   }
     147        1850 :   return pbes_system::replace_variables_capture_avoiding(x, sigma, id_generator);
     148         925 : }
     149             : //--- end generated pbes_system replace_capture_avoiding code ---//
     150             : 
     151             : } // namespace pbes_system
     152             : 
     153             : } // namespace mcrl2
     154             : 
     155             : #endif // MCRL2_PBES_REPLACE_CAPTURE_AVOIDING_H