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/list.h
10 : /// \brief The standard sort list.
11 : ///
12 : /// This file was generated from the data sort specification
13 : /// mcrl2/data/build/list.spec.
14 :
15 : #ifndef MCRL2_DATA_LIST_H
16 : #define MCRL2_DATA_LIST_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/container_sort.h"
27 : #include "mcrl2/data/bool.h"
28 : #include "mcrl2/data/pos.h"
29 : #include "mcrl2/data/nat.h"
30 :
31 : namespace mcrl2 {
32 :
33 : namespace data {
34 :
35 : /// \brief Namespace for system defined sort list.
36 : namespace sort_list {
37 :
38 : /// \brief Constructor for sort expression List(S)
39 : /// \param s A sort expression
40 : /// \return Sort expression list(s)
41 : inline
42 233337 : container_sort list(const sort_expression& s)
43 : {
44 233337 : container_sort list(list_container(), s);
45 233337 : return list;
46 : }
47 :
48 : /// \brief Recogniser for sort expression List(s)
49 : /// \param e A sort expression
50 : /// \return true iff e is a container sort of which the name matches
51 : /// list
52 : inline
53 9575 : bool is_list(const sort_expression& e)
54 : {
55 9575 : if (is_container_sort(e))
56 : {
57 8201 : return container_sort(e).container_name() == list_container();
58 : }
59 1374 : return false;
60 : }
61 :
62 :
63 : /// \brief Generate identifier [].
64 : /// \return Identifier [].
65 : inline
66 30782 : const core::identifier_string& empty_name()
67 : {
68 30782 : static core::identifier_string empty_name = core::identifier_string("[]");
69 30782 : return empty_name;
70 : }
71 :
72 : /// \brief Constructor for function symbol [].
73 : /// \param s A sort expression.
74 : /// \return Function symbol empty.
75 : inline
76 22009 : function_symbol empty(const sort_expression& s)
77 : {
78 22009 : function_symbol empty(empty_name(), list(s));
79 22009 : return empty;
80 : }
81 :
82 : /// \brief Recogniser for function [].
83 : /// \param e A data expression.
84 : /// \return true iff e is the function symbol matching [].
85 : inline
86 13345 : bool is_empty_function_symbol(const atermpp::aterm_appl& e)
87 : {
88 13345 : if (is_function_symbol(e))
89 : {
90 8773 : return atermpp::down_cast<function_symbol>(e).name() == empty_name();
91 : }
92 4572 : return false;
93 : }
94 :
95 : /// \brief Generate identifier |>.
96 : /// \return Identifier |>.
97 : inline
98 215156 : const core::identifier_string& cons_name()
99 : {
100 215156 : static core::identifier_string cons_name = core::identifier_string("|>");
101 215156 : return cons_name;
102 : }
103 :
104 : /// \brief Constructor for function symbol |>.
105 : /// \param s A sort expression.
106 : /// \return Function symbol cons_.
107 : inline
108 40484 : function_symbol cons_(const sort_expression& s)
109 : {
110 80968 : function_symbol cons_(cons_name(), make_function_sort_(s, list(s), list(s)));
111 40484 : return cons_;
112 : }
113 :
114 : /// \brief Recogniser for function |>.
115 : /// \param e A data expression.
116 : /// \return true iff e is the function symbol matching |>.
117 : inline
118 116301 : bool is_cons_function_symbol(const atermpp::aterm_appl& e)
119 : {
120 116301 : if (is_function_symbol(e))
121 : {
122 115067 : return atermpp::down_cast<function_symbol>(e).name() == cons_name();
123 : }
124 1234 : return false;
125 : }
126 :
127 : /// \brief Application of function symbol |>.
128 : /// \param s A sort expression.
129 : /// \param arg0 A data expression.
130 : /// \param arg1 A data expression.
131 : /// \return Application of |> to a number of arguments.
132 : inline
133 34757 : application cons_(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
134 : {
135 69514 : return sort_list::cons_(s)(arg0, arg1);
136 : }
137 :
138 : /// \brief Make an application of function symbol |>.
139 : /// \param result The data expression where the |> expression is put.
140 : /// \param s A sort expression.
141 : /// \param arg0 A data expression.
142 : /// \param arg1 A data expression.
143 : inline
144 : void make_cons_(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
145 : {
146 : make_application(result, sort_list::cons_(s),arg0, arg1);
147 : }
148 :
149 : /// \brief Recogniser for application of |>.
150 : /// \param e A data expression.
151 : /// \return true iff e is an application of function symbol cons_ to a
152 : /// number of arguments.
153 : inline
154 133822 : bool is_cons_application(const atermpp::aterm_appl& e)
155 : {
156 133822 : return is_application(e) && is_cons_function_symbol(atermpp::down_cast<application>(e).head());
157 : }
158 : /// \brief Give all system defined constructors for list.
159 : /// \param s A sort expression.
160 : /// \return All system defined constructors for list.
161 : inline
162 1078 : function_symbol_vector list_generate_constructors_code(const sort_expression& s)
163 : {
164 1078 : function_symbol_vector result;
165 1078 : result.push_back(sort_list::empty(s));
166 1078 : result.push_back(sort_list::cons_(s));
167 :
168 1078 : return result;
169 0 : }
170 : /// \brief Give all defined constructors which can be used in mCRL2 specs for list.
171 : /// \param s A sort expression.
172 : /// \return All system defined constructors that can be used in an mCRL2 specification for list.
173 : inline
174 4578 : function_symbol_vector list_mCRL2_usable_constructors(const sort_expression& s)
175 : {
176 4578 : function_symbol_vector result;
177 4578 : result.push_back(sort_list::empty(s));
178 4578 : result.push_back(sort_list::cons_(s));
179 :
180 4578 : return result;
181 0 : }
182 : // 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
183 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
184 : /// \brief Give all system defined constructors which have an implementation in C++ and not in rewrite rules for list.
185 : /// \param s A sort expression.
186 : /// \return All system defined constructors that are to be implemented in C++ for list.
187 : inline
188 1078 : implementation_map list_cpp_implementable_constructors(const sort_expression& s)
189 : {
190 1078 : implementation_map result;
191 : static_cast< void >(s); // suppress unused variable warnings
192 1078 : return result;
193 : }
194 :
195 : /// \brief Generate identifier in.
196 : /// \return Identifier in.
197 : inline
198 105531 : const core::identifier_string& in_name()
199 : {
200 105531 : static core::identifier_string in_name = core::identifier_string("in");
201 105531 : return in_name;
202 : }
203 :
204 : /// \brief Constructor for function symbol in.
205 : /// \param s A sort expression.
206 : /// \return Function symbol in.
207 : inline
208 8965 : function_symbol in(const sort_expression& s)
209 : {
210 17930 : function_symbol in(in_name(), make_function_sort_(s, list(s), sort_bool::bool_()));
211 8965 : return in;
212 : }
213 :
214 : /// \brief Recogniser for function in.
215 : /// \param e A data expression.
216 : /// \return true iff e is the function symbol matching in.
217 : inline
218 38733 : bool is_in_function_symbol(const atermpp::aterm_appl& e)
219 : {
220 38733 : if (is_function_symbol(e))
221 : {
222 37499 : return atermpp::down_cast<function_symbol>(e).name() == in_name();
223 : }
224 1234 : return false;
225 : }
226 :
227 : /// \brief Application of function symbol in.
228 : /// \param s A sort expression.
229 : /// \param arg0 A data expression.
230 : /// \param arg1 A data expression.
231 : /// \return Application of in to a number of arguments.
232 : inline
233 3238 : application in(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
234 : {
235 6476 : return sort_list::in(s)(arg0, arg1);
236 : }
237 :
238 : /// \brief Make an application of function symbol in.
239 : /// \param result The data expression where the in expression is put.
240 : /// \param s A sort expression.
241 : /// \param arg0 A data expression.
242 : /// \param arg1 A data expression.
243 : inline
244 : void make_in(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
245 : {
246 : make_application(result, sort_list::in(s),arg0, arg1);
247 : }
248 :
249 : /// \brief Recogniser for application of in.
250 : /// \param e A data expression.
251 : /// \return true iff e is an application of function symbol in to a
252 : /// number of arguments.
253 : inline
254 38733 : bool is_in_application(const atermpp::aterm_appl& e)
255 : {
256 38733 : return is_application(e) && is_in_function_symbol(atermpp::down_cast<application>(e).head());
257 : }
258 :
259 : /// \brief Generate identifier #.
260 : /// \return Identifier #.
261 : inline
262 22691 : const core::identifier_string& count_name()
263 : {
264 22691 : static core::identifier_string count_name = core::identifier_string("#");
265 22691 : return count_name;
266 : }
267 :
268 : /// \brief Constructor for function symbol #.
269 : /// \param s A sort expression.
270 : /// \return Function symbol count.
271 : inline
272 8960 : function_symbol count(const sort_expression& s)
273 : {
274 17920 : function_symbol count(count_name(), make_function_sort_(list(s), sort_nat::nat()));
275 8960 : return count;
276 : }
277 :
278 : /// \brief Recogniser for function #.
279 : /// \param e A data expression.
280 : /// \return true iff e is the function symbol matching #.
281 : inline
282 14573 : bool is_count_function_symbol(const atermpp::aterm_appl& e)
283 : {
284 14573 : if (is_function_symbol(e))
285 : {
286 13731 : return atermpp::down_cast<function_symbol>(e).name() == count_name();
287 : }
288 842 : return false;
289 : }
290 :
291 : /// \brief Application of function symbol #.
292 : /// \param s A sort expression.
293 : /// \param arg0 A data expression.
294 : /// \return Application of # to a number of arguments.
295 : inline
296 3233 : application count(const sort_expression& s, const data_expression& arg0)
297 : {
298 6466 : return sort_list::count(s)(arg0);
299 : }
300 :
301 : /// \brief Make an application of function symbol #.
302 : /// \param result The data expression where the # expression is put.
303 : /// \param s A sort expression.
304 : /// \param arg0 A data expression.
305 : inline
306 : void make_count(data_expression& result, const sort_expression& s, const data_expression& arg0)
307 : {
308 : make_application(result, sort_list::count(s),arg0);
309 : }
310 :
311 : /// \brief Recogniser for application of #.
312 : /// \param e A data expression.
313 : /// \return true iff e is an application of function symbol count to a
314 : /// number of arguments.
315 : inline
316 14573 : bool is_count_application(const atermpp::aterm_appl& e)
317 : {
318 14573 : return is_application(e) && is_count_function_symbol(atermpp::down_cast<application>(e).head());
319 : }
320 :
321 : /// \brief Generate identifier <|.
322 : /// \return Identifier <|.
323 : inline
324 107411 : const core::identifier_string& snoc_name()
325 : {
326 107411 : static core::identifier_string snoc_name = core::identifier_string("<|");
327 107411 : return snoc_name;
328 : }
329 :
330 : /// \brief Constructor for function symbol <|.
331 : /// \param s A sort expression.
332 : /// \return Function symbol snoc.
333 : inline
334 8971 : function_symbol snoc(const sort_expression& s)
335 : {
336 17942 : function_symbol snoc(snoc_name(), make_function_sort_(list(s), s, list(s)));
337 8971 : return snoc;
338 : }
339 :
340 : /// \brief Recogniser for function <|.
341 : /// \param e A data expression.
342 : /// \return true iff e is the function symbol matching <|.
343 : inline
344 40537 : bool is_snoc_function_symbol(const atermpp::aterm_appl& e)
345 : {
346 40537 : if (is_function_symbol(e))
347 : {
348 39303 : return atermpp::down_cast<function_symbol>(e).name() == snoc_name();
349 : }
350 1234 : return false;
351 : }
352 :
353 : /// \brief Application of function symbol <|.
354 : /// \param s A sort expression.
355 : /// \param arg0 A data expression.
356 : /// \param arg1 A data expression.
357 : /// \return Application of <| to a number of arguments.
358 : inline
359 3244 : application snoc(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
360 : {
361 6488 : return sort_list::snoc(s)(arg0, arg1);
362 : }
363 :
364 : /// \brief Make an application of function symbol <|.
365 : /// \param result The data expression where the <| expression is put.
366 : /// \param s A sort expression.
367 : /// \param arg0 A data expression.
368 : /// \param arg1 A data expression.
369 : inline
370 : void make_snoc(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
371 : {
372 : make_application(result, sort_list::snoc(s),arg0, arg1);
373 : }
374 :
375 : /// \brief Recogniser for application of <|.
376 : /// \param e A data expression.
377 : /// \return true iff e is an application of function symbol snoc to a
378 : /// number of arguments.
379 : inline
380 45001 : bool is_snoc_application(const atermpp::aterm_appl& e)
381 : {
382 45001 : return is_application(e) && is_snoc_function_symbol(atermpp::down_cast<application>(e).head());
383 : }
384 :
385 : /// \brief Generate identifier ++.
386 : /// \return Identifier ++.
387 : inline
388 94998 : const core::identifier_string& concat_name()
389 : {
390 94998 : static core::identifier_string concat_name = core::identifier_string("++");
391 94998 : return concat_name;
392 : }
393 :
394 : /// \brief Constructor for function symbol ++.
395 : /// \param s A sort expression.
396 : /// \return Function symbol concat.
397 : inline
398 10040 : function_symbol concat(const sort_expression& s)
399 : {
400 20080 : function_symbol concat(concat_name(), make_function_sort_(list(s), list(s), list(s)));
401 10040 : return concat;
402 : }
403 :
404 : /// \brief Recogniser for function ++.
405 : /// \param e A data expression.
406 : /// \return true iff e is the function symbol matching ++.
407 : inline
408 27057 : bool is_concat_function_symbol(const atermpp::aterm_appl& e)
409 : {
410 27057 : if (is_function_symbol(e))
411 : {
412 25823 : return atermpp::down_cast<function_symbol>(e).name() == concat_name();
413 : }
414 1234 : return false;
415 : }
416 :
417 : /// \brief Application of function symbol ++.
418 : /// \param s A sort expression.
419 : /// \param arg0 A data expression.
420 : /// \param arg1 A data expression.
421 : /// \return Application of ++ to a number of arguments.
422 : inline
423 4313 : application concat(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
424 : {
425 8626 : return sort_list::concat(s)(arg0, arg1);
426 : }
427 :
428 : /// \brief Make an application of function symbol ++.
429 : /// \param result The data expression where the ++ expression is put.
430 : /// \param s A sort expression.
431 : /// \param arg0 A data expression.
432 : /// \param arg1 A data expression.
433 : inline
434 : void make_concat(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
435 : {
436 : make_application(result, sort_list::concat(s),arg0, arg1);
437 : }
438 :
439 : /// \brief Recogniser for application of ++.
440 : /// \param e A data expression.
441 : /// \return true iff e is an application of function symbol concat to a
442 : /// number of arguments.
443 : inline
444 27057 : bool is_concat_application(const atermpp::aterm_appl& e)
445 : {
446 27057 : return is_application(e) && is_concat_function_symbol(atermpp::down_cast<application>(e).head());
447 : }
448 :
449 : /// \brief Generate identifier ..
450 : /// \return Identifier ..
451 : inline
452 92276 : const core::identifier_string& element_at_name()
453 : {
454 92276 : static core::identifier_string element_at_name = core::identifier_string(".");
455 92276 : return element_at_name;
456 : }
457 :
458 : /// \brief Constructor for function symbol ..
459 : /// \param s A sort expression.
460 : /// \return Function symbol element_at.
461 : inline
462 8960 : function_symbol element_at(const sort_expression& s)
463 : {
464 17920 : function_symbol element_at(element_at_name(), make_function_sort_(list(s), sort_nat::nat(), s));
465 8960 : return element_at;
466 : }
467 :
468 : /// \brief Recogniser for function ..
469 : /// \param e A data expression.
470 : /// \return true iff e is the function symbol matching ..
471 : inline
472 25487 : bool is_element_at_function_symbol(const atermpp::aterm_appl& e)
473 : {
474 25487 : if (is_function_symbol(e))
475 : {
476 24253 : return atermpp::down_cast<function_symbol>(e).name() == element_at_name();
477 : }
478 1234 : return false;
479 : }
480 :
481 : /// \brief Application of function symbol ..
482 : /// \param s A sort expression.
483 : /// \param arg0 A data expression.
484 : /// \param arg1 A data expression.
485 : /// \return Application of . to a number of arguments.
486 : inline
487 3233 : application element_at(const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
488 : {
489 6466 : return sort_list::element_at(s)(arg0, arg1);
490 : }
491 :
492 : /// \brief Make an application of function symbol ..
493 : /// \param result The data expression where the . expression is put.
494 : /// \param s A sort expression.
495 : /// \param arg0 A data expression.
496 : /// \param arg1 A data expression.
497 : inline
498 : void make_element_at(data_expression& result, const sort_expression& s, const data_expression& arg0, const data_expression& arg1)
499 : {
500 : make_application(result, sort_list::element_at(s),arg0, arg1);
501 : }
502 :
503 : /// \brief Recogniser for application of ..
504 : /// \param e A data expression.
505 : /// \return true iff e is an application of function symbol element_at to a
506 : /// number of arguments.
507 : inline
508 25487 : bool is_element_at_application(const atermpp::aterm_appl& e)
509 : {
510 25487 : return is_application(e) && is_element_at_function_symbol(atermpp::down_cast<application>(e).head());
511 : }
512 :
513 : /// \brief Generate identifier head.
514 : /// \return Identifier head.
515 : inline
516 65428 : const core::identifier_string& head_name()
517 : {
518 65428 : static core::identifier_string head_name = core::identifier_string("head");
519 65428 : return head_name;
520 : }
521 :
522 : /// \brief Constructor for function symbol head.
523 : /// \param s A sort expression.
524 : /// \return Function symbol head.
525 : inline
526 6806 : function_symbol head(const sort_expression& s)
527 : {
528 13612 : function_symbol head(head_name(), make_function_sort_(list(s), s));
529 6806 : return head;
530 : }
531 :
532 : /// \brief Recogniser for function head.
533 : /// \param e A data expression.
534 : /// \return true iff e is the function symbol matching head.
535 : inline
536 1 : bool is_head_function_symbol(const atermpp::aterm_appl& e)
537 : {
538 1 : if (is_function_symbol(e))
539 : {
540 1 : return atermpp::down_cast<function_symbol>(e).name() == head_name();
541 : }
542 0 : return false;
543 : }
544 :
545 : /// \brief Application of function symbol head.
546 : /// \param s A sort expression.
547 : /// \param arg0 A data expression.
548 : /// \return Application of head to a number of arguments.
549 : inline
550 1079 : application head(const sort_expression& s, const data_expression& arg0)
551 : {
552 2158 : return sort_list::head(s)(arg0);
553 : }
554 :
555 : /// \brief Make an application of function symbol head.
556 : /// \param result The data expression where the head expression is put.
557 : /// \param s A sort expression.
558 : /// \param arg0 A data expression.
559 : inline
560 : void make_head(data_expression& result, const sort_expression& s, const data_expression& arg0)
561 : {
562 : make_application(result, sort_list::head(s),arg0);
563 : }
564 :
565 : /// \brief Recogniser for application of head.
566 : /// \param e A data expression.
567 : /// \return true iff e is an application of function symbol head to a
568 : /// number of arguments.
569 : inline
570 1 : bool is_head_application(const atermpp::aterm_appl& e)
571 : {
572 1 : return is_application(e) && is_head_function_symbol(atermpp::down_cast<application>(e).head());
573 : }
574 :
575 : /// \brief Generate identifier tail.
576 : /// \return Identifier tail.
577 : inline
578 65428 : const core::identifier_string& tail_name()
579 : {
580 65428 : static core::identifier_string tail_name = core::identifier_string("tail");
581 65428 : return tail_name;
582 : }
583 :
584 : /// \brief Constructor for function symbol tail.
585 : /// \param s A sort expression.
586 : /// \return Function symbol tail.
587 : inline
588 6806 : function_symbol tail(const sort_expression& s)
589 : {
590 13612 : function_symbol tail(tail_name(), make_function_sort_(list(s), list(s)));
591 6806 : return tail;
592 : }
593 :
594 : /// \brief Recogniser for function tail.
595 : /// \param e A data expression.
596 : /// \return true iff e is the function symbol matching tail.
597 : inline
598 1 : bool is_tail_function_symbol(const atermpp::aterm_appl& e)
599 : {
600 1 : if (is_function_symbol(e))
601 : {
602 1 : return atermpp::down_cast<function_symbol>(e).name() == tail_name();
603 : }
604 0 : return false;
605 : }
606 :
607 : /// \brief Application of function symbol tail.
608 : /// \param s A sort expression.
609 : /// \param arg0 A data expression.
610 : /// \return Application of tail to a number of arguments.
611 : inline
612 1079 : application tail(const sort_expression& s, const data_expression& arg0)
613 : {
614 2158 : return sort_list::tail(s)(arg0);
615 : }
616 :
617 : /// \brief Make an application of function symbol tail.
618 : /// \param result The data expression where the tail expression is put.
619 : /// \param s A sort expression.
620 : /// \param arg0 A data expression.
621 : inline
622 : void make_tail(data_expression& result, const sort_expression& s, const data_expression& arg0)
623 : {
624 : make_application(result, sort_list::tail(s),arg0);
625 : }
626 :
627 : /// \brief Recogniser for application of tail.
628 : /// \param e A data expression.
629 : /// \return true iff e is an application of function symbol tail to a
630 : /// number of arguments.
631 : inline
632 1 : bool is_tail_application(const atermpp::aterm_appl& e)
633 : {
634 1 : return is_application(e) && is_tail_function_symbol(atermpp::down_cast<application>(e).head());
635 : }
636 :
637 : /// \brief Generate identifier rhead.
638 : /// \return Identifier rhead.
639 : inline
640 67498 : const core::identifier_string& rhead_name()
641 : {
642 67498 : static core::identifier_string rhead_name = core::identifier_string("rhead");
643 67498 : return rhead_name;
644 : }
645 :
646 : /// \brief Constructor for function symbol rhead.
647 : /// \param s A sort expression.
648 : /// \return Function symbol rhead.
649 : inline
650 8960 : function_symbol rhead(const sort_expression& s)
651 : {
652 17920 : function_symbol rhead(rhead_name(), make_function_sort_(list(s), s));
653 8960 : return rhead;
654 : }
655 :
656 : /// \brief Recogniser for function rhead.
657 : /// \param e A data expression.
658 : /// \return true iff e is the function symbol matching rhead.
659 : inline
660 1 : bool is_rhead_function_symbol(const atermpp::aterm_appl& e)
661 : {
662 1 : if (is_function_symbol(e))
663 : {
664 1 : return atermpp::down_cast<function_symbol>(e).name() == rhead_name();
665 : }
666 0 : return false;
667 : }
668 :
669 : /// \brief Application of function symbol rhead.
670 : /// \param s A sort expression.
671 : /// \param arg0 A data expression.
672 : /// \return Application of rhead to a number of arguments.
673 : inline
674 3233 : application rhead(const sort_expression& s, const data_expression& arg0)
675 : {
676 6466 : return sort_list::rhead(s)(arg0);
677 : }
678 :
679 : /// \brief Make an application of function symbol rhead.
680 : /// \param result The data expression where the rhead expression is put.
681 : /// \param s A sort expression.
682 : /// \param arg0 A data expression.
683 : inline
684 : void make_rhead(data_expression& result, const sort_expression& s, const data_expression& arg0)
685 : {
686 : make_application(result, sort_list::rhead(s),arg0);
687 : }
688 :
689 : /// \brief Recogniser for application of rhead.
690 : /// \param e A data expression.
691 : /// \return true iff e is an application of function symbol rhead to a
692 : /// number of arguments.
693 : inline
694 1 : bool is_rhead_application(const atermpp::aterm_appl& e)
695 : {
696 1 : return is_application(e) && is_rhead_function_symbol(atermpp::down_cast<application>(e).head());
697 : }
698 :
699 : /// \brief Generate identifier rtail.
700 : /// \return Identifier rtail.
701 : inline
702 67442 : const core::identifier_string& rtail_name()
703 : {
704 67442 : static core::identifier_string rtail_name = core::identifier_string("rtail");
705 67442 : return rtail_name;
706 : }
707 :
708 : /// \brief Constructor for function symbol rtail.
709 : /// \param s A sort expression.
710 : /// \return Function symbol rtail.
711 : inline
712 8960 : function_symbol rtail(const sort_expression& s)
713 : {
714 17920 : function_symbol rtail(rtail_name(), make_function_sort_(list(s), list(s)));
715 8960 : return rtail;
716 : }
717 :
718 : /// \brief Recogniser for function rtail.
719 : /// \param e A data expression.
720 : /// \return true iff e is the function symbol matching rtail.
721 : inline
722 1 : bool is_rtail_function_symbol(const atermpp::aterm_appl& e)
723 : {
724 1 : if (is_function_symbol(e))
725 : {
726 1 : return atermpp::down_cast<function_symbol>(e).name() == rtail_name();
727 : }
728 0 : return false;
729 : }
730 :
731 : /// \brief Application of function symbol rtail.
732 : /// \param s A sort expression.
733 : /// \param arg0 A data expression.
734 : /// \return Application of rtail to a number of arguments.
735 : inline
736 3233 : application rtail(const sort_expression& s, const data_expression& arg0)
737 : {
738 6466 : return sort_list::rtail(s)(arg0);
739 : }
740 :
741 : /// \brief Make an application of function symbol rtail.
742 : /// \param result The data expression where the rtail expression is put.
743 : /// \param s A sort expression.
744 : /// \param arg0 A data expression.
745 : inline
746 : void make_rtail(data_expression& result, const sort_expression& s, const data_expression& arg0)
747 : {
748 : make_application(result, sort_list::rtail(s),arg0);
749 : }
750 :
751 : /// \brief Recogniser for application of rtail.
752 : /// \param e A data expression.
753 : /// \return true iff e is an application of function symbol rtail to a
754 : /// number of arguments.
755 : inline
756 1 : bool is_rtail_application(const atermpp::aterm_appl& e)
757 : {
758 1 : return is_application(e) && is_rtail_function_symbol(atermpp::down_cast<application>(e).head());
759 : }
760 : /// \brief Give all system defined mappings for list
761 : /// \param s A sort expression
762 : /// \return All system defined mappings for list
763 : inline
764 1078 : function_symbol_vector list_generate_functions_code(const sort_expression& s)
765 : {
766 1078 : function_symbol_vector result;
767 1078 : result.push_back(sort_list::in(s));
768 1078 : result.push_back(sort_list::count(s));
769 1078 : result.push_back(sort_list::snoc(s));
770 1078 : result.push_back(sort_list::concat(s));
771 1078 : result.push_back(sort_list::element_at(s));
772 1078 : result.push_back(sort_list::head(s));
773 1078 : result.push_back(sort_list::tail(s));
774 1078 : result.push_back(sort_list::rhead(s));
775 1078 : result.push_back(sort_list::rtail(s));
776 1078 : return result;
777 0 : }
778 :
779 : /// \brief Give all system defined mappings and constructors for list
780 : /// \param s A sort expression
781 : /// \return All system defined mappings for list
782 : inline
783 : function_symbol_vector list_generate_constructors_and_functions_code(const sort_expression& s)
784 : {
785 : function_symbol_vector result=list_generate_functions_code(s);
786 : for(const function_symbol& f: list_generate_constructors_code(s))
787 : {
788 : result.push_back(f);
789 : }
790 : return result;
791 : }
792 :
793 : /// \brief Give all system defined mappings that can be used in mCRL2 specs for list
794 : /// \param s A sort expression
795 : /// \return All system defined mappings for that can be used in mCRL2 specificationis list
796 : inline
797 4578 : function_symbol_vector list_mCRL2_usable_mappings(const sort_expression& s)
798 : {
799 4578 : function_symbol_vector result;
800 4578 : result.push_back(sort_list::in(s));
801 4578 : result.push_back(sort_list::count(s));
802 4578 : result.push_back(sort_list::snoc(s));
803 4578 : result.push_back(sort_list::concat(s));
804 4578 : result.push_back(sort_list::element_at(s));
805 4578 : result.push_back(sort_list::head(s));
806 4578 : result.push_back(sort_list::tail(s));
807 4578 : result.push_back(sort_list::rhead(s));
808 4578 : result.push_back(sort_list::rtail(s));
809 4578 : return result;
810 0 : }
811 :
812 :
813 : // 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
814 : typedef std::map<function_symbol,std::pair<std::function<data_expression(const data_expression&)>, std::string> > implementation_map;
815 : /// \brief Give all system defined mappings that are to be implemented in C++ code for list
816 : /// \param s A sort expression
817 : /// \return A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for list
818 : inline
819 1078 : implementation_map list_cpp_implementable_mappings(const sort_expression& s)
820 : {
821 1078 : implementation_map result;
822 : static_cast< void >(s); // suppress unused variable warnings
823 1078 : return result;
824 : }
825 : ///\brief Function for projecting out argument.
826 : /// left from an application.
827 : /// \param e A data expression.
828 : /// \pre left is defined for e.
829 : /// \return The argument of e that corresponds to left.
830 : inline
831 18195 : const data_expression& left(const data_expression& e)
832 : {
833 18195 : assert(is_cons_application(e) || is_in_application(e) || is_snoc_application(e) || is_concat_application(e) || is_element_at_application(e));
834 18195 : return atermpp::down_cast<application>(e)[0];
835 : }
836 :
837 : ///\brief Function for projecting out argument.
838 : /// right from an application.
839 : /// \param e A data expression.
840 : /// \pre right is defined for e.
841 : /// \return The argument of e that corresponds to right.
842 : inline
843 27628 : const data_expression& right(const data_expression& e)
844 : {
845 27628 : assert(is_cons_application(e) || is_in_application(e) || is_snoc_application(e) || is_concat_application(e) || is_element_at_application(e));
846 27628 : return atermpp::down_cast<application>(e)[1];
847 : }
848 :
849 : ///\brief Function for projecting out argument.
850 : /// arg from an application.
851 : /// \param e A data expression.
852 : /// \pre arg is defined for e.
853 : /// \return The argument of e that corresponds to arg.
854 : inline
855 2242 : const data_expression& arg(const data_expression& e)
856 : {
857 2242 : assert(is_count_application(e) || is_head_application(e) || is_tail_application(e) || is_rhead_application(e) || is_rtail_application(e));
858 2242 : return atermpp::down_cast<application>(e)[0];
859 : }
860 :
861 : /// \brief Give all system defined equations for list
862 : /// \param s A sort expression
863 : /// \return All system defined equations for sort list
864 : inline
865 1077 : data_equation_vector list_generate_equations_code(const sort_expression& s)
866 : {
867 2154 : variable vd("d",s);
868 2154 : variable ve("e",s);
869 2154 : variable vs("s",list(s));
870 2154 : variable vt("t",list(s));
871 2154 : variable vp("p",sort_pos::pos());
872 :
873 1077 : data_equation_vector result;
874 3231 : result.push_back(data_equation(variable_list({vd, vs}), equal_to(empty(s), cons_(s, vd, vs)), sort_bool::false_()));
875 3231 : result.push_back(data_equation(variable_list({vd, vs}), equal_to(cons_(s, vd, vs), empty(s)), sort_bool::false_()));
876 5385 : result.push_back(data_equation(variable_list({vd, ve, vs, vt}), equal_to(cons_(s, vd, vs), cons_(s, ve, vt)), sort_bool::and_(equal_to(vd, ve), equal_to(vs, vt))));
877 3231 : result.push_back(data_equation(variable_list({vd, vs}), less(empty(s), cons_(s, vd, vs)), sort_bool::true_()));
878 3231 : result.push_back(data_equation(variable_list({vd, vs}), less(cons_(s, vd, vs), empty(s)), sort_bool::false_()));
879 5385 : result.push_back(data_equation(variable_list({vd, ve, vs, vt}), less(cons_(s, vd, vs), cons_(s, ve, vt)), sort_bool::or_(sort_bool::and_(equal_to(vd, ve), less(vs, vt)), less(vd, ve))));
880 3231 : result.push_back(data_equation(variable_list({vd, vs}), less_equal(empty(s), cons_(s, vd, vs)), sort_bool::true_()));
881 3231 : result.push_back(data_equation(variable_list({vd, vs}), less_equal(cons_(s, vd, vs), empty(s)), sort_bool::false_()));
882 5385 : result.push_back(data_equation(variable_list({vd, ve, vs, vt}), less_equal(cons_(s, vd, vs), cons_(s, ve, vt)), sort_bool::or_(sort_bool::and_(equal_to(vd, ve), less_equal(vs, vt)), less(vd, ve))));
883 2154 : result.push_back(data_equation(variable_list({vd}), in(s, vd, empty(s)), sort_bool::false_()));
884 4308 : result.push_back(data_equation(variable_list({vd, ve, vs}), in(s, vd, cons_(s, ve, vs)), sort_bool::or_(equal_to(vd, ve), in(s, vd, vs))));
885 1077 : result.push_back(data_equation(variable_list(), count(s, empty(s)), sort_nat::c0()));
886 3231 : result.push_back(data_equation(variable_list({vd, vs}), count(s, cons_(s, vd, vs)), sort_nat::cnat(sort_nat::succ(count(s, vs)))));
887 2154 : result.push_back(data_equation(variable_list({vd}), snoc(s, empty(s), vd), cons_(s, vd, empty(s))));
888 4308 : result.push_back(data_equation(variable_list({vd, ve, vs}), snoc(s, cons_(s, vd, vs), ve), cons_(s, vd, snoc(s, vs, ve))));
889 2154 : result.push_back(data_equation(variable_list({vs}), concat(s, empty(s), vs), vs));
890 4308 : result.push_back(data_equation(variable_list({vd, vs, vt}), concat(s, cons_(s, vd, vs), vt), cons_(s, vd, concat(s, vs, vt))));
891 2154 : result.push_back(data_equation(variable_list({vs}), concat(s, vs, empty(s)), vs));
892 3231 : result.push_back(data_equation(variable_list({vd, vs}), element_at(s, cons_(s, vd, vs), sort_nat::c0()), vd));
893 4308 : result.push_back(data_equation(variable_list({vd, vp, vs}), element_at(s, cons_(s, vd, vs), sort_nat::cnat(vp)), element_at(s, vs, sort_nat::pred(vp))));
894 3231 : result.push_back(data_equation(variable_list({vd, vs}), head(s, cons_(s, vd, vs)), vd));
895 3231 : result.push_back(data_equation(variable_list({vd, vs}), tail(s, cons_(s, vd, vs)), vs));
896 2154 : result.push_back(data_equation(variable_list({vd}), rhead(s, cons_(s, vd, empty(s))), vd));
897 4308 : result.push_back(data_equation(variable_list({vd, ve, vs}), rhead(s, cons_(s, vd, cons_(s, ve, vs))), rhead(s, cons_(s, ve, vs))));
898 2154 : result.push_back(data_equation(variable_list({vd}), rtail(s, cons_(s, vd, empty(s))), empty(s)));
899 4308 : result.push_back(data_equation(variable_list({vd, ve, vs}), rtail(s, cons_(s, vd, cons_(s, ve, vs))), cons_(s, vd, rtail(s, cons_(s, ve, vs)))));
900 2154 : return result;
901 1077 : }
902 :
903 : } // namespace sort_list
904 :
905 : } // namespace data
906 :
907 : } // namespace mcrl2
908 :
909 : #endif // MCRL2_DATA_LIST_H
|
