Line data Source code
1 : // Author(s): Jan Friso Groote
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/replace_capture_avoiding_with_an_identifier_generator.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_DATA_REPLACE_CAPTURE_AVOIDING_WITH_AN_IDENTIFIER_GENERATOR_H
13 : #define MCRL2_DATA_REPLACE_CAPTURE_AVOIDING_WITH_AN_IDENTIFIER_GENERATOR_H
14 :
15 : #include "mcrl2/data/add_binding.h"
16 : #include "mcrl2/data/builder.h"
17 :
18 : namespace mcrl2 {
19 :
20 : namespace data {
21 :
22 : namespace detail {
23 :
24 : template <typename Substitution, typename IdentifierGenerator>
25 : class substitution_updater_with_an_identifier_generator
26 : {
27 : protected:
28 : Substitution& m_sigma;
29 : IdentifierGenerator& m_id_generator;
30 : std::vector<data::assignment> m_undo; // why not a stack datatype?
31 :
32 : public:
33 55832 : substitution_updater_with_an_identifier_generator(Substitution& sigma, IdentifierGenerator& id_generator)
34 55832 : : m_sigma(sigma), m_id_generator(id_generator)
35 55832 : {}
36 :
37 57352 : Substitution& substitution()
38 : {
39 57352 : return m_sigma;
40 : }
41 :
42 100 : data::variable bind(const data::variable& v)
43 : {
44 100 : m_undo.push_back(data::assignment(v, m_sigma(v))); // save the old assignment of m_sigma.
45 100 : if (m_sigma.variable_occurs_in_a_rhs(v)) // v notin FV(m_sigma).
46 : {
47 0 : m_sigma[v] = v; // Clear sigma[v].
48 0 : return v;
49 : }
50 : else
51 : {
52 200 : data::variable w(m_id_generator(v.name()), v.sort());
53 100 : m_sigma[v] = w;
54 100 : return w;
55 100 : }
56 : }
57 :
58 : data::variable push(const data::variable& v)
59 : {
60 : return bind(v);
61 : }
62 :
63 100 : void pop(const data::variable& )
64 : {
65 100 : const data::assignment& a = m_undo.back();
66 100 : m_sigma[a.lhs()] = a.rhs();
67 100 : m_undo.pop_back();
68 100 : }
69 :
70 : template <typename VariableContainer>
71 100 : VariableContainer push(const VariableContainer& container)
72 : {
73 100 : std::vector<data::variable> result;
74 300 : for (const variable& v: container)
75 : {
76 100 : result.push_back(bind(v));
77 : }
78 200 : return VariableContainer(result.begin(), result.end());
79 100 : }
80 :
81 : template <typename VariableContainer>
82 100 : void pop(const VariableContainer& container)
83 : {
84 300 : for (const variable& v: container)
85 : {
86 100 : pop(v);
87 : }
88 100 : }
89 : };
90 :
91 : template <typename Substitution, typename IdentifierGenerator>
92 : data::variable update_substitution(Substitution& sigma, const data::variable& v, const std::multiset<data::variable>& V, IdentifierGenerator& id_generator)
93 : {
94 : using utilities::detail::contains;
95 : if (!contains(V, v) && sigma(v) == v)
96 : {
97 : return v;
98 : }
99 : else
100 : {
101 : id_generator.add_identifier(v.name());
102 : data::variable w(id_generator(v.name()), v.sort());
103 :
104 : while (sigma(w) != w || contains(V, w))
105 : {
106 : w = data::variable(id_generator(v.name()), v.sort());
107 : }
108 : sigma[v] = w;
109 : return w;
110 : }
111 : }
112 :
113 : template <typename Substitution, typename IdentifierGenerator, typename VariableContainer>
114 : VariableContainer update_substitution(Substitution& sigma, const VariableContainer& v, const std::multiset<data::variable>& V, IdentifierGenerator& id_generator)
115 : {
116 : std::vector<data::variable> result;
117 : for (typename VariableContainer::const_iterator i = v.begin(); i != v.end(); ++i)
118 : {
119 : result.push_back(update_substitution(sigma, *i, V, id_generator));
120 : }
121 : return VariableContainer(result.begin(), result.end());
122 : }
123 :
124 : // Helper code for replace_capture_avoiding_variables_with_an_identifier_generator.
125 : template<template<class> class Builder,
126 : template<template<class> class, class, class, class> class Binder, class Substitution, class IdentifierGenerator>
127 : struct replace_capture_avoiding_variables_builder_with_an_identifier_generator
128 : : public Binder<Builder, replace_capture_avoiding_variables_builder_with_an_identifier_generator<Builder, Binder, Substitution, IdentifierGenerator>, Substitution, IdentifierGenerator>
129 : {
130 : typedef Binder<Builder, replace_capture_avoiding_variables_builder_with_an_identifier_generator<Builder, Binder, Substitution, IdentifierGenerator>, Substitution, IdentifierGenerator> super;
131 : using super::enter;
132 : using super::leave;
133 : using super::apply;
134 : using super::update;
135 :
136 55832 : replace_capture_avoiding_variables_builder_with_an_identifier_generator(Substitution& sigma,
137 : IdentifierGenerator& id_generator)
138 55832 : : super(sigma, id_generator)
139 : {
140 55832 : }
141 : };
142 :
143 : template<template<class> class Builder,
144 : template<template<class> class, class, class, class> class Binder, class Substitution, class IdentifierGenerator>
145 : replace_capture_avoiding_variables_builder_with_an_identifier_generator<Builder, Binder, Substitution, IdentifierGenerator>
146 55832 : apply_replace_capture_avoiding_variables_builder_with_an_identifier_generator(Substitution& sigma,
147 : IdentifierGenerator& id_generator)
148 : {
149 : return replace_capture_avoiding_variables_builder_with_an_identifier_generator<Builder, Binder, Substitution, IdentifierGenerator>(
150 55832 : sigma, id_generator);
151 : }
152 :
153 : // In the class below, the IdentifierGenerator is expected to generate fresh identifiers, not
154 : // occurring anywhere using the operator (). The enumerator_identifier_generator can do this.
155 : // The substitution has as property that it provides a method "variables_in_rhs" yielding the
156 : // variables occurring in the right hand side of assignments. The mutable_indexed_substitution has this
157 : // method.
158 : template<template<class> class Builder, class Derived, class Substitution, class IdentifierGenerator>
159 : struct add_capture_avoiding_replacement_with_an_identifier_generator : public Builder<Derived>
160 : {
161 : typedef Builder<Derived> super;
162 : using super::enter;
163 : using super::leave;
164 : using super::apply;
165 : using super::update;
166 :
167 : protected:
168 : substitution_updater_with_an_identifier_generator <Substitution, IdentifierGenerator> update_sigma;
169 :
170 : public:
171 55832 : add_capture_avoiding_replacement_with_an_identifier_generator(Substitution& sigma_,
172 : IdentifierGenerator& id_generator_)
173 55832 : : update_sigma(sigma_, id_generator_)
174 : {
175 55832 : }
176 :
177 : template <class T>
178 57352 : void apply(T& result, const variable& v)
179 : {
180 57352 : result = update_sigma.substitution()(v);
181 57352 : }
182 :
183 : template <class T>
184 0 : void apply(T& result, const data::where_clause& x)
185 : {
186 0 : const auto& assignments = atermpp::container_cast<data::assignment_list>(x.declarations());
187 0 : std::vector<data::variable> tmp;
188 0 : for (const data::assignment& a: assignments)
189 : {
190 0 : tmp.push_back(a.lhs());
191 : }
192 0 : std::vector<data::variable> v = update_sigma.push(tmp);
193 :
194 : // The updated substitution should be applied to the body.
195 0 : data::data_expression new_body;
196 0 : apply(new_body, x.body());
197 0 : update_sigma.pop(v);
198 :
199 : // The original substitution should be applied to the right hand sides of the assignments.
200 0 : std::vector<data::assignment> a;
201 0 : std::vector<data::variable>::const_iterator j = v.begin();
202 0 : for (data::assignment_list::const_iterator i = assignments.begin(); i != assignments.end(); ++i, ++j)
203 : {
204 0 : data::data_expression rhs;
205 0 : apply(rhs, i->rhs());
206 0 : a.push_back(data::assignment(*j, rhs));
207 : }
208 0 : data::make_where_clause(result, new_body, assignment_list(a.begin(), a.end()));
209 0 : }
210 :
211 : template <class T>
212 0 : void apply(T& result, const data::forall& x)
213 : {
214 0 : const data::variable_list v = update_sigma.push(x.variables());
215 0 : data::data_expression body;
216 0 : apply(body, x.body());
217 0 : data::make_forall(result, v, body);
218 0 : update_sigma.pop(v);
219 0 : }
220 :
221 : template <class T>
222 0 : void apply(T& result, const data::exists& x)
223 : {
224 0 : const data::variable_list v = update_sigma.push(x.variables());
225 0 : data::data_expression body;
226 0 : apply(body, x.body());
227 0 : data::make_exists(result, v, body);
228 0 : update_sigma.pop(v);
229 0 : }
230 :
231 : template <class T>
232 86 : void apply(T& result, const data::lambda& x)
233 : {
234 86 : const data::variable_list v = update_sigma.push(x.variables());
235 86 : data::data_expression body;
236 86 : apply(body, x.body());
237 86 : data::make_lambda(result, v, body);
238 86 : update_sigma.pop(v);
239 86 : }
240 :
241 : template <class T>
242 : void apply(T& /* result */, data_equation& /* x */)
243 : {
244 : throw mcrl2::runtime_error("not implemented yet");
245 : }
246 : };
247 :
248 : } // namespace detail
249 :
250 : //--- start generated data replace_capture_avoiding_with_identifier_generator code ---//
251 : /// \\brief Applies sigma as a capture avoiding substitution to x using an identifier generator.
252 : /// \\details This substitution function is much faster than replace_variables_capture_avoiding, but
253 : /// it requires an identifier generator that generates strings for fresh variables. These
254 : /// strings must be unique in the sense that they have not been used for other variables.
255 : /// \\param x The object to which the subsitution is applied.
256 : /// \\param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its
257 : /// right hand side. The class maintain_variables_in_rhs is useful for this purpose.
258 : /// \\param id_generator A generator that generates unique strings, not yet used as variable names.
259 :
260 : template <typename T, typename Substitution, typename IdentifierGenerator>
261 : void replace_variables_capture_avoiding_with_an_identifier_generator(T& x,
262 : Substitution& sigma,
263 : IdentifierGenerator& id_generator,
264 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
265 : )
266 : {
267 : data::detail::apply_replace_capture_avoiding_variables_builder_with_an_identifier_generator<data::data_expression_builder, data::detail::add_capture_avoiding_replacement_with_an_identifier_generator>(sigma, id_generator).update(x);
268 : }
269 :
270 : /// \\brief Applies sigma as a capture avoiding substitution to x using an identifier generator..
271 : /// \\details This substitution function is much faster than replace_variables_capture_avoiding, but
272 : /// it requires an identifier generator that generates strings for fresh variables. These
273 : /// strings must be unique in the sense that they have not been used for other variables.
274 : /// \\param x The object to which the substiution is applied.
275 : /// \\param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its
276 : /// right hand side. The class maintain_variables_in_rhs is useful for this purpose.
277 : /// \\param id_generator A generator that generates unique strings, not yet used as variable names.
278 : /// \\return The result is the term x to which sigma has been applied.
279 : template <typename T, typename Substitution, typename IdentifierGenerator>
280 : T replace_variables_capture_avoiding_with_an_identifier_generator(const T& x,
281 : Substitution& sigma,
282 : IdentifierGenerator& id_generator,
283 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
284 : )
285 : {
286 : T result;
287 : data::detail::apply_replace_capture_avoiding_variables_builder_with_an_identifier_generator<data::data_expression_builder, data::detail::add_capture_avoiding_replacement_with_an_identifier_generator>(sigma, id_generator).apply(result, x);
288 : return result;
289 : }
290 : //--- end generated data replace_capture_avoiding_with_identifier_generator code ---//
291 :
292 : } // namespace data
293 :
294 : } // namespace mcrl2
295 :
296 : #endif // MCRL2_DATA_REPLACE_CAPTURE_AVOIDING_WITH_AN_IDENTIFIER_GENERATOR_H
|
