Line data    Source code

       1             : // Author(s): Maurice Laveaux
       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             : 
      10             : #include "mcrl2/data/data_io.h"
      11             : 
      12             : #include "mcrl2/atermpp/algorithm.h"
      13             : #include "mcrl2/data/data_specification.h"
      14             : 
      15             : using namespace mcrl2;
      16             : using namespace mcrl2::data;
      17             : 
      18             : static
      19        2233 : atermpp::aterm_appl remove_index_impl(const atermpp::aterm_appl& x)
      20             : {
      21        2233 :   if (x.function() == core::detail::function_symbol_OpId())
      22             :   {
      23         344 :     return atermpp::aterm_appl(core::detail::function_symbol_OpIdNoIndex(), x.begin(), --x.end());
      24             :   }
      25        2061 :   return x;
      26             : }
      27             : 
      28             : static
      29         832 : atermpp::aterm_appl add_index_impl(const atermpp::aterm_appl& x)
      30             : {
      31         832 :   if (x.function() == core::detail::function_symbol_DataVarIdNoIndex())  // Obsolete. Remove in say 2025. 
      32             :   {
      33           0 :     const data::variable& y = reinterpret_cast<const data::variable&>(x);
      34           0 :     return variable(y.name(), y.sort()); 
      35             :   }
      36         832 :   else if (x.function() == core::detail::function_symbol_OpIdNoIndex())
      37             :   {
      38          90 :     const data::function_symbol& y = reinterpret_cast<const data::function_symbol&>(x);
      39          90 :     return function_symbol(y.name(), y.sort()); 
      40             :   }
      41         742 :   return x;
      42             : }
      43             : 
      44         344 : atermpp::aterm_appl detail::data_specification_to_aterm(const data_specification& s)
      45             : {
      46             :   return atermpp::aterm_appl(core::detail::function_symbol_DataSpec(),
      47         688 :            atermpp::aterm_appl(core::detail::function_symbol_SortSpec(), atermpp::aterm_list(s.user_defined_sorts().begin(),s.user_defined_sorts().end()) +
      48         688 :                               atermpp::aterm_list(s.user_defined_aliases().begin(),s.user_defined_aliases().end())),
      49         688 :            atermpp::aterm_appl(core::detail::function_symbol_ConsSpec(), atermpp::aterm_list(s.user_defined_constructors().begin(),s.user_defined_constructors().end())),
      50         688 :            atermpp::aterm_appl(core::detail::function_symbol_MapSpec(), atermpp::aterm_list(s.user_defined_mappings().begin(),s.user_defined_mappings().end())),
      51        1032 :            atermpp::aterm_appl(core::detail::function_symbol_DataEqnSpec(), atermpp::aterm_list(s.user_defined_equations().begin(),s.user_defined_equations().end())));
      52             : }
      53             : 
      54             : inline
      55             : atermpp::aterm add_index(const atermpp::aterm& x)
      56             : {
      57             :   return atermpp::bottom_up_replace(x, add_index_impl);
      58             : }
      59             : 
      60             : inline
      61             : atermpp::aterm remove_index(const atermpp::aterm& x)
      62             : {
      63             :   return atermpp::bottom_up_replace(x, remove_index_impl);
      64             : }
      65             : 
      66          72 : atermpp::aterm_istream& data::operator>>(atermpp::aterm_istream& stream, data_specification& spec)
      67             : {
      68          72 :   atermpp::aterm_stream_state state(stream);
      69          72 :   stream >> add_index_impl;
      70             : 
      71          72 :   basic_sort_vector sorts;
      72          72 :   alias_vector aliases;
      73          72 :   function_symbol_vector constructors;
      74          72 :   function_symbol_vector user_defined_mappings;
      75          72 :   data_equation_vector user_defined_equations;
      76             : 
      77          72 :   stream >> sorts;
      78          72 :   stream >> aliases;
      79          72 :   stream >> constructors;
      80          72 :   stream >> user_defined_mappings;
      81          72 :   stream >> user_defined_equations;
      82             : 
      83             :   // Store the given information in a new data specification (to ignore existing elements of spec).
      84          72 :   spec = data_specification(sorts, aliases, constructors, user_defined_mappings, user_defined_equations);
      85             : 
      86          72 :   return stream;
      87          72 : }
      88             : 
      89          69 : atermpp::aterm_ostream& data::operator<<(atermpp::aterm_ostream& stream, const data_specification& spec)
      90             : {
      91          69 :   atermpp::aterm_stream_state state(stream);
      92          69 :   stream << remove_index_impl;
      93             : 
      94          69 :   stream << spec.user_defined_sorts();
      95          69 :   stream << spec.user_defined_aliases();
      96          69 :   stream << spec.user_defined_constructors();
      97          69 :   stream << spec.user_defined_mappings();
      98          69 :   stream << spec.user_defined_equations();
      99          69 :   return stream;
     100          69 : }