Line data Source code
1 : // Author(s): Jeroen Keiren, Jeroen van der Wulp, 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 :
10 : #include "mcrl2/core/load_aterm.h"
11 : #include "mcrl2/data/data_specification.h"
12 : #include "mcrl2/data/detail/data_utility.h"
13 : #include "mcrl2/data/detail/io.h"
14 : #include "mcrl2/data/replace.h"
15 : #include "mcrl2/data/substitutions/sort_expression_assignment.h"
16 :
17 : // Predefined datatypes
18 : #include "mcrl2/data/function_update.h"
19 : #include "mcrl2/data/list.h"
20 :
21 : namespace mcrl2
22 : {
23 : namespace data
24 : {
25 :
26 : class finiteness_helper
27 : {
28 : protected:
29 :
30 : const data_specification& m_specification;
31 : std::set< sort_expression > m_visiting;
32 :
33 1991 : bool is_finite_aux(const sort_expression& s)
34 : {
35 1991 : const function_symbol_vector& constructors=m_specification.constructors(s);
36 1991 : if (constructors.empty())
37 : {
38 7 : return false;
39 : }
40 :
41 5196 : for(const function_symbol& f: constructors)
42 : {
43 3969 : if (is_function_sort(f.sort()))
44 : {
45 763 : const function_sort& f_sort=atermpp::down_cast<function_sort>(f.sort());
46 763 : const sort_expression_list& l=f_sort.domain();
47 :
48 1158 : for(const sort_expression& e: l)
49 : {
50 1152 : if (!is_finite(e))
51 : {
52 757 : return false;
53 : }
54 : }
55 : }
56 : }
57 1227 : return true;
58 : }
59 :
60 : public:
61 :
62 1169 : finiteness_helper(const data_specification& specification) : m_specification(specification)
63 1169 : { }
64 :
65 2518 : bool is_finite(const sort_expression& s)
66 : {
67 2518 : assert(s==normalize_sorts(s,m_specification));
68 2518 : if (m_visiting.count(s)>0)
69 : {
70 396 : return false;
71 : }
72 :
73 2122 : m_visiting.insert(s);
74 :
75 2122 : bool result=false;
76 2122 : if (is_basic_sort(s))
77 : {
78 1991 : result=is_finite(basic_sort(s));
79 : }
80 131 : else if (is_container_sort(s))
81 : {
82 51 : result=is_finite(container_sort(s));
83 : }
84 80 : else if (is_function_sort(s))
85 : {
86 80 : result=is_finite(function_sort(s));
87 : }
88 0 : else if (is_structured_sort(s))
89 : {
90 0 : result=is_finite(structured_sort(s));
91 : }
92 :
93 2122 : m_visiting.erase(s);
94 2122 : return result;
95 : }
96 :
97 1991 : bool is_finite(const basic_sort& s)
98 : {
99 1991 : return is_finite_aux(s);
100 : }
101 :
102 80 : bool is_finite(const function_sort& s)
103 : {
104 182 : for(const sort_expression& sort: s.domain())
105 : {
106 105 : if (!is_finite(sort))
107 : {
108 3 : return false;
109 : }
110 : }
111 :
112 77 : return is_finite(s.codomain());
113 : }
114 :
115 51 : bool is_finite(const container_sort& s)
116 : {
117 51 : return (s.container_name() == set_container()) ? is_finite(s.element_sort()) : false;
118 : }
119 :
120 : bool is_finite(const alias&)
121 : {
122 : assert(0);
123 : return false;
124 : }
125 :
126 0 : bool is_finite(const structured_sort& s)
127 : {
128 0 : return is_finite_aux(s);
129 : }
130 : };
131 :
132 : /// \brief Checks whether a sort is certainly finite.
133 : ///
134 : /// \param[in] s A sort expression
135 : /// \return true if s can be determined to be finite,
136 : /// false otherwise.
137 1169 : bool data_specification::is_certainly_finite(const sort_expression& s) const
138 : {
139 1169 : const bool result=finiteness_helper(*this).is_finite(s);
140 1169 : return result;
141 : }
142 :
143 :
144 : // The function below checks whether there is an alias loop, e.g. aliases
145 : // of the form A=B; B=A; or more complex A=B->C; B=Set(D); D=List(A); Loops
146 : // through structured sorts are allowed. If a loop is detected, an exception
147 : // is thrown.
148 10081 : void sort_specification::check_for_alias_loop(
149 : const sort_expression& s,
150 : std::set<sort_expression> sorts_already_seen,
151 : const bool toplevel) const
152 : {
153 10081 : if (is_basic_sort(s))
154 : {
155 5516 : if (sorts_already_seen.count(s)>0)
156 : {
157 6 : throw mcrl2::runtime_error("Sort alias " + pp(s) + " is defined in terms of itself.");
158 : }
159 11572 : for(const alias& a: m_user_defined_aliases)
160 : {
161 10934 : if (a.name() == s)
162 : {
163 4872 : sorts_already_seen.insert(s);
164 4881 : check_for_alias_loop(a.reference(), sorts_already_seen, true);
165 4863 : sorts_already_seen.erase(s);
166 4863 : return;
167 : }
168 : }
169 638 : return;
170 : }
171 :
172 4565 : if (is_container_sort(s))
173 : {
174 405 : check_for_alias_loop(container_sort(s).element_sort(),sorts_already_seen,false);
175 399 : return;
176 : }
177 :
178 4164 : if (is_function_sort(s))
179 : {
180 152 : sort_expression_list s_domain(function_sort(s).domain());
181 303 : for(const sort_expression& sort: s_domain)
182 : {
183 153 : check_for_alias_loop(sort,sorts_already_seen,false);
184 : }
185 :
186 153 : check_for_alias_loop(function_sort(s).codomain(),sorts_already_seen,false);
187 150 : return;
188 152 : }
189 :
190 : // A sort declaration with a struct on toplevel can be recursive. Otherwise a
191 : // check needs to be made.
192 4012 : if (is_structured_sort(s) && !toplevel)
193 : {
194 5 : const structured_sort ss(s);
195 5 : structured_sort_constructor_list constructors=ss.constructors();
196 11 : for(const structured_sort_constructor& constructor: constructors)
197 : {
198 8 : structured_sort_constructor_argument_list ssca=constructor.arguments();
199 11 : for(const structured_sort_constructor_argument& a: ssca)
200 : {
201 7 : check_for_alias_loop(a.sort(),sorts_already_seen,false);
202 : }
203 8 : }
204 7 : }
205 :
206 : }
207 :
208 :
209 : // This function returns the normal form of e, under the the map map1.
210 : // This normal form is obtained by repeatedly applying map1, until this
211 : // is not possible anymore. It is assumed that this procedure terminates. There is
212 : // no check for loops.
213 17202 : static sort_expression find_normal_form(
214 : const sort_expression& e,
215 : const std::multimap< sort_expression, sort_expression >& map1,
216 : std::set < sort_expression > sorts_already_seen = std::set < sort_expression >())
217 : {
218 17202 : assert(sorts_already_seen.find(e)==sorts_already_seen.end()); // e has not been seen already.
219 17202 : assert(!is_untyped_sort(e));
220 17202 : assert(!is_untyped_possible_sorts(e));
221 :
222 17202 : if (is_function_sort(e))
223 : {
224 239 : const function_sort fs(e);
225 : const sort_expression normalised_codomain=
226 239 : find_normal_form(fs.codomain(),map1,sorts_already_seen);
227 239 : const sort_expression_list& domain=fs.domain();
228 239 : sort_expression_list normalised_domain;
229 478 : for(const sort_expression& s: domain)
230 : {
231 239 : normalised_domain.push_front(find_normal_form(s,map1,sorts_already_seen));
232 : }
233 239 : return function_sort(reverse(normalised_domain),normalised_codomain);
234 239 : }
235 :
236 16963 : if (is_container_sort(e))
237 : {
238 558 : const container_sort cs(e);
239 558 : return container_sort(cs.container_name(),find_normal_form(cs.element_sort(),map1,sorts_already_seen));
240 558 : }
241 :
242 16405 : sort_expression result_sort;
243 :
244 16405 : if (is_structured_sort(e))
245 : {
246 3785 : const structured_sort ss(e);
247 3785 : structured_sort_constructor_list constructors=ss.constructors();
248 3785 : structured_sort_constructor_list normalised_constructors;
249 11175 : for(const structured_sort_constructor& constructor: constructors)
250 : {
251 7390 : structured_sort_constructor_argument_list normalised_ssa;
252 10792 : for(const structured_sort_constructor_argument& a: constructor.arguments())
253 : {
254 3402 : normalised_ssa.push_front(structured_sort_constructor_argument(a.name(),
255 6804 : find_normal_form(a.sort(),map1,sorts_already_seen)));
256 : }
257 :
258 7390 : normalised_constructors.push_front(
259 14780 : structured_sort_constructor(
260 7390 : constructor.name(),
261 14780 : reverse(normalised_ssa),
262 7390 : constructor.recogniser()));
263 :
264 7390 : }
265 3785 : result_sort=structured_sort(reverse(normalised_constructors));
266 3785 : }
267 :
268 16405 : if (is_basic_sort(e))
269 : {
270 12620 : result_sort=e;
271 : }
272 :
273 :
274 16405 : assert(is_basic_sort(result_sort) || is_structured_sort(result_sort));
275 16405 : const std::multimap< sort_expression, sort_expression >::const_iterator i1=map1.find(result_sort);
276 16405 : if (i1!=map1.end()) // found
277 : {
278 : #ifndef NDEBUG
279 772 : sorts_already_seen.insert(result_sort);
280 : #endif
281 772 : return find_normal_form(i1->second,map1,sorts_already_seen);
282 : }
283 15633 : return result_sort;
284 16405 : }
285 :
286 30852 : void sort_specification::add_predefined_basic_sorts()
287 : {
288 30852 : add_system_defined_sort(sort_bool::bool_());
289 30852 : add_system_defined_sort(sort_pos::pos());
290 30852 : }
291 :
292 142070 : void sort_specification::import_system_defined_sort(const sort_expression& sort)
293 : {
294 142070 : if (is_untyped_sort(sort) || is_untyped_possible_sorts(sort))
295 : {
296 102 : mCRL2log(mcrl2::log::debug) << "Erroneous attempt to insert an untyped sort into the a sort specification\n";
297 102 : return;
298 : }
299 : // Add an element, and stop if it was already added.
300 141968 : if (!m_sorts_in_context.insert(sort).second)
301 : {
302 60405 : return;
303 : }
304 :
305 81563 : sorts_are_not_necessarily_normalised_anymore();
306 : // add the sorts on which this sorts depends.
307 81563 : if (sort == sort_real::real_())
308 : {
309 : // Int is required as the rewrite rules of Real rely on it.
310 973 : import_system_defined_sort(sort_int::int_());
311 : }
312 80590 : else if (sort == sort_int::int_())
313 : {
314 : // See above, Int requires Nat.
315 1029 : import_system_defined_sort(sort_nat::nat());
316 : }
317 79561 : else if (sort == sort_nat::nat())
318 : {
319 : // Nat requires NatPair.
320 1996 : import_system_defined_sort(sort_nat::natpair());
321 : }
322 77565 : else if (is_function_sort(sort))
323 : {
324 9286 : const function_sort& fsort=atermpp::down_cast<function_sort>(sort);
325 9286 : import_system_defined_sorts(fsort.domain());
326 9286 : import_system_defined_sort(fsort.codomain());
327 : }
328 68279 : else if (is_container_sort(sort))
329 : {
330 717 : const sort_expression element_sort(container_sort(sort).element_sort());
331 : // Import the element sort (which may be a complex sort also).
332 717 : import_system_defined_sort(element_sort);
333 717 : if (sort_list::is_list(sort))
334 : {
335 348 : import_system_defined_sort(sort_nat::nat()); // Required for lists.
336 : }
337 369 : else if (sort_set::is_set(sort))
338 : {
339 141 : import_system_defined_sort(sort_fset::fset(element_sort));
340 : // Import the functions from element_sort->Bool.
341 141 : sort_expression_list element_sorts;
342 141 : element_sorts.push_front(element_sort);
343 141 : import_system_defined_sort(function_sort(element_sorts,sort_bool::bool_()));
344 141 : }
345 228 : else if (sort_fset::is_fset(sort))
346 : {
347 : }
348 63 : else if (sort_bag::is_bag(sort))
349 : {
350 : // Add the sorts Nat and set_(element_sort) to the specification.
351 22 : import_system_defined_sort(sort_nat::nat()); // Required for bags.
352 22 : import_system_defined_sort(sort_set::set_(element_sort));
353 22 : import_system_defined_sort(sort_fbag::fbag(element_sort));
354 :
355 : // Add the function sort element_sort->Nat to the specification
356 22 : sort_expression_list element_sorts ;
357 22 : element_sorts.push_front(element_sort);
358 22 : import_system_defined_sort(function_sort(element_sorts,sort_nat::nat()));
359 22 : }
360 41 : else if (sort_fbag::is_fbag(sort))
361 : {
362 41 : import_system_defined_sort(sort_nat::nat()); // Required for bags.
363 : }
364 717 : }
365 67562 : else if (is_structured_sort(sort))
366 : {
367 1629 : structured_sort s_sort(sort);
368 1629 : function_symbol_vector f(s_sort.constructor_functions(sort));
369 4899 : for(const function_symbol& f: s_sort.constructor_functions(sort))
370 : {
371 3270 : import_system_defined_sort(f.sort());
372 1629 : }
373 1629 : }
374 : }
375 :
376 : // The function below recalculates m_normalised_aliases, such that
377 : // it forms a confluent terminating rewriting system using which
378 : // sorts can be normalised.
379 : // This algorithm is described in the document: algorithm-for-sort-equivalence.tex in
380 : // the developers library of the mCRL2 toolset.
381 11400 : void sort_specification::reconstruct_m_normalised_aliases() const
382 : {
383 : // First reset the normalised aliases and the mappings and constructors that have been
384 : // inherited to basic sort aliases during a previous round of sort normalisation.
385 11400 : m_normalised_aliases.clear();
386 :
387 : // This is the first step of the algorithm.
388 : // Check for loops in the aliases. The type checker should already have done this,
389 : // but we check it again here. If there is a loop m_normalised_aliases will not be
390 : // built.
391 15894 : for(const alias& a: m_user_defined_aliases)
392 : {
393 4500 : std::set < sort_expression > sorts_already_seen; // Empty set.
394 : try
395 : {
396 4506 : check_for_alias_loop(a.name(),sorts_already_seen,true);
397 : }
398 6 : catch (mcrl2::runtime_error &)
399 : {
400 6 : mCRL2log(log::debug) << "Encountered an alias loop in the alias for " << a.name() <<". The normalised aliases are not constructed\n";
401 6 : return;
402 6 : }
403 4500 : }
404 :
405 : // This is the second step of the algorithm.
406 : // Copy m_normalised_aliases. All aliases are stored from left to right,
407 : // except structured sorts, which are stored from right to left. The reason is
408 : // that structured sorts can be recursive, and therefore, they cannot be
409 : // rewritten from left to right, as this can cause sorts to be infinitely rewritten.
410 :
411 11394 : std::multimap< sort_expression, sort_expression > sort_aliases_to_be_investigated;
412 11394 : std::multimap< sort_expression, sort_expression > resulting_normalized_sort_aliases;
413 :
414 15888 : for(const alias& a: m_user_defined_aliases)
415 : {
416 4494 : if (is_structured_sort(a.reference()))
417 : {
418 3707 : sort_aliases_to_be_investigated.insert(std::pair<sort_expression,sort_expression>(a.reference(),a.name()));
419 : }
420 : else
421 : {
422 787 : resulting_normalized_sort_aliases.insert(std::pair<sort_expression,sort_expression>(a.name(),a.reference()));
423 : }
424 : }
425 :
426 : // Apply Knuth-Bendix completion to the rules in m_normalised_aliases.
427 15115 : for(; !sort_aliases_to_be_investigated.empty() ;)
428 : {
429 3721 : const std::multimap< sort_expression, sort_expression >::iterator it=sort_aliases_to_be_investigated.begin();
430 3721 : const sort_expression lhs=it->first;
431 3721 : const sort_expression rhs=it->second;
432 3721 : sort_aliases_to_be_investigated.erase(it);
433 :
434 7239 : for(const std::pair<const sort_expression, sort_expression >& p: resulting_normalized_sort_aliases)
435 : {
436 3518 : const sort_expression s1=data::replace_sort_expressions(lhs,sort_expression_assignment(p.first,p.second), true);
437 :
438 3518 : if (s1!=lhs)
439 : {
440 : // There is a conflict between the two sort rewrite rules.
441 69 : assert(is_basic_sort(rhs));
442 : // Choose the normal form on the basis of a lexicographical ordering. This guarantees
443 : // uniqueness of normal forms over different tools. Ordering on addresses (as used previously)
444 : // proved to be unstable over different tools.
445 69 : const bool rhs_to_s1 = is_basic_sort(s1) && pp(basic_sort(s1))<=pp(rhs);
446 69 : const sort_expression left_hand_side=(rhs_to_s1?rhs:s1);
447 69 : const sort_expression pre_normal_form=(rhs_to_s1?s1:rhs);
448 69 : assert(is_basic_sort(pre_normal_form));
449 69 : const sort_expression& e1=pre_normal_form;
450 69 : if (e1!=left_hand_side)
451 : {
452 56 : const sort_expression normalised_lhs=find_normal_form(left_hand_side,resulting_normalized_sort_aliases);
453 : // Check whether the inserted sort rewrite rule is already in sort_aliases_to_be_investigated.
454 56 : if (std::find_if(sort_aliases_to_be_investigated.lower_bound(normalised_lhs),
455 : sort_aliases_to_be_investigated.upper_bound(normalised_lhs),
456 42 : [&rhs](const std::pair<sort_expression,sort_expression>& x){ return x.second==rhs; })
457 112 : == sort_aliases_to_be_investigated.upper_bound(normalised_lhs)) // Not found.
458 : {
459 14 : sort_aliases_to_be_investigated.insert(
460 28 : std::pair<sort_expression,sort_expression > (normalised_lhs, e1));
461 : }
462 56 : }
463 69 : }
464 : else
465 : {
466 3449 : const sort_expression s2 = data::replace_sort_expressions(p.first,sort_expression_assignment(lhs,rhs), true);
467 3449 : if (s2!=p.first)
468 : {
469 0 : assert(is_basic_sort(p.second));
470 : // Choose the normal form on the basis of a lexicographical ordering. This guarantees
471 : // uniqueness of normal forms over different tools.
472 0 : const bool i_second_to_s2 = is_basic_sort(s2) && pp(basic_sort(s2))<=pp(p.second);
473 0 : const sort_expression left_hand_side=(i_second_to_s2?p.second:s2);
474 0 : const sort_expression pre_normal_form=(i_second_to_s2?s2:p.second);
475 0 : assert(is_basic_sort(pre_normal_form));
476 0 : const sort_expression& e2=pre_normal_form;
477 0 : if (e2!=left_hand_side)
478 : {
479 0 : const sort_expression normalised_lhs=find_normal_form(left_hand_side,resulting_normalized_sort_aliases);
480 : // Check whether the inserted sort rewrite rule is already in sort_aliases_to_be_investigated.
481 0 : if (std::find_if(sort_aliases_to_be_investigated.lower_bound(normalised_lhs),
482 : sort_aliases_to_be_investigated.upper_bound(normalised_lhs),
483 0 : [&rhs](const std::pair<sort_expression,sort_expression>& x){ return x.second==rhs; })
484 0 : == sort_aliases_to_be_investigated.upper_bound(normalised_lhs)) // Not found.
485 : {
486 0 : sort_aliases_to_be_investigated.insert(
487 0 : std::pair<sort_expression,sort_expression > (normalised_lhs,e2));
488 : }
489 0 : }
490 0 : }
491 3449 : }
492 3518 : }
493 3721 : assert(lhs!=rhs);
494 3721 : const sort_expression normalised_lhs = find_normal_form(lhs,resulting_normalized_sort_aliases);
495 3721 : const sort_expression normalised_rhs = find_normal_form(rhs,resulting_normalized_sort_aliases);
496 3721 : if (normalised_lhs!=normalised_rhs)
497 : {
498 3707 : resulting_normalized_sort_aliases.insert(std::pair<sort_expression,sort_expression >(normalised_lhs,normalised_rhs));
499 : }
500 3721 : }
501 : // Copy resulting_normalized_sort_aliases into m_normalised_aliases, i.e. from multimap to map.
502 : // If there are rules with equal left hand side, only one is arbitrarily chosen. Rewrite the
503 : // right hand side to normal form.
504 :
505 15888 : for(const std::pair<const sort_expression,sort_expression>& p: resulting_normalized_sort_aliases)
506 : {
507 4494 : const sort_expression normalised_rhs = find_normal_form(p.second,resulting_normalized_sort_aliases);
508 4494 : m_normalised_aliases[p.first]=normalised_rhs;
509 :
510 4494 : assert(p.first!=normalised_rhs);
511 4494 : }
512 11394 : }
513 :
514 : ///\brief Adds the system defined sorts to the sets with constructors, mappings, and equations for
515 : // a given sort. If the boolean skip_equations is true, no equations are added.
516 72141 : void data_specification::find_associated_system_defined_data_types_for_a_sort(
517 : const sort_expression& sort,
518 : std::set < function_symbol >& constructors,
519 : std::set < function_symbol >& mappings,
520 : std::set < data_equation >& equations,
521 : implementation_map& cpp_implemented_functions,
522 : const bool skip_equations) const
523 : {
524 : // add sorts, constructors, mappings and equations
525 72141 : if (sort == sort_bool::bool_())
526 : {
527 10405 : function_symbol_vector f(sort_bool::bool_generate_constructors_code());
528 10405 : constructors.insert(f.begin(), f.end());
529 10405 : f = sort_bool::bool_generate_functions_code();
530 10405 : mappings.insert(f.begin(), f.end());
531 10405 : implementation_map f1 = sort_bool::bool_cpp_implementable_mappings();
532 10405 : cpp_implemented_functions.insert(f1.begin(), f1.end());
533 10405 : f1 = sort_bool::bool_cpp_implementable_constructors();
534 10405 : cpp_implemented_functions.insert(f1.begin(), f1.end());
535 10405 : if (!skip_equations)
536 : {
537 10404 : data_equation_vector e(sort_bool::bool_generate_equations_code());
538 10404 : equations.insert(e.begin(),e.end());
539 10404 : }
540 10405 : }
541 61736 : else if (sort == sort_real::real_())
542 : {
543 5431 : function_symbol_vector f(sort_real::real_generate_constructors_code());
544 5431 : constructors.insert(f.begin(),f.end());
545 5431 : f = sort_real::real_generate_functions_code();
546 5431 : mappings.insert(f.begin(),f.end());
547 5431 : implementation_map f1 = sort_int::int_cpp_implementable_mappings();
548 5431 : cpp_implemented_functions.insert(f1.begin(), f1.end());
549 5431 : f1 = sort_int::int_cpp_implementable_constructors();
550 5431 : cpp_implemented_functions.insert(f1.begin(), f1.end());
551 5431 : if (!skip_equations)
552 : {
553 5430 : data_equation_vector e(sort_real::real_generate_equations_code());
554 5430 : equations.insert(e.begin(),e.end());
555 5430 : }
556 5431 : }
557 56305 : else if (sort == sort_int::int_())
558 : {
559 5483 : function_symbol_vector f(sort_int::int_generate_constructors_code());
560 5483 : constructors.insert(f.begin(),f.end());
561 5483 : f = sort_int::int_generate_functions_code();
562 5483 : mappings.insert(f.begin(),f.end());
563 5483 : implementation_map f1 = sort_int::int_cpp_implementable_mappings();
564 5483 : cpp_implemented_functions.insert(f1.begin(), f1.end());
565 5483 : f1 = sort_int::int_cpp_implementable_constructors();
566 5483 : cpp_implemented_functions.insert(f1.begin(), f1.end());
567 5483 : if (!skip_equations)
568 : {
569 5482 : data_equation_vector e(sort_int::int_generate_equations_code());
570 5482 : equations.insert(e.begin(),e.end());
571 5482 : }
572 5483 : }
573 50822 : else if (sort == sort_nat::nat())
574 : {
575 6296 : function_symbol_vector f(sort_nat::nat_generate_constructors_code());
576 6296 : constructors.insert(f.begin(),f.end());
577 6296 : f = sort_nat::nat_generate_functions_code();
578 6296 : mappings.insert(f.begin(),f.end());
579 6296 : implementation_map f1 = sort_nat::nat_cpp_implementable_mappings();
580 6296 : cpp_implemented_functions.insert(f1.begin(), f1.end());
581 6296 : f1 = sort_nat::nat_cpp_implementable_constructors();
582 6296 : cpp_implemented_functions.insert(f1.begin(), f1.end());
583 6296 : if (!skip_equations)
584 : {
585 6295 : data_equation_vector e(sort_nat::nat_generate_equations_code());
586 6295 : equations.insert(e.begin(),e.end());
587 6295 : }
588 6296 : }
589 44526 : else if (sort == sort_pos::pos())
590 : {
591 10484 : function_symbol_vector f(sort_pos::pos_generate_constructors_code());
592 10484 : constructors.insert(f.begin(),f.end());
593 10484 : f = sort_pos::pos_generate_functions_code();
594 10484 : mappings.insert(f.begin(),f.end());
595 10484 : implementation_map f1 = sort_pos::pos_cpp_implementable_mappings();
596 10484 : cpp_implemented_functions.insert(f1.begin(), f1.end());
597 10484 : f1 = sort_pos::pos_cpp_implementable_constructors();
598 10484 : cpp_implemented_functions.insert(f1.begin(), f1.end());
599 10484 : if (!skip_equations)
600 : {
601 10483 : data_equation_vector e(sort_pos::pos_generate_equations_code());
602 10483 : equations.insert(e.begin(),e.end());
603 10483 : }
604 10484 : }
605 34042 : else if (is_function_sort(sort))
606 : {
607 18479 : const sort_expression& t=function_sort(sort).codomain();
608 18479 : const sort_expression_list& l=function_sort(sort).domain();
609 18479 : if (l.size()==1)
610 : {
611 6992 : const function_symbol_vector f = function_update_generate_functions_code(l.front(),t);
612 6992 : mappings.insert(f.begin(),f.end());
613 6992 : implementation_map f1 = function_update_cpp_implementable_mappings(l.front(),t);
614 6992 : cpp_implemented_functions.insert(f1.begin(), f1.end());
615 6992 : f1 = function_update_cpp_implementable_constructors();
616 6992 : cpp_implemented_functions.insert(f1.begin(), f1.end());
617 6992 : if (!skip_equations)
618 : {
619 6992 : data_equation_vector e(function_update_generate_equations_code(l.front(),t));
620 6992 : equations.insert(e.begin(),e.end());
621 6992 : }
622 6992 : }
623 : }
624 15563 : else if (is_container_sort(sort))
625 : {
626 1833 : sort_expression element_sort(container_sort(sort).element_sort());
627 1833 : if (sort_list::is_list(sort))
628 : {
629 1078 : function_symbol_vector f(sort_list::list_generate_constructors_code(element_sort));
630 1078 : constructors.insert(f.begin(),f.end());
631 1078 : f = sort_list::list_generate_functions_code(element_sort);
632 1078 : mappings.insert(f.begin(),f.end());
633 1078 : implementation_map f1 = sort_list::list_cpp_implementable_mappings(element_sort);
634 1078 : cpp_implemented_functions.insert(f1.begin(), f1.end());
635 1078 : f1 = sort_list::list_cpp_implementable_constructors(element_sort);
636 1078 : cpp_implemented_functions.insert(f1.begin(), f1.end());
637 1078 : if (!skip_equations)
638 : {
639 1077 : data_equation_vector e(sort_list::list_generate_equations_code(element_sort));
640 1077 : equations.insert(e.begin(),e.end());
641 1077 : }
642 1078 : }
643 755 : else if (sort_set::is_set(sort))
644 : {
645 283 : sort_expression_list element_sorts;
646 283 : element_sorts.push_front(element_sort);
647 283 : function_symbol_vector f(sort_set::set_generate_constructors_code(element_sort));
648 283 : constructors.insert(f.begin(),f.end());
649 283 : f = sort_set::set_generate_functions_code(element_sort);
650 283 : mappings.insert(f.begin(),f.end());
651 283 : implementation_map f1 = sort_set::set_cpp_implementable_mappings(element_sort);
652 283 : cpp_implemented_functions.insert(f1.begin(), f1.end());
653 283 : f1 = sort_set::set_cpp_implementable_constructors(element_sort);
654 283 : cpp_implemented_functions.insert(f1.begin(), f1.end());
655 283 : if (!skip_equations)
656 : {
657 282 : data_equation_vector e(sort_set::set_generate_equations_code(element_sort));
658 282 : equations.insert(e.begin(),e.end());
659 282 : }
660 283 : }
661 472 : else if (sort_fset::is_fset(sort))
662 : {
663 332 : function_symbol_vector f = sort_fset::fset_generate_constructors_code(element_sort);
664 332 : constructors.insert(f.begin(),f.end());
665 332 : f = sort_fset::fset_generate_functions_code(element_sort);
666 332 : mappings.insert(f.begin(),f.end());
667 332 : implementation_map f1 = sort_fset::fset_cpp_implementable_mappings(element_sort);
668 332 : cpp_implemented_functions.insert(f1.begin(), f1.end());
669 332 : f1 = sort_fset::fset_cpp_implementable_constructors(element_sort);
670 332 : cpp_implemented_functions.insert(f1.begin(), f1.end());
671 332 : if (!skip_equations)
672 : {
673 331 : data_equation_vector e = sort_fset::fset_generate_equations_code(element_sort);
674 331 : equations.insert(e.begin(),e.end());
675 331 : }
676 332 : }
677 140 : else if (sort_bag::is_bag(sort))
678 : {
679 68 : sort_expression_list element_sorts;
680 68 : element_sorts.push_front(element_sort);
681 68 : function_symbol_vector f(sort_bag::bag_generate_constructors_code(element_sort));
682 68 : constructors.insert(f.begin(),f.end());
683 68 : f = sort_bag::bag_generate_functions_code(element_sort);
684 68 : mappings.insert(f.begin(),f.end());
685 68 : implementation_map f1 = sort_bag::bag_cpp_implementable_mappings(element_sort);
686 68 : cpp_implemented_functions.insert(f1.begin(), f1.end());
687 68 : f1 = sort_bag::bag_cpp_implementable_constructors(element_sort);
688 68 : cpp_implemented_functions.insert(f1.begin(), f1.end());
689 68 : if (!skip_equations)
690 : {
691 67 : data_equation_vector e(sort_bag::bag_generate_equations_code(element_sort));
692 67 : equations.insert(e.begin(),e.end());
693 67 : }
694 68 : }
695 72 : else if (sort_fbag::is_fbag(sort))
696 : {
697 72 : function_symbol_vector f = sort_fbag::fbag_generate_constructors_code(element_sort);
698 72 : constructors.insert(f.begin(),f.end());
699 72 : f = sort_fbag::fbag_generate_functions_code(element_sort);
700 72 : mappings.insert(f.begin(),f.end());
701 72 : implementation_map f1 = sort_fbag::fbag_cpp_implementable_mappings(element_sort);
702 72 : cpp_implemented_functions.insert(f1.begin(), f1.end());
703 72 : f1 = sort_fbag::fbag_cpp_implementable_constructors(element_sort);
704 72 : cpp_implemented_functions.insert(f1.begin(), f1.end());
705 72 : if (!skip_equations)
706 : {
707 71 : data_equation_vector e = sort_fbag::fbag_generate_equations_code(element_sort);
708 71 : equations.insert(e.begin(),e.end());
709 71 : }
710 72 : }
711 1833 : }
712 13730 : else if (is_structured_sort(sort))
713 : {
714 3496 : insert_mappings_constructors_for_structured_sort(
715 : atermpp::down_cast<structured_sort>(sort),
716 : constructors, mappings, equations, skip_equations);
717 : }
718 72141 : add_standard_mappings_and_equations(sort, mappings, equations, skip_equations);
719 72141 : }
720 :
721 1 : void data_specification::get_system_defined_sorts_constructors_and_mappings(
722 : std::set < sort_expression >& sorts,
723 : std::set < function_symbol >& constructors,
724 : std::set <function_symbol >& mappings) const
725 : {
726 1 : implementation_map cpp_implemented_functions;
727 :
728 1 : sorts.insert(sort_bool::bool_());
729 1 : sorts.insert(sort_pos::pos());
730 1 : sorts.insert(sort_nat::nat());
731 1 : sorts.insert(sort_int::int_());
732 1 : sorts.insert(sort_real::real_());
733 1 : sorts.insert(sort_list::list(sort_pos::pos()));
734 1 : sorts.insert(sort_fset::fset(sort_pos::pos()));
735 1 : sorts.insert(sort_set::set_(sort_pos::pos()));
736 1 : sorts.insert(sort_fbag::fbag(sort_pos::pos()));
737 1 : sorts.insert(sort_bag::bag(sort_pos::pos()));
738 :
739 1 : std::set < data_equation > dummy_equations;
740 11 : for(const sort_expression& s: sorts)
741 : {
742 10 : find_associated_system_defined_data_types_for_a_sort(s, constructors, mappings, dummy_equations, cpp_implemented_functions, true);
743 : }
744 1 : assert(dummy_equations.size()==0);
745 1 : }
746 :
747 994 : bool data_specification::is_well_typed() const
748 : {
749 : // check 1)
750 994 : if (!detail::check_data_spec_sorts(constructors(), sorts()))
751 : {
752 : std::clog << "data_specification::is_well_typed() failed: not all of the sorts appearing in the constructors "
753 0 : << data::pp(constructors()) << " are declared in " << data::pp(sorts()) << std::endl;
754 0 : return false;
755 : }
756 :
757 : // check 2)
758 994 : if (!detail::check_data_spec_sorts(mappings(), sorts()))
759 : {
760 : std::clog << "data_specification::is_well_typed() failed: not all of the sorts appearing in the mappings "
761 0 : << data::pp(mappings()) << " are declared in " << data::pp(sorts()) << std::endl;
762 0 : return false;
763 : }
764 :
765 994 : return true;
766 : }
767 :
768 : /// There are two types of representations of ATerms:
769 : /// - the bare specification that does not contain constructor, mappings
770 : /// and equations for system defined sorts
771 : /// - specification that includes all system defined information (legacy)
772 : /// The last type must eventually disappear but is unfortunately still in
773 : /// use in a substantial amount of source code.
774 : /// Note, all sorts with name prefix \@legacy_ are eliminated
775 3 : void data_specification::build_from_aterm(const atermpp::aterm_appl& term)
776 : {
777 3 : assert(core::detail::check_rule_DataSpec(term));
778 :
779 : // Note backwards compatibility measure: alias is no longer a sort_expression
780 : const atermpp::term_list<atermpp::aterm_appl> term_sorts=
781 3 : atermpp::down_cast<atermpp::term_list<atermpp::aterm_appl> >(atermpp::down_cast<atermpp::aterm_appl>(term[0])[0]);
782 : const data::function_symbol_list term_constructors=
783 3 : atermpp::down_cast<data::function_symbol_list>(atermpp::down_cast<atermpp::aterm_appl>(term[1])[0]);
784 : const data::function_symbol_list term_mappings=
785 3 : atermpp::down_cast<data::function_symbol_list>(atermpp::down_cast<atermpp::aterm_appl>(term[2])[0]);
786 : const data::data_equation_list term_equations=
787 3 : atermpp::down_cast<data::data_equation_list>(atermpp::down_cast<atermpp::aterm_appl>(term[3])[0]);
788 :
789 : // Store the sorts and aliases.
790 9 : for(const atermpp::aterm_appl& t: term_sorts)
791 : {
792 6 : if (data::is_alias(t)) // Compatibility with legacy code
793 : {
794 5 : add_alias(atermpp::down_cast<data::alias>(t));
795 : }
796 : else
797 : {
798 1 : add_sort(atermpp::down_cast<basic_sort>(t));
799 : }
800 : }
801 :
802 : // Store the constructors.
803 4 : for(const function_symbol& f: term_constructors)
804 : {
805 1 : add_constructor(f);
806 : }
807 :
808 : // Store the mappings.
809 4 : for(const function_symbol& f: term_mappings)
810 : {
811 1 : add_mapping(f);
812 : }
813 :
814 : // Store the equations.
815 3 : for(const data_equation& e: term_equations)
816 : {
817 0 : add_equation(e);
818 : }
819 3 : }
820 :
821 72 : data_specification::data_specification(const basic_sort_vector& sorts,
822 : const alias_vector& aliases,
823 : const function_symbol_vector& constructors,
824 : const function_symbol_vector& user_defined_mappings,
825 72 : const data_equation_vector& user_defined_equations)
826 72 : : sort_specification(sorts, aliases)
827 : {
828 : // Store the constructors.
829 72 : for(const function_symbol& f: constructors)
830 : {
831 0 : add_constructor(f);
832 : }
833 :
834 : // Store the mappings.
835 93 : for(const function_symbol& f: user_defined_mappings)
836 : {
837 21 : add_mapping(f);
838 : }
839 :
840 : // Store the equations.
841 89 : for(const data_equation& e: user_defined_equations)
842 : {
843 17 : add_equation(e);
844 : }
845 :
846 72 : assert(is_well_typed());
847 72 : }
848 :
849 : } // namespace data
850 : } // namespace mcrl2
|
