Line data Source code
1 : // Author(s): Jeroen van der Wulp
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_container_utility.h
10 : /// \brief Provides utilities for working with data expressions of standard container sorts
11 :
12 : #ifndef MCRL2_DATA_STANDARD_CONTAINER_UTILITY_H
13 : #define MCRL2_DATA_STANDARD_CONTAINER_UTILITY_H
14 :
15 : #include "mcrl2/utilities/detail/join.h"
16 : #include "mcrl2/data/bag.h"
17 : #include "mcrl2/data/list.h"
18 :
19 : namespace mcrl2
20 : {
21 :
22 : namespace data
23 : {
24 :
25 : namespace sort_list
26 : {
27 : /// \brief Constructs a list expression from a range of expressions
28 : //
29 : /// Type Sequence must be a model of the Forward Traversal Iterator concept;
30 : /// with value_type convertible to data_expression.
31 : /// \param[in] s the sort of list elements
32 : /// \param[in] range an iterator range of elements of sort s
33 : template < typename Sequence >
34 : inline
35 118 : application list(const sort_expression& s,
36 : Sequence const& range,
37 : typename atermpp::enable_if_container< Sequence, data_expression >::type* = nullptr)
38 : {
39 118 : data_expression list_expression(empty(s));
40 118 : std::vector< data_expression > elements(range.begin(), range.end());
41 :
42 368 : for (std::vector< data_expression >::reverse_iterator i = elements.rbegin(); i != elements.rend(); ++i)
43 : {
44 250 : list_expression = sort_list::cons_(s, *i, list_expression);
45 : }
46 :
47 236 : return static_cast< application >(list_expression);
48 118 : }
49 :
50 : /// \brief Generate identifier list_enumeration
51 : /// \return Identifier list_enumeration
52 : inline
53 56325 : core::identifier_string const& list_enumeration_name()
54 : {
55 56325 : static core::identifier_string list_enumeration_name = core::identifier_string("@ListEnum");
56 56325 : return list_enumeration_name;
57 : }
58 :
59 : /// \brief Constructor for function symbol list_enumeration
60 : /// \param s A sort expression
61 : /// \return Function symbol list_enumeration
62 : inline
63 246 : function_symbol list_enumeration(const sort_expression& s)
64 : {
65 246 : function_symbol list_enumeration(list_enumeration_name(), s);
66 246 : return list_enumeration;
67 : }
68 :
69 : /// \brief Recogniser for function list_enumeration
70 : /// \param e A data expression
71 : /// \return true iff e is the function symbol matching list_enumeration
72 : inline
73 31013 : bool is_list_enumeration_function_symbol(const atermpp::aterm_appl& e)
74 : {
75 31013 : if (is_function_symbol(e))
76 : {
77 29382 : return function_symbol(e).name() == list_enumeration_name();
78 : }
79 1631 : return false;
80 : }
81 :
82 : /// \brief Application of function symbol list_enumeration
83 : ///
84 : /// Type Sequence must be a model of the Forward Traversal Iterator concept;
85 : /// with value_type convertible to data_expression.
86 : /// \param s A sort expression
87 : /// \param range A range of data expressions
88 : /// \return Application of list_enum to the data expressions in range.
89 : template <typename Sequence>
90 : inline
91 1 : data_expression list_enumeration(const sort_expression& s,
92 : Sequence const& range,
93 : typename atermpp::enable_if_container< Sequence, data_expression >::type* = nullptr)
94 : {
95 1 : if (range.empty())
96 : {
97 0 : return list_enumeration(s);
98 : }
99 : else
100 : {
101 2 : sort_expression_vector v(range.size(), range.begin()->sort());
102 :
103 1 : return application(list_enumeration(function_sort(v,s)), range);
104 1 : }
105 : }
106 :
107 : /// \brief Application of function symbol list_enumeration
108 : /// \param s A sort expression
109 : /// \param range A range of data expressions
110 : /// \return Application of list_enum to the data expressions in range.
111 : inline
112 245 : data_expression list_enumeration(const sort_expression& s, data_expression_list const& range)
113 : {
114 245 : if (range.empty())
115 : {
116 0 : return list_enumeration(s);
117 : }
118 : else
119 : {
120 490 : sort_expression_vector v(range.size(), range.begin()->sort());
121 :
122 245 : return application(list_enumeration(function_sort(v,s)), range);
123 245 : }
124 : }
125 :
126 : /// \brief Recogniser for application of list_enumeration
127 : /// \param e A data expression
128 : /// \return true iff e is an application of function symbol
129 : /// list_enumeration to a number of arguments
130 : inline
131 31013 : bool is_list_enumeration_application(const atermpp::aterm_appl& e)
132 : {
133 31013 : if (is_application(e))
134 : {
135 31013 : return is_list_enumeration_function_symbol(application(e).head());
136 : }
137 0 : return false;
138 : }
139 : } // namespace sort_list
140 :
141 : namespace sort_set
142 : {
143 : /// \brief Generate identifier set_enumeration
144 : /// \return Identifier set_enumeration
145 : inline
146 35781 : core::identifier_string const& set_enumeration_name()
147 : {
148 35781 : static core::identifier_string set_enumeration_name = core::identifier_string("@SetEnum");
149 35781 : return set_enumeration_name;
150 : }
151 :
152 : /// \brief Constructor for function symbol set_enumeration
153 : /// \param s A sort expression
154 : /// \return Function symbol set_enumeration
155 : inline
156 393 : function_symbol set_enumeration(const sort_expression& s)
157 : {
158 393 : function_symbol set_enumeration(set_enumeration_name(), s);
159 393 : return set_enumeration;
160 : }
161 :
162 : /// \brief Recogniser for function set_enumeration
163 : /// \param e A data expression
164 : /// \return true iff e is the function symbol matching set_enumeration
165 : inline
166 9726 : bool is_set_enumeration_function_symbol(const atermpp::aterm_appl& e)
167 : {
168 9726 : if (is_function_symbol(e))
169 : {
170 8937 : return function_symbol(e).name() == set_enumeration_name();
171 : }
172 789 : return false;
173 : }
174 :
175 : /// \brief Application of function symbol set_enumeration
176 : ///
177 : /// Type Sequence must be a model of the Forward Traversal Iterator concept;
178 : /// with value_type convertible to data_expression.
179 : /// \param s A sort expression
180 : /// \param range A range of data expressions
181 : /// \return Application of set_enum to the data expressions in range.
182 : template <typename Sequence>
183 : inline
184 : data_expression set_enumeration(const sort_expression& s,
185 : Sequence const& range,
186 : typename atermpp::enable_if_container< Sequence, data_expression >::type* = 0)
187 : {
188 : if (range.empty())
189 : {
190 : return set_enumeration(sort_fset::fset(s));
191 : }
192 : else
193 : {
194 : sort_expression_vector v(range.size(), range.begin()->sort());
195 :
196 : return application(set_enumeration(function_sort(v,sort_fset::fset(s))), range);
197 : }
198 : }
199 :
200 : /// \brief Application of function symbol set_enumeration
201 : /// \param s A sort expression
202 : /// \param range A range of data expressions
203 : /// \return Application of set_enum to the data expressions in range.
204 : inline
205 393 : data_expression set_enumeration(const sort_expression& s,
206 : data_expression_list const& range)
207 : {
208 393 : if (range.empty())
209 : {
210 0 : return set_enumeration(sort_fset::fset(s));
211 : }
212 : else
213 : {
214 786 : sort_expression_vector v(range.size(), range.begin()->sort());
215 :
216 393 : return application(set_enumeration(function_sort(v,sort_fset::fset(s))), range);
217 393 : }
218 : }
219 :
220 : /// \brief Recogniser for application of set_enumeration
221 : /// \param e A data expression
222 : /// \return true iff e is an application of function symbol
223 : /// set_enumeration to a number of arguments
224 : inline
225 9726 : bool is_set_enumeration_application(const atermpp::aterm_appl& e)
226 : {
227 9726 : if (is_application(e))
228 : {
229 9726 : return is_set_enumeration_function_symbol(application(e).head());
230 : }
231 0 : return false;
232 : }
233 : } // namespace sort_set
234 :
235 : namespace sort_fset
236 : {
237 :
238 : /// \brief Constructs a finite set expression from a range of expressions
239 : //
240 : /// Type Sequence must be a model of the Forward Traversal Iterator concept;
241 : /// with value_type convertible to data_expression.
242 : /// \param[in] s the sort of list elements
243 : /// \param[in] range a sequence of elements
244 : template < typename Sequence >
245 : inline
246 193 : application fset(const sort_expression& s,
247 : Sequence const& range,
248 : typename atermpp::enable_if_container< Sequence, data_expression >::type* = nullptr)
249 : {
250 193 : data_expression fset_expression(sort_fset::empty(s));
251 :
252 : // We process the elements in reverse order to have a resulting enumeration
253 : // in the same order as the input
254 482 : for (typename Sequence::const_reverse_iterator i = range.rbegin(); i != range.rend(); ++i)
255 : {
256 289 : fset_expression = sort_fset::insert(s, *i, fset_expression);
257 : }
258 :
259 386 : return static_cast< application >(fset_expression);
260 193 : }
261 :
262 : /// \brief Constructs a finite set expression from a list of expressions
263 : //
264 : /// \param[in] s the sort of list elements
265 : /// \param[in] range a sequence of elements
266 : inline
267 193 : application fset(const sort_expression& s,
268 : const data_expression_list& range)
269 : {
270 386 : return fset(s, data_expression_vector(range.begin(),range.end()));
271 : }
272 :
273 : } // namespace sort_fset
274 :
275 : namespace sort_bag
276 : {
277 : /// \brief Generate identifier bag_enumeration
278 : /// \return Identifier bag_enumeration
279 : inline
280 35348 : core::identifier_string const& bag_enumeration_name()
281 : {
282 35348 : static core::identifier_string bag_enumeration_name = core::identifier_string("@BagEnum");
283 35348 : return bag_enumeration_name;
284 : }
285 :
286 : /// \brief Constructor for function symbol bag_enumeration
287 : /// \param s A sort expression
288 : /// \return Function symbol bag_enumeration
289 : inline
290 386 : function_symbol bag_enumeration(const sort_expression& s)
291 : {
292 386 : function_symbol bag_enumeration(bag_enumeration_name(), s);
293 386 : return bag_enumeration;
294 : }
295 :
296 : /// \brief Recogniser for function bag_enumeration
297 : /// \param e A data expression
298 : /// \return true iff e is the function symbol matching bag_enumeration
299 : inline
300 9712 : bool is_bag_enumeration_function_symbol(const atermpp::aterm_appl& e)
301 : {
302 9712 : if (is_function_symbol(e))
303 : {
304 8923 : return function_symbol(e).name() == bag_enumeration_name();
305 : }
306 789 : return false;
307 : }
308 :
309 : /// \brief Application of function symbol bag_enumeration
310 : ///
311 : /// Type Sequence must be a model of the Forward Traversal Iterator concept;
312 : /// with value_type convertible to data_expression.
313 : /// \param s A sort expression
314 : /// \param range A range of data expressions
315 : /// \return Application of bag_enum to the data expressions in range.
316 : template <typename Sequence>
317 : inline
318 : data_expression bag_enumeration(const sort_expression& s,
319 : Sequence const& range,
320 : typename atermpp::enable_if_container< Sequence, data_expression >::type* = 0)
321 : {
322 : if (range.empty())
323 : {
324 : return bag_enumeration(sort_fbag::fbag(s));
325 : }
326 : else
327 : {
328 : assert(range.size() % 2 == 0);
329 : sort_expression t(range.begin()->sort());
330 :
331 : sort_expression_vector v;
332 :
333 : for (std::size_t i = 0; i < range.size() / 2; ++i)
334 : {
335 : v.push_back(t);
336 : v.push_back(sort_nat::nat());
337 : }
338 :
339 : return application(bag_enumeration(function_sort(v,sort_fbag::fbag(s))), range);
340 : }
341 : }
342 :
343 : /// \brief Application of function symbol bag_enumeration
344 : /// \param s A sort expression
345 : /// \param range A range of data expressions
346 : /// \return Application of bag_enum to the data expressions in range.
347 : inline
348 386 : data_expression bag_enumeration(const sort_expression& s,
349 : data_expression_list const& range)
350 : {
351 386 : if (range.empty())
352 : {
353 0 : return bag_enumeration(sort_fbag::fbag(s));
354 : }
355 : else
356 : {
357 386 : assert(range.size() % 2 == 0);
358 386 : sort_expression t(range.begin()->sort());
359 386 : sort_expression_vector v;
360 :
361 918 : for (std::size_t i = 0; i < range.size() / 2; ++i)
362 : {
363 532 : v.push_back(t);
364 532 : v.push_back(sort_nat::nat());
365 : }
366 :
367 386 : return application(bag_enumeration(function_sort(v,sort_fbag::fbag(s))), range);
368 386 : }
369 : }
370 :
371 : /// \brief Recogniser for application of bag_enumeration
372 : /// \param e A data expression
373 : /// \return true iff e is an application of function symbol
374 : /// bag_enumeration to a number of arguments
375 : inline
376 9712 : bool is_bag_enumeration_application(const atermpp::aterm_appl& e)
377 : {
378 9712 : if (is_application(e))
379 : {
380 9712 : return is_bag_enumeration_function_symbol(application(e).head());
381 : }
382 0 : return false;
383 : }
384 :
385 : } // namespace sort_bag
386 :
387 : namespace sort_fbag
388 : {
389 : /// \brief Constructs a finite bag expression from a range of expressions
390 : /// Type Sequence must be a model of the Forward Traversal Iterator concept;
391 : /// with value_type convertible to data_expression.
392 : /// \pre range must contain element, count, element, count, ...
393 : /// \param[in] s the sort of list elements
394 : /// \param[in] range a range of elements of sort s.
395 : template < typename Sequence >
396 : inline
397 186 : application fbag(const sort_expression& s, Sequence const& range,
398 : typename atermpp::enable_if_container< Sequence, data_expression >::type* = nullptr)
399 : {
400 186 : data_expression fbag_expression(sort_fbag::empty(s));
401 :
402 : // The sequence contains element, count, ...
403 : // As we process the list in reverse, we have count, element, ...
404 : // We process the elements in reverse order to have a resulting enumeration
405 : // in the same order as the input
406 442 : for (typename Sequence::const_reverse_iterator i = range.rbegin(); i != range.rend(); ++i, ++i)
407 : {
408 256 : fbag_expression = sort_fbag::cinsert(s, *std::next(i, 1), *i, fbag_expression);
409 : }
410 :
411 372 : return static_cast< application >(fbag_expression);
412 186 : }
413 :
414 : /// \brief Constructs a finite bag expression from a list of expressions
415 : /// \pre range must contain element, count, element, count, ...
416 : /// \param[in] s the sort of list elements
417 : /// \param[in] range a range of elements of sort s.
418 : inline
419 186 : application fbag(const sort_expression& s, const data_expression_list& range)
420 : {
421 372 : return fbag(s, data_expression_vector(range.begin(),range.end()));
422 : }
423 : } // namespace sort_fbag
424 :
425 : } // namespace data
426 :
427 : } // namespace mcrl2
428 :
429 : #endif
430 :
|
