LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/experimental - type_check_tree.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 570 660 86.4 %
Date: 2020-10-20 00:45:57 Functions: 133 138 96.4 %
Legend: Lines: hit not hit

          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         964 :   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         964 :   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             : }
      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          71 : 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         142 :     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         296 :     std::vector<function_sort> result;
     171         507 :     for (const function_sort& f: sorts)
     172             :     {
     173         359 :       if (has_untyped_sort(f))
     174             :       {
     175         318 :         function_sort f1 = replace_untyped_sort(f, create_sort_variable());
     176         159 :         result.push_back(f1);
     177             :       }
     178             :       else
     179             :       {
     180         200 :         result.push_back(f);
     181             :       }
     182             :     }
     183         296 :     return function_sort_list(result.begin(), result.end());
     184             :   }
     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: 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
     213             :   {
     214          34 :     return "true";
     215             :   }
     216             : };
     217             : 
     218           2 : struct false_constraint: 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
     227             :   {
     228           2 :     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        1328 : struct is_element_of_constraint: 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
     255             :   {
     256        1236 :     if (sorts.size() == 1)
     257             :     {
     258         746 :       return data::pp(s) + " = " + data::pp(*sorts.begin());
     259             :     }
     260         490 :     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             : }
     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             :   }
     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: 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
     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         571 :     return make_is_element_of_constraint(s1, { s2 });
     349             :   }
     350         175 :   if (is_untyped_sort_variable(s2))
     351             :   {
     352         175 :     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          75 : struct subsort_constraint: 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
     369             :   {
     370          75 :     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             :   }
     429         721 :   if (sort_pos::is_pos(s1))
     430             :   {
     431         141 :     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          57 :     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          42 :     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         121 :     return make_is_element_of_constraint(s1, { sort_pos::pos(), sort_nat::nat() });
     452             :   }
     453         204 :   if (sort_int::is_int(s2))
     454             :   {
     455          65 :     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          64 :     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         324 :   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             : }
     490             : 
     491          44 : struct or_constraint: 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         324 :   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             : }
     540             : 
     541         382 : struct and_constraint: 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
     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         794 :   std::vector<constraint_ptr> v;
     559        1528 :   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             :   }
     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             : }
     589             : 
     590         321 : 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             :   // Adds a value to the 'sort' attribute
     604             :   // Sets the constraints that apply to this node to 'constraint'
     605           4 :   virtual void set_constraint(type_check_context& /* context */)
     606           4 :   {}
     607             : 
     608           0 :   virtual void apply_substitution(const sort_substitution& sigma)
     609             :   {
     610           0 :     for (const type_check_node_ptr& child: children)
     611             :     {
     612           0 :       child->apply_substitution(sigma);
     613             :     }
     614           0 :     constraint = substitute_constraint(constraint, sigma);
     615           0 :   }
     616             : 
     617         131 :   void set_children_constraints(type_check_context& context)
     618             :   {
     619         358 :     for (const type_check_node_ptr& child: children)
     620             :     {
     621         227 :       child->set_constraint(context);
     622             :     }
     623         131 :   }
     624             : 
     625             :   // Throws an exception if the node violates a well typedness rule
     626           0 :   virtual void check_well_typedness(const type_check_context& /* context */)
     627           0 :   {}
     628             : 
     629             :   virtual std::string print() const = 0;
     630             : };
     631             : 
     632          84 : struct id_node: public type_check_node
     633             : {
     634             :   std::string value;
     635             : 
     636          84 :   id_node(type_check_context& context, const std::string& value_)
     637          84 :     : type_check_node(context, {}), value(value_)
     638          84 :   {}
     639             : 
     640          80 :   void set_constraint(type_check_context& context)
     641             :   {
     642         160 :     std::vector<constraint_ptr> alternatives;
     643             : 
     644             :     // it is a variable
     645         160 :     std::vector<sort_expression> variable_sorts = context.find_matching_variables(value);
     646          80 :     if (variable_sorts.size() == 1)
     647             :     {
     648          77 :       alternatives.push_back(make_is_equal_to_constraint(sort, variable_sorts.front()));
     649             :     }
     650             : 
     651             :     // it is a constant
     652         160 :     std::pair<sort_expression_list, sort_expression_list> p = context.find_matching_constants(value);
     653          80 :     for (const sort_expression& s: p.first + p.second)
     654             :     {
     655           0 :       alternatives.push_back(make_is_equal_to_constraint(sort, s));
     656             :     }
     657             : 
     658             :     // it is a function
     659         160 :     std::pair<function_sort_list, function_sort_list> q = context.find_matching_functions(value);
     660          81 :     for (const function_sort& s: q.first + q.second)
     661             :     {
     662           1 :       alternatives.push_back(make_is_equal_to_constraint(sort, s));
     663             :     }
     664             : 
     665          80 :     if (alternatives.empty())
     666             :     {
     667           2 :       constraint = make_false_constraint("The id " + value + " is not declared!");
     668             :     }
     669             :     else
     670             :     {
     671          78 :       constraint = make_or_constraint(alternatives);
     672             :     }
     673          80 :   }
     674             : 
     675         250 :   std::string print() const
     676             :   {
     677         250 :     return "id(" + value + ")";
     678             :   }
     679             : };
     680             : 
     681          74 : struct number_node: public type_check_node
     682             : {
     683             :   std::string value;
     684             : 
     685          74 :   number_node(type_check_context& context, const std::string& value_)
     686          74 :     : type_check_node(context, {}), value(value_)
     687          74 :   {}
     688             : 
     689          70 :   void set_constraint(type_check_context& /* context */)
     690             :   {
     691          70 :     if (detail::is_pos(value))
     692             :     {
     693          55 :       constraint = make_subsort_constraint(sort_pos::pos(), sort);
     694             :     }
     695          15 :     else if (detail::is_nat(value))
     696             :     {
     697          15 :       constraint = make_subsort_constraint(sort_nat::nat(), sort);
     698             :     }
     699             :     else
     700             :     {
     701           0 :       throw mcrl2::runtime_error("unknown numeric string " + value);
     702             :     }
     703          70 :   }
     704             : 
     705         184 :   std::string print() const
     706             :   {
     707         184 :     return "number(" + value + ")";
     708             :   }
     709             : };
     710             : 
     711          35 : struct constant_node: public type_check_node
     712             : {
     713             :   std::string name;
     714             : 
     715          35 :   constant_node(type_check_context& context, const std::string& name_)
     716          35 :     : type_check_node(context, {}), name(name_)
     717          35 :   {}
     718             : 
     719          14 :   void set_constraint(type_check_context& context)
     720             :   {
     721          28 :     std::pair<sort_expression_list, sort_expression_list> p = context.find_matching_constants(name);
     722          28 :     std::vector<constraint_ptr> alternatives;
     723          28 :     for (const sort_expression& s: p.first + p.second)
     724             :     {
     725          14 :       alternatives.push_back(make_subsort_constraint(s, sort));
     726             :     }
     727          14 :     constraint = make_or_constraint(alternatives);
     728          14 :     set_children_constraints(context);
     729          14 :   }
     730             : 
     731          70 :   std::string print() const
     732             :   {
     733          70 :     return "constant(" + name + ")";
     734             :   }
     735             : };
     736             : 
     737          12 : struct true_node: public constant_node
     738             : {
     739          12 :   true_node(type_check_context& context)
     740          12 :     : constant_node(context, "true")
     741          12 :   { }
     742             : };
     743             : 
     744          10 : struct false_node: public constant_node
     745             : {
     746          10 :   false_node(type_check_context& context)
     747          10 :     : constant_node(context, "false")
     748          10 :   { }
     749             : };
     750             : 
     751           5 : struct empty_list_node: public constant_node
     752             : {
     753           5 :   empty_list_node(type_check_context& context)
     754           5 :     : constant_node(context, "[]")
     755           5 :   { }
     756             : 
     757           5 :   void set_constraint(type_check_context& context)
     758             :   {
     759          10 :     auto element_sort = context.create_sort_variable();
     760           5 :     constraint = make_is_equal_to_constraint(sort, sort_list::list(element_sort));
     761           5 :   }
     762             : };
     763             : 
     764           6 : struct empty_set_node: public constant_node
     765             : {
     766           6 :   empty_set_node(type_check_context& context)
     767           6 :     : constant_node(context, "{}")
     768           6 :   { }
     769             : 
     770           6 :   void set_constraint(type_check_context& context)
     771             :   {
     772          12 :     auto element_sort = context.create_sort_variable();
     773           6 :     constraint = make_is_equal_to_constraint(sort, sort_set::set_(element_sort));
     774           6 :   }
     775             : };
     776             : 
     777           2 : struct empty_bag_node: public constant_node
     778             : {
     779           2 :   empty_bag_node(type_check_context& context)
     780           2 :     : constant_node(context, "{:}")
     781           2 :   { }
     782             : 
     783           2 :   void set_constraint(type_check_context& context)
     784             :   {
     785           4 :     auto element_sort = context.create_sort_variable();
     786           2 :     constraint = make_is_equal_to_constraint(sort, sort_bag::bag(element_sort));
     787           2 :   }
     788             : };
     789             : 
     790          15 : struct list_enumeration_node: public type_check_node
     791             : {
     792          15 :   list_enumeration_node(type_check_context& context, const std::vector<type_check_node_ptr>& children)
     793          15 :     : type_check_node(context, children)
     794          15 :   {}
     795             : 
     796          15 :   void set_constraint(type_check_context& context)
     797             :   {
     798          30 :     auto element_sort = context.create_sort_variable();
     799          15 :     set_children_constraints(context);
     800             : 
     801          30 :     std::vector<constraint_ptr> alternatives;
     802          15 :     alternatives.push_back(make_is_equal_to_constraint(sort, sort_list::list(element_sort)));
     803          41 :     for (const type_check_node_ptr& child: children)
     804             :     {
     805          26 :       alternatives.push_back(make_subsort_constraint(element_sort, child->sort));
     806             :     }
     807          15 :     constraint = make_and_constraint(alternatives);
     808          15 :   }
     809             : 
     810          25 :   std::string print() const
     811             :   {
     812          25 :     return print_node_vector("list_enumeration", children);
     813             :   }
     814             : };
     815             : 
     816           2 : struct bag_enumeration_node: public type_check_node
     817             : {
     818           2 :   bag_enumeration_node(type_check_context& context, const std::vector<type_check_node_ptr>& children)
     819           2 :     : type_check_node(context, children)
     820           2 :   {}
     821             : 
     822           2 :   void set_constraint(type_check_context& context)
     823             :   {
     824           4 :     auto element_sort = context.create_sort_variable();
     825           2 :     set_children_constraints(context);
     826             : 
     827           4 :     std::vector<constraint_ptr> alternatives;
     828           2 :     alternatives.push_back(make_is_equal_to_constraint(sort, sort_bag::bag(element_sort)));
     829          12 :     for (std::size_t i = 0; i < children.size(); i++)
     830             :     {
     831          10 :       if (i % 2 == 0)
     832             :       {
     833           5 :         alternatives.push_back(make_subsort_constraint(element_sort, children[i]->sort));
     834             :       }
     835             :       else
     836             :       {
     837           5 :         alternatives.push_back(make_subsort_constraint(sort_nat::nat(), children[i]->sort));
     838             :       }
     839             :     }
     840           2 :     constraint = make_and_constraint(alternatives);
     841           2 :   }
     842             : 
     843           2 :   std::string print() const
     844             :   {
     845           2 :     return print_node_vector("bag_enumeration", children);
     846             :   }
     847             : };
     848             : 
     849           2 : struct set_enumeration_node: public type_check_node
     850             : {
     851           2 :   set_enumeration_node(type_check_context& context, const std::vector<type_check_node_ptr>& children)
     852           2 :     : type_check_node(context, children)
     853           2 :   {}
     854             : 
     855           2 :   void set_constraint(type_check_context& context)
     856             :   {
     857           4 :     auto element_sort = context.create_sort_variable();
     858           2 :     set_children_constraints(context);
     859             : 
     860           4 :     std::vector<constraint_ptr> alternatives;
     861           2 :     alternatives.push_back(make_is_equal_to_constraint(sort, sort_set::set_(element_sort)));
     862           7 :     for (const type_check_node_ptr& child: children)
     863             :     {
     864           5 :       alternatives.push_back(make_subsort_constraint(element_sort, child->sort));
     865             :     }
     866           2 :     constraint = make_and_constraint(alternatives);
     867           2 :   }
     868             : 
     869           2 :   std::string print() const
     870             :   {
     871           2 :     return print_node_vector("set_enumeration", children);
     872             :   }
     873             : };
     874             : 
     875           2 : struct bag_or_set_enumeration_node: public type_check_node
     876             : {
     877             :   variable v;
     878             : 
     879           2 :   bag_or_set_enumeration_node(type_check_context& context, const variable& v_, type_check_node_ptr x)
     880           2 :     : type_check_node(context, {}), v(v_)
     881             :   {
     882           2 :     children.push_back(x);
     883           2 :   }
     884             : 
     885           2 :   void set_constraint(type_check_context& context)
     886             :   {
     887           2 :     context.add_context_variable(v);
     888           2 :     set_children_constraints(context);
     889             : 
     890           4 :     auto element_sort = v.sort();
     891             :     constraint_ptr set_constraint = make_and_constraint({
     892           4 :       make_is_equal_to_constraint(sort, sort_set::set_(element_sort)),
     893           4 :       make_is_equal_to_constraint(children.front()->sort, sort_bool::bool_())
     894           8 :     });
     895             :     constraint_ptr bag_constraint = make_and_constraint({
     896           4 :         make_is_equal_to_constraint(sort, sort_bag::bag(element_sort)),
     897           4 :         make_subsort_constraint(sort_nat::nat(), children.front()->sort)
     898           8 :        });
     899           2 :     constraint = make_or_constraint({ set_constraint, bag_constraint });
     900           2 :     context.remove_context_variable(v);
     901           2 :   }
     902             : 
     903           2 :   std::string print() const
     904             :   {
     905           2 :     return print_node_vector("bag_or_set_enumeration", children);
     906             :   }
     907             : };
     908             : 
     909           5 : struct function_update_node: public type_check_node
     910             : {
     911           5 :   function_update_node(type_check_context& context, type_check_node_ptr x1, type_check_node_ptr x2, type_check_node_ptr x3)
     912           5 :     : type_check_node(context, {})
     913             :   {
     914           5 :     children.push_back(x1);
     915           5 :     children.push_back(x2);
     916           5 :     children.push_back(x3);
     917           5 :   }
     918             : 
     919           6 :   std::string print() const
     920             :   {
     921           6 :     return print_node_vector("function_update", children);
     922             :   }
     923             : };
     924             : 
     925           3 : struct application_node: public type_check_node
     926             : {
     927             :   std::size_t arity;
     928             : 
     929           3 :   application_node(type_check_context& context, type_check_node_ptr head, const std::vector<type_check_node_ptr>& arguments)
     930           3 :     : type_check_node(context, {}), arity(arguments.size())
     931             :   {
     932           3 :     children.push_back(head);
     933           8 :     for (const auto& arg: arguments)
     934             :     {
     935           5 :       children.push_back(arg);
     936             :     }
     937           3 :   }
     938             : 
     939           3 :   void set_constraint(type_check_context& context)
     940             :   {
     941           3 :     set_children_constraints(context);
     942             : 
     943           3 :     const sort_expression& codomain = sort;
     944           6 :     std::vector<constraint_ptr> alternatives;
     945           6 :     std::vector<sort_expression> domain;
     946           8 :     for (std::size_t i = 0; i < arity; i++)
     947             :     {
     948           5 :       domain.push_back(children[i+1]->sort);
     949             :     }
     950           3 :     alternatives.push_back(make_is_equal_to_constraint(children[0]->sort, function_sort(sort_expression_list(domain.begin(), domain.end()), codomain)));
     951             : 
     952             :     // add missing constraints for if application
     953             :     // TODO: handle this in a more structured way
     954           3 :     if (children[0]->print() == "id(if)")
     955             :     {
     956           1 :       alternatives.push_back(make_subsort_constraint(codomain, children[1]->sort));
     957           1 :       alternatives.push_back(make_subsort_constraint(codomain, children[2]->sort));
     958             :     }
     959             : 
     960           3 :     constraint = make_and_constraint(alternatives);
     961           3 :   }
     962             : 
     963           6 :   std::string print() const
     964             :   {
     965           6 :     return print_node_vector("application", children);
     966             :   }
     967             : };
     968             : 
     969          21 : struct unary_operator_node: public type_check_node
     970             : {
     971             :   std::string name;
     972             : 
     973          21 :   unary_operator_node(type_check_context& context, const std::string& name_, type_check_node_ptr arg)
     974          21 :     : type_check_node(context, { arg }), name(name_)
     975          21 :   {}
     976             : 
     977          10 :   void set_constraint(type_check_context& context)
     978             :   {
     979          10 :     set_children_constraints(context);
     980             : 
     981          20 :     std::pair<function_sort_list, function_sort_list> p = context.find_matching_functions(name, 1);
     982          20 :     std::vector<constraint_ptr> alternatives;
     983          39 :     for (const function_sort& s: p.first + p.second)
     984             :     {
     985         116 :       alternatives.push_back(make_and_constraint({
     986          58 :           make_subsort_constraint(children[0]->sort, s.domain().front()),
     987             :           make_subsort_constraint(s.codomain(), sort)
     988          58 :          })
     989             :       );
     990             :     }
     991          10 :     constraint = make_or_constraint(alternatives);
     992          10 :   }
     993             : 
     994          16 :   std::string print() const
     995             :   {
     996          32 :     std::ostringstream out;
     997          16 :     out << "unary_operator(" << name << ", " << children.front()->print() << ")";
     998          32 :     return out.str();
     999             :   }
    1000             : };
    1001             : 
    1002           3 : struct forall_node: public type_check_node
    1003             : {
    1004             :   variable_list variables;
    1005             : 
    1006           3 :   forall_node(type_check_context& context, const variable_list& variables_, type_check_node_ptr arg)
    1007           3 :     : type_check_node(context, { arg }), variables(variables_)
    1008           3 :   {}
    1009             : 
    1010           3 :   void set_constraint(type_check_context& context)
    1011             :   {
    1012           3 :     context.add_context_variables(variables);
    1013           3 :     set_children_constraints(context);
    1014             : 
    1015           3 :     constraint = make_is_equal_to_constraint(sort, sort_bool::bool_());
    1016           3 :     context.remove_context_variables(variables);
    1017           3 :   }
    1018             : 
    1019           3 :   std::string print() const
    1020             :   {
    1021           6 :     std::ostringstream out;
    1022           3 :     out << "forall(" << data::pp(variables) << ". " << children.front()->print() << ")";
    1023           6 :     return out.str();
    1024             :   }
    1025             : };
    1026             : 
    1027           2 : struct exists_node: public type_check_node
    1028             : {
    1029             :   variable_list variables;
    1030             : 
    1031           2 :   exists_node(type_check_context& context, const variable_list& variables_, type_check_node_ptr arg)
    1032           2 :     : type_check_node(context, { arg }), variables(variables_)
    1033           2 :   {}
    1034             : 
    1035           2 :   void set_constraint(type_check_context& context)
    1036             :   {
    1037           2 :     context.add_context_variables(variables);
    1038           2 :     set_children_constraints(context);
    1039             : 
    1040           2 :     constraint = make_is_equal_to_constraint(sort, sort_bool::bool_());
    1041           2 :     context.remove_context_variables(variables);
    1042           2 :   }
    1043             : 
    1044           2 :   std::string print() const
    1045             :   {
    1046           4 :     std::ostringstream out;
    1047           2 :     out << "exists(" << data::pp(variables) << ". " << children.front()->print() << ")";
    1048           4 :     return out.str();
    1049             :   }
    1050             : };
    1051             : 
    1052          11 : struct lambda_node: public unary_operator_node
    1053             : {
    1054             :   variable_list variables;
    1055             : 
    1056          11 :   lambda_node(type_check_context& context, const variable_list& variables_, type_check_node_ptr arg)
    1057          11 :     : unary_operator_node(context, "lambda", arg), variables(variables_)
    1058          11 :   {}
    1059             : 
    1060           7 :   void set_constraint(type_check_context& context)
    1061             :   {
    1062           7 :     context.add_context_variables(variables);
    1063           7 :     set_children_constraints(context);
    1064             : 
    1065           7 :     constraint = make_true_constraint();
    1066           7 :     context.remove_context_variables(variables);
    1067           7 :   }
    1068             : 
    1069          20 :   std::string print() const
    1070             :   {
    1071          40 :     std::ostringstream out;
    1072          20 :     out << "lambda(" << data::pp(variables) << ". " << children.front()->print() << ")";
    1073          40 :     return out.str();
    1074             :   }
    1075             : };
    1076             : 
    1077          60 : struct binary_operator_node: public type_check_node
    1078             : {
    1079             :   std::string name;
    1080             : 
    1081          60 :   binary_operator_node(type_check_context& context, const std::string& name_, type_check_node_ptr left, type_check_node_ptr right)
    1082          60 :     : type_check_node(context, { left, right }), name(name_)
    1083          60 :   {}
    1084             : 
    1085          58 :   void set_constraint(type_check_context& context)
    1086             :   {
    1087          58 :     set_children_constraints(context);
    1088             : 
    1089         116 :     std::pair<function_sort_list, function_sort_list> p = context.find_matching_functions(name, 2);
    1090         116 :     std::vector<constraint_ptr> alternatives;
    1091         387 :     for (const function_sort& s: p.first + p.second)
    1092             :     {
    1093         329 :       auto i = s.domain().begin();
    1094         329 :       const sort_expression& left = *i++;
    1095         329 :       const sort_expression& right = *i;
    1096        1645 :       alternatives.push_back(make_and_constraint({
    1097         329 :           make_subsort_constraint(children[0]->sort, left),
    1098         329 :           make_subsort_constraint(children[1]->sort, right),
    1099             :           make_subsort_constraint(s.codomain(), sort)
    1100         987 :          })
    1101             :       );
    1102             :     }
    1103          58 :     constraint = make_or_constraint(alternatives);
    1104          58 :   }
    1105             : 
    1106         108 :   std::string print() const
    1107             :   {
    1108         216 :     std::ostringstream out;
    1109         108 :     out << "binary_operator(" << name << ", " << children[0]->print() << ", " << children[1]->print() << ")";
    1110         216 :     return out.str();
    1111             :   }
    1112             : };
    1113             : 
    1114          13 : struct where_clause_node: public type_check_node
    1115             : {
    1116             :   std::vector<variable> variables;
    1117             : 
    1118          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)
    1119          13 :     : type_check_node(context, {})
    1120             :   {
    1121          13 :     children.push_back(body);
    1122          38 :     for (const std::pair<std::string, type_check_node_ptr>& a: assignments)
    1123             :     {
    1124          25 :       children.push_back(a.second);
    1125          25 :       variables.push_back(variable(a.first, a.second->sort));
    1126             :     }
    1127          13 :   }
    1128             : 
    1129          13 :   void set_constraint(type_check_context& context)
    1130             :   {
    1131          26 :     variable_list v(variables.begin(), variables.end());
    1132          13 :     context.add_context_variables(v);
    1133          13 :     set_children_constraints(context);
    1134          13 :     context.remove_context_variables(v);
    1135             : 
    1136          26 :     std::vector<constraint_ptr> constraints;
    1137          13 :     constraints.push_back(make_is_equal_to_constraint(sort, children[0]->sort));
    1138          13 :     auto i = variables.begin();
    1139          13 :     auto j = ++children.begin();
    1140          63 :     for (; i != variables.end(); ++i, ++j)
    1141             :     {
    1142          25 :       constraints.push_back(make_is_equal_to_constraint((*j)->sort, i->sort()));
    1143             :     }
    1144          13 :     constraint = make_and_constraint(constraints);
    1145          13 :   }
    1146             : 
    1147          13 :   std::string print() const
    1148             :   {
    1149          26 :     std::ostringstream out;
    1150          13 :     return print_node_vector("where_clause", children);
    1151             :     return out.str();
    1152             :   }
    1153             : };
    1154             : 
    1155             : struct type_check_tree_generator: public detail::data_expression_actions
    1156             : {
    1157             :   type_check_context& context;
    1158             : 
    1159          71 :   type_check_tree_generator(type_check_context& context_, const core::parser& parser_)
    1160          71 :     : data_expression_actions(parser_), context(context_)
    1161          71 :   {}
    1162             : 
    1163          22 :   std::vector<type_check_node_ptr> parse_DataExprList(const core::parse_node& node) const
    1164             :   {
    1165          68 :     return parse_vector<type_check_node_ptr>(node, "DataExpr", [&](const core::parse_node& node) { return parse_DataExpr(node); });
    1166             :   }
    1167             : 
    1168           2 :   std::vector<type_check_node_ptr> parse_BagEnumEltList(const core::parse_node& node) const
    1169             :   {
    1170           2 :     return parse_DataExprList(node);
    1171             :   }
    1172             : 
    1173          25 :   std::pair<std::string, type_check_node_ptr> parse_Assignment(const core::parse_node& node) const
    1174             :   {
    1175          25 :     return std::make_pair(parse_Id(node.child(0)), parse_DataExpr(node.child(2)));
    1176             :   }
    1177             : 
    1178          13 :   std::vector<std::pair<std::string, type_check_node_ptr> > parse_AssignmentList(const core::parse_node& node) const
    1179             :   {
    1180          38 :     return parse_vector<std::pair<std::string, type_check_node_ptr> >(node, "Assignment", [&](const core::parse_node& node) { return parse_Assignment(node); });
    1181             :   }
    1182             : 
    1183         326 :   type_check_node_ptr parse_DataExpr(const core::parse_node& node) const
    1184             :   {
    1185         326 :     assert(symbol_name(node) == "DataExpr");
    1186         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)))); }
    1187         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)))); }
    1188         168 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "true")) { return type_check_node_ptr(new true_node(context)); }
    1189         156 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "false")) { return type_check_node_ptr(new false_node(context)); }
    1190         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)); }
    1191         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)); }
    1192         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)); }
    1193         133 :     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)))); }
    1194         118 :     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)))); }
    1195         116 :     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)))); }
    1196         114 :     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)))); }
    1197         112 :     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)); }
    1198         107 :     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)))); }
    1199         102 :     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)))); }
    1200          99 :     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)))); }
    1201          94 :     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)))); }
    1202          90 :     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)))); }
    1203          89 :     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)))); }
    1204          86 :     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)))); }
    1205          84 :     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)))); }
    1206          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)))); }
    1207          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)))); }
    1208          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)))); }
    1209          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)))); }
    1210          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)))); }
    1211          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)))); }
    1212          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)))); }
    1213          58 :     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          57 :     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          55 :     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)))); }
    1216          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)))); }
    1217          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)))); }
    1218          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)))); }
    1219          45 :     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          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)))); }
    1221          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)))); }
    1222          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)))); }
    1223          17 :     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)))); }
    1224          15 :     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          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)))); }
    1226          13 :     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)))); }
    1227           0 :     throw core::parse_node_unexpected_exception(m_parser, node);
    1228             :   }
    1229             : };
    1230             : 
    1231             : inline
    1232          94 : std::pair<sort_expression_list, sort_expression_list> type_check_context::find_matching_constants(const std::string& name) const
    1233             : {
    1234         188 :   sort_expression_list system_result;
    1235         188 :   sort_expression_list user_result;
    1236          94 :   auto i = system_constants.find(core::identifier_string(name));
    1237          94 :   if (i != system_constants.end())
    1238             :   {
    1239          14 :     system_result = i->second;
    1240             :   }
    1241          94 :   auto j = user_constants.find(core::identifier_string(name));
    1242          94 :   if (j != user_constants.end())
    1243             :   {
    1244           0 :     user_result = { j->second };
    1245             :   }
    1246         188 :   return std::make_pair(system_result, user_result);
    1247             : }
    1248             : 
    1249             : inline
    1250          68 : function_sort_list filter_sorts(const function_sort_list& sorts, std::size_t arity)
    1251             : {
    1252         136 :   std::vector<function_sort> result;
    1253         458 :   for (const function_sort& sort: sorts)
    1254             :   {
    1255         390 :     if (sort.domain().size() == arity)
    1256             :     {
    1257         358 :       result.push_back(sort);
    1258             :     }
    1259             :   }
    1260         136 :   return function_sort_list(result.begin(), result.end());
    1261             : }
    1262             : 
    1263             : inline
    1264          68 : std::pair<function_sort_list, function_sort_list> type_check_context::find_matching_functions(const std::string& name, std::size_t arity) const
    1265             : {
    1266         136 :   function_sort_list system_result;
    1267         136 :   function_sort_list user_result;
    1268          68 :   auto i = system_functions.find(core::identifier_string(name));
    1269          68 :   if (i != system_functions.end())
    1270             :   {
    1271          68 :     system_result = filter_sorts(i->second, arity);
    1272             :   }
    1273          68 :   auto j = user_functions.find(core::identifier_string(name));
    1274          68 :   if (j != user_functions.end())
    1275             :   {
    1276           0 :     user_result = filter_sorts(j->second, arity);
    1277             :   }
    1278         136 :   return { replace_untyped_sorts(system_result), user_result };
    1279             : }
    1280             : 
    1281             : inline
    1282          80 : std::pair<function_sort_list, function_sort_list> type_check_context::find_matching_functions(const std::string& name) const
    1283             : {
    1284         160 :   function_sort_list system_result;
    1285         160 :   function_sort_list user_result;
    1286          80 :   auto i = system_functions.find(core::identifier_string(name));
    1287          80 :   if (i != system_functions.end())
    1288             :   {
    1289           1 :     system_result = i->second;
    1290             :   }
    1291          80 :   auto j = user_functions.find(core::identifier_string(name));
    1292          80 :   if (j != user_functions.end())
    1293             :   {
    1294           0 :     user_result = j->second;
    1295             :   }
    1296         160 :   return { replace_untyped_sorts(system_result), user_result };
    1297             : }
    1298             : 
    1299             : inline
    1300          80 : std::vector<sort_expression> type_check_context::find_matching_variables(const std::string& name) const
    1301             : {
    1302          80 :   std::vector<sort_expression> result;
    1303          80 :   auto i = declared_variables.find(core::identifier_string(name));
    1304          80 :   if (i != declared_variables.end())
    1305             :   {
    1306          77 :     result.push_back(i->second.back());
    1307             :   }
    1308          80 :   return result;
    1309             : }
    1310             : 
    1311             : inline
    1312         321 : void print_node(const type_check_node_ptr& node)
    1313             : {
    1314         321 :   std::cout << "\nnode = " << node->print() << std::endl;
    1315         321 :   std::cout << "sort = " << node->sort << std::endl;
    1316         321 :   std::cout << "constraint = " << node->constraint->print() << std::endl;
    1317         571 :   for (const type_check_node_ptr& child: node->children)
    1318             :   {
    1319         250 :     print_node(child);
    1320             :   }
    1321         321 : }
    1322             : 
    1323             : // TODO: This design is ugly, but for the moment it seems the easiest solution to modify
    1324             : // the constraint tree
    1325             : inline
    1326           0 : constraint_ptr substitute_constraint(constraint_ptr p, const sort_substitution& sigma)
    1327             : {
    1328             :   {
    1329           0 :     or_constraint* x = dynamic_cast<or_constraint*>(p.get());
    1330           0 :     if (x)
    1331             :     {
    1332           0 :       for (constraint_ptr& q: x->alternatives)
    1333             :       {
    1334           0 :         q = substitute_constraint(q, sigma);
    1335             :       }
    1336           0 :       return p;
    1337             :     }
    1338             :   }
    1339             :   {
    1340           0 :     and_constraint* x = dynamic_cast<and_constraint*>(p.get());
    1341           0 :     if (x)
    1342             :     {
    1343           0 :       for (constraint_ptr& q: x->alternatives)
    1344             :       {
    1345           0 :         q = substitute_constraint(q, sigma);
    1346             :       }
    1347           0 :       return p;
    1348             :     }
    1349             :   }
    1350             :   {
    1351           0 :     is_equal_to_constraint* x = dynamic_cast<is_equal_to_constraint*>(p.get());
    1352           0 :     if (x)
    1353             :     {
    1354           0 :       sort_expression s1 = substitute(x->s1, sigma);
    1355           0 :       sort_expression s2 = substitute(x->s2, sigma);
    1356           0 :       return make_is_equal_to_constraint(s1, s2);
    1357             :     }
    1358             :   }
    1359           0 :   return p;
    1360             : }
    1361             : 
    1362             : } // namespace data
    1363             : 
    1364             : } // namespace mcrl2
    1365             : 
    1366             : #endif // MCRL2_DATA_EXPERIMENTAL_TYPE_CHECK_TREE_H

Generated by: LCOV version 1.13