Line data Source code
1 : // Author(s): Jeroen Keiren, Jan Friso Groote
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/application.h
10 : /// \brief The class application.
11 :
12 : #ifndef MCRL2_DATA_VARIABLE_H
13 : #include "mcrl2/data/variable.h"
14 : #endif
15 :
16 : #ifndef MCRL2_DATA_APPLICATION_H
17 : #define MCRL2_DATA_APPLICATION_H
18 :
19 : namespace mcrl2
20 : {
21 :
22 : namespace data
23 : {
24 :
25 : namespace detail
26 : {
27 :
28 : // The class and the specialisation below are intended to
29 : // make the type of the term_appl_prepend_iterator a forward iterator,
30 : // unless it is based on an input iterator, in which case it should be an
31 : // input iterator.
32 : template <class IteratorTag>
33 : class prepend_iterator_tag_convertor
34 : {
35 : public:
36 : typedef std::forward_iterator_tag iterator_category;
37 : };
38 :
39 : template <>
40 : class prepend_iterator_tag_convertor<std::input_iterator_tag>
41 : {
42 : public:
43 : typedef std::input_iterator_tag iterator_category;
44 : };
45 :
46 : // Iterator for term_appl which prepends a data_expression to a list convertible to data_expressions.
47 : template <class Iterator >
48 : class term_appl_prepend_iterator
49 : {
50 : private:
51 : typedef std::iterator_traits<int*> traits;
52 :
53 : public:
54 : // The value_type.
55 : typedef data_expression value_type;
56 : // The reference type.
57 : typedef const data_expression& reference;
58 : // The pointer type.
59 : typedef const data_expression* pointer;
60 : // Difference type
61 : typedef ptrdiff_t difference_type;
62 : // The iterator category.
63 : // The iterator category is a forward_iterator, unless Iterator is an input iterator, in which case
64 : // it is an input iterator.
65 : typedef typename prepend_iterator_tag_convertor<traits::iterator_category>::iterator_category iterator_category;
66 :
67 : protected:
68 : Iterator m_it;
69 : pointer m_prepend;
70 :
71 : private:
72 : // Prevent the use of the following operators in this class, including the
73 : // postfix increment.
74 : reference operator[](difference_type n) const;
75 : term_appl_prepend_iterator operator++(int);
76 : term_appl_prepend_iterator& operator--();
77 : term_appl_prepend_iterator& operator--(int);
78 : term_appl_prepend_iterator& operator+=(difference_type n);
79 : term_appl_prepend_iterator& operator-=(difference_type n);
80 : term_appl_prepend_iterator operator+(difference_type n) const;
81 : term_appl_prepend_iterator operator-(difference_type n) const;
82 : difference_type operator-(const term_appl_prepend_iterator& other) const;
83 : difference_type distance_to(const term_appl_prepend_iterator& other) const;
84 :
85 : public:
86 : // Constructor.
87 21400844 : term_appl_prepend_iterator(Iterator it,
88 : pointer prepend=nullptr)
89 21400844 : : m_it(it), m_prepend(prepend)
90 21400844 : {}
91 :
92 : // The copy constructor.
93 87669280 : term_appl_prepend_iterator(const term_appl_prepend_iterator& other)
94 87669280 : : m_it(other.m_it),
95 87669280 : m_prepend(other.m_prepend)
96 : {
97 87669280 : }
98 :
99 : // The assignment operator.
100 : // other The term to be assigned.
101 : // Returns a reference to the assigned iterator.
102 : term_appl_prepend_iterator& operator=(const term_appl_prepend_iterator& other)
103 : {
104 : m_it=other.m_it;
105 : m_prepend=other.m_prepend;
106 : return *this;
107 : }
108 :
109 : // The dereference operator.
110 : // Return the dereferenced term.
111 32564544 : reference operator*() const
112 : {
113 32564544 : if (m_prepend)
114 : {
115 11734187 : return *m_prepend;
116 : }
117 20830357 : return *(this->m_it);
118 : }
119 :
120 : // Dereference the current iterator.
121 : pointer operator->() const
122 : {
123 : if (m_prepend)
124 : {
125 : return m_prepend;
126 : }
127 : return &*(this->m_it);
128 : }
129 :
130 : // Prefix increment.
131 : // Returns the iterator after it is incremented.
132 32393201 : term_appl_prepend_iterator& operator++()
133 : {
134 32393201 : if (m_prepend)
135 : {
136 11663194 : m_prepend = nullptr;
137 : }
138 : else
139 : {
140 20730007 : ++(this->m_it);
141 : }
142 32393201 : return *this;
143 : }
144 :
145 : // Equality of iterators.
146 44127388 : bool operator ==(const term_appl_prepend_iterator& other) const
147 : {
148 44127388 : return m_prepend==other.m_prepend && this->m_it==other.m_it;
149 : }
150 :
151 : // Inequality of iterators.
152 32564544 : bool operator !=(const term_appl_prepend_iterator& other) const
153 : {
154 32564544 : return !(*this==other);
155 : }
156 :
157 : // Comparison of iterators.
158 : bool operator <(const term_appl_prepend_iterator& other) const
159 : {
160 : return m_prepend < other.m_prepend || (m_prepend==other.m_prepend && this->m_it<other.m_it);
161 : }
162 :
163 : // Comparison of iterators.
164 : bool operator <=(const term_appl_prepend_iterator& other) const
165 : {
166 : return m_prepend < other.m_prepend || (m_prepend==other.m_prepend && this->m_it<=other.m_it);
167 : }
168 :
169 : // Comparison of iterators.
170 : bool operator >(const term_appl_prepend_iterator& other) const
171 : {
172 : return other<*this;
173 : }
174 :
175 : // Comparison of iterators.
176 : bool operator >=(const term_appl_prepend_iterator& other) const
177 : {
178 : return other<=*this;
179 : }
180 : };
181 :
182 : // The class below transforms a function that is to be applied to
183 : // the arguments of an application into a function that is not applied
184 : // to the head, and only applied to the arguments.
185 : template <class ArgumentConverter>
186 : class skip_function_application_to_head
187 : {
188 : protected:
189 : ArgumentConverter& m_f;
190 : std::size_t m_current_index;
191 : const bool m_skip_head;
192 : public:
193 792454 : skip_function_application_to_head(ArgumentConverter&f, const bool skip_head )
194 792454 : : m_f(f),
195 792454 : m_current_index(0),
196 792454 : m_skip_head(skip_head)
197 792454 : {}
198 :
199 2283527 : data_expression operator()(const data_expression& d)
200 : {
201 2283527 : if (m_skip_head && m_current_index++==0)
202 : {
203 0 : return d;
204 : }
205 2283527 : return m_f(d);
206 : }
207 : };
208 :
209 : // The class below transforms a function that is to be applied to
210 : // the arguments of an application into a function that is not applied
211 : // to the head, and only applied to the arguments.
212 : template <class ArgumentConverter>
213 : class skip_function_application_to_head_assignment
214 : {
215 : protected:
216 : ArgumentConverter& m_f;
217 : std::size_t m_current_index;
218 : const bool m_skip_head;
219 : public:
220 9045546 : skip_function_application_to_head_assignment(ArgumentConverter& f, const bool skip_head )
221 9045546 : : m_f(f),
222 9045546 : m_current_index(0),
223 9045546 : m_skip_head(skip_head)
224 9045546 : {}
225 :
226 25167148 : void operator()(data_expression& result, const data_expression& d)
227 : {
228 25167148 : if (m_skip_head && m_current_index++==0)
229 : {
230 0 : result=d;
231 0 : return;
232 : }
233 25167148 : m_f(result,d);
234 25167148 : return;
235 : }
236 : };
237 :
238 :
239 21359837 : inline bool contains_untyped_sort(const sort_expression& s)
240 : {
241 21359837 : if (is_untyped_sort(s))
242 : {
243 333642 : return true;
244 : }
245 21026195 : if (is_function_sort(s))
246 : {
247 10530815 : const function_sort& fs=atermpp::down_cast<function_sort>(s);
248 10530815 : if (contains_untyped_sort(fs.codomain()))
249 : {
250 10530815 : return true;
251 : }
252 0 : for(const sort_expression& sd: fs.domain())
253 : {
254 0 : if (contains_untyped_sort(sd))
255 : {
256 0 : return true;
257 : }
258 : }
259 : }
260 10495380 : if (is_container_sort(s))
261 : {
262 191360 : if (contains_untyped_sort(atermpp::down_cast<container_sort>(s).element_sort()))
263 : {
264 191360 : return true;
265 : }
266 : }
267 10304020 : assert(is_structured_sort(s) || is_basic_sort(s));
268 10304020 : return true;
269 : }
270 :
271 25822981 : inline const data_expression& evaluate_lambda_data_expression(const data_expression& t)
272 : {
273 25822981 : return t;
274 : }
275 :
276 : template <class TERM>
277 354996 : inline data_expression evaluate_lambda_data_expression(
278 : const TERM& t,
279 : typename std::enable_if<std::is_invocable_r<void, TERM, data_expression&>::value>::type* = nullptr)
280 : {
281 354996 : data_expression result;
282 354996 : t(result);
283 354996 : return result;
284 0 : }
285 :
286 : template <class TERM >
287 : inline data_expression evaluate_lambda_data_expression(
288 : const TERM& t,
289 : typename std::enable_if<std::is_invocable_r<const data_expression, TERM, void>::value>::type* = nullptr)
290 : {
291 : return t();
292 : }
293 :
294 : template <class HEAD, class CONTAINER>
295 10637662 : inline bool check_whether_sorts_match(const HEAD& head_lambda, const CONTAINER& l)
296 : {
297 10637662 : data_expression head = evaluate_lambda_data_expression(head_lambda);
298 10637662 : if (contains_untyped_sort(head.sort()))
299 : {
300 : // Most likely head is a just parsed, untyped object.
301 10637662 : return true;
302 : }
303 0 : function_sort fs(head.sort());
304 0 : if ((fs.domain().size()==1 && contains_untyped_sort(fs.domain().front())) ||
305 0 : (l.size()==1 && contains_untyped_sort(l.front().sort())))
306 : {
307 : // This is most likely an application from or to an Rewritten@@term, used in the jitty rewriter
308 : // to indicate that a term is in normal form.
309 0 : return true;
310 : }
311 : // Check that the sorts of the function domain of the head matches those of the arguments.
312 0 : if (fs.domain().size()!=l.size())
313 : {
314 0 : return false;
315 : }
316 0 : typename CONTAINER::const_iterator i=l.begin();
317 0 : for(const sort_expression& s: fs.domain())
318 : {
319 0 : if (!contains_untyped_sort(i->sort()) && s!=i->sort())
320 : {
321 0 : return false;
322 : }
323 0 : ++i;
324 : }
325 0 : return true;
326 10637662 : }
327 :
328 8982786 : inline data_expression_list get_arguments()
329 : {
330 8982786 : return data_expression_list();
331 : }
332 :
333 : template <class HEAD, class... ARGUMENTS>
334 : inline
335 15540315 : data_expression_list get_arguments(const HEAD& h, const ARGUMENTS&... args)
336 : {
337 15540315 : data_expression_list result=get_arguments(args...);
338 15540315 : result.push_front(evaluate_lambda_data_expression(h));
339 15540315 : return result;
340 0 : }
341 :
342 : /* template <class HEAD, class... CONTAINER>
343 : inline bool check_whether_sorts_match(const HEAD& head_lambda, const CONTAINER&... l)
344 : {
345 : data_expression_list arguments=get_arguments(l...);
346 : return check_whether_sorts_match(head_lambda, arguments);
347 : } */
348 :
349 : } // namespace detail
350 :
351 : /// \brief An application of a data expression to a number of arguments
352 : class application: public data_expression
353 : {
354 : public:
355 : /// \brief Default constructor.
356 2 : application()
357 2 : : data_expression(atermpp::term_appl<aterm>(core::detail::function_symbol_DataAppl(0)))
358 2 : {}
359 :
360 : /// \brief Constructor.
361 : template<typename ...Terms,
362 : typename = std::enable_if_t<std::conjunction_v<std::is_convertible<Terms, data_expression>...>> >
363 8647599 : application(const data_expression& head,
364 : const data_expression& arg1,
365 : const Terms& ...other_arguments
366 : )
367 17295198 : : data_expression(atermpp::term_appl<aterm>(
368 17295198 : core::detail::function_symbol_DataAppl(sizeof...(Terms)+2),head,arg1,other_arguments...))
369 : {
370 8647599 : assert(detail::check_whether_sorts_match(head, detail::get_arguments(arg1, other_arguments...)));
371 8647599 : }
372 :
373 : /// \brief Constructor.
374 : /// \param term A term
375 42530883 : explicit application(const atermpp::aterm& term)
376 42530883 : : data_expression(term)
377 : {
378 42530883 : assert(core::detail::check_term_DataAppl(*this));
379 42530883 : }
380 :
381 : /// \brief Constructor.
382 : template <typename Container>
383 37119 : application(const data_expression& head,
384 : const Container& arguments,
385 : typename atermpp::enable_if_container<Container, data_expression>::type* = nullptr)
386 74238 : : data_expression(atermpp::term_appl<aterm>(core::detail::function_symbol_DataAppl(arguments.size() + 1),
387 37119 : detail::term_appl_prepend_iterator<typename Container::const_iterator>(arguments.begin(), &head),
388 74238 : detail::term_appl_prepend_iterator<typename Container::const_iterator>(arguments.end())))
389 : {
390 37119 : assert(arguments.size()>0);
391 37119 : assert(detail::check_whether_sorts_match(head,arguments));
392 37119 : }
393 :
394 : private:
395 : // forbid the use of iterator, which is silently inherited from
396 : // aterm_appl. Modifying the arguments of an application through the iterator
397 : // is not allowed!
398 : typedef data_expression::iterator iterator;
399 :
400 : public:
401 :
402 : /// \brief An iterator to traverse the arguments of an application.
403 : /// \details There is a subtle difference with the arguments of an iterator on
404 : /// the arguments of an aterm_appl from which an application is derived.
405 : /// As an application has a head as its first argument, the iterator
406 : /// of the aterm_appl starts at this head, where the iterator of the
407 : /// application starts at the first argument. This also means that
408 : /// t[n] for t an application is equal to t[n+1] if t is interpreted as an
409 : /// aterm_appl.
410 : typedef atermpp::term_appl_iterator<data_expression> const_iterator;
411 :
412 : /// \brief Constructor.
413 : template <typename FwdIter>
414 49635 : application(const data_expression& head,
415 : FwdIter first,
416 : FwdIter last,
417 : typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = nullptr)
418 99270 : : data_expression(atermpp::term_appl<aterm>(core::detail::function_symbol_DataAppl(std::distance(first, last) + 1),
419 49635 : detail::term_appl_prepend_iterator<FwdIter>(first, &head),
420 99270 : detail::term_appl_prepend_iterator<FwdIter>(last)))
421 : {
422 49635 : assert(first!=last);
423 49635 : assert(detail::check_whether_sorts_match(head,data_expression_list(begin(), end())));
424 49635 : }
425 :
426 : /// \brief Constructor.
427 : template <typename FwdIter>
428 : application(const std::size_t arity,
429 : const data_expression& head,
430 : FwdIter first,
431 : FwdIter last,
432 : typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = 0)
433 : : data_expression(atermpp::term_appl<aterm>(core::detail::function_symbol_DataAppl(arity + 1),
434 : detail::term_appl_prepend_iterator<FwdIter>(first, &head),
435 : detail::term_appl_prepend_iterator<FwdIter>(last)))
436 : {
437 : assert(arity>0);
438 : assert(std::distance(first, last)==arity);
439 : assert(detail::check_whether_sorts_match(head,data_expression_list(begin(), end())));
440 : }
441 :
442 :
443 : /// \brief Constructor.
444 : /// \details Construct at term head(arg_first,...,arg_last) where convert_arguments
445 : /// has been applied to the head and all the arguments.
446 : /// \parameter head This is the new head for the application.
447 : /// \parameter first This is a forward iterator yielding the first argument.
448 : /// \parameter last This is an iterator beyond the last argument.
449 : /// \parameter convert_arguments This is a function applied to optionally the head and the arguments.
450 : /// \parameter skip_first_argument A boolean which is true if the function must not be applied to the head.
451 : template <typename FwdIter, class ArgumentConverter>
452 792454 : application(const data_expression& head,
453 : FwdIter first,
454 : FwdIter last,
455 : ArgumentConverter convert_arguments,
456 : const bool skip_first_argument=false,
457 : typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = nullptr,
458 : typename std::enable_if< !std::is_base_of<data_expression, ArgumentConverter>::value>::type* = nullptr )
459 : // typename std::enable_if< std::is_convertible<typename std::invoke_result<ArgumentConverter,typename FwdIter::value_type>::type, data_expression>::value>::type* = nullptr)
460 1584908 : : data_expression(atermpp::term_appl<aterm>(
461 792454 : core::detail::function_symbol_DataAppl(std::distance(first, last) + 1),
462 792454 : detail::term_appl_prepend_iterator<FwdIter>(first, &head),
463 792454 : detail::term_appl_prepend_iterator<FwdIter>(last),
464 1584908 : detail::skip_function_application_to_head(convert_arguments,skip_first_argument)))
465 : {
466 792454 : assert(first!=last);
467 792454 : assert(detail::check_whether_sorts_match(head,data_expression_list(begin(), end())));
468 792454 : }
469 :
470 : /// \brief Constructor.
471 : /// \details Construct at term head(arg_first,...,arg_last) where convert_arguments
472 : /// has been applied to the head and all the arguments.
473 : /// \parameter head This is the new head for the application.
474 : /// \parameter first This is a forward iterator yielding the first argument.
475 : /// \parameter last This is an iterator beyond the last argument.
476 : /// \parameter convert_arguments This is a function applied to optionally the head and the arguments.
477 : /// \parameter skip_first_argument A boolean which is true if the function must not be applied to the head.
478 : template <typename FwdIter, class ArgumentConverter>
479 : application(const data_expression& head,
480 : FwdIter first,
481 : FwdIter last,
482 : ArgumentConverter convert_arguments,
483 : const bool skip_first_argument=false,
484 : typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = nullptr,
485 : typename std::enable_if< !std::is_base_of<data_expression, ArgumentConverter>::value>::type* = nullptr,
486 : typename std::enable_if<std::is_same<typename std::invoke_result<ArgumentConverter,data_expression&,typename FwdIter::value_type>::type, void>::value>::type* = nullptr)
487 :
488 : : data_expression(atermpp::term_appl<aterm>(
489 : core::detail::function_symbol_DataAppl(std::distance(first, last) + 1),
490 : detail::term_appl_prepend_iterator<FwdIter>(first, &head),
491 : detail::term_appl_prepend_iterator<FwdIter>(last),
492 : detail::skip_function_application_to_head_assignment(convert_arguments,skip_first_argument)))
493 : {
494 : assert(first!=last);
495 : assert(detail::check_whether_sorts_match(head,data_expression_list(begin(), end())));
496 : }
497 :
498 : /// Move semantics
499 14 : application(const application&) noexcept = default;
500 1 : application(application&&) noexcept = default;
501 1 : application& operator=(const application&) noexcept = default;
502 45 : application& operator=(application&&) noexcept = default;
503 :
504 : /// \brief Get the function at the head of this expression.
505 43570395 : const data_expression& head() const
506 : {
507 43570395 : return atermpp::down_cast<data_expression>(atermpp::aterm_appl::operator[](0));
508 : }
509 :
510 : /// \brief Get the i-th argument of this expression.
511 11212445 : const data_expression& operator[](std::size_t index) const
512 : {
513 11212445 : assert(index<size());
514 11212445 : return atermpp::down_cast<data_expression>(atermpp::aterm_appl::operator[](index+1));
515 : }
516 :
517 : /// \brief Returns an iterator pointing to the first argument of the
518 : /// application.
519 18868302 : const_iterator begin() const
520 : {
521 37736604 : return atermpp::detail::aterm_appl_iterator_cast<data_expression>(atermpp::aterm_appl::begin()+1);
522 : }
523 :
524 : /// \brief Returns an iterator pointing past the last argument of the
525 : /// application.
526 18895100 : const_iterator end() const
527 : {
528 37790200 : return atermpp::detail::aterm_appl_iterator_cast<data_expression>(atermpp::aterm_appl::end());
529 : }
530 :
531 : /// \return The number of arguments of this application.
532 27636808 : std::size_t size() const
533 : {
534 27636808 : return atermpp::aterm_appl::size() - 1;
535 : }
536 : };
537 :
538 : /// \brief swap overload
539 : inline void swap(application& t1, application& t2)
540 : {
541 : t1.swap(t2);
542 : }
543 :
544 : /// \brief Make function for an application.
545 : /// \param result variable into which the application is constructed.
546 : inline void make_application(atermpp::aterm& result)
547 : {
548 : atermpp::make_term_appl(result,core::detail::function_symbol_DataAppl(1));
549 : }
550 :
551 : /*
552 : // ---------------------------------------------------------------------------------
553 : // ---------------------------- TYPEDEF --------------------------------------------
554 : // ---------------------------------------------------------------------------------
555 : template <typename TERM, typename = void>
556 : struct yields_a_data_expression
557 : : public std::false_type
558 : {
559 : };
560 :
561 : template <typename TERM>
562 : struct yields_a_data_expression<TERM,
563 : typename std::enable_if<std::is_convertible<TERM, data_expression>::type>::type >
564 : : public std::true_type
565 : {}; */
566 :
567 : /// \brief Constructor.
568 : /// \param result variable into which the application is constructed.
569 : template<typename HEAD, typename TERM, typename ...Terms,
570 : typename = std::enable_if_t<
571 : std::disjunction<typename std::is_convertible<HEAD, data_expression>,
572 : typename std::is_invocable_r<void, HEAD, data_expression&>,
573 : typename std::is_invocable_r<const data_expression, HEAD, void> >::value >,
574 : typename = std::enable_if_t<std::conjunction_v<
575 : std::disjunction<typename std::is_convertible<Terms, data_expression>,
576 : typename std::is_invocable_r<void, Terms, data_expression&>,
577 : typename std::is_invocable_r<const data_expression, Terms, void> > ...>> >
578 335187 : inline void make_application(
579 : atermpp::aterm& result,
580 : const HEAD& head,
581 : const TERM& arg1,
582 : const Terms& ...other_arguments
583 : )
584 : {
585 335187 : assert(detail::check_whether_sorts_match(head, detail::get_arguments(arg1, other_arguments...)));
586 335187 : atermpp::make_term_appl(result,
587 : core::detail::function_symbol_DataAppl(sizeof...(Terms)+2),
588 : head,
589 : arg1,
590 : other_arguments...);
591 335187 : }
592 :
593 : /// \brief Constructor.
594 : /// \param result variable into which the application is constructed.
595 : template <typename Container>
596 : inline void make_application(data_expression& result,
597 : const data_expression& head,
598 : const Container& arguments,
599 : typename atermpp::enable_if_container<Container, data_expression>::type* = nullptr)
600 : {
601 : assert(arguments.size()>0);
602 : assert(detail::check_whether_sorts_match(head,arguments));
603 : atermpp::make_term_appl(result,
604 : core::detail::function_symbol_DataAppl(arguments.size() + 1),
605 : detail::term_appl_prepend_iterator<typename Container::const_iterator>(arguments.begin(), &head),
606 : detail::term_appl_prepend_iterator<typename Container::const_iterator>(arguments.end()));
607 : }
608 :
609 : /// \brief Constructor.
610 : /// \param result variable into which the application is constructed.
611 : template <typename FwdIter>
612 775668 : inline void make_application(atermpp::aterm& result,
613 : const data_expression& head,
614 : FwdIter first,
615 : FwdIter last,
616 : typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = nullptr)
617 : {
618 775668 : assert(first!=last);
619 775668 : atermpp::make_term_appl(result,
620 775668 : core::detail::function_symbol_DataAppl(std::distance(first, last) + 1),
621 775668 : detail::term_appl_prepend_iterator<FwdIter>(first, &head),
622 775668 : detail::term_appl_prepend_iterator<FwdIter>(last));
623 775668 : assert(detail::check_whether_sorts_match(head,data_expression_list(
624 : atermpp::down_cast<application>(result).begin(),
625 : atermpp::down_cast<application>(result).end())));
626 775668 : }
627 :
628 : /// \brief Constructor.
629 : /// \param result variable into which the application is constructed.
630 : template <typename FwdIter>
631 : inline void make_application(atermpp::aterm& result,
632 : const std::size_t arity,
633 : const data_expression& head,
634 : FwdIter first,
635 : FwdIter last,
636 : typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = 0)
637 : {
638 : assert(arity>0);
639 : assert(std::distance(first, last)==arity);
640 : atermpp::make_term_appl(result,
641 : core::detail::function_symbol_DataAppl(arity + 1),
642 : detail::term_appl_prepend_iterator<FwdIter>(first, &head),
643 : detail::term_appl_prepend_iterator<FwdIter>(last));
644 : assert(detail::check_whether_sorts_match(head,data_expression_list(
645 : atermpp::down_cast<application>(result).begin(),
646 : atermpp::down_cast<application>(result).end())));
647 : }
648 :
649 :
650 : /// \brief Constructor.
651 : /// \details Construct at term head(arg_first,...,arg_last) where convert_arguments
652 : /// has been applied to the head and all the arguments.
653 : /// \param result variable into which the application is constructed.
654 : /// \parameter head This is the new head for the application.
655 : /// \parameter first This is a forward iterator yielding the first argument.
656 : /// \parameter last This is an iterator beyond the last argument.
657 : /// \parameter convert_arguments This is a function applied to optionally the head and the arguments.
658 : /// \parameter skip_first_argument A boolean which is true if the function must not be applied to the head.
659 : template <typename FwdIter, class ArgumentConverter>
660 0 : inline void make_application(atermpp::aterm& result,
661 : const data_expression& head,
662 : FwdIter first,
663 : FwdIter last,
664 : ArgumentConverter convert_arguments,
665 : const bool skip_first_argument=false,
666 : typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = nullptr,
667 : typename std::enable_if< !std::is_base_of<data_expression, ArgumentConverter>::value>::type* = nullptr,
668 : typename std::enable_if< std::is_same<typename std::invoke_result<ArgumentConverter,typename FwdIter::value_type>::type, data_expression>::value>::type* = nullptr)
669 : {
670 0 : assert(first!=last);
671 0 : atermpp::make_term_appl(result,
672 0 : core::detail::function_symbol_DataAppl(std::distance(first, last) + 1),
673 0 : detail::term_appl_prepend_iterator<FwdIter>(first, &head),
674 0 : detail::term_appl_prepend_iterator<FwdIter>(last),
675 : detail::skip_function_application_to_head(convert_arguments,skip_first_argument));
676 0 : assert(detail::check_whether_sorts_match(head,data_expression_list(
677 : atermpp::down_cast<application>(result).begin(),
678 : atermpp::down_cast<application>(result).end())));
679 0 : }
680 :
681 : /// \brief Constructor.
682 : /// \details Construct at term head(arg_first,...,arg_last) where convert_arguments
683 : /// has been applied to the head and all the arguments.
684 : /// \param result variable into which the application is constructed.
685 : /// \parameter head This is the new head for the application.
686 : /// \parameter first This is a forward iterator yielding the first argument.
687 : /// \parameter last This is an iterator beyond the last argument.
688 : /// \parameter convert_arguments This is a function applied to optionally the head and the arguments.
689 : /// \parameter skip_first_argument A boolean which is true if the function must not be applied to the head.
690 : template <typename FwdIter, class ArgumentConverter>
691 9045546 : static inline void make_application(
692 : atermpp::aterm& result,
693 : const data_expression& head,
694 : FwdIter first,
695 : FwdIter last,
696 : ArgumentConverter convert_arguments,
697 : const bool skip_first_argument=false,
698 : typename std::enable_if< !std::is_base_of<data_expression, FwdIter>::value>::type* = nullptr,
699 : typename std::enable_if< !std::is_base_of<data_expression, ArgumentConverter>::value>::type* = nullptr,
700 : typename std::enable_if<std::is_same<typename std::invoke_result<ArgumentConverter,data_expression&,typename FwdIter::value_type>::type, void>::value>::type* = nullptr)
701 : {
702 18091092 : atermpp::make_term_appl(
703 : result,
704 9045546 : core::detail::function_symbol_DataAppl(std::distance(first, last) + 1),
705 9045546 : detail::term_appl_prepend_iterator<FwdIter>(first, &head),
706 9045546 : detail::term_appl_prepend_iterator<FwdIter>(last),
707 : detail::skip_function_application_to_head_assignment(convert_arguments,skip_first_argument));
708 9045546 : }
709 :
710 :
711 : //--- start generated class application ---//
712 : // prototype declaration
713 : std::string pp(const application& x);
714 :
715 : /// \\brief Outputs the object to a stream
716 : /// \\param out An output stream
717 : /// \\param x Object x
718 : /// \\return The output stream
719 : inline
720 2 : std::ostream& operator<<(std::ostream& out, const application& x)
721 : {
722 2 : return out << data::pp(x);
723 : }
724 : //--- end generated class application ---//
725 :
726 : inline
727 0 : const data_expression& unary_operand(const application& x)
728 : {
729 0 : return x[0];
730 : }
731 :
732 : inline
733 418351 : const data_expression& binary_left(const application& x)
734 : {
735 418351 : return x[0];
736 : }
737 :
738 : inline
739 329533 : const data_expression& binary_right(const application& x)
740 : {
741 329533 : return x[1];
742 : }
743 :
744 : inline
745 41 : const data_expression& unary_operand1(const data_expression& x)
746 : {
747 41 : const application& y = atermpp::down_cast<application>(x);
748 41 : return y[0];
749 : }
750 :
751 : inline
752 154 : const data_expression& binary_left1(const data_expression& x)
753 : {
754 154 : const application& y = atermpp::down_cast<application>(x);
755 154 : return y[0];
756 : }
757 :
758 : inline
759 154 : const data_expression& binary_right1(const data_expression & x)
760 : {
761 154 : const application& y = atermpp::down_cast<application>(x);
762 154 : return y[1];
763 : }
764 :
765 : } // namespace data
766 :
767 : } // namespace mcrl2
768 :
769 : #endif // MCRL2_DATA_APPLICATION_H
|
