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/process/add_binding.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_ADD_BINDING_H
      13             : #define MCRL2_PROCESS_ADD_BINDING_H
      14             : 
      15             : #include "mcrl2/data/add_binding.h"
      16             : #include "mcrl2/process/process_specification.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace process
      22             : {
      23             : 
      24             : /// \brief Maintains a multiset of bound data variables during traversal
      25             : template <template <class> class Builder, class Derived>
      26             : struct add_data_variable_binding: public data::add_data_variable_binding<Builder, Derived>
      27             : {
      28             :   typedef data::add_data_variable_binding<Builder, Derived> super;
      29             :   using super::enter;
      30             :   using super::leave;
      31             :   using super::apply;
      32             :   using super::bound_variables;
      33             :   using super::increase_bind_count;
      34             :   using super::decrease_bind_count;
      35             : 
      36           0 :   void enter(const process::sum& x)
      37             :   {
      38           0 :     increase_bind_count(x.variables());
      39           0 :   }
      40             : 
      41           0 :   void leave(const process::sum& x)
      42             :   {
      43           0 :     decrease_bind_count(x.variables());
      44           0 :   }
      45             : 
      46           0 :   void enter(const process::stochastic_operator& x)
      47             :   {
      48           0 :     increase_bind_count(x.variables());
      49           0 :   }
      50             : 
      51           0 :   void leave(const process::stochastic_operator& x)
      52             :   {
      53           0 :     decrease_bind_count(x.variables());
      54           0 :   }
      55             : };
      56             : 
      57             : // TODO: get rid of this code duplication
      58             : // special handling for where clauses
      59             : template <template <class> class Builder, class Derived>
      60             : struct add_data_variable_traverser_binding: public add_data_variable_binding<Builder, Derived>
      61             : {
      62             :   typedef add_data_variable_binding<Builder, Derived> super;
      63             :   using super::enter;
      64             :   using super::leave;
      65             :   using super::apply;
      66             :   using super::bound_variables;
      67             :   using super::increase_bind_count;
      68             :   using super::decrease_bind_count;
      69             : 
      70           0 :   void apply(const data::where_clause& x)
      71             :   {
      72           0 :     static_cast<Derived&>(*this).apply(x.declarations());
      73           0 :     static_cast<Derived&>(*this).enter(x);
      74           0 :     static_cast<Derived&>(*this).apply(x.body());
      75           0 :     static_cast<Derived&>(*this).leave(x);
      76           0 :   }
      77             : };
      78             : 
      79             : // special handling for where clauses
      80             : template <template <class> class Builder, class Derived>
      81             : struct add_data_variable_builder_binding: public add_data_variable_binding<Builder, Derived>
      82             : {
      83             :   typedef add_data_variable_binding<Builder, Derived> super;
      84             :   using super::enter;
      85             :   using super::leave;
      86             :   using super::apply;
      87             :   using super::bound_variables;
      88             :   using super::increase_bind_count;
      89             :   using super::decrease_bind_count;
      90             : 
      91             :   template <class T>
      92             :   void apply(T& result, const data::where_clause& x)
      93             :   {
      94             :     data::assignment_expression_list declarations;
      95             :     static_cast<Derived&>(*this).apply(declarations, x.declarations());
      96             :     static_cast<Derived&>(*this).enter(x);
      97             :     data::make_where_clause(result, [&](data::data_expression& r){ static_cast<Derived&>(*this).apply(r, x.body()); }, declarations);
      98             :     static_cast<Derived&>(*this).leave(x);
      99             :   }
     100             : };
     101             : 
     102             : } // namespace process
     103             : 
     104             : } // namespace mcrl2
     105             : 
     106             : #endif // MCRL2_PROCESS_ADD_BINDING_H