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 data.cpp
      10             : /// \brief
      11             : 
      12             : #include "mcrl2/data/normalize_sorts.h"
      13             : #include "mcrl2/data/parse_impl.h"
      14             : #include "mcrl2/data/print.h"
      15             : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
      16             : #include "mcrl2/data/translate_user_notation.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace data
      22             : {
      23             : 
      24             : //--- start generated data overloads ---//
      25          28 : std::string pp(const data::sort_expression_list& x) { return data::pp< data::sort_expression_list >(x); }
      26           0 : std::string pp(const data::sort_expression_vector& x) { return data::pp< data::sort_expression_vector >(x); }
      27         114 : std::string pp(const data::data_expression_list& x) { return data::pp< data::data_expression_list >(x); }
      28           0 : std::string pp(const data::data_expression_vector& x) { return data::pp< data::data_expression_vector >(x); }
      29           0 : std::string pp(const data::assignment_list& x) { return data::pp< data::assignment_list >(x); }
      30           1 : std::string pp(const data::assignment_vector& x) { return data::pp< data::assignment_vector >(x); }
      31          28 : std::string pp(const data::variable_list& x) { return data::pp< data::variable_list >(x); }
      32           0 : std::string pp(const data::variable_vector& x) { return data::pp< data::variable_vector >(x); }
      33           0 : std::string pp(const data::function_symbol_list& x) { return data::pp< data::function_symbol_list >(x); }
      34           0 : std::string pp(const data::function_symbol_vector& x) { return data::pp< data::function_symbol_vector >(x); }
      35           0 : std::string pp(const data::structured_sort_constructor_list& x) { return data::pp< data::structured_sort_constructor_list >(x); }
      36           0 : std::string pp(const data::structured_sort_constructor_vector& x) { return data::pp< data::structured_sort_constructor_vector >(x); }
      37           0 : std::string pp(const data::data_equation_list& x) { return data::pp< data::data_equation_list >(x); }
      38           9 : std::string pp(const data::data_equation_vector& x) { return data::pp< data::data_equation_vector >(x); }
      39           0 : std::string pp(const data::abstraction& x) { return data::pp< data::abstraction >(x); }
      40          10 : std::string pp(const data::alias& x) { return data::pp< data::alias >(x); }
      41          85 : std::string pp(const data::application& x) { return data::pp< data::application >(x); }
      42           0 : std::string pp(const data::assignment& x) { return data::pp< data::assignment >(x); }
      43           0 : std::string pp(const data::assignment_expression& x) { return data::pp< data::assignment_expression >(x); }
      44           0 : std::string pp(const data::bag_comprehension& x) { return data::pp< data::bag_comprehension >(x); }
      45           0 : std::string pp(const data::bag_comprehension_binder& x) { return data::pp< data::bag_comprehension_binder >(x); }
      46           0 : std::string pp(const data::bag_container& x) { return data::pp< data::bag_container >(x); }
      47          43 : std::string pp(const data::basic_sort& x) { return data::pp< data::basic_sort >(x); }
      48           0 : std::string pp(const data::binder_type& x) { return data::pp< data::binder_type >(x); }
      49           6 : std::string pp(const data::container_sort& x) { return data::pp< data::container_sort >(x); }
      50           0 : std::string pp(const data::container_type& x) { return data::pp< data::container_type >(x); }
      51          10 : std::string pp(const data::data_equation& x) { return data::pp< data::data_equation >(x); }
      52       12591 : std::string pp(const data::data_expression& x) { return data::pp< data::data_expression >(x); }
      53         127 : std::string pp(const data::data_specification& x) { return data::pp< data::data_specification >(x); }
      54           4 : std::string pp(const data::exists& x) { return data::pp< data::exists >(x); }
      55           0 : std::string pp(const data::exists_binder& x) { return data::pp< data::exists_binder >(x); }
      56           0 : std::string pp(const data::fbag_container& x) { return data::pp< data::fbag_container >(x); }
      57           6 : std::string pp(const data::forall& x) { return data::pp< data::forall >(x); }
      58           0 : std::string pp(const data::forall_binder& x) { return data::pp< data::forall_binder >(x); }
      59           0 : std::string pp(const data::fset_container& x) { return data::pp< data::fset_container >(x); }
      60           0 : std::string pp(const data::function_sort& x) { return data::pp< data::function_sort >(x); }
      61        1895 : std::string pp(const data::function_symbol& x) { return data::pp< data::function_symbol >(x); }
      62           4 : std::string pp(const data::lambda& x) { return data::pp< data::lambda >(x); }
      63           0 : std::string pp(const data::lambda_binder& x) { return data::pp< data::lambda_binder >(x); }
      64           0 : std::string pp(const data::list_container& x) { return data::pp< data::list_container >(x); }
      65           0 : std::string pp(const data::set_comprehension& x) { return data::pp< data::set_comprehension >(x); }
      66           0 : std::string pp(const data::set_comprehension_binder& x) { return data::pp< data::set_comprehension_binder >(x); }
      67           0 : std::string pp(const data::set_container& x) { return data::pp< data::set_container >(x); }
      68       12497 : std::string pp(const data::sort_expression& x) { return data::pp< data::sort_expression >(x); }
      69           0 : std::string pp(const data::structured_sort& x) { return data::pp< data::structured_sort >(x); }
      70           0 : std::string pp(const data::structured_sort_constructor& x) { return data::pp< data::structured_sort_constructor >(x); }
      71          42 : std::string pp(const data::structured_sort_constructor_argument& x) { return data::pp< data::structured_sort_constructor_argument >(x); }
      72           0 : std::string pp(const data::untyped_data_parameter& x) { return data::pp< data::untyped_data_parameter >(x); }
      73           0 : std::string pp(const data::untyped_identifier& x) { return data::pp< data::untyped_identifier >(x); }
      74           0 : std::string pp(const data::untyped_identifier_assignment& x) { return data::pp< data::untyped_identifier_assignment >(x); }
      75           0 : std::string pp(const data::untyped_possible_sorts& x) { return data::pp< data::untyped_possible_sorts >(x); }
      76           0 : std::string pp(const data::untyped_set_or_bag_comprehension& x) { return data::pp< data::untyped_set_or_bag_comprehension >(x); }
      77           0 : std::string pp(const data::untyped_set_or_bag_comprehension_binder& x) { return data::pp< data::untyped_set_or_bag_comprehension_binder >(x); }
      78           1 : std::string pp(const data::untyped_sort& x) { return data::pp< data::untyped_sort >(x); }
      79        1557 : std::string pp(const data::untyped_sort_variable& x) { return data::pp< data::untyped_sort_variable >(x); }
      80        2296 : std::string pp(const data::variable& x) { return data::pp< data::variable >(x); }
      81           0 : std::string pp(const data::where_clause& x) { return data::pp< data::where_clause >(x); }
      82     2726561 : data::data_equation normalize_sorts(const data::data_equation& x, const data::sort_specification& sortspec) { return data::normalize_sorts< data::data_equation >(x, sortspec); }
      83           0 : data::data_equation_list normalize_sorts(const data::data_equation_list& x, const data::sort_specification& sortspec) { return data::normalize_sorts< data::data_equation_list >(x, sortspec); }
      84         387 : void normalize_sorts(data::data_equation_vector& x, const data::sort_specification& sortspec) { data::normalize_sorts< data::data_equation_vector >(x, sortspec); }
      85     1290306 : data::data_expression normalize_sorts(const data::data_expression& x, const data::sort_specification& sortspec) { return data::normalize_sorts< data::data_expression >(x, sortspec); }
      86      747509 : data::sort_expression normalize_sorts(const data::sort_expression& x, const data::sort_specification& sortspec) { return data::normalize_sorts< data::sort_expression >(x, sortspec); }
      87         124 : data::variable_list normalize_sorts(const data::variable_list& x, const data::sort_specification& sortspec) { return data::normalize_sorts< data::variable_list >(x, sortspec); }
      88         696 : data::data_expression translate_user_notation(const data::data_expression& x) { return data::translate_user_notation< data::data_expression >(x); }
      89        3793 : data::data_equation translate_user_notation(const data::data_equation& x) { return data::translate_user_notation< data::data_equation >(x); }
      90        2220 : std::set<data::sort_expression> find_sort_expressions(const data::data_equation& x) { return data::find_sort_expressions< data::data_equation >(x); }
      91           2 : std::set<data::sort_expression> find_sort_expressions(const data::data_expression& x) { return data::find_sort_expressions< data::data_expression >(x); }
      92      179119 : std::set<data::sort_expression> find_sort_expressions(const data::sort_expression& x) { return data::find_sort_expressions< data::sort_expression >(x); }
      93         312 : std::set<data::variable> find_all_variables(const data::data_expression& x) { return data::find_all_variables< data::data_expression >(x); }
      94          10 : std::set<data::variable> find_all_variables(const data::data_expression_list& x) { return data::find_all_variables< data::data_expression_list >(x); }
      95           0 : std::set<data::variable> find_all_variables(const data::function_symbol& x) { return data::find_all_variables< data::function_symbol >(x); }
      96           0 : std::set<data::variable> find_all_variables(const data::variable& x) { return data::find_all_variables< data::variable >(x); }
      97           2 : std::set<data::variable> find_all_variables(const data::variable_list& x) { return data::find_all_variables< data::variable_list >(x); }
      98     3064892 : std::set<data::variable> find_free_variables(const data::data_expression& x) { return data::find_free_variables< data::data_expression >(x); }
      99        1205 : std::set<data::variable> find_free_variables(const data::data_expression_list& x) { return data::find_free_variables< data::data_expression_list >(x); }
     100         112 : std::set<data::function_symbol> find_function_symbols(const data::data_equation& x) { return data::find_function_symbols< data::data_equation >(x); }
     101           0 : std::set<core::identifier_string> find_identifiers(const data::variable_list& x) { return data::find_identifiers< data::variable_list >(x); }
     102           4 : bool search_variable(const data::data_expression& x, const data::variable& v) { return data::search_variable< data::data_expression >(x, v); }
     103             : //--- end generated data overloads ---//
     104             : 
     105           0 : std::string pp(const std::set<variable>& x) { return data::pp< std::set<variable> >(x); }
     106             : 
     107    21756002 : sort_expression data_expression::sort() const
     108             : {
     109             :   using namespace atermpp;
     110             :   // This implementation is currently done in this class, because there
     111             :   // is no elegant solution of distributing the implementation of the
     112             :   // derived classes (as we need to support requesting the sort of a
     113             :   // data_expression we do need to provide an implementation here).
     114    21756002 :   if (is_variable(*this))
     115             :   {
     116     6047481 :     const auto& v = atermpp::down_cast<variable>(*this);
     117     6047481 :     return v.sort();
     118             :   }
     119    15708521 :   else if (is_function_symbol(*this))
     120             :   {
     121    13266371 :     const auto& f = atermpp::down_cast<function_symbol>(*this);
     122    13266371 :     return f.sort();
     123             :   }
     124     2442150 :   else if (is_abstraction(*this))
     125             :   {
     126         593 :     if (is_forall(*this) || is_exists(*this))
     127             :     {
     128         253 :       return sort_bool::bool_();
     129             :     }
     130         340 :     else if (is_lambda(*this))
     131             :     {
     132         307 :       const auto& v_variables = atermpp::down_cast<atermpp::term_list<aterm_appl> >((*this)[1]);
     133         307 :       sort_expression_vector s;
     134         623 :       for (const auto & v_variable : v_variables)
     135             :       {
     136         316 :         s.push_back(down_cast<sort_expression>(v_variable[1])); // Push the sort.
     137             :       }
     138         307 :       return function_sort(sort_expression_list(s.begin(),s.end()), atermpp::down_cast<data_expression>((*this)[2]).sort());
     139         307 :     }
     140             :     else
     141             :     {
     142          33 :       assert(is_set_comprehension(*this) || is_bag_comprehension(*this) || is_untyped_set_or_bag_comprehension(*this));
     143          33 :       const auto& v_variables  = atermpp::down_cast<atermpp::term_list<aterm_appl> >((*this)[1]);
     144          33 :       assert(v_variables.size() == 1);
     145             : 
     146          33 :       if (is_bag_comprehension(*this))
     147             :       {
     148          20 :         return container_sort(bag_container(), atermpp::down_cast<const sort_expression>(v_variables.front()[1]));
     149             :       }
     150             :       else // If it is not known whether the term is a set or a bag, it returns the type of a set, as there is
     151             :            // no setbag type. This can only occur for terms that are not propertly type checked.
     152             :       {
     153          13 :         return container_sort(set_container(), atermpp::down_cast<sort_expression>(v_variables.front()[1]));
     154             :       }
     155             :     }
     156             :   }
     157     2441557 :   else if (is_where_clause(*this))
     158             :   {
     159          50 :     return atermpp::down_cast<data_expression>((*this)[0]).sort();
     160             :   }
     161     2441507 :   else if (is_untyped_identifier(*this))
     162             :   {
     163        6990 :     return untyped_sort();
     164             :   }
     165             : 
     166     2434517 :   assert(is_application(*this));
     167     2434517 :   const auto& head = atermpp::down_cast<const data_expression>((*this)[0]);
     168     2434517 :   sort_expression s(head.sort());
     169     2434517 :   if (is_function_sort(s))
     170             :   {
     171     2434169 :     const auto& fs = atermpp::down_cast<function_sort>(s);
     172     2434169 :     assert(fs.domain().size()+1==this->size());
     173     2434169 :     return (fs.codomain());
     174             :   }
     175         348 :   return s;
     176     2434517 : }
     177             : 
     178        8723 : std::set<data::variable> substitution_variables(const mutable_map_substitution<>& sigma)
     179             : {
     180        8723 :   std::set<data::variable> result;
     181       19883 :   for (const auto& i: sigma)
     182             :   {
     183       11160 :     data::find_free_variables(i.second, std::inserter(result, result.end()));
     184             :   }
     185        8723 :   return result;
     186           0 : }
     187             : 
     188          15 : variable_list free_variables(const data_expression& x)
     189             : {
     190          15 :   std::set<variable> v = find_free_variables(x);
     191          30 :   return variable_list(v.begin(), v.end());
     192          15 : }
     193             : 
     194             : namespace detail {
     195             : 
     196         116 : sort_expression parse_sort_expression(const std::string& text)
     197             : {
     198         116 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     199         116 :   unsigned int start_symbol_index = p.start_symbol_index("SortExpr");
     200         116 :   bool partial_parses = false;
     201         116 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     202         120 :   sort_expression result = data_expression_actions(p).parse_SortExpr(node);
     203         224 :   return result;
     204         120 : }
     205             : 
     206         142 : variable_list parse_variables(const std::string& text)
     207             : {
     208         142 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     209         142 :   unsigned int start_symbol_index = p.start_symbol_index("VarSpec");
     210         142 :   bool partial_parses = false;
     211         142 :   std::string var_text("var " + text);
     212         142 :   core::parse_node node = p.parse(var_text, start_symbol_index, partial_parses);
     213         142 :   variable_list result = data_specification_actions(p).parse_VarSpec(node);
     214         284 :   return result;
     215         142 : }
     216             : 
     217         806 : data_expression parse_data_expression(const std::string& text)
     218             : {
     219         806 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     220         806 :   unsigned int start_symbol_index = p.start_symbol_index("DataExpr");
     221         806 :   bool partial_parses = false;
     222         806 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     223         806 :   core::warn_and_or(node);
     224         806 :   data_expression result = data_expression_actions(p).parse_DataExpr(node);
     225        1612 :   return result;
     226         806 : }
     227             : 
     228         158 : data_specification parse_data_specification_new(const std::string& text)
     229             : {
     230         158 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     231         158 :   unsigned int start_symbol_index = p.start_symbol_index("DataSpec");
     232         158 :   bool partial_parses = false;
     233         158 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     234         158 :   untyped_data_specification untyped_dataspec = data_specification_actions(p).parse_DataSpec(node);
     235         158 :   data_specification result = untyped_dataspec.construct_data_specification();
     236         316 :   return result;
     237         158 : }
     238             : 
     239           0 : variable_list parse_variable_declaration_list(const std::string& text)
     240             : {
     241           0 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     242           0 :   unsigned int start_symbol_index = p.start_symbol_index("VarsDeclList");
     243           0 :   bool partial_parses = false;
     244           0 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     245           0 :   variable_list result = data_specification_actions(p).parse_VarsDeclList(node);
     246           0 :   return result;
     247           0 : }
     248             : 
     249             : } // namespace detail
     250             : 
     251           1 : std::pair<basic_sort_vector, alias_vector> parse_sort_specification(const std::string& text)
     252             : {
     253           1 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     254           1 :   unsigned int start_symbol_index = p.start_symbol_index("SortSpec");
     255           1 :   bool partial_parses = false;
     256           1 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     257           1 :   std::vector<atermpp::aterm_appl> elements = detail::data_specification_actions(p).parse_SortSpec(node);
     258           1 :   basic_sort_vector sorts;
     259           1 :   alias_vector aliases;
     260          19 :   for (const atermpp::aterm_appl& x: elements)
     261             :   {
     262          18 :     if (is_basic_sort(x))
     263             :     {
     264           3 :       sorts.push_back(atermpp::down_cast<basic_sort>(x));
     265             :     }
     266          15 :     else if (is_alias(x))
     267             :     {
     268          15 :       aliases.push_back(atermpp::down_cast<alias>(x));
     269             :     }
     270             :   }
     271           1 :   auto result = std::make_pair(sorts, aliases);
     272           2 :   return result;
     273           1 : }
     274             : 
     275             : } // namespace data
     276             : 
     277             : } // namespace mcrl2
     278             :