LCOV - code coverage report
Current view: top level - modal_formula/include/mcrl2/modal_formula - replace_capture_avoiding.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 12 22 54.5 %
Date: 2020-04-01 00:44:46 Functions: 3 5 60.0 %
Legend: Lines: hit not hit

          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/modal_formula/replace_capture_avoiding.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_REPLACE_CAPTURE_AVOIDING_H
      13             : #define MCRL2_MODAL_FORMULA_REPLACE_CAPTURE_AVOIDING_H
      14             : 
      15             : #include "mcrl2/lps/replace_capture_avoiding.h"
      16             : #include "mcrl2/modal_formula/builder.h"
      17             : #include "mcrl2/modal_formula/find.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace action_formulas {
      22             : 
      23             : namespace detail {
      24             : 
      25             : template <template <class> class Builder, class Derived, class Substitution>
      26             : struct add_capture_avoiding_replacement: public lps::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution>
      27             : {
      28             :   typedef lps::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution> super;
      29             :   using super::enter;
      30             :   using super::leave;
      31             :   using super::update;
      32             :   using super::apply;
      33             :   using super::sigma;
      34             : 
      35           9 :   explicit add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater<Substitution>& sigma)
      36           9 :     : super(sigma)
      37           9 :   { }
      38             : 
      39           0 :   action_formula apply(const forall& x)
      40             :   {
      41           0 :     data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
      42           0 :     action_formula result = forall(v1, apply(x.body()));
      43           0 :     sigma.remove_fresh_variable_assignments(x.variables());
      44           0 :     return result;
      45             :   }
      46             : 
      47           0 :   action_formula apply(const exists& x)
      48             :   {
      49           0 :     data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
      50           0 :     action_formula result = exists(v1, apply(x.body()));
      51           0 :     sigma.remove_fresh_variable_assignments(x.variables());
      52           0 :     return result;
      53             :   }
      54             : };
      55             : 
      56             : } // namespace detail
      57             : 
      58             : //--- start generated action_formulas replace_capture_avoiding code ---//
      59             : /// \brief Applies sigma as a capture avoiding substitution to x.
      60             : /// \param x The object to which the subsitution is applied.
      61             : /// \param sigma A substitution.
      62             : /// \param id_generator An identifier generator that generates names that do not appear in x and sigma
      63             : template <typename T, typename Substitution>
      64             : void replace_variables_capture_avoiding(T& x,
      65             :                                         Substitution& sigma,
      66             :                                         data::set_identifier_generator& id_generator,
      67             :                                         typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      68             : )
      69             : {
      70             :   data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
      71             :   data::detail::apply_replace_capture_avoiding_variables_builder<action_formulas::data_expression_builder, action_formulas::detail::add_capture_avoiding_replacement>(sigma1).update(x);
      72             : }
      73             : 
      74             : /// \brief Applies sigma as a capture avoiding substitution to x.
      75             : /// \param x The object to which the substiution is applied.
      76             : /// \param sigma A substitution.
      77             : /// \param id_generator An identifier generator that generates names that do not appear in x and sigma
      78             : template <typename T, typename Substitution>
      79           9 : T replace_variables_capture_avoiding(const T& x,
      80             :                                      Substitution& sigma,
      81             :                                      data::set_identifier_generator& id_generator,
      82             :                                      typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      83             : )
      84             : {
      85          18 :   data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
      86          18 :   return data::detail::apply_replace_capture_avoiding_variables_builder<action_formulas::data_expression_builder, action_formulas::detail::add_capture_avoiding_replacement>(sigma1).apply(x);
      87             : }
      88             : 
      89             : /// \brief Applies sigma as a capture avoiding substitution to x.
      90             : /// \param x The object to which the subsitution is applied.
      91             : /// \param sigma A substitution.
      92             : template <typename T, typename Substitution>
      93             : void replace_variables_capture_avoiding(T& x,
      94             :                                         Substitution& sigma,
      95             :                                         typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      96             : )
      97             : {
      98             :   data::set_identifier_generator id_generator;
      99             :   id_generator.add_identifiers(action_formulas::find_identifiers(x));
     100             :   for (const data::variable& v: substitution_variables(sigma))
     101             :   {
     102             :     id_generator.add_identifier(v.name());
     103             :   }
     104             :   action_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
     105             : }
     106             : 
     107             : /// \brief Applies sigma as a capture avoiding substitution to x.
     108             : /// \param x The object to which the substiution is applied.
     109             : /// \param sigma A substitution.
     110             : template <typename T, typename Substitution>
     111           9 : T replace_variables_capture_avoiding(const T& x,
     112             :                                      Substitution& sigma,
     113             :                                      typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     114             : )
     115             : {
     116          18 :   data::set_identifier_generator id_generator;
     117           9 :   id_generator.add_identifiers(action_formulas::find_identifiers(x));
     118          18 :   for (const data::variable& v: substitution_variables(sigma))
     119             :   {
     120           9 :     id_generator.add_identifier(v.name());
     121             :   }
     122          18 :   return action_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
     123             : }
     124             : //--- end generated action_formulas replace_capture_avoiding code ---//
     125             : 
     126             : } // namespace action_formulas
     127             : 
     128             : } // namespace mcrl2
     129             : 
     130             : namespace mcrl2 {
     131             : 
     132             : namespace regular_formulas {
     133             : 
     134             : namespace detail {
     135             : 
     136             : template <template <class> class Builder, class Derived, class Substitution>
     137             : struct add_capture_avoiding_replacement: public action_formulas::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution>
     138             : {
     139             :   typedef action_formulas::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution> super;
     140             :   using super::enter;
     141             :   using super::leave;
     142             :   using super::update;
     143             :   using super::apply;
     144             :   using super::sigma;
     145             : 
     146             :   explicit add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater<Substitution>& sigma)
     147             :     : super(sigma)
     148             :   { }
     149             : };
     150             : 
     151             : } // namespace detail
     152             : 
     153             : //--- start generated regular_formulas replace_capture_avoiding code ---//
     154             : /// \brief Applies sigma as a capture avoiding substitution to x.
     155             : /// \param x The object to which the subsitution is applied.
     156             : /// \param sigma A substitution.
     157             : /// \param id_generator An identifier generator that generates names that do not appear in x and sigma
     158             : template <typename T, typename Substitution>
     159             : void replace_variables_capture_avoiding(T& x,
     160             :                                         Substitution& sigma,
     161             :                                         data::set_identifier_generator& id_generator,
     162             :                                         typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     163             : )
     164             : {
     165             :   data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
     166             :   data::detail::apply_replace_capture_avoiding_variables_builder<regular_formulas::data_expression_builder, regular_formulas::detail::add_capture_avoiding_replacement>(sigma1).update(x);
     167             : }
     168             : 
     169             : /// \brief Applies sigma as a capture avoiding substitution to x.
     170             : /// \param x The object to which the substiution is applied.
     171             : /// \param sigma A substitution.
     172             : /// \param id_generator An identifier generator that generates names that do not appear in x and sigma
     173             : template <typename T, typename Substitution>
     174             : T replace_variables_capture_avoiding(const T& x,
     175             :                                      Substitution& sigma,
     176             :                                      data::set_identifier_generator& id_generator,
     177             :                                      typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     178             : )
     179             : {
     180             :   data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
     181             :   return data::detail::apply_replace_capture_avoiding_variables_builder<regular_formulas::data_expression_builder, regular_formulas::detail::add_capture_avoiding_replacement>(sigma1).apply(x);
     182             : }
     183             : 
     184             : /// \brief Applies sigma as a capture avoiding substitution to x.
     185             : /// \param x The object to which the subsitution is applied.
     186             : /// \param sigma A substitution.
     187             : template <typename T, typename Substitution>
     188             : void replace_variables_capture_avoiding(T& x,
     189             :                                         Substitution& sigma,
     190             :                                         typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     191             : )
     192             : {
     193             :   data::set_identifier_generator id_generator;
     194             :   id_generator.add_identifiers(regular_formulas::find_identifiers(x));
     195             :   for (const data::variable& v: substitution_variables(sigma))
     196             :   {
     197             :     id_generator.add_identifier(v.name());
     198             :   }
     199             :   regular_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
     200             : }
     201             : 
     202             : /// \brief Applies sigma as a capture avoiding substitution to x.
     203             : /// \param x The object to which the substiution is applied.
     204             : /// \param sigma A substitution.
     205             : template <typename T, typename Substitution>
     206             : T replace_variables_capture_avoiding(const T& x,
     207             :                                      Substitution& sigma,
     208             :                                      typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     209             : )
     210             : {
     211             :   data::set_identifier_generator id_generator;
     212             :   id_generator.add_identifiers(regular_formulas::find_identifiers(x));
     213             :   for (const data::variable& v: substitution_variables(sigma))
     214             :   {
     215             :     id_generator.add_identifier(v.name());
     216             :   }
     217             :   return regular_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
     218             : }
     219             : //--- end generated regular_formulas replace_capture_avoiding code ---//
     220             : 
     221             : } // namespace regular_formulas
     222             : 
     223             : } // namespace mcrl2
     224             : 
     225             : namespace mcrl2 {
     226             : 
     227             : namespace state_formulas {
     228             : 
     229             : namespace detail {
     230             : 
     231             : template <template <class> class Builder, class Derived, class Substitution>
     232             : struct add_capture_avoiding_replacement: public data::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution>
     233             : {
     234             :   typedef data::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution> super;
     235             :   using super::enter;
     236             :   using super::leave;
     237             :   using super::update;
     238             :   using super::apply;
     239             :   using super::sigma;
     240             : 
     241             :   explicit add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater<Substitution>& sigma)
     242             :     : super(sigma)
     243             :   { }
     244             : 
     245             :   state_formula operator()(const forall& x)
     246             :   {
     247             :     data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
     248             :     state_formula result = forall(v1, (*this)(x.body()));
     249             :     sigma.remove_fresh_variable_assignments(x.variables());
     250             :     return result;
     251             :   }
     252             : 
     253             :   state_formula operator()(const exists& x)
     254             :   {
     255             :     data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
     256             :     state_formula result = exists(v1, (*this)(x.body()));
     257             :     sigma.remove_fresh_variable_assignments(x.variables());
     258             :     return result;
     259             :   }
     260             : };
     261             : 
     262             : } // namespace detail
     263             : 
     264             : //--- start generated state_formulas replace_capture_avoiding code ---//
     265             : /// \brief Applies sigma as a capture avoiding substitution to x.
     266             : /// \param x The object to which the subsitution is applied.
     267             : /// \param sigma A substitution.
     268             : /// \param id_generator An identifier generator that generates names that do not appear in x and sigma
     269             : template <typename T, typename Substitution>
     270             : void replace_variables_capture_avoiding(T& x,
     271             :                                         Substitution& sigma,
     272             :                                         data::set_identifier_generator& id_generator,
     273             :                                         typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     274             : )
     275             : {
     276             :   data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
     277             :   data::detail::apply_replace_capture_avoiding_variables_builder<state_formulas::data_expression_builder, state_formulas::detail::add_capture_avoiding_replacement>(sigma1).update(x);
     278             : }
     279             : 
     280             : /// \brief Applies sigma as a capture avoiding substitution to x.
     281             : /// \param x The object to which the substiution is applied.
     282             : /// \param sigma A substitution.
     283             : /// \param id_generator An identifier generator that generates names that do not appear in x and sigma
     284             : template <typename T, typename Substitution>
     285             : T replace_variables_capture_avoiding(const T& x,
     286             :                                      Substitution& sigma,
     287             :                                      data::set_identifier_generator& id_generator,
     288             :                                      typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     289             : )
     290             : {
     291             :   data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
     292             :   return data::detail::apply_replace_capture_avoiding_variables_builder<state_formulas::data_expression_builder, state_formulas::detail::add_capture_avoiding_replacement>(sigma1).apply(x);
     293             : }
     294             : 
     295             : /// \brief Applies sigma as a capture avoiding substitution to x.
     296             : /// \param x The object to which the subsitution is applied.
     297             : /// \param sigma A substitution.
     298             : template <typename T, typename Substitution>
     299             : void replace_variables_capture_avoiding(T& x,
     300             :                                         Substitution& sigma,
     301             :                                         typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     302             : )
     303             : {
     304             :   data::set_identifier_generator id_generator;
     305             :   id_generator.add_identifiers(state_formulas::find_identifiers(x));
     306             :   for (const data::variable& v: substitution_variables(sigma))
     307             :   {
     308             :     id_generator.add_identifier(v.name());
     309             :   }
     310             :   state_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
     311             : }
     312             : 
     313             : /// \brief Applies sigma as a capture avoiding substitution to x.
     314             : /// \param x The object to which the substiution is applied.
     315             : /// \param sigma A substitution.
     316             : template <typename T, typename Substitution>
     317             : T replace_variables_capture_avoiding(const T& x,
     318             :                                      Substitution& sigma,
     319             :                                      typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     320             : )
     321             : {
     322             :   data::set_identifier_generator id_generator;
     323             :   id_generator.add_identifiers(state_formulas::find_identifiers(x));
     324             :   for (const data::variable& v: substitution_variables(sigma))
     325             :   {
     326             :     id_generator.add_identifier(v.name());
     327             :   }
     328             :   return state_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
     329             : }
     330             : //--- end generated state_formulas replace_capture_avoiding code ---//
     331             : 
     332             : } // namespace state_formulas
     333             : 
     334             : } // namespace mcrl2
     335             : 
     336             : #endif // MCRL2_MODAL_FORMULA_REPLACE_CAPTURE_AVOIDING_H

Generated by: LCOV version 1.13