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/normalize_sorts.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_NORMALIZE_SORTS_H
      13             : #define MCRL2_DATA_NORMALIZE_SORTS_H
      14             : 
      15             : #include "mcrl2/data/builder.h"
      16             : #include "mcrl2/data/sort_specification.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace data
      22             : {
      23             : 
      24             : namespace detail
      25             : {
      26             : 
      27             : struct normalize_sorts_function
      28             : {
      29             :   using argument_type = sort_expression;
      30             :   using result_type = sort_expression;
      31             : 
      32             :   /* const sort_specification& m_sort_spec; */
      33             :   const std::map< sort_expression, sort_expression >& m_normalised_aliases;
      34             : 
      35     4767099 :   normalize_sorts_function(const sort_specification& sort_spec)
      36     4767099 :     : m_normalised_aliases(sort_spec.sort_alias_map())
      37             :   {
      38     4767099 :   }
      39             : 
      40             :   ///\brief Normalise sorts.
      41    65249475 :   sort_expression operator()(const sort_expression& e) const
      42             :   {
      43             :     // This routine takes the map m_normalised_aliases which contains pairs of sort expressions
      44             :     // <A,B> and takes all these pairs as rewrite rules, which are applied to e using an innermost
      45             :     // strategy. Note that it is assumed that m_normalised_aliases contain rewrite rules <A,B>, such
      46             :     // that B is a normal form. This allows to check that if e matches A, then we can return B.
      47             : 
      48    65249475 :     const std::map< sort_expression, sort_expression >::const_iterator i1=m_normalised_aliases.find(e);
      49    65249475 :     if (i1!=m_normalised_aliases.end())
      50             :     {
      51      793582 :       return i1->second;
      52             :     }
      53             : 
      54    64455893 :     sort_expression new_sort=e; // This will be a placeholder for the sort of which all
      55             :     // arguments will be normalised.
      56             : 
      57             :     // We do not have to do anything if e is a basic sort, as new_sort=e.
      58    64455893 :     if (is_function_sort(e))
      59             :     {
      60             :       // Rewrite the arguments into normal form.
      61    12442876 :       std::vector< sort_expression > new_domain;
      62    12442876 :       sort_expression_list e_domain(function_sort(e).domain());
      63    33912998 :       for (const sort_expression& sort: e_domain)
      64             :       {
      65    21470122 :         new_domain.push_back(this->operator()(sort));
      66             :       }
      67    12442876 :       new_sort=function_sort(new_domain, this->operator()(function_sort(e).codomain()));
      68    12442876 :     }
      69    52013017 :     else if (is_container_sort(e))
      70             :     {
      71             :       // Rewrite the argument of the container sort to normal form.
      72     2841406 :       new_sort=container_sort(
      73     2841406 :                  container_sort(e).container_name(),
      74     4262109 :                  this->operator()(container_sort(e).element_sort()));
      75             : 
      76             :     }
      77    50592314 :     else if (is_structured_sort(e))
      78             :     {
      79             :       // Rewrite the argument sorts to normal form.
      80       20781 :       std::vector< structured_sort_constructor > new_constructors;
      81       20781 :       const structured_sort_constructor_list& e_constructors(static_cast<const structured_sort&>(e).constructors());
      82       54361 :       for (const structured_sort_constructor& e_constructor: e_constructors)
      83             :       {
      84       33580 :         std::vector<structured_sort_constructor_argument> new_arguments;
      85       33580 :         const structured_sort_constructor_argument_list& i_arguments(e_constructor.arguments());
      86       56052 :         for (const structured_sort_constructor_argument& i_argument : i_arguments)
      87             :         {
      88       22472 :           new_arguments.push_back(structured_sort_constructor_argument(
      89             :                                     i_argument.name(),
      90       44944 :                                     this->operator()(i_argument.sort())));
      91             :         }
      92       33580 :         new_constructors.push_back(structured_sort_constructor(e_constructor.name(), new_arguments, e_constructor.recogniser()));
      93       33580 :       }
      94       20781 :       new_sort=structured_sort(new_constructors);
      95       20781 :     }
      96             : 
      97             :     // The arguments of new_sort are now in normal form.
      98             :     // Rewrite it to normal form.
      99    64455893 :     const std::map< sort_expression, sort_expression >::const_iterator i2=m_normalised_aliases.find(new_sort);
     100    64455893 :     if (i2!=m_normalised_aliases.end())
     101             :     {
     102        1762 :       new_sort=this->operator()(i2->second); // rewrite the result until normal form.
     103             :     }
     104    64455893 :     return new_sort;
     105    64455893 :   }
     106             : 
     107             : };
     108             : 
     109             : } // namespace detail
     110             : 
     111             : 
     112             : template <typename T>
     113         387 : void normalize_sorts(T& x,
     114             :                      const data::sort_specification& sort_spec,
     115             :                      typename std::enable_if< !std::is_base_of<atermpp::aterm, T>::value >::type* = nullptr
     116             :                     )
     117             : {
     118             :   core::make_update_apply_builder<data::sort_expression_builder>
     119         387 :   (data::detail::normalize_sorts_function(sort_spec)).update(x);
     120         387 : } 
     121             : 
     122             : template <typename T>
     123     4764828 : T normalize_sorts(const T& x,
     124             :                   const data::sort_specification& sort_spec,
     125             :                   typename std::enable_if< std::is_base_of<atermpp::aterm, T>::value >::type* = nullptr
     126             :                  )
     127             : {
     128     4764828 :   T result;
     129             :   core::make_update_apply_builder<data::sort_expression_builder>
     130     4764828 :          (data::detail::normalize_sorts_function(sort_spec)).apply(result, x);
     131     4764828 :   return result;
     132           0 : }
     133             : 
     134             : /* The functions below are defined as the function normalize_sorts
     135             :    above does not work on other sorts than sort expressions. 
     136             : 
     137             : inline sort_expression normalize_sorts(const basic_sort& x,
     138             :                                        const data::sort_specification& sort_spec)
     139             : {
     140             :   return normalize_sorts(static_cast<sort_expression>(x),sort_spec);
     141             : }
     142             : 
     143             : inline sort_expression normalize_sorts(const function_sort& x,
     144             :                                        const data::sort_specification& sort_spec)
     145             : {
     146             :   return normalize_sorts(static_cast<sort_expression>(x),sort_spec);
     147             : }
     148             : 
     149             : inline sort_expression normalize_sorts(const container_sort& x,
     150             :                                        const data::sort_specification& sort_spec)
     151             : {
     152             :   return normalize_sorts(static_cast<sort_expression>(x),sort_spec);
     153             : }
     154             : 
     155             : inline sort_expression normalize_sorts(const structured_sort& x,
     156             :                                        const data::sort_specification& sort_spec)
     157             : {
     158             :   return normalize_sorts(static_cast<sort_expression>(x),sort_spec);
     159             : }
     160             : */
     161             : 
     162             : } // namespace data
     163             : 
     164             : } // namespace mcrl2
     165             : 
     166             : #endif // MCRL2_DATA_NORMALIZE_SORTS_H