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/modal_formula/replace_capture_avoiding.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_MODAL_FORMULA_REPLACE_CAPTURE_AVOIDING_H
13 : #define MCRL2_MODAL_FORMULA_REPLACE_CAPTURE_AVOIDING_H
14 :
15 : #include "mcrl2/lps/replace_capture_avoiding.h"
16 : #include "mcrl2/modal_formula/builder.h"
17 : #include "mcrl2/modal_formula/find.h"
18 :
19 : namespace mcrl2 {
20 :
21 : namespace action_formulas {
22 :
23 : namespace detail {
24 :
25 : template <template <class> class Builder, class Derived, class Substitution>
26 : struct add_capture_avoiding_replacement: public lps::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution>
27 : {
28 : typedef lps::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution> super;
29 : using super::enter;
30 : using super::leave;
31 : using super::update;
32 : using super::apply;
33 : using super::sigma;
34 :
35 9 : explicit add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater<Substitution>& sigma)
36 9 : : super(sigma)
37 9 : { }
38 :
39 : template <class T>
40 0 : void apply(T& result, const forall& x)
41 : {
42 0 : data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
43 0 : action_formula body;
44 0 : apply(body, x.body());
45 0 : make_forall(result, v1, body);
46 0 : sigma.remove_fresh_variable_assignments(x.variables());
47 0 : }
48 :
49 : template <class T>
50 0 : void apply(T& result, const exists& x)
51 : {
52 0 : data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
53 0 : action_formula body;
54 0 : apply(body, x.body());
55 0 : make_exists(result, v1, body);
56 0 : sigma.remove_fresh_variable_assignments(x.variables());
57 0 : }
58 : };
59 :
60 : } // namespace detail
61 :
62 : //--- start generated action_formulas replace_capture_avoiding code ---//
63 : /// \\brief Applies sigma as a capture avoiding substitution to x.
64 : /// \\param x The object to which the subsitution is applied.
65 : /// \\param sigma A substitution.
66 : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
67 : template <typename T, typename Substitution>
68 : void replace_variables_capture_avoiding(T& x,
69 : Substitution& sigma,
70 : data::set_identifier_generator& id_generator,
71 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
72 : )
73 : {
74 : data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
75 : data::detail::apply_replace_capture_avoiding_variables_builder<action_formulas::data_expression_builder, action_formulas::detail::add_capture_avoiding_replacement>(sigma1).update(x);
76 : }
77 :
78 : /// \\brief Applies sigma as a capture avoiding substitution to x.
79 : /// \\param x The object to which the substiution is applied.
80 : /// \\param sigma A substitution.
81 : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
82 : template <typename T, typename Substitution>
83 9 : T replace_variables_capture_avoiding(const T& x,
84 : Substitution& sigma,
85 : data::set_identifier_generator& id_generator,
86 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
87 : )
88 : {
89 9 : data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
90 9 : T result;
91 9 : data::detail::apply_replace_capture_avoiding_variables_builder<action_formulas::data_expression_builder, action_formulas::detail::add_capture_avoiding_replacement>(sigma1).apply(result, x);
92 18 : return result;
93 9 : }
94 :
95 : /// \\brief Applies sigma as a capture avoiding substitution to x.
96 : /// \\param x The object to which the subsitution is applied.
97 : /// \\param sigma A substitution.
98 : template <typename T, typename Substitution>
99 : void replace_variables_capture_avoiding(T& x,
100 : Substitution& sigma,
101 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
102 : )
103 : {
104 : data::set_identifier_generator id_generator;
105 : id_generator.add_identifiers(action_formulas::find_identifiers(x));
106 : for (const data::variable& v: substitution_variables(sigma))
107 : {
108 : id_generator.add_identifier(v.name());
109 : }
110 : action_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
111 : }
112 :
113 : /// \\brief Applies sigma as a capture avoiding substitution to x.
114 : /// \\param x The object to which the substiution is applied.
115 : /// \\param sigma A substitution.
116 : template <typename T, typename Substitution>
117 9 : T replace_variables_capture_avoiding(const T& x,
118 : Substitution& sigma,
119 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
120 : )
121 : {
122 9 : data::set_identifier_generator id_generator;
123 9 : id_generator.add_identifiers(action_formulas::find_identifiers(x));
124 18 : for (const data::variable& v: substitution_variables(sigma))
125 : {
126 9 : id_generator.add_identifier(v.name());
127 : }
128 18 : return action_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
129 9 : }
130 : //--- end generated action_formulas replace_capture_avoiding code ---//
131 :
132 : } // namespace action_formulas
133 :
134 : } // namespace mcrl2
135 :
136 : namespace mcrl2 {
137 :
138 : namespace regular_formulas {
139 :
140 : namespace detail {
141 :
142 : template <template <class> class Builder, class Derived, class Substitution>
143 : struct add_capture_avoiding_replacement: public action_formulas::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution>
144 : {
145 : typedef action_formulas::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution> super;
146 : using super::enter;
147 : using super::leave;
148 : using super::update;
149 : using super::apply;
150 : using super::sigma;
151 :
152 : explicit add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater<Substitution>& sigma)
153 : : super(sigma)
154 : { }
155 : };
156 :
157 : } // namespace detail
158 :
159 : //--- start generated regular_formulas replace_capture_avoiding code ---//
160 : /// \\brief Applies sigma as a capture avoiding substitution to x.
161 : /// \\param x The object to which the subsitution is applied.
162 : /// \\param sigma A substitution.
163 : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
164 : template <typename T, typename Substitution>
165 : void replace_variables_capture_avoiding(T& x,
166 : Substitution& sigma,
167 : data::set_identifier_generator& id_generator,
168 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
169 : )
170 : {
171 : data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
172 : data::detail::apply_replace_capture_avoiding_variables_builder<regular_formulas::data_expression_builder, regular_formulas::detail::add_capture_avoiding_replacement>(sigma1).update(x);
173 : }
174 :
175 : /// \\brief Applies sigma as a capture avoiding substitution to x.
176 : /// \\param x The object to which the substiution is applied.
177 : /// \\param sigma A substitution.
178 : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
179 : template <typename T, typename Substitution>
180 : T replace_variables_capture_avoiding(const T& x,
181 : Substitution& sigma,
182 : data::set_identifier_generator& id_generator,
183 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
184 : )
185 : {
186 : data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
187 : T result;
188 : data::detail::apply_replace_capture_avoiding_variables_builder<regular_formulas::data_expression_builder, regular_formulas::detail::add_capture_avoiding_replacement>(sigma1).apply(result, x);
189 : return result;
190 : }
191 :
192 : /// \\brief Applies sigma as a capture avoiding substitution to x.
193 : /// \\param x The object to which the subsitution is applied.
194 : /// \\param sigma A substitution.
195 : template <typename T, typename Substitution>
196 : void replace_variables_capture_avoiding(T& x,
197 : Substitution& sigma,
198 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
199 : )
200 : {
201 : data::set_identifier_generator id_generator;
202 : id_generator.add_identifiers(regular_formulas::find_identifiers(x));
203 : for (const data::variable& v: substitution_variables(sigma))
204 : {
205 : id_generator.add_identifier(v.name());
206 : }
207 : regular_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
208 : }
209 :
210 : /// \\brief Applies sigma as a capture avoiding substitution to x.
211 : /// \\param x The object to which the substiution is applied.
212 : /// \\param sigma A substitution.
213 : template <typename T, typename Substitution>
214 : T replace_variables_capture_avoiding(const T& x,
215 : Substitution& sigma,
216 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
217 : )
218 : {
219 : data::set_identifier_generator id_generator;
220 : id_generator.add_identifiers(regular_formulas::find_identifiers(x));
221 : for (const data::variable& v: substitution_variables(sigma))
222 : {
223 : id_generator.add_identifier(v.name());
224 : }
225 : return regular_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
226 : }
227 : //--- end generated regular_formulas replace_capture_avoiding code ---//
228 :
229 : } // namespace regular_formulas
230 :
231 : } // namespace mcrl2
232 :
233 : namespace mcrl2 {
234 :
235 : namespace state_formulas {
236 :
237 : namespace detail {
238 :
239 : template <template <class> class Builder, class Derived, class Substitution>
240 : struct add_capture_avoiding_replacement: public data::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution>
241 : {
242 : typedef data::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution> super;
243 : using super::enter;
244 : using super::leave;
245 : using super::update;
246 : using super::apply;
247 : using super::sigma;
248 :
249 : explicit add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater<Substitution>& sigma)
250 : : super(sigma)
251 : { }
252 :
253 : state_formula operator()(const forall& x)
254 : {
255 : data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
256 : state_formula result = forall(v1, (*this)(x.body()));
257 : sigma.remove_fresh_variable_assignments(x.variables());
258 : return result;
259 : }
260 :
261 : state_formula operator()(const exists& x)
262 : {
263 : data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
264 : state_formula result = exists(v1, (*this)(x.body()));
265 : sigma.remove_fresh_variable_assignments(x.variables());
266 : return result;
267 : }
268 : };
269 :
270 : } // namespace detail
271 :
272 : //--- start generated state_formulas replace_capture_avoiding code ---//
273 : /// \\brief Applies sigma as a capture avoiding substitution to x.
274 : /// \\param x The object to which the subsitution is applied.
275 : /// \\param sigma A substitution.
276 : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
277 : template <typename T, typename Substitution>
278 : void replace_variables_capture_avoiding(T& x,
279 : Substitution& sigma,
280 : data::set_identifier_generator& id_generator,
281 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
282 : )
283 : {
284 : data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
285 : data::detail::apply_replace_capture_avoiding_variables_builder<state_formulas::data_expression_builder, state_formulas::detail::add_capture_avoiding_replacement>(sigma1).update(x);
286 : }
287 :
288 : /// \\brief Applies sigma as a capture avoiding substitution to x.
289 : /// \\param x The object to which the substiution is applied.
290 : /// \\param sigma A substitution.
291 : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
292 : template <typename T, typename Substitution>
293 : T replace_variables_capture_avoiding(const T& x,
294 : Substitution& sigma,
295 : data::set_identifier_generator& id_generator,
296 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
297 : )
298 : {
299 : data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
300 : T result;
301 : data::detail::apply_replace_capture_avoiding_variables_builder<state_formulas::data_expression_builder, state_formulas::detail::add_capture_avoiding_replacement>(sigma1).apply(result, x);
302 : return result;
303 : }
304 :
305 : /// \\brief Applies sigma as a capture avoiding substitution to x.
306 : /// \\param x The object to which the subsitution is applied.
307 : /// \\param sigma A substitution.
308 : template <typename T, typename Substitution>
309 : void replace_variables_capture_avoiding(T& x,
310 : Substitution& sigma,
311 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
312 : )
313 : {
314 : data::set_identifier_generator id_generator;
315 : id_generator.add_identifiers(state_formulas::find_identifiers(x));
316 : for (const data::variable& v: substitution_variables(sigma))
317 : {
318 : id_generator.add_identifier(v.name());
319 : }
320 : state_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
321 : }
322 :
323 : /// \\brief Applies sigma as a capture avoiding substitution to x.
324 : /// \\param x The object to which the substiution is applied.
325 : /// \\param sigma A substitution.
326 : template <typename T, typename Substitution>
327 : T replace_variables_capture_avoiding(const T& x,
328 : Substitution& sigma,
329 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
330 : )
331 : {
332 : data::set_identifier_generator id_generator;
333 : id_generator.add_identifiers(state_formulas::find_identifiers(x));
334 : for (const data::variable& v: substitution_variables(sigma))
335 : {
336 : id_generator.add_identifier(v.name());
337 : }
338 : return state_formulas::replace_variables_capture_avoiding(x, sigma, id_generator);
339 : }
340 : //--- end generated state_formulas replace_capture_avoiding code ---//
341 :
342 : } // namespace state_formulas
343 :
344 : } // namespace mcrl2
345 :
346 : #endif // MCRL2_MODAL_FORMULA_REPLACE_CAPTURE_AVOIDING_H
|
