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/standard.h
10 : /// \brief Standard functions that are available for all sorts.
11 :
12 : #ifndef MCRL2_DATA_STANDARD_H
13 : #define MCRL2_DATA_STANDARD_H
14 :
15 : #include "mcrl2/core/detail/construction_utility.h"
16 : #include "mcrl2/data/abstraction.h"
17 : #include "mcrl2/data/data_equation.h"
18 :
19 :
20 : namespace mcrl2
21 : {
22 :
23 : namespace data
24 : {
25 :
26 : // predeclare
27 : namespace sort_bool
28 : {
29 : const basic_sort& bool_();
30 : const function_symbol& false_();
31 : const function_symbol& true_();
32 : application and_(const data_expression&,const data_expression&);
33 : application not_(const data_expression&);
34 : bool is_bool(const sort_expression&);
35 : } // namespace sort_bool
36 :
37 : /// \cond INTERNAL_DOCS
38 : namespace detail
39 : {
40 :
41 : /// \ Component to facilitate code generation
42 : template < typename Derived >
43 : struct symbol : public core::detail::singleton_identifier< Derived >
44 : {
45 893073 : static bool is_symbol(const core::identifier_string& e)
46 : {
47 893073 : return e == core::detail::singleton_identifier< Derived >::instance();
48 : }
49 :
50 1969 : static bool is_application(const data_expression& e)
51 : {
52 1969 : return data::is_application(e) ? is_application(atermpp::down_cast<application>(e)) : false;
53 : }
54 :
55 523449 : static bool is_application(const application& e)
56 : {
57 523449 : return is_function_symbol(e.head());
58 : }
59 :
60 523449 : static bool is_function_symbol(const data_expression& e)
61 : {
62 523449 : return data::is_function_symbol(e) ? is_function_symbol(atermpp::down_cast<function_symbol>(e)) : false;
63 : }
64 :
65 515209 : static bool is_function_symbol(const function_symbol& e)
66 : {
67 515209 : return is_symbol(e.name());
68 : }
69 : };
70 :
71 : struct equal_symbol : public symbol< equal_symbol >
72 : {
73 110 : static char const* initialise()
74 : {
75 110 : return "==";
76 : }
77 : };
78 : struct not_equal_symbol : public symbol< not_equal_symbol >
79 : {
80 110 : static char const* initialise()
81 : {
82 110 : return "!=";
83 : }
84 : };
85 : struct if_symbol : public symbol< if_symbol >
86 : {
87 109 : static char const* initialise()
88 : {
89 109 : return "if";
90 : }
91 : };
92 : struct less_symbol : public symbol< less_symbol >
93 : {
94 109 : static char const* initialise()
95 : {
96 109 : return "<";
97 : }
98 : };
99 : struct less_equal_symbol : public symbol< less_equal_symbol >
100 : {
101 109 : static char const* initialise()
102 : {
103 109 : return "<=";
104 : }
105 : };
106 : struct greater_symbol : public symbol< greater_symbol >
107 : {
108 109 : static char const* initialise()
109 : {
110 109 : return ">";
111 : }
112 : };
113 : struct greater_equal_symbol : public symbol< greater_equal_symbol >
114 : {
115 109 : static char const* initialise()
116 : {
117 109 : return ">=";
118 : }
119 : };
120 : } // namespace detail
121 : /// \endcond
122 :
123 : /// \brief Constructor for function symbol ==
124 : /// \param[in] s A sort expression
125 : /// \return function symbol equal_to
126 600762 : inline function_symbol equal_to(const sort_expression& s)
127 : {
128 1201524 : return function_symbol(detail::equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
129 : }
130 :
131 : /// \brief Recogniser for function ==
132 : /// \param[in] e A data expression
133 : /// \return true iff e is the function symbol matching ==
134 : template < typename DataExpression >
135 : inline bool is_equal_to_function_symbol(const DataExpression& e)
136 : {
137 : return detail::equal_symbol::is_function_symbol(e);
138 : }
139 :
140 : /// \brief Application of function symbol ==
141 : /// \param[in] arg0 A data expression
142 : /// \param[in] arg1 A data expression
143 : /// \return Application of == to a number of arguments
144 524238 : inline application equal_to(const data_expression& arg0, const data_expression& arg1)
145 : {
146 524238 : assert(arg0.sort() == arg1.sort());
147 1048476 : return equal_to(arg0.sort())(arg0, arg1);
148 : }
149 :
150 : /// \brief Recogniser for application of ==
151 : /// \param[in] e A data expression
152 : /// \return true iff e is an application of function symbol equal_to to a
153 : /// number of arguments
154 : template < typename DataExpression >
155 163292 : inline bool is_equal_to_application(const DataExpression& e)
156 : {
157 163292 : return detail::equal_symbol::is_application(e);
158 : }
159 :
160 : /// \brief Constructor for function symbol !=
161 : /// \param[in] s A sort expression
162 : /// \return function symbol not_equal_to
163 194554 : inline function_symbol not_equal_to(const sort_expression& s)
164 : {
165 389108 : return function_symbol(detail::not_equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
166 : }
167 :
168 : /// \brief Recogniser for function !=
169 : /// \param[in] e A data expression
170 : /// \return true iff e is the function symbol matching !=
171 : template < typename DataExpression >
172 : inline bool is_not_equal_to_function_symbol(const DataExpression& e)
173 : {
174 : return detail::not_equal_symbol::is_function_symbol(e);
175 : }
176 :
177 : /// \brief Application of function symbol !=
178 : /// \param[in] arg0 A data expression
179 : /// \param[in] arg1 A data expression
180 : /// \return Application of != to a number of arguments
181 118030 : inline application not_equal_to(const data_expression& arg0, const data_expression& arg1)
182 : {
183 118030 : assert(arg0.sort() == arg1.sort());
184 236060 : return not_equal_to(arg0.sort())(arg0, arg1);
185 : }
186 :
187 : /// \brief Recogniser for application of !=
188 : /// \param[in] e A data expression
189 : /// \return true iff e is an application of function symbol not_equal_to to a
190 : /// number of arguments
191 : template < typename DataExpression >
192 102752 : inline bool is_not_equal_to_application(const DataExpression& e)
193 : {
194 102752 : return detail::not_equal_symbol::is_application(e);
195 : }
196 :
197 : /// \brief Constructor for function symbol if
198 : /// \param[in] s A sort expression
199 : /// \return function symbol if_
200 425052 : inline function_symbol if_(const sort_expression& s)
201 : {
202 850104 : return function_symbol(detail::if_symbol::instance(), make_function_sort_(sort_bool::bool_(), s, s, s));
203 : }
204 :
205 : /// \brief Recogniser for function if
206 : /// \param[in] e A data expression
207 : /// \return true iff e is the function symbol matching if_
208 : template < typename DataExpression >
209 6 : inline bool is_if_function_symbol(const DataExpression& e)
210 : {
211 6 : return detail::if_symbol::is_function_symbol(e);
212 : }
213 :
214 : /// \brief Application of function symbol if
215 : /// \param[in] arg0 A data expression
216 : /// \param[in] arg1 A data expression
217 : /// \param[in] arg2 A data expression
218 : /// \return Application of if to a number of arguments
219 348051 : inline application if_(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
220 : {
221 348051 : assert(sort_bool::is_bool(arg0.sort()));
222 348051 : assert(arg1.sort() == arg2.sort());
223 :
224 696102 : return if_(arg1.sort())(arg0, arg1, arg2);
225 : }
226 :
227 : /// \brief Recogniser for application of if
228 : /// \param[in] e A data expression
229 : /// \return true iff e is an application of function symbol if_ to a
230 : /// number of arguments
231 : template < typename DataExpression >
232 39520 : inline bool is_if_application(const DataExpression& e)
233 : {
234 39520 : return detail::if_symbol::is_application(e);
235 : }
236 :
237 : /// \brief Constructor for function symbol <
238 : /// \param[in] s A sort expression
239 : /// \return function symbol less
240 542480 : inline function_symbol less(const sort_expression& s)
241 : {
242 1084960 : return function_symbol(detail::less_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
243 : }
244 :
245 : /// \brief Recogniser for function <
246 : /// \param[in] e A data expression
247 : /// \return true iff e is the function symbol matching <
248 : template < typename DataExpression >
249 : inline bool is_less_function_symbol(const DataExpression& e)
250 : {
251 : return detail::less_symbol::is_function_symbol(e);
252 : }
253 :
254 : /// \brief Application of function symbol <
255 : /// \param[in] arg0 A data expression
256 : /// \param[in] arg1 A data expression
257 : /// \return Application of < to a number of arguments
258 466128 : inline application less(const data_expression& arg0, const data_expression& arg1)
259 : {
260 466128 : assert(arg0.sort() == arg1.sort());
261 932256 : return less(arg0.sort())(arg0, arg1);
262 : }
263 :
264 : /// \brief Recogniser for application of <
265 : /// \param[in] e A data expression
266 : /// \return true iff e is an application of function symbol less to a
267 : /// number of arguments
268 : template < typename DataExpression >
269 60595 : inline bool is_less_application(const DataExpression& e)
270 : {
271 60595 : return detail::less_symbol::is_application(e);
272 : }
273 :
274 : /// \brief Constructor for function symbol <=
275 : /// \param[in] s A sort expression
276 : /// \return function symbol less_equal
277 556431 : inline function_symbol less_equal(const sort_expression& s)
278 : {
279 1112862 : return function_symbol(detail::less_equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
280 : }
281 :
282 : /// \brief Recogniser for function <=
283 : /// \param[in] e A data expression
284 : /// \return true iff e is the function symbol matching <=
285 : template < typename DataExpression >
286 : inline bool is_less_equal_function_symbol(const DataExpression& e)
287 : {
288 : return detail::less_equal_symbol::is_function_symbol(e);
289 : }
290 :
291 : /// \brief Application of function symbol <=
292 : /// \param[in] arg0 A data expression
293 : /// \param[in] arg1 A data expression
294 : /// \return Application of <= to a number of arguments
295 480079 : inline application less_equal(const data_expression& arg0, const data_expression& arg1)
296 : {
297 480079 : assert(arg0.sort() == arg1.sort());
298 960158 : return less_equal(arg0.sort())(arg0, arg1);
299 : }
300 :
301 : /// \brief Recogniser for application of <=
302 : /// \param[in] e A data expression
303 : /// \return true iff e is an application of function symbol less_equal to a
304 : /// number of arguments
305 : template < typename DataExpression >
306 53106 : inline bool is_less_equal_application(const DataExpression& e)
307 : {
308 53106 : return detail::less_equal_symbol::is_application(e);
309 : }
310 :
311 : /// \brief Constructor for function symbol >
312 : /// \param[in] s A sort expression
313 : /// \return function symbol greater
314 161661 : inline function_symbol greater(const sort_expression& s)
315 : {
316 323322 : return function_symbol(detail::greater_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
317 : }
318 :
319 : /// \brief Recogniser for function >
320 : /// \param[in] e A data expression
321 : /// \return true iff e is the function symbol matching >
322 : template < typename DataExpression >
323 : inline bool is_greater_function_symbol(const DataExpression& e)
324 : {
325 : return detail::greater_symbol::is_function_symbol(e);
326 : }
327 :
328 : /// \brief Application of function symbol >
329 : /// \param[in] arg0 A data expression
330 : /// \param[in] arg1 A data expression
331 : /// \return Application of > to a number of arguments
332 85309 : inline application greater(const data_expression& arg0, const data_expression& arg1)
333 : {
334 85309 : assert(arg0.sort() == arg1.sort());
335 170618 : return greater(arg0.sort())(arg0, arg1);
336 : }
337 :
338 : /// \brief Recogniser for application of >
339 : /// \param[in] e A data expression
340 : /// \return true iff e is an application of function symbol greater to a
341 : /// number of arguments
342 : template < typename DataExpression >
343 52623 : inline bool is_greater_application(const DataExpression& e)
344 : {
345 52623 : return detail::greater_symbol::is_application(e);
346 : }
347 :
348 : /// \brief Constructor for function symbol >=
349 : /// \param[in] s A sort expression
350 : /// \return function symbol greater_equal
351 148095 : inline function_symbol greater_equal(const sort_expression& s)
352 : {
353 296190 : return function_symbol(detail::greater_equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
354 : }
355 :
356 : /// \brief Recogniser for function >=
357 : /// \param[in] e A data expression
358 : /// \return true iff e is the function symbol matching >=
359 : template < typename DataExpression >
360 : inline bool is_greater_equal_function_symbol(const DataExpression& e)
361 : {
362 : return detail::greater_equal_symbol::is_function_symbol(e);
363 : }
364 :
365 : /// \brief Application of function symbol >=
366 : /// \param[in] arg0 A data expression
367 : /// \param[in] arg1 A data expression
368 : /// \return Application of >= to a number of arguments
369 71743 : inline application greater_equal(const data_expression& arg0, const data_expression& arg1)
370 : {
371 71743 : assert(arg0.sort() == arg1.sort());
372 143486 : return greater_equal(arg0.sort())(arg0, arg1);
373 : }
374 :
375 : /// \brief Recogniser for application of >=
376 : /// \param[in] e A data expression
377 : /// \return true iff e is an application of function symbol greater_equal to a
378 : /// number of arguments
379 : template < typename DataExpression >
380 52489 : inline bool is_greater_equal_application(const DataExpression& e)
381 : {
382 52489 : return detail::greater_equal_symbol::is_application(e);
383 : }
384 :
385 : /// \brief Give all standard system defined functions for sort s
386 : /// \param[in] s A sort expression
387 : /// \return All standard system defined functions for sort s
388 71752 : inline function_symbol_vector standard_generate_functions_code(const sort_expression& s)
389 : {
390 71752 : function_symbol_vector result;
391 71752 : result.push_back(equal_to(s));
392 71752 : result.push_back(not_equal_to(s));
393 71752 : result.push_back(if_(s));
394 71752 : result.push_back(less(s));
395 71752 : result.push_back(less_equal(s));
396 71752 : result.push_back(greater_equal(s));
397 71752 : result.push_back(greater(s));
398 :
399 71752 : return result;
400 0 : }
401 :
402 : /// \brief Give all standard system defined equations for sort s
403 : /// \param[in] s A sort expression
404 : /// \return All standard system defined equations for sort s
405 71742 : inline data_equation_vector standard_generate_equations_code(const sort_expression& s)
406 : {
407 71742 : data_equation_vector result;
408 143484 : variable b("b", sort_bool::bool_());
409 143484 : variable x("x", s);
410 143484 : variable y("y", s);
411 143484 : result.push_back(data_equation(variable_list({x}), equal_to(x, x), sort_bool::true_()));
412 215226 : result.push_back(data_equation(variable_list({x, y}), not_equal_to(x, y), sort_bool::not_(equal_to(x, y))));
413 215226 : result.push_back(data_equation(variable_list({x, y}), if_(sort_bool::true_(), x, y), x));
414 215226 : result.push_back(data_equation(variable_list({x, y}), if_(sort_bool::false_(), x, y), y));
415 215226 : result.push_back(data_equation(variable_list({b, x}), if_(b, x, x), x));
416 143484 : result.push_back(data_equation(variable_list({x}), less(x,x), sort_bool::false_()));
417 143484 : result.push_back(data_equation(variable_list({x}), less_equal(x,x), sort_bool::true_()));
418 215226 : result.push_back(data_equation(variable_list({x, y}), greater_equal(x,y), less_equal(y,x)));
419 215226 : result.push_back(data_equation(variable_list({x, y}), greater(x,y), less(y,x)));
420 :
421 : // For a function sort, add the equation f==g iff forall x.f(x)==g(x). This equation is not in the Specification and Analysis of Communicating Systems of 2014.
422 71742 : if (is_function_sort(s))
423 : {
424 18434 : const function_sort& fs = atermpp::down_cast<function_sort>(s);
425 18434 : variable_vector xvars,yvars;
426 18434 : std::size_t index=0;
427 50671 : for(const sort_expression& sort: fs.domain())
428 : {
429 32237 : std::stringstream xs;
430 32237 : xs << "x" << index;
431 32237 : ++index;
432 32237 : variable x(xs.str(),sort);
433 32237 : xvars.push_back(x);
434 32237 : }
435 36868 : variable f("f",s);
436 36868 : variable g("g",s);
437 18434 : variable_list xvar_list=variable_list(xvars.begin(),xvars.end());
438 55302 : result.push_back(data_equation(variable_list({ f, g }) + xvar_list,
439 36868 : equal_to(f,g),
440 36868 : abstraction(forall_binder(),xvar_list,
441 36868 : equal_to(
442 36868 : application(f,xvars.begin(),xvars.end()),
443 36868 : application(g,xvars.begin(),xvars.end())))));
444 18434 : }
445 :
446 143484 : return result;
447 71742 : }
448 :
449 : } // namespace data
450 : } // namespace mcrl2
451 :
452 : #endif // MCRL2_DATA_STANDARD_H
|