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/rewriters/data_rewriter.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_REWRITERS_DATA_REWRITER_H
13 : #define MCRL2_PBES_REWRITERS_DATA_REWRITER_H
14 :
15 : #include "mcrl2/data/substitutions/no_substitution.h"
16 : #include "mcrl2/pbes/builder.h"
17 :
18 : namespace mcrl2 {
19 :
20 : namespace pbes_system {
21 :
22 : namespace detail {
23 :
24 : template <typename DataRewriter, typename SubstitutionFunction>
25 : const data::data_expression data_rewrite(const data::data_expression& x, const DataRewriter& R, SubstitutionFunction& sigma)
26 : {
27 : mCRL2log(log::trace) << "data_rewrite " << x << sigma << " -> " << R(x, sigma) << std::endl;
28 : return R(x, sigma);
29 : }
30 :
31 : template <typename DataRewriter, typename SubstitutionFunction>
32 122717 : void data_rewrite(data::data_expression& result, const data::data_expression& x, const DataRewriter& R, SubstitutionFunction& sigma)
33 : {
34 122717 : mCRL2log(log::trace) << "data_rewrite " << x << sigma << " -> " << R(x, sigma) << std::endl;
35 122717 : R(result, x, sigma);
36 122717 : }
37 :
38 : template <typename DataRewriter>
39 : const data::data_expression data_rewrite(const data::data_expression& x, const DataRewriter& R, data::no_substitution&)
40 : {
41 : mCRL2log(log::trace) << "data_rewrite " << x << "[]" << " -> " << R(x) << std::endl;
42 : return R(x);
43 : }
44 :
45 : template <typename DataRewriter>
46 13797 : void data_rewrite(data::data_expression& result, const data::data_expression& x, const DataRewriter& R, data::no_substitution&)
47 : {
48 13797 : mCRL2log(log::trace) << "data_rewrite " << x << "[]" << " -> " << R(x) << std::endl;
49 13797 : result = R(x);
50 13797 : }
51 :
52 : template <template <class> class Builder, class Derived, class DataRewriter, class SubstitutionFunction = data::no_substitution>
53 : struct add_data_rewriter: public Builder<Derived>
54 : {
55 : typedef Builder<Derived> super;
56 : using super::apply;
57 :
58 : const DataRewriter& R;
59 : SubstitutionFunction& sigma;
60 :
61 7092 : add_data_rewriter(const DataRewriter& R_, SubstitutionFunction& sigma_)
62 7092 : : R(R_), sigma(sigma_)
63 7092 : {}
64 :
65 : template <class T>
66 31639 : void apply(T& result, const data::data_expression& x)
67 : {
68 31639 : data_rewrite(atermpp::reference_cast<data::data_expression>(result), x, R, sigma);
69 31639 : }
70 :
71 : template <class T>
72 13667 : void apply(T& result, const propositional_variable_instantiation& x)
73 : {
74 41001 : make_propositional_variable_instantiation(
75 : result,
76 13667 : x.name(),
77 41001 : [this, &x](data::data_expression_list& r) -> void
78 13667 : { atermpp::make_term_list<data::data_expression>(
79 : r,
80 13667 : x.parameters().begin(),
81 13667 : x.parameters().end(),
82 209750 : [this](data::data_expression& r1, const data::data_expression& arg) -> void
83 104875 : { data_rewrite(r1, arg, R, sigma); } ) ;
84 : });
85 13667 : }
86 : };
87 :
88 : template <typename Derived, typename DataRewriter, typename SubstitutionFunction>
89 : struct data_rewriter_builder: public add_data_rewriter<pbes_system::pbes_expression_builder, Derived, DataRewriter, SubstitutionFunction>
90 : {
91 : typedef add_data_rewriter<pbes_system::pbes_expression_builder, Derived, DataRewriter, SubstitutionFunction> super;
92 : using super::enter;
93 : using super::leave;
94 :
95 139 : data_rewriter_builder(const DataRewriter& R, SubstitutionFunction& sigma)
96 139 : : super(R, sigma)
97 139 : {}
98 : };
99 :
100 : template <template <class, class, class> class Builder, class DataRewriter, class SubstitutionFunction>
101 : struct apply_rewriter_builder: public Builder<apply_rewriter_builder<Builder, DataRewriter, SubstitutionFunction>, DataRewriter, SubstitutionFunction>
102 : {
103 : typedef Builder<apply_rewriter_builder<Builder, DataRewriter, SubstitutionFunction>, DataRewriter, SubstitutionFunction> super;
104 : using super::enter;
105 : using super::leave;
106 :
107 1159 : apply_rewriter_builder(const DataRewriter& datar, SubstitutionFunction& sigma)
108 1159 : : super(datar, sigma)
109 1159 : {}
110 : };
111 :
112 : template <template <class, class, class> class Builder, class DataRewriter, class SubstitutionFunction>
113 : apply_rewriter_builder<Builder, DataRewriter, SubstitutionFunction>
114 1159 : make_apply_rewriter_builder(const DataRewriter& datar, SubstitutionFunction& sigma)
115 : {
116 1159 : return apply_rewriter_builder<Builder, DataRewriter, SubstitutionFunction>(datar, sigma);
117 : }
118 :
119 : } // namespace detail
120 :
121 : /// \brief A rewriter that applies a data rewriter to data expressions in a term.
122 : template <typename DataRewriter>
123 : struct data_rewriter
124 : {
125 : typedef pbes_expression term_type;
126 : typedef data::variable variable_type;
127 :
128 : const DataRewriter& R;
129 :
130 15 : data_rewriter(const DataRewriter& R_)
131 15 : : R(R_)
132 15 : {}
133 :
134 85 : pbes_expression operator()(const pbes_expression& x) const
135 : {
136 : data::no_substitution sigma;
137 85 : pbes_expression result;
138 85 : detail::make_apply_rewriter_builder<detail::data_rewriter_builder>(R, sigma).apply(result, x);
139 170 : return result;
140 0 : }
141 :
142 : template <typename SubstitutionFunction>
143 14 : pbes_expression operator()(const pbes_expression& x, SubstitutionFunction& sigma) const
144 : {
145 14 : pbes_expression result;
146 14 : detail::make_apply_rewriter_builder<detail::data_rewriter_builder>(R, sigma).apply(result, x);
147 14 : return result;
148 0 : }
149 : };
150 :
151 : } // namespace pbes_system
152 :
153 : } // namespace mcrl2
154 :
155 : #endif // MCRL2_PBES_REWRITERS_DATA_REWRITER_H
|
