Line data    Source code

       1             : // Author(s): Jan Friso Groote
       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/lps/replace_capture_avoiding_with_an_identifier_generator.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_REPLACE_CAPTURE_AVOIDING_WITH_AN_IDENTIFIER_GENERATOR_H
      13             : #define MCRL2_LPS_REPLACE_CAPTURE_AVOIDING_WITH_AN_IDENTIFIER_GENERATOR_H
      14             : 
      15             : #include "mcrl2/lps/add_binding.h"
      16             : #include "mcrl2/lps/builder.h"
      17             : #include "mcrl2/process/replace_capture_avoiding_with_an_identifier_generator.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace lps {
      22             : 
      23             : namespace detail {
      24             : 
      25             : // Below code for capture avoiding subsitutions with an identifier generator are provided.
      26             : 
      27             : template<template<class> class Builder, class Derived, class Substitution, class IdentifierGenerator>
      28             : struct add_capture_avoiding_replacement_with_an_identifier_generator
      29             :   : public process::detail::add_capture_avoiding_replacement_with_an_identifier_generator<Builder, Derived, Substitution, IdentifierGenerator>
      30             : {
      31             :   typedef process::detail::add_capture_avoiding_replacement_with_an_identifier_generator<Builder, Derived, Substitution, IdentifierGenerator> super;
      32             :   using super::enter;
      33             :   using super::leave;
      34             :   using super::apply;
      35             :   using super::update;
      36             :   using super::update_sigma;
      37             : 
      38        5223 :   add_capture_avoiding_replacement_with_an_identifier_generator(Substitution& sigma, IdentifierGenerator& id_generator)
      39        5223 :     : super(sigma, id_generator)
      40             :   {
      41        5223 :   }
      42             : 
      43             :   template<typename ActionSummand>
      44             :   void do_action_summand(ActionSummand& x, const data::variable_list& v)
      45             :   {
      46             :     x.summation_variables() = v;
      47             :     x.condition() = apply(x.condition());
      48             :     x.multi_action() = apply(x.multi_action());
      49             :     x.assignments() = apply(x.assignments());
      50             :   }
      51             : 
      52             :   void update(action_summand& x)
      53             :   {
      54             :     data::variable_list v = update_sigma.push(x.summation_variables());
      55             :     do_action_summand(x, v);
      56             :     update_sigma.pop(v);
      57             :   }
      58             : 
      59             :   void update(stochastic_action_summand& x)
      60             :   {
      61             :     data::variable_list v = update_sigma.push(x.summation_variables());
      62             :     do_action_summand(x, v);
      63             :     x.distribution() = apply(x.distribution());
      64             :     update_sigma.pop(v);
      65             :   }
      66             : 
      67             :   void update(deadlock_summand& x)
      68             :   {
      69             :     data::variable_list v = update_sigma.push(x.summation_variables());
      70             :     x.summation_variables() = v;
      71             :     x.condition() = apply(x.condition());
      72             :     update(x.deadlock());
      73             :     update_sigma.pop(v);
      74             :   }
      75             : 
      76             :   template<typename LinearProcess>
      77             :   void do_linear_process(LinearProcess& x)
      78             :   {
      79             :     data::variable_list v = update_sigma.push(x.process_parameters());
      80             :     x.process_parameters() = v;
      81             :     update(x.action_summands());
      82             :     update(x.deadlock_summands());
      83             :     update_sigma.pop(v);
      84             :   }
      85             : 
      86             :   void update(linear_process& x)
      87             :   {
      88             :     do_linear_process(x);
      89             :   }
      90             : 
      91             :   void update(stochastic_linear_process& x)
      92             :   {
      93             :     do_linear_process(x);
      94             :   }
      95             : 
      96             :   template<typename Specification>
      97             :   void do_specification(Specification& x)
      98             :   {
      99             :     std::set<data::variable> v = update_sigma(x.global_variables());
     100             :     x.global_variables() = v;
     101             :     update(x.process());
     102             :     x.action_labels() = apply(x.action_labels());
     103             :     x.initial_process() = apply(x.initial_process());
     104             :     update_sigma.pop(v);
     105             :   }
     106             : 
     107             :   void operator()(specification& x)
     108             :   {
     109             :     do_specification(x);
     110             :   }
     111             : 
     112             :   void operator()(stochastic_specification& x)
     113             :   {
     114             :     do_specification(x);
     115             :   }
     116             : 
     117             :   stochastic_distribution apply(stochastic_distribution& x)
     118             :   {
     119             :     data::variable_list v = update_sigma.push(x.variables());
     120             :     stochastic_distribution result(x.variables(), apply(x.distribution()));
     121             :     update_sigma.pop(v);
     122             :     return result;
     123             :   }
     124             : };
     125             : 
     126             : } // namespace detail
     127             : 
     128             : //--- start generated lps replace_capture_avoiding_with_identifier_generator code ---//
     129             : /// \\brief Applies sigma as a capture avoiding substitution to x using an identifier generator.
     130             : /// \\details This substitution function is much faster than replace_variables_capture_avoiding, but
     131             : ///          it requires an identifier generator that generates strings for fresh variables. These
     132             : ///          strings must be unique in the sense that they have not been used for other variables.
     133             : /// \\param x The object to which the subsitution is applied.
     134             : /// \\param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its
     135             : ///              right hand side. The class maintain_variables_in_rhs is useful for this purpose.
     136             : /// \\param id_generator A generator that generates unique strings, not yet used as variable names.
     137             : 
     138             : template <typename T, typename Substitution, typename IdentifierGenerator>
     139             : void replace_variables_capture_avoiding_with_an_identifier_generator(T& x,
     140             :                        Substitution& sigma,
     141             :                        IdentifierGenerator& id_generator,
     142             :                        typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     143             :                       )
     144             : {
     145             :   data::detail::apply_replace_capture_avoiding_variables_builder_with_an_identifier_generator<lps::data_expression_builder, lps::detail::add_capture_avoiding_replacement_with_an_identifier_generator>(sigma, id_generator).update(x);
     146             : }
     147             : 
     148             : /// \\brief Applies sigma as a capture avoiding substitution to x using an identifier generator..
     149             : /// \\details This substitution function is much faster than replace_variables_capture_avoiding, but
     150             : ///          it requires an identifier generator that generates strings for fresh variables. These
     151             : ///          strings must be unique in the sense that they have not been used for other variables.
     152             : /// \\param x The object to which the substiution is applied.
     153             : /// \\param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its
     154             : ///              right hand side. The class maintain_variables_in_rhs is useful for this purpose.
     155             : /// \\param id_generator A generator that generates unique strings, not yet used as variable names.
     156             : /// \\return The result is the term x to which sigma has been applied.
     157             : template <typename T, typename Substitution, typename IdentifierGenerator>
     158        5223 : T replace_variables_capture_avoiding_with_an_identifier_generator(const T& x,
     159             :                     Substitution& sigma,
     160             :                     IdentifierGenerator& id_generator,
     161             :                     typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     162             :                    )
     163             : {
     164        5223 :   T result;
     165        5223 :   data::detail::apply_replace_capture_avoiding_variables_builder_with_an_identifier_generator<lps::data_expression_builder, lps::detail::add_capture_avoiding_replacement_with_an_identifier_generator>(sigma, id_generator).apply(result, x);
     166        5223 :   return result;
     167           0 : }
     168             : //--- end generated lps replace_capture_avoiding_with_identifier_generator code ---//
     169             : 
     170             : } // namespace lps
     171             : 
     172             : } // namespace mcrl2
     173             : 
     174             : #endif // MCRL2_LPS_REPLACE_CAPTURE_AVOIDING_WITH_AN_IDENTIFIER_GENERATOR_H