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/add_binding.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_DATA_ADD_BINDING_H 13 : #define MCRL2_DATA_ADD_BINDING_H 14 : 15 : #include "mcrl2/core/add_binding.h" 16 : #include "mcrl2/data/exists.h" 17 : #include "mcrl2/data/forall.h" 18 : #include "mcrl2/data/lambda.h" 19 : #include "mcrl2/data/where_clause.h" 20 : #include "mcrl2/data/set_comprehension.h" 21 : #include "mcrl2/data/bag_comprehension.h" 22 : #include "mcrl2/data/untyped_set_or_bag_comprehension.h" 23 : 24 : 25 : namespace mcrl2 26 : { 27 : 28 : namespace data 29 : { 30 : 31 : /// \brief Maintains a multiset of bound data variables during traversal 32 : template <template <class> class Builder, class Derived> 33 : struct add_data_variable_binding: public core::add_binding<Builder, Derived, variable> 34 : { 35 : typedef core::add_binding<Builder, Derived, variable> super; 36 : using super::enter; 37 : using super::leave; 38 : using super::apply; 39 : using super::bound_variables; 40 : using super::increase_bind_count; 41 : using super::decrease_bind_count; 42 : 43 50 : void increase_bind_count(const assignment_list& assignments) 44 : { 45 150 : for (const auto& assignment : assignments) 46 : { 47 50 : increase_bind_count(assignment.lhs()); 48 : } 49 50 : } 50 : 51 50 : void decrease_bind_count(const assignment_list& assignments) 52 : { 53 150 : for (const auto& assignment : assignments) 54 : { 55 50 : decrease_bind_count(assignment.lhs()); 56 : } 57 50 : } 58 : 59 50 : void enter(const data::where_clause& x) 60 : { 61 50 : increase_bind_count(x.assignments()); 62 50 : } 63 : 64 50 : void leave(const data::where_clause& x) 65 : { 66 50 : decrease_bind_count(x.assignments()); 67 50 : } 68 : 69 96 : void enter(const data::forall& x) 70 : { 71 96 : increase_bind_count(x.variables()); 72 96 : } 73 : 74 96 : void leave(const data::forall& x) 75 : { 76 96 : decrease_bind_count(x.variables()); 77 96 : } 78 : 79 22 : void enter(const data::exists& x) 80 : { 81 22 : increase_bind_count(x.variables()); 82 22 : } 83 : 84 22 : void leave(const data::exists& x) 85 : { 86 22 : decrease_bind_count(x.variables()); 87 22 : } 88 : 89 1509 : void enter(const data::lambda& x) 90 : { 91 1509 : increase_bind_count(x.variables()); 92 1509 : } 93 : 94 1509 : void leave(const data::lambda& x) 95 : { 96 1509 : decrease_bind_count(x.variables()); 97 1509 : } 98 : 99 0 : void enter(const data::set_comprehension& x) 100 : { 101 0 : increase_bind_count(x.variables()); 102 0 : } 103 : 104 0 : void leave(const data::set_comprehension& x) 105 : { 106 0 : decrease_bind_count(x.variables()); 107 0 : } 108 : 109 0 : void enter(const data::bag_comprehension& x) 110 : { 111 0 : increase_bind_count(x.variables()); 112 0 : } 113 : 114 0 : void leave(const data::bag_comprehension& x) 115 : { 116 0 : decrease_bind_count(x.variables()); 117 0 : } 118 : 119 0 : void enter(const data::untyped_set_or_bag_comprehension& x) 120 : { 121 0 : increase_bind_count(x.variables()); 122 0 : } 123 : 124 0 : void leave(const data::untyped_set_or_bag_comprehension& x) 125 : { 126 0 : decrease_bind_count(x.variables()); 127 0 : } 128 : 129 : void enter(const data::data_equation& x) 130 : { 131 : increase_bind_count(x.variables()); 132 : } 133 : 134 : void leave(const data::data_equation& x) 135 : { 136 : decrease_bind_count(x.variables()); 137 : } 138 : }; 139 : 140 : // special handling for where clauses 141 : template <template <class> class Builder, class Derived> 142 : struct add_data_variable_traverser_binding: public add_data_variable_binding<Builder, Derived> 143 : { 144 : typedef add_data_variable_binding<Builder, Derived> super; 145 : using super::enter; 146 : using super::leave; 147 : using super::apply; 148 : using super::bound_variables; 149 : using super::increase_bind_count; 150 : using super::decrease_bind_count; 151 : 152 50 : void apply(const data::where_clause& x) 153 : { 154 50 : static_cast<Derived&>(*this).apply(x.declarations()); 155 50 : static_cast<Derived&>(*this).enter(x); 156 50 : static_cast<Derived&>(*this).apply(x.body()); 157 50 : static_cast<Derived&>(*this).leave(x); 158 50 : } 159 : }; 160 : 161 : // special handling for where clauses 162 : template <template <class> class Builder, class Derived> 163 : struct add_data_variable_builder_binding: public add_data_variable_binding<Builder, Derived> 164 : { 165 : typedef add_data_variable_binding<Builder, Derived> super; 166 : using super::enter; 167 : using super::leave; 168 : using super::apply; 169 : using super::bound_variables; 170 : using super::increase_bind_count; 171 : using super::decrease_bind_count; 172 : 173 : template <class T> 174 0 : void apply(T& result, const data::where_clause& x) 175 : { 176 0 : assignment_expression_list declarations; 177 0 : static_cast<Derived&>(*this).apply(declarations, x.declarations()); 178 0 : static_cast<Derived&>(*this).enter(x); 179 0 : data::make_where_clause(result, 180 0 : [&](data_expression& r){ static_cast<Derived&>(*this).apply(r, x.body()); }, 181 : declarations); 182 0 : static_cast<Derived&>(*this).leave(x); 183 0 : } 184 : }; 185 : 186 : } // namespace data 187 : 188 : } // namespace mcrl2 189 : 190 : #endif // MCRL2_DATA_ADD_BINDING_H