mCRL2
Loading...
Searching...
No Matches
rewrite.h
Go to the documentation of this file.
1// Author(s): Muck van Weerdenburg
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//
10
11#ifndef MCRL2_DATA_DETAIL_REWRITE_H
12#define MCRL2_DATA_DETAIL_REWRITE_H
13
18
19namespace mcrl2
20{
21namespace data
22{
23namespace detail
24{
25
42{
43 protected:
45
48 Rewriter& operator=(const Rewriter& other) = default;
49
52 Rewriter(const Rewriter& other) = default;
53
54 public:
56
63 Rewriter(const data_specification& data_spec, const used_data_equation_selector& eq_selector):
64 data_equation_selector(eq_selector),
66 {
67 }
68
70 virtual ~Rewriter()
71 {
72 }
73
76 {
77 return m_generator;
78 }
79
85
92
98 virtual void rewrite(data_expression& result, const data_expression& term, substitution_type& sigma) = 0;
99
106 {
107 return rewrite(term,sigma);
108 }
109
114 virtual std::shared_ptr<detail::Rewriter> clone() = 0;
115
116 public:
117 /* The functions below are public, because they are used in the compiling jitty rewriter */
119 data_expression& result,
120 const abstraction& t,
123 data_expression& result,
124 const variable_list& vl,
125 const data_expression& t1,
126 const bool t1_is_normal_form,
128
130 data_expression& result,
131 const abstraction& t,
134 data_expression& result,
135 const variable_list& vl,
136 const data_expression& t1,
137 const bool t1_is_normal_form,
139
140 /* The functions below exist temporarily in the transformation of the jittyc rewriter to a rewrite_stack */
141 /* They ought to be removed. */
142 data_expression existential_quantifier_enumeration( // TODO: THIS SHOULD BE REMOVED IN DUE TIME.
143 const abstraction& t,
145 {
146 data_expression result;
148 return result;
149 }
150 data_expression existential_quantifier_enumeration( // TODO: THIS SHOULD BE REMOVED IN DUE TIME.
151 const variable_list& vl,
152 const data_expression& t1,
153 const bool t1_is_normal_form,
155 {
156 data_expression result;
157 existential_quantifier_enumeration(result, vl, t1, t1_is_normal_form, sigma);
158 return result;
159 }
160
161 data_expression universal_quantifier_enumeration( // TODO: THIS SHOULD BE REMOVED IN DUE TIME.
162 const abstraction& t,
164 {
165 data_expression result;
167 return result;
168 }
169
170 data_expression universal_quantifier_enumeration( // TODO: THIS SHOULD BE REMOVED IN DUE TIME.
171 const variable_list& vl,
172 const data_expression& t1,
173 const bool t1_is_normal_form,
175 {
176 data_expression result;
177 universal_quantifier_enumeration(result, vl, t1, t1_is_normal_form, sigma);
178 return result;
179 }
180
181 // Rewrite a where expression where the subdataexpressions are in internal format.
182 // It yields a term without a where expression. The result is passed back in the variable result.
183 void rewrite_where(data_expression& result,
184 const where_clause& term,
186
187 data_expression rewrite_where(const where_clause& term, // TODO: THIS SHOULD BE REMOVED IN DUE TIME.
189
190 // Rewrite an expression with a lambda as outermost symbol. The expression is in internal format.
191 // Bound variables are replaced by new variables to avoid a clash with variables in the right hand sides
192 // of sigma.
193
195 data_expression& result,
196 const variable_list& vl,
197 const data_expression& body,
198 const bool body_in_normal_form,
200
201 data_expression rewrite_single_lambda( // TODO: THIS SHOULD BE REMOVED IN DUE TIME.
202 const variable_list& vl,
203 const data_expression& body,
204 const bool body_in_normal_form,
206 {
207 data_expression result;
208 rewrite_single_lambda(result, vl, body, body_in_normal_form, sigma);
209 return result;
210 }
211
214 data_expression& result,
215 const data_expression& t,
217
219 data_expression& result,
220 const abstraction& lambda_term,
221 const application& t,
223
224 virtual void thread_initialise()
225 {
226 }
227
228 protected:
229
231
233 data_expression& result,
234 const variable_list& vl,
235 const data_expression& t1,
236 const bool t1_is_normal_form,
238 const binder_type& binder,
239 data_expression (*lazy_op)(const data_expression&, const data_expression&),
240 const data_expression& identity_element,
241 const data_expression& absorbing_element);
242
243};
244
252std::shared_ptr<detail::Rewriter> createRewriter(
253 const data_specification& DataSpec,
254 const used_data_equation_selector& equations_selector,
255 const rewrite_strategy Strategy = jitty);
256
262void CheckRewriteRule(const data_equation& data_eqn);
263
269bool isValidRewriteRule(const data_equation& data_eqn);
270
271
272// This function calculates the cumulated length of all
273// potential function arguments.
274inline std::size_t getArity(const data::function_symbol& op)
275{
276 sort_expression sort = op.sort();
277 std::size_t arity = 0;
278
279 while (is_function_sort(sort))
280 {
281 const function_sort fsort(sort);
282 const sort_expression_list& sort_dom = fsort.domain();
283 arity += sort_dom.size();
284 sort = fsort.codomain();
285 }
286 return arity;
287}
288
289// This function calculates the number of direct function arguments.
290inline std::size_t get_direct_arity(const data::function_symbol& op)
291{
292 sort_expression sort = op.sort();
293 if (is_function_sort(sort))
294 {
295 return atermpp::down_cast<function_sort>(sort).domain().size();
296 }
297 return 0;
298}
299
300} // namespace detail
301} // namespace data
302} // namespace mcrl2
303
304#endif
size_type size() const
Returns the number of arguments of this term.
Definition aterm.h:151
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:256
An abstraction expression.
Definition abstraction.h:26
An application of a data expression to a number of arguments.
\brief A data equation
Rewriter interface class.
Definition rewrite.h:42
used_data_equation_selector data_equation_selector
Definition rewrite.h:57
mcrl2::data::data_specification m_data_specification_for_enumeration
Definition rewrite.h:230
virtual std::shared_ptr< detail::Rewriter > clone()=0
Clone a rewriter.
data_expression universal_quantifier_enumeration(const abstraction &t, substitution_type &sigma)
Definition rewrite.h:161
void rewrite_lambda_application(data_expression &result, const data_expression &t, substitution_type &sigma)
Rewrite t, assuming that the headsymbol of t, which can be nested, is a lambda term.
Definition rewrite.cpp:214
void rewrite_where(data_expression &result, const where_clause &term, substitution_type &sigma)
Definition rewrite.cpp:70
void existential_quantifier_enumeration(data_expression &result, const abstraction &t, substitution_type &sigma)
Definition rewrite.cpp:325
virtual void rewrite(data_expression &result, const data_expression &term, substitution_type &sigma)=0
Rewrite an mCRL2 data term.
data_expression operator()(const data_expression &term, substitution_type &sigma)
Provide the rewriter with a () operator, such that it can also rewrite terms using this operator.
Definition rewrite.h:105
data_expression existential_quantifier_enumeration(const abstraction &t, substitution_type &sigma)
Definition rewrite.h:142
void universal_quantifier_enumeration(data_expression &result, const abstraction &t, substitution_type &sigma)
Definition rewrite.cpp:353
data_expression universal_quantifier_enumeration(const variable_list &vl, const data_expression &t1, const bool t1_is_normal_form, substitution_type &sigma)
Definition rewrite.h:170
Rewriter(const Rewriter &other)=default
The copy constructor operator is protected. Public copying is not allowed.
virtual rewrite_strategy getStrategy()=0
Get rewriter strategy that is used.
mutable_indexed_substitution substitution_type
Definition rewrite.h:55
virtual data_expression rewrite(const data_expression &term, substitution_type &sigma)=0
Rewrite an mCRL2 data term.
data_expression existential_quantifier_enumeration(const variable_list &vl, const data_expression &t1, const bool t1_is_normal_form, substitution_type &sigma)
Definition rewrite.h:150
data_expression rewrite_single_lambda(const variable_list &vl, const data_expression &body, const bool body_in_normal_form, substitution_type &sigma)
Definition rewrite.h:201
virtual ~Rewriter()
Destructor.
Definition rewrite.h:70
data::enumerator_identifier_generator & identifier_generator()
The fresh name generator of the rewriter.
Definition rewrite.h:75
void rewrite_single_lambda(data_expression &result, const variable_list &vl, const data_expression &body, const bool body_in_normal_form, substitution_type &sigma)
Definition rewrite.cpp:109
virtual void thread_initialise()
Definition rewrite.h:224
Rewriter(const data_specification &data_spec, const used_data_equation_selector &eq_selector)
Constructor. Do not use directly; use createRewriter() function instead.
Definition rewrite.h:63
Rewriter & operator=(const Rewriter &other)=default
The copy assignment operator is protected. Public copying is not allowed.
enumerator_identifier_generator m_generator
Definition rewrite.h:44
void quantifier_enumeration(data_expression &result, const variable_list &vl, const data_expression &t1, const bool t1_is_normal_form, substitution_type &sigma, const binder_type &binder, data_expression(*lazy_op)(const data_expression &, const data_expression &), const data_expression &identity_element, const data_expression &absorbing_element)
Definition rewrite.cpp:377
\brief A function sort
const sort_expression & codomain() const
const sort_expression_list & domain() const
\brief A function symbol
const sort_expression & sort() const
\brief A sort expression
Component for selecting a subset of equations that are actually used in an encompassing specification...
Definition selection.h:37
\brief A where expression
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
add your file description here.
void CheckRewriteRule(const data_equation &data_eqn)
Check that an mCRL2 data equation is a valid rewrite rule. If not, an runtime_error is thrown indicat...
Definition rewrite.cpp:588
bool isValidRewriteRule(const data_equation &data_eqn)
Check whether or not an mCRL2 data equation is a valid rewrite rule.
Definition rewrite.cpp:646
std::shared_ptr< detail::Rewriter > createRewriter(const data_specification &DataSpec, const used_data_equation_selector &equations_selector, const rewrite_strategy Strategy=jitty)
Create a rewriter.
Definition rewrite.cpp:504
std::size_t getArity(const data::function_symbol &op)
Definition rewrite.h:274
std::size_t get_direct_arity(const data::function_symbol &op)
Definition rewrite.h:290
rewrite_strategy
The strategy of the rewriter.
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Provides selection utility functionality.