Line data Source code
1 : // Author(s): Jeroen Keiren
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/data/function_update.h
10 : /// \brief The standard sort function_update.
11 : ///
12 : /// This file was generated from the data sort specification
13 : /// mcrl2/data/build/function_update.spec.
14 :
15 : #ifndef MCRL2_DATA_FUNCTION_UPDATE_H
16 : #define MCRL2_DATA_FUNCTION_UPDATE_H
17 :
18 : #include "functional" // std::function
19 : #include "mcrl2/utilities/exception.h"
20 : #include "mcrl2/data/basic_sort.h"
21 : #include "mcrl2/data/function_sort.h"
22 : #include "mcrl2/data/function_symbol.h"
23 : #include "mcrl2/data/application.h"
24 : #include "mcrl2/data/data_equation.h"
25 : #include "mcrl2/data/standard.h"
26 : #include "mcrl2/data/bool.h"
27 :
28 : namespace mcrl2 {
29 :
30 : namespace data {
31 :
32 : /// \brief Give all system defined constructors for function_update.
33 : /// \return All system defined constructors for function_update.
34 : inline
35 : function_symbol_vector function_update_generate_constructors_code()
36 : {
37 : function_symbol_vector result;
38 : return result;
39 : }
40 : /// \brief Give all defined constructors which can be used in mCRL2 specs for function_update.
41 : /// \return All system defined constructors that can be used in an mCRL2 specification for function_update.
42 : inline
43 : function_symbol_vector function_update_mCRL2_usable_constructors()
44 : {
45 : function_symbol_vector result;
46 : return result;
47 : }
48 : // The typedef is the sort that maps a function symbol to an function that rewrites it as well as a string of a function that can be used to implement it
49 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
50 : /// \brief Give all system defined constructors which have an implementation in C++ and not in rewrite rules for function_update.
51 : /// \return All system defined constructors that are to be implemented in C++ for function_update.
52 : inline
53 6992 : implementation_map function_update_cpp_implementable_constructors()
54 : {
55 6992 : implementation_map result;
56 6992 : return result;
57 : }
58 :
59 : /// \brief Generate identifier \@func_update.
60 : /// \return Identifier \@func_update.
61 : inline
62 136166 : const core::identifier_string& function_update_name()
63 : {
64 136166 : static core::identifier_string function_update_name = core::identifier_string("@func_update");
65 136166 : return function_update_name;
66 : }
67 :
68 : /// \brief Constructor for function symbol \@func_update.
69 : /// \param s A sort expression.
70 : /// \param t A sort expression.
71 : /// \return Function symbol function_update.
72 : inline
73 60662 : function_symbol function_update(const sort_expression& s, const sort_expression& t)
74 : {
75 121324 : function_symbol function_update(function_update_name(), make_function_sort_(make_function_sort_(s, t), s, t, make_function_sort_(s, t)));
76 60662 : return function_update;
77 : }
78 :
79 : /// \brief Recogniser for function \@func_update.
80 : /// \param e A data expression.
81 : /// \return true iff e is the function symbol matching \@func_update.
82 : inline
83 25036 : bool is_function_update_function_symbol(const atermpp::aterm_appl& e)
84 : {
85 25036 : if (is_function_symbol(e))
86 : {
87 23802 : return atermpp::down_cast<function_symbol>(e).name() == function_update_name();
88 : }
89 1234 : return false;
90 : }
91 :
92 : /// \brief Application of function symbol \@func_update.
93 : /// \param s A sort expression.
94 : /// \param t A sort expression.
95 : /// \param arg0 A data expression.
96 : /// \param arg1 A data expression.
97 : /// \param arg2 A data expression.
98 : /// \return Application of \@func_update to a number of arguments.
99 : inline
100 48944 : application function_update(const sort_expression& s, const sort_expression& t, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
101 : {
102 97888 : return function_update(s, t)(arg0, arg1, arg2);
103 : }
104 :
105 : /// \brief Make an application of function symbol \@func_update.
106 : /// \param result The data expression where the \@func_update expression is put.
107 : /// \param s A sort expression.
108 : /// \param t A sort expression.
109 : /// \param arg0 A data expression.
110 : /// \param arg1 A data expression.
111 : /// \param arg2 A data expression.
112 : inline
113 : void make_function_update(data_expression& result, const sort_expression& s, const sort_expression& t, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
114 : {
115 : make_application(result, function_update(s, t),arg0, arg1, arg2);
116 : }
117 :
118 : /// \brief Recogniser for application of \@func_update.
119 : /// \param e A data expression.
120 : /// \return true iff e is an application of function symbol function_update to a
121 : /// number of arguments.
122 : inline
123 25036 : bool is_function_update_application(const atermpp::aterm_appl& e)
124 : {
125 25036 : return is_application(e) && is_function_update_function_symbol(atermpp::down_cast<application>(e).head());
126 : }
127 :
128 : /// \brief Generate identifier \@func_update_stable.
129 : /// \return Identifier \@func_update_stable.
130 : inline
131 112344 : const core::identifier_string& function_update_stable_name()
132 : {
133 112344 : static core::identifier_string function_update_stable_name = core::identifier_string("@func_update_stable");
134 112344 : return function_update_stable_name;
135 : }
136 :
137 : /// \brief Constructor for function symbol \@func_update_stable.
138 : /// \param s A sort expression.
139 : /// \param t A sort expression.
140 : /// \return Function symbol function_update_stable.
141 : inline
142 88646 : function_symbol function_update_stable(const sort_expression& s, const sort_expression& t)
143 : {
144 177292 : function_symbol function_update_stable(function_update_stable_name(), make_function_sort_(make_function_sort_(s, t), s, t, make_function_sort_(s, t)));
145 88646 : return function_update_stable;
146 : }
147 :
148 : /// \brief Recogniser for function \@func_update_stable.
149 : /// \param e A data expression.
150 : /// \return true iff e is the function symbol matching \@func_update_stable.
151 : inline
152 24932 : bool is_function_update_stable_function_symbol(const atermpp::aterm_appl& e)
153 : {
154 24932 : if (is_function_symbol(e))
155 : {
156 23698 : return atermpp::down_cast<function_symbol>(e).name() == function_update_stable_name();
157 : }
158 1234 : return false;
159 : }
160 :
161 : /// \brief Application of function symbol \@func_update_stable.
162 : /// \param s A sort expression.
163 : /// \param t A sort expression.
164 : /// \param arg0 A data expression.
165 : /// \param arg1 A data expression.
166 : /// \param arg2 A data expression.
167 : /// \return Application of \@func_update_stable to a number of arguments.
168 : inline
169 76912 : application function_update_stable(const sort_expression& s, const sort_expression& t, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
170 : {
171 153824 : return function_update_stable(s, t)(arg0, arg1, arg2);
172 : }
173 :
174 : /// \brief Make an application of function symbol \@func_update_stable.
175 : /// \param result The data expression where the \@func_update_stable expression is put.
176 : /// \param s A sort expression.
177 : /// \param t A sort expression.
178 : /// \param arg0 A data expression.
179 : /// \param arg1 A data expression.
180 : /// \param arg2 A data expression.
181 : inline
182 : void make_function_update_stable(data_expression& result, const sort_expression& s, const sort_expression& t, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
183 : {
184 : make_application(result, function_update_stable(s, t),arg0, arg1, arg2);
185 : }
186 :
187 : /// \brief Recogniser for application of \@func_update_stable.
188 : /// \param e A data expression.
189 : /// \return true iff e is an application of function symbol function_update_stable to a
190 : /// number of arguments.
191 : inline
192 24932 : bool is_function_update_stable_application(const atermpp::aterm_appl& e)
193 : {
194 24932 : return is_application(e) && is_function_update_stable_function_symbol(atermpp::down_cast<application>(e).head());
195 : }
196 :
197 : /// \brief Generate identifier \@is_not_an_update.
198 : /// \return Identifier \@is_not_an_update.
199 : inline
200 25554 : const core::identifier_string& is_not_a_function_update_name()
201 : {
202 25554 : static core::identifier_string is_not_a_function_update_name = core::identifier_string("@is_not_an_update");
203 25554 : return is_not_a_function_update_name;
204 : }
205 :
206 : /// \brief Constructor for function symbol \@is_not_an_update.
207 : /// \param s A sort expression.
208 : /// \param t A sort expression.
209 : /// \return Function symbol is_not_a_function_update.
210 : inline
211 25554 : function_symbol is_not_a_function_update(const sort_expression& s, const sort_expression& t)
212 : {
213 51108 : function_symbol is_not_a_function_update(is_not_a_function_update_name(), make_function_sort_(make_function_sort_(s, t), sort_bool::bool_()));
214 25554 : return is_not_a_function_update;
215 : }
216 :
217 : /// \brief Recogniser for function \@is_not_an_update.
218 : /// \param e A data expression.
219 : /// \return true iff e is the function symbol matching \@is_not_an_update.
220 : inline
221 0 : bool is_is_not_a_function_update_function_symbol(const atermpp::aterm_appl& e)
222 : {
223 0 : if (is_function_symbol(e))
224 : {
225 0 : return atermpp::down_cast<function_symbol>(e).name() == is_not_a_function_update_name();
226 : }
227 0 : return false;
228 : }
229 :
230 : /// \brief Application of function symbol \@is_not_an_update.
231 : /// \param s A sort expression.
232 : /// \param t A sort expression.
233 : /// \param arg0 A data expression.
234 : /// \return Application of \@is_not_an_update to a number of arguments.
235 : inline
236 6992 : application is_not_a_function_update(const sort_expression& s, const sort_expression& t, const data_expression& arg0)
237 : {
238 13984 : return is_not_a_function_update(s, t)(arg0);
239 : }
240 :
241 : /// \brief Make an application of function symbol \@is_not_an_update.
242 : /// \param result The data expression where the \@is_not_an_update expression is put.
243 : /// \param s A sort expression.
244 : /// \param t A sort expression.
245 : /// \param arg0 A data expression.
246 : inline
247 : void make_is_not_a_function_update(data_expression& result, const sort_expression& s, const sort_expression& t, const data_expression& arg0)
248 : {
249 : make_application(result, is_not_a_function_update(s, t),arg0);
250 : }
251 :
252 : /// \brief Recogniser for application of \@is_not_an_update.
253 : /// \param e A data expression.
254 : /// \return true iff e is an application of function symbol is_not_a_function_update to a
255 : /// number of arguments.
256 : inline
257 0 : bool is_is_not_a_function_update_application(const atermpp::aterm_appl& e)
258 : {
259 0 : return is_application(e) && is_is_not_a_function_update_function_symbol(atermpp::down_cast<application>(e).head());
260 : }
261 :
262 : /// \brief The data expression of an application of the function symbol \@is_not_an_update.
263 : /// \details This function is to be implemented manually.
264 : /// \param arg0 A data expression.
265 : /// \return The data expression corresponding to an application of \@is_not_an_update to a number of arguments.
266 : inline
267 : data_expression is_not_a_function_update_manual_implementation(const data_expression& arg0);
268 :
269 :
270 : /// \brief Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
271 : inline
272 164 : data_expression is_not_a_function_update_application(const data_expression& a1)
273 : {
274 164 : assert(is_application(a1));
275 164 : const application& a=atermpp::down_cast<application>(a1);
276 : // assert(a.head()==is_not_a_function_update());
277 164 : return is_not_a_function_update_manual_implementation(a[0]);
278 : }
279 :
280 :
281 : /// \brief Generate identifier \@if_always_else.
282 : /// \return Identifier \@if_always_else.
283 : inline
284 39538 : const core::identifier_string& if_always_else_name()
285 : {
286 39538 : static core::identifier_string if_always_else_name = core::identifier_string("@if_always_else");
287 39538 : return if_always_else_name;
288 : }
289 :
290 : /// \brief Constructor for function symbol \@if_always_else.
291 : /// \param s A sort expression.
292 : /// \param t A sort expression.
293 : /// \return Function symbol if_always_else.
294 : inline
295 39538 : function_symbol if_always_else(const sort_expression& s, const sort_expression& t)
296 : {
297 79076 : function_symbol if_always_else(if_always_else_name(), make_function_sort_(sort_bool::bool_(), make_function_sort_(s, t), make_function_sort_(s, t), make_function_sort_(s, t)));
298 39538 : return if_always_else;
299 : }
300 :
301 : /// \brief Recogniser for function \@if_always_else.
302 : /// \param e A data expression.
303 : /// \return true iff e is the function symbol matching \@if_always_else.
304 : inline
305 0 : bool is_if_always_else_function_symbol(const atermpp::aterm_appl& e)
306 : {
307 0 : if (is_function_symbol(e))
308 : {
309 0 : return atermpp::down_cast<function_symbol>(e).name() == if_always_else_name();
310 : }
311 0 : return false;
312 : }
313 :
314 : /// \brief Application of function symbol \@if_always_else.
315 : /// \param s A sort expression.
316 : /// \param t A sort expression.
317 : /// \param arg0 A data expression.
318 : /// \param arg1 A data expression.
319 : /// \param arg2 A data expression.
320 : /// \return Application of \@if_always_else to a number of arguments.
321 : inline
322 20976 : application if_always_else(const sort_expression& s, const sort_expression& t, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
323 : {
324 41952 : return if_always_else(s, t)(arg0, arg1, arg2);
325 : }
326 :
327 : /// \brief Make an application of function symbol \@if_always_else.
328 : /// \param result The data expression where the \@if_always_else expression is put.
329 : /// \param s A sort expression.
330 : /// \param t A sort expression.
331 : /// \param arg0 A data expression.
332 : /// \param arg1 A data expression.
333 : /// \param arg2 A data expression.
334 : inline
335 : void make_if_always_else(data_expression& result, const sort_expression& s, const sort_expression& t, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
336 : {
337 : make_application(result, if_always_else(s, t),arg0, arg1, arg2);
338 : }
339 :
340 : /// \brief Recogniser for application of \@if_always_else.
341 : /// \param e A data expression.
342 : /// \return true iff e is an application of function symbol if_always_else to a
343 : /// number of arguments.
344 : inline
345 0 : bool is_if_always_else_application(const atermpp::aterm_appl& e)
346 : {
347 0 : return is_application(e) && is_if_always_else_function_symbol(atermpp::down_cast<application>(e).head());
348 : }
349 :
350 : /// \brief The data expression of an application of the function symbol \@if_always_else.
351 : /// \details This function is to be implemented manually.
352 : /// \param arg0 A data expression.
353 : /// \param arg1 A data expression.
354 : /// \param arg2 A data expression.
355 : /// \return The data expression corresponding to an application of \@if_always_else to a number of arguments.
356 : inline
357 : data_expression if_always_else_manual_implementation(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2);
358 :
359 :
360 : /// \brief Application of a function that is user defined instead of by rewrite rules. It does not have sort parameters.
361 : inline
362 156 : data_expression if_always_else_application(const data_expression& a1)
363 : {
364 156 : assert(is_application(a1));
365 156 : const application& a=atermpp::down_cast<application>(a1);
366 : // assert(a.head()==if_always_else());
367 156 : return if_always_else_manual_implementation(a[0], a[1], a[2]);
368 : }
369 :
370 : /// \brief Give all system defined mappings for function_update
371 : /// \param s A sort expression
372 : /// \param t A sort expression
373 : /// \return All system defined mappings for function_update
374 : inline
375 6992 : function_symbol_vector function_update_generate_functions_code(const sort_expression& s, const sort_expression& t)
376 : {
377 6992 : function_symbol_vector result;
378 6992 : result.push_back(function_update(s, t));
379 6992 : result.push_back(function_update_stable(s, t));
380 6992 : result.push_back(is_not_a_function_update(s, t));
381 6992 : result.push_back(if_always_else(s, t));
382 6992 : return result;
383 0 : }
384 :
385 : /// \brief Give all system defined mappings and constructors for function_update
386 : /// \param s A sort expression
387 : /// \param t A sort expression
388 : /// \return All system defined mappings for function_update
389 : inline
390 : function_symbol_vector function_update_generate_constructors_and_functions_code(const sort_expression& s, const sort_expression& t)
391 : {
392 : function_symbol_vector result=function_update_generate_functions_code(s, t);
393 : for(const function_symbol& f: function_update_generate_constructors_code())
394 : {
395 : result.push_back(f);
396 : }
397 : return result;
398 : }
399 :
400 : /// \brief Give all system defined mappings that can be used in mCRL2 specs for function_update
401 : /// \param s A sort expression
402 : /// \param t A sort expression
403 : /// \return All system defined mappings for that can be used in mCRL2 specificationis function_update
404 : inline
405 4578 : function_symbol_vector function_update_mCRL2_usable_mappings(const sort_expression& s, const sort_expression& t)
406 : {
407 4578 : function_symbol_vector result;
408 4578 : result.push_back(function_update(s, t));
409 4578 : result.push_back(function_update_stable(s, t));
410 4578 : result.push_back(is_not_a_function_update(s, t));
411 4578 : result.push_back(if_always_else(s, t));
412 4578 : return result;
413 0 : }
414 :
415 :
416 : // The typedef is the sort that maps a function symbol to an function that rewrites it as well as a string of a function that can be used to implement it
417 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
418 : /// \brief Give all system defined mappings that are to be implemented in C++ code for function_update
419 : /// \param s A sort expression
420 : /// \param t A sort expression
421 : /// \return A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for function_update
422 : inline
423 6992 : implementation_map function_update_cpp_implementable_mappings(const sort_expression& s, const sort_expression& t)
424 : {
425 6992 : implementation_map result;
426 6992 : result[is_not_a_function_update(s, t)]=std::pair<std::function<data_expression(const data_expression&)>, std::string>(is_not_a_function_update_application,"is_not_a_function_update_manual_implementation");
427 6992 : result[if_always_else(s, t)]=std::pair<std::function<data_expression(const data_expression&)>, std::string>(if_always_else_application,"if_always_else_manual_implementation");
428 6992 : return result;
429 0 : }
430 : ///\brief Function for projecting out argument.
431 : /// arg1 from an application.
432 : /// \param e A data expression.
433 : /// \pre arg1 is defined for e.
434 : /// \return The argument of e that corresponds to arg1.
435 : inline
436 92 : const data_expression& arg1(const data_expression& e)
437 : {
438 92 : assert(is_function_update_application(e) || is_function_update_stable_application(e) || is_is_not_a_function_update_application(e) || is_if_always_else_application(e));
439 92 : return atermpp::down_cast<application>(e)[0];
440 : }
441 :
442 : ///\brief Function for projecting out argument.
443 : /// arg2 from an application.
444 : /// \param e A data expression.
445 : /// \pre arg2 is defined for e.
446 : /// \return The argument of e that corresponds to arg2.
447 : inline
448 92 : const data_expression& arg2(const data_expression& e)
449 : {
450 92 : assert(is_function_update_application(e) || is_function_update_stable_application(e) || is_if_always_else_application(e));
451 92 : return atermpp::down_cast<application>(e)[1];
452 : }
453 :
454 : ///\brief Function for projecting out argument.
455 : /// arg3 from an application.
456 : /// \param e A data expression.
457 : /// \pre arg3 is defined for e.
458 : /// \return The argument of e that corresponds to arg3.
459 : inline
460 92 : const data_expression& arg3(const data_expression& e)
461 : {
462 92 : assert(is_function_update_application(e) || is_function_update_stable_application(e) || is_if_always_else_application(e));
463 92 : return atermpp::down_cast<application>(e)[2];
464 : }
465 :
466 : /// \brief Give all system defined equations for function_update
467 : /// \param s A sort expression
468 : /// \param t A sort expression
469 : /// \return All system defined equations for sort function_update
470 : inline
471 6992 : data_equation_vector function_update_generate_equations_code(const sort_expression& s, const sort_expression& t)
472 : {
473 13984 : variable vx("x",s);
474 13984 : variable vy("y",s);
475 13984 : variable vv("v",t);
476 13984 : variable vw("w",t);
477 13984 : variable vf("f",make_function_sort_(s, t));
478 :
479 6992 : data_equation_vector result;
480 27968 : result.push_back(data_equation(variable_list({vf, vv, vx}), is_not_a_function_update(s, t, vf), function_update(s, t, vf, vx, vv), if_always_else(s, t, equal_to(vf(vx), vv), vf, function_update_stable(s, t, vf, vx, vv))));
481 34960 : result.push_back(data_equation(variable_list({vf, vv, vw, vx}), function_update(s, t, function_update_stable(s, t, vf, vx, vw), vx, vv), if_always_else(s, t, equal_to(vf(vx), vv), vf, function_update_stable(s, t, vf, vx, vv))));
482 41952 : result.push_back(data_equation(variable_list({vf, vv, vw, vx, vy}), less(vy, vx), function_update(s, t, function_update_stable(s, t, vf, vy, vw), vx, vv), function_update_stable(s, t, function_update(s, t, vf, vx, vv), vy, vw)));
483 41952 : result.push_back(data_equation(variable_list({vf, vv, vw, vx, vy}), less(vx, vy), function_update(s, t, function_update_stable(s, t, vf, vy, vw), vx, vv), if_always_else(s, t, equal_to(vf(vx), vv), function_update_stable(s, t, vf, vy, vw), function_update_stable(s, t, function_update_stable(s, t, vf, vy, vw), vx, vv))));
484 34960 : result.push_back(data_equation(variable_list({vf, vv, vx, vy}), not_equal_to(vx, vy), function_update_stable(s, t, vf, vx, vv)(vy), vf(vy)));
485 27968 : result.push_back(data_equation(variable_list({vf, vv, vx}), function_update_stable(s, t, vf, vx, vv)(vx), vv));
486 34960 : result.push_back(data_equation(variable_list({vf, vv, vx, vy}), not_equal_to(vx, vy), function_update(s, t, vf, vx, vv)(vy), vf(vy)));
487 27968 : result.push_back(data_equation(variable_list({vf, vv, vx}), function_update(s, t, vf, vx, vv)(vx), vv));
488 13984 : return result;
489 6992 : }
490 :
491 : } // namespace data
492 :
493 : } // namespace mcrl2
494 :
495 : #include "mcrl2/data/detail/function_update.h" // This file contains the manual implementations of rewrite functions.
496 : #endif // MCRL2_DATA_FUNCTION_UPDATE_H
|
