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