mCRL2
Loading...
Searching...
No Matches
data_rewriter.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_PBES_REWRITERS_DATA_REWRITER_H
13#define MCRL2_PBES_REWRITERS_DATA_REWRITER_H
14
16#include "mcrl2/pbes/builder.h"
17
18namespace mcrl2 {
19
20namespace pbes_system {
21
22namespace detail {
23
24template <typename DataRewriter, typename SubstitutionFunction>
25const 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
31template <typename DataRewriter, typename SubstitutionFunction>
32void data_rewrite(data::data_expression& result, const data::data_expression& x, const DataRewriter& R, SubstitutionFunction& sigma)
33{
34 mCRL2log(log::trace) << "data_rewrite " << x << sigma << " -> " << R(x, sigma) << std::endl;
35 R(result, x, sigma);
36}
37
38template <typename DataRewriter>
40{
41 mCRL2log(log::trace) << "data_rewrite " << x << "[]" << " -> " << R(x) << std::endl;
42 return R(x);
43}
44
45template <typename DataRewriter>
46void data_rewrite(data::data_expression& result, const data::data_expression& x, const DataRewriter& R, data::no_substitution&)
47{
48 mCRL2log(log::trace) << "data_rewrite " << x << "[]" << " -> " << R(x) << std::endl;
49 result = R(x);
50}
51
52template <template <class> class Builder, class Derived, class DataRewriter, class SubstitutionFunction = data::no_substitution>
53struct 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 add_data_rewriter(const DataRewriter& R_, SubstitutionFunction& sigma_)
62 : R(R_), sigma(sigma_)
63 {}
64
65 template <class T>
66 void apply(T& result, const data::data_expression& x)
67 {
68 data_rewrite(atermpp::reference_cast<data::data_expression>(result), x, R, sigma);
69 }
70
71 template <class T>
73 {
75 result,
76 x.name(),
77 [this, &x](data::data_expression_list& r) -> void
78 { atermpp::make_term_list<data::data_expression>(
79 r,
80 x.parameters().begin(),
81 x.parameters().end(),
82 [this](data::data_expression& r1, const data::data_expression& arg) -> void
83 { data_rewrite(r1, arg, R, sigma); } ) ;
84 });
85 }
86};
87
88template <typename Derived, typename DataRewriter, typename SubstitutionFunction>
89struct data_rewriter_builder: public add_data_rewriter<pbes_system::pbes_expression_builder, Derived, DataRewriter, SubstitutionFunction>
90{
92 using super::enter;
93 using super::leave;
94
95 data_rewriter_builder(const DataRewriter& R, SubstitutionFunction& sigma)
96 : super(R, sigma)
97 {}
98};
99
100template <template <class, class, class> class Builder, class DataRewriter, class SubstitutionFunction>
101struct 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 apply_rewriter_builder(const DataRewriter& datar, SubstitutionFunction& sigma)
108 : super(datar, sigma)
109 {}
110};
111
112template <template <class, class, class> class Builder, class DataRewriter, class SubstitutionFunction>
113apply_rewriter_builder<Builder, DataRewriter, SubstitutionFunction>
114make_apply_rewriter_builder(const DataRewriter& datar, SubstitutionFunction& sigma)
115{
117}
118
119} // namespace detail
120
122template <typename DataRewriter>
124{
127
128 const DataRewriter& R;
129
130 data_rewriter(const DataRewriter& R_)
131 : R(R_)
132 {}
133
135 {
137 pbes_expression result;
138 detail::make_apply_rewriter_builder<detail::data_rewriter_builder>(R, sigma).apply(result, x);
139 return result;
140 }
141
142 template <typename SubstitutionFunction>
143 pbes_expression operator()(const pbes_expression& x, SubstitutionFunction& sigma) const
144 {
145 pbes_expression result;
146 detail::make_apply_rewriter_builder<detail::data_rewriter_builder>(R, sigma).apply(result, x);
147 return result;
148 }
149};
150
151} // namespace pbes_system
152
153} // namespace mcrl2
154
155#endif // MCRL2_PBES_REWRITERS_DATA_REWRITER_H
\brief A data variable
Definition variable.h:28
\brief A propositional variable instantiation
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
const data::data_expression data_rewrite(const data::data_expression &x, const DataRewriter &R, SubstitutionFunction &sigma)
void make_propositional_variable_instantiation(atermpp::aterm_appl &t, const ARGUMENTS &... args)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
add your file description here.
add your file description here.
An empty struct that is used to denote the absence of a substitution. Used for rewriters.
A rewriter that applies a data rewriter to data expressions in a term.
pbes_expression operator()(const pbes_expression &x, SubstitutionFunction &sigma) const
pbes_expression operator()(const pbes_expression &x) const
data_rewriter(const DataRewriter &R_)
void apply(T &result, const data::data_expression &x)
add_data_rewriter(const DataRewriter &R_, SubstitutionFunction &sigma_)
void apply(T &result, const propositional_variable_instantiation &x)
apply_rewriter_builder(const DataRewriter &datar, SubstitutionFunction &sigma)
Builder< apply_rewriter_builder< Builder, DataRewriter, SubstitutionFunction >, DataRewriter, SubstitutionFunction > super
add_data_rewriter< pbes_system::pbes_expression_builder, Derived, DataRewriter, SubstitutionFunction > super
data_rewriter_builder(const DataRewriter &R, SubstitutionFunction &sigma)