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

Generated by: LCOV version 1.13