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/process/replace_capture_avoiding.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PROCESS_REPLACE_CAPTURE_AVOIDING_H
13 : #define MCRL2_PROCESS_REPLACE_CAPTURE_AVOIDING_H
14 :
15 : #include "mcrl2/data/replace_capture_avoiding.h"
16 : #include "mcrl2/process/builder.h"
17 : #include "mcrl2/process/find.h"
18 :
19 : namespace mcrl2 {
20 :
21 : namespace process {
22 :
23 : namespace detail {
24 :
25 : template<template<class> class Builder, class Derived, class Substitution>
26 : struct add_capture_avoiding_replacement
27 : : public data::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution>
28 : {
29 : typedef data::detail::add_capture_avoiding_replacement <Builder, Derived, Substitution> super;
30 : using super::enter;
31 : using super::leave;
32 : using super::apply;
33 : using super::update;
34 : using super::sigma;
35 :
36 4 : data::assignment_list::const_iterator find_variable(const data::assignment_list& a, const data::variable& v) const
37 : {
38 6 : for (auto i = a.begin(); i != a.end(); ++i)
39 : {
40 4 : if (i->lhs() == v)
41 : {
42 2 : return i;
43 : }
44 : }
45 2 : return a.end();
46 : }
47 :
48 1711 : explicit add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater<Substitution>& sigma)
49 1711 : : super(sigma)
50 1711 : { }
51 :
52 : template <class T>
53 2 : void apply(T& result, const process::process_instance_assignment& x)
54 : {
55 2 : static_cast<Derived&>(*this).enter(x);
56 2 : const data::assignment_list& a = x.assignments();
57 2 : std::vector <data::assignment> v;
58 :
59 8 : for (const data::variable& variable: x.identifier().variables())
60 : {
61 4 : auto k = find_variable(a, variable);
62 4 : if (k == a.end())
63 : {
64 2 : data::data_expression e;
65 2 : apply(e, variable);
66 2 : if (e != variable)
67 : {
68 1 : v.emplace_back(variable, e);
69 : }
70 2 : }
71 : else
72 : {
73 2 : data::data_expression rhs;
74 2 : apply(rhs, k->rhs());
75 2 : v.emplace_back(k->lhs(), rhs);
76 2 : }
77 : }
78 2 : make_process_instance_assignment(result, x.identifier(),data::assignment_list(v.begin(), v.end()));
79 2 : static_cast<Derived&>(*this).leave(x);
80 2 : }
81 :
82 : template <class T>
83 2 : void apply(T& result, const sum& x)
84 : {
85 2 : data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
86 2 : process_expression body;
87 2 : apply(body, x.operand());
88 2 : make_sum(result, v1, body);
89 2 : sigma.remove_fresh_variable_assignments(x.variables());
90 2 : }
91 :
92 : template <class T>
93 0 : void apply(T& result, const stochastic_operator& x)
94 : {
95 0 : data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
96 0 : process_expression body;
97 0 : apply(body, x.operand());
98 0 : data::data_expression dist;
99 0 : apply(dist, x.distribution());
100 0 : make_stochastic_operator(result, v1, dist, body);
101 0 : sigma.remove_fresh_variable_assignments(x.variables());
102 0 : }
103 : };
104 :
105 : } // namespace detail
106 :
107 : //--- start generated process replace_capture_avoiding code ---//
108 : /// \\brief Applies sigma as a capture avoiding substitution to x.
109 : /// \\param x The object to which the subsitution is applied.
110 : /// \\param sigma A substitution.
111 : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
112 : template <typename T, typename Substitution>
113 : void replace_variables_capture_avoiding(T& x,
114 : Substitution& sigma,
115 : data::set_identifier_generator& id_generator,
116 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
117 : )
118 : {
119 : data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
120 : data::detail::apply_replace_capture_avoiding_variables_builder<process::data_expression_builder, process::detail::add_capture_avoiding_replacement>(sigma1).update(x);
121 : }
122 :
123 : /// \\brief Applies sigma as a capture avoiding substitution to x.
124 : /// \\param x The object to which the substiution is applied.
125 : /// \\param sigma A substitution.
126 : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
127 : template <typename T, typename Substitution>
128 25 : T replace_variables_capture_avoiding(const T& x,
129 : Substitution& sigma,
130 : data::set_identifier_generator& id_generator,
131 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
132 : )
133 : {
134 25 : data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
135 25 : T result;
136 25 : data::detail::apply_replace_capture_avoiding_variables_builder<process::data_expression_builder, process::detail::add_capture_avoiding_replacement>(sigma1).apply(result, x);
137 50 : return result;
138 25 : }
139 :
140 : /// \\brief Applies sigma as a capture avoiding substitution to x.
141 : /// \\param x The object to which the subsitution is applied.
142 : /// \\param sigma A substitution.
143 : template <typename T, typename Substitution>
144 : void replace_variables_capture_avoiding(T& x,
145 : Substitution& sigma,
146 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
147 : )
148 : {
149 : data::set_identifier_generator id_generator;
150 : id_generator.add_identifiers(process::find_identifiers(x));
151 : for (const data::variable& v: substitution_variables(sigma))
152 : {
153 : id_generator.add_identifier(v.name());
154 : }
155 : process::replace_variables_capture_avoiding(x, sigma, id_generator);
156 : }
157 :
158 : /// \\brief Applies sigma as a capture avoiding substitution to x.
159 : /// \\param x The object to which the substiution is applied.
160 : /// \\param sigma A substitution.
161 : template <typename T, typename Substitution>
162 5 : T replace_variables_capture_avoiding(const T& x,
163 : Substitution& sigma,
164 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
165 : )
166 : {
167 5 : data::set_identifier_generator id_generator;
168 5 : id_generator.add_identifiers(process::find_identifiers(x));
169 8 : for (const data::variable& v: substitution_variables(sigma))
170 : {
171 3 : id_generator.add_identifier(v.name());
172 : }
173 10 : return process::replace_variables_capture_avoiding(x, sigma, id_generator);
174 5 : }
175 : //--- end generated process replace_capture_avoiding code ---//
176 :
177 : } // namespace process
178 :
179 : } // namespace mcrl2
180 :
181 : #endif // MCRL2_PROCESS_REPLACE_CAPTURE_AVOIDING_H
|
