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/substitutions/mutable_substitution_composer.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_SUBSTITUTIONS_MUTABLE_SUBSTITUTION_COMPOSER_H
      13             : #define MCRL2_DATA_SUBSTITUTIONS_MUTABLE_SUBSTITUTION_COMPOSER_H
      14             : 
      15             : #include "mcrl2/data/replace.h"
      16             : #include "mcrl2/data/substitutions/mutable_indexed_substitution.h"
      17             : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace data {
      22             : 
      23             : /// \brief An adapter that makes an arbitrary substitution function mutable.
      24             : template <typename Substitution>
      25             : class mutable_substitution_composer
      26             : {
      27             :   public:
      28             :     /// \brief type used to represent variables.
      29             :     using variable_type = typename Substitution::variable_type ;
      30             : 
      31             :     /// \brief type used to represent expressions.
      32             :     using expression_type = typename Substitution::expression_type;
      33             : 
      34             :     /// \brief Wrapper class for internal storage and substitution updates using operator().
      35             :     using assignment = typename mutable_map_substitution<std::map<variable_type, expression_type> >::assignment ;
      36             : 
      37             :     /// \brief The type of the wrapped substitution.
      38             :     using substitution_type = Substitution;
      39             : 
      40             :     using argument_type = variable_type;
      41             :     using result_type = expression_type;
      42             : 
      43             :   protected:
      44             :     /// \brief The wrapped substitution.
      45             :     const Substitution& f_;
      46             : 
      47             :     /// \brief An additional mutable substitution.
      48             :     mutable_map_substitution<std::map<variable_type, expression_type> > g_;
      49             : 
      50             :   public:
      51             :     /// \brief Constructor
      52             :     mutable_substitution_composer(const Substitution& f)
      53             :       : f_(f)
      54             :     {}
      55             : 
      56             :     /// \brief Apply on single single variable expression.
      57             :     /// \param[in] v the variable for which to give the associated expression.
      58             :     /// \return expression equivalent to s(e), or a reference to such an expression.
      59             :     expression_type operator()(variable_type const& v) const
      60             :     {
      61             :       return data::replace_free_variables(f_(v), g_);
      62             :     }
      63             : 
      64             :     assignment operator[](variable_type const& v)
      65             :     {
      66             :       return g_[v];
      67             :     }
      68             : 
      69             :     /// \brief Returns the wrapped substitution.
      70             :     /// \return The wrapped substitution.
      71             :     const substitution_type& substitution() const
      72             :     {
      73             :       return f_;
      74             :     }
      75             : };
      76             : 
      77             : /// \brief Specialization for mutable_map_substitution.
      78             : template <typename AssociativeContainer>
      79             : class mutable_substitution_composer<mutable_map_substitution<AssociativeContainer>>
      80             : {
      81             :   public:
      82             :     /// \brief The type of the wrapped substitution.
      83             :     using substitution_type = mutable_map_substitution<AssociativeContainer>;
      84             : 
      85             :     /// \brief type used to represent variables.
      86             :     using variable_type = typename substitution_type::variable_type;
      87             : 
      88             :     /// \brief type used to represent expressions.
      89             :     using expression_type = typename substitution_type::expression_type;
      90             : 
      91             :     /// \brief Wrapper class for internal storage and substitution updates using operator().
      92             :     using assignment = typename substitution_type::assignment;
      93             :     
      94             :     using argument_type = variable_type;
      95             :     using result_type = expression_type;
      96             : 
      97             :   protected:
      98             :     /// \brief object on which substitution manipulations are performed.
      99             :     substitution_type& g_;
     100             : 
     101             :   public:
     102             : 
     103             :     /// \brief Constructor with mutable substitution object.
     104             :     /// \param[in,out] g underlying substitution object.
     105           0 :     mutable_substitution_composer(mutable_map_substitution<AssociativeContainer>& g)
     106           0 :       : g_(g)
     107           0 :     {}
     108             : 
     109             :     /// \brief Apply on single single variable expression.
     110             :     /// \param[in] v the variable for which to give the associated expression.
     111             :     /// \return expression equivalent to s(e), or a reference to such an expression.
     112           0 :     const expression_type operator()(variable_type const& v) const
     113             :     {
     114           0 :       return g_(v);
     115             :     }
     116             : 
     117             :     assignment operator[](variable_type const& v)
     118             :     {
     119             :       return g_[v];
     120             :     }
     121             : 
     122             :     /// \brief Returns the wrapped substitution
     123             :     /// \return The wrapped substitution
     124             :     const substitution_type& substitution() const
     125             :     {
     126             :       return g_;
     127             :     }
     128             : };
     129             : 
     130             : /// \brief Specialization for mutable_indexed_substitution.
     131             : template <typename VariableType, typename ExpressionSequence>
     132             : class mutable_substitution_composer<mutable_indexed_substitution<VariableType, ExpressionSequence>>
     133             : {
     134             :   public:
     135             :     /// \brief The type of the wrapped substitution.
     136             :     using substitution_type = mutable_indexed_substitution<VariableType, ExpressionSequence>;
     137             : 
     138             :     /// \brief type used to represent variables.
     139             :     using variable_type = typename substitution_type::variable_type;
     140             : 
     141             :     /// \brief type used to represent expressions.
     142             :     using expression_type = typename substitution_type::expression_type;
     143             : 
     144             :     /// \brief Wrapper class for internal storage and substitution updates using operator().
     145             :     using assignment = typename substitution_type::assignment;
     146             : 
     147             :     using argument_type = variable_type;
     148             :     using result_type = expression_type;
     149             : 
     150             :   protected:
     151             :     /// \brief object on which substitution manipulations are performed.
     152             :     substitution_type& g_;
     153             : 
     154             :   public:
     155             : 
     156             :     /// \brief Constructor with mutable substitution object.
     157             :     /// \param[in,out] g underlying substitution object.
     158             :     mutable_substitution_composer(substitution_type& g)
     159             :       : g_(g)
     160             :     {}
     161             : 
     162             :     /// \brief Apply on single single variable expression.
     163             :     /// \param[in] v the variable for which to give the associated expression.
     164             :     /// \return expression equivalent to s(e), or a reference to such an expression.
     165             :     const expression_type operator()(variable_type const& v) const
     166             :     {
     167             :       return g_(v);
     168             :     }
     169             : 
     170             :     assignment operator[](variable_type const& v)
     171             :     {
     172             :       return g_[v];
     173             :     }
     174             : 
     175             :     /// \brief Returns the wrapped substitution.
     176             :     /// \return The wrapped substitution.
     177             :     const substitution_type& substitution() const
     178             :     {
     179             :       return g_;
     180             :     }
     181             : };
     182             : 
     183             : } // namespace data
     184             : 
     185             : } // namespace mcrl2
     186             : 
     187             : #endif // MCRL2_DATA_SUBSTITUTIONS_MUTABLE_SUBSTITUTION_COMPOSER_H