LCOV - code coverage report
Current view: top level - data/include/mcrl2/data - replace_capture_avoiding.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 71 81 87.7 %
Date: 2020-02-19 00:44:21 Functions: 39 61 63.9 %
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/data/replace_capture_avoiding.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_REPLACE_CAPTURE_AVOIDING_H
      13             : #define MCRL2_DATA_REPLACE_CAPTURE_AVOIDING_H
      14             : 
      15             : #include "mcrl2/core/detail/print_utility.h"
      16             : #include "mcrl2/data/builder.h"
      17             : #include "mcrl2/data/find.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace data {
      22             : 
      23             : namespace detail {
      24             : 
      25             : // Wraps a substitution, such that assignments to variables can be added and removed.
      26             : template <typename Substitution>
      27        5002 : struct capture_avoiding_substitution_updater
      28             : {
      29             :   Substitution& sigma;
      30             :   data::set_identifier_generator& id_generator;
      31             :   std::map<variable, std::list<variable>> updates;
      32             : 
      33        5002 :   capture_avoiding_substitution_updater(Substitution& sigma_, data::set_identifier_generator& id_generator_)
      34        5002 :     : sigma(sigma_), id_generator(id_generator_)
      35        5002 :   {}
      36             : 
      37             :   // adds the assignment [v := v'] to sigma, and returns v'
      38          28 :   variable add_fresh_variable_assignment(const variable& v)
      39             :   {
      40          28 :     variable v1(id_generator(v.name()), v.sort());
      41          28 :     updates[v].push_back(v1);
      42          28 :     return v1;
      43             :   }
      44             : 
      45             :   // removes the assignment [v := v'] from sigma
      46          28 :   void remove_fresh_variable_assignment(const variable& v)
      47             :   {
      48          28 :     auto i = updates.find(v);
      49          28 :     id_generator.remove_identifier(i->second.back().name());
      50          28 :     i->second.pop_back();
      51          28 :     if (i->second.empty())
      52             :     {
      53          25 :       updates.erase(i);
      54             :     }
      55          28 :   }
      56             : 
      57             :   // adds the assignments [variables := variables'] to sigma, and returns variables'
      58             :   template <typename VariableContainer>
      59          22 :   variable_list add_fresh_variable_assignments(const VariableContainer& variables)
      60             :   {
      61             :     return variable_list(
      62             :       variables.begin(),
      63             :       variables.end(),
      64          24 :       [&](const variable& v)
      65             :       {
      66          24 :         return add_fresh_variable_assignment(v);
      67          24 :       }
      68          22 :     );
      69             :   }
      70             : 
      71             :   // removes the assignments [variables := variables'] from sigma
      72             :   template <typename VariableContainer>
      73          22 :   void remove_fresh_variable_assignments(const VariableContainer& variables)
      74             :   {
      75          46 :     for (const variable& v: variables)
      76             :     {
      77          24 :       remove_fresh_variable_assignment(v);
      78             :     }
      79          22 :   }
      80             : 
      81       29186 :   data_expression operator()(const variable& x)
      82             :   {
      83       29186 :     auto i = updates.find(x);
      84       29186 :     if (i != updates.end())
      85             :     {
      86          33 :       return i->second.back();
      87             :     }
      88             :     else
      89             :     {
      90       29153 :       return sigma(x);
      91             :     }
      92             :   }
      93             : };
      94             : 
      95             : template <typename Substitution>
      96             : std::ostream& operator<<(std::ostream& out, const capture_avoiding_substitution_updater<Substitution>& sigma)
      97             : {
      98             :   std::vector<std::string> updates;
      99             :   for (const auto& p: sigma.updates)
     100             :   {
     101             :     updates.push_back(data::pp(p.first) + " := " + core::detail::print_list(p.second));
     102             :   }
     103             :   return out << sigma.sigma << " with updates " << core::detail::print_list(updates);
     104             : }
     105             : 
     106             : template <template <class> class Builder, template <template <class> class, class, class> class Binder, class Substitution>
     107             : struct replace_capture_avoiding_variables_builder: public Binder<Builder, replace_capture_avoiding_variables_builder<Builder, Binder, Substitution>, Substitution>
     108             : {
     109             :   typedef Binder<Builder, replace_capture_avoiding_variables_builder<Builder, Binder, Substitution>, Substitution> super;
     110             :   using super::enter;
     111             :   using super::leave;
     112             :   using super::apply;
     113             :   using super::update;
     114             : 
     115        5002 :   explicit replace_capture_avoiding_variables_builder(capture_avoiding_substitution_updater<Substitution>& sigma)
     116        5002 :     : super(sigma)
     117        5002 :   { }
     118             : };
     119             : 
     120             : template <template <class> class Builder, template <template <class> class, class, class> class Binder, class Substitution>
     121             : replace_capture_avoiding_variables_builder<Builder, Binder, Substitution>
     122        5002 : apply_replace_capture_avoiding_variables_builder(capture_avoiding_substitution_updater<Substitution>& sigma)
     123             : {
     124        5002 :   return replace_capture_avoiding_variables_builder<Builder, Binder, Substitution>(sigma);
     125             : }
     126             : 
     127             : template <template <class> class Builder, class Derived, class Substitution>
     128             : struct add_capture_avoiding_replacement: public Builder<Derived>
     129             : {
     130             :   typedef Builder<Derived> super;
     131             :   using super::enter;
     132             :   using super::leave;
     133             :   using super::apply;
     134             :   using super::update;
     135             : 
     136             :   capture_avoiding_substitution_updater<Substitution>& sigma;
     137             : 
     138        5002 :   explicit add_capture_avoiding_replacement(capture_avoiding_substitution_updater<Substitution>& sigma_)
     139        5002 :     : sigma(sigma_)
     140        5002 :   { }
     141             : 
     142             :   // applies the substitution to the right hand sides of the assignments
     143        2280 :   assignment_list apply(const assignment_list& x)
     144             :   {
     145             :     return assignment_list(
     146             :       x.begin(),
     147             :       x.end(),
     148       10771 :       [&](const data::assignment& a)
     149             :       {
     150       10771 :         return data::assignment(a.lhs(), apply(a.rhs()));
     151       10771 :       }
     152        2280 :     );
     153             :   }
     154             : 
     155       29186 :   data_expression apply(const variable& v)
     156             :   {
     157       29186 :     return sigma(v);
     158             :   }
     159             : 
     160           3 :   data_expression apply(const data::where_clause& x)
     161             :   {
     162           3 :     const auto& declarations = atermpp::container_cast<data::assignment_list>(x.declarations());
     163             : 
     164           6 :     auto declarations1 = data::assignment_list(
     165             :       declarations.begin(),
     166             :       declarations.end(),
     167           4 :       [&](const assignment& a)
     168             :       {
     169           4 :         const data::variable& v = a.lhs();
     170           4 :         const data_expression& x1 = a.rhs();
     171             :         // add the assignment [v := v'] to sigma
     172           8 :         data::variable v1 = sigma.add_fresh_variable_assignment(v);
     173           8 :         return assignment(v1, apply(x1));
     174             :       }
     175             :     );
     176           3 :     data_expression result = where_clause(apply(x.body()), declarations1);
     177             : 
     178             :     // remove the assignments [v := v'] from sigma
     179           7 :     for (const assignment& a: declarations)
     180             :     {
     181           4 :       const variable& v = a.lhs();
     182           4 :       sigma.remove_fresh_variable_assignment(v);
     183             :     }
     184             : 
     185           6 :     return result;
     186             :   }
     187             : 
     188          12 :   data_expression apply(const data::forall& x)
     189             :   {
     190          24 :     variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
     191          12 :     data_expression result = data::forall(v1, apply(x.body()));
     192          12 :     sigma.remove_fresh_variable_assignments(x.variables());
     193          24 :     return result;
     194             :   }
     195             : 
     196           0 :   data_expression apply(const data::exists& x)
     197             :   {
     198           0 :     variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
     199           0 :     data_expression result = data::exists(v1, apply(x.body()));
     200           0 :     sigma.remove_fresh_variable_assignments(x.variables());
     201           0 :     return result;
     202             :   }
     203             : 
     204           0 :   data_expression apply(const data::lambda& x)
     205             :   {
     206           0 :     variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
     207           0 :     data_expression result = data::lambda(v1, apply(x.body()));
     208           0 :     sigma.remove_fresh_variable_assignments(x.variables());
     209           0 :     return result;
     210             :   }
     211             : 
     212             :   data_equation apply(data_equation& /* x */)
     213             :   {
     214             :     throw mcrl2::runtime_error("not implemented yet");
     215             :   }
     216             : };
     217             : 
     218             : } // namespace detail
     219             : 
     220             : //--- start generated data replace_capture_avoiding code ---//
     221             : /// \brief Applies sigma as a capture avoiding substitution to x.
     222             : /// \param x The object to which the subsitution is applied.
     223             : /// \param sigma A substitution.
     224             : /// \param id_generator An identifier generator that generates names that do not appear in x and sigma
     225             : template <typename T, typename Substitution>
     226             : void replace_variables_capture_avoiding(T& x,
     227             :                                         Substitution& sigma,
     228             :                                         data::set_identifier_generator& id_generator,
     229             :                                         typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     230             : )
     231             : {
     232             :   data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
     233             :   data::detail::apply_replace_capture_avoiding_variables_builder<data::data_expression_builder, data::detail::add_capture_avoiding_replacement>(sigma1).update(x);
     234             : }
     235             : 
     236             : /// \brief Applies sigma as a capture avoiding substitution to x.
     237             : /// \param x The object to which the substiution is applied.
     238             : /// \param sigma A substitution.
     239             : /// \param id_generator An identifier generator that generates names that do not appear in x and sigma
     240             : template <typename T, typename Substitution>
     241        1746 : T replace_variables_capture_avoiding(const T& x,
     242             :                                      Substitution& sigma,
     243             :                                      data::set_identifier_generator& id_generator,
     244             :                                      typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     245             : )
     246             : {
     247        3492 :   data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
     248        3492 :   return data::detail::apply_replace_capture_avoiding_variables_builder<data::data_expression_builder, data::detail::add_capture_avoiding_replacement>(sigma1).apply(x);
     249             : }
     250             : 
     251             : /// \brief Applies sigma as a capture avoiding substitution to x.
     252             : /// \param x The object to which the subsitution is applied.
     253             : /// \param sigma A substitution.
     254             : template <typename T, typename Substitution>
     255             : void replace_variables_capture_avoiding(T& x,
     256             :                                         Substitution& sigma,
     257             :                                         typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     258             : )
     259             : {
     260             :   data::set_identifier_generator id_generator;
     261             :   id_generator.add_identifiers(data::find_identifiers(x));
     262             :   for (const data::variable& v: substitution_variables(sigma))
     263             :   {
     264             :     id_generator.add_identifier(v.name());
     265             :   }
     266             :   data::replace_variables_capture_avoiding(x, sigma, id_generator);
     267             : }
     268             : 
     269             : /// \brief Applies sigma as a capture avoiding substitution to x.
     270             : /// \param x The object to which the substiution is applied.
     271             : /// \param sigma A substitution.
     272             : template <typename T, typename Substitution>
     273         947 : T replace_variables_capture_avoiding(const T& x,
     274             :                                      Substitution& sigma,
     275             :                                      typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     276             : )
     277             : {
     278        1894 :   data::set_identifier_generator id_generator;
     279         947 :   id_generator.add_identifiers(data::find_identifiers(x));
     280        1416 :   for (const data::variable& v: substitution_variables(sigma))
     281             :   {
     282         469 :     id_generator.add_identifier(v.name());
     283             :   }
     284        1894 :   return data::replace_variables_capture_avoiding(x, sigma, id_generator);
     285             : }
     286             : //--- end generated data replace_capture_avoiding code ---//
     287             : 
     288             : } // namespace data
     289             : 
     290             : } // namespace mcrl2
     291             : 
     292             : #endif // MCRL2_DATA_REPLACE_CAPTURE_AVOIDING_H

Generated by: LCOV version 1.13