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/replace.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_REPLACE_H
13 : #define MCRL2_PBES_REPLACE_H
14 :
15 : #include "mcrl2/data/replace.h"
16 : #include "mcrl2/pbes/replace_capture_avoiding.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace pbes_system
22 : {
23 :
24 : namespace detail {
25 :
26 : /// \cond INTERNAL_DOCS
27 : template <template <class> class Builder, class Substitution>
28 : struct substitute_pbes_expressions_builder: public Builder<substitute_pbes_expressions_builder<Builder, Substitution> >
29 : {
30 : typedef Builder<substitute_pbes_expressions_builder<Builder, Substitution> > super;
31 : using super::apply;
32 :
33 : Substitution sigma;
34 : bool innermost;
35 :
36 87 : substitute_pbes_expressions_builder(Substitution sigma_, bool innermost_)
37 1 : : sigma(sigma_),
38 87 : innermost(innermost_)
39 87 : {}
40 :
41 : template <class T>
42 97 : void apply(T& result, const pbes_expression& x)
43 : {
44 97 : if (innermost)
45 : {
46 3 : pbes_expression y;
47 3 : super::apply(y, x);
48 3 : result = sigma(y);
49 3 : return;
50 3 : }
51 94 : result = sigma(x);
52 : }
53 : };
54 :
55 : template <template <class> class Builder, class Substitution>
56 : substitute_pbes_expressions_builder<Builder, Substitution>
57 87 : make_replace_pbes_expressions_builder(Substitution sigma, bool innermost)
58 : {
59 87 : return substitute_pbes_expressions_builder<Builder, Substitution>(sigma, innermost);
60 : }
61 :
62 : template <template <class> class Builder, class Substitution>
63 : struct replace_propositional_variables_builder: public Builder<replace_propositional_variables_builder<Builder, Substitution> >
64 : {
65 : typedef Builder<replace_propositional_variables_builder<Builder, Substitution> > super;
66 : using super::apply;
67 :
68 : const Substitution& sigma;
69 :
70 178 : explicit replace_propositional_variables_builder(const Substitution& sigma_)
71 178 : : sigma(sigma_)
72 178 : {}
73 :
74 : template <class T>
75 237 : void apply(T& result, const propositional_variable_instantiation& x)
76 : {
77 237 : result = sigma(x);
78 237 : }
79 : };
80 :
81 : template <template <class> class Builder, class Substitution>
82 : replace_propositional_variables_builder<Builder, Substitution>
83 178 : make_replace_propositional_variables_builder(const Substitution& sigma)
84 : {
85 178 : return replace_propositional_variables_builder<Builder, Substitution>(sigma);
86 : }
87 :
88 :
89 : /// \endcond
90 :
91 : } // namespace detail
92 :
93 : //--- start generated pbes_system replace code ---//
94 : template <typename T, typename Substitution>
95 : void replace_sort_expressions(T& x,
96 : const Substitution& sigma,
97 : bool innermost,
98 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
99 : )
100 : {
101 : data::detail::make_replace_sort_expressions_builder<pbes_system::sort_expression_builder>(sigma, innermost).update(x);
102 : }
103 :
104 : template <typename T, typename Substitution>
105 : T replace_sort_expressions(const T& x,
106 : const Substitution& sigma,
107 : bool innermost,
108 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
109 : )
110 : {
111 : T result;
112 : data::detail::make_replace_sort_expressions_builder<pbes_system::sort_expression_builder>(sigma, innermost).apply(result, x);
113 : return result;
114 : }
115 :
116 : template <typename T, typename Substitution>
117 : void replace_data_expressions(T& x,
118 : const Substitution& sigma,
119 : bool innermost,
120 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
121 : )
122 : {
123 : data::detail::make_replace_data_expressions_builder<pbes_system::data_expression_builder>(sigma, innermost).update(x);
124 : }
125 :
126 : template <typename T, typename Substitution>
127 : T replace_data_expressions(const T& x,
128 : const Substitution& sigma,
129 : bool innermost,
130 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
131 : )
132 : {
133 : T result;
134 : data::detail::make_replace_data_expressions_builder<pbes_system::data_expression_builder>(sigma, innermost).apply(result, x);
135 : return result;
136 : }
137 :
138 :
139 : template <typename T, typename Substitution>
140 1 : void replace_variables(T& x,
141 : const Substitution& sigma,
142 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
143 : )
144 : {
145 1 : core::make_update_apply_builder<pbes_system::data_expression_builder>(sigma).update(x);
146 1 : }
147 :
148 : template <typename T, typename Substitution>
149 2 : T replace_variables(const T& x,
150 : const Substitution& sigma,
151 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
152 : )
153 : {
154 2 : T result;
155 2 : core::make_update_apply_builder<pbes_system::data_expression_builder>(sigma).apply(result, x);
156 2 : return result;
157 0 : }
158 :
159 : template <typename T, typename Substitution>
160 : void replace_all_variables(T& x,
161 : const Substitution& sigma,
162 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
163 : )
164 : {
165 : core::make_update_apply_builder<pbes_system::variable_builder>(sigma).update(x);
166 : }
167 :
168 : template <typename T, typename Substitution>
169 : T replace_all_variables(const T& x,
170 : const Substitution& sigma,
171 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
172 : )
173 : {
174 : T result;
175 : core::make_update_apply_builder<pbes_system::variable_builder>(sigma).apply(result, x);
176 : return result;
177 : }
178 :
179 : /// \\brief Applies the substitution sigma to x.
180 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
181 : template <typename T, typename Substitution>
182 5 : void replace_free_variables(T& x,
183 : const Substitution& sigma,
184 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
185 : )
186 : {
187 5 : assert(data::is_simple_substitution(sigma));
188 5 : data::detail::make_replace_free_variables_builder<pbes_system::data_expression_builder, pbes_system::add_data_variable_builder_binding>(sigma).update(x);
189 5 : }
190 :
191 : /// \\brief Applies the substitution sigma to x.
192 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
193 : template <typename T, typename Substitution>
194 22 : T replace_free_variables(const T& x,
195 : const Substitution& sigma,
196 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
197 : )
198 : {
199 22 : assert(data::is_simple_substitution(sigma));
200 22 : T result;
201 22 : data::detail::make_replace_free_variables_builder<pbes_system::data_expression_builder, pbes_system::add_data_variable_builder_binding>(sigma).apply(result, x);
202 22 : return result;
203 0 : }
204 :
205 : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
206 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
207 : template <typename T, typename Substitution, typename VariableContainer>
208 : void replace_free_variables(T& x,
209 : const Substitution& sigma,
210 : const VariableContainer& bound_variables,
211 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
212 : )
213 : {
214 : assert(data::is_simple_substitution(sigma));
215 : data::detail::make_replace_free_variables_builder<pbes_system::data_expression_builder, pbes_system::add_data_variable_builder_binding>(sigma).update(x, bound_variables);
216 : }
217 :
218 : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
219 : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
220 : template <typename T, typename Substitution, typename VariableContainer>
221 : T replace_free_variables(const T& x,
222 : const Substitution& sigma,
223 : const VariableContainer& bound_variables,
224 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
225 : )
226 : {
227 : assert(data::is_simple_substitution(sigma));
228 : T result;
229 : data::detail::make_replace_free_variables_builder<pbes_system::data_expression_builder, pbes_system::add_data_variable_builder_binding>(sigma).apply(result, x, bound_variables);
230 : return result;
231 : }
232 : //--- end generated pbes_system replace code ---//
233 :
234 : /// \brief Applies a propositional variable substitution.
235 : template <typename T, typename Substitution>
236 2 : void replace_propositional_variables(T& x,
237 : const Substitution& sigma,
238 : typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
239 : )
240 : {
241 2 : pbes_system::detail::make_replace_propositional_variables_builder<pbes_system::pbes_expression_builder>(sigma).update(x);
242 2 : }
243 :
244 : /// \brief Applies a propositional variable substitution.
245 : template <typename T, typename Substitution>
246 176 : T replace_propositional_variables(const T& x,
247 : const Substitution& sigma,
248 : typename std::enable_if<std::is_base_of< atermpp::aterm, T>::value>::type* = nullptr
249 : )
250 : {
251 176 : T result;
252 176 : pbes_system::detail::make_replace_propositional_variables_builder<pbes_system::pbes_expression_builder>(sigma).apply(result, x);
253 176 : return result;
254 0 : }
255 :
256 : /// \brief Applies a propositional variable substitution.
257 : template <typename T, typename Substitution>
258 0 : void replace_propositional_variables(T& result,
259 : const T& x,
260 : const Substitution& sigma,
261 : typename std::enable_if<std::is_base_of< atermpp::aterm, T>::value>::type* = nullptr
262 : )
263 : {
264 0 : pbes_system::detail::make_replace_propositional_variables_builder<pbes_system::pbes_expression_builder>(sigma).apply(result, x);
265 0 : }
266 :
267 : template <typename T, typename Substitution>
268 86 : void replace_pbes_expressions(T& x,
269 : const Substitution& sigma,
270 : bool innermost = true,
271 : typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
272 : )
273 : {
274 86 : pbes_system::detail::make_replace_pbes_expressions_builder<pbes_system::pbes_expression_builder>(sigma, innermost).update(x);
275 86 : }
276 :
277 : template <typename T, typename Substitution>
278 1 : T replace_pbes_expressions(const T& x,
279 : const Substitution& sigma,
280 : bool innermost = true,
281 : typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
282 : )
283 : {
284 1 : T result;
285 1 : pbes_system::detail::make_replace_pbes_expressions_builder<pbes_system::pbes_expression_builder>(sigma, innermost).apply(result, x);
286 1 : return result;
287 0 : }
288 :
289 : } // namespace pbes_system
290 :
291 : } // namespace mcrl2
292 :
293 : #ifndef MCRL2_PBES_SUBSTITUTIONS_H
294 : #include "mcrl2/pbes/substitutions.h"
295 : #endif
296 :
297 : #endif // MCRL2_PBES_REPLACE_H
|
