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/process/replace_capture_avoiding_with_an_identifier_generator.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PROCESS_REPLACE_CAPTURE_AVOIDING_WITH_AN_IDENTIFIER_GENERATOR_H
13 : #define MCRL2_PROCESS_REPLACE_CAPTURE_AVOIDING_WITH_AN_IDENTIFIER_GENERATOR_H
14 :
15 : #include "mcrl2/data/replace_capture_avoiding_with_an_identifier_generator.h"
16 : #include "mcrl2/process/add_binding.h"
17 : #include "mcrl2/process/builder.h"
18 :
19 : namespace mcrl2 {
20 :
21 : namespace process {
22 :
23 : namespace detail {
24 :
25 : // Below the definitions are given for capture avoiding subsitution witn an identifier generator.
26 : template <template <class> class Builder, class Derived, class Substitution, class IdentifierGenerator>
27 : struct add_capture_avoiding_replacement_with_an_identifier_generator: public data::detail::add_capture_avoiding_replacement_with_an_identifier_generator<Builder, Derived, Substitution, IdentifierGenerator>
28 : {
29 : typedef data::detail::add_capture_avoiding_replacement_with_an_identifier_generator<Builder, Derived, Substitution, IdentifierGenerator> super;
30 : using super::enter;
31 : using super::leave;
32 : using super::apply;
33 : using super::update;
34 : using super::update_sigma;
35 :
36 210 : data::assignment_list::const_iterator find_variable(const data::assignment_list& a, const data::variable& v) const
37 : {
38 307 : for (data::assignment_list::const_iterator i = a.begin(); i != a.end(); ++i)
39 : {
40 294 : if (i->lhs() == v)
41 : {
42 197 : return i;
43 : }
44 : }
45 13 : return a.end();
46 : }
47 :
48 55832 : add_capture_avoiding_replacement_with_an_identifier_generator(Substitution& sigma, IdentifierGenerator& id_generator)
49 55832 : : super(sigma, id_generator)
50 55832 : { }
51 :
52 : template <class T>
53 163 : void apply(T& result, const process::process_instance_assignment& x)
54 : {
55 163 : static_cast<Derived&>(*this).enter(x);
56 163 : const data::assignment_list& a = x.assignments();
57 163 : std::vector<data::assignment> v;
58 :
59 536 : for (const data::variable& variable: x.identifier().variables())
60 : {
61 210 : const data::assignment_list::const_iterator k = find_variable(a, variable);
62 210 : if (k == a.end())
63 : {
64 13 : data::data_expression e;
65 13 : apply(e, variable);
66 13 : if (e != variable)
67 : {
68 0 : v.emplace_back(variable, e);
69 : }
70 13 : }
71 : else
72 : {
73 197 : data::data_expression rhs;
74 197 : apply(rhs, k->rhs());
75 197 : v.emplace_back(k->lhs(), rhs);
76 197 : }
77 : }
78 163 : process::make_process_instance_assignment(result, x.identifier(), data::assignment_list(v.begin(), v.end()));
79 163 : static_cast<Derived&>(*this).leave(x);
80 163 : }
81 :
82 : template <class T>
83 7 : void apply(T& result, const sum& x)
84 : {
85 7 : data::variable_list v = update_sigma.push(x.variables());
86 7 : process_expression body;
87 7 : apply(body, x.operand());
88 7 : make_sum(result, v, body);
89 7 : update_sigma.pop(v);
90 7 : }
91 :
92 : template <class T>
93 7 : void apply(T& result, const stochastic_operator& x)
94 : {
95 7 : data::variable_list v = update_sigma.push(x.variables());
96 7 : process_expression body;
97 7 : apply(body, x.operand());
98 7 : data::data_expression dist;
99 7 : apply(dist, x.distribution());
100 7 : make_stochastic_operator(result, v, dist, body);
101 7 : update_sigma.pop(v);
102 7 : }
103 : };
104 :
105 : template <template <class> class Builder, template <template <class> class, class, class, class> class Binder, class Substitution, class IdentifierGenerator>
106 : struct replace_capture_avoiding_variables__with_an_identifier_generator_builder: public Binder<Builder, replace_capture_avoiding_variables__with_an_identifier_generator_builder<Builder, Binder, Substitution, IdentifierGenerator>, Substitution, IdentifierGenerator>
107 : {
108 : typedef Binder<Builder, replace_capture_avoiding_variables__with_an_identifier_generator_builder<Builder, Binder, Substitution, IdentifierGenerator>, Substitution, IdentifierGenerator> super;
109 : using super::enter;
110 : using super::leave;
111 : using super::apply;
112 : using super::update;
113 :
114 : replace_capture_avoiding_variables__with_an_identifier_generator_builder(Substitution& sigma, IdentifierGenerator& id_generator)
115 : : super(sigma, id_generator)
116 : { }
117 : };
118 :
119 : template <template <class> class Builder, template <template <class> class, class, class, class> class Binder, class Substitution, class IdentifierGenerator>
120 : replace_capture_avoiding_variables__with_an_identifier_generator_builder<Builder, Binder, Substitution, IdentifierGenerator>
121 : apply_replace_capture_avoiding_variables__with_an_identifier_generator_builder(Substitution& sigma, IdentifierGenerator& id_generator)
122 : {
123 : return replace_capture_avoiding_variables__with_an_identifier_generator_builder<Builder, Binder, Substitution, IdentifierGenerator>(sigma, id_generator);
124 : }
125 :
126 : } // namespace detail
127 :
128 : //--- start generated process replace_capture_avoiding_with_identifier_generator code ---//
129 : /// \\brief Applies sigma as a capture avoiding substitution to x using an identifier generator.
130 : /// \\details This substitution function is much faster than replace_variables_capture_avoiding, but
131 : /// it requires an identifier generator that generates strings for fresh variables. These
132 : /// strings must be unique in the sense that they have not been used for other variables.
133 : /// \\param x The object to which the subsitution is applied.
134 : /// \\param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its
135 : /// right hand side. The class maintain_variables_in_rhs is useful for this purpose.
136 : /// \\param id_generator A generator that generates unique strings, not yet used as variable names.
137 :
138 : template <typename T, typename Substitution, typename IdentifierGenerator>
139 : void replace_variables_capture_avoiding_with_an_identifier_generator(T& x,
140 : Substitution& sigma,
141 : IdentifierGenerator& id_generator,
142 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
143 : )
144 : {
145 : data::detail::apply_replace_capture_avoiding_variables_builder_with_an_identifier_generator<process::data_expression_builder, process::detail::add_capture_avoiding_replacement_with_an_identifier_generator>(sigma, id_generator).update(x);
146 : }
147 :
148 : /// \\brief Applies sigma as a capture avoiding substitution to x using an identifier generator..
149 : /// \\details This substitution function is much faster than replace_variables_capture_avoiding, but
150 : /// it requires an identifier generator that generates strings for fresh variables. These
151 : /// strings must be unique in the sense that they have not been used for other variables.
152 : /// \\param x The object to which the substiution is applied.
153 : /// \\param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its
154 : /// right hand side. The class maintain_variables_in_rhs is useful for this purpose.
155 : /// \\param id_generator A generator that generates unique strings, not yet used as variable names.
156 : /// \\return The result is the term x to which sigma has been applied.
157 : template <typename T, typename Substitution, typename IdentifierGenerator>
158 50609 : T replace_variables_capture_avoiding_with_an_identifier_generator(const T& x,
159 : Substitution& sigma,
160 : IdentifierGenerator& id_generator,
161 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
162 : )
163 : {
164 50609 : T result;
165 50609 : data::detail::apply_replace_capture_avoiding_variables_builder_with_an_identifier_generator<process::data_expression_builder, process::detail::add_capture_avoiding_replacement_with_an_identifier_generator>(sigma, id_generator).apply(result, x);
166 50609 : return result;
167 0 : }
168 : //--- end generated process replace_capture_avoiding_with_identifier_generator code ---//
169 :
170 : } // namespace process
171 :
172 : } // namespace mcrl2
173 :
174 : #endif // MCRL2_PROCESS_REPLACE_CAPTURE_AVOIDING_WITH_AN_IDENTIFIER_GENERATOR_H
|
