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/detail/io.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_DETAIL_IO_H
      13             : #define MCRL2_DATA_DETAIL_IO_H
      14             : 
      15             : #include "mcrl2/atermpp/algorithm.h"
      16             : #include "mcrl2/atermpp/aterm_io.h"
      17             : 
      18             : #include "mcrl2/data/index_traits.h"
      19             : 
      20             : namespace mcrl2 {
      21             : 
      22             : namespace data {
      23             : 
      24             : namespace detail {
      25             : 
      26             : // transforms DataVarId to DataVarIdNoIndex
      27             : // transforms OpId to OpIdNoIndex
      28      230995 : inline atermpp::aterm_appl remove_index_impl(const atermpp::aterm_appl& x)
      29             : {
      30      230995 :   if (x.function() == core::detail::function_symbol_OpId())
      31             :   {
      32       56358 :     return atermpp::aterm_appl(core::detail::function_symbol_OpIdNoIndex(), x.begin(), --x.end());
      33             :   }
      34      202816 :   return x;
      35             : }
      36             : 
      37             : // transforms DataVarIdNoIndex to DataVarId
      38             : // transforms OpIdNoIndex to OpId
      39      219892 : inline atermpp::aterm_appl add_index_impl(const atermpp::aterm_appl& x)
      40             : {
      41      219892 :   if (x.function() == core::detail::function_symbol_DataVarIdNoIndex())    // Obsolete. Remove in say 2025.
      42             :   {
      43           0 :     const data::variable& y = reinterpret_cast<const data::variable&>(x);
      44           0 :     return variable(y.name(), y.sort()); 
      45             :   }
      46      219892 :   else if (x.function() == core::detail::function_symbol_OpIdNoIndex())
      47             :   {
      48       27885 :     const data::function_symbol& y = reinterpret_cast<const data::function_symbol&>(x);
      49       27885 :     return function_symbol(y.name(), y.sort());
      50             :   }
      51      192007 :   return x;
      52             : }
      53             : 
      54             : inline
      55       10004 : atermpp::aterm add_index(const atermpp::aterm& x)
      56             : {
      57       10004 :   return atermpp::bottom_up_replace(x, detail::add_index_impl);
      58             : }
      59             : 
      60             : inline
      61       10004 : atermpp::aterm remove_index(const atermpp::aterm& x)
      62             : {
      63       10004 :   return atermpp::bottom_up_replace(x, detail::remove_index_impl);
      64             : }
      65             : 
      66             : } // namespace detail
      67             : 
      68             : } // namespace data
      69             : 
      70             : } // namespace mcrl2
      71             : 
      72             : #endif // MCRL2_DATA_DETAIL_IO_H