LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/experimental - type_checker.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 169 274 61.7 %
Date: 2020-08-10 00:45:53 Functions: 12 22 54.5 %
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_checker.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_TYPE_CHECKER_H
      13             : #define MCRL2_DATA_TYPE_CHECKER_H
      14             : 
      15             : #include "mcrl2/data/parse_impl.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace data {
      20             : 
      21             : namespace detail {
      22             : 
      23             : inline
      24          70 : bool is_pos(const core::identifier_string& Number)
      25             : {
      26          70 :   char c = Number.function().name()[0];
      27          70 :   return isdigit(c) && c > '0';
      28             : }
      29             : 
      30             : inline
      31          15 : bool is_nat(const core::identifier_string& Number)
      32             : {
      33          15 :   return isdigit(Number.function().name()[0]) != 0;
      34             : }
      35             : 
      36             : inline
      37             : function_sort make_function_sort(const sort_expression& domain, const sort_expression& codomain)
      38             : {
      39             :   return function_sort({ domain }, codomain);
      40             : }
      41             : 
      42             : template <typename Function, typename T>
      43           0 : atermpp::term_list<T> transform_aterm_list(const Function& f, const atermpp::term_list<T>& x)
      44             : {
      45           0 :   atermpp::term_list<T> result;
      46           0 :   for (const T& t: x)
      47             :   {
      48           0 :     result.push_front(f(t));
      49             :   }
      50           0 :   return atermpp::reverse(result);
      51             : }
      52             : 
      53             : inline
      54           0 : sort_expression unwind_sort_expression(const sort_expression& x, const alias_vector& aliases)
      55             : {
      56           0 :   if (is_container_sort(x))
      57             :   {
      58           0 :     const container_sort& cs = atermpp::down_cast<const container_sort>(x);
      59           0 :     return container_sort(cs.container_name(), unwind_sort_expression(cs.element_sort(), aliases));
      60             :   }
      61           0 :   else if (is_function_sort(x))
      62             :   {
      63           0 :     const function_sort& fs = atermpp::down_cast<function_sort>(x);
      64           0 :     auto new_arguments = detail::transform_aterm_list([&](const sort_expression& s) { return unwind_sort_expression(s, aliases); }, fs.domain());
      65           0 :     return function_sort(new_arguments, unwind_sort_expression(fs.codomain(), aliases));
      66             :   }
      67           0 :   else if (is_basic_sort(x))
      68             :   {
      69           0 :     const basic_sort& bs = atermpp::down_cast<const basic_sort>(x);
      70           0 :     for(const alias& a: aliases)
      71             :     {
      72           0 :       if (bs == a.name())
      73             :       {
      74           0 :         return unwind_sort_expression(a.reference(), aliases);
      75             :       }
      76           0 :       return x;
      77             :     }
      78             :   }
      79           0 :   return x;
      80             : }
      81             : 
      82             : inline
      83             : bool is_numeric_type(const sort_expression& x)
      84             : {
      85             :   if (data::is_untyped_sort(x))
      86             :   {
      87             :     return false;
      88             :   }
      89             :   return sort_bool::is_bool(x)  ||
      90             :          sort_pos::is_pos(x)    ||
      91             :          sort_nat::is_nat(x)    ||
      92             :          sort_int::is_int(x)    ||
      93             :          sort_real::is_real(x);
      94             : }
      95             : 
      96             : } // namespace detail
      97             : 
      98          71 : class type_checker: public sort_type_checker
      99             : {
     100             :   protected:
     101             :     std::map<core::identifier_string, sort_expression_list> m_system_constants;
     102             :     std::map<core::identifier_string, function_sort_list> m_system_functions;
     103             :     std::map<core::identifier_string, sort_expression> m_user_constants;
     104             :     std::map<core::identifier_string, function_sort_list> m_user_functions;
     105             : 
     106         426 :     void add_system_constant(const data::function_symbol& f)
     107             :     {
     108             :       // append the Type to the entry of the Name of the OpId in system constants table
     109         426 :       auto i = m_system_constants.find(f.name());
     110         852 :       sort_expression_list sorts;
     111         426 :       if (i != m_system_constants.end())
     112             :       {
     113           0 :         sorts = i->second;
     114             :       }
     115         426 :       sorts = push_back(sorts, f.sort());
     116         426 :       m_system_constants[f.name()] = sorts;
     117         426 :     }
     118             : 
     119        8733 :     void add_system_function(const data::function_symbol& f)
     120             :     {
     121        8733 :       m_system_functions[f.name()] = m_system_functions[f.name()] + function_sort_list({ atermpp::down_cast<function_sort>(f.sort()) });
     122        8733 :     }
     123             : 
     124           0 :     sort_expression unwind_sort_expression(const sort_expression& x) const
     125             :     {
     126           0 :       return detail::unwind_sort_expression(x, get_sort_specification().user_defined_aliases());
     127             :     }
     128             : 
     129           0 :     bool equal_types(const sort_expression& x1, const sort_expression& x2) const
     130             :     {
     131           0 :       if (x1 == x2)
     132             :       {
     133           0 :         return true;
     134             :       }
     135           0 :       return unwind_sort_expression(x1) == unwind_sort_expression(x2);
     136             :     }
     137             : 
     138           0 :     bool find_sort(const sort_expression& x, const function_sort_list& sorts) const
     139             :     {
     140           0 :       return std::any_of(sorts.begin(), sorts.end(), [&](const function_sort& s) { return equal_types(x, s); });
     141             :     }
     142             : 
     143          71 :     void initialise_system_defined_functions()
     144             :     {
     145             :       //Creation of operation identifiers for system defined operations.
     146             :       //Bool
     147          71 :       add_system_constant(sort_bool::true_());
     148          71 :       add_system_constant(sort_bool::false_());
     149          71 :       add_system_function(sort_bool::not_());
     150          71 :       add_system_function(sort_bool::and_());
     151          71 :       add_system_function(sort_bool::or_());
     152          71 :       add_system_function(sort_bool::implies());
     153          71 :       add_system_function(equal_to(data::untyped_sort()));
     154          71 :       add_system_function(not_equal_to(data::untyped_sort()));
     155          71 :       add_system_function(if_(data::untyped_sort()));
     156          71 :       add_system_function(less(data::untyped_sort()));
     157          71 :       add_system_function(less_equal(data::untyped_sort()));
     158          71 :       add_system_function(greater_equal(data::untyped_sort()));
     159          71 :       add_system_function(greater(data::untyped_sort()));
     160             :       //Numbers
     161          71 :       add_system_function(sort_nat::pos2nat());
     162          71 :       add_system_function(sort_nat::cnat());
     163          71 :       add_system_function(sort_real::pos2real());
     164          71 :       add_system_function(sort_nat::nat2pos());
     165          71 :       add_system_function(sort_int::nat2int());
     166          71 :       add_system_function(sort_int::cint());
     167          71 :       add_system_function(sort_real::nat2real());
     168          71 :       add_system_function(sort_int::int2pos());
     169          71 :       add_system_function(sort_int::int2nat());
     170          71 :       add_system_function(sort_real::int2real());
     171          71 :       add_system_function(sort_real::creal());
     172          71 :       add_system_function(sort_real::real2pos());
     173          71 :       add_system_function(sort_real::real2nat());
     174          71 :       add_system_function(sort_real::real2int());
     175          71 :       add_system_constant(sort_pos::c1());
     176             :       //Square root for the natural numbers.
     177          71 :       add_system_function(sort_nat::sqrt());
     178             :       //more about numbers
     179          71 :       add_system_function(sort_real::maximum(sort_pos::pos(),sort_pos::pos()));
     180          71 :       add_system_function(sort_real::maximum(sort_pos::pos(),sort_nat::nat()));
     181          71 :       add_system_function(sort_real::maximum(sort_nat::nat(),sort_pos::pos()));
     182          71 :       add_system_function(sort_real::maximum(sort_nat::nat(),sort_nat::nat()));
     183          71 :       add_system_function(sort_real::maximum(sort_pos::pos(),sort_int::int_()));
     184          71 :       add_system_function(sort_real::maximum(sort_int::int_(),sort_pos::pos()));
     185          71 :       add_system_function(sort_real::maximum(sort_nat::nat(),sort_int::int_()));
     186          71 :       add_system_function(sort_real::maximum(sort_int::int_(),sort_nat::nat()));
     187          71 :       add_system_function(sort_real::maximum(sort_int::int_(),sort_int::int_()));
     188          71 :       add_system_function(sort_real::maximum(sort_real::real_(),sort_real::real_()));
     189             :       //more
     190          71 :       add_system_function(sort_real::minimum(sort_pos::pos(), sort_pos::pos()));
     191          71 :       add_system_function(sort_real::minimum(sort_nat::nat(), sort_nat::nat()));
     192          71 :       add_system_function(sort_real::minimum(sort_int::int_(), sort_int::int_()));
     193          71 :       add_system_function(sort_real::minimum(sort_real::real_(), sort_real::real_()));
     194             :       //more
     195             :       // add_system_function(sort_real::abs(sort_pos::pos()));
     196             :       // add_system_function(sort_real::abs(sort_nat::nat()));
     197          71 :       add_system_function(sort_real::abs(sort_int::int_()));
     198          71 :       add_system_function(sort_real::abs(sort_real::real_()));
     199             :       //more
     200          71 :       add_system_function(sort_real::negate(sort_pos::pos()));
     201          71 :       add_system_function(sort_real::negate(sort_nat::nat()));
     202          71 :       add_system_function(sort_real::negate(sort_int::int_()));
     203          71 :       add_system_function(sort_real::negate(sort_real::real_()));
     204          71 :       add_system_function(sort_real::succ(sort_pos::pos()));
     205          71 :       add_system_function(sort_real::succ(sort_nat::nat()));
     206          71 :       add_system_function(sort_real::succ(sort_int::int_()));
     207          71 :       add_system_function(sort_real::succ(sort_real::real_()));
     208          71 :       add_system_function(sort_real::pred(sort_pos::pos()));
     209          71 :       add_system_function(sort_real::pred(sort_nat::nat()));
     210          71 :       add_system_function(sort_real::pred(sort_int::int_()));
     211          71 :       add_system_function(sort_real::pred(sort_real::real_()));
     212          71 :       add_system_function(sort_real::plus(sort_pos::pos(),sort_pos::pos()));
     213          71 :       add_system_function(sort_real::plus(sort_pos::pos(),sort_nat::nat()));
     214          71 :       add_system_function(sort_real::plus(sort_nat::nat(),sort_pos::pos()));
     215          71 :       add_system_function(sort_real::plus(sort_nat::nat(),sort_nat::nat()));
     216          71 :       add_system_function(sort_real::plus(sort_int::int_(),sort_int::int_()));
     217          71 :       add_system_function(sort_real::plus(sort_real::real_(),sort_real::real_()));
     218             :       //more
     219          71 :       add_system_function(sort_real::minus(sort_pos::pos(), sort_pos::pos()));
     220          71 :       add_system_function(sort_real::minus(sort_nat::nat(), sort_nat::nat()));
     221          71 :       add_system_function(sort_real::minus(sort_int::int_(), sort_int::int_()));
     222          71 :       add_system_function(sort_real::minus(sort_real::real_(), sort_real::real_()));
     223          71 :       add_system_function(sort_real::times(sort_pos::pos(), sort_pos::pos()));
     224          71 :       add_system_function(sort_real::times(sort_nat::nat(), sort_nat::nat()));
     225          71 :       add_system_function(sort_real::times(sort_int::int_(), sort_int::int_()));
     226          71 :       add_system_function(sort_real::times(sort_real::real_(), sort_real::real_()));
     227             :       //more
     228             :       // add_system_function(sort_int::div(sort_pos::pos(), sort_pos::pos()));
     229          71 :       add_system_function(sort_int::div(sort_nat::nat(), sort_pos::pos()));
     230          71 :       add_system_function(sort_int::div(sort_int::int_(), sort_pos::pos()));
     231             :       // add_system_function(sort_int::mod(sort_pos::pos(), sort_pos::pos()));
     232          71 :       add_system_function(sort_int::mod(sort_nat::nat(), sort_pos::pos()));
     233          71 :       add_system_function(sort_int::mod(sort_int::int_(), sort_pos::pos()));
     234          71 :       add_system_function(sort_real::divides(sort_pos::pos(), sort_pos::pos()));
     235          71 :       add_system_function(sort_real::divides(sort_nat::nat(), sort_nat::nat()));
     236          71 :       add_system_function(sort_real::divides(sort_int::int_(), sort_int::int_()));
     237          71 :       add_system_function(sort_real::divides(sort_real::real_(), sort_real::real_()));
     238          71 :       add_system_function(sort_real::exp(sort_pos::pos(), sort_nat::nat()));
     239          71 :       add_system_function(sort_real::exp(sort_nat::nat(), sort_nat::nat()));
     240          71 :       add_system_function(sort_real::exp(sort_int::int_(), sort_nat::nat()));
     241          71 :       add_system_function(sort_real::exp(sort_real::real_(), sort_int::int_()));
     242          71 :       add_system_function(sort_real::floor());
     243          71 :       add_system_function(sort_real::ceil());
     244          71 :       add_system_function(sort_real::round());
     245             :       //Lists
     246          71 :       add_system_constant(sort_list::empty(data::untyped_sort()));
     247          71 :       add_system_function(sort_list::cons_(data::untyped_sort()));
     248          71 :       add_system_function(sort_list::count(data::untyped_sort()));
     249          71 :       add_system_function(sort_list::snoc(data::untyped_sort()));
     250          71 :       add_system_function(sort_list::concat(data::untyped_sort()));
     251          71 :       add_system_function(sort_list::element_at(data::untyped_sort()));
     252          71 :       add_system_function(sort_list::head(data::untyped_sort()));
     253          71 :       add_system_function(sort_list::tail(data::untyped_sort()));
     254          71 :       add_system_function(sort_list::rhead(data::untyped_sort()));
     255          71 :       add_system_function(sort_list::rtail(data::untyped_sort()));
     256          71 :       add_system_function(sort_list::in(data::untyped_sort()));
     257             : 
     258             :       //Sets
     259             : 
     260          71 :       add_system_function(sort_bag::set2bag(data::untyped_sort()));
     261          71 :       add_system_function(sort_set::in(data::untyped_sort(), data::untyped_sort(), sort_fset::fset(data::untyped_sort())));
     262          71 :       add_system_function(sort_set::in(data::untyped_sort(), data::untyped_sort(), sort_set::set_(data::untyped_sort())));
     263          71 :       add_system_function(sort_set::union_(data::untyped_sort(), sort_fset::fset(data::untyped_sort()), sort_fset::fset(data::untyped_sort())));
     264          71 :       add_system_function(sort_set::union_(data::untyped_sort(), sort_set::set_(data::untyped_sort()), sort_set::set_(data::untyped_sort())));
     265          71 :       add_system_function(sort_set::difference(data::untyped_sort(), sort_fset::fset(data::untyped_sort()), sort_fset::fset(data::untyped_sort())));
     266          71 :       add_system_function(sort_set::difference(data::untyped_sort(), sort_set::set_(data::untyped_sort()), sort_set::set_(data::untyped_sort())));
     267          71 :       add_system_function(sort_set::intersection(data::untyped_sort(), sort_fset::fset(data::untyped_sort()), sort_fset::fset(data::untyped_sort())));
     268          71 :       add_system_function(sort_set::intersection(data::untyped_sort(), sort_set::set_(data::untyped_sort()), sort_set::set_(data::untyped_sort())));
     269          71 :       add_system_function(sort_set::false_function(data::untyped_sort())); // Needed as it is used within the typechecker.
     270          71 :       add_system_function(sort_set::constructor(data::untyped_sort())); // Needed as it is used within the typechecker.
     271             :       //**** add_system_function(sort_bag::set2bag(data::untyped_sort()));
     272             :       // add_system_constant(sort_set::empty(data::untyped_sort()));
     273             :       // add_system_function(sort_set::in(data::untyped_sort()));
     274             :       // add_system_function(sort_set::union_(data::untyped_sort()));
     275             :       // add_system_function(sort_set::difference(data::untyped_sort()));
     276             :       // add_system_function(sort_set::intersection(data::untyped_sort()));
     277          71 :       add_system_function(sort_set::complement(data::untyped_sort()));
     278             : 
     279             :       //FSets
     280          71 :       add_system_constant(sort_fset::empty(data::untyped_sort()));
     281             :       // add_system_function(sort_fset::in(data::untyped_sort()));
     282             :       // add_system_function(sort_fset::union_(data::untyped_sort()));
     283             :       // add_system_function(sort_fset::intersection(data::untyped_sort()));
     284             :       // add_system_function(sort_fset::difference(data::untyped_sort()));
     285          71 :       add_system_function(sort_fset::count(data::untyped_sort()));
     286          71 :       add_system_function(sort_fset::insert(data::untyped_sort())); // Needed as it is used within the typechecker.
     287             : 
     288             :       //Bags
     289          71 :       add_system_function(sort_bag::bag2set(data::untyped_sort()));
     290          71 :       add_system_function(sort_bag::in(data::untyped_sort(), data::untyped_sort(), sort_fbag::fbag(data::untyped_sort())));
     291          71 :       add_system_function(sort_bag::in(data::untyped_sort(), data::untyped_sort(), sort_bag::bag(data::untyped_sort())));
     292          71 :       add_system_function(sort_bag::union_(data::untyped_sort(), sort_fbag::fbag(data::untyped_sort()), sort_fbag::fbag(data::untyped_sort())));
     293          71 :       add_system_function(sort_bag::union_(data::untyped_sort(), sort_bag::bag(data::untyped_sort()), sort_bag::bag(data::untyped_sort())));
     294          71 :       add_system_function(sort_bag::difference(data::untyped_sort(), sort_fbag::fbag(data::untyped_sort()), sort_fbag::fbag(data::untyped_sort())));
     295          71 :       add_system_function(sort_bag::difference(data::untyped_sort(), sort_bag::bag(data::untyped_sort()), sort_bag::bag(data::untyped_sort())));
     296          71 :       add_system_function(sort_bag::intersection(data::untyped_sort(), sort_fbag::fbag(data::untyped_sort()), sort_fbag::fbag(data::untyped_sort())));
     297          71 :       add_system_function(sort_bag::intersection(data::untyped_sort(), sort_bag::bag(data::untyped_sort()), sort_bag::bag(data::untyped_sort())));
     298          71 :       add_system_function(sort_bag::count(data::untyped_sort(), data::untyped_sort(), sort_fbag::fbag(data::untyped_sort())));
     299          71 :       add_system_function(sort_bag::count(data::untyped_sort(), data::untyped_sort(), sort_bag::bag(data::untyped_sort())));
     300             :       // add_system_constant(sort_bag::empty(data::untyped_sort()));
     301             :       // add_system_function(sort_bag::in(data::untyped_sort()));
     302             :       //**** add_system_function(sort_bag::count(data::untyped_sort()));
     303             :       // add_system_function(sort_bag::count(data::untyped_sort(), data::untyped_sort(), sort_fset::fset(data::untyped_sort())));
     304             :       //add_system_function(sort_bag::join(data::untyped_sort()));
     305             :       // add_system_function(sort_bag::difference(data::untyped_sort()));
     306             :       // add_system_function(sort_bag::intersection(data::untyped_sort()));
     307          71 :       add_system_function(sort_bag::zero_function(data::untyped_sort())); // Needed as it is used within the typechecker.
     308          71 :       add_system_function(sort_bag::constructor(data::untyped_sort())); // Needed as it is used within the typechecker.
     309             : 
     310             :       //FBags
     311          71 :       add_system_constant(sort_fbag::empty(data::untyped_sort()));
     312             :       // add_system_function(sort_fbag::count(data::untyped_sort()));
     313             :       // add_system_function(sort_fbag::in(data::untyped_sort()));
     314             :       // add_system_function(sort_fbag::union_(data::untyped_sort()));
     315             :       // add_system_function(sort_fbag::intersection(data::untyped_sort()));
     316             :       // add_system_function(sort_fbag::difference(data::untyped_sort()));
     317          71 :       add_system_function(sort_fbag::count_all(data::untyped_sort()));
     318          71 :       add_system_function(sort_fbag::cinsert(data::untyped_sort())); // Needed as it is used within the typechecker.
     319             : 
     320             :       // function update
     321          71 :       add_system_function(data::function_update(data::untyped_sort(),data::untyped_sort()));
     322          71 :     }
     323             : 
     324           0 :     void add_constant(const data::function_symbol& f, const std::string& msg)
     325             :     {
     326           0 :       if (m_user_constants.count(f.name()) > 0)
     327             :       {
     328           0 :         throw mcrl2::runtime_error("double declaration of " + msg + " " + core::pp(f.name()));
     329             :       }
     330           0 :       if (m_system_constants.count(f.name()) > 0 || m_system_functions.count(f.name()) > 0)
     331             :       {
     332           0 :         throw mcrl2::runtime_error("attempt to declare a constant with the name that is a built-in identifier (" + core::pp(f.name()) + ")");
     333             :       }
     334           0 :       m_user_constants[f.name()] = f.sort();
     335           0 :     }
     336             : 
     337           0 :     void add_function(const data::function_symbol& f, const std::string& msg, bool allow_double_decls = false)
     338             :     {
     339           0 :       if (m_system_constants.count(f.name()) > 0)
     340             :       {
     341           0 :         throw mcrl2::runtime_error("attempt to redeclare the system constant with a " + msg + " " + data::pp(f));
     342             :       }
     343             : 
     344           0 :       if (m_system_functions.count(f.name()) > 0)
     345             :       {
     346           0 :         throw mcrl2::runtime_error("attempt to redeclare a system function with a " + msg + " " + data::pp(f));
     347             :       }
     348             : 
     349           0 :       auto j = m_user_functions.find(f.name());
     350           0 :       const function_sort& fsort = atermpp::down_cast<function_sort>(f.sort());
     351             : 
     352             :       // the table m_user_functions contains a list of types for each
     353             :       // function name. We need to check if there is already such a type
     354             :       // in the list. If so -- error, otherwise -- add
     355           0 :       if (j != m_user_functions.end())
     356             :       {
     357           0 :         auto& sorts = j->second;
     358           0 :         if (find_sort(fsort, sorts))
     359             :         {
     360           0 :           if (!allow_double_decls)
     361             :           {
     362           0 :             throw mcrl2::runtime_error("double declaration of " + msg + " " + core::pp(f.name()));
     363             :           }
     364             :         }
     365             :       }
     366           0 :       m_user_functions[f.name()] = m_user_functions[f.name()] + function_sort_list({ fsort });
     367           0 :     }
     368             : 
     369             :     // Adds constants and functions corresponding to the sort x
     370           0 :     void read_sort(const sort_expression& x)
     371             :     {
     372           0 :       if (is_basic_sort(x))
     373             :       {
     374             :         // This should be checked elsewhere
     375             :         // check_basic_sort_is_declared(atermpp::down_cast<basic_sort>(x).name());
     376             :       }
     377           0 :       else if (is_container_sort(x))
     378             :       {
     379           0 :         read_sort(atermpp::down_cast<container_sort>(x).element_sort());
     380             :       }
     381           0 :       else if (is_function_sort(x))
     382             :       {
     383           0 :         const function_sort& fs = atermpp::down_cast<function_sort>(x);
     384           0 :         read_sort(fs.codomain());
     385           0 :         for (const sort_expression& sort: fs.domain())
     386             :         {
     387           0 :           read_sort(sort);
     388             :         }
     389             :       }
     390           0 :       else if (is_structured_sort(x))
     391             :       {
     392           0 :         const structured_sort& struct_sort = atermpp::down_cast<structured_sort>(x);
     393           0 :         for (const structured_sort_constructor& constructor: struct_sort.constructors())
     394             :         {
     395             :           // recognizer -- if present -- a function from SortExpr to Bool
     396           0 :           core::identifier_string name = constructor.recogniser();
     397           0 :           if (name != core::empty_identifier_string())
     398             :           {
     399           0 :             add_function(data::function_symbol(name, make_function_sort(x, sort_bool::bool_())), "recognizer");
     400             :           }
     401             : 
     402             :           // constructor type and projections
     403           0 :           structured_sort_constructor_argument_list arguments = constructor.arguments();
     404           0 :           name = constructor.name();
     405           0 :           if (arguments.empty())
     406             :           {
     407           0 :             add_constant(data::function_symbol(name, x), "constructor constant");
     408           0 :             continue;
     409             :           }
     410             : 
     411           0 :           sort_expression_list sorts;
     412           0 :           for (const structured_sort_constructor_argument& arg: arguments)
     413             :           {
     414           0 :             read_sort(arg.sort());
     415           0 :             if (arg.name() != core::empty_identifier_string())
     416             :             {
     417           0 :               add_function(function_symbol(arg.name(), function_sort({ x }, arg.sort())), "projection", true);
     418             :             }
     419           0 :             sorts.push_front(arg.sort());
     420             :           }
     421           0 :           add_function(data::function_symbol(name, function_sort(atermpp::reverse(sorts), x)), "constructor");
     422             :         }
     423             :       }
     424             :       // other sorts can be ignored
     425           0 :     }
     426             : 
     427          71 :     void read_constructors_and_mappings(const function_symbol_vector& constructors, const function_symbol_vector& mappings, const function_symbol_vector& normalized_constructors)
     428             :     {
     429          71 :       mCRL2log(log::debug) << "Start Read-in Func" << std::endl;
     430             : 
     431          71 :       std::size_t constr_number=constructors.size();
     432         142 :       function_symbol_vector functions_and_constructors=constructors;
     433          71 :       functions_and_constructors.insert(functions_and_constructors.end(),mappings.begin(),mappings.end());
     434          71 :       for (const function_symbol& f: functions_and_constructors)
     435             :       {
     436           0 :         sort_expression fsort = f.sort();
     437             : 
     438             :         // This should be checked elsewhere
     439             :         // check_sort_is_declared(fsort);
     440             : 
     441             :         //if fsort is a defined function sort, unwind it
     442           0 :         if (is_basic_sort(fsort))
     443             :         {
     444           0 :           const sort_expression s = unwind_sort_expression(fsort);
     445           0 :           if (is_function_sort(s))
     446             :           {
     447           0 :             fsort = s;
     448             :           }
     449             :         }
     450             : 
     451           0 :         if (is_function_sort(fsort))
     452             :         {
     453           0 :           add_function(data::function_symbol(f.name(), fsort), "function");
     454             :         }
     455             :         else
     456             :         {
     457             :           try
     458             :           {
     459           0 :             add_constant(data::function_symbol(f.name(), fsort), "constant");
     460             :           }
     461           0 :           catch (mcrl2::runtime_error& e)
     462             :           {
     463           0 :             throw mcrl2::runtime_error(std::string(e.what()) + "\ncould not add constant");
     464             :           }
     465             :         }
     466             : 
     467           0 :         if (constr_number)
     468             :         {
     469           0 :           constr_number--;
     470             : 
     471             :           //Here checks for the constructors
     472           0 :           sort_expression s = fsort;
     473           0 :           if (is_function_sort(s))
     474             :           {
     475           0 :             s = atermpp::down_cast<function_sort>(s).codomain();
     476             :           }
     477           0 :           s = unwind_sort_expression(s);
     478           0 :           if (!is_basic_sort(s) ||
     479           0 :               sort_bool::is_bool(sort_expression(s)) ||
     480           0 :               sort_pos::is_pos(sort_expression(s)) ||
     481           0 :               sort_nat::is_nat(sort_expression(s)) ||
     482           0 :               sort_int::is_int(sort_expression(s)) ||
     483           0 :               sort_real::is_real(sort_expression(s))
     484             :               )
     485             :           {
     486           0 :             throw mcrl2::runtime_error("Could not add constructor " + core::pp(f.name()) + " of sort " + data::pp(fsort) + ". Constructors of built-in sorts are not allowed.");
     487             :           }
     488             :         }
     489             : 
     490           0 :         mCRL2log(log::debug) << "Read-in Func " << f.name() << ", Types " << fsort << "" << std::endl;
     491             :       }
     492             : 
     493             :       // Check that the constructors are defined such that they cannot generate an empty sort.
     494             :       // E.g. in the specification sort D; cons f:D->D; the sort D must be necessarily empty, which is
     495             :       // forbidden. The function below checks whether such malicious specifications occur.
     496          71 :       check_for_empty_constructor_domains(normalized_constructors); // throws exception if not ok.
     497          71 :     }
     498             : 
     499             :   public:
     500          71 :     type_checker(const data_specification& data_spec)
     501          71 :       : sort_type_checker(data_spec)
     502             :     {
     503          71 :       initialise_system_defined_functions();
     504             :       try
     505             :       {
     506          71 :         for (const alias& a: get_sort_specification().user_defined_aliases())
     507             :         {
     508           0 :           read_sort(a.reference());
     509             :         }
     510          71 :         read_constructors_and_mappings(data_spec.user_defined_constructors(),data_spec.user_defined_mappings(),data_spec.constructors());
     511             :       }
     512           0 :       catch (mcrl2::runtime_error& e)
     513             :       {
     514           0 :         throw mcrl2::runtime_error(std::string(e.what()) + "\ntype checking of data expression failed");
     515             :       }
     516          71 :     }
     517             : 
     518          71 :     const std::map<core::identifier_string, sort_expression_list>& system_constants() const
     519             :     {
     520          71 :       return m_system_constants;
     521             :     }
     522             : 
     523          71 :     const std::map<core::identifier_string, function_sort_list>& system_functions() const
     524             :     {
     525          71 :       return m_system_functions;
     526             :     }
     527             : 
     528          71 :     const std::map<core::identifier_string, sort_expression>& user_constants() const
     529             :     {
     530          71 :       return m_user_constants;
     531             :     }
     532             : 
     533          71 :     const std::map<core::identifier_string, function_sort_list>& user_functions() const
     534             :     {
     535          71 :       return m_user_functions;
     536             :     }
     537             : };
     538             : 
     539             : } // namespace data
     540             : 
     541             : } // namespace mcrl2
     542             : 
     543             : #endif // MCRL2_DATA_TYPE_CHECKER_H
     544             : 

Generated by: LCOV version 1.13