sort_specification.h

Go to the documentation of this file.

// Author(s): Jan Friso Groote
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
//         which contains declared sorts and sort aliases.
 
#ifndef MCRL2_DATA_SORT_SPECIFICATION_H
#define MCRL2_DATA_SORT_SPECIFICATION_H
 
#include "mcrl2/data/alias.h"
#include "mcrl2/data/structured_sort.h"
 
namespace mcrl2
{
namespace data
{
 
namespace detail
{
 
  template < typename Container, typename T >
  inline
  void remove(Container& container, const T& t)
  {
    typename Container::iterator i = std::find(container.begin(), container.end(), t);
    if(i != container.end())
    {
      container.erase(i);
    }
  }
 
} // end namespace detail
 
class sort_specification;
sort_expression normalize_sorts(const sort_expression& x, const data::sort_specification& sortspec);
 
class sort_specification
{
  protected:
 
    mutable bool m_normalised_sorts_are_up_to_date;
 
    mutable bool m_normalised_data_is_up_to_date;
 
    basic_sort_vector m_user_defined_sorts;
 
    mutable std::set<sort_expression> m_normalised_sorts;
 
    std::set< sort_expression > m_sorts_in_context;
 
    alias_vector m_user_defined_aliases;
 
    mutable std::map< sort_expression, sort_expression > m_normalised_aliases;
 
  public:
 
    sort_specification()
     : m_normalised_sorts_are_up_to_date(false),
       m_normalised_data_is_up_to_date(false)
    {
      add_predefined_basic_sorts();
    }
 
    sort_specification(const basic_sort_vector& sorts, const alias_vector& aliases)
     : m_normalised_sorts_are_up_to_date(false),
       m_normalised_data_is_up_to_date(false)
    {
      add_predefined_basic_sorts();
 
      for(const basic_sort& sort: sorts)
      {
        add_sort(sort);
      }
      for(const alias& a: aliases)
      {
        add_alias(a);
      }
    }
 
 
    void add_sort(const basic_sort& s)
    {
      if (std::find(m_user_defined_sorts.begin(),m_user_defined_sorts.end(),s)==m_user_defined_sorts.end())
      {
        m_user_defined_sorts.push_back(s);
        import_system_defined_sort(s);
        sorts_are_not_necessarily_normalised_anymore();
      }
    }
 
    void add_system_defined_sort(const sort_expression& s)
    {
      import_system_defined_sort(s);
    }
 
    void add_context_sort(const sort_expression& s)
    {
      import_system_defined_sort(s);
      sorts_are_not_necessarily_normalised_anymore();
    }
 
    template <typename Container>
    void add_context_sorts(const Container& c, typename atermpp::enable_if_container<Container>::type* = nullptr)
    {
      for(typename Container::const_iterator i=c.begin(); i!=c.end(); ++i)
      {
        add_context_sort(*i);
      }
    }
 
    void remove_sort(const sort_expression& s)
    {
      detail::remove(m_user_defined_sorts,s);
      sorts_are_not_necessarily_normalised_anymore();
    }
 
    inline
    const std::set<sort_expression>& sorts() const
    {
      normalise_sort_specification_if_required();
      return m_normalised_sorts;
    }
 
    const std::set<sort_expression>& context_sorts() const
    {
      return m_sorts_in_context;
    }
 
    inline
    const basic_sort_vector& user_defined_sorts() const
    {
      return m_user_defined_sorts;
    }
 
    void add_alias(const alias& a)
    {
      if (std::find(m_user_defined_aliases.begin(),m_user_defined_aliases.end(),a)==m_user_defined_aliases.end())
      {
        m_user_defined_aliases.push_back(a);
        import_system_defined_sort(a.name());
        import_system_defined_sort(a.reference());
        sorts_are_not_necessarily_normalised_anymore();
      }
    }
 
 
    void remove_alias(const alias& a)
    {
      detail::remove(m_user_defined_sorts, a.name());
      detail::remove(m_user_defined_aliases, a);
      sorts_are_not_necessarily_normalised_anymore();
    }
 
 
    inline
    const alias_vector& user_defined_aliases() const
    {
      return m_user_defined_aliases;
    }
 
 
    const std::map< sort_expression, sort_expression >& sort_alias_map() const
    {
      normalise_sort_specification_if_required();
      return m_normalised_aliases;
    }
 
    bool operator==(const sort_specification& other) const
    {
      return m_user_defined_sorts==other.m_user_defined_sorts &&
             m_sorts_in_context == other.m_sorts_in_context &&
             m_user_defined_aliases==other.m_user_defined_aliases;
    }
 
  // Below are auxiliary functions for this class.
  protected:
    void sorts_are_not_necessarily_normalised_anymore() const
    {
      m_normalised_sorts_are_up_to_date=false;
      data_is_not_necessarily_normalised_anymore();
    }
 
    void data_is_not_necessarily_normalised_anymore() const
    {
      m_normalised_data_is_up_to_date=false;
    }
 
    void normalise_sort_specification_if_required() const
    {
      if (!m_normalised_sorts_are_up_to_date)
      {
        m_normalised_sorts_are_up_to_date=true;
        m_normalised_sorts.clear();
        reconstruct_m_normalised_aliases();
        for (const sort_expression& s: m_sorts_in_context)
        {
          m_normalised_sorts.insert(normalize_sorts(s,*this));
        }
        for (const sort_expression& s: m_user_defined_sorts)
        {
          m_normalised_sorts.insert(normalize_sorts(s,*this));
        }
        data_is_not_necessarily_normalised_anymore();
      }
    }
 
    void add_predefined_basic_sorts();
 
    template <class CONTAINER>
    void import_system_defined_sorts(const CONTAINER& sorts)
    {
      for(const sort_expression& sort: sorts)
      {
        import_system_defined_sort(sort);
      }
    }
 
    void import_system_defined_sort(const sort_expression& sort);
 
    // The function below recalculates m_normalised_aliases, such that
    // it forms a confluent terminating rewriting system using which
    // sorts can be normalised.
    void reconstruct_m_normalised_aliases() const;
 
    // The function below checks whether there is an alias loop, e.g. aliases
    // of the form A=B; B=A; or more complex A=B->C; B=Set(D); D=List(A); Loops
    // through structured sorts are allowed. If a loop is detected, an exception
    // is thrown.
    void check_for_alias_loop(
      const sort_expression& s,
      std::set<sort_expression> sorts_already_seen,
      const bool toplevel=true) const;
 
 
}
;
 
} // namespace data
 
} // namespace mcrl2
 
#endif // MCRL2_DATA_SORT_SPECIFICATION_H