mCRL2
Loading...
Searching...
No Matches
function_update.h
Go to the documentation of this file.
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//
14
15#ifndef MCRL2_DATA_FUNCTION_UPDATE_H
16#define MCRL2_DATA_FUNCTION_UPDATE_H
17
18#include "functional" // std::function
25#include "mcrl2/data/standard.h"
26#include "mcrl2/data/bool.h"
27
28namespace mcrl2 {
29
30 namespace data {
31
34 inline
36 {
38 return result;
39 }
42 inline
44 {
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;
52 inline
54 {
55 implementation_map result;
56 return result;
57 }
58
61 inline
63 {
66 }
67
72 inline
74 {
76 return function_update;
77 }
78
82 inline
84 {
85 if (is_function_symbol(e))
86 {
87 return atermpp::down_cast<function_symbol>(e).name() == function_update_name();
88 }
89 return false;
90 }
91
99 inline
101 {
102 return function_update(s, t)(arg0, arg1, arg2);
103 }
104
112 inline
114 {
115 make_application(result, function_update(s, t),arg0, arg1, arg2);
116 }
117
122 inline
124 {
125 return is_application(e) && is_function_update_function_symbol(atermpp::down_cast<application>(e).head());
126 }
127
130 inline
132 {
135 }
136
141 inline
143 {
146 }
147
151 inline
153 {
154 if (is_function_symbol(e))
155 {
156 return atermpp::down_cast<function_symbol>(e).name() == function_update_stable_name();
157 }
158 return false;
159 }
160
168 inline
170 {
171 return function_update_stable(s, t)(arg0, arg1, arg2);
172 }
173
181 inline
183 {
184 make_application(result, function_update_stable(s, t),arg0, arg1, arg2);
185 }
186
191 inline
193 {
194 return is_application(e) && is_function_update_stable_function_symbol(atermpp::down_cast<application>(e).head());
195 }
196
199 inline
201 {
204 }
205
210 inline
212 {
215 }
216
220 inline
222 {
223 if (is_function_symbol(e))
224 {
225 return atermpp::down_cast<function_symbol>(e).name() == is_not_a_function_update_name();
226 }
227 return false;
228 }
229
235 inline
237 {
238 return is_not_a_function_update(s, t)(arg0);
239 }
240
246 inline
248 {
249 make_application(result, is_not_a_function_update(s, t),arg0);
250 }
251
256 inline
258 {
259 return is_application(e) && is_is_not_a_function_update_function_symbol(atermpp::down_cast<application>(e).head());
260 }
261
266 inline
267 data_expression is_not_a_function_update_manual_implementation(const data_expression& arg0);
268
269
271 inline
273 {
274 assert(is_application(a1));
275 const application& a=atermpp::down_cast<application>(a1);
276 // assert(a.head()==is_not_a_function_update());
278 }
279
280
283 inline
285 {
287 return if_always_else_name;
288 }
289
294 inline
296 {
298 return if_always_else;
299 }
300
304 inline
306 {
307 if (is_function_symbol(e))
308 {
309 return atermpp::down_cast<function_symbol>(e).name() == if_always_else_name();
310 }
311 return false;
312 }
313
321 inline
323 {
324 return if_always_else(s, t)(arg0, arg1, arg2);
325 }
326
334 inline
336 {
337 make_application(result, if_always_else(s, t),arg0, arg1, arg2);
338 }
339
344 inline
346 {
347 return is_application(e) && is_if_always_else_function_symbol(atermpp::down_cast<application>(e).head());
348 }
349
356 inline
357 data_expression if_always_else_manual_implementation(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2);
358
359
361 inline
363 {
364 assert(is_application(a1));
365 const application& a=atermpp::down_cast<application>(a1);
366 // assert(a.head()==if_always_else());
367 return if_always_else_manual_implementation(a[0], a[1], a[2]);
368 }
369
374 inline
376 {
378 result.push_back(function_update(s, t));
379 result.push_back(function_update_stable(s, t));
380 result.push_back(is_not_a_function_update(s, t));
381 result.push_back(if_always_else(s, t));
382 return result;
383 }
384
389 inline
391 {
394 {
395 result.push_back(f);
396 }
397 return result;
398 }
399
404 inline
406 {
408 result.push_back(function_update(s, t));
409 result.push_back(function_update_stable(s, t));
410 result.push_back(is_not_a_function_update(s, t));
411 result.push_back(if_always_else(s, t));
412 return result;
413 }
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;
422 inline
424 {
425 implementation_map result;
426 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 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 return result;
429 }
435 inline
437 {
439 return atermpp::down_cast<application>(e)[0];
440 }
441
447 inline
449 {
451 return atermpp::down_cast<application>(e)[1];
452 }
453
459 inline
461 {
463 return atermpp::down_cast<application>(e)[2];
464 }
465
470 inline
472 {
473 variable vx("x",s);
474 variable vy("y",s);
475 variable vv("v",t);
476 variable vw("w",t);
477 variable vf("f",make_function_sort_(s, t));
478
480 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 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 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 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 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 result.push_back(data_equation(variable_list({vf, vv, vx}), function_update_stable(s, t, vf, vx, vv)(vx), vv));
486 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 result.push_back(data_equation(variable_list({vf, vv, vx}), function_update(s, t, vf, vx, vv)(vx), vv));
488 return result;
489 }
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
The class application.
The class basic_sort.
The standard sort bool_.
Term containing a string.
An application of a data expression to a number of arguments.
\brief A data equation
\brief A function symbol
\brief A sort expression
\brief A data variable
Definition variable.h:28
The class function symbol.
The class data_equation.
This files contains the implementation of the function "is_not_a_function_update" which was declared ...
Exception classes for use in libraries and tools.
The class function_sort.
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
bool is_is_not_a_function_update_application(const atermpp::aterm_appl &e)
Recogniser for application of @is_not_an_update.
function_symbol_vector function_update_mCRL2_usable_mappings(const sort_expression &s, const sort_expression &t)
Give all system defined mappings that can be used in mCRL2 specs for function_update.
bool is_if_always_else_function_symbol(const atermpp::aterm_appl &e)
Recogniser for function @if_always_else.
data_expression is_not_a_function_update_manual_implementation(const data_expression &f)
The data expression of an application of the function symbol @is_not_an_update.
bool is_is_not_a_function_update_function_symbol(const atermpp::aterm_appl &e)
Recogniser for function @is_not_an_update.
function_symbol not_equal_to(const sort_expression &s)
Constructor for function symbol !=.
Definition standard.h:163
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
function_symbol_vector function_update_mCRL2_usable_constructors()
Give all defined constructors which can be used in mCRL2 specs for function_update.
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)
Make an application of function symbol @func_update_stable.
implementation_map function_update_cpp_implementable_mappings(const sort_expression &s, const sort_expression &t)
Give all system defined mappings that are to be implemented in C++ code for function_update.
bool is_function_update_application(const atermpp::aterm_appl &e)
Recogniser for application of @func_update.
function_symbol if_always_else(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @if_always_else.
function_symbol less(const sort_expression &s)
Constructor for function symbol <.
Definition standard.h:240
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)
Make an application of function symbol @func_update.
const core::identifier_string & function_update_name()
Generate identifier @func_update.
function_symbol_vector function_update_generate_constructors_and_functions_code(const sort_expression &s, const sort_expression &t)
Give all system defined mappings and constructors for function_update.
std::map< function_symbol, std::pair< std::function< data_expression(const data_expression &)>, std::string > > implementation_map
bool is_function_symbol(const atermpp::aterm_appl &x)
Returns true if the term t is a function symbol.
data_expression if_always_else_application(const data_expression &a1)
Application of a function that is user defined instead of by rewrite rules. It does not have sort par...
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
function_symbol_vector function_update_generate_constructors_code()
Give all system defined constructors for function_update.
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &codomain)
Convenience constructor for function sort with domain size 1.
const core::identifier_string & if_always_else_name()
Generate identifier @if_always_else.
bool is_function_update_stable_function_symbol(const atermpp::aterm_appl &e)
Recogniser for function @func_update_stable.
const core::identifier_string & is_not_a_function_update_name()
Generate identifier @is_not_an_update.
bool is_application(const atermpp::aterm_appl &x)
Returns true if the term t is an application.
data_expression if_always_else_manual_implementation(const data_expression &b, const data_expression &e1, const data_expression &e2)
The data expression of an application of the function symbol @if_always_else.
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)
Make an application of function symbol @if_always_else.
bool is_if_always_else_application(const atermpp::aterm_appl &e)
Recogniser for application of @if_always_else.
bool is_function_update_stable_application(const atermpp::aterm_appl &e)
Recogniser for application of @func_update_stable.
data_equation_vector function_update_generate_equations_code(const sort_expression &s, const sort_expression &t)
Give all system defined equations for function_update.
bool is_function_update_function_symbol(const atermpp::aterm_appl &e)
Recogniser for function @func_update.
atermpp::term_list< variable > variable_list
\brief list of variables
implementation_map function_update_cpp_implementable_constructors()
Give all system defined constructors which have an implementation in C++ and not in rewrite rules for...
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
data_expression is_not_a_function_update_application(const data_expression &a1)
Application of a function that is user defined instead of by rewrite rules. It does not have sort par...
function_symbol function_update_stable(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @func_update_stable.
void make_is_not_a_function_update(data_expression &result, const sort_expression &s, const sort_expression &t, const data_expression &arg0)
Make an application of function symbol @is_not_an_update.
function_symbol_vector function_update_generate_functions_code(const sort_expression &s, const sort_expression &t)
Give all system defined mappings for function_update.
function_symbol function_update(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @func_update.
const core::identifier_string & function_update_stable_name()
Generate identifier @func_update_stable.
const data_expression & arg3(const data_expression &e)
Function for projecting out argument. arg3 from an application.
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
function_symbol is_not_a_function_update(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @is_not_an_update.
void make_application(atermpp::aterm &result)
Make function for an application.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Standard functions that are available for all sorts.