Line data Source code
1 : // Author(s): Yaroslav Usenko, Jan Friso Groote, Wieger Wesselink (2015)
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 : #include "mcrl2/data/print.h"
10 : #include "mcrl2/data/typecheck.h"
11 :
12 : using namespace mcrl2::log;
13 : using namespace mcrl2::core::detail;
14 : using namespace mcrl2::data;
15 : using namespace atermpp;
16 :
17 : namespace mcrl2
18 : {
19 : namespace data
20 : {
21 :
22 : namespace detail
23 : {
24 :
25 9990 : void variable_context::typecheck_variable(const data_type_checker& typechecker, const variable& v) const
26 : {
27 9990 : typechecker(v, *this);
28 9990 : }
29 :
30 : // This function checks whether the set s1 is included in s2. If not the variable culprit
31 : // is the variable occuring in s1 but not in s2.
32 0 : static bool includes(const std::set<variable>& s1, const std::set<variable>& s2, variable& culprit)
33 : {
34 0 : for(const variable& v: s1)
35 : {
36 0 : if (s2.count(v)==0)
37 : {
38 0 : culprit=v;
39 0 : return false;
40 : }
41 : }
42 0 : return true;
43 : }
44 :
45 6623 : static inline bool IsPos(const core::identifier_string& Number)
46 : {
47 6623 : char c=Number.function().name()[0];
48 6623 : return isdigit(c) && c>'0';
49 : }
50 788 : static inline bool IsNat(const core::identifier_string& Number)
51 : {
52 788 : return isdigit(Number.function().name()[0]) != 0;
53 : }
54 :
55 : static sort_expression_list GetVarTypes(variable_list VarDecls);
56 : static bool HasUnknown(const sort_expression& Type);
57 : static bool IsNumericType(const sort_expression& Type);
58 : static sort_expression MinType(const sort_expression_list& TypeList);
59 : static sort_expression replace_possible_sorts(const sort_expression& Type);
60 :
61 : // Insert an element in the list provided, it did not already occur in the list.
62 : template<class S>
63 22530 : inline atermpp::term_list<S> insert_sort_unique(const atermpp::term_list<S>& list, const S& el)
64 : {
65 22530 : if (std::find(list.begin(),list.end(), el) == list.end())
66 : {
67 22410 : atermpp::term_list<S> result=list;
68 22410 : result.push_front(el);
69 22410 : return result;
70 22410 : }
71 120 : return list;
72 : }
73 :
74 : } // namespace detail
75 : } // namespace data
76 :
77 : // ------------------------------ Here starts the new class based data expression checker -----------------------
78 :
79 : // The function below is used to check whether a term is well typed.
80 : // It always yields true, but if the dataterm is not properly typed, using the types
81 : // that are included inside the term it calls an assert. This function is useful to check
82 : // whether typing was succesful, using assert(strict_type_check(d)).
83 :
84 0 : bool mcrl2::data::data_type_checker::strict_type_check(const data_expression& d) const
85 : {
86 0 : if (is_abstraction(d))
87 : {
88 0 : const abstraction& abstr=down_cast<const abstraction>(d);
89 0 : assert(abstr.variables().size()>0);
90 0 : const binder_type& BindingOperator = abstr.binding_operator();
91 :
92 0 : if (is_forall_binder(BindingOperator) || is_exists_binder(BindingOperator))
93 : {
94 0 : assert(d.sort()==sort_bool::bool_());
95 0 : strict_type_check(abstr.body());
96 : }
97 :
98 0 : if (is_lambda_binder(BindingOperator))
99 : {
100 0 : strict_type_check(abstr.body());
101 : }
102 0 : return true;
103 : }
104 :
105 0 : if (is_where_clause(d))
106 : {
107 0 : const where_clause& where=down_cast<const where_clause>(d);
108 0 : const assignment_expression_list& where_asss=where.declarations();
109 0 : for (assignment_expression_list::const_iterator i=where_asss.begin(); i!=where_asss.end(); ++i)
110 : {
111 0 : const assignment_expression WhereElem= *i;
112 0 : const assignment& t=down_cast<const assignment>(WhereElem);
113 0 : strict_type_check(t.rhs());
114 0 : }
115 0 : strict_type_check(where.body());
116 0 : return true;
117 : }
118 :
119 0 : if (is_application(d))
120 : {
121 0 : const application& appl=down_cast<application>(d);
122 0 : const data_expression& head = appl.head();
123 :
124 0 : if (data::is_function_symbol(head))
125 : {
126 0 : core::identifier_string name = function_symbol(head).name();
127 0 : if (name == sort_list::list_enumeration_name())
128 : {
129 0 : const sort_expression s=d.sort();
130 0 : assert(sort_list::is_list(s));
131 0 : const sort_expression s1=container_sort(s).element_sort();
132 :
133 0 : for (application::const_iterator i=appl.begin(); i!=appl.end(); ++i)
134 : {
135 0 : strict_type_check(*i);
136 0 : assert(i->sort()==s1);
137 :
138 : }
139 0 : return true;
140 0 : }
141 0 : if (name == sort_set::set_enumeration_name())
142 : {
143 0 : const sort_expression s=d.sort();
144 0 : assert(sort_fset::is_fset(s));
145 0 : const sort_expression s1=container_sort(s).element_sort();
146 :
147 0 : for (application::const_iterator i=appl.begin(); i!=appl.end(); ++i)
148 : {
149 0 : strict_type_check(*i);
150 0 : assert(i->sort()==s1);
151 :
152 : }
153 0 : return true;
154 0 : }
155 0 : if (name == sort_bag::bag_enumeration_name())
156 : {
157 0 : const sort_expression s=d.sort();
158 0 : assert(sort_fbag::is_fbag(s));
159 0 : const sort_expression s1=container_sort(s).element_sort();
160 :
161 0 : for (application::const_iterator i=appl.begin(); i!=appl.end(); ++i)
162 : {
163 0 : strict_type_check(*i);
164 0 : assert(i->sort()==s1);
165 : // Every second element in a bag enumeration should be of type Nat.
166 0 : ++i;
167 0 : strict_type_check(*i);
168 0 : assert(i->sort()==sort_nat::nat());
169 :
170 : }
171 0 : return true;
172 :
173 0 : }
174 0 : }
175 0 : strict_type_check(head);
176 0 : const sort_expression& s=head.sort();
177 0 : assert(is_function_sort(s));
178 0 : assert(d.sort()==function_sort(s).codomain());
179 0 : sort_expression_list argument_sorts=function_sort(s).domain();
180 0 : assert(appl.size()==argument_sorts.size());
181 0 : application::const_iterator j=appl.begin();
182 0 : for(sort_expression_list::const_iterator i=argument_sorts.begin(); i!=argument_sorts.end(); ++i,++j)
183 : {
184 0 : assert(UnwindType(j->sort())==UnwindType(*i));
185 0 : strict_type_check(*j);
186 : }
187 0 : return true;
188 0 : }
189 :
190 0 : if (data::is_function_symbol(d)||is_variable(d))
191 : {
192 0 : return true;
193 : }
194 :
195 0 : assert(0); // Unexpected data_expression.
196 : return true;
197 : }
198 :
199 11569 : sort_expression mcrl2::data::data_type_checker::UpCastNumericType(
200 : sort_expression NeededType,
201 : sort_expression Type,
202 : data_expression& Par,
203 : const detail::variable_context& DeclaredVars,
204 : const bool strictly_ambiguous,
205 : bool warn_upcasting,
206 : const bool print_cast_error) const
207 : {
208 : // Makes upcasting from Type to Needed Type for Par. Returns the resulting type.
209 : // Moreover, *Par is extended with the required type transformations.
210 :
211 11569 : if (data::is_untyped_sort(Type))
212 : {
213 1 : return Type;
214 : }
215 11568 : if (data::is_untyped_sort(NeededType))
216 : {
217 3527 : return Type;
218 : }
219 :
220 : // Added to make sure that the types are sufficiently unrolled, because this function is not always called
221 : // with unrolled types.
222 8041 : NeededType=UnwindType(NeededType);
223 8041 : Type=UnwindType(Type);
224 :
225 8041 : if (EqTypesA(NeededType,Type))
226 : {
227 4780 : return Type;
228 : }
229 :
230 3261 : if (data::is_untyped_possible_sorts(NeededType))
231 : {
232 0 : untyped_possible_sorts mps(NeededType);
233 0 : const sort_expression_list& l=mps.sorts();
234 0 : for(sort_expression_list::const_iterator i=l.begin(); i!=l.end(); ++i)
235 : {
236 0 : bool found_solution=true;
237 0 : sort_expression r;
238 : try
239 : {
240 0 : r=UpCastNumericType(*i,Type,Par,DeclaredVars,strictly_ambiguous,warn_upcasting,print_cast_error);
241 : }
242 0 : catch (mcrl2::runtime_error&)
243 : {
244 0 : found_solution=false;
245 0 : }
246 0 : if (found_solution)
247 : {
248 0 : return r;
249 : }
250 0 : }
251 0 : throw mcrl2::runtime_error("Cannot transform " + data::pp(Type) + " to a number.");
252 0 : }
253 :
254 3261 : if (warn_upcasting && data::is_function_symbol(Par) && utilities::is_numeric_string(down_cast<function_symbol>(Par).name().function().name()))
255 : {
256 1 : warn_upcasting=false;
257 : }
258 :
259 : // Try Upcasting to Pos
260 3261 : sort_expression temp;
261 3261 : if (TypeMatchA(NeededType,sort_pos::pos(),temp))
262 : {
263 8 : if (TypeMatchA(Type,sort_pos::pos(),temp))
264 : {
265 0 : return sort_pos::pos();
266 : }
267 : }
268 :
269 : // Try Upcasting to Nat
270 3261 : if (TypeMatchA(NeededType,sort_nat::nat(),temp))
271 : {
272 2240 : if (TypeMatchA(Type,sort_pos::pos(),temp))
273 : {
274 2240 : data_expression OldPar=Par;
275 2240 : Par=application(sort_nat::cnat(),Par);
276 2240 : if (warn_upcasting)
277 : {
278 1 : was_warning_upcasting=true;
279 1 : mCRL2log(warning) << "Upcasting " << OldPar << " to sort Nat by applying Pos2Nat to it." << std::endl;
280 : }
281 2240 : return sort_nat::nat();
282 2240 : }
283 0 : if (TypeMatchA(Type,sort_nat::nat(),temp))
284 : {
285 0 : return sort_nat::nat();
286 : }
287 : }
288 :
289 : // Try Upcasting to Int
290 1021 : if (TypeMatchA(NeededType,sort_int::int_(),temp))
291 : {
292 143 : if (TypeMatchA(Type,sort_pos::pos(),temp))
293 : {
294 96 : data_expression OldPar=Par;
295 96 : Par=application(sort_int::cint(),application(sort_nat::cnat(),Par));
296 96 : if (warn_upcasting)
297 : {
298 0 : was_warning_upcasting=true;
299 0 : mCRL2log(warning) << "Upcasting " << OldPar << " to sort Int by applying Pos2Int to it." << std::endl;
300 : }
301 96 : return sort_int::int_();
302 96 : }
303 47 : if (TypeMatchA(Type,sort_nat::nat(),temp))
304 : {
305 47 : data_expression OldPar=Par;
306 47 : Par=application(sort_int::cint(),Par);
307 47 : if (warn_upcasting)
308 : {
309 0 : was_warning_upcasting=true;
310 0 : mCRL2log(warning) << "Upcasting " << OldPar << " to sort Int by applying Nat2Int to it." << std::endl;
311 : }
312 47 : return sort_int::int_();
313 47 : }
314 0 : if (TypeMatchA(Type,sort_int::int_(),temp))
315 : {
316 0 : return sort_int::int_();
317 : }
318 : }
319 :
320 : // Try Upcasting to Real
321 878 : if (TypeMatchA(NeededType,sort_real::real_(),temp))
322 : {
323 448 : if (TypeMatchA(Type,sort_pos::pos(),temp))
324 : {
325 401 : data_expression OldPar=Par;
326 1203 : Par=application(sort_real::creal(),
327 802 : application(sort_int::cint(), application(sort_nat::cnat(),Par)),
328 401 : sort_pos::c1());
329 401 : if (warn_upcasting)
330 : {
331 0 : was_warning_upcasting=true;
332 0 : mCRL2log(warning) << "Upcasting " << OldPar << " to sort Real by applying Pos2Real to it." << std::endl;
333 : }
334 401 : return sort_real::real_();
335 401 : }
336 47 : if (TypeMatchA(Type,sort_nat::nat(),temp))
337 : {
338 34 : data_expression OldPar=Par;
339 102 : Par=application(sort_real::creal(),
340 68 : application(sort_int::cint(),Par),
341 34 : sort_pos::c1());
342 34 : if (warn_upcasting)
343 : {
344 0 : was_warning_upcasting=true;
345 0 : mCRL2log(warning) << "Upcasting " << OldPar << " to sort Real by applying Nat2Real to it." << std::endl;
346 : }
347 34 : return sort_real::real_();
348 34 : }
349 13 : if (TypeMatchA(Type,sort_int::int_(),temp))
350 : {
351 13 : data_expression OldPar=Par;
352 13 : Par=application(sort_real::creal(),Par, sort_pos::c1());
353 13 : if (warn_upcasting)
354 : {
355 0 : was_warning_upcasting=true;
356 0 : mCRL2log(warning) << "Upcasting " << OldPar << " to sort Real by applying Int2Real to it." << std::endl;
357 : }
358 13 : return sort_real::real_();
359 13 : }
360 0 : if (TypeMatchA(Type,sort_real::real_(),temp))
361 : {
362 0 : return sort_real::real_();
363 : }
364 : }
365 :
366 : // If NeededType and Type are both container types, try to upcast the argument.
367 430 : if (is_container_sort(NeededType) && is_container_sort(Type))
368 : {
369 302 : const container_sort needed_container_type(NeededType);
370 302 : const container_sort container_type(Type);
371 302 : sort_expression needed_argument_type=needed_container_type.element_sort();
372 302 : const sort_expression& argument_type=container_type.element_sort();
373 302 : if (is_untyped_sort(needed_argument_type))
374 : {
375 5 : needed_argument_type=argument_type;
376 : }
377 302 : const sort_expression needed_similar_container_type=container_sort(container_type.container_name(),needed_argument_type);
378 302 : if (needed_similar_container_type==NeededType)
379 : {
380 235 : throw mcrl2::runtime_error("Cannot typecast " + data::pp(Type) + " into " + data::pp(NeededType) + " for data expression " + data::pp(Par) + ".");
381 : }
382 : try
383 : {
384 134 : Type=TraverseVarConsTypeD(DeclaredVars,Par,
385 67 : needed_similar_container_type,strictly_ambiguous,warn_upcasting,print_cast_error);
386 67 : assert(UnwindType(Type)==UnwindType(needed_similar_container_type));
387 :
388 : }
389 0 : catch (mcrl2::runtime_error& e)
390 : {
391 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nError occurred while trying to match argument types of " + data::pp(NeededType) + " and " +
392 0 : data::pp(Type) + " in data expression " + data::pp(Par) + ".");
393 0 : }
394 1007 : }
395 :
396 :
397 : // If is is an fset, try upcasting to a set.
398 195 : if (is_container_sort(NeededType) && is_set_container(container_sort(NeededType).container_name()))
399 : {
400 56 : if (is_container_sort(Type) && is_fset_container(container_sort(Type).container_name()))
401 : {
402 56 : Par=sort_set::constructor(container_sort(NeededType).element_sort(),sort_set::false_function(container_sort(NeededType).element_sort()),Par);
403 : // Do this again to lift argument types if needed. TODO.
404 56 : return NeededType;
405 : }
406 0 : else if (is_container_sort(Type) && is_set_container(container_sort(Type).container_name()))
407 : {
408 0 : if (Type==NeededType)
409 : {
410 0 : return Type;
411 : }
412 : else
413 : {
414 0 : throw mcrl2::runtime_error("Upcasting " + data::pp(Type) + " to " + data::pp(NeededType) + " fails (1).");
415 : }
416 : }
417 : }
418 :
419 : // If is is an fbag, try upcasting to a bag.
420 139 : if (is_container_sort(NeededType) && is_bag_container(container_sort(NeededType).container_name()))
421 : {
422 11 : if (is_container_sort(Type) && is_fbag_container(container_sort(Type).container_name()))
423 : {
424 11 : Par=sort_bag::constructor(container_sort(NeededType).element_sort(),sort_bag::zero_function(container_sort(NeededType).element_sort()),Par);
425 : // Do this again to lift argument types if needed. TODO.
426 11 : return NeededType;
427 : }
428 0 : else if (is_container_sort(Type) && is_bag_container(container_sort(Type).container_name()))
429 : {
430 0 : if (Type==NeededType)
431 : {
432 0 : return Type;
433 : }
434 : else
435 : {
436 0 : throw mcrl2::runtime_error("Upcasting " + data::pp(Type) + " to " + data::pp(NeededType) + " fails (1).");
437 : }
438 : }
439 : }
440 :
441 128 : if (is_function_sort(NeededType))
442 : {
443 17 : const function_sort needed_function_type(NeededType);
444 17 : if (is_function_sort(Type))
445 : {
446 : // we only deal here with @false_ and @zero (false_function and zero_function).
447 17 : if (Par==sort_set::false_function(data::untyped_sort()))
448 : {
449 11 : assert(needed_function_type.domain().size()==1);
450 11 : Par=sort_set::false_function(needed_function_type.domain().front());
451 11 : return NeededType;
452 : }
453 6 : else if (Par==sort_bag::zero_function(data::untyped_sort()))
454 : {
455 6 : assert(needed_function_type.domain().size()==1);
456 6 : Par=sort_bag::zero_function(needed_function_type.domain().front());
457 6 : return NeededType;
458 : }
459 : }
460 17 : }
461 :
462 111 : throw mcrl2::runtime_error("Upcasting " + data::pp(Type) + " to " + data::pp(NeededType) + " fails (3).");
463 3261 : }
464 :
465 :
466 219 : bool mcrl2::data::data_type_checker::UnFSet(sort_expression PosType, sort_expression& result) const
467 : {
468 : //select Set(Type), elements, return their list of arguments.
469 219 : if (is_basic_sort(PosType))
470 : {
471 0 : PosType=UnwindType(PosType);
472 : }
473 219 : if (sort_fset::is_fset(PosType) || sort_set::is_set(PosType))
474 : {
475 60 : result=down_cast<container_sort>(PosType).element_sort();
476 60 : return true;
477 : }
478 159 : if (data::is_untyped_sort(PosType))
479 : {
480 159 : result=PosType;
481 159 : return true;
482 : }
483 :
484 0 : sort_expression_list NewPosTypes;
485 0 : if (is_untyped_possible_sorts(PosType))
486 : {
487 0 : const untyped_possible_sorts& mps=down_cast<untyped_possible_sorts>(PosType);
488 0 : for (sort_expression_list PosTypes=mps.sorts(); !PosTypes.empty(); PosTypes=PosTypes.tail())
489 : {
490 0 : sort_expression NewPosType=PosTypes.front();
491 0 : if (is_basic_sort(NewPosType))
492 : {
493 0 : NewPosType=UnwindType(NewPosType);
494 : }
495 0 : if (sort_fset::is_fset(sort_expression(NewPosType))|| (sort_set::is_set(sort_expression(NewPosType))))
496 : {
497 0 : NewPosType=down_cast<const container_sort>(NewPosType).element_sort();
498 : }
499 0 : else if (!data::is_untyped_sort(data::sort_expression(NewPosType)))
500 : {
501 0 : continue;
502 : }
503 0 : NewPosTypes.push_front(NewPosType);
504 0 : }
505 0 : NewPosTypes=reverse(NewPosTypes);
506 0 : result=untyped_possible_sorts(sort_expression_list(NewPosTypes));
507 0 : return true;
508 : }
509 0 : return false;
510 0 : }
511 :
512 198 : bool mcrl2::data::data_type_checker::UnFBag(sort_expression PosType, sort_expression& result) const
513 : {
514 : //select Bag(Type), elements, return their list of arguments.
515 198 : if (is_basic_sort(PosType))
516 : {
517 0 : PosType=UnwindType(PosType);
518 : }
519 198 : if (sort_fbag::is_fbag(sort_expression(PosType)) || (sort_bag::is_bag(sort_expression(PosType))))
520 : {
521 10 : result=down_cast<const container_sort>(PosType).element_sort();
522 10 : return true;
523 : }
524 188 : if (data::is_untyped_sort(data::sort_expression(PosType)))
525 : {
526 188 : result=PosType;
527 188 : return true;
528 : }
529 :
530 0 : sort_expression_list NewPosTypes;
531 0 : if (is_untyped_possible_sorts(PosType))
532 : {
533 0 : const untyped_possible_sorts& mps=down_cast<untyped_possible_sorts>(PosType);
534 0 : for (sort_expression_list PosTypes=mps.sorts(); !PosTypes.empty(); PosTypes=PosTypes.tail())
535 : {
536 0 : sort_expression NewPosType=PosTypes.front();
537 0 : if (is_basic_sort(NewPosType))
538 : {
539 0 : NewPosType=UnwindType(NewPosType);
540 : }
541 0 : if (sort_fbag::is_fbag(sort_expression(NewPosType))|| (sort_fbag::is_fbag(sort_expression(NewPosType))))
542 : {
543 0 : NewPosType=down_cast<const container_sort>(NewPosType).element_sort();
544 : }
545 0 : else if (!data::is_untyped_sort(data::sort_expression(NewPosType)))
546 : {
547 0 : continue;
548 : }
549 0 : NewPosTypes.push_front(NewPosType);
550 0 : }
551 0 : NewPosTypes=reverse(NewPosTypes);
552 0 : result=untyped_possible_sorts(sort_expression_list(NewPosTypes));
553 0 : return true;
554 : }
555 0 : return false;
556 0 : }
557 :
558 130 : bool mcrl2::data::data_type_checker::UnList(sort_expression PosType, sort_expression& result) const
559 : {
560 : //select List(Type), elements, return their list of arguments.
561 130 : if (is_basic_sort(PosType))
562 : {
563 0 : PosType=UnwindType(PosType);
564 : }
565 130 : if (sort_list::is_list(sort_expression(PosType)))
566 : {
567 85 : result=down_cast<const container_sort>(PosType).element_sort();
568 85 : return true;
569 : }
570 45 : if (data::is_untyped_sort(data::sort_expression(PosType)))
571 : {
572 45 : result=PosType;
573 45 : return true;
574 : }
575 :
576 0 : sort_expression_list NewPosTypes;
577 0 : if (is_untyped_possible_sorts(PosType))
578 : {
579 0 : const untyped_possible_sorts& mps=down_cast<untyped_possible_sorts>(PosType);
580 0 : for (sort_expression_list PosTypes=mps.sorts(); !PosTypes.empty(); PosTypes=PosTypes.tail())
581 : {
582 0 : sort_expression NewPosType=PosTypes.front();
583 0 : if (is_basic_sort(NewPosType))
584 : {
585 0 : NewPosType=UnwindType(NewPosType);
586 : }
587 0 : if (sort_list::is_list(NewPosType))
588 : {
589 0 : NewPosType=down_cast<const container_sort>(NewPosType).element_sort();
590 : }
591 0 : else if (!data::is_untyped_sort(NewPosType))
592 : {
593 0 : continue;
594 : }
595 0 : NewPosTypes.push_front(NewPosType);
596 0 : }
597 0 : NewPosTypes=reverse(NewPosTypes);
598 0 : result=untyped_possible_sorts(sort_expression_list(NewPosTypes));
599 0 : return true;
600 : }
601 0 : return false;
602 0 : }
603 :
604 :
605 111 : bool mcrl2::data::data_type_checker::UnArrowProd(const sort_expression_list& ArgTypes, sort_expression PosType, sort_expression& result) const
606 : {
607 : //Filter PosType to contain only functions ArgTypes -> TypeX
608 : //result is TypeX if unique, the set of TypeX as NotInferred if many.
609 : //return true if successful, otherwise false.
610 :
611 111 : if (is_basic_sort(PosType))
612 : {
613 0 : PosType=UnwindType(PosType);
614 : }
615 111 : if (is_function_sort(PosType))
616 : {
617 72 : const function_sort& s=down_cast<const function_sort>(PosType);
618 72 : const sort_expression_list& PosArgTypes=s.domain();
619 :
620 72 : if (PosArgTypes.size()!=ArgTypes.size())
621 : {
622 1 : return false;
623 : }
624 71 : sort_expression_list temp;
625 71 : if (TypeMatchL(PosArgTypes,ArgTypes,temp))
626 : {
627 65 : result=s.codomain();
628 65 : return true;
629 : }
630 : else
631 : {
632 : // Lift the argument of PosType.
633 6 : TypeMatchL(ArgTypes,ExpandNumTypesUpL(PosArgTypes),temp);
634 6 : result=s.codomain();
635 6 : return true;
636 : }
637 71 : }
638 39 : if (data::is_untyped_sort(data::sort_expression(PosType)))
639 : {
640 39 : result=PosType;
641 39 : return true;
642 : }
643 :
644 0 : sort_expression_list NewPosTypes;
645 0 : if (is_untyped_possible_sorts(PosType))
646 : {
647 0 : const untyped_possible_sorts& mps=down_cast<untyped_possible_sorts>(PosType);
648 0 : for (sort_expression_list PosTypes=mps.sorts(); !PosTypes.empty(); PosTypes=PosTypes.tail())
649 : {
650 0 : sort_expression NewPosType=PosTypes.front();
651 0 : if (is_basic_sort(NewPosType))
652 : {
653 0 : NewPosType=UnwindType(NewPosType);
654 : }
655 0 : if (is_function_sort(NewPosType))
656 : {
657 0 : const function_sort& s=down_cast<const function_sort>(NewPosType);
658 0 : const sort_expression_list& PosArgTypes=s.domain();
659 0 : if (PosArgTypes.size()!=ArgTypes.size())
660 : {
661 0 : continue;
662 : }
663 0 : sort_expression_list temp_list;
664 0 : if (TypeMatchL(PosArgTypes,ArgTypes,temp_list))
665 : {
666 0 : NewPosType=s.codomain();
667 : }
668 0 : }
669 0 : else if (!data::is_untyped_sort(data::sort_expression(NewPosType)))
670 : {
671 0 : continue;
672 : }
673 0 : NewPosTypes=detail::insert_sort_unique(NewPosTypes,NewPosType);
674 0 : }
675 0 : NewPosTypes=reverse(NewPosTypes);
676 0 : result=untyped_possible_sorts(sort_expression_list(NewPosTypes));
677 0 : return true;
678 : }
679 0 : return false;
680 0 : }
681 :
682 17024 : bool mcrl2::data::data_type_checker::UnifyMinType(const sort_expression& Type1, const sort_expression& Type2, sort_expression& result) const
683 : {
684 : //Find the minimal type that Unifies the 2. If not possible, return false.
685 17024 : if (!TypeMatchA(Type1,Type2,result))
686 : {
687 883 : if (!TypeMatchA(Type1,ExpandNumTypesUp(Type2),result))
688 : {
689 77 : if (!TypeMatchA(Type2,ExpandNumTypesUp(Type1),result))
690 : {
691 13 : return false;
692 : }
693 : }
694 : }
695 :
696 17011 : if (is_untyped_possible_sorts(result))
697 : {
698 74 : result=down_cast<untyped_possible_sorts>(result).sorts().front();
699 : }
700 17011 : return true;
701 : }
702 :
703 1094 : bool mcrl2::data::data_type_checker::MatchIf(const function_sort& type, sort_expression& result) const
704 : {
705 : //tries to sort out the types for if.
706 : //If some of the parameters are Pos,Nat, or Int do upcasting
707 :
708 1094 : sort_expression_list Args=type.domain();
709 1094 : sort_expression Res=type.codomain();
710 1094 : if (Args.size()!=3)
711 : {
712 0 : return false;
713 : }
714 1094 : Args=Args.tail();
715 :
716 1094 : if (!UnifyMinType(Res,Args.front(),Res))
717 : {
718 10 : return false;
719 : }
720 1084 : Args=Args.tail();
721 1084 : if (!UnifyMinType(Res,Args.front(),Res))
722 : {
723 0 : return false;
724 : }
725 :
726 4336 : result = function_sort({ sort_bool::bool_(), Res, Res }, Res);
727 1084 : return true;
728 1094 : }
729 :
730 9598 : bool mcrl2::data::data_type_checker::MatchEqNeqComparison(const function_sort& type, sort_expression& result) const
731 : {
732 : //tries to sort out the types for ==, !=, <, <=, >= and >.
733 : //If some of the parameters are Pos,Nat, or Int do upcasting.
734 :
735 9598 : sort_expression_list Args=type.domain();
736 9598 : if (Args.size()!=2)
737 : {
738 0 : return false;
739 : }
740 9598 : sort_expression Arg1=Args.front();
741 9598 : Args=Args.tail();
742 9598 : sort_expression Arg2=Args.front();
743 :
744 9598 : sort_expression Arg;
745 9598 : if (!UnifyMinType(Arg1,Arg2,Arg))
746 : {
747 2 : return false;
748 : }
749 :
750 28788 : result = function_sort({ Arg, Arg },sort_bool::bool_());
751 9596 : return true;
752 9598 : }
753 :
754 268 : bool mcrl2::data::data_type_checker::MatchSqrt(const function_sort& type, sort_expression& result) const
755 : {
756 : //tries to sort out the types for sqrt. There is only one option: sqrt:Nat->Nat.
757 :
758 268 : const sort_expression_list& Args=type.domain();
759 268 : if (Args.size()!=1)
760 : {
761 0 : return false;
762 : }
763 268 : const sort_expression& Arg=Args.front();
764 :
765 268 : if (Arg==sort_nat::nat())
766 : {
767 246 : result=function_sort(Args,sort_nat::nat());
768 246 : return true;
769 : }
770 22 : return false;
771 : }
772 :
773 :
774 :
775 1440 : bool mcrl2::data::data_type_checker::MatchListOpCons(const function_sort& type, sort_expression& result) const
776 : {
777 : //tries to sort out the types of Cons operations (SxList(S)->List(S))
778 : //If some of the parameters are Pos,Nat, or Int do upcasting.
779 :
780 1440 : sort_expression Res=type.codomain();
781 1440 : if (is_basic_sort(Res))
782 : {
783 0 : Res=UnwindType(Res);
784 : }
785 1440 : if (!sort_list::is_list(UnwindType(Res)))
786 : {
787 468 : return false;
788 : }
789 972 : Res=down_cast<container_sort>(Res).element_sort();
790 972 : sort_expression_list Args=type.domain();
791 972 : if (Args.size()!=2)
792 : {
793 0 : return false;
794 : }
795 972 : sort_expression Arg1=Args.front();
796 972 : Args=Args.tail();
797 972 : sort_expression Arg2=Args.front();
798 972 : if (is_basic_sort(Arg2))
799 : {
800 0 : Arg2=UnwindType(Arg2);
801 : }
802 972 : if (!sort_list::is_list(sort_expression(Arg2)))
803 : {
804 0 : return false;
805 : }
806 972 : Arg2=down_cast<container_sort>(Arg2).element_sort();
807 :
808 972 : sort_expression new_result;
809 972 : if (!UnifyMinType(Res,Arg1,new_result))
810 : {
811 0 : return false;
812 : }
813 :
814 972 : if (!UnifyMinType(new_result,Arg2,Res))
815 : {
816 0 : return false;
817 : }
818 :
819 2916 : result=function_sort({ Res,sort_list::list(sort_expression(Res)) },sort_list::list(sort_expression(Res)));
820 972 : return true;
821 1440 : }
822 :
823 80 : bool mcrl2::data::data_type_checker::MatchListOpSnoc(const function_sort& type, sort_expression& result) const
824 : {
825 : //tries to sort out the types of Cons operations (SxList(S)->List(S))
826 : //If some of the parameters are Pos,Nat, or Int do upcasting.
827 :
828 80 : sort_expression Res=type.codomain();
829 80 : if (is_basic_sort(Res))
830 : {
831 0 : Res=UnwindType(Res);
832 : }
833 80 : if (!sort_list::is_list(sort_expression(Res)))
834 : {
835 2 : return false;
836 : }
837 78 : Res=down_cast<container_sort>(Res).element_sort();
838 78 : sort_expression_list Args=type.domain();
839 78 : if (Args.size()!=2)
840 : {
841 0 : return false;
842 : }
843 78 : sort_expression Arg1=Args.front();
844 78 : if (is_basic_sort(Arg1))
845 : {
846 0 : Arg1=UnwindType(Arg1);
847 : }
848 78 : if (!sort_list::is_list(sort_expression(Arg1)))
849 : {
850 0 : return false;
851 : }
852 78 : Arg1=down_cast<container_sort>(Arg1).element_sort();
853 :
854 78 : Args=Args.tail();
855 78 : sort_expression Arg2=Args.front();
856 :
857 78 : sort_expression new_result;
858 78 : if (!UnifyMinType(Res,Arg1,new_result))
859 : {
860 0 : return false;
861 : }
862 :
863 78 : if (!UnifyMinType(new_result,Arg2,Res))
864 : {
865 0 : return false;
866 : }
867 :
868 234 : result=function_sort({ sort_list::list(sort_expression(Res)),Res },sort_list::list(sort_expression(Res)));
869 78 : return true;
870 80 : }
871 :
872 33 : bool mcrl2::data::data_type_checker::MatchListOpConcat(const function_sort& type, sort_expression& result) const
873 : {
874 : //tries to sort out the types of Concat operations (List(S)xList(S)->List(S))
875 : //If some of the parameters are Pos,Nat, or Int do upcasting.
876 :
877 33 : sort_expression Res=type.codomain();
878 33 : if (is_basic_sort(Res))
879 : {
880 0 : Res=UnwindType(Res);
881 : }
882 33 : if (!sort_list::is_list(sort_expression(Res)))
883 : {
884 14 : return false;
885 : }
886 19 : Res=down_cast<container_sort>(Res).element_sort();
887 19 : sort_expression_list Args=type.domain();
888 19 : if (Args.size()!=2)
889 : {
890 0 : return false;
891 : }
892 :
893 19 : sort_expression Arg1=Args.front();
894 19 : if (is_basic_sort(Arg1))
895 : {
896 1 : Arg1=UnwindType(Arg1);
897 : }
898 19 : if (!sort_list::is_list(sort_expression(Arg1)))
899 : {
900 1 : return false;
901 : }
902 18 : Arg1=down_cast<container_sort>(Arg1).element_sort();
903 :
904 18 : Args=Args.tail();
905 :
906 18 : sort_expression Arg2=Args.front();
907 18 : if (is_basic_sort(Arg2))
908 : {
909 0 : Arg2=UnwindType(Arg2);
910 : }
911 18 : if (!sort_list::is_list(sort_expression(Arg2)))
912 : {
913 0 : return false;
914 : }
915 18 : Arg2=down_cast<container_sort>(Arg2).element_sort();
916 :
917 18 : sort_expression new_result;
918 18 : if (!UnifyMinType(Res,Arg1,new_result))
919 : {
920 0 : return false;
921 : }
922 :
923 18 : if (!UnifyMinType(new_result,Arg2,Res))
924 : {
925 0 : return false;
926 : }
927 :
928 90 : result=function_sort({ sort_list::list(sort_expression(Res)), sort_list::list(sort_expression(Res)) },
929 108 : sort_list::list(sort_expression(Res)));
930 18 : return true;
931 33 : }
932 :
933 168 : bool mcrl2::data::data_type_checker::MatchListOpEltAt(const function_sort& type, sort_expression& result) const
934 : {
935 : //tries to sort out the types of EltAt operations (List(S)xNat->S)
936 : //If some of the parameters are Pos,Nat, or Int do upcasting.
937 :
938 168 : sort_expression Res=type.codomain();
939 168 : const sort_expression_list& Args=type.domain();
940 168 : if (Args.size()!=2)
941 : {
942 0 : return false;
943 : }
944 :
945 168 : sort_expression Arg1=Args.front();
946 168 : if (is_basic_sort(Arg1))
947 : {
948 0 : Arg1=UnwindType(Arg1);
949 : }
950 168 : if (!sort_list::is_list(sort_expression(Arg1)))
951 : {
952 0 : return false;
953 : }
954 168 : Arg1=down_cast<container_sort>(Arg1).element_sort();
955 :
956 168 : sort_expression new_result;
957 168 : if (!UnifyMinType(Res,Arg1,new_result))
958 : {
959 0 : return false;
960 : }
961 168 : Res=new_result;
962 :
963 504 : result=function_sort({ sort_list::list(sort_expression(Res)), sort_nat::nat() },Res);
964 168 : return true;
965 168 : }
966 :
967 120 : bool mcrl2::data::data_type_checker::MatchListOpHead(const function_sort& type, sort_expression& result) const
968 : {
969 : //tries to sort out the types of Cons operations (SxList(S)->List(S))
970 : //If some of the parameters are Pos,Nat, or Int do upcasting.
971 :
972 120 : sort_expression Res=type.codomain();
973 120 : const sort_expression_list& Args=type.domain();
974 120 : if (Args.size()!=1)
975 : {
976 0 : return false;
977 : }
978 120 : sort_expression Arg=Args.front();
979 120 : if (is_basic_sort(Arg))
980 : {
981 0 : Arg=UnwindType(Arg);
982 : }
983 120 : if (!sort_list::is_list(Arg))
984 : {
985 0 : return false;
986 : }
987 120 : Arg=down_cast<container_sort>(Arg).element_sort();
988 :
989 120 : sort_expression new_result;
990 120 : if (!UnifyMinType(Res,Arg,new_result))
991 : {
992 0 : return false;
993 : }
994 120 : Res=new_result;
995 :
996 240 : result=function_sort({ sort_expression(sort_list::list(sort_expression(Res))) },Res);
997 120 : return true;
998 120 : }
999 :
1000 176 : bool mcrl2::data::data_type_checker::MatchListOpTail(const function_sort& type, sort_expression& result) const
1001 : {
1002 : //tries to sort out the types of Cons operations (SxList(S)->List(S))
1003 : //If some of the parameters are Pos,Nat, or Int do upcasting.
1004 :
1005 176 : sort_expression Res=type.codomain();
1006 176 : if (is_basic_sort(Res))
1007 : {
1008 0 : Res=UnwindType(Res);
1009 : }
1010 176 : if (!sort_list::is_list(sort_expression(Res)))
1011 : {
1012 26 : return false;
1013 : }
1014 150 : Res=down_cast<container_sort>(Res).element_sort();
1015 150 : const sort_expression_list& Args=type.domain();
1016 150 : if (Args.size()!=1)
1017 : {
1018 0 : return false;
1019 : }
1020 150 : sort_expression Arg=Args.front();
1021 150 : if (is_basic_sort(Arg))
1022 : {
1023 0 : Arg=UnwindType(Arg);
1024 : }
1025 150 : if (!sort_list::is_list(sort_expression(Arg)))
1026 : {
1027 0 : return false;
1028 : }
1029 150 : Arg=down_cast<container_sort>(Arg).element_sort();
1030 :
1031 150 : sort_expression new_result;
1032 150 : if (!UnifyMinType(Res,Arg,new_result))
1033 : {
1034 0 : return false;
1035 : }
1036 150 : Res=new_result;
1037 :
1038 450 : result=function_sort(sort_expression_list({ sort_expression(sort_list::list(sort_expression(Res))) }),
1039 450 : sort_list::list(sort_expression(Res)));
1040 150 : return true;
1041 176 : }
1042 :
1043 : //Sets
1044 76 : bool mcrl2::data::data_type_checker::MatchSetOpSet2Bag(const function_sort& type, sort_expression& result) const
1045 : {
1046 : //tries to sort out the types of Set2Bag (Set(S)->Bag(s))
1047 : //If some of the parameters are Pos,Nat, or Int do upcasting.
1048 :
1049 :
1050 76 : sort_expression Res=type.codomain();
1051 76 : if (is_basic_sort(Res))
1052 : {
1053 0 : Res=UnwindType(Res);
1054 : }
1055 76 : if (!sort_bag::is_bag(sort_expression(Res)))
1056 : {
1057 22 : return false;
1058 : }
1059 54 : Res=down_cast<container_sort>(Res).element_sort();
1060 :
1061 54 : const sort_expression_list& Args=type.domain();
1062 54 : if (Args.size()!=1)
1063 : {
1064 0 : return false;
1065 : }
1066 :
1067 54 : sort_expression Arg=Args.front();
1068 54 : if (is_basic_sort(Arg))
1069 : {
1070 0 : Arg=UnwindType(Arg);
1071 : }
1072 54 : if (!sort_set::is_set(sort_expression(Arg)))
1073 : {
1074 6 : return false;
1075 : }
1076 48 : Arg=down_cast<container_sort>(Arg).element_sort();
1077 :
1078 48 : sort_expression new_result;
1079 48 : if (!UnifyMinType(Arg,Res,new_result))
1080 : {
1081 0 : return false;
1082 : }
1083 48 : Arg=new_result;
1084 :
1085 144 : result=function_sort(sort_expression_list({ sort_expression(sort_set::set_(sort_expression(Arg))) }),
1086 144 : sort_bag::bag(sort_expression(Arg)));
1087 48 : return true;
1088 76 : }
1089 :
1090 80 : bool mcrl2::data::data_type_checker::MatchSetConstructor(const function_sort& type, sort_expression& result) const
1091 : {
1092 : //tries to sort out the types of @set (Set(S)->Bool)->FSet(s))->Set(S)
1093 : //If some of the parameters are Pos,Nat, or Int do upcasting.
1094 80 : sort_expression Res=type.codomain();
1095 80 : if (is_basic_sort(Res))
1096 : {
1097 0 : Res=UnwindType(Res);
1098 : }
1099 80 : if (!sort_set::is_set(Res))
1100 : {
1101 6 : return false;
1102 : }
1103 74 : Res=down_cast<container_sort>(Res).element_sort();
1104 :
1105 74 : sort_expression_list Args=type.domain();
1106 74 : if (Args.size()!=2)
1107 : {
1108 0 : return false;
1109 : }
1110 :
1111 74 : sort_expression Arg1=Args.front();
1112 74 : if (is_basic_sort(Arg1))
1113 : {
1114 0 : Arg1=UnwindType(Arg1);
1115 : }
1116 74 : if (!is_function_sort(sort_expression(Arg1)))
1117 : {
1118 0 : return false;
1119 : }
1120 :
1121 74 : const sort_expression Arg12=down_cast<function_sort>(Arg1).codomain();
1122 :
1123 74 : sort_expression new_result;
1124 74 : if (!UnifyMinType(Arg12,sort_bool::bool_(),new_result))
1125 : {
1126 0 : return false;
1127 : }
1128 :
1129 74 : const sort_expression_list Arg11l=down_cast<function_sort>(Arg1).domain();
1130 74 : if (Arg11l.size()!=1)
1131 : {
1132 0 : return false;
1133 : }
1134 74 : const sort_expression& Arg11=Arg11l.front();
1135 :
1136 74 : if (!UnifyMinType(Arg11,Res,new_result))
1137 : {
1138 0 : return false;
1139 : }
1140 :
1141 :
1142 74 : Args.pop_front();
1143 74 : sort_expression Arg2=Args.front();
1144 74 : if (is_basic_sort(Arg2))
1145 : {
1146 0 : Arg2=UnwindType(Arg2);
1147 : }
1148 74 : if (!sort_fset::is_fset(Arg2))
1149 : {
1150 0 : return false;
1151 : }
1152 74 : sort_expression Arg21=down_cast<container_sort>(Arg2).element_sort();
1153 :
1154 74 : sort_expression new_result2;
1155 74 : if (!UnifyMinType(Arg21,new_result,new_result2))
1156 : {
1157 0 : return false;
1158 : }
1159 :
1160 148 : Arg1=function_sort({ new_result2 }, sort_bool::bool_());
1161 74 : Arg2=sort_fset::fset(new_result2);
1162 222 : result=function_sort({ Arg1, Arg2 }, sort_set::set_(new_result2));
1163 74 : return true;
1164 80 : }
1165 :
1166 0 : bool mcrl2::data::data_type_checker::MatchFalseFunction(const function_sort& type, sort_expression& result) const
1167 : {
1168 : //tries to sort out the types of @false (S->Bool)
1169 : //If some of the parameters are Pos,Nat, or Int do upcasting.
1170 :
1171 0 : result=type;
1172 0 : return true;
1173 :
1174 :
1175 :
1176 : }
1177 :
1178 24 : bool mcrl2::data::data_type_checker::MatchBagConstructor(const function_sort& type, sort_expression& result) const
1179 : {
1180 : //tries to sort out the types of @bag (Bag(S)->Bool)->FBag(s))->Bag(S)
1181 : //If some of the parameters are Pos,Nat, or Int do upcasting.
1182 :
1183 24 : sort_expression Res=type.codomain();
1184 24 : if (is_basic_sort(Res))
1185 : {
1186 0 : Res=UnwindType(Res);
1187 : }
1188 24 : if (!sort_bag::is_bag(Res))
1189 : {
1190 10 : return false;
1191 : }
1192 14 : Res=down_cast<container_sort>(Res).element_sort();
1193 :
1194 14 : sort_expression_list Args=type.domain();
1195 14 : if (Args.size()!=2)
1196 : {
1197 0 : return false;
1198 : }
1199 :
1200 14 : sort_expression Arg1=Args.front();
1201 14 : if (is_basic_sort(Arg1))
1202 : {
1203 0 : Arg1=UnwindType(Arg1);
1204 : }
1205 14 : if (!is_function_sort(sort_expression(Arg1)))
1206 : {
1207 0 : return false;
1208 : }
1209 :
1210 14 : const sort_expression Arg12=down_cast<function_sort>(Arg1).codomain();
1211 :
1212 14 : sort_expression new_result;
1213 14 : if (!UnifyMinType(Arg12,sort_nat::nat(),new_result))
1214 : {
1215 0 : return false;
1216 : }
1217 :
1218 14 : const sort_expression_list Arg11l=down_cast<function_sort>(Arg1).domain();
1219 14 : if (Arg11l.size()!=1)
1220 : {
1221 0 : return false;
1222 : }
1223 14 : const sort_expression& Arg11=Arg11l.front();
1224 :
1225 14 : if (!UnifyMinType(Arg11,Res,new_result))
1226 : {
1227 0 : return false;
1228 : }
1229 :
1230 :
1231 14 : Args.pop_front();
1232 14 : sort_expression Arg2=Args.front();
1233 14 : if (is_basic_sort(Arg2))
1234 : {
1235 0 : Arg2=UnwindType(Arg2);
1236 : }
1237 14 : if (!sort_fbag::is_fbag(Arg2))
1238 : {
1239 0 : return false;
1240 : }
1241 14 : sort_expression Arg21=down_cast<container_sort>(Arg2).element_sort();
1242 :
1243 14 : sort_expression new_result2;
1244 14 : if (!UnifyMinType(Arg21,new_result,new_result2))
1245 : {
1246 0 : return false;
1247 : }
1248 :
1249 28 : Arg1=function_sort(sort_expression_list({ new_result2 }),sort_nat::nat());
1250 14 : Arg2=sort_fbag::fbag(new_result2);
1251 42 : result=function_sort(sort_expression_list({ Arg1, Arg2 }), sort_bag::bag(new_result2));
1252 14 : return true;
1253 24 : }
1254 :
1255 :
1256 1024 : bool mcrl2::data::data_type_checker::MatchListSetBagOpIn(const function_sort& type, sort_expression& result) const
1257 : {
1258 : //tries to sort out the type of EltIn (SxList(S)->Bool or SxSet(S)->Bool or SxBag(S)->Bool)
1259 : //If some of the parameters are Pos,Nat, or Int do upcasting.
1260 :
1261 1024 : sort_expression_list Args=type.domain();
1262 1024 : if (Args.size()!=2)
1263 : {
1264 0 : return false;
1265 : }
1266 :
1267 1024 : sort_expression Arg1=Args.front();
1268 :
1269 1024 : Args=Args.tail();
1270 1024 : sort_expression Arg2=Args.front();
1271 1024 : if (is_basic_sort(Arg2))
1272 : {
1273 0 : Arg2=UnwindType(Arg2);
1274 : }
1275 1024 : if (!is_container_sort(Arg2))
1276 : {
1277 0 : return false;
1278 : }
1279 1024 : sort_expression Arg2s=down_cast<container_sort>(Arg2).element_sort();
1280 1024 : sort_expression Arg;
1281 1024 : if (!UnifyMinType(Arg1,Arg2s,Arg))
1282 : {
1283 0 : return false;
1284 : }
1285 :
1286 5120 : result=function_sort({ Arg, container_sort(down_cast<const container_sort>(Arg2).container_name(),Arg)},
1287 5120 : sort_bool::bool_());
1288 1024 : return true;
1289 1024 : }
1290 :
1291 84 : bool mcrl2::data::data_type_checker::match_fset_insert(const function_sort& type, sort_expression& result) const
1292 : {
1293 84 : sort_expression_list Args=type.domain();
1294 84 : if (Args.size()!=2)
1295 : {
1296 0 : return false;
1297 : }
1298 :
1299 84 : sort_expression Arg1=Args.front();
1300 :
1301 84 : Args=Args.tail();
1302 84 : sort_expression Arg2=Args.front();
1303 84 : if (is_basic_sort(Arg2))
1304 : {
1305 0 : Arg2=UnwindType(Arg2);
1306 : }
1307 84 : if (!is_container_sort(Arg2))
1308 : {
1309 0 : return false;
1310 : }
1311 84 : sort_expression Arg2s=down_cast<container_sort>(Arg2).element_sort();
1312 84 : sort_expression Arg;
1313 84 : if (!UnifyMinType(Arg1,Arg2s,Arg))
1314 : {
1315 0 : return false;
1316 : }
1317 :
1318 84 : const sort_expression fset_type=container_sort(down_cast<const container_sort>(Arg2).container_name(),Arg);
1319 252 : result=function_sort({ Arg, fset_type },fset_type);
1320 84 : return true;
1321 84 : }
1322 :
1323 8 : bool mcrl2::data::data_type_checker::match_fbag_cinsert(const function_sort& type, sort_expression& result) const
1324 : {
1325 8 : sort_expression_list Args=type.domain();
1326 8 : if (Args.size()!=3)
1327 : {
1328 0 : return false;
1329 : }
1330 :
1331 8 : sort_expression Arg1=Args.front();
1332 :
1333 8 : Args=Args.tail();
1334 8 : sort_expression Arg2=Args.front();
1335 8 : if (is_basic_sort(Arg2))
1336 : {
1337 8 : Arg2=UnwindType(Arg2);
1338 : }
1339 8 : Args=Args.tail();
1340 8 : sort_expression Arg3=Args.front();
1341 8 : if (is_basic_sort(Arg3))
1342 : {
1343 0 : Arg3=UnwindType(Arg3);
1344 : }
1345 :
1346 8 : sort_expression Arg2r;
1347 8 : if (!UnifyMinType(Arg2,sort_nat::nat(),Arg2r))
1348 : {
1349 0 : return false;
1350 : }
1351 :
1352 8 : if (!is_container_sort(Arg3))
1353 : {
1354 0 : return false;
1355 : }
1356 :
1357 8 : sort_expression Arg3s=down_cast<container_sort>(Arg3).element_sort();
1358 8 : sort_expression Arg3r;
1359 8 : if (!UnifyMinType(Arg1,Arg3s,Arg3r))
1360 : {
1361 0 : return false;
1362 : }
1363 :
1364 :
1365 8 : const sort_expression fbag_type=container_sort(down_cast<const container_sort>(Arg3).container_name(),Arg3r);
1366 32 : result=function_sort({ Arg3r, Arg2r, fbag_type },fbag_type);
1367 8 : return true;
1368 8 : }
1369 :
1370 16144 : bool mcrl2::data::data_type_checker::MatchSetBagOpUnionDiffIntersect(const function_sort& type, sort_expression& result) const
1371 : {
1372 : //tries to sort out the types of Set or Bag Union, Diff or Intersect
1373 : //operations (Set(S)xSet(S)->Set(S)). It can also be that this operation is
1374 : //performed on numbers. In this case we do nothing.
1375 : //If some of the parameters are Pos,Nat, or Int do upcasting.
1376 16144 : sort_expression Res=type.codomain();
1377 16144 : if (is_basic_sort(Res))
1378 : {
1379 8874 : Res=UnwindType(Res);
1380 : }
1381 16144 : if (data::detail::IsNumericType(Res))
1382 : {
1383 8874 : result=type;
1384 8874 : return true;
1385 : }
1386 21592 : if (!(sort_set::is_set(sort_expression(Res))||sort_bag::is_bag(sort_expression(Res))||
1387 14322 : sort_fset::is_fset(sort_expression(Res))||sort_fbag::is_fbag(sort_expression(Res))))
1388 : {
1389 6864 : return false;
1390 : }
1391 406 : sort_expression_list Args=type.domain();
1392 406 : if (Args.size()!=2)
1393 : {
1394 0 : return false;
1395 : }
1396 :
1397 406 : sort_expression Arg1=Args.front();
1398 406 : if (is_basic_sort(Arg1))
1399 : {
1400 0 : Arg1=UnwindType(Arg1);
1401 : }
1402 406 : if (data::detail::IsNumericType(Arg1))
1403 : {
1404 0 : result=type;
1405 0 : return true;
1406 : }
1407 1000 : if (!(sort_set::is_set(sort_expression(Arg1))||sort_bag::is_bag(sort_expression(Arg1))||
1408 594 : sort_fset::is_fset(sort_expression(Arg1))||sort_fbag::is_fbag(sort_expression(Arg1))))
1409 : {
1410 0 : return false;
1411 : }
1412 :
1413 406 : Args=Args.tail();
1414 :
1415 406 : sort_expression Arg2=Args.front();
1416 406 : if (is_basic_sort(Arg2))
1417 : {
1418 0 : Arg2=UnwindType(Arg2);
1419 : }
1420 406 : if (detail::IsNumericType(Arg2))
1421 : {
1422 0 : result=type;
1423 0 : return true;
1424 : }
1425 1000 : if (!(sort_set::is_set(sort_expression(Arg2))||sort_bag::is_bag(sort_expression(Arg2))||
1426 594 : sort_fset::is_fset(sort_expression(Arg2))||sort_fbag::is_fbag(sort_expression(Arg2))))
1427 : {
1428 0 : return false;
1429 : }
1430 :
1431 : // If one of the argumenst is an fset/fbag and the other a set/bag, lift it to match the bag/set.
1432 406 : if (sort_set::is_set(sort_expression(Arg1)) && sort_fset::is_fset(sort_expression(Arg2)))
1433 : {
1434 0 : Arg2=sort_set::set_(container_sort(Arg2).element_sort());
1435 : }
1436 :
1437 406 : if (sort_fset::is_fset(sort_expression(Arg1)) && sort_set::is_set(sort_expression(Arg2)))
1438 : {
1439 0 : Arg1=sort_set::set_(container_sort(Arg1).element_sort());
1440 : }
1441 :
1442 406 : if (sort_bag::is_bag(sort_expression(Arg1)) && sort_fbag::is_fbag(sort_expression(Arg2)))
1443 : {
1444 0 : Arg2=sort_bag::bag(container_sort(Arg2).element_sort());
1445 : }
1446 :
1447 406 : if (sort_fbag::is_fbag(sort_expression(Arg1)) && sort_bag::is_bag(sort_expression(Arg2)))
1448 : {
1449 0 : Arg1=sort_bag::bag(container_sort(Arg1).element_sort());
1450 : }
1451 :
1452 406 : sort_expression temp_result;
1453 406 : if (!UnifyMinType(Res,Arg1,temp_result))
1454 : {
1455 0 : return false;
1456 : }
1457 :
1458 406 : if (!UnifyMinType(temp_result,Arg2,Res))
1459 : {
1460 0 : return false;
1461 : }
1462 :
1463 1218 : result=function_sort({ Res,Res },Res);
1464 406 : return true;
1465 16144 : }
1466 :
1467 3012 : bool mcrl2::data::data_type_checker::MatchSetOpSetCompl(const function_sort& type, sort_expression& result) const
1468 : {
1469 : //tries to sort out the types of SetCompl operation (Set(S)->Set(S))
1470 : //If some of the parameters are Pos,Nat, or Int do upcasting.
1471 :
1472 3012 : sort_expression Res=type.codomain();
1473 3012 : if (is_basic_sort(Res))
1474 : {
1475 2152 : Res=UnwindType(Res);
1476 : }
1477 : // if (detail::IsNumericType(Res))
1478 3012 : if (Res==sort_bool::bool_())
1479 : {
1480 2100 : result=type;
1481 2100 : return true;
1482 : }
1483 :
1484 912 : const sort_expression_list& Args=type.domain();
1485 912 : if (Args.size()!=1)
1486 : {
1487 0 : return false;
1488 : }
1489 :
1490 912 : sort_expression Arg=Args.front();
1491 912 : if (is_basic_sort(Arg))
1492 : {
1493 868 : Arg=UnwindType(Arg);
1494 : }
1495 : // if (detail::IsNumericType(Arg))
1496 912 : if (Arg==sort_bool::bool_())
1497 : {
1498 868 : result=type;
1499 868 : return true;
1500 : }
1501 44 : if (!sort_set::is_set(sort_expression(Res)))
1502 : {
1503 30 : return false;
1504 : }
1505 14 : Res=down_cast<container_sort>(Res).element_sort();
1506 14 : if (!sort_set::is_set(sort_expression(Arg)))
1507 : {
1508 0 : return false;
1509 : }
1510 14 : Arg=down_cast<container_sort>(Arg).element_sort();
1511 :
1512 14 : sort_expression temp_result;
1513 14 : if (!UnifyMinType(Res,Arg,temp_result))
1514 : {
1515 0 : return false;
1516 : }
1517 14 : Res=temp_result;
1518 :
1519 28 : result=function_sort({ sort_expression(sort_set::set_(sort_expression(Res))) },sort_set::set_(sort_expression(Res)));
1520 14 : return true;
1521 3012 : }
1522 :
1523 : //Bags
1524 0 : bool mcrl2::data::data_type_checker::MatchBagOpBag2Set(const function_sort& type, sort_expression& result) const
1525 : {
1526 : //tries to sort out the types of Bag2Set (Bag(S)->Set(S))
1527 : //If some of the parameters are Pos,Nat, or Int do upcasting.
1528 :
1529 :
1530 0 : sort_expression Res=type.codomain();
1531 0 : if (is_basic_sort(Res))
1532 : {
1533 0 : Res=UnwindType(Res);
1534 : }
1535 0 : if (!sort_set::is_set(sort_expression(Res)))
1536 : {
1537 0 : return false;
1538 : }
1539 0 : Res=down_cast<container_sort>(Res).element_sort();
1540 :
1541 0 : const sort_expression_list& Args=type.domain();
1542 0 : if (Args.size()!=1)
1543 : {
1544 0 : return false;
1545 : }
1546 :
1547 0 : sort_expression Arg=Args.front();
1548 0 : if (is_basic_sort(Arg))
1549 : {
1550 0 : Arg=UnwindType(Arg);
1551 : }
1552 0 : if (!sort_bag::is_bag(sort_expression(Arg)))
1553 : {
1554 0 : return false;
1555 : }
1556 0 : Arg=down_cast<container_sort>(Arg).element_sort();
1557 :
1558 0 : sort_expression temp_result;
1559 0 : if (!UnifyMinType(Arg,Res,temp_result))
1560 : {
1561 0 : return false;
1562 : }
1563 0 : Arg=temp_result;
1564 :
1565 0 : result=function_sort({ sort_expression(sort_bag::bag(sort_expression(Arg))) },sort_set::set_(sort_expression(Arg)));
1566 0 : return true;
1567 0 : }
1568 :
1569 128 : bool mcrl2::data::data_type_checker::MatchBagOpBagCount(const function_sort& type, sort_expression& result) const
1570 : {
1571 : //tries to sort out the types of BagCount (SxBag(S)->Nat)
1572 : //If some of the parameters are Pos,Nat, or Int do upcasting.
1573 :
1574 : //If the second argument is not a Bag, don't match
1575 :
1576 128 : if (!is_function_sort(type))
1577 : {
1578 0 : result=type;
1579 0 : return true;
1580 : }
1581 128 : sort_expression_list Args=type.domain();
1582 128 : if (!(Args.size()==2))
1583 : {
1584 0 : result=type;
1585 0 : return true;
1586 : }
1587 :
1588 128 : sort_expression Arg1=Args.front();
1589 :
1590 128 : Args=Args.tail();
1591 128 : sort_expression Arg2=Args.front();
1592 128 : if (is_basic_sort(Arg2))
1593 : {
1594 0 : Arg2=UnwindType(Arg2);
1595 : }
1596 128 : if (!sort_bag::is_bag(sort_expression(Arg2)))
1597 : {
1598 24 : result=type;
1599 24 : return true;
1600 : }
1601 104 : Arg2=down_cast<container_sort>(Arg2).element_sort();
1602 :
1603 104 : sort_expression Arg;
1604 104 : if (!UnifyMinType(Arg1,Arg2,Arg))
1605 : {
1606 0 : return false;
1607 : }
1608 :
1609 312 : result=function_sort(sort_expression_list({ Arg,sort_bag::bag(sort_expression(Arg)) }),sort_nat::nat());
1610 104 : return true;
1611 128 : }
1612 :
1613 :
1614 130 : bool mcrl2::data::data_type_checker::MatchFuncUpdate(const function_sort& type, sort_expression& result) const
1615 : {
1616 : //tries to sort out the types of FuncUpdate ((A->B)xAxB->(A->B))
1617 : //If some of the parameters are Pos,Nat, or Int do upcasting.
1618 :
1619 130 : sort_expression_list Args=type.domain();
1620 130 : if (Args.size()!=3)
1621 : {
1622 0 : return false;
1623 : }
1624 130 : function_sort Arg1=down_cast<function_sort>(Args.front());
1625 130 : Args=Args.tail();
1626 130 : sort_expression Arg2=Args.front();
1627 130 : Args=Args.tail();
1628 130 : sort_expression Arg3=Args.front();
1629 130 : const sort_expression& Res=type.codomain();
1630 130 : if (!is_function_sort(Res))
1631 : {
1632 27 : return false;
1633 : }
1634 :
1635 103 : sort_expression temp_result;
1636 103 : if (!UnifyMinType(Arg1,Res,temp_result))
1637 : {
1638 0 : return false;
1639 : }
1640 103 : Arg1 = atermpp::down_cast<function_sort>(UnwindType(temp_result));
1641 :
1642 : // determine A and B from Arg1:
1643 103 : sort_expression_list LA=Arg1.domain();
1644 103 : if (LA.size()!=1)
1645 : {
1646 0 : return false;
1647 : }
1648 103 : const sort_expression& A=LA.front();
1649 103 : sort_expression B=Arg1.codomain();
1650 :
1651 103 : if (!UnifyMinType(A,Arg2,temp_result))
1652 : {
1653 1 : return false;
1654 : }
1655 102 : if (!UnifyMinType(B,Arg3,temp_result))
1656 : {
1657 0 : return false;
1658 : }
1659 :
1660 408 : result=function_sort(sort_expression_list({ Arg1,A,B}) ,Arg1);
1661 102 : return true;
1662 130 : }
1663 :
1664 :
1665 :
1666 210 : bool mcrl2::data::data_type_checker::MaximumType(const sort_expression& Type1, const sort_expression& Type2, sort_expression& result) const
1667 : {
1668 : // if Type1 is convertible into Type2 or vice versa, the most general
1669 : // of these types are returned in result. If no conversion is possible false is returned
1670 : // and result is not changed. Conversions only take place between numerical types
1671 210 : if (EqTypesA(Type1,Type2))
1672 : {
1673 200 : result=Type1;
1674 200 : return true;
1675 : }
1676 10 : if (data::is_untyped_sort(data::sort_expression(Type1)))
1677 : {
1678 0 : result=Type2;
1679 0 : return true;
1680 : }
1681 10 : if (data::is_untyped_sort(data::sort_expression(Type2)))
1682 : {
1683 0 : result=Type1;
1684 0 : return true;
1685 : }
1686 10 : if (EqTypesA(Type1,sort_real::real_()))
1687 : {
1688 0 : if (EqTypesA(Type2,sort_int::int_()))
1689 : {
1690 0 : result=Type1;
1691 0 : return true;
1692 : }
1693 0 : if (EqTypesA(Type2,sort_nat::nat()))
1694 : {
1695 0 : result=Type1;
1696 0 : return true;
1697 : }
1698 0 : if (EqTypesA(Type2,sort_pos::pos()))
1699 : {
1700 0 : result=Type1;
1701 0 : return true;
1702 : }
1703 0 : return false;
1704 : }
1705 10 : if (EqTypesA(Type1,sort_int::int_()))
1706 : {
1707 0 : if (EqTypesA(Type2,sort_real::real_()))
1708 : {
1709 0 : result=Type2;
1710 0 : return true;
1711 : }
1712 0 : if (EqTypesA(Type2,sort_nat::nat()))
1713 : {
1714 0 : result=Type1;
1715 0 : return true;
1716 : }
1717 0 : if (EqTypesA(Type2,sort_pos::pos()))
1718 : {
1719 0 : result=Type1;
1720 0 : return true;
1721 : }
1722 0 : return false;
1723 : }
1724 10 : if (EqTypesA(Type1,sort_nat::nat()))
1725 : {
1726 8 : if (EqTypesA(Type2,sort_real::real_()))
1727 : {
1728 0 : result=Type2;
1729 0 : return true;
1730 : }
1731 8 : if (EqTypesA(Type2,sort_int::int_()))
1732 : {
1733 0 : result=Type2;
1734 0 : return true;
1735 : }
1736 8 : if (EqTypesA(Type2,sort_pos::pos()))
1737 : {
1738 8 : result=Type1;
1739 8 : return true;
1740 : }
1741 0 : return false;
1742 : }
1743 2 : if (EqTypesA(Type1,sort_pos::pos()))
1744 : {
1745 2 : if (EqTypesA(Type2,sort_real::real_()))
1746 : {
1747 0 : result=Type2;
1748 0 : return true;
1749 : }
1750 2 : if (EqTypesA(Type2,sort_int::int_()))
1751 : {
1752 2 : result=Type2;
1753 2 : return true;
1754 : }
1755 0 : if (EqTypesA(Type2,sort_nat::nat()))
1756 : {
1757 0 : result=Type2;
1758 0 : return true;
1759 : }
1760 0 : return false;
1761 : }
1762 0 : return false;
1763 : }
1764 :
1765 6 : sort_expression_list mcrl2::data::data_type_checker::ExpandNumTypesUpL(const sort_expression_list& type_list) const
1766 : {
1767 6 : sort_expression_vector result;
1768 12 : for(sort_expression_list::const_iterator i=type_list.begin(); i!=type_list.end(); ++i)
1769 : {
1770 6 : result.push_back(ExpandNumTypesUp(*i));
1771 : }
1772 12 : return sort_expression_list(result.begin(),result.end());
1773 6 : }
1774 :
1775 7244 : sort_expression mcrl2::data::data_type_checker::ExpandNumTypesUp(sort_expression Type) const
1776 : {
1777 : //Expand Type to possible bigger types.
1778 7244 : if (data::is_untyped_sort(data::sort_expression(Type)))
1779 : {
1780 59 : return Type;
1781 : }
1782 7185 : if (EqTypesA(sort_pos::pos(),Type))
1783 : {
1784 12035 : return untyped_possible_sorts(sort_expression_list({ sort_pos::pos(), sort_nat::nat(), sort_int::int_(),sort_real::real_() } ));
1785 : }
1786 4778 : if (EqTypesA(sort_nat::nat(),Type))
1787 : {
1788 3220 : return untyped_possible_sorts(sort_expression_list({ sort_nat::nat(), sort_int::int_(),sort_real::real_() } ));
1789 : }
1790 3973 : if (EqTypesA(sort_int::int_(),Type))
1791 : {
1792 312 : return untyped_possible_sorts(sort_expression_list({ sort_int::int_(), sort_real::real_() } ));
1793 : }
1794 3869 : if (is_basic_sort(Type))
1795 : {
1796 934 : return Type;
1797 : }
1798 2935 : if (is_container_sort(Type))
1799 : {
1800 1000 : const container_sort& s=down_cast<container_sort>(Type);
1801 1000 : const container_type& ConsType = s.container_name();
1802 1000 : if (is_list_container(ConsType))
1803 : {
1804 670 : return container_sort(s.container_name(),ExpandNumTypesUp(s.element_sort()));
1805 : }
1806 :
1807 330 : if (is_set_container(ConsType))
1808 : {
1809 66 : return container_sort(s.container_name(),ExpandNumTypesUp(s.element_sort()));
1810 : }
1811 :
1812 264 : if (is_bag_container(ConsType))
1813 : {
1814 27 : return container_sort(s.container_name(),ExpandNumTypesUp(s.element_sort()));
1815 : }
1816 :
1817 237 : if (is_fset_container(ConsType))
1818 : {
1819 94 : const sort_expression expanded_sorts=ExpandNumTypesUp(s.element_sort());
1820 564 : return untyped_possible_sorts(sort_expression_list({
1821 94 : container_sort(s.container_name(),expanded_sorts),
1822 564 : container_sort(set_container(),expanded_sorts) }));
1823 94 : }
1824 :
1825 143 : if (is_fbag_container(ConsType))
1826 : {
1827 143 : const sort_expression expanded_sorts=ExpandNumTypesUp(s.element_sort());
1828 858 : return untyped_possible_sorts(sort_expression_list({
1829 143 : container_sort(s.container_name(),expanded_sorts),
1830 858 : container_sort(bag_container(),expanded_sorts) }));
1831 143 : }
1832 : }
1833 :
1834 1935 : if (is_structured_sort(Type))
1835 : {
1836 6 : return Type;
1837 : }
1838 :
1839 1929 : if (is_function_sort(Type))
1840 : {
1841 1890 : const function_sort& t=down_cast<const function_sort>(Type);
1842 : //the argument types, and if the resulting type is SortArrow -- recursively
1843 1890 : sort_expression_list NewTypeList;
1844 5325 : for (sort_expression_list TypeList=t.domain(); !TypeList.empty(); TypeList=TypeList.tail())
1845 : {
1846 3435 : NewTypeList.push_front(ExpandNumTypesUp(UnwindType(TypeList.front())));
1847 1890 : }
1848 1890 : const sort_expression& ResultType=t.codomain();
1849 1890 : if (!is_function_sort(ResultType))
1850 : {
1851 1867 : return function_sort(reverse(NewTypeList),ResultType);
1852 : }
1853 : else
1854 : {
1855 23 : return function_sort(reverse(NewTypeList),ExpandNumTypesUp(UnwindType(ResultType)));
1856 : }
1857 1890 : }
1858 :
1859 39 : return Type;
1860 : }
1861 :
1862 63 : sort_expression mcrl2::data::data_type_checker::ExpandNumTypesDown(sort_expression Type) const
1863 : {
1864 : // Expand Numeric types down
1865 63 : if (data::is_untyped_sort(Type))
1866 : {
1867 0 : return Type;
1868 : }
1869 63 : if (is_basic_sort(Type))
1870 : {
1871 1 : Type=UnwindType(Type);
1872 : }
1873 :
1874 63 : bool function=false;
1875 63 : sort_expression_list Args;
1876 63 : if (is_function_sort(Type))
1877 : {
1878 62 : const function_sort& fs=down_cast<const function_sort>(Type);
1879 62 : function=true;
1880 62 : Args=fs.domain();
1881 62 : Type=fs.codomain();
1882 : }
1883 :
1884 63 : if (EqTypesA(sort_real::real_(),Type))
1885 : {
1886 0 : Type=untyped_possible_sorts(sort_expression_list({ sort_pos::pos(),sort_nat::nat(),sort_int::int_(),sort_real::real_() }));
1887 : }
1888 63 : if (EqTypesA(sort_int::int_(),Type))
1889 : {
1890 104 : Type=untyped_possible_sorts(sort_expression_list({ sort_pos::pos(),sort_nat::nat(),sort_int::int_() } ));
1891 : }
1892 63 : if (EqTypesA(sort_nat::nat(),Type))
1893 : {
1894 15 : Type=untyped_possible_sorts(sort_expression_list({ sort_pos::pos(),sort_nat::nat() } ));
1895 : }
1896 63 : if (is_container_sort(Type))
1897 : {
1898 1 : const container_sort& s=down_cast<container_sort>(Type);
1899 1 : const container_type& ConsType = s.container_name();
1900 1 : if (is_list_container(ConsType))
1901 : {
1902 1 : Type=container_sort(s.container_name(),ExpandNumTypesDown(s.element_sort()));
1903 : }
1904 :
1905 1 : if (is_fset_container(ConsType))
1906 : {
1907 0 : Type=container_sort(s.container_name(),ExpandNumTypesDown(s.element_sort()));
1908 : }
1909 :
1910 1 : if (is_fbag_container(ConsType))
1911 : {
1912 0 : Type=container_sort(s.container_name(),ExpandNumTypesDown(s.element_sort()));
1913 : }
1914 :
1915 1 : if (is_set_container(ConsType))
1916 : {
1917 0 : const sort_expression shrinked_sorts=ExpandNumTypesDown(s.element_sort());
1918 0 : Type=untyped_possible_sorts(sort_expression_list({
1919 0 : container_sort(s.container_name(),shrinked_sorts),
1920 0 : container_sort(set_container(),shrinked_sorts) } ));
1921 0 : }
1922 :
1923 1 : if (is_bag_container(ConsType))
1924 : {
1925 0 : const sort_expression shrinked_sorts=ExpandNumTypesDown(s.element_sort());
1926 0 : Type=untyped_possible_sorts(sort_expression_list({
1927 0 : container_sort(s.container_name(),shrinked_sorts),
1928 0 : container_sort(bag_container(),shrinked_sorts) } ));
1929 0 : }
1930 : }
1931 :
1932 126 : return (function)?function_sort(Args,Type):Type;
1933 63 : }
1934 :
1935 :
1936 116 : bool mcrl2::data::data_type_checker::InTypesA(const sort_expression& Type, sort_expression_list Types) const
1937 : {
1938 251 : for (const sort_expression& s: Types)
1939 : {
1940 136 : if (EqTypesA(Type,s))
1941 : {
1942 1 : return true;
1943 : }
1944 : }
1945 115 : return false;
1946 : }
1947 :
1948 323278 : bool mcrl2::data::data_type_checker::EqTypesA(const sort_expression& Type1, const sort_expression& Type2) const
1949 : {
1950 323278 : if (Type1==Type2)
1951 : {
1952 170658 : return true;
1953 : }
1954 :
1955 152620 : return UnwindType(Type1)==UnwindType(Type2);
1956 : }
1957 :
1958 0 : bool mcrl2::data::data_type_checker::InTypesL(const sort_expression_list& Type, term_list<sort_expression_list> Types) const
1959 : {
1960 0 : for (const sort_expression_list&l: Types)
1961 : {
1962 0 : if (EqTypesL(Type,l))
1963 : {
1964 0 : return true;
1965 : }
1966 : }
1967 0 : return false;
1968 : }
1969 :
1970 0 : bool mcrl2::data::data_type_checker::EqTypesL(sort_expression_list Type1, sort_expression_list Type2) const
1971 : {
1972 0 : if (Type1==Type2)
1973 : {
1974 0 : return true;
1975 : }
1976 0 : if (Type1.size()!=Type2.size())
1977 : {
1978 0 : return false;
1979 : }
1980 0 : sort_expression_list::const_iterator i=Type1.begin();
1981 0 : for (const sort_expression& s: Type2)
1982 : {
1983 0 : if (!EqTypesA(*i,s))
1984 : {
1985 0 : return false;
1986 : }
1987 0 : ++i;
1988 : }
1989 0 : return true;
1990 : }
1991 :
1992 59140 : sort_expression mcrl2::data::data_type_checker::determine_allowed_type(const data_expression& d, const sort_expression& proposed_type) const
1993 : {
1994 59140 : if (is_variable(d))
1995 : {
1996 0 : variable v(d);
1997 : // Set the type to one option in possible sorts, if there are more options.
1998 0 : const sort_expression new_type=detail::replace_possible_sorts(proposed_type);
1999 0 : v=variable(v.name(),new_type);
2000 0 : return new_type;
2001 0 : }
2002 :
2003 59140 : assert(proposed_type.defined());
2004 :
2005 59140 : sort_expression Type=proposed_type;
2006 : // If d is not a variable it is an untyped name, or a function symbol.
2007 59140 : const core::identifier_string& data_term_name=data::is_untyped_identifier(d)?
2008 20048 : atermpp::down_cast<const untyped_identifier>(d).name():
2009 39092 : (down_cast<const data::function_symbol>(d).name());
2010 :
2011 59140 : if (data::detail::if_symbol::is_symbol(data_term_name))
2012 : {
2013 1094 : sort_expression NewType;
2014 1094 : if (!MatchIf(atermpp::down_cast<function_sort>(Type), NewType))
2015 : {
2016 10 : throw mcrl2::runtime_error("The function if has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2017 : }
2018 1084 : Type=NewType;
2019 1094 : }
2020 :
2021 59130 : if (data::detail::equal_symbol::is_symbol(data_term_name)
2022 53248 : || data::detail::not_equal_symbol::is_symbol(data_term_name)
2023 52992 : || data::detail::less_symbol::is_symbol(data_term_name)
2024 50908 : || data::detail::less_equal_symbol::is_symbol(data_term_name)
2025 50388 : || data::detail::greater_symbol::is_symbol(data_term_name)
2026 112378 : || data::detail::greater_equal_symbol::is_symbol(data_term_name)
2027 : )
2028 : {
2029 9598 : sort_expression NewType;
2030 9598 : if (!MatchEqNeqComparison(atermpp::down_cast<function_sort>(Type), NewType))
2031 : {
2032 2 : throw mcrl2::runtime_error("The function " + core::pp(data_term_name) + " has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2033 : }
2034 9596 : Type=NewType;
2035 9598 : }
2036 :
2037 59128 : if (sort_nat::sqrt_name()==data_term_name)
2038 : {
2039 268 : sort_expression NewType;
2040 268 : if (!MatchSqrt(atermpp::down_cast<function_sort>(Type), NewType))
2041 : {
2042 22 : throw mcrl2::runtime_error("The function sqrt has an incorrect argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2043 : }
2044 246 : Type=NewType;
2045 268 : }
2046 :
2047 59106 : if (sort_list::cons_name()==data_term_name)
2048 : {
2049 1440 : sort_expression NewType;
2050 1440 : if (!MatchListOpCons(atermpp::down_cast<function_sort>(Type), NewType))
2051 : {
2052 468 : throw mcrl2::runtime_error("The function |> has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2053 : }
2054 972 : Type=NewType;
2055 1440 : }
2056 :
2057 58638 : if (sort_list::snoc_name()==data_term_name)
2058 : {
2059 80 : sort_expression NewType;
2060 80 : if (!MatchListOpSnoc(atermpp::down_cast<function_sort>(Type), NewType))
2061 : {
2062 2 : throw mcrl2::runtime_error("The function <| has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2063 : }
2064 78 : Type=NewType;
2065 80 : }
2066 :
2067 58636 : if (sort_list::concat_name()==data_term_name)
2068 : {
2069 33 : sort_expression NewType;
2070 33 : if (!MatchListOpConcat(atermpp::down_cast<function_sort>(Type), NewType))
2071 : {
2072 15 : throw mcrl2::runtime_error("The function ++ has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2073 : }
2074 18 : Type=NewType;
2075 33 : }
2076 :
2077 58621 : if (sort_list::element_at_name()==data_term_name)
2078 : {
2079 168 : sort_expression NewType;
2080 168 : if (!MatchListOpEltAt(atermpp::down_cast<function_sort>(Type), NewType))
2081 : {
2082 0 : throw mcrl2::runtime_error("The function @ has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2083 : }
2084 168 : Type=NewType;
2085 168 : }
2086 :
2087 117158 : if (sort_list::head_name()==data_term_name||
2088 58537 : sort_list::rhead_name()==data_term_name)
2089 : {
2090 :
2091 120 : sort_expression NewType;
2092 120 : if (!MatchListOpHead(atermpp::down_cast<function_sort>(Type), NewType))
2093 : {
2094 0 : throw mcrl2::runtime_error("The function {R,L}head has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2095 : }
2096 120 : Type=NewType;
2097 120 : }
2098 :
2099 117102 : if (sort_list::tail_name()==data_term_name||
2100 58481 : sort_list::rtail_name()==data_term_name)
2101 : {
2102 176 : sort_expression NewType;
2103 176 : if (!MatchListOpTail(atermpp::down_cast<function_sort>(Type), NewType))
2104 : {
2105 26 : throw mcrl2::runtime_error("The function {R,L}tail has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2106 : }
2107 150 : Type=NewType;
2108 176 : }
2109 :
2110 58595 : if (sort_bag::set2bag_name()==data_term_name)
2111 : {
2112 76 : sort_expression NewType;
2113 76 : if (!MatchSetOpSet2Bag(atermpp::down_cast<function_sort>(Type), NewType))
2114 : {
2115 28 : throw mcrl2::runtime_error("The function Set2Bag has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2116 : }
2117 48 : Type=NewType;
2118 76 : }
2119 :
2120 58567 : if (sort_list::in_name()==data_term_name)
2121 : {
2122 1024 : sort_expression NewType;
2123 1024 : if (!MatchListSetBagOpIn(atermpp::down_cast<function_sort>(Type), NewType))
2124 : {
2125 0 : throw mcrl2::runtime_error("The function {List,Set,Bag}In has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2126 : }
2127 1024 : Type=NewType;
2128 1024 : }
2129 :
2130 106344 : if (sort_set::union_name()==data_term_name||
2131 106344 : sort_set::difference_name()==data_term_name||
2132 44073 : sort_set::intersection_name()==data_term_name)
2133 : {
2134 16144 : sort_expression NewType;
2135 16144 : if (!MatchSetBagOpUnionDiffIntersect(atermpp::down_cast<function_sort>(Type), NewType))
2136 : {
2137 6864 : throw mcrl2::runtime_error("The function {Set,Bag}{Union,Difference,Intersect} has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2138 : }
2139 9280 : Type=NewType;
2140 16144 : }
2141 :
2142 :
2143 51703 : if (sort_fset::insert_name()==data_term_name)
2144 : {
2145 84 : sort_expression NewType;
2146 84 : if (!match_fset_insert(atermpp::down_cast<function_sort>(Type), NewType))
2147 : {
2148 0 : throw mcrl2::runtime_error("Set enumeration has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2149 : }
2150 84 : Type=NewType;
2151 84 : }
2152 :
2153 51703 : if (sort_fbag::cinsert_name()==data_term_name)
2154 : {
2155 8 : sort_expression NewType;
2156 8 : if (!match_fbag_cinsert(atermpp::down_cast<function_sort>(Type), NewType))
2157 : {
2158 0 : throw mcrl2::runtime_error("Bag enumeration has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2159 : }
2160 8 : Type=NewType;
2161 8 : }
2162 :
2163 :
2164 :
2165 51703 : if (sort_set::complement_name()==data_term_name)
2166 : {
2167 3012 : sort_expression NewType;
2168 3012 : if (!MatchSetOpSetCompl(atermpp::down_cast<function_sort>(Type), NewType))
2169 : {
2170 30 : throw mcrl2::runtime_error("The function SetCompl has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2171 : }
2172 2982 : Type=NewType;
2173 3012 : }
2174 :
2175 51673 : if (sort_bag::bag2set_name()==data_term_name)
2176 : {
2177 0 : sort_expression NewType;
2178 0 : if (!MatchBagOpBag2Set(atermpp::down_cast<function_sort>(Type), NewType))
2179 : {
2180 0 : throw mcrl2::runtime_error("The function Bag2Set has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2181 : }
2182 0 : Type=NewType;
2183 0 : }
2184 :
2185 51673 : if (sort_bag::count_name()==data_term_name)
2186 : {
2187 128 : sort_expression NewType;
2188 128 : if (!MatchBagOpBagCount(atermpp::down_cast<function_sort>(Type), NewType))
2189 : {
2190 0 : throw mcrl2::runtime_error("The function BagCount has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2191 : }
2192 128 : Type=NewType;
2193 128 : }
2194 :
2195 :
2196 51673 : if (data::function_update_name()==data_term_name)
2197 : {
2198 130 : sort_expression NewType;
2199 130 : if (!MatchFuncUpdate(atermpp::down_cast<function_sort>(Type), NewType))
2200 : {
2201 28 : throw mcrl2::runtime_error("Function update has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2202 : }
2203 102 : Type=NewType;
2204 130 : }
2205 :
2206 51645 : if (sort_set::constructor_name()==data_term_name)
2207 : {
2208 80 : sort_expression NewType;
2209 80 : if (!MatchSetConstructor(atermpp::down_cast<function_sort>(Type), NewType))
2210 : {
2211 6 : throw mcrl2::runtime_error("Set constructor has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2212 : }
2213 74 : Type=NewType;
2214 80 : }
2215 :
2216 :
2217 51639 : if (sort_bag::constructor_name()==data_term_name)
2218 : {
2219 24 : sort_expression NewType;
2220 24 : if (!MatchBagConstructor(atermpp::down_cast<function_sort>(Type), NewType))
2221 : {
2222 10 : throw mcrl2::runtime_error("Bag constructor has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2223 : }
2224 14 : Type=NewType;
2225 24 : }
2226 :
2227 51629 : if (sort_set::false_function_name()==data_term_name)
2228 : {
2229 0 : sort_expression NewType;
2230 0 : if (!MatchFalseFunction(atermpp::down_cast<function_sort>(Type), NewType))
2231 : {
2232 0 : throw mcrl2::runtime_error("Bag constructor has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2233 : }
2234 0 : Type=NewType;
2235 0 : }
2236 :
2237 51629 : if (sort_bag::zero_function_name()==data_term_name)
2238 : {
2239 0 : sort_expression NewType;
2240 0 : if (!MatchBagConstructor(atermpp::down_cast<function_sort>(Type), NewType))
2241 : {
2242 0 : throw mcrl2::runtime_error("Bag constructor has incompatible argument types " + data::pp(Type) + " (while typechecking " + data::pp(d) + ").");
2243 : }
2244 0 : Type=NewType;
2245 0 : }
2246 :
2247 51629 : return Type;
2248 59140 : }
2249 :
2250 :
2251 :
2252 24501 : sort_expression mcrl2::data::data_type_checker::TraverseVarConsTypeDN(
2253 : const detail::variable_context& DeclaredVars,
2254 : data_expression& DataTerm,
2255 : sort_expression PosType,
2256 : const bool strictly_ambiguous,
2257 : const std::size_t nFactPars,
2258 : const bool warn_upcasting,
2259 : const bool print_cast_error) const
2260 : {
2261 : // std::string::npos for nFactPars means the number of arguments is not known.
2262 24501 : if (data::is_untyped_identifier(DataTerm)||data::is_function_symbol(DataTerm))
2263 : {
2264 27205 : core::identifier_string Name=data::is_untyped_identifier(DataTerm)?down_cast<const untyped_identifier>(DataTerm).name():
2265 27205 : atermpp::down_cast<const function_symbol>(DataTerm).name();
2266 :
2267 20858 : bool variable_=false;
2268 20858 : bool TypeADefined=false;
2269 20858 : sort_expression TypeA;
2270 20858 : std::map<core::identifier_string,sort_expression>::const_iterator i=DeclaredVars.context().find(Name);
2271 :
2272 20858 : if (i!=DeclaredVars.context().end())
2273 : {
2274 34 : TypeA=normalize_sorts(i->second,get_sort_specification());
2275 34 : TypeADefined=true;
2276 34 : const sort_expression Type1(UnwindType(TypeA));
2277 34 : if (is_function_sort(Type1)?(function_sort(Type1).domain().size()==nFactPars):(nFactPars==0))
2278 : {
2279 34 : variable_=true;
2280 :
2281 : //Add to free variables list
2282 : }
2283 : else
2284 : {
2285 0 : TypeADefined=false;
2286 : }
2287 34 : }
2288 :
2289 20858 : sort_expression_list ParList;
2290 20858 : if (nFactPars==0)
2291 : {
2292 0 : std::map<core::identifier_string,sort_expression>::const_iterator i=DeclaredVars.context().find(Name);
2293 0 : if (i!=DeclaredVars.context().end())
2294 : {
2295 0 : TypeA=normalize_sorts(i->second,get_sort_specification());
2296 0 : TypeADefined=true;
2297 0 : sort_expression temp;
2298 0 : if (!TypeMatchA(TypeA,PosType,temp))
2299 : {
2300 0 : throw mcrl2::runtime_error("The type " + data::pp(TypeA) + " of variable " + core::pp(Name)
2301 0 : + " is incompatible with " + data::pp(PosType) + " (typechecking " + data::pp(DataTerm) + ").");
2302 : }
2303 0 : DataTerm=variable(Name,TypeA);
2304 0 : return TypeA;
2305 0 : }
2306 : else
2307 : {
2308 0 : std::map<core::identifier_string,sort_expression>::const_iterator i=user_constants.find(Name);
2309 0 : if (i!=user_constants.end())
2310 : {
2311 0 : TypeA=i->second;
2312 0 : TypeADefined=true;
2313 0 : sort_expression temp;
2314 0 : if (!TypeMatchA(TypeA,PosType,temp))
2315 : {
2316 0 : throw mcrl2::runtime_error("The type " + data::pp(TypeA) + " of constant " + core::pp(Name)
2317 0 : + " is incompatible with " + data::pp(PosType) + " (typechecking " + data::pp(DataTerm) + ").");
2318 : }
2319 0 : DataTerm=data::function_symbol(Name,TypeA);
2320 0 : return TypeA;
2321 0 : }
2322 : else
2323 : {
2324 0 : std::map<core::identifier_string,sort_expression_list>::const_iterator j=system_constants.find(Name);
2325 :
2326 0 : if (j!=system_constants.end())
2327 : {
2328 0 : ParList=j->second;
2329 0 : if (ParList.size()==1)
2330 : {
2331 0 : sort_expression Type1=ParList.front();
2332 0 : DataTerm=function_symbol(Name,Type1);
2333 0 : return Type1;
2334 0 : }
2335 : else
2336 : {
2337 0 : DataTerm=data::function_symbol(Name,data::untyped_sort());
2338 0 : throw mcrl2::runtime_error("Ambiguous system constant " + core::pp(Name) + ".");
2339 : }
2340 : }
2341 : else
2342 : {
2343 0 : throw mcrl2::runtime_error("Unknown constant " + core::pp(Name) + ".");
2344 : }
2345 : }
2346 : }
2347 : }
2348 :
2349 20858 : if (TypeADefined)
2350 : {
2351 68 : ParList = sort_expression_list({ UnwindType(TypeA) });
2352 : }
2353 : else
2354 : {
2355 20824 : const std::map <core::identifier_string,sort_expression_list>::const_iterator j_context=user_functions.find(Name);
2356 20824 : const std::map <core::identifier_string,sort_expression_list>::const_iterator j_gssystem=system_functions.find(Name);
2357 :
2358 20824 : if (j_context==user_functions.end())
2359 : {
2360 13785 : if (j_gssystem!=system_functions.end())
2361 : {
2362 13713 : ParList=j_gssystem->second; // The function only occurs in the system.
2363 : }
2364 : else // None are defined.
2365 : {
2366 72 : if (nFactPars!=std::string::npos)
2367 : {
2368 72 : throw mcrl2::runtime_error("Unknown operation " + core::pp(Name) + " with " + std::to_string(nFactPars) + " parameter" + ((nFactPars != 1)?"s.":"."));
2369 : }
2370 : else
2371 : {
2372 0 : throw mcrl2::runtime_error("Unknown operation " + core::pp(Name) + ".");
2373 : }
2374 : }
2375 : }
2376 7039 : else if (j_gssystem==system_functions.end())
2377 : {
2378 7039 : ParList=j_context->second; // only the context sorts are defined.
2379 : }
2380 : else // Both are defined.
2381 : {
2382 0 : ParList=j_gssystem->second+j_context->second;
2383 : }
2384 : }
2385 :
2386 20786 : sort_expression_list CandidateParList=ParList;
2387 :
2388 : {
2389 : // filter ParList keeping only functions A_0#...#A_nFactPars->A
2390 20786 : sort_expression_list NewParList;
2391 20786 : if (nFactPars!=std::string::npos)
2392 : {
2393 61743 : for (; !ParList.empty(); ParList=ParList.tail())
2394 : {
2395 40966 : const sort_expression& Par=ParList.front();
2396 40966 : if (!is_function_sort(Par))
2397 : {
2398 0 : continue;
2399 : }
2400 40966 : if (down_cast<function_sort>(Par).domain().size()!=nFactPars)
2401 : {
2402 2580 : continue;
2403 : }
2404 38386 : NewParList.push_front(Par);
2405 : }
2406 20777 : ParList=reverse(NewParList);
2407 : }
2408 :
2409 20786 : if (!ParList.empty())
2410 : {
2411 20786 : CandidateParList=ParList;
2412 : }
2413 :
2414 : // filter ParList keeping only functions of the right type
2415 20786 : sort_expression_list BackupParList=ParList;
2416 20786 : NewParList=sort_expression_list();
2417 59190 : for (; !ParList.empty(); ParList=ParList.tail())
2418 : {
2419 38404 : const sort_expression& Par=ParList.front();
2420 : try
2421 : {
2422 38404 : PosType=determine_allowed_type(DataTerm, PosType); // XXXXXXXXXX
2423 30900 : sort_expression result;
2424 30900 : if (TypeMatchA(Par,PosType,result))
2425 : {
2426 19108 : NewParList=detail::insert_sort_unique(NewParList,result);
2427 : }
2428 30900 : }
2429 7504 : catch (mcrl2::runtime_error&)
2430 : {
2431 : // Ignore the error. Just do not add the type to NewParList
2432 7504 : }
2433 : }
2434 20786 : NewParList=reverse(NewParList);
2435 :
2436 20786 : if (NewParList.empty())
2437 : {
2438 : //Ok, this looks like a type error. We are not that strict.
2439 : //Pos can be Nat, or even Int...
2440 : //So lets make PosType more liberal
2441 : //We change every Pos to NotInferred(Pos,Nat,Int)...
2442 : //and get the list. Then we take the min of the list.
2443 :
2444 1738 : ParList=BackupParList;
2445 1738 : PosType=ExpandNumTypesUp(PosType);
2446 12440 : for (; !ParList.empty(); ParList=ParList.tail())
2447 : {
2448 10702 : const sort_expression& Par=ParList.front();
2449 10702 : sort_expression result;
2450 10702 : if (TypeMatchA(Par,PosType,result))
2451 : {
2452 3392 : NewParList=detail::insert_sort_unique(NewParList,result);
2453 : }
2454 10702 : }
2455 1738 : NewParList=reverse(NewParList);
2456 1738 : if (NewParList.size()>1)
2457 : {
2458 1218 : NewParList = sort_expression_list({ detail::MinType(NewParList) });
2459 : }
2460 : }
2461 :
2462 20786 : if (NewParList.empty())
2463 : {
2464 : //Ok, casting of the arguments did not help.
2465 : //Let's try to be more relaxed about the result, e.g. returning Pos or Nat is not a bad idea for int.
2466 :
2467 62 : ParList=BackupParList;
2468 :
2469 62 : PosType=ExpandNumTypesDown(ExpandNumTypesUp(PosType));
2470 155 : for (; !ParList.empty(); ParList=ParList.tail())
2471 : {
2472 93 : const sort_expression& Par=ParList.front();
2473 93 : sort_expression result;
2474 93 : if (TypeMatchA(Par,PosType,result))
2475 : {
2476 30 : NewParList=detail::insert_sort_unique(NewParList,result);
2477 : }
2478 93 : }
2479 62 : NewParList=reverse(NewParList);
2480 62 : if (NewParList.size()>1)
2481 : {
2482 0 : NewParList = sort_expression_list({ detail::MinType(NewParList) });
2483 : }
2484 : }
2485 :
2486 20786 : ParList=NewParList;
2487 20786 : }
2488 20786 : if (ParList.empty())
2489 : {
2490 : //provide some information to the upper layer for a better error message
2491 32 : sort_expression Sort;
2492 32 : if (CandidateParList.size()==1)
2493 : {
2494 5 : Sort=CandidateParList.front();
2495 : }
2496 : else
2497 : {
2498 27 : Sort=untyped_possible_sorts(sort_expression_list(CandidateParList));
2499 : }
2500 32 : DataTerm=data::function_symbol(Name,Sort);
2501 32 : if (nFactPars!=std::string::npos)
2502 : {
2503 96 : throw mcrl2::runtime_error("Unknown operation/variable " + core::pp(Name)
2504 128 : + " with " + std::to_string(nFactPars) + " argument" + ((nFactPars != 1)?"s":"")
2505 128 : + " that matches type " + data::pp(PosType) + ".");
2506 : }
2507 : else
2508 : {
2509 0 : throw mcrl2::runtime_error("Unknown operation/variable " + core::pp(Name) + " that matches type " + data::pp(PosType) + ".");
2510 : }
2511 32 : }
2512 :
2513 20754 : if (ParList.size()==1)
2514 : {
2515 : // replace PossibleSorts by a single possibility.
2516 20736 : sort_expression Type=ParList.front();
2517 :
2518 20736 : sort_expression OldType=Type;
2519 20736 : bool result=true;
2520 20736 : assert(Type.defined());
2521 20736 : if (detail::HasUnknown(Type))
2522 : {
2523 719 : sort_expression new_type;
2524 719 : result=TypeMatchA(Type,PosType,new_type);
2525 719 : Type=new_type;
2526 719 : }
2527 :
2528 20736 : if (detail::HasUnknown(Type) && data::is_function_symbol(DataTerm))
2529 : {
2530 489 : sort_expression new_type;
2531 489 : result=TypeMatchA(Type,DataTerm.sort(),new_type);
2532 489 : Type=new_type;
2533 489 : }
2534 :
2535 20736 : if (!result)
2536 : {
2537 0 : throw mcrl2::runtime_error("Fail to match sort " + data::pp(OldType) + " with " + data::pp(PosType) + ".");
2538 : }
2539 :
2540 20736 : Type=determine_allowed_type(DataTerm,Type);
2541 :
2542 20729 : Type=detail::replace_possible_sorts(Type); // Set the type to one option in possible sorts, if there are more options.
2543 :
2544 20729 : if (variable_)
2545 : {
2546 34 : DataTerm=variable(Name,Type);
2547 : }
2548 20695 : else if (is_untyped_identifier(DataTerm))
2549 : {
2550 6186 : DataTerm=data::function_symbol(untyped_identifier(DataTerm).name(),Type);
2551 : }
2552 : else
2553 : {
2554 14509 : DataTerm=data::function_symbol(function_symbol(DataTerm).name(),Type);
2555 : }
2556 20729 : assert(Type.defined());
2557 20729 : return Type;
2558 20743 : }
2559 : else
2560 : {
2561 18 : if (strictly_ambiguous)
2562 : {
2563 10 : if (nFactPars!=std::string::npos)
2564 : {
2565 1 : throw mcrl2::runtime_error("Ambiguous operation " + core::pp(Name) + " with " + std::to_string(nFactPars) + " parameter" + ((nFactPars != 1)?"s.":"."));
2566 : }
2567 : else
2568 : {
2569 9 : throw mcrl2::runtime_error("Ambiguous operation " + core::pp(Name) + ".");
2570 : }
2571 : }
2572 : else
2573 : {
2574 8 : return data::untyped_sort();
2575 : }
2576 : }
2577 21149 : }
2578 : else
2579 : {
2580 3643 : return TraverseVarConsTypeD(DeclaredVars,DataTerm,PosType,strictly_ambiguous,warn_upcasting,print_cast_error);
2581 : }
2582 : }
2583 :
2584 :
2585 42692 : sort_expression mcrl2::data::data_type_checker::TraverseVarConsTypeD(
2586 : const detail::variable_context& DeclaredVars,
2587 : data_expression& DataTerm,
2588 : const sort_expression& PosType,
2589 : const bool strictly_ambiguous,
2590 : const bool warn_upcasting,
2591 : const bool print_cast_error) const
2592 : {
2593 : //Type checks and transforms DataTerm replacing Unknown datatype with other ones.
2594 : //Returns the type of the term which should match the PosType.
2595 :
2596 42692 : if (is_abstraction(DataTerm))
2597 : {
2598 259 : const abstraction& abstr=down_cast<const abstraction>(DataTerm);
2599 : //The variable declaration of a binder should have at least 1 declaration
2600 259 : if (abstr.variables().size()==0)
2601 : {
2602 0 : throw mcrl2::runtime_error("Binder " + data::pp(DataTerm) + " should have at least one declared variable.");
2603 : }
2604 :
2605 259 : const binder_type& BindingOperator = abstr.binding_operator();
2606 :
2607 259 : if (is_untyped_set_or_bag_comprehension_binder(BindingOperator) ||
2608 489 : is_set_comprehension_binder(BindingOperator) ||
2609 230 : is_bag_comprehension_binder(BindingOperator))
2610 : {
2611 29 : const variable_list& comprehension_variables=abstr.variables();
2612 : // Type check the comprehension_variables.
2613 : try
2614 : {
2615 29 : (*this)(comprehension_variables,DeclaredVars);
2616 : }
2617 0 : catch (mcrl2::runtime_error& e)
2618 : {
2619 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nError occurred while typechecking the bag/set " + data::pp(DataTerm) + ".");
2620 0 : }
2621 :
2622 :
2623 : //A Set/bag comprehension should have exactly one variable declared
2624 29 : if (comprehension_variables.size()!=1)
2625 : {
2626 0 : throw mcrl2::runtime_error("Set/bag comprehension " + data::pp(DataTerm) + " should have exactly one declared variable.");
2627 : }
2628 :
2629 29 : const sort_expression element_sort=comprehension_variables.front().sort();
2630 :
2631 29 : detail::variable_context CopyDeclaredVars(DeclaredVars);
2632 29 : CopyDeclaredVars.add_context_variables(comprehension_variables);
2633 :
2634 29 : data_expression Data=abstr.body();
2635 :
2636 29 : sort_expression ResType;
2637 29 : sort_expression NewType;
2638 : try
2639 : {
2640 29 : ResType=TraverseVarConsTypeD(CopyDeclaredVars,Data,data::untyped_sort(),strictly_ambiguous,warn_upcasting,print_cast_error);
2641 : }
2642 0 : catch (mcrl2::runtime_error& e)
2643 : {
2644 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nThe condition or count of a set/bag comprehension " + data::pp(DataTerm) + " cannot be determined.");
2645 0 : }
2646 29 : sort_expression temp;
2647 29 : if (TypeMatchA(sort_bool::bool_(),ResType,temp))
2648 : {
2649 19 : NewType=sort_set::set_(sort_expression(element_sort));
2650 19 : DataTerm = abstraction(set_comprehension_binder(),comprehension_variables,Data);
2651 : }
2652 10 : else if (TypeMatchA(sort_nat::nat(),ResType,temp))
2653 : {
2654 7 : NewType=sort_bag::bag(sort_expression(element_sort));
2655 7 : DataTerm = abstraction(bag_comprehension_binder(),comprehension_variables,Data);
2656 : }
2657 3 : else if (TypeMatchA(sort_pos::pos(),ResType,temp))
2658 : {
2659 1 : NewType=sort_bag::bag(sort_expression(element_sort));
2660 1 : Data=application(sort_nat::cnat(),Data);
2661 1 : DataTerm = abstraction(bag_comprehension_binder(),comprehension_variables,Data);
2662 : }
2663 : else
2664 : {
2665 2 : throw mcrl2::runtime_error("The condition or count of a set/bag comprehension is not of sort Bool, Nat or Pos, but of sort " + data::pp(ResType) + ".");
2666 : }
2667 :
2668 27 : if (!TypeMatchA(NewType,PosType,NewType))
2669 : {
2670 0 : throw mcrl2::runtime_error("A set or bag comprehension of type " + data::pp(element_sort) + " does not match possible type " +
2671 0 : data::pp(PosType) + " (while typechecking " + data::pp(DataTerm) + ").");
2672 : }
2673 :
2674 27 : return NewType;
2675 39 : }
2676 :
2677 230 : if (is_forall_binder(BindingOperator) || is_exists_binder(BindingOperator))
2678 : {
2679 121 : const variable_list& bound_variables=abstr.variables();
2680 :
2681 : // Type check the variables.
2682 : try
2683 : {
2684 121 : (*this)(bound_variables,DeclaredVars);
2685 : }
2686 0 : catch (mcrl2::runtime_error& e)
2687 : {
2688 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nError occurred while typechecking the quantification " + data::pp(DataTerm) + ".");
2689 0 : }
2690 :
2691 121 : detail::variable_context CopyDeclaredVars(DeclaredVars);
2692 121 : CopyDeclaredVars.add_context_variables(bound_variables);
2693 :
2694 121 : data_expression Data=abstr.body();
2695 121 : sort_expression temp;
2696 121 : if (!TypeMatchA(sort_bool::bool_(),PosType,temp))
2697 : {
2698 0 : throw mcrl2::runtime_error("The type of an exist/forall for " + data::pp(DataTerm) + " cannot be determined.");
2699 : }
2700 121 : sort_expression NewType=TraverseVarConsTypeD(CopyDeclaredVars,Data,sort_bool::bool_(),strictly_ambiguous,warn_upcasting,print_cast_error);
2701 :
2702 121 : if (!TypeMatchA(sort_bool::bool_(),NewType,temp))
2703 : {
2704 0 : throw mcrl2::runtime_error("The type of an exist/forall for " + data::pp(DataTerm) + " cannot be determined.");
2705 : }
2706 :
2707 121 : DataTerm=abstraction(BindingOperator,bound_variables,Data);
2708 121 : return sort_bool::bool_();
2709 121 : }
2710 :
2711 109 : if (is_lambda_binder(BindingOperator))
2712 : {
2713 109 : const variable_list& bound_variables=abstr.variables();
2714 : // Typecheck the variables.
2715 : try
2716 : {
2717 109 : (*this)(bound_variables,DeclaredVars);
2718 : }
2719 2 : catch (mcrl2::runtime_error& e)
2720 : {
2721 2 : throw mcrl2::runtime_error(std::string(e.what()) + "\nError occurred while typechecking the lambda expression " + data::pp(DataTerm) + ".");
2722 2 : }
2723 :
2724 107 : detail::variable_context CopyDeclaredVars(DeclaredVars);
2725 107 : CopyDeclaredVars.add_context_variables(bound_variables);
2726 :
2727 107 : sort_expression_list ArgTypes=detail::GetVarTypes(bound_variables);
2728 107 : sort_expression NewType;
2729 107 : if (!UnArrowProd(ArgTypes,PosType,NewType))
2730 : {
2731 1 : throw mcrl2::runtime_error("No functions with arguments " + data::pp(ArgTypes) + " among " + data::pp(PosType) + " (while typechecking " + data::pp(DataTerm) + ").");
2732 : }
2733 106 : data_expression Data=abstr.body();
2734 :
2735 : try
2736 : {
2737 106 : NewType=TraverseVarConsTypeD(CopyDeclaredVars,Data,NewType,strictly_ambiguous,warn_upcasting,print_cast_error);
2738 : }
2739 4 : catch (mcrl2::runtime_error& e)
2740 : {
2741 4 : throw e;
2742 4 : }
2743 :
2744 102 : DataTerm=abstraction(BindingOperator,bound_variables,Data);
2745 102 : return function_sort(ArgTypes,NewType);
2746 121 : }
2747 : }
2748 :
2749 42433 : if (is_where_clause(DataTerm))
2750 : {
2751 45 : const where_clause& where=down_cast<const where_clause>(DataTerm);
2752 45 : variable_list WhereVarList;
2753 45 : assignment_list NewWhereList;
2754 45 : const assignment_expression_list& where_asss=where.declarations();
2755 94 : for (assignment_expression_list::const_iterator i=where_asss.begin(); i!=where_asss.end(); ++i)
2756 : {
2757 55 : const assignment_expression WhereElem= *i;
2758 55 : data_expression WhereTerm;
2759 55 : variable NewWhereVar;
2760 55 : if (data::is_untyped_identifier_assignment(WhereElem))
2761 : {
2762 53 : const data::untyped_identifier_assignment& t=down_cast<const data::untyped_identifier_assignment>(WhereElem);
2763 53 : WhereTerm=t.rhs();
2764 59 : sort_expression WhereType=TraverseVarConsTypeD(DeclaredVars,WhereTerm,data::untyped_sort(),strictly_ambiguous,warn_upcasting,print_cast_error);
2765 :
2766 : // The variable in WhereElem is just a string and needs to be transformed to a DataVarId.
2767 47 : NewWhereVar=variable(t.lhs(),WhereType);
2768 47 : }
2769 : else
2770 : {
2771 2 : const assignment& t=down_cast<const assignment>(WhereElem);
2772 2 : WhereTerm=t.rhs();
2773 2 : NewWhereVar=t.lhs();
2774 2 : sort_expression WhereType=TraverseVarConsTypeD(DeclaredVars,WhereTerm,NewWhereVar.sort(),strictly_ambiguous,warn_upcasting,print_cast_error);
2775 2 : }
2776 49 : WhereVarList.push_front(NewWhereVar);
2777 49 : NewWhereList.push_front(assignment(NewWhereVar,WhereTerm));
2778 67 : }
2779 39 : NewWhereList=reverse(NewWhereList);
2780 :
2781 39 : variable_list where_variables=reverse(WhereVarList);
2782 : // Typecheck the where_variables
2783 : try
2784 : {
2785 39 : (*this)(where_variables,DeclaredVars);
2786 : }
2787 0 : catch (mcrl2::runtime_error& e)
2788 : {
2789 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nError occurred while typechecking the where expression " + data::pp(DataTerm) + ".");
2790 0 : }
2791 :
2792 39 : detail::variable_context CopyDeclaredVars(DeclaredVars);
2793 39 : CopyDeclaredVars.add_context_variables(where_variables);
2794 :
2795 39 : data_expression Data=where.body();
2796 39 : sort_expression NewType=TraverseVarConsTypeD(CopyDeclaredVars,Data,PosType,strictly_ambiguous,warn_upcasting,print_cast_error);
2797 :
2798 39 : DataTerm=where_clause(Data,NewWhereList);
2799 39 : return NewType;
2800 51 : }
2801 :
2802 42388 : if (is_application(DataTerm))
2803 : {
2804 : //arguments
2805 12866 : const application& appl=down_cast<application>(DataTerm);
2806 12866 : std::size_t nArguments=appl.size();
2807 :
2808 : //The following is needed to check enumerations
2809 12866 : const data_expression& Arg0 = appl.head();
2810 12866 : if (data::is_function_symbol(Arg0) || data::is_untyped_identifier(Arg0))
2811 : {
2812 15771 : core::identifier_string Name = is_function_symbol(Arg0)?down_cast<function_symbol>(Arg0).name():
2813 15771 : atermpp::down_cast<untyped_identifier>(Arg0).name();
2814 11061 : if (Name == sort_list::list_enumeration_name())
2815 : {
2816 130 : sort_expression Type;
2817 130 : if (!UnList(PosType,Type))
2818 : {
2819 0 : throw mcrl2::runtime_error("It is not possible to cast list to " + data::pp(PosType) + " (while typechecking " + data::pp(data_expression_list(appl.begin(),appl.end())) + ").");
2820 : }
2821 :
2822 : //First time to determine the common type only!
2823 130 : data_expression_list NewArguments;
2824 130 : bool Type_is_stable=true;
2825 377 : for (application::const_iterator i=appl.begin(); i!=appl.end(); ++i)
2826 : {
2827 248 : data_expression Argument= *i;
2828 248 : sort_expression Type0;
2829 : try
2830 : {
2831 248 : Type0=TraverseVarConsTypeD(DeclaredVars,Argument,Type,strictly_ambiguous,warn_upcasting,false);
2832 : }
2833 3 : catch (mcrl2::runtime_error&)
2834 : {
2835 : // Try again, but now without Type as the suggestion.
2836 : // If this does not work, it will be caught in the second pass below.
2837 4 : Type0=TraverseVarConsTypeD(DeclaredVars,Argument,data::untyped_sort(),strictly_ambiguous,warn_upcasting,print_cast_error);
2838 3 : }
2839 247 : NewArguments.push_front(Argument);
2840 247 : Type_is_stable=Type_is_stable && (Type==Type0);
2841 247 : Type=Type0;
2842 249 : }
2843 : // Arguments=OldArguments;
2844 :
2845 : //Second time to do the real work, but only if the elements in the list have different types.
2846 129 : if (!Type_is_stable)
2847 : {
2848 44 : NewArguments=data_expression_list();
2849 120 : for (application::const_iterator i=appl.begin(); i!=appl.end(); ++i)
2850 : {
2851 76 : data_expression Argument= *i;
2852 76 : sort_expression Type0=TraverseVarConsTypeD(DeclaredVars,Argument,Type,strictly_ambiguous,warn_upcasting,print_cast_error);
2853 76 : NewArguments.push_front(Argument);
2854 76 : Type=Type0;
2855 76 : }
2856 : }
2857 :
2858 129 : Type=sort_list::list(sort_expression(Type));
2859 129 : DataTerm=sort_list::list_enumeration(sort_expression(Type), data_expression_list(reverse(NewArguments)));
2860 129 : return Type;
2861 131 : }
2862 10931 : if (Name == sort_set::set_enumeration_name())
2863 : {
2864 219 : sort_expression Type;
2865 219 : if (!UnFSet(PosType,Type))
2866 : {
2867 0 : throw mcrl2::runtime_error("It is not possible to cast set to " + data::pp(PosType) + " (while typechecking " + data::pp(data_expression_list(appl.begin(),appl.end())) + ").");
2868 : }
2869 :
2870 : //First time to determine the common type only (which will be NewType)!
2871 219 : bool NewTypeDefined=false;
2872 219 : sort_expression NewType;
2873 575 : for (application::const_iterator i=appl.begin(); i!=appl.end(); ++i)
2874 : {
2875 356 : data_expression Argument= *i;
2876 356 : sort_expression Type0;
2877 : try
2878 : {
2879 356 : Type0=TraverseVarConsTypeD(DeclaredVars,Argument,Type,strictly_ambiguous,warn_upcasting,print_cast_error);
2880 : }
2881 0 : catch (mcrl2::runtime_error& e)
2882 : {
2883 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nImpossible to cast element to " + data::pp(Type) + " (while typechecking " + data::pp(Argument) + ").");
2884 0 : }
2885 :
2886 356 : sort_expression OldNewType=NewType;
2887 356 : if (!NewTypeDefined)
2888 : {
2889 219 : NewType=Type0;
2890 219 : NewTypeDefined=true;
2891 : }
2892 : else
2893 : {
2894 137 : sort_expression temp;
2895 137 : if (!MaximumType(NewType,Type0,temp))
2896 : {
2897 0 : throw mcrl2::runtime_error("Set contains incompatible elements of sorts " + data::pp(OldNewType) + " and " + data::pp(Type0) + " (while typechecking " + data::pp(Argument) + ".");
2898 : }
2899 137 : NewType=temp;
2900 137 : NewTypeDefined=true;
2901 137 : }
2902 356 : }
2903 :
2904 :
2905 : // Type is now the most generic type to be used.
2906 219 : assert(Type.defined());
2907 219 : assert(NewTypeDefined);
2908 219 : Type=NewType;
2909 : // Arguments=OldArguments;
2910 :
2911 : //Second time to do the real work.
2912 219 : data_expression_list NewArguments;
2913 575 : for (application::const_iterator i=appl.begin(); i!=appl.end(); ++i)
2914 : {
2915 356 : data_expression Argument= *i;
2916 356 : sort_expression Type0;
2917 : try
2918 : {
2919 356 : Type0=TraverseVarConsTypeD(DeclaredVars,Argument,Type,strictly_ambiguous,warn_upcasting,print_cast_error);
2920 : }
2921 0 : catch (mcrl2::runtime_error& e)
2922 : {
2923 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nImpossible to cast element to " + data::pp(Type) + " (while typechecking " + data::pp(Argument) + ").");
2924 0 : }
2925 356 : NewArguments.push_front(Argument);
2926 356 : Type=Type0;
2927 356 : }
2928 219 : DataTerm=sort_set::set_enumeration(sort_expression(Type),data_expression_list(reverse(NewArguments)));
2929 219 : if (sort_set::is_set(PosType))
2930 : {
2931 20 : DataTerm=sort_set::constructor(Type, sort_set::false_function(Type),DataTerm);
2932 :
2933 20 : return sort_set::set_(Type);
2934 : }
2935 199 : return sort_fset::fset(Type);
2936 219 : }
2937 10712 : if (Name == sort_bag::bag_enumeration_name())
2938 : {
2939 198 : sort_expression Type;
2940 198 : if (!UnFBag(PosType,Type))
2941 : {
2942 0 : throw mcrl2::runtime_error("Impossible to cast bag to " + data::pp(PosType) + "(while typechecking " +
2943 0 : data::pp(data_expression_list(appl.begin(),appl.end())) + ").");
2944 : }
2945 :
2946 : //First time to determine the common type only!
2947 198 : sort_expression NewType;
2948 198 : bool NewTypeDefined=false;
2949 469 : for (application::const_iterator i=appl.begin(); i!=appl.end(); ++i)
2950 : {
2951 271 : data_expression Argument0= *i;
2952 271 : ++i;
2953 271 : data_expression Argument1= *i;
2954 271 : sort_expression Type0;
2955 : try
2956 : {
2957 271 : Type0=TraverseVarConsTypeD(DeclaredVars,Argument0,Type,strictly_ambiguous,warn_upcasting,print_cast_error);
2958 : }
2959 0 : catch (mcrl2::runtime_error& e)
2960 : {
2961 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nImpossible to cast element to " + data::pp(Type) + " (while typechecking " + data::pp(Argument0) + ").");
2962 0 : }
2963 271 : sort_expression Type1;
2964 : try
2965 : {
2966 271 : Type1=TraverseVarConsTypeD(DeclaredVars,Argument1,sort_nat::nat(),strictly_ambiguous,warn_upcasting,print_cast_error);
2967 : }
2968 0 : catch (mcrl2::runtime_error& e)
2969 : {
2970 0 : if (print_cast_error)
2971 : {
2972 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nImpossible to cast number to " + data::pp(sort_nat::nat()) + " (while typechecking " + data::pp(Argument1) + ").");
2973 : }
2974 : else
2975 : {
2976 0 : throw e;
2977 : }
2978 0 : }
2979 271 : sort_expression OldNewType=NewType;
2980 271 : if (!NewTypeDefined)
2981 : {
2982 198 : NewType=Type0;
2983 198 : NewTypeDefined=true;
2984 : }
2985 : else
2986 : {
2987 73 : sort_expression temp;
2988 73 : if (!MaximumType(NewType,Type0,temp))
2989 : {
2990 0 : throw mcrl2::runtime_error("Bag contains incompatible elements of sorts " + data::pp(OldNewType) + " and " + data::pp(Type0) + " (while typechecking " + data::pp(Argument0) + ").");
2991 : }
2992 :
2993 73 : NewType=temp;
2994 73 : NewTypeDefined=true;
2995 73 : }
2996 271 : }
2997 198 : assert(Type.defined());
2998 198 : assert(NewTypeDefined);
2999 198 : Type=NewType;
3000 : // Arguments=OldArguments;
3001 :
3002 : //Second time to do the real work.
3003 198 : data_expression_list NewArguments;
3004 469 : for (application::const_iterator i=appl.begin(); i!=appl.end(); ++i)
3005 : {
3006 271 : data_expression Argument0= *i;
3007 271 : ++i;
3008 271 : data_expression Argument1= *i;
3009 271 : sort_expression Type0;
3010 : try
3011 : {
3012 271 : Type0=TraverseVarConsTypeD(DeclaredVars,Argument0,Type,strictly_ambiguous,warn_upcasting,print_cast_error);
3013 : }
3014 0 : catch (mcrl2::runtime_error& e)
3015 : {
3016 0 : if (print_cast_error)
3017 : {
3018 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nImpossible to cast element to " + data::pp(Type) + " (while typechecking " + data::pp(Argument0) + ").");
3019 : }
3020 : else
3021 : {
3022 0 : throw e;
3023 : }
3024 0 : }
3025 271 : sort_expression Type1;
3026 : try
3027 : {
3028 271 : Type1=TraverseVarConsTypeD(DeclaredVars,Argument1,sort_nat::nat(),strictly_ambiguous,warn_upcasting,print_cast_error);
3029 : }
3030 0 : catch (mcrl2::runtime_error& e)
3031 : {
3032 0 : if (print_cast_error)
3033 : {
3034 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nImpossible to cast number to " + data::pp(sort_nat::nat()) + " (while typechecking " + data::pp(Argument1) + ").");
3035 : }
3036 : else
3037 : {
3038 0 : throw e;
3039 : }
3040 0 : }
3041 271 : NewArguments.push_front(Argument0);
3042 271 : NewArguments.push_front(Argument1);
3043 271 : Type=Type0;
3044 271 : }
3045 198 : DataTerm=sort_bag::bag_enumeration(Type, data_expression_list(reverse(NewArguments)));
3046 198 : if (sort_bag::is_bag(PosType))
3047 : {
3048 1 : DataTerm=sort_bag::constructor(Type, sort_bag::zero_function(Type),DataTerm);
3049 :
3050 1 : return sort_bag::bag(Type);
3051 : }
3052 197 : return sort_fbag::fbag(Type);
3053 198 : }
3054 11061 : }
3055 12319 : sort_expression_list NewArgumentTypes;
3056 12319 : data_expression_list NewArguments;
3057 12319 : sort_expression_list argument_sorts;
3058 32479 : for (application::const_iterator i=appl.begin(); i!=appl.end(); ++i)
3059 : {
3060 20177 : data_expression Arg= *i;
3061 20194 : sort_expression Type=TraverseVarConsTypeD(DeclaredVars,Arg,data::untyped_sort(),false,warn_upcasting,print_cast_error);
3062 20160 : assert(Type.defined());
3063 20160 : NewArguments.push_front(Arg);
3064 20160 : NewArgumentTypes.push_front(Type);
3065 20177 : }
3066 12302 : data_expression_list Arguments=reverse(NewArguments);
3067 12302 : sort_expression_list ArgumentTypes=reverse(NewArgumentTypes);
3068 : //function
3069 12302 : data_expression Data=appl.head();
3070 12302 : sort_expression NewType;
3071 : try
3072 : {
3073 24604 : NewType=TraverseVarConsTypeDN(DeclaredVars,
3074 : Data,
3075 : // data::untyped_sort(), /* function_sort(ArgumentTypes,PosType) */
3076 24716 : function_sort(ArgumentTypes,PosType), // XXXXXXXX
3077 12190 : false,nArguments,warn_upcasting,print_cast_error);
3078 : }
3079 112 : catch (mcrl2::runtime_error& e)
3080 : {
3081 336 : throw mcrl2::runtime_error(std::string(e.what()) + "\nType error while trying to cast an application of " +
3082 448 : data::pp(Data) + " to arguments " + data::pp(Arguments) + " to type " + data::pp(PosType) + ".");
3083 112 : }
3084 :
3085 : //it is possible that:
3086 : //1) a cast has happened
3087 : //2) some parameter Types became sharper.
3088 : //we do the arguments again with the types.
3089 :
3090 :
3091 12190 : if (is_function_sort(UnwindType(NewType)))
3092 : {
3093 12186 : sort_expression_list NeededArgumentTypes=down_cast<function_sort>(UnwindType(NewType)).domain();
3094 :
3095 12186 : if (NeededArgumentTypes.size()!=Arguments.size())
3096 : {
3097 0 : throw mcrl2::runtime_error("Need argumens of sorts " + data::pp(NeededArgumentTypes) +
3098 : " which does not match the number of provided arguments "
3099 0 : + data::pp(Arguments) + " (while typechecking "
3100 0 : + data::pp(DataTerm) + ").");
3101 : }
3102 : //arguments again
3103 12186 : sort_expression_list NewArgumentTypes;
3104 12186 : data_expression_list NewArguments;
3105 52238 : for (; !Arguments.empty(); Arguments=Arguments.tail(),
3106 20026 : ArgumentTypes=ArgumentTypes.tail(),NeededArgumentTypes=NeededArgumentTypes.tail())
3107 : {
3108 20026 : assert(!Arguments.empty());
3109 20026 : assert(!NeededArgumentTypes.empty());
3110 20026 : data_expression Arg=Arguments.front();
3111 20026 : const sort_expression& NeededType=NeededArgumentTypes.front();
3112 20026 : sort_expression Type=ArgumentTypes.front();
3113 20026 : if (!EqTypesA(NeededType,Type))
3114 : {
3115 : //upcasting
3116 : try
3117 : {
3118 2087 : Type=UpCastNumericType(NeededType,Type,Arg,DeclaredVars,strictly_ambiguous,warn_upcasting,print_cast_error);
3119 : }
3120 235 : catch (mcrl2::runtime_error&)
3121 : {
3122 235 : }
3123 : }
3124 20026 : if (!EqTypesA(NeededType,Type))
3125 : {
3126 236 : sort_expression NewArgType;
3127 236 : if (!TypeMatchA(NeededType,Type,NewArgType))
3128 : {
3129 20 : if (!TypeMatchA(NeededType,ExpandNumTypesUp(Type),NewArgType))
3130 : {
3131 0 : NewArgType=NeededType;
3132 : }
3133 : }
3134 : try
3135 : {
3136 236 : NewArgType=TraverseVarConsTypeD(DeclaredVars,Arg,NewArgType,strictly_ambiguous,warn_upcasting,print_cast_error);
3137 : }
3138 0 : catch (mcrl2::runtime_error& e)
3139 : {
3140 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nRequired type " + data::pp(NeededType) + " does not match possible type "
3141 0 : + data::pp(Type) + " (while typechecking " + data::pp(Arg) + " in " + data::pp(DataTerm) + ").");
3142 0 : }
3143 236 : Type=NewArgType;
3144 236 : }
3145 20026 : NewArguments.push_front(Arg);
3146 20026 : NewArgumentTypes.push_front(Type);
3147 20026 : }
3148 12186 : Arguments=reverse(NewArguments);
3149 12186 : ArgumentTypes=reverse(NewArgumentTypes);
3150 12186 : }
3151 :
3152 : //the function again
3153 : try
3154 : {
3155 24380 : NewType=TraverseVarConsTypeDN(DeclaredVars,
3156 24381 : Data,function_sort(ArgumentTypes,PosType),
3157 12189 : strictly_ambiguous,nArguments,warn_upcasting,print_cast_error);
3158 : }
3159 1 : catch (mcrl2::runtime_error& e)
3160 : {
3161 3 : throw mcrl2::runtime_error(std::string(e.what()) + "\nType error while trying to cast " +
3162 4 : data::pp(application(Data,Arguments)) + " to type " + data::pp(PosType) + ".");
3163 1 : }
3164 :
3165 : //and the arguments once more
3166 12189 : if (is_function_sort(UnwindType(NewType)))
3167 : {
3168 12185 : sort_expression_list NeededArgumentTypes=down_cast<function_sort>(UnwindType(NewType)).domain();
3169 12185 : sort_expression_list NewArgumentTypes;
3170 12185 : data_expression_list NewArguments;
3171 52235 : for (; !Arguments.empty(); Arguments=Arguments.tail(),
3172 20025 : ArgumentTypes=ArgumentTypes.tail(),NeededArgumentTypes=NeededArgumentTypes.tail())
3173 : {
3174 20025 : data_expression Arg=Arguments.front();
3175 20025 : const sort_expression& NeededType=NeededArgumentTypes.front();
3176 20025 : sort_expression Type=ArgumentTypes.front();
3177 :
3178 20025 : if (!EqTypesA(NeededType,Type))
3179 : {
3180 : //upcasting
3181 : try
3182 : {
3183 0 : Type=UpCastNumericType(NeededType,Type,Arg,DeclaredVars,strictly_ambiguous,warn_upcasting,print_cast_error);
3184 : }
3185 0 : catch (mcrl2::runtime_error&)
3186 : {
3187 0 : }
3188 : }
3189 20025 : if (!EqTypesA(NeededType,Type))
3190 : {
3191 0 : sort_expression NewArgType;
3192 0 : if (!TypeMatchA(NeededType,Type,NewArgType))
3193 : {
3194 0 : if (!TypeMatchA(NeededType,ExpandNumTypesUp(Type),NewArgType))
3195 : {
3196 0 : NewArgType=NeededType;
3197 : }
3198 : }
3199 : try
3200 : {
3201 0 : NewArgType=TraverseVarConsTypeD(DeclaredVars,Arg,NewArgType,strictly_ambiguous,warn_upcasting,print_cast_error);
3202 : }
3203 0 : catch (mcrl2::runtime_error& e)
3204 : {
3205 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nNeeded type " + data::pp(NeededType) + " does not match possible type "
3206 0 : + data::pp(Type) + " (while typechecking " + data::pp(Arg) + " in " + data::pp(DataTerm) + ").");
3207 0 : }
3208 0 : Type=NewArgType;
3209 0 : }
3210 :
3211 20025 : NewArguments.push_front(Arg);
3212 20025 : NewArgumentTypes.push_front(Type);
3213 20025 : }
3214 12185 : Arguments=reverse(NewArguments);
3215 12185 : ArgumentTypes=reverse(NewArgumentTypes);
3216 12185 : }
3217 :
3218 12189 : DataTerm=application(Data,Arguments);
3219 :
3220 12189 : if (is_function_sort(UnwindType(NewType)))
3221 : {
3222 : // Code below is a hack as sometimes the type of the returned numeral is not equal
3223 : // to the PosType that is requested. Hence, a typecast must be added explicitly.
3224 12185 : const sort_expression s=DataTerm.sort();
3225 19285 : if (PosType !=data::untyped_sort() && s != PosType &&
3226 7100 : (s == sort_int::int_() || s == sort_pos::pos() || s == sort_nat::nat() || s == sort_real::real_()))
3227 : {
3228 30 : return UpCastNumericType(PosType, atermpp::down_cast<function_sort>(UnwindType(NewType)).codomain(),
3229 30 : DataTerm,DeclaredVars,strictly_ambiguous,warn_upcasting,print_cast_error);
3230 : }
3231 : // end of the explicit upcast hack. Continuing with the original code.
3232 12170 : return atermpp::down_cast<function_sort>(UnwindType(NewType)).codomain();
3233 12185 : }
3234 :
3235 4 : sort_expression temp_type;
3236 4 : if (!UnArrowProd(ArgumentTypes,NewType,temp_type))
3237 : {
3238 0 : throw mcrl2::runtime_error("Fail to properly type " + data::pp(DataTerm) + ".");
3239 : }
3240 4 : if (detail::HasUnknown(temp_type))
3241 : {
3242 4 : throw mcrl2::runtime_error("Fail to properly type " + data::pp(DataTerm) + ".");
3243 : }
3244 0 : return temp_type;
3245 13059 : }
3246 :
3247 29522 : if (data::is_untyped_identifier(DataTerm)||data::is_function_symbol(DataTerm)||is_variable(DataTerm))
3248 : {
3249 : core::identifier_string Name=
3250 47097 : data::is_untyped_identifier(DataTerm)?down_cast<untyped_identifier>(DataTerm).name():
3251 18446 : is_function_symbol(DataTerm)?down_cast<function_symbol>(DataTerm).name():
3252 65543 : atermpp::down_cast<variable>(DataTerm).name();
3253 29522 : if (utilities::is_numeric_string(Name.function().name()))
3254 : {
3255 6623 : sort_expression Sort=sort_int::int_();
3256 6623 : if (detail::IsPos(Name))
3257 : {
3258 5835 : Sort=sort_pos::pos();
3259 : }
3260 788 : else if (detail::IsNat(Name))
3261 : {
3262 788 : Sort=sort_nat::nat();
3263 : }
3264 6623 : DataTerm=data::function_symbol(Name,Sort);
3265 :
3266 6623 : sort_expression temp;
3267 6623 : if (TypeMatchA(Sort,PosType,temp))
3268 : {
3269 5128 : return Sort;
3270 : }
3271 :
3272 : //upcasting
3273 1495 : sort_expression CastedNewType;
3274 : try
3275 : {
3276 1501 : CastedNewType=UpCastNumericType(PosType,Sort,DataTerm,DeclaredVars,strictly_ambiguous,warn_upcasting,print_cast_error);
3277 : }
3278 3 : catch (mcrl2::runtime_error& e)
3279 : {
3280 3 : throw mcrl2::runtime_error(std::string(e.what()) + "\nCannot (up)cast number " + data::pp(DataTerm) + " to type " + data::pp(PosType) + ".");
3281 3 : }
3282 1492 : return CastedNewType;
3283 6629 : }
3284 :
3285 22899 : const std::map<core::identifier_string,sort_expression>::const_iterator it=DeclaredVars.context().find(Name);
3286 22899 : if (it!=DeclaredVars.context().end())
3287 : {
3288 13684 : sort_expression Type=normalize_sorts(it->second,get_sort_specification());
3289 13684 : DataTerm=variable(Name,Type);
3290 :
3291 13684 : sort_expression NewType;
3292 13684 : if (TypeMatchA(Type,PosType,NewType))
3293 : {
3294 13620 : Type=NewType;
3295 : }
3296 : else
3297 : {
3298 : //upcasting
3299 64 : sort_expression CastedNewType;
3300 : try
3301 : {
3302 154 : CastedNewType=UpCastNumericType(PosType,Type,DataTerm,DeclaredVars,strictly_ambiguous,warn_upcasting,print_cast_error);
3303 : }
3304 45 : catch (mcrl2::runtime_error& e)
3305 : {
3306 45 : if (print_cast_error)
3307 : {
3308 44 : throw mcrl2::runtime_error(std::string(e.what()) + "\nCannot (up)cast variable " + data::pp(DataTerm) + " to type " + data::pp(PosType) + ".");
3309 : }
3310 : else
3311 : {
3312 1 : throw e;
3313 : }
3314 45 : }
3315 :
3316 19 : Type=CastedNewType;
3317 64 : }
3318 :
3319 : //Add to free variables list
3320 13639 : return Type;
3321 13729 : }
3322 :
3323 9215 : std::map<core::identifier_string,sort_expression>::const_iterator i=user_constants.find(Name);
3324 9215 : if (i!=user_constants.end())
3325 : {
3326 1551 : sort_expression Type=i->second;
3327 1551 : sort_expression NewType;
3328 1551 : if (TypeMatchA(Type,PosType,NewType))
3329 : {
3330 1501 : Type=NewType;
3331 1501 : DataTerm=data::function_symbol(Name,Type);
3332 1501 : return Type;
3333 : }
3334 : else
3335 : {
3336 : // The type cannot be unified. Try upcasting the type.
3337 50 : DataTerm=data::function_symbol(Name,Type);
3338 : try
3339 : {
3340 148 : return UpCastNumericType(PosType,Type,DataTerm,DeclaredVars,strictly_ambiguous,warn_upcasting,print_cast_error);
3341 : }
3342 49 : catch (mcrl2::runtime_error& e)
3343 : {
3344 49 : throw mcrl2::runtime_error(std::string(e.what()) + "\nNo constant " + data::pp(DataTerm) + " with type " + data::pp(PosType) + ".");
3345 49 : }
3346 : }
3347 1600 : }
3348 :
3349 7664 : std::map<core::identifier_string,sort_expression_list>::const_iterator j=system_constants.find(Name);
3350 7664 : if (j!=system_constants.end())
3351 : {
3352 7462 : sort_expression_list TypeList=j->second;
3353 7462 : sort_expression_list NewParList;
3354 14924 : for (sort_expression_list::const_iterator i=TypeList.begin(); i!=TypeList.end(); ++i)
3355 : {
3356 7462 : const sort_expression Type=*i;
3357 7462 : sort_expression result;
3358 7462 : if (TypeMatchA(Type,PosType,result))
3359 : {
3360 7455 : DataTerm=data::function_symbol(Name,result);
3361 7455 : NewParList.push_front(result);
3362 : }
3363 7462 : }
3364 7462 : sort_expression_list ParList=reverse(NewParList);
3365 7462 : if (ParList.empty())
3366 : {
3367 : // Try to do the matching again with relaxed typing.
3368 14 : for (sort_expression_list::const_iterator i=TypeList.begin(); i!=TypeList.end(); ++i)
3369 : {
3370 7 : sort_expression Type=*i;
3371 7 : if (is_untyped_identifier(DataTerm) )
3372 : {
3373 7 : DataTerm=data::function_symbol(Name,Type);
3374 : }
3375 7 : Type=UpCastNumericType(PosType,Type,DataTerm,DeclaredVars,strictly_ambiguous,warn_upcasting,print_cast_error);
3376 : // if (EqTypesA(Type,PosType))
3377 7 : sort_expression result;
3378 7 : if (TypeMatchA(Type,PosType,result))
3379 : {
3380 7 : NewParList.push_front(result);
3381 : }
3382 7 : }
3383 7 : ParList=reverse(NewParList);
3384 : }
3385 :
3386 7462 : if (ParList.empty())
3387 : {
3388 0 : throw mcrl2::runtime_error("No system constant " + data::pp(DataTerm) + " with type " + data::pp(PosType) + ".");
3389 : }
3390 :
3391 7462 : if (ParList.size()==1)
3392 : {
3393 7462 : const sort_expression& Type=ParList.front();
3394 :
3395 7462 : if (is_untyped_identifier(DataTerm) )
3396 : {
3397 0 : assert(0);
3398 : DataTerm=data::function_symbol(Name,Type);
3399 : }
3400 : try
3401 : {
3402 14924 : sort_expression r= UpCastNumericType(PosType,Type,DataTerm,DeclaredVars,strictly_ambiguous,warn_upcasting,print_cast_error);
3403 7462 : return r;
3404 7462 : }
3405 0 : catch (mcrl2::runtime_error& e)
3406 : {
3407 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nNo constant " + data::pp(DataTerm) + " with type " + data::pp(PosType) + ".");
3408 0 : }
3409 : }
3410 : else
3411 : {
3412 0 : DataTerm=data::function_symbol(Name,data::untyped_sort());
3413 0 : return data::untyped_sort();
3414 : }
3415 7462 : }
3416 :
3417 202 : const std::map <core::identifier_string,sort_expression_list>::const_iterator j_context=user_functions.find(Name);
3418 202 : const std::map <core::identifier_string,sort_expression_list>::const_iterator j_gssystem=system_functions.find(Name);
3419 :
3420 202 : sort_expression_list ParList;
3421 202 : if (j_context==user_functions.end())
3422 : {
3423 130 : if (j_gssystem!=system_functions.end())
3424 : {
3425 17 : ParList=j_gssystem->second; // The function only occurs in the system.
3426 : }
3427 : else
3428 : {
3429 113 : throw mcrl2::runtime_error("Unknown operation " + core::pp(Name) + ".");
3430 : }
3431 : }
3432 72 : else if (j_gssystem==system_functions.end())
3433 : {
3434 72 : ParList=j_context->second; // only the context sorts are defined.
3435 : }
3436 : else // Both are defined.
3437 : {
3438 0 : ParList=j_gssystem->second+j_context->second;
3439 : }
3440 :
3441 :
3442 89 : if (ParList.size()==1)
3443 : {
3444 80 : const sort_expression& Type=ParList.front();
3445 80 : DataTerm=data::function_symbol(Name,Type);
3446 : try
3447 : {
3448 108 : return UpCastNumericType(PosType,Type,DataTerm,DeclaredVars,strictly_ambiguous,warn_upcasting,print_cast_error);
3449 : }
3450 14 : catch (mcrl2::runtime_error& e)
3451 : {
3452 14 : throw mcrl2::runtime_error(std::string(e.what()) + "\nNo constant " + data::pp(DataTerm) + " with type " + data::pp(PosType) + ".");
3453 14 : }
3454 : }
3455 : else
3456 : {
3457 18 : return TraverseVarConsTypeDN(DeclaredVars, DataTerm, PosType, strictly_ambiguous, std::string::npos, warn_upcasting,print_cast_error);
3458 : }
3459 29658 : }
3460 :
3461 0 : throw mcrl2::runtime_error("Internal type checking error: " + data::pp(DataTerm) + " does not match any type checking case." );
3462 : }
3463 :
3464 4577 : void mcrl2::data::data_type_checker::read_constructors_and_mappings(const function_symbol_vector& constructors, const function_symbol_vector& mappings, const function_symbol_vector& normalized_constructors)
3465 : {
3466 4577 : std::size_t constr_number=constructors.size();
3467 4577 : function_symbol_vector functions_and_constructors=constructors;
3468 4577 : functions_and_constructors.insert(functions_and_constructors.end(),mappings.begin(),mappings.end());
3469 5659 : for (const function_symbol& Func: functions_and_constructors)
3470 : {
3471 1087 : const core::identifier_string& FuncName=Func.name();
3472 1087 : sort_expression FuncType=Func.sort();
3473 :
3474 1087 : check_sort_is_declared(FuncType);
3475 :
3476 : //if FuncType is a defined function sort, unwind it
3477 1087 : if (is_basic_sort(FuncType))
3478 : {
3479 259 : const sort_expression NewFuncType=UnwindType(FuncType);
3480 259 : if (is_function_sort(NewFuncType))
3481 : {
3482 10 : FuncType=NewFuncType;
3483 : }
3484 259 : }
3485 :
3486 1087 : if (is_function_sort(FuncType))
3487 : {
3488 797 : add_function(data::function_symbol(FuncName,FuncType),"function");
3489 : }
3490 : else
3491 : {
3492 : try
3493 : {
3494 302 : add_constant(data::function_symbol(FuncName,FuncType),"constant");
3495 : }
3496 2 : catch (mcrl2::runtime_error& e)
3497 : {
3498 2 : throw mcrl2::runtime_error(std::string(e.what()) + "\nCould not add constant.");
3499 2 : }
3500 : }
3501 :
3502 1083 : if (constr_number)
3503 : {
3504 77 : constr_number--;
3505 :
3506 : //Here checks for the constructors
3507 77 : sort_expression ConstructorType=FuncType;
3508 77 : if (is_function_sort(ConstructorType))
3509 : {
3510 30 : ConstructorType=down_cast<function_sort>(ConstructorType).codomain();
3511 : }
3512 77 : ConstructorType=UnwindType(ConstructorType);
3513 385 : if (!is_basic_sort(ConstructorType) ||
3514 154 : sort_bool::is_bool(sort_expression(ConstructorType)) ||
3515 153 : sort_pos::is_pos(sort_expression(ConstructorType)) ||
3516 153 : sort_nat::is_nat(sort_expression(ConstructorType)) ||
3517 307 : sort_int::is_int(sort_expression(ConstructorType)) ||
3518 153 : sort_real::is_real(sort_expression(ConstructorType))
3519 : )
3520 : {
3521 1 : throw mcrl2::runtime_error("Could not add constructor " + core::pp(FuncName) + " of sort " + data::pp(FuncType) + ". Constructors of built-in sorts are not allowed.");
3522 : }
3523 77 : }
3524 1087 : }
3525 :
3526 : // Check that the constructors are defined such that they cannot generate an empty sort.
3527 : // E.g. in the specification sort D; cons f:D->D; the sort D must be necessarily empty, which is
3528 : // forbidden. The function below checks whether such malicious specifications occur.
3529 :
3530 4572 : check_for_empty_constructor_domains(normalized_constructors); // throws exception if not ok.
3531 4577 : }
3532 :
3533 1310 : void mcrl2::data::data_type_checker::add_constant(const data::function_symbol& f, const std::string& msg)
3534 : {
3535 1310 : const core::identifier_string& Name = f.name();
3536 1310 : const sort_expression& Sort = f.sort();
3537 :
3538 1310 : if (user_constants.count(Name)>0)
3539 : {
3540 3 : throw mcrl2::runtime_error("Double declaration of " + msg + " " + core::pp(Name) + ".");
3541 : }
3542 :
3543 1307 : if (system_constants.count(Name)>0 || system_functions.count(Name)>0)
3544 : {
3545 0 : throw mcrl2::runtime_error("Attempt to declare a constant with the name that is a built-in identifier (" + core::pp(Name) + ").");
3546 : }
3547 :
3548 1307 : user_constants[Name]=normalize_sorts(Sort,get_sort_specification());
3549 1307 : }
3550 :
3551 :
3552 55241 : bool mcrl2::data::data_type_checker::TypeMatchL(
3553 : const sort_expression_list& TypeList,
3554 : const sort_expression_list& PosTypeList,
3555 : sort_expression_list& result) const
3556 : {
3557 55241 : if (TypeList.size()!=PosTypeList.size())
3558 : {
3559 0 : return false;
3560 : }
3561 :
3562 55241 : sort_expression_list Result;
3563 55241 : sort_expression_list::const_iterator j=PosTypeList.begin();
3564 112205 : for (sort_expression_list::const_iterator i=TypeList.begin(); i!=TypeList.end(); ++i, ++j)
3565 : {
3566 75095 : sort_expression Type;
3567 75095 : if (!TypeMatchA(*i,*j,Type))
3568 : {
3569 18131 : return false;
3570 : }
3571 56964 : Result.push_front(Type);
3572 75095 : }
3573 37110 : result=reverse(Result);
3574 37110 : return true;
3575 55241 : }
3576 :
3577 :
3578 508306 : sort_expression mcrl2::data::data_type_checker::UnwindType(const sort_expression& Type) const
3579 : {
3580 508306 : return normalize_sorts(Type,get_sort_specification());
3581 : }
3582 :
3583 0 : variable mcrl2::data::data_type_checker::UnwindType(const variable& v) const
3584 : {
3585 0 : return variable(v.name(),UnwindType(v.sort()));
3586 : }
3587 :
3588 266245 : bool mcrl2::data::data_type_checker::TypeMatchA(
3589 : const sort_expression& Type_in,
3590 : const sort_expression& PosType_in,
3591 : sort_expression& result) const
3592 : {
3593 : // Checks if Type and PosType match by instantiating unknown sorts.
3594 : // It returns the matching instantiation of Type in result. If matching fails,
3595 : // it returns false, otherwise true.
3596 :
3597 266245 : sort_expression Type=Type_in;
3598 266245 : sort_expression PosType=PosType_in;
3599 :
3600 266245 : if (data::is_untyped_sort(Type))
3601 : {
3602 17401 : result=PosType;
3603 17401 : return true;
3604 : }
3605 248844 : if (data::is_untyped_sort(PosType) || EqTypesA(Type,PosType))
3606 : {
3607 114302 : result=Type;
3608 114302 : return true;
3609 : }
3610 134542 : if (is_untyped_possible_sorts(Type) && !is_untyped_possible_sorts(PosType))
3611 : {
3612 544 : PosType.swap(Type);
3613 : }
3614 134542 : if (is_untyped_possible_sorts(PosType))
3615 : {
3616 14182 : sort_expression_list NewTypeList;
3617 14182 : const untyped_possible_sorts& mps=down_cast<const untyped_possible_sorts>(PosType);
3618 61946 : for (sort_expression_list::const_iterator i=mps.sorts().begin(); i!=mps.sorts().end(); ++i)
3619 : {
3620 47764 : sort_expression NewPosType= *i;
3621 :
3622 47764 : sort_expression new_type;
3623 47764 : if (TypeMatchA(Type,NewPosType,new_type))
3624 : {
3625 8480 : NewPosType=new_type;
3626 : // Avoid double insertions.
3627 8480 : if (std::find(NewTypeList.begin(),NewTypeList.end(),NewPosType)==NewTypeList.end())
3628 : {
3629 8480 : NewTypeList.push_front(NewPosType);
3630 : }
3631 : }
3632 47764 : }
3633 14182 : if (NewTypeList.empty())
3634 : {
3635 5716 : return false;
3636 : }
3637 8466 : if (NewTypeList.tail().empty())
3638 : {
3639 8459 : result=NewTypeList.front();
3640 8459 : return true;
3641 : }
3642 :
3643 7 : result=untyped_possible_sorts(sort_expression_list(reverse(NewTypeList)));
3644 7 : return true;
3645 14182 : }
3646 :
3647 120360 : if (is_basic_sort(Type))
3648 : {
3649 38015 : Type=UnwindType(Type);
3650 : }
3651 120360 : if (is_basic_sort(PosType))
3652 : {
3653 57277 : PosType=UnwindType(PosType);
3654 : }
3655 120360 : if (is_container_sort(Type))
3656 : {
3657 27100 : const container_sort& s=down_cast<container_sort>(Type);
3658 27100 : const container_type& ConsType = s.container_name();
3659 27100 : if (is_list_container(ConsType))
3660 : {
3661 3641 : if (!sort_list::is_list(PosType))
3662 : {
3663 924 : return false;
3664 : }
3665 2717 : sort_expression Res;
3666 2717 : if (!TypeMatchA(s.element_sort(),down_cast<container_sort>(PosType).element_sort(),Res))
3667 : {
3668 57 : return false;
3669 : }
3670 2660 : result=sort_list::list(Res);
3671 2660 : return true;
3672 2717 : }
3673 :
3674 23459 : if (is_set_container(ConsType))
3675 : {
3676 4941 : if (!sort_set::is_set(PosType))
3677 : {
3678 4621 : return false;
3679 : }
3680 : else
3681 : {
3682 320 : sort_expression Res;
3683 320 : if (!TypeMatchA(s.element_sort(),down_cast<container_sort>(PosType).element_sort(),Res))
3684 : {
3685 2 : return false;
3686 : }
3687 318 : result=sort_set::set_(Res);
3688 318 : return true;
3689 320 : }
3690 : }
3691 :
3692 18518 : if (is_bag_container(ConsType))
3693 : {
3694 3694 : if (!sort_bag::is_bag(PosType))
3695 : {
3696 3402 : return false;
3697 : }
3698 : else
3699 : {
3700 292 : sort_expression Res;
3701 292 : if (!TypeMatchA(s.element_sort(),down_cast<container_sort>(PosType).element_sort(),Res))
3702 : {
3703 8 : return false;
3704 : }
3705 284 : result=sort_bag::bag(Res);
3706 284 : return true;
3707 292 : }
3708 : }
3709 :
3710 14824 : if (is_fset_container(ConsType))
3711 : {
3712 7390 : if (!sort_fset::is_fset(PosType))
3713 : {
3714 6956 : return false;
3715 : }
3716 : else
3717 : {
3718 434 : sort_expression Res;
3719 434 : if (!TypeMatchA(s.element_sort(),down_cast<container_sort>(PosType).element_sort(),Res))
3720 : {
3721 3 : return false;
3722 : }
3723 431 : result=sort_fset::fset(Res);
3724 431 : return true;
3725 434 : }
3726 : }
3727 :
3728 7434 : if (is_fbag_container(ConsType))
3729 : {
3730 7434 : if (!sort_fbag::is_fbag(PosType))
3731 : {
3732 7063 : return false;
3733 : }
3734 : else
3735 : {
3736 371 : sort_expression Res;
3737 371 : if (!TypeMatchA(s.element_sort(),down_cast<container_sort>(PosType).element_sort(),Res))
3738 : {
3739 1 : return false;
3740 : }
3741 370 : result=sort_fbag::fbag(Res);
3742 370 : return true;
3743 371 : }
3744 : }
3745 : }
3746 :
3747 93260 : if (is_function_sort(Type))
3748 : {
3749 55239 : if (!is_function_sort(PosType))
3750 : {
3751 75 : return false;
3752 : }
3753 : else
3754 : {
3755 55164 : const function_sort& fs=down_cast<const function_sort>(Type);
3756 55164 : const function_sort& posfs=down_cast<const function_sort>(PosType);
3757 55164 : sort_expression_list ArgTypes;
3758 55164 : if (!TypeMatchL(fs.domain(),posfs.domain(),ArgTypes))
3759 : {
3760 18125 : return false;
3761 : }
3762 37039 : sort_expression ResType;
3763 37039 : if (!TypeMatchA(fs.codomain(),posfs.codomain(),ResType))
3764 : {
3765 1051 : return false;
3766 : }
3767 35988 : result=function_sort(ArgTypes,ResType);
3768 35988 : return true;
3769 55164 : }
3770 : }
3771 :
3772 38021 : return false;
3773 266245 : }
3774 :
3775 :
3776 32046 : void mcrl2::data::data_type_checker::add_system_constant(const data::function_symbol& f)
3777 : {
3778 : // append the Type to the entry of the Name of the OpId in system constants table
3779 :
3780 32046 : const core::identifier_string& OpIdName = f.name();
3781 32046 : const sort_expression& Type = f.sort();
3782 :
3783 32046 : std::map<core::identifier_string,sort_expression_list>::const_iterator i=system_constants.find(OpIdName);
3784 :
3785 32046 : sort_expression_list Types;
3786 32046 : if (i!=system_constants.end())
3787 : {
3788 0 : Types=i->second;
3789 : }
3790 32046 : Types=push_back(Types,Type);
3791 32046 : system_constants[OpIdName]=Types;
3792 32046 : }
3793 :
3794 755370 : void mcrl2::data::data_type_checker::add_system_function(const data::function_symbol& f)
3795 : {
3796 : //Pre: OpId is an OpId
3797 : // append the Type to the entry of the Name of the OpId in gssystem.functions table
3798 755370 : const core::identifier_string& OpIdName = f.name();
3799 755370 : const sort_expression& Type = f.sort();
3800 755370 : assert(is_function_sort(Type));
3801 :
3802 755370 : const std::map <core::identifier_string,sort_expression_list>::const_iterator j=system_functions.find(OpIdName);
3803 :
3804 755370 : sort_expression_list Types;
3805 755370 : if (j!=system_functions.end())
3806 : {
3807 325038 : Types=j->second;
3808 : }
3809 1510740 : Types=Types + sort_expression_list({ Type }); // TODO: Avoid concatenate but the order is essential.
3810 755370 : system_functions[OpIdName]=Types;
3811 755370 : }
3812 :
3813 77826 : void mcrl2::data::data_type_checker::add_system_constants_and_functions(const std::vector<data::function_symbol>& v)
3814 : {
3815 718746 : for(const function_symbol& f: v)
3816 : {
3817 640920 : if (is_function_sort(f.sort()))
3818 : {
3819 608874 : add_system_function(f);
3820 : }
3821 : else
3822 : {
3823 32046 : add_system_constant(f);
3824 : }
3825 : }
3826 77826 : }
3827 :
3828 4578 : void mcrl2::data::data_type_checker::initialise_system_defined_functions(void)
3829 : {
3830 : //Creation of operation identifiers for system defined operations.
3831 : //Bool
3832 4578 : add_system_function(if_(data::untyped_sort()));
3833 4578 : add_system_function(less(data::untyped_sort()));
3834 4578 : add_system_function(less_equal(data::untyped_sort()));
3835 4578 : add_system_function(greater_equal(data::untyped_sort()));
3836 4578 : add_system_function(greater(data::untyped_sort()));
3837 4578 : add_system_function(equal_to(data::untyped_sort()));
3838 4578 : add_system_function(not_equal_to(data::untyped_sort()));
3839 :
3840 : //Bool
3841 4578 : add_system_constants_and_functions(sort_bool::bool_mCRL2_usable_constructors());
3842 4578 : add_system_constants_and_functions(sort_bool::bool_mCRL2_usable_mappings());
3843 : // add_system_constants_and_functions(sort_bool::bool_generate_constructors_and_functions_code());
3844 :
3845 : //Numbers
3846 4578 : add_system_constants_and_functions(sort_pos::pos_mCRL2_usable_constructors());
3847 4578 : add_system_constants_and_functions(sort_pos::pos_mCRL2_usable_mappings());
3848 4578 : assert(system_constants.find(sort_pos::c1().name())!=system_constants.end());
3849 : // This function is explicitly required by the typechecker.
3850 : // It adds it and then typechecks the terms containing this function.
3851 4578 : add_system_constants_and_functions(sort_nat::nat_mCRL2_usable_constructors());
3852 4578 : add_system_constants_and_functions(sort_nat::nat_mCRL2_usable_mappings());
3853 4578 : assert(system_functions.find(sort_nat::cnat().name())!=system_functions.end());
3854 : // This function is explicitly required by the typechecker.
3855 : // It adds it and then typechecks the terms containing this function.
3856 4578 : add_system_constants_and_functions(sort_int::int_mCRL2_usable_constructors());
3857 4578 : add_system_constants_and_functions(sort_int::int_mCRL2_usable_mappings());
3858 4578 : assert(system_functions.find(sort_int::cint().name())!=system_functions.end());
3859 : // This function is explicitly required by the typechecker.
3860 : // It adds it and then typechecks the terms containing this function.
3861 4578 : add_system_constants_and_functions(sort_real::real_mCRL2_usable_constructors());
3862 4578 : add_system_constants_and_functions(sort_real::real_mCRL2_usable_mappings());
3863 4578 : assert(system_functions.find(sort_real::creal().name())!=system_functions.end());
3864 : // This function is explicitly required by the typechecker.
3865 : // It adds it and then typechecks the terms containing this function.
3866 :
3867 : //Lists
3868 4578 : add_system_constants_and_functions(sort_list::list_mCRL2_usable_constructors(data::untyped_sort()));
3869 4578 : add_system_constants_and_functions(sort_list::list_mCRL2_usable_mappings(data::untyped_sort()));
3870 :
3871 : //FSets
3872 4578 : add_system_constants_and_functions(sort_fset::fset_mCRL2_usable_constructors(data::untyped_sort()));
3873 4578 : add_system_constants_and_functions(sort_fset::fset_mCRL2_usable_mappings(data::untyped_sort()));
3874 :
3875 : //Sets
3876 : // add_system_constants_and_functions(sort_set::set_mCRL2_usable_constructors(data::untyped_sort()));
3877 : // add_system_constants_and_functions(sort_set::set_mCRL2_usable_mappings(data::untyped_sort()));
3878 4578 : add_system_function(sort_set::false_function(data::untyped_sort())); // Needed as it is used within the typechecker.
3879 4578 : add_system_function(sort_set::constructor(data::untyped_sort())); // Needed as it is used within the typechecker.
3880 :
3881 4578 : add_system_function(sort_set::in(data::untyped_sort(), data::untyped_sort(), sort_fset::fset(data::untyped_sort())));
3882 4578 : add_system_function(sort_set::in(data::untyped_sort(), data::untyped_sort(), sort_set::set_(data::untyped_sort())));
3883 4578 : add_system_function(sort_set::union_(data::untyped_sort(), sort_fset::fset(data::untyped_sort()), sort_fset::fset(data::untyped_sort())));
3884 4578 : add_system_function(sort_set::union_(data::untyped_sort(), sort_set::set_(data::untyped_sort()), sort_set::set_(data::untyped_sort())));
3885 4578 : add_system_function(sort_set::difference(data::untyped_sort(), sort_fset::fset(data::untyped_sort()), sort_fset::fset(data::untyped_sort())));
3886 4578 : add_system_function(sort_set::difference(data::untyped_sort(), sort_set::set_(data::untyped_sort()), sort_set::set_(data::untyped_sort())));
3887 4578 : add_system_function(sort_set::intersection(data::untyped_sort(), sort_fset::fset(data::untyped_sort()), sort_fset::fset(data::untyped_sort())));
3888 4578 : add_system_function(sort_set::intersection(data::untyped_sort(), sort_set::set_(data::untyped_sort()), sort_set::set_(data::untyped_sort())));
3889 : // **** add_system_function(sort_bag::set2bag(data::untyped_sort()));
3890 : // add_system_constant(sort_set::empty(data::untyped_sort()));
3891 : // add_system_function(sort_set::in(data::untyped_sort()));
3892 : // add_system_function(sort_set::union_(data::untyped_sort()));
3893 : // add_system_function(sort_set::difference(data::untyped_sort()));
3894 : // add_system_function(sort_set::intersection(data::untyped_sort()));
3895 4578 : add_system_function(sort_set::complement(data::untyped_sort()));
3896 :
3897 : //FBags
3898 4578 : add_system_constants_and_functions(sort_fbag::fbag_mCRL2_usable_constructors(data::untyped_sort()));
3899 4578 : add_system_constants_and_functions(sort_fbag::fbag_mCRL2_usable_mappings(data::untyped_sort()));
3900 : /* add_system_constant(sort_fbag::empty(data::untyped_sort()));
3901 : // add_system_function(sort_fbag::count(data::untyped_sort()));
3902 : // add_system_function(sort_fbag::in(data::untyped_sort()));
3903 : // add_system_function(sort_fbag::union_(data::untyped_sort()));
3904 : // add_system_function(sort_fbag::intersection(data::untyped_sort()));
3905 : // add_system_function(sort_fbag::difference(data::untyped_sort()));
3906 : add_system_function(sort_fbag::count_all(data::untyped_sort()));
3907 : add_system_function(sort_fbag::cinsert(data::untyped_sort())); // Needed as it is used within the typechecker. */
3908 :
3909 : //Bags
3910 4578 : add_system_function(sort_bag::bag2set(data::untyped_sort()));
3911 4578 : add_system_function(sort_bag::set2bag(data::untyped_sort()));
3912 4578 : add_system_function(sort_bag::in(data::untyped_sort(), data::untyped_sort(), sort_fbag::fbag(data::untyped_sort())));
3913 4578 : add_system_function(sort_bag::in(data::untyped_sort(), data::untyped_sort(), sort_bag::bag(data::untyped_sort())));
3914 4578 : add_system_function(sort_bag::union_(data::untyped_sort(), sort_fbag::fbag(data::untyped_sort()), sort_fbag::fbag(data::untyped_sort())));
3915 4578 : add_system_function(sort_bag::union_(data::untyped_sort(), sort_bag::bag(data::untyped_sort()), sort_bag::bag(data::untyped_sort())));
3916 4578 : add_system_function(sort_bag::difference(data::untyped_sort(), sort_fbag::fbag(data::untyped_sort()), sort_fbag::fbag(data::untyped_sort())));
3917 4578 : add_system_function(sort_bag::difference(data::untyped_sort(), sort_bag::bag(data::untyped_sort()), sort_bag::bag(data::untyped_sort())));
3918 4578 : add_system_function(sort_bag::intersection(data::untyped_sort(), sort_fbag::fbag(data::untyped_sort()), sort_fbag::fbag(data::untyped_sort())));
3919 4578 : add_system_function(sort_bag::intersection(data::untyped_sort(), sort_bag::bag(data::untyped_sort()), sort_bag::bag(data::untyped_sort())));
3920 4578 : add_system_function(sort_bag::count(data::untyped_sort(), data::untyped_sort(), sort_fbag::fbag(data::untyped_sort())));
3921 4578 : add_system_function(sort_bag::count(data::untyped_sort(), data::untyped_sort(), sort_bag::bag(data::untyped_sort())));
3922 : // add_system_constant(sort_bag::empty(data::untyped_sort()));
3923 : // add_system_function(sort_bag::in(data::untyped_sort()));
3924 : //**** add_system_function(sort_bag::count(data::untyped_sort()));
3925 : // add_system_function(sort_bag::count(data::untyped_sort(), data::untyped_sort(), sort_fset::fset(data::untyped_sort())));
3926 : //add_system_function(sort_bag::join(data::untyped_sort()));
3927 : // add_system_function(sort_bag::difference(data::untyped_sort()));
3928 : // add_system_function(sort_bag::intersection(data::untyped_sort()));
3929 4578 : add_system_function(sort_bag::zero_function(data::untyped_sort())); // Needed as it is used within the typechecker.
3930 4578 : add_system_function(sort_bag::constructor(data::untyped_sort())); // Needed as it is used within the typechecker.
3931 :
3932 : // function update
3933 : // add_system_constants_and_functions(data::function_update_mCRL2_usable_constructors());
3934 4578 : add_system_constants_and_functions(data::function_update_mCRL2_usable_mappings(data::untyped_sort(),data::untyped_sort()));
3935 4578 : }
3936 :
3937 1127 : void mcrl2::data::data_type_checker::add_function(const data::function_symbol& f, const std::string& msg, bool allow_double_decls)
3938 : {
3939 1127 : const sort_expression_list domain=function_sort(f.sort()).domain();
3940 1127 : const core::identifier_string& Name = f.name();
3941 1127 : const sort_expression& Sort = f.sort();
3942 :
3943 1127 : if (system_constants.count(Name)>0)
3944 : {
3945 0 : throw mcrl2::runtime_error("Attempt to redeclare the system constant with a " + msg + " " + data::pp(f) + ".");
3946 : }
3947 :
3948 1127 : if (system_functions.count(Name)>0)
3949 : {
3950 2 : throw mcrl2::runtime_error("Attempt to redeclare a system function with a " + msg + " " + data::pp(f) + ".");
3951 : }
3952 :
3953 1125 : std::map <core::identifier_string,sort_expression_list>::const_iterator j=user_functions.find(Name);
3954 :
3955 : // the table user_functions contains a list of types for each
3956 : // function name. We need to check if there is already such a type
3957 : // in the list. If so -- error, otherwise -- add
3958 1125 : if (j!=user_functions.end())
3959 : {
3960 116 : sort_expression_list Types=j->second;
3961 116 : if (InTypesA(Sort, Types))
3962 : {
3963 1 : if (!allow_double_decls)
3964 : {
3965 0 : throw mcrl2::runtime_error("Double declaration of " + msg + " " + core::pp(Name) + ".");
3966 : }
3967 : }
3968 232 : Types = Types + sort_expression_list({ UnwindType(Sort) });
3969 116 : user_functions[Name]=Types;
3970 116 : }
3971 : else
3972 : {
3973 2018 : user_functions[Name] = sort_expression_list({ UnwindType(Sort) });
3974 : }
3975 1127 : }
3976 :
3977 1285 : void mcrl2::data::data_type_checker::read_sort(const sort_expression& sort_expr)
3978 : {
3979 1285 : if (is_basic_sort(sort_expr))
3980 : {
3981 469 : check_basic_sort_is_declared(down_cast<basic_sort>(sort_expr));
3982 469 : return;
3983 : }
3984 :
3985 816 : if (is_container_sort(sort_expr))
3986 : {
3987 142 : return read_sort(down_cast<container_sort>(sort_expr).element_sort());
3988 : }
3989 :
3990 674 : if (is_function_sort(sort_expr))
3991 : {
3992 51 : const function_sort& fs = atermpp::down_cast<function_sort>(sort_expr);
3993 51 : read_sort(fs.codomain());
3994 :
3995 102 : for (const sort_expression& s: fs.domain())
3996 : {
3997 51 : read_sort(s);
3998 : }
3999 51 : return;
4000 : }
4001 :
4002 623 : if (is_structured_sort(sort_expr))
4003 : {
4004 : // The map below is used to warn that there are projections with the same name
4005 : // in this structured sort. This hardly ever serves a purpose and gives rise confusion.
4006 623 : std::map<core::identifier_string, sort_expression> duplicate_projections_warner;
4007 623 : const structured_sort& struct_sort = atermpp::down_cast<structured_sort>(sort_expr);
4008 1804 : for (const structured_sort_constructor& constr: struct_sort.constructors())
4009 : {
4010 : // recognizer -- if present -- a function from SortExpr to Bool
4011 1182 : core::identifier_string Name=constr.recogniser();
4012 1182 : if (Name!=core::empty_identifier_string())
4013 : {
4014 132 : add_function(data::function_symbol(Name,function_sort(sort_expression_list({ sort_expr }),sort_bool::bool_())),"recognizer");
4015 : }
4016 :
4017 : // constructor type and projections
4018 1182 : const structured_sort_constructor_argument_list& Projs=constr.arguments();
4019 1182 : Name=constr.name();
4020 1182 : if (Projs.empty())
4021 : {
4022 1017 : add_constant(data::function_symbol(Name,sort_expr),"constructor constant");
4023 1013 : continue;
4024 : }
4025 :
4026 168 : sort_expression_list ConstructorType;
4027 364 : for (const structured_sort_constructor_argument& proj: Projs)
4028 : {
4029 196 : if (!proj.name().empty() && duplicate_projections_warner.count(proj.name())>0 && duplicate_projections_warner[proj.name()]!=proj.sort())
4030 : {
4031 0 : mCRL2log(warning) << "Warning. Projection function " << proj.name() << " occurs multiple times with different sorts in " << struct_sort << ". " << std::endl;
4032 : }
4033 : else
4034 : {
4035 196 : duplicate_projections_warner[proj.name()]=proj.sort();
4036 : }
4037 196 : const sort_expression& proj_sort=proj.sort();
4038 :
4039 : // not to forget, recursive call for proj_sort ;-)
4040 196 : read_sort(proj_sort);
4041 :
4042 196 : const core::identifier_string& proj_name=proj.name();
4043 196 : if (proj_name!=core::empty_identifier_string())
4044 : {
4045 204 : add_function(function_symbol(proj_name,function_sort(sort_expression_list({ sort_expr }),proj_sort)),"projection",true);
4046 : }
4047 196 : ConstructorType.push_front(proj_sort);
4048 : }
4049 168 : add_function(data::function_symbol(Name,function_sort(reverse(ConstructorType),sort_expr)),"constructor");
4050 1182 : }
4051 622 : return;
4052 623 : }
4053 : }
4054 :
4055 0 : sort_expression_list mcrl2::data::data_type_checker::InsertType(const sort_expression_list& TypeList, const sort_expression& Type) const
4056 : {
4057 0 : for (const sort_expression& s: TypeList)
4058 : {
4059 0 : if (EqTypesA(s,Type))
4060 : {
4061 0 : return TypeList;
4062 : }
4063 : }
4064 0 : sort_expression_list result=TypeList;
4065 0 : result.push_front(Type);
4066 0 : return result;
4067 0 : }
4068 :
4069 :
4070 :
4071 :
4072 0 : bool mcrl2::data::data_type_checker::IsTypeAllowedA(const sort_expression& Type, const sort_expression& PosType) const
4073 : {
4074 : //Checks if Type is allowed by PosType
4075 0 : if (data::is_untyped_sort(data::sort_expression(PosType)))
4076 : {
4077 0 : return true;
4078 : }
4079 0 : if (is_untyped_possible_sorts(PosType))
4080 : {
4081 0 : return InTypesA(Type,down_cast<const untyped_possible_sorts>(PosType).sorts());
4082 : }
4083 :
4084 : //PosType is a normal type
4085 0 : return EqTypesA(Type,PosType);
4086 : }
4087 :
4088 0 : bool mcrl2::data::data_type_checker::IsTypeAllowedL(const sort_expression_list& TypeList, const sort_expression_list& PosTypeList) const
4089 : {
4090 : //Checks if TypeList is allowed by PosTypeList (each respective element)
4091 0 : assert(TypeList.size()==PosTypeList.size());
4092 0 : sort_expression_list::const_iterator j=PosTypeList.begin();
4093 0 : for (sort_expression_list::const_iterator i=TypeList.begin(); i!=TypeList.end(); ++i,++j)
4094 0 : if (!IsTypeAllowedA(*i,*j))
4095 : {
4096 0 : return false;
4097 : }
4098 0 : return true;
4099 : }
4100 :
4101 0 : bool mcrl2::data::data_type_checker::IsNotInferredL(sort_expression_list TypeList) const
4102 : {
4103 0 : for (const sort_expression& Type: TypeList)
4104 : {
4105 0 : if (is_untyped_sort(Type) || is_untyped_possible_sorts(Type))
4106 : {
4107 0 : return true;
4108 : }
4109 : }
4110 0 : return false;
4111 : }
4112 :
4113 :
4114 :
4115 0 : std::pair<bool,sort_expression_list> mcrl2::data::data_type_checker::AdjustNotInferredList(
4116 : const sort_expression_list& PosTypeList,
4117 : const term_list<sort_expression_list>& TypeListList) const
4118 : {
4119 : // PosTypeList -- List of Sortexpressions (possibly NotInferred(List Sortexpr))
4120 : // TypeListList -- List of (Lists of Types)
4121 : // returns: PosTypeList, adjusted to the elements of TypeListList
4122 : // NULL if cannot be ajusted.
4123 :
4124 : //if PosTypeList has only normal types -- check if it is in TypeListList,
4125 : //if so return PosTypeList, otherwise return false.
4126 0 : if (!IsNotInferredL(PosTypeList))
4127 : {
4128 0 : if (InTypesL(PosTypeList,TypeListList))
4129 : {
4130 0 : return std::make_pair(true,PosTypeList);
4131 : }
4132 : else
4133 : {
4134 0 : return std::make_pair(false, sort_expression_list());
4135 : }
4136 : }
4137 :
4138 : //Filter TypeListList to contain only compatible with TypeList lists of parameters.
4139 0 : term_list<sort_expression_list> NewTypeListList;
4140 0 : for (term_list<sort_expression_list>::const_iterator i=TypeListList.begin();
4141 0 : i!=TypeListList.end(); ++i)
4142 : {
4143 0 : sort_expression_list TypeList= *i;
4144 0 : if (IsTypeAllowedL(TypeList,PosTypeList))
4145 : {
4146 0 : NewTypeListList.push_front(TypeList);
4147 : }
4148 0 : }
4149 0 : if (NewTypeListList.empty())
4150 : {
4151 0 : return std::make_pair(false, sort_expression_list());
4152 : }
4153 0 : if (NewTypeListList.size()==1)
4154 : {
4155 0 : return std::make_pair(true,NewTypeListList.front());
4156 : }
4157 :
4158 : // otherwise return not inferred.
4159 0 : return std::make_pair(true,GetNotInferredList(reverse(NewTypeListList)));
4160 0 : }
4161 :
4162 :
4163 0 : sort_expression_list mcrl2::data::data_type_checker::GetNotInferredList(const term_list<sort_expression_list>& TypeListList) const
4164 : {
4165 : //we get: List of Lists of SortExpressions
4166 : //Outer list: possible parameter types 0..nPosParsVectors-1
4167 : //inner lists: parameter types vectors 0..nFormPars-1
4168 :
4169 : //we constuct 1 vector (list) of sort expressions (NotInferred if ambiguous)
4170 : //0..nFormPars-1
4171 :
4172 0 : sort_expression_list Result;
4173 0 : std::size_t nFormPars=TypeListList.front().size();
4174 0 : std::vector<sort_expression_list> Pars(nFormPars);
4175 0 : for (std::size_t i=0; i<nFormPars; i++)
4176 : {
4177 0 : Pars[i]=sort_expression_list();
4178 : }
4179 :
4180 0 : for (term_list<sort_expression_list>::const_iterator j=TypeListList.begin(); j!=TypeListList.end(); ++j)
4181 : {
4182 0 : sort_expression_list TypeList=*j;
4183 0 : for (std::size_t i=0; i<nFormPars; TypeList=TypeList.tail(),i++)
4184 : {
4185 0 : Pars[i]=InsertType(Pars[i],TypeList.front());
4186 : }
4187 0 : }
4188 :
4189 0 : for (std::size_t i=nFormPars; i>0; i--)
4190 : {
4191 0 : sort_expression Sort;
4192 0 : if (Pars[i-1].size()==1)
4193 : {
4194 0 : Sort=Pars[i-1].front();
4195 : }
4196 : else
4197 : {
4198 0 : Sort=untyped_possible_sorts(sort_expression_list(reverse(Pars[i-1])));
4199 : }
4200 0 : Result.push_front(Sort);
4201 0 : }
4202 0 : return Result;
4203 0 : }
4204 :
4205 4585 : mcrl2::data::data_type_checker::data_type_checker(const data_specification& data_spec)
4206 : : sort_type_checker(data_spec),
4207 4585 : was_warning_upcasting(false)
4208 : {
4209 4578 : initialise_system_defined_functions();
4210 :
4211 : try
4212 : {
4213 5422 : for (const alias& a: get_sort_specification().user_defined_aliases())
4214 : {
4215 845 : read_sort(a.reference());
4216 : }
4217 4577 : read_constructors_and_mappings(data_spec.user_defined_constructors(),data_spec.user_defined_mappings(),data_spec.constructors());
4218 : }
4219 11 : catch (mcrl2::runtime_error& e)
4220 : {
4221 11 : throw mcrl2::runtime_error(std::string(e.what()) + "\nType checking of data expression failed.");
4222 11 : }
4223 :
4224 4567 : type_checked_data_spec=data_spec;
4225 :
4226 : // Type check equations and add them to the specification.
4227 : try
4228 : {
4229 4567 : TransformVarConsTypeData(type_checked_data_spec);
4230 : }
4231 10 : catch (mcrl2::runtime_error& e)
4232 : {
4233 10 : type_checked_data_spec=data_specification(); // Type checking failed. Data specification is not usable.
4234 10 : throw mcrl2::runtime_error(std::string(e.what()) + "\nFailed to type check data specification.");
4235 10 : }
4236 4683 : }
4237 :
4238 0 : data_expression mcrl2::data::data_type_checker::operator()(
4239 : const data_expression& data_expr,
4240 : const detail::variable_context& context_variables) const
4241 : {
4242 0 : data_expression data=data_expr;
4243 0 : sort_expression Type;
4244 : try
4245 : {
4246 0 : Type=TraverseVarConsTypeD(context_variables,data,data::untyped_sort());
4247 : }
4248 0 : catch (mcrl2::runtime_error& e)
4249 : {
4250 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nType checking of data expression failed.");
4251 0 : }
4252 0 : if (data::is_untyped_sort(Type))
4253 : {
4254 0 : throw mcrl2::runtime_error("Type checking of data expression " + data::pp(data_expr) + " failed. Result is an unknown sort.");
4255 : }
4256 :
4257 0 : assert(strict_type_check(data));
4258 0 : return data;
4259 0 : }
4260 :
4261 :
4262 16788 : void mcrl2::data::data_type_checker::operator()(const variable& v,
4263 : const detail::variable_context& context_variables) const
4264 : {
4265 : // First check whether the variable name clashes with a system or user defined function or constant.
4266 16788 : const std::map<core::identifier_string,sort_expression_list>::const_iterator i1=system_constants.find(v.name());
4267 16788 : if (i1!=system_constants.end())
4268 : {
4269 0 : throw mcrl2::runtime_error("The variable " + core::pp(v.name()) + ":" + data::pp(v.sort()) +
4270 0 : " clashes with the system defined constant " + core::pp(i1->first) + ":" + data::pp(i1->second.front()) + ".");
4271 : }
4272 16788 : const std::map<core::identifier_string,sort_expression_list>::const_iterator i2=system_functions.find(v.name());
4273 16788 : if (i2!=system_functions.end())
4274 : {
4275 0 : throw mcrl2::runtime_error("The variable " + core::pp(v.name()) + ":" + data::pp(v.sort()) +
4276 0 : " clashes with the system defined function " + core::pp(i2->first) + ":" + data::pp(i2->second.front()) + ".");
4277 : }
4278 16788 : const std::map<core::identifier_string,sort_expression>::const_iterator i3=user_constants.find(v.name());
4279 16788 : if (i3!=user_constants.end())
4280 : {
4281 0 : throw mcrl2::runtime_error("The variable " + core::pp(v.name()) + ":" + data::pp(v.sort()) +
4282 0 : " clashes with the user defined constant " + core::pp(i3->first) + ":" + data::pp(i3->second) + ".");
4283 : }
4284 16788 : const std::map<core::identifier_string,sort_expression_list>::const_iterator i4=user_functions.find(v.name());
4285 16788 : if (i4!=user_functions.end())
4286 : {
4287 3 : throw mcrl2::runtime_error("The variable " + core::pp(v.name()) + ":" + data::pp(v.sort()) +
4288 4 : " clashes with the user defined function " + core::pp(i4->first) + ":" + data::pp(i4->second.front()) + ".");
4289 : }
4290 :
4291 : // Second, check that the variable has a valid sort.
4292 : try
4293 : {
4294 16787 : sort_type_checker::check_sort_is_declared(v.sort());
4295 : }
4296 0 : catch (mcrl2::runtime_error& e)
4297 : {
4298 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nType error while typechecking the data variable " + core::pp(v.name()) + ":" + data::pp(v.sort()) + ".");
4299 0 : }
4300 :
4301 : // Third, check that the variable did not occur in the context with a different type.
4302 16787 : const std::map<core::identifier_string,sort_expression>::const_iterator i=context_variables.context().find(v.name());
4303 16787 : sort_expression temp;
4304 16787 : if (i!=context_variables.context().end() && !TypeMatchA(i->second,v.sort(),temp))
4305 : {
4306 6 : throw mcrl2::runtime_error("The variable " + core::pp(v.name()) + ":" + data::pp(v.sort()) +
4307 8 : " is used in its surrounding context with a different sort " + core::pp(i->second) + ".");
4308 : }
4309 16787 : }
4310 :
4311 :
4312 :
4313 1452 : void mcrl2::data::data_type_checker::operator()(const variable_list& l,
4314 : const detail::variable_context& context_variables) const
4315 : {
4316 : // Type check each variable.
4317 8247 : for (const variable& v: l)
4318 : {
4319 6798 : (*this)(v, context_variables);
4320 : }
4321 :
4322 : // Check that all variable names are unique.
4323 1449 : std::set<core::identifier_string> variable_names;
4324 8244 : for (const variable& v: l)
4325 : {
4326 6795 : if (!variable_names.insert(v.name()).second) // The variable name is already in the set.
4327 : {
4328 0 : throw mcrl2::runtime_error("The variable " + data::pp(v) + " occurs multiple times.");
4329 : }
4330 : }
4331 1449 : }
4332 :
4333 : // ------------------------------ Here ends the new class based data expression checker -----------------------
4334 : // ------------------------------ Here starts the new class based data specification checker -----------------------
4335 :
4336 4567 : void mcrl2::data::data_type_checker::operator()(data_equation_vector& eqns)
4337 : {
4338 4567 : data_equation_vector resulting_equations;
4339 5597 : for (const data_equation& eqn: eqns)
4340 : {
4341 1040 : const variable_list& vars=eqn.variables();
4342 : try
4343 : {
4344 : // Typecheck the variables in an equation.
4345 1041 : (*this)(vars,detail::variable_context());
4346 : }
4347 1 : catch (mcrl2::runtime_error& e)
4348 : {
4349 1 : throw mcrl2::runtime_error(std::string(e.what()) + "\nThis error occurred while typechecking equation " + data::pp(eqn) + ".");
4350 1 : }
4351 :
4352 1039 : detail::variable_context DeclaredVars;
4353 1039 : DeclaredVars.add_context_variables(vars);
4354 :
4355 1039 : data_expression left=eqn.lhs();
4356 :
4357 1039 : sort_expression leftType;
4358 : try
4359 : {
4360 1045 : leftType=TraverseVarConsTypeD(DeclaredVars,left,data::untyped_sort(),true,true);
4361 : }
4362 6 : catch (mcrl2::runtime_error& e)
4363 : {
4364 6 : throw mcrl2::runtime_error(std::string(e.what()) + "\nError occurred while typechecking " + data::pp(left) + " as left hand side of equation " + data::pp(eqn) + ".");
4365 6 : }
4366 :
4367 1033 : if (was_warning_upcasting)
4368 : {
4369 1 : was_warning_upcasting=false;
4370 1 : mCRL2log(warning) << "Warning occurred while typechecking " << left << " as left hand side of equation " << eqn << "." << std::endl;
4371 : }
4372 :
4373 1033 : data_expression cond=eqn.condition();
4374 1033 : TraverseVarConsTypeD(DeclaredVars,cond,sort_bool::bool_());
4375 :
4376 1032 : data_expression right=eqn.rhs();
4377 1032 : sort_expression rightType;
4378 : try
4379 : {
4380 1032 : rightType=TraverseVarConsTypeD(DeclaredVars,right,leftType,false);
4381 : }
4382 2 : catch (mcrl2::runtime_error& e)
4383 : {
4384 2 : throw mcrl2::runtime_error(std::string(e.what()) + "\nError occurred while typechecking " + data::pp(right) + " as right hand side of equation " + data::pp(eqn) + ".");
4385 2 : }
4386 :
4387 : //If the types are not uniquely the same now: do once more:
4388 1030 : if (!EqTypesA(leftType,rightType))
4389 : {
4390 0 : sort_expression Type;
4391 0 : if (!TypeMatchA(leftType,rightType,Type))
4392 : {
4393 0 : throw mcrl2::runtime_error("Types of the left- (" + data::pp(leftType) + ") and right- (" + data::pp(rightType) + ") hand-sides of the equation " + data::pp(eqn) + " do not match.");
4394 : }
4395 0 : left=eqn.lhs();
4396 : try
4397 : {
4398 0 : leftType=TraverseVarConsTypeD(DeclaredVars,left,Type,true);
4399 : }
4400 0 : catch (mcrl2::runtime_error& e)
4401 : {
4402 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nTypes of the left- and right-hand-sides of the equation " + data::pp(eqn) + " do not match.");
4403 0 : }
4404 0 : if (was_warning_upcasting)
4405 : {
4406 0 : was_warning_upcasting=false;
4407 0 : mCRL2log(warning) << "Warning occurred while typechecking " << left << " as left hand side of equation " << eqn << "." << std::endl;
4408 : }
4409 0 : right=eqn.rhs();
4410 : try
4411 : {
4412 0 : rightType=TraverseVarConsTypeD(DeclaredVars,right,leftType);
4413 : }
4414 0 : catch (mcrl2::runtime_error& e)
4415 : {
4416 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nTypes of the left- and right-hand-sides of the equation " + data::pp(eqn) + " do not match.");
4417 0 : }
4418 0 : if (!TypeMatchA(leftType,rightType,Type))
4419 : {
4420 0 : throw mcrl2::runtime_error("Types of the left- (" + data::pp(leftType) + ") and right- (" + data::pp(rightType) + ") hand-sides of the equation " + data::pp(eqn) + " do not match.");
4421 : }
4422 0 : if (detail::HasUnknown(Type))
4423 : {
4424 0 : throw mcrl2::runtime_error("Types of the left- (" + data::pp(leftType) + ") and right- (" + data::pp(rightType) + ") hand-sides of the equation " + data::pp(eqn) + " cannot be uniquely determined.");
4425 : }
4426 : // Check that the variable in the condition and the right hand side are a subset of those in the left hand side of the equation.
4427 0 : const std::set<variable> vars_in_lhs=find_free_variables(left);
4428 0 : const std::set<variable> vars_in_rhs=find_free_variables(right);
4429 :
4430 0 : variable culprit;
4431 0 : if (!detail::includes(vars_in_rhs,vars_in_lhs,culprit))
4432 : {
4433 0 : throw mcrl2::runtime_error("The variable " + data::pp(culprit) + " in the right hand side is not included in the left hand side of the equation " + data::pp(eqn) + ".");
4434 : }
4435 :
4436 0 : const std::set<variable> vars_in_condition=find_free_variables(cond);
4437 0 : if (!detail::includes(vars_in_condition,vars_in_lhs,culprit))
4438 : {
4439 0 : throw mcrl2::runtime_error("The variable " + data::pp(culprit) + " in the condition is not included in the left hand side of the equation " + data::pp(eqn) + ".");
4440 : }
4441 0 : }
4442 1030 : resulting_equations.push_back(data_equation(vars,cond,left,right));
4443 1064 : }
4444 4557 : eqns = resulting_equations;
4445 4567 : }
4446 :
4447 : // Type check and replace user defined equations.
4448 4567 : void mcrl2::data::data_type_checker::TransformVarConsTypeData(data_specification& data_spec)
4449 : {
4450 :
4451 : //Create a new specification; admittedly, this is somewhat clumsy.
4452 4567 : data_specification new_specification;
4453 4678 : for(const basic_sort& s: data_spec.user_defined_sorts())
4454 : {
4455 111 : new_specification.add_sort(s);
4456 : }
4457 5405 : for(const alias& a: data_spec.user_defined_aliases())
4458 : {
4459 838 : new_specification.add_alias(a);
4460 : }
4461 4640 : for(const function_symbol& f: data_spec.user_defined_constructors())
4462 : {
4463 73 : new_specification.add_constructor(f);
4464 : }
4465 5573 : for(const function_symbol& f: data_spec.user_defined_mappings())
4466 : {
4467 1006 : new_specification.add_mapping(f);
4468 : }
4469 :
4470 4567 : data_equation_vector eqns=data_spec.user_defined_equations();
4471 4567 : operator ()(eqns); // Type check the equations.
4472 5587 : for(const data_equation& eqn: eqns)
4473 : {
4474 1030 : new_specification.add_equation(eqn);
4475 : }
4476 :
4477 4557 : std::map<std::pair<data_expression, data_expression>, data_equation> lhs_map;
4478 5587 : for (const data_equation& eqn: new_specification.user_defined_equations())
4479 : {
4480 1030 : const auto find_result = lhs_map.find(std::make_pair(eqn.condition(), eqn.lhs()));
4481 1030 : if(find_result != lhs_map.end())
4482 : {
4483 0 : mCRL2log(warning) << "Warning: condition and left-hand side of equations " << find_result->second << " and " << eqn << " completely overlap." << std::endl;
4484 : }
4485 : else
4486 : {
4487 1030 : lhs_map[std::make_pair(eqn.condition(), eqn.lhs())] = eqn;
4488 : }
4489 : }
4490 4557 : data_spec=new_specification;
4491 4577 : }
4492 :
4493 155 : const data_specification mcrl2::data::data_type_checker::operator()() const
4494 : {
4495 155 : return type_checked_data_spec;
4496 : }
4497 :
4498 : // ------------------------------ Here ends the new class based data specification checker -----------------------
4499 :
4500 :
4501 :
4502 :
4503 :
4504 : namespace data
4505 : {
4506 : namespace detail
4507 : {
4508 :
4509 107 : static sort_expression_list GetVarTypes(variable_list VarDecls)
4510 : {
4511 107 : sort_expression_list Result;
4512 218 : for (const variable& VarDecl: VarDecls)
4513 : {
4514 111 : Result.push_front(VarDecl.sort());
4515 : }
4516 214 : return reverse(Result);
4517 107 : }
4518 :
4519 : // Replace occurrences of untyped_possible_sorts([s1,...,sn]) by selecting
4520 : // one of the possible sorts from s1,...,sn. Currently, the first is chosen.
4521 116035 : static sort_expression replace_possible_sorts(const sort_expression& Type)
4522 : {
4523 116035 : if (is_untyped_possible_sorts(data::sort_expression(Type)))
4524 : {
4525 64 : return atermpp::down_cast<untyped_possible_sorts>(Type).sorts().front(); // get the first element of the possible sorts.
4526 : }
4527 115971 : if (data::is_untyped_sort(data::sort_expression(Type)))
4528 : {
4529 44 : return data::untyped_sort();
4530 : }
4531 115927 : if (is_basic_sort(Type))
4532 : {
4533 72104 : return Type;
4534 : }
4535 43823 : if (is_container_sort(Type))
4536 : {
4537 7314 : const container_sort& s=down_cast<container_sort>(Type);
4538 7314 : return container_sort(s.container_name(),replace_possible_sorts(s.element_sort()));
4539 : }
4540 :
4541 36509 : if (is_structured_sort(Type))
4542 : {
4543 485 : return Type; // I assume that there are no possible sorts in sort constructors. JFG.
4544 : }
4545 :
4546 36024 : if (is_function_sort(Type))
4547 : {
4548 36024 : const function_sort& s=down_cast<function_sort>(Type);
4549 36024 : sort_expression_list NewTypeList;
4550 87992 : for (sort_expression_list::const_iterator TypeList=s.domain().begin(); TypeList!=s.domain().end(); ++TypeList)
4551 : {
4552 51968 : NewTypeList.push_front(replace_possible_sorts(*TypeList));
4553 : }
4554 36024 : const sort_expression& ResultType=s.codomain();
4555 36024 : return function_sort(reverse(NewTypeList),replace_possible_sorts(ResultType));
4556 36024 : }
4557 0 : assert(0); // All cases are dealt with above.
4558 : return Type; // Avoid compiler warnings.
4559 : }
4560 :
4561 :
4562 229040 : static bool HasUnknown(const sort_expression& Type)
4563 : {
4564 229040 : if (data::is_untyped_sort(data::sort_expression(Type)))
4565 : {
4566 740 : return true;
4567 : }
4568 228300 : if (is_basic_sort(Type))
4569 : {
4570 141438 : return false;
4571 : }
4572 86862 : if (is_container_sort(Type))
4573 : {
4574 13162 : return HasUnknown(down_cast<container_sort>(Type).element_sort());
4575 : }
4576 73700 : if (is_structured_sort(Type))
4577 : {
4578 974 : return false;
4579 : }
4580 :
4581 72726 : if (is_function_sort(Type))
4582 : {
4583 72024 : const function_sort& s=down_cast<function_sort>(Type);
4584 174402 : for (sort_expression_list::const_iterator TypeList=s.domain().begin(); TypeList!=s.domain().end(); ++TypeList)
4585 103260 : if (HasUnknown(*TypeList))
4586 : {
4587 882 : return true;
4588 : }
4589 71142 : return HasUnknown(s.codomain());
4590 : }
4591 :
4592 702 : return true;
4593 : }
4594 :
4595 16956 : static bool IsNumericType(const sort_expression& Type)
4596 : {
4597 : //returns true if Type is Bool,Pos,Nat,Int or Real
4598 : //otherwise return fase
4599 16956 : if (data::is_untyped_sort(Type))
4600 : {
4601 6864 : return false;
4602 : }
4603 10092 : return (bool)(sort_bool::is_bool(Type)||
4604 10092 : sort_pos::is_pos(Type)||
4605 8656 : sort_nat::is_nat(Type)||
4606 21702 : sort_int::is_int(Type)||
4607 11610 : sort_real::is_real(Type));
4608 : }
4609 :
4610 :
4611 609 : static sort_expression MinType(const sort_expression_list& TypeList)
4612 : {
4613 609 : return TypeList.front();
4614 : }
4615 :
4616 : } //namespace detail
4617 : } //namespace data
4618 : }
|
