Line data Source code
1 : // Author(s): Wieger Wesselink
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/data/experimental/type_check_tree.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_DATA_EXPERIMENTAL_TYPE_CHECK_TREE_H
13 : #define MCRL2_DATA_EXPERIMENTAL_TYPE_CHECK_TREE_H
14 :
15 : #include "mcrl2/data/parse.h"
16 : #include "mcrl2/data/replace.h"
17 : #include "mcrl2/data/experimental/type_checker.h"
18 :
19 : namespace mcrl2 {
20 :
21 : namespace data {
22 :
23 : typedef std::map<untyped_sort_variable, sort_expression> sort_substitution;
24 : typedef std::pair<sort_substitution, int> solution; // the second element is the cost of the solution
25 :
26 : template <typename T>
27 361 : bool has_untyped_sort(const T& x)
28 : {
29 361 : return data::search_sort_expression(x, untyped_sort());
30 : }
31 :
32 : template <typename T>
33 160 : T replace_untyped_sort(const T& x, const sort_expression& replacement)
34 : {
35 1042 : return data::replace_sort_expressions(x, [&replacement](const sort_expression& x) { return is_untyped_sort(x) ? replacement : x; }, true);
36 : }
37 :
38 : inline
39 1328 : const untyped_sort_variable& make_untyped_sort_variable(const sort_expression& x)
40 : {
41 1328 : return atermpp::down_cast<untyped_sort_variable>(x);
42 : }
43 :
44 0 : inline sort_expression substitute(const sort_expression& x, const sort_substitution& sigma)
45 : {
46 0 : if (is_untyped_sort_variable(x))
47 : {
48 0 : const untyped_sort_variable& v = make_untyped_sort_variable(x);
49 0 : auto i = sigma.find(v);
50 0 : if (i != sigma.end())
51 : {
52 0 : return i->second;
53 : }
54 : }
55 0 : return x;
56 : }
57 :
58 : template <typename Container>
59 482 : std::string print_node_vector(const std::string& name, const Container& nodes, const std::string& sep = ", ", const std::string& first = "", const std::string& last = "")
60 : {
61 482 : std::vector<std::string> s;
62 2062 : for (auto i = nodes.begin(); i != nodes.end(); ++i)
63 : {
64 1580 : s.push_back((*i)->print());
65 : }
66 482 : std::ostringstream out;
67 482 : out << name << "(" << first;
68 482 : out << utilities::string_join(s, sep);
69 482 : out << last << ")";
70 964 : return out.str();
71 482 : }
72 :
73 : template <typename Container>
74 : std::string print_vector(const std::string& name, const Container& nodes)
75 : {
76 : std::ostringstream out;
77 : out << name << "(";
78 : for (auto i = nodes.begin(); i != nodes.end(); ++i)
79 : {
80 : if (i != nodes.begin())
81 : {
82 : out << ", ";
83 : }
84 : out << *i;
85 : }
86 : out << ")";
87 : return out.str();
88 : }
89 :
90 : struct type_check_node;
91 :
92 : typedef std::shared_ptr<type_check_node> type_check_node_ptr;
93 :
94 : struct type_check_context
95 : {
96 : std::map<core::identifier_string, sort_expression_list> system_constants;
97 : std::map<core::identifier_string, function_sort_list> system_functions;
98 : std::map<core::identifier_string, sort_expression> user_constants;
99 : std::map<core::identifier_string, function_sort_list> user_functions;
100 : std::map<core::identifier_string, std::vector<sort_expression> > declared_variables;
101 : mutable std::size_t sort_variable_index;
102 :
103 71 : type_check_context(const data::data_specification& dataspec = data::data_specification())
104 71 : : sort_variable_index(0)
105 : {
106 71 : type_checker checker(dataspec);
107 71 : system_constants = checker.system_constants();
108 71 : system_functions = checker.system_functions();
109 71 : user_constants = checker.user_constants();
110 71 : user_functions = checker.user_functions();
111 71 : }
112 :
113 : // Returns the system defined constants and the user defined constants matching with name
114 : std::pair<sort_expression_list, sort_expression_list> find_matching_constants(const std::string& name) const;
115 :
116 : // Returns the system defined functions and the user defined functions matching with (name, arity)
117 : // N.B. Untyped sorts are replaced with fresh sort variables.
118 : std::pair<function_sort_list, function_sort_list> find_matching_functions(const std::string& name, std::size_t arity) const;
119 :
120 : // Returns the system defined functions and the user defined functions matching with name
121 : // N.B. Untyped sorts are replaced with fresh sort variables.
122 : std::pair<function_sort_list, function_sort_list> find_matching_functions(const std::string& name) const;
123 :
124 : // Returns the variables matching with name
125 : std::vector<sort_expression> find_matching_variables(const std::string& name) const;
126 :
127 512 : untyped_sort_variable create_sort_variable() const
128 : {
129 512 : return untyped_sort_variable(sort_variable_index++);
130 : }
131 :
132 75 : void add_context_variable(const variable& v)
133 : {
134 75 : declared_variables[v.name()].push_back(v.sort());
135 75 : }
136 :
137 96 : void add_context_variables(const variable_list& variables)
138 : {
139 169 : for (const variable& v: variables)
140 : {
141 73 : add_context_variable(v);
142 : }
143 96 : }
144 :
145 75 : void remove_context_variable(const variable& v)
146 : {
147 75 : auto i = declared_variables.find(v.name());
148 75 : if (i->second.size() <= 1)
149 : {
150 59 : declared_variables.erase(i);
151 : }
152 : else
153 : {
154 16 : i->second.pop_back();
155 : }
156 75 : }
157 :
158 96 : void remove_context_variables(const variable_list& variables)
159 : {
160 169 : for (const variable& v: variables) // N.B. the order of insertion and removal should not matter
161 : {
162 73 : remove_context_variable(v);
163 : }
164 96 : }
165 :
166 : protected:
167 : // replace occurrences of untyped sort in sorts by fresh sort variables
168 148 : function_sort_list replace_untyped_sorts(const function_sort_list& sorts) const
169 : {
170 148 : std::vector<function_sort> result;
171 507 : for (const function_sort& f: sorts)
172 : {
173 359 : if (has_untyped_sort(f))
174 : {
175 159 : function_sort f1 = replace_untyped_sort(f, create_sort_variable());
176 159 : result.push_back(f1);
177 159 : }
178 : else
179 : {
180 200 : result.push_back(f);
181 : }
182 : }
183 296 : return function_sort_list(result.begin(), result.end());
184 148 : }
185 : };
186 :
187 : struct type_check_constraint;
188 : typedef std::shared_ptr<type_check_constraint> constraint_ptr;
189 : constraint_ptr substitute_constraint(constraint_ptr p, const sort_substitution& sigma);
190 :
191 : struct type_check_constraint
192 : {
193 : int cost;
194 :
195 2184 : type_check_constraint(int cost_ = 0)
196 2184 : : cost(cost_)
197 2184 : {}
198 :
199 : virtual std::string print() const = 0;
200 : };
201 :
202 : constraint_ptr make_and_constraint(const std::vector<constraint_ptr>& alternatives);
203 : constraint_ptr make_or_constraint(const std::vector<constraint_ptr>& alternatives);
204 : constraint_ptr make_is_equal_to_constraint(const sort_expression& s1, const sort_expression& s2, int cost = 0);
205 :
206 : struct true_constraint final: public type_check_constraint
207 : {
208 353 : true_constraint(int cost = 0)
209 353 : : type_check_constraint(cost)
210 353 : {}
211 :
212 34 : std::string print() const override
213 : {
214 34 : return "true";
215 : }
216 : };
217 :
218 : struct false_constraint final: public type_check_constraint
219 : {
220 : std::string message;
221 :
222 2 : false_constraint(const std::string& message_)
223 2 : : message(message_)
224 2 : {}
225 :
226 2 : std::string print() const override
227 : {
228 4 : return "false(" + message + ")";
229 : }
230 : };
231 :
232 : inline
233 2 : constraint_ptr make_false_constraint(const std::string& message)
234 : {
235 2 : return constraint_ptr(new false_constraint(message));
236 : }
237 :
238 : inline
239 353 : constraint_ptr make_true_constraint(int cost = 0)
240 : {
241 353 : return constraint_ptr(new true_constraint(cost));
242 : }
243 :
244 : // The sort of the corresponding data expression should be equal to 'sort'.
245 : struct is_element_of_constraint final: public type_check_constraint
246 : {
247 : untyped_sort_variable s;
248 : std::vector<sort_expression> sorts;
249 :
250 1328 : is_element_of_constraint(const untyped_sort_variable& s_, const std::vector<sort_expression>& sorts_, int cost = 0)
251 1328 : : type_check_constraint(cost), s(s_), sorts(sorts_)
252 1328 : {}
253 :
254 1236 : std::string print() const override
255 : {
256 1236 : if (sorts.size() == 1)
257 : {
258 1492 : return data::pp(s) + " = " + data::pp(*sorts.begin());
259 : }
260 980 : return data::pp(s) + " in " + core::detail::print_set(sorts);
261 : }
262 : };
263 :
264 : inline
265 0 : constraint_ptr make_function_sort_constraint(const function_sort& f1, const sort_expression& s2)
266 : {
267 0 : auto const& domain1 = f1.domain();
268 0 : if (!is_function_sort(s2))
269 : {
270 0 : throw mcrl2::runtime_error("could not make function sort constraint");
271 : }
272 0 : const function_sort& f2 = atermpp::down_cast<function_sort>(s2);
273 0 : auto const& domain2 = f2.domain();
274 0 : if (domain1.size() != domain1.size())
275 : {
276 0 : return make_false_constraint("function sorts do not match");
277 : }
278 0 : std::vector<constraint_ptr> alternatives;
279 0 : alternatives.push_back(make_is_equal_to_constraint(f1.codomain(), f2.codomain()));
280 0 : auto i1 = domain1.begin();
281 0 : auto i2 = domain2.begin();
282 0 : for (; i1 != domain1.end(); ++i1, ++i2)
283 : {
284 0 : alternatives.push_back(make_is_equal_to_constraint(*i1, *i2));
285 : }
286 0 : return make_and_constraint(alternatives);
287 0 : }
288 :
289 : inline
290 1328 : constraint_ptr make_is_element_of_constraint(const sort_expression& s, const std::vector<sort_expression>& sorts, int cost = 0)
291 : {
292 : // optimizations
293 1328 : if (is_untyped_sort(s))
294 : {
295 0 : return make_true_constraint();
296 : }
297 1328 : if (std::find(sorts.begin(), sorts.end(), untyped_sort()) != sorts.end())
298 : {
299 0 : return make_true_constraint();
300 : }
301 1328 : if (is_function_sort(s))
302 : {
303 0 : const function_sort& f1 = atermpp::down_cast<function_sort>(s);
304 0 : std::vector<constraint_ptr> alternatives;
305 0 : for (const sort_expression& s2: sorts)
306 : {
307 0 : alternatives.push_back(make_function_sort_constraint(f1, s2));
308 : }
309 0 : return make_and_constraint(alternatives);
310 0 : }
311 1328 : if (std::find(sorts.begin(), sorts.end(), s) != sorts.end())
312 : {
313 0 : return make_true_constraint();
314 : }
315 1328 : return constraint_ptr(new is_element_of_constraint(make_untyped_sort_variable(s), sorts, cost));
316 : }
317 :
318 : // The sort of the corresponding data expression should be equal to 'sort'.
319 : struct is_equal_to_constraint final: public type_check_constraint
320 : {
321 : untyped_sort_variable s1;
322 : sort_expression s2;
323 :
324 : is_equal_to_constraint(const untyped_sort_variable& s1_, const sort_expression& s2_, int cost = 0)
325 : : type_check_constraint(cost), s1(s1_), s2(s2_)
326 : {}
327 :
328 : std::string print() const override
329 : {
330 : return "is_equal_to(" + data::pp(s1) + ", " + data::pp(s2) + ")";
331 : }
332 : };
333 :
334 : inline
335 771 : constraint_ptr make_is_equal_to_constraint(const sort_expression& s1,
336 : const sort_expression& s2, int /* cost */)
337 : {
338 771 : if (s1 == s2)
339 : {
340 25 : return make_true_constraint();
341 : }
342 746 : if (is_untyped_sort(s1) || is_untyped_sort(s2))
343 : {
344 0 : return make_true_constraint();
345 : }
346 746 : if (is_untyped_sort_variable(s1))
347 : {
348 1142 : return make_is_element_of_constraint(s1, { s2 });
349 : }
350 175 : if (is_untyped_sort_variable(s2))
351 : {
352 350 : return make_is_element_of_constraint(s2, { s1 });
353 : // return constraint_ptr(new is_equal_to_constraint(make_untyped_sort_variable(s2), s1, cost));
354 : }
355 0 : throw mcrl2::runtime_error("cannot make is_equal_to constraint");
356 : }
357 :
358 : // The sort variable s1 should be a subsort of s2.
359 : struct subsort_constraint final: public type_check_constraint
360 : {
361 : sort_expression s1;
362 : sort_expression s2;
363 :
364 75 : subsort_constraint(const sort_expression& s1_, const sort_expression& s2_, int cost = 0)
365 75 : : type_check_constraint(cost), s1(s1_), s2(s2_)
366 75 : {}
367 :
368 75 : std::string print() const override
369 : {
370 150 : return "subsort(" + data::pp(s1) + ", " + data::pp(s2) + ")";
371 : }
372 : };
373 :
374 : inline
375 1174 : constraint_ptr make_subsort_constraint(const sort_expression& s1, const sort_expression& s2, int cost = 0)
376 : {
377 : // optimizations
378 1174 : if (sort_bool::is_bool(s1) || sort_bool::is_bool(s2))
379 : {
380 48 : return make_is_equal_to_constraint(s1, s2, cost);
381 : }
382 1126 : if (is_untyped_sort(s1) || is_untyped_sort(s2))
383 : {
384 0 : return make_true_constraint(cost);
385 : }
386 1126 : if (is_container_sort(s1) && is_container_sort(s2))
387 : {
388 0 : const container_sort& c1 = atermpp::down_cast<container_sort>(s1);
389 0 : const container_sort& c2 = atermpp::down_cast<container_sort>(s2);
390 0 : if (c1.container_name() == c2.container_name())
391 : {
392 0 : return make_subsort_constraint(c1.element_sort(), c2.element_sort());
393 : }
394 : else
395 : {
396 0 : return make_false_constraint("incompatible container sorts");
397 : }
398 : }
399 1126 : if (is_container_sort(s1) && is_untyped_sort_variable(s2))
400 : {
401 134 : return make_is_equal_to_constraint(s1, s2);
402 : }
403 992 : if (is_untyped_sort_variable(s1) && is_container_sort(s2))
404 : {
405 271 : return make_is_equal_to_constraint(s1, s2);
406 : }
407 721 : if (is_function_sort(s1) && is_function_sort(s2))
408 : {
409 0 : const function_sort& f1 = atermpp::down_cast<function_sort>(s1);
410 0 : const function_sort& f2 = atermpp::down_cast<function_sort>(s2);
411 0 : auto const& domain1 = f1.domain();
412 0 : auto const& domain2 = f2.domain();
413 :
414 0 : if (domain1.size() != domain1.size())
415 : {
416 0 : return make_false_constraint("function sorts do not match");
417 : }
418 :
419 0 : std::vector<constraint_ptr> alternatives;
420 0 : alternatives.push_back(make_subsort_constraint(f1.codomain(), f2.codomain()));
421 0 : auto i1 = domain1.begin();
422 0 : auto i2 = domain2.begin();
423 0 : for (; i1 != domain1.end(); ++i1, ++i2)
424 : {
425 0 : alternatives.push_back(make_subsort_constraint(*i2, *i1));
426 : }
427 0 : return make_and_constraint(alternatives);
428 0 : }
429 721 : if (sort_pos::is_pos(s1))
430 : {
431 705 : return make_is_element_of_constraint(s2, { sort_pos::pos(), sort_nat::nat(), sort_int::int_(), sort_real::real_() });
432 : }
433 580 : if (sort_nat::is_nat(s1))
434 : {
435 228 : return make_is_element_of_constraint(s2, { sort_nat::nat(), sort_int::int_(), sort_real::real_() });
436 : }
437 523 : if (sort_int::is_int(s1))
438 : {
439 126 : return make_is_element_of_constraint(s2, { sort_int::int_(), sort_real::real_() });
440 : }
441 481 : if (sort_real::is_real(s1))
442 : {
443 34 : return make_is_equal_to_constraint(s2, sort_real::real_());
444 : }
445 447 : if (sort_pos::is_pos(s2))
446 : {
447 122 : return make_is_equal_to_constraint(s1, sort_pos::pos());
448 : }
449 325 : if (sort_nat::is_nat(s2))
450 : {
451 363 : return make_is_element_of_constraint(s1, { sort_pos::pos(), sort_nat::nat() });
452 : }
453 204 : if (sort_int::is_int(s2))
454 : {
455 260 : return make_is_element_of_constraint(s1, { sort_pos::pos(), sort_nat::nat(), sort_int::int_() });
456 : }
457 139 : if (sort_real::is_real(s2))
458 : {
459 320 : return make_is_element_of_constraint(s1, { sort_pos::pos(), sort_nat::nat(), sort_int::int_(), sort_real::real_() });
460 : }
461 :
462 75 : return constraint_ptr(new subsort_constraint(s1, s2, cost));
463 : }
464 :
465 : // joins disjunctions of is_element_of constraints
466 : inline
467 162 : std::vector<constraint_ptr> join_or_is_element_of_constraints(const std::vector<constraint_ptr>& constraints)
468 : {
469 162 : std::vector<constraint_ptr> result;
470 162 : std::map<untyped_sort_variable, std::set<sort_expression> > is_element_of_constraints;
471 :
472 616 : for (const constraint_ptr& p: constraints)
473 : {
474 454 : is_element_of_constraint* x_is_element_of = dynamic_cast<is_element_of_constraint*>(p.get());
475 454 : if (x_is_element_of)
476 : {
477 92 : is_element_of_constraints[x_is_element_of->s].insert(x_is_element_of->sorts.begin(), x_is_element_of->sorts.end());
478 : }
479 : else
480 : {
481 362 : result.push_back(p);
482 : }
483 : }
484 254 : for (const auto& i: is_element_of_constraints)
485 : {
486 92 : result.push_back(make_is_element_of_constraint(i.first, std::vector<sort_expression>(i.second.begin(), i.second.end())));
487 : }
488 324 : return result;
489 162 : }
490 :
491 : struct or_constraint final: public type_check_constraint
492 : {
493 : std::vector<constraint_ptr> alternatives;
494 :
495 44 : or_constraint(const std::vector<constraint_ptr>& alternatives_)
496 44 : : alternatives(alternatives_)
497 44 : {}
498 :
499 44 : std::string print() const
500 : {
501 44 : return print_node_vector("or", alternatives, "\n ", "\n ", "\n ");
502 : }
503 : };
504 :
505 : inline
506 162 : constraint_ptr make_or_constraint(const std::vector<constraint_ptr>& alternatives)
507 : {
508 162 : std::vector<constraint_ptr> v;
509 616 : for (const constraint_ptr& p: alternatives)
510 : {
511 454 : true_constraint* x_no = dynamic_cast<true_constraint*>(p.get());
512 454 : if (x_no)
513 : {
514 0 : continue;
515 : }
516 454 : false_constraint* x_false = dynamic_cast<false_constraint*>(p.get());
517 454 : if (x_false)
518 : {
519 0 : continue;
520 : }
521 454 : or_constraint* x_or = dynamic_cast<or_constraint*>(p.get());
522 454 : if (x_or)
523 : {
524 0 : v.insert(v.end(), x_or->alternatives.begin(), x_or->alternatives.end());
525 0 : continue;
526 : }
527 454 : v.push_back(p);
528 : }
529 162 : v = join_or_is_element_of_constraints(v);
530 162 : if (v.size() == 0)
531 : {
532 0 : return constraint_ptr(new true_constraint());
533 : }
534 162 : if (v.size() == 1)
535 : {
536 118 : return v.front();
537 : }
538 44 : return constraint_ptr(new or_constraint(v));
539 162 : }
540 :
541 : struct and_constraint final: public type_check_constraint
542 : {
543 : std::vector<constraint_ptr> alternatives;
544 :
545 382 : and_constraint(const std::vector<constraint_ptr>& alternatives_)
546 382 : : alternatives(alternatives_)
547 382 : {}
548 :
549 382 : std::string print() const override
550 : {
551 382 : return print_node_vector("and", alternatives);
552 : }
553 : };
554 :
555 : inline
556 397 : constraint_ptr make_and_constraint(const std::vector<constraint_ptr>& alternatives)
557 : {
558 397 : std::vector<constraint_ptr> v;
559 1553 : for (constraint_ptr p: alternatives)
560 : {
561 1156 : false_constraint* x_false = dynamic_cast<false_constraint*>(p.get());
562 1156 : if (x_false)
563 : {
564 0 : return p;
565 : }
566 1156 : true_constraint* x_no = dynamic_cast<true_constraint*>(p.get());
567 1156 : if (x_no)
568 : {
569 25 : continue;
570 : }
571 1131 : and_constraint* x_and = dynamic_cast<and_constraint*>(p.get());
572 1131 : if (x_and)
573 : {
574 0 : v.insert(v.end(), x_and->alternatives.begin(), x_and->alternatives.end());
575 0 : continue;
576 : }
577 1131 : v.push_back(p);
578 1156 : }
579 397 : if (v.size() == 0)
580 : {
581 0 : return make_true_constraint();
582 : }
583 397 : if (v.size() == 1)
584 : {
585 15 : return v.front();
586 : }
587 382 : return constraint_ptr(new and_constraint(v));
588 397 : }
589 :
590 : struct type_check_node
591 : {
592 : type_check_context& context;
593 : std::vector<type_check_node_ptr> children;
594 : constraint_ptr constraint;
595 : untyped_sort_variable sort;
596 :
597 321 : type_check_node(type_check_context& context_, const std::vector<type_check_node_ptr>& children_)
598 321 : : context(context_), children(children_), constraint(make_true_constraint())
599 : {
600 321 : sort = context.create_sort_variable();
601 321 : }
602 :
603 321 : virtual ~type_check_node() {};
604 :
605 : // Adds a value to the 'sort' attribute
606 : // Sets the constraints that apply to this node to 'constraint'
607 4 : virtual void set_constraint(type_check_context& /* context */)
608 4 : {}
609 :
610 0 : virtual void apply_substitution(const sort_substitution& sigma)
611 : {
612 0 : for (const type_check_node_ptr& child: children)
613 : {
614 0 : child->apply_substitution(sigma);
615 : }
616 0 : constraint = substitute_constraint(constraint, sigma);
617 0 : }
618 :
619 131 : void set_children_constraints(type_check_context& context)
620 : {
621 358 : for (const type_check_node_ptr& child: children)
622 : {
623 227 : child->set_constraint(context);
624 : }
625 131 : }
626 :
627 : // Throws an exception if the node violates a well typedness rule
628 0 : virtual void check_well_typedness(const type_check_context& /* context */)
629 0 : {}
630 :
631 : virtual std::string print() const = 0;
632 : };
633 :
634 : struct id_node final: public type_check_node
635 : {
636 : std::string value;
637 :
638 84 : id_node(type_check_context& context, const std::string& value_)
639 84 : : type_check_node(context, {}), value(value_)
640 84 : {}
641 :
642 80 : void set_constraint(type_check_context& context) override
643 : {
644 80 : std::vector<constraint_ptr> alternatives;
645 :
646 : // it is a variable
647 80 : std::vector<sort_expression> variable_sorts = context.find_matching_variables(value);
648 80 : if (variable_sorts.size() == 1)
649 : {
650 77 : alternatives.push_back(make_is_equal_to_constraint(sort, variable_sorts.front()));
651 : }
652 :
653 : // it is a constant
654 80 : std::pair<sort_expression_list, sort_expression_list> p = context.find_matching_constants(value);
655 80 : for (const sort_expression& s: p.first + p.second)
656 : {
657 0 : alternatives.push_back(make_is_equal_to_constraint(sort, s));
658 80 : }
659 :
660 : // it is a function
661 80 : std::pair<function_sort_list, function_sort_list> q = context.find_matching_functions(value);
662 81 : for (const function_sort& s: q.first + q.second)
663 : {
664 1 : alternatives.push_back(make_is_equal_to_constraint(sort, s));
665 80 : }
666 :
667 80 : if (alternatives.empty())
668 : {
669 2 : constraint = make_false_constraint("The id " + value + " is not declared!");
670 : }
671 : else
672 : {
673 78 : constraint = make_or_constraint(alternatives);
674 : }
675 80 : }
676 :
677 250 : std::string print() const override
678 : {
679 500 : return "id(" + value + ")";
680 : }
681 : };
682 :
683 : struct number_node final: public type_check_node
684 : {
685 : std::string value;
686 :
687 74 : number_node(type_check_context& context, const std::string& value_)
688 74 : : type_check_node(context, {}), value(value_)
689 74 : {}
690 :
691 70 : void set_constraint(type_check_context& /* context */) override
692 : {
693 70 : if (detail::is_pos(value))
694 : {
695 55 : constraint = make_subsort_constraint(sort_pos::pos(), sort);
696 : }
697 15 : else if (detail::is_nat(value))
698 : {
699 15 : constraint = make_subsort_constraint(sort_nat::nat(), sort);
700 : }
701 : else
702 : {
703 0 : throw mcrl2::runtime_error("unknown numeric string " + value);
704 : }
705 70 : }
706 :
707 184 : std::string print() const override
708 : {
709 368 : return "number(" + value + ")";
710 : }
711 : };
712 :
713 : struct constant_node: public type_check_node
714 : {
715 : std::string name;
716 :
717 35 : constant_node(type_check_context& context, const std::string& name_)
718 35 : : type_check_node(context, {}), name(name_)
719 35 : {}
720 :
721 35 : virtual ~constant_node() {}
722 :
723 14 : void set_constraint(type_check_context& context) override
724 : {
725 14 : std::pair<sort_expression_list, sort_expression_list> p = context.find_matching_constants(name);
726 14 : std::vector<constraint_ptr> alternatives;
727 28 : for (const sort_expression& s: p.first + p.second)
728 : {
729 14 : alternatives.push_back(make_subsort_constraint(s, sort));
730 14 : }
731 14 : constraint = make_or_constraint(alternatives);
732 14 : set_children_constraints(context);
733 14 : }
734 :
735 70 : std::string print() const override
736 : {
737 140 : return "constant(" + name + ")";
738 : }
739 : };
740 :
741 : struct true_node final: public constant_node
742 : {
743 12 : true_node(type_check_context& context)
744 12 : : constant_node(context, "true")
745 12 : { }
746 : };
747 :
748 : struct false_node final: public constant_node
749 : {
750 10 : false_node(type_check_context& context)
751 10 : : constant_node(context, "false")
752 10 : { }
753 : };
754 :
755 : struct empty_list_node final: public constant_node
756 : {
757 5 : empty_list_node(type_check_context& context)
758 5 : : constant_node(context, "[]")
759 5 : { }
760 :
761 5 : void set_constraint(type_check_context& context) override
762 : {
763 5 : auto element_sort = context.create_sort_variable();
764 5 : constraint = make_is_equal_to_constraint(sort, sort_list::list(element_sort));
765 5 : }
766 : };
767 :
768 : struct empty_set_node final: public constant_node
769 : {
770 6 : empty_set_node(type_check_context& context)
771 6 : : constant_node(context, "{}")
772 6 : { }
773 :
774 6 : void set_constraint(type_check_context& context) override
775 : {
776 6 : auto element_sort = context.create_sort_variable();
777 6 : constraint = make_is_equal_to_constraint(sort, sort_set::set_(element_sort));
778 6 : }
779 : };
780 :
781 : struct empty_bag_node final: public constant_node
782 : {
783 2 : empty_bag_node(type_check_context& context)
784 2 : : constant_node(context, "{:}")
785 2 : { }
786 :
787 2 : void set_constraint(type_check_context& context) override
788 : {
789 2 : auto element_sort = context.create_sort_variable();
790 2 : constraint = make_is_equal_to_constraint(sort, sort_bag::bag(element_sort));
791 2 : }
792 : };
793 :
794 : struct list_enumeration_node final: public type_check_node
795 : {
796 15 : list_enumeration_node(type_check_context& context, const std::vector<type_check_node_ptr>& children)
797 15 : : type_check_node(context, children)
798 15 : {}
799 :
800 15 : void set_constraint(type_check_context& context) override
801 : {
802 15 : auto element_sort = context.create_sort_variable();
803 15 : set_children_constraints(context);
804 :
805 15 : std::vector<constraint_ptr> alternatives;
806 15 : alternatives.push_back(make_is_equal_to_constraint(sort, sort_list::list(element_sort)));
807 41 : for (const type_check_node_ptr& child: children)
808 : {
809 26 : alternatives.push_back(make_subsort_constraint(element_sort, child->sort));
810 : }
811 15 : constraint = make_and_constraint(alternatives);
812 15 : }
813 :
814 25 : std::string print() const override
815 : {
816 25 : return print_node_vector("list_enumeration", children);
817 : }
818 : };
819 :
820 : struct bag_enumeration_node final: public type_check_node
821 : {
822 2 : bag_enumeration_node(type_check_context& context, const std::vector<type_check_node_ptr>& children)
823 2 : : type_check_node(context, children)
824 2 : {}
825 :
826 2 : void set_constraint(type_check_context& context) override
827 : {
828 2 : auto element_sort = context.create_sort_variable();
829 2 : set_children_constraints(context);
830 :
831 2 : std::vector<constraint_ptr> alternatives;
832 2 : alternatives.push_back(make_is_equal_to_constraint(sort, sort_bag::bag(element_sort)));
833 12 : for (std::size_t i = 0; i < children.size(); i++)
834 : {
835 10 : if (i % 2 == 0)
836 : {
837 5 : alternatives.push_back(make_subsort_constraint(element_sort, children[i]->sort));
838 : }
839 : else
840 : {
841 5 : alternatives.push_back(make_subsort_constraint(sort_nat::nat(), children[i]->sort));
842 : }
843 : }
844 2 : constraint = make_and_constraint(alternatives);
845 2 : }
846 :
847 2 : std::string print() const override
848 : {
849 2 : return print_node_vector("bag_enumeration", children);
850 : }
851 : };
852 :
853 : struct set_enumeration_node final: public type_check_node
854 : {
855 2 : set_enumeration_node(type_check_context& context, const std::vector<type_check_node_ptr>& children)
856 2 : : type_check_node(context, children)
857 2 : {}
858 :
859 2 : void set_constraint(type_check_context& context) override
860 : {
861 2 : auto element_sort = context.create_sort_variable();
862 2 : set_children_constraints(context);
863 :
864 2 : std::vector<constraint_ptr> alternatives;
865 2 : alternatives.push_back(make_is_equal_to_constraint(sort, sort_set::set_(element_sort)));
866 7 : for (const type_check_node_ptr& child: children)
867 : {
868 5 : alternatives.push_back(make_subsort_constraint(element_sort, child->sort));
869 : }
870 2 : constraint = make_and_constraint(alternatives);
871 2 : }
872 :
873 2 : std::string print() const override
874 : {
875 2 : return print_node_vector("set_enumeration", children);
876 : }
877 : };
878 :
879 : struct bag_or_set_enumeration_node final: public type_check_node
880 : {
881 : variable v;
882 :
883 2 : bag_or_set_enumeration_node(type_check_context& context, const variable& v_, type_check_node_ptr x)
884 2 : : type_check_node(context, {}), v(v_)
885 : {
886 2 : children.push_back(x);
887 2 : }
888 :
889 2 : void set_constraint(type_check_context& context) override
890 : {
891 2 : context.add_context_variable(v);
892 2 : set_children_constraints(context);
893 :
894 2 : auto element_sort = v.sort();
895 4 : constraint_ptr set_constraint = make_and_constraint({
896 2 : make_is_equal_to_constraint(sort, sort_set::set_(element_sort)),
897 4 : make_is_equal_to_constraint(children.front()->sort, sort_bool::bool_())
898 10 : });
899 4 : constraint_ptr bag_constraint = make_and_constraint({
900 2 : make_is_equal_to_constraint(sort, sort_bag::bag(element_sort)),
901 2 : make_subsort_constraint(sort_nat::nat(), children.front()->sort)
902 8 : });
903 6 : constraint = make_or_constraint({ set_constraint, bag_constraint });
904 2 : context.remove_context_variable(v);
905 2 : }
906 :
907 2 : std::string print() const override
908 : {
909 2 : return print_node_vector("bag_or_set_enumeration", children);
910 : }
911 : };
912 :
913 : struct function_update_node final: public type_check_node
914 : {
915 5 : function_update_node(type_check_context& context, type_check_node_ptr x1, type_check_node_ptr x2, type_check_node_ptr x3)
916 5 : : type_check_node(context, {})
917 : {
918 5 : children.push_back(x1);
919 5 : children.push_back(x2);
920 5 : children.push_back(x3);
921 5 : }
922 :
923 6 : std::string print() const override
924 : {
925 6 : return print_node_vector("function_update", children);
926 : }
927 : };
928 :
929 : struct application_node final: public type_check_node
930 : {
931 : std::size_t arity;
932 :
933 3 : application_node(type_check_context& context, type_check_node_ptr head, const std::vector<type_check_node_ptr>& arguments)
934 3 : : type_check_node(context, {}), arity(arguments.size())
935 : {
936 3 : children.push_back(head);
937 8 : for (const auto& arg: arguments)
938 : {
939 5 : children.push_back(arg);
940 : }
941 3 : }
942 :
943 3 : void set_constraint(type_check_context& context) override
944 : {
945 3 : set_children_constraints(context);
946 :
947 3 : const sort_expression& codomain = sort;
948 3 : std::vector<constraint_ptr> alternatives;
949 3 : std::vector<sort_expression> domain;
950 8 : for (std::size_t i = 0; i < arity; i++)
951 : {
952 5 : domain.push_back(children[i+1]->sort);
953 : }
954 3 : alternatives.push_back(make_is_equal_to_constraint(children[0]->sort, function_sort(sort_expression_list(domain.begin(), domain.end()), codomain)));
955 :
956 : // add missing constraints for if application
957 : // TODO: handle this in a more structured way
958 3 : if (children[0]->print() == "id(if)")
959 : {
960 1 : alternatives.push_back(make_subsort_constraint(codomain, children[1]->sort));
961 1 : alternatives.push_back(make_subsort_constraint(codomain, children[2]->sort));
962 : }
963 :
964 3 : constraint = make_and_constraint(alternatives);
965 3 : }
966 :
967 6 : std::string print() const override
968 : {
969 6 : return print_node_vector("application", children);
970 : }
971 : };
972 :
973 : struct unary_operator_node: public type_check_node
974 : {
975 : std::string name;
976 :
977 21 : unary_operator_node(type_check_context& context, const std::string& name_, type_check_node_ptr arg)
978 42 : : type_check_node(context, { arg }), name(name_)
979 21 : {}
980 :
981 31 : virtual ~unary_operator_node() {}
982 :
983 10 : void set_constraint(type_check_context& context) override
984 : {
985 10 : set_children_constraints(context);
986 :
987 10 : std::pair<function_sort_list, function_sort_list> p = context.find_matching_functions(name, 1);
988 10 : std::vector<constraint_ptr> alternatives;
989 39 : for (const function_sort& s: p.first + p.second)
990 : {
991 87 : alternatives.push_back(make_and_constraint({
992 29 : make_subsort_constraint(children[0]->sort, s.domain().front()),
993 : make_subsort_constraint(s.codomain(), sort)
994 : })
995 : );
996 10 : }
997 10 : constraint = make_or_constraint(alternatives);
998 10 : }
999 :
1000 16 : std::string print() const override
1001 : {
1002 16 : std::ostringstream out;
1003 16 : out << "unary_operator(" << name << ", " << children.front()->print() << ")";
1004 32 : return out.str();
1005 16 : }
1006 : };
1007 :
1008 : struct forall_node final: public type_check_node
1009 : {
1010 : variable_list variables;
1011 :
1012 3 : forall_node(type_check_context& context, const variable_list& variables_, type_check_node_ptr arg)
1013 6 : : type_check_node(context, { arg }), variables(variables_)
1014 3 : {}
1015 :
1016 3 : void set_constraint(type_check_context& context) override
1017 : {
1018 3 : context.add_context_variables(variables);
1019 3 : set_children_constraints(context);
1020 :
1021 3 : constraint = make_is_equal_to_constraint(sort, sort_bool::bool_());
1022 3 : context.remove_context_variables(variables);
1023 3 : }
1024 :
1025 3 : std::string print() const override
1026 : {
1027 3 : std::ostringstream out;
1028 3 : out << "forall(" << data::pp(variables) << ". " << children.front()->print() << ")";
1029 6 : return out.str();
1030 3 : }
1031 : };
1032 :
1033 : struct exists_node final: public type_check_node
1034 : {
1035 : variable_list variables;
1036 :
1037 2 : exists_node(type_check_context& context, const variable_list& variables_, type_check_node_ptr arg)
1038 4 : : type_check_node(context, { arg }), variables(variables_)
1039 2 : {}
1040 :
1041 2 : void set_constraint(type_check_context& context) override
1042 : {
1043 2 : context.add_context_variables(variables);
1044 2 : set_children_constraints(context);
1045 :
1046 2 : constraint = make_is_equal_to_constraint(sort, sort_bool::bool_());
1047 2 : context.remove_context_variables(variables);
1048 2 : }
1049 :
1050 2 : std::string print() const override
1051 : {
1052 2 : std::ostringstream out;
1053 2 : out << "exists(" << data::pp(variables) << ". " << children.front()->print() << ")";
1054 4 : return out.str();
1055 2 : }
1056 : };
1057 :
1058 : struct lambda_node final: public unary_operator_node
1059 : {
1060 : variable_list variables;
1061 :
1062 11 : lambda_node(type_check_context& context, const variable_list& variables_, type_check_node_ptr arg)
1063 11 : : unary_operator_node(context, "lambda", arg), variables(variables_)
1064 11 : {}
1065 :
1066 7 : void set_constraint(type_check_context& context) override
1067 : {
1068 7 : context.add_context_variables(variables);
1069 7 : set_children_constraints(context);
1070 :
1071 7 : constraint = make_true_constraint();
1072 7 : context.remove_context_variables(variables);
1073 7 : }
1074 :
1075 20 : std::string print() const override
1076 : {
1077 20 : std::ostringstream out;
1078 20 : out << "lambda(" << data::pp(variables) << ". " << children.front()->print() << ")";
1079 40 : return out.str();
1080 20 : }
1081 : };
1082 :
1083 : struct binary_operator_node final: public type_check_node
1084 : {
1085 : std::string name;
1086 :
1087 60 : binary_operator_node(type_check_context& context, const std::string& name_, type_check_node_ptr left, type_check_node_ptr right)
1088 180 : : type_check_node(context, { left, right }), name(name_)
1089 60 : {}
1090 :
1091 58 : void set_constraint(type_check_context& context) override
1092 : {
1093 58 : set_children_constraints(context);
1094 :
1095 58 : std::pair<function_sort_list, function_sort_list> p = context.find_matching_functions(name, 2);
1096 58 : std::vector<constraint_ptr> alternatives;
1097 387 : for (const function_sort& s: p.first + p.second)
1098 : {
1099 329 : auto i = s.domain().begin();
1100 329 : const sort_expression& left = *i++;
1101 329 : const sort_expression& right = *i;
1102 1645 : alternatives.push_back(make_and_constraint({
1103 329 : make_subsort_constraint(children[0]->sort, left),
1104 329 : make_subsort_constraint(children[1]->sort, right),
1105 : make_subsort_constraint(s.codomain(), sort)
1106 : })
1107 : );
1108 58 : }
1109 58 : constraint = make_or_constraint(alternatives);
1110 58 : }
1111 :
1112 108 : std::string print() const override
1113 : {
1114 108 : std::ostringstream out;
1115 108 : out << "binary_operator(" << name << ", " << children[0]->print() << ", " << children[1]->print() << ")";
1116 216 : return out.str();
1117 108 : }
1118 : };
1119 :
1120 : struct where_clause_node final: public type_check_node
1121 : {
1122 : std::vector<variable> variables;
1123 :
1124 13 : where_clause_node(type_check_context& context, type_check_node_ptr body, const std::vector<std::pair<std::string, type_check_node_ptr> >& assignments)
1125 13 : : type_check_node(context, {})
1126 : {
1127 13 : children.push_back(body);
1128 38 : for (const std::pair<std::string, type_check_node_ptr>& a: assignments)
1129 : {
1130 25 : children.push_back(a.second);
1131 25 : variables.push_back(variable(a.first, a.second->sort));
1132 : }
1133 13 : }
1134 :
1135 13 : void set_constraint(type_check_context& context) override
1136 : {
1137 13 : variable_list v(variables.begin(), variables.end());
1138 13 : context.add_context_variables(v);
1139 13 : set_children_constraints(context);
1140 13 : context.remove_context_variables(v);
1141 :
1142 13 : std::vector<constraint_ptr> constraints;
1143 13 : constraints.push_back(make_is_equal_to_constraint(sort, children[0]->sort));
1144 13 : auto i = variables.begin();
1145 13 : auto j = ++children.begin();
1146 38 : for (; i != variables.end(); ++i, ++j)
1147 : {
1148 25 : constraints.push_back(make_is_equal_to_constraint((*j)->sort, i->sort()));
1149 : }
1150 13 : constraint = make_and_constraint(constraints);
1151 13 : }
1152 :
1153 13 : std::string print() const override
1154 : {
1155 13 : std::ostringstream out;
1156 13 : return print_node_vector("where_clause", children);
1157 : return out.str();
1158 13 : }
1159 : };
1160 :
1161 : struct type_check_tree_generator final: public detail::data_expression_actions
1162 : {
1163 : type_check_context& context;
1164 :
1165 71 : type_check_tree_generator(type_check_context& context_, const core::parser& parser_)
1166 71 : : data_expression_actions(parser_), context(context_)
1167 71 : {}
1168 :
1169 22 : std::vector<type_check_node_ptr> parse_DataExprList(const core::parse_node& node) const
1170 : {
1171 68 : return parse_vector<type_check_node_ptr>(node, "DataExpr", [&](const core::parse_node& node) { return parse_DataExpr(node); });
1172 : }
1173 :
1174 2 : std::vector<type_check_node_ptr> parse_BagEnumEltList(const core::parse_node& node) const
1175 : {
1176 2 : return parse_DataExprList(node);
1177 : }
1178 :
1179 25 : std::pair<std::string, type_check_node_ptr> parse_Assignment(const core::parse_node& node) const
1180 : {
1181 50 : return std::make_pair(parse_Id(node.child(0)), parse_DataExpr(node.child(2)));
1182 : }
1183 :
1184 13 : std::vector<std::pair<std::string, type_check_node_ptr> > parse_AssignmentList(const core::parse_node& node) const
1185 : {
1186 38 : return parse_vector<std::pair<std::string, type_check_node_ptr> >(node, "Assignment", [&](const core::parse_node& node) { return parse_Assignment(node); });
1187 : }
1188 :
1189 326 : type_check_node_ptr parse_DataExpr(const core::parse_node& node) const
1190 : {
1191 326 : assert(symbol_name(node) == "DataExpr");
1192 326 : if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "Id")) { return type_check_node_ptr(new id_node(context, parse_Id(node.child(0)))); }
1193 242 : else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "Number")) { return type_check_node_ptr(new number_node(context, parse_Number(node.child(0)))); }
1194 168 : else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "true")) { return type_check_node_ptr(new true_node(context)); }
1195 156 : else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "false")) { return type_check_node_ptr(new false_node(context)); }
1196 146 : else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "[") && (symbol_name(node.child(1)) == "]")) { return type_check_node_ptr(new empty_list_node(context)); }
1197 141 : else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "{") && (symbol_name(node.child(1)) == "}")) { return type_check_node_ptr(new empty_set_node(context)); }
1198 135 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "{") && (symbol_name(node.child(1)) == ":") && (symbol_name(node.child(2)) == "}")) { return type_check_node_ptr(new empty_bag_node(context)); }
1199 148 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "[") && (symbol_name(node.child(1)) == "DataExprList") && (symbol_name(node.child(2)) == "]")) { return type_check_node_ptr(new list_enumeration_node(context, parse_DataExprList(node.child(1)))); }
1200 120 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "{") && (symbol_name(node.child(1)) == "BagEnumEltList") && (symbol_name(node.child(2)) == "}")) { return type_check_node_ptr(new bag_enumeration_node(context, parse_BagEnumEltList(node.child(1)))); }
1201 118 : else if ((node.child_count() == 5) && (symbol_name(node.child(0)) == "{") && (symbol_name(node.child(1)) == "VarDecl") && (symbol_name(node.child(2)) == "|") && (symbol_name(node.child(3)) == "DataExpr") && (symbol_name(node.child(4)) == "}")) { return type_check_node_ptr(new bag_or_set_enumeration_node(context, parse_VarDecl(node.child(1)), parse_DataExpr(node.child(3)))); }
1202 116 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "{") && (symbol_name(node.child(1)) == "DataExprList") && (symbol_name(node.child(2)) == "}")) { return type_check_node_ptr(new set_enumeration_node(context, parse_DataExprList(node.child(1)))); }
1203 117 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "(") && (symbol_name(node.child(1)) == "DataExpr") && (symbol_name(node.child(2)) == ")")) { return parse_DataExpr(node.child(1)); }
1204 112 : else if ((node.child_count() == 6) && (symbol_name(node.child(0)) == "DataExpr") && (symbol_name(node.child(1)) == "[") && (symbol_name(node.child(2)) == "DataExpr") && (symbol_name(node.child(3)) == "->") && (symbol_name(node.child(4)) == "DataExpr") && (symbol_name(node.child(5)) == "]")) { return type_check_node_ptr(new function_update_node(context, parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)), parse_DataExpr(node.child(4)))); }
1205 105 : else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "DataExpr") && (symbol_name(node.child(1)) == "(") && (symbol_name(node.child(2)) == "DataExprList") && (symbol_name(node.child(3)) == ")")) { return type_check_node_ptr(new application_node(context, parse_DataExpr(node.child(0)), parse_DataExprList(node.child(2)))); }
1206 104 : else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "!") && (symbol_name(node.child(1)) == "DataExpr")) { return type_check_node_ptr(new unary_operator_node(context, "!", parse_DataExpr(node.child(1)))); }
1207 98 : else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "-") && (symbol_name(node.child(1)) == "DataExpr")) { return type_check_node_ptr(new unary_operator_node(context, "-", parse_DataExpr(node.child(1)))); }
1208 91 : else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "#") && (symbol_name(node.child(1)) == "DataExpr")) { return type_check_node_ptr(new unary_operator_node(context, "#", parse_DataExpr(node.child(1)))); }
1209 92 : else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "forall") && (symbol_name(node.child(1)) == "VarsDeclList") && (symbol_name(node.child(2)) == ".") && (symbol_name(node.child(3)) == "DataExpr")) { return type_check_node_ptr(new forall_node(context, parse_VarsDeclList(node.child(1)), parse_DataExpr(node.child(3)))); }
1210 88 : else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "exists") && (symbol_name(node.child(1)) == "VarsDeclList") && (symbol_name(node.child(2)) == ".") && (symbol_name(node.child(3)) == "DataExpr")) { return type_check_node_ptr(new exists_node(context, parse_VarsDeclList(node.child(1)), parse_DataExpr(node.child(3)))); }
1211 95 : else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "lambda") && (symbol_name(node.child(1)) == "VarsDeclList") && (symbol_name(node.child(2)) == ".") && (symbol_name(node.child(3)) == "DataExpr")) { return type_check_node_ptr(new lambda_node(context, parse_VarsDeclList(node.child(1)), parse_DataExpr(node.child(3)))); }
1212 73 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "=>" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "=>" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1213 74 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "&&" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "&&" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1214 72 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "||" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "||" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1215 84 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "==" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "==" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1216 60 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "!=" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "!=" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1217 60 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "<" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "<" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1218 62 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "<=" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "<=" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1219 59 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == ">=" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, ">=" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1220 59 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == ">" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, ">" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1221 56 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "in" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "in" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1222 54 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "|>" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "|>" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1223 54 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "<|" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "<|" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1224 63 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "++" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "++" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1225 73 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "+" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "+" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1226 17 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "-" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "-" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1227 17 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "/" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "/" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1228 17 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "div") && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "div", parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1229 19 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "mod") && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "mod", parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1230 17 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "*" ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "*" , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1231 13 : else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "." ) && (symbol_name(node.child(2)) == "DataExpr")) { return type_check_node_ptr(new binary_operator_node(context, "." , parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)))); }
1232 26 : else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "DataExpr") && (symbol_name(node.child(1)) == "whr") && (symbol_name(node.child(2)) == "AssignmentList") && (symbol_name(node.child(3)) == "end")) { return type_check_node_ptr(new where_clause_node(context, { parse_DataExpr(node.child(0)) }, parse_AssignmentList(node.child(2)))); }
1233 0 : throw core::parse_node_unexpected_exception(m_parser, node);
1234 : }
1235 : };
1236 :
1237 : inline
1238 94 : std::pair<sort_expression_list, sort_expression_list> type_check_context::find_matching_constants(const std::string& name) const
1239 : {
1240 94 : sort_expression_list system_result;
1241 94 : sort_expression_list user_result;
1242 94 : auto i = system_constants.find(core::identifier_string(name));
1243 94 : if (i != system_constants.end())
1244 : {
1245 14 : system_result = i->second;
1246 : }
1247 94 : auto j = user_constants.find(core::identifier_string(name));
1248 94 : if (j != user_constants.end())
1249 : {
1250 0 : user_result = { j->second };
1251 : }
1252 188 : return std::make_pair(system_result, user_result);
1253 94 : }
1254 :
1255 : inline
1256 68 : function_sort_list filter_sorts(const function_sort_list& sorts, std::size_t arity)
1257 : {
1258 68 : std::vector<function_sort> result;
1259 458 : for (const function_sort& sort: sorts)
1260 : {
1261 390 : if (sort.domain().size() == arity)
1262 : {
1263 358 : result.push_back(sort);
1264 : }
1265 : }
1266 136 : return function_sort_list(result.begin(), result.end());
1267 68 : }
1268 :
1269 : inline
1270 68 : std::pair<function_sort_list, function_sort_list> type_check_context::find_matching_functions(const std::string& name, std::size_t arity) const
1271 : {
1272 68 : function_sort_list system_result;
1273 68 : function_sort_list user_result;
1274 68 : auto i = system_functions.find(core::identifier_string(name));
1275 68 : if (i != system_functions.end())
1276 : {
1277 68 : system_result = filter_sorts(i->second, arity);
1278 : }
1279 68 : auto j = user_functions.find(core::identifier_string(name));
1280 68 : if (j != user_functions.end())
1281 : {
1282 0 : user_result = filter_sorts(j->second, arity);
1283 : }
1284 136 : return { replace_untyped_sorts(system_result), user_result };
1285 68 : }
1286 :
1287 : inline
1288 80 : std::pair<function_sort_list, function_sort_list> type_check_context::find_matching_functions(const std::string& name) const
1289 : {
1290 80 : function_sort_list system_result;
1291 80 : function_sort_list user_result;
1292 80 : auto i = system_functions.find(core::identifier_string(name));
1293 80 : if (i != system_functions.end())
1294 : {
1295 1 : system_result = i->second;
1296 : }
1297 80 : auto j = user_functions.find(core::identifier_string(name));
1298 80 : if (j != user_functions.end())
1299 : {
1300 0 : user_result = j->second;
1301 : }
1302 160 : return { replace_untyped_sorts(system_result), user_result };
1303 80 : }
1304 :
1305 : inline
1306 80 : std::vector<sort_expression> type_check_context::find_matching_variables(const std::string& name) const
1307 : {
1308 80 : std::vector<sort_expression> result;
1309 80 : auto i = declared_variables.find(core::identifier_string(name));
1310 80 : if (i != declared_variables.end())
1311 : {
1312 77 : result.push_back(i->second.back());
1313 : }
1314 160 : return result;
1315 0 : }
1316 :
1317 : inline
1318 321 : void print_node(const type_check_node_ptr& node)
1319 : {
1320 321 : std::cout << "\nnode = " << node->print() << std::endl;
1321 321 : std::cout << "sort = " << node->sort << std::endl;
1322 321 : std::cout << "constraint = " << node->constraint->print() << std::endl;
1323 571 : for (const type_check_node_ptr& child: node->children)
1324 : {
1325 250 : print_node(child);
1326 : }
1327 321 : }
1328 :
1329 : // TODO: This design is ugly, but for the moment it seems the easiest solution to modify
1330 : // the constraint tree
1331 : inline
1332 0 : constraint_ptr substitute_constraint(constraint_ptr p, const sort_substitution& sigma)
1333 : {
1334 : {
1335 0 : or_constraint* x = dynamic_cast<or_constraint*>(p.get());
1336 0 : if (x)
1337 : {
1338 0 : for (constraint_ptr& q: x->alternatives)
1339 : {
1340 0 : q = substitute_constraint(q, sigma);
1341 : }
1342 0 : return p;
1343 : }
1344 : }
1345 : {
1346 0 : and_constraint* x = dynamic_cast<and_constraint*>(p.get());
1347 0 : if (x)
1348 : {
1349 0 : for (constraint_ptr& q: x->alternatives)
1350 : {
1351 0 : q = substitute_constraint(q, sigma);
1352 : }
1353 0 : return p;
1354 : }
1355 : }
1356 : {
1357 0 : is_equal_to_constraint* x = dynamic_cast<is_equal_to_constraint*>(p.get());
1358 0 : if (x)
1359 : {
1360 0 : sort_expression s1 = substitute(x->s1, sigma);
1361 0 : sort_expression s2 = substitute(x->s2, sigma);
1362 0 : return make_is_equal_to_constraint(s1, s2);
1363 0 : }
1364 : }
1365 0 : return p;
1366 : }
1367 :
1368 : } // namespace data
1369 :
1370 : } // namespace mcrl2
1371 :
1372 : #endif // MCRL2_DATA_EXPERIMENTAL_TYPE_CHECK_TREE_H
|
