Line data    Source code

       1             : // Author(s): Thomas Neele
       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             : #ifndef MCRL2_SMT_TRANSLATE_SORT_H
      10             : #define MCRL2_SMT_TRANSLATE_SORT_H
      11             : 
      12             : #include "mcrl2/data/traverser.h"
      13             : #include "mcrl2/smt/utilities.h"
      14             : 
      15             : namespace mcrl2
      16             : {
      17             : namespace smt
      18             : {
      19             : namespace detail
      20             : {
      21             : 
      22             : static inline
      23           0 : const std::map<data::structured_sort, std::string>& empty_name_map()
      24             : {
      25           0 :   static std::map<data::structured_sort, std::string> result;
      26           0 :   return result;
      27             : }
      28             : 
      29             : template <template <class> class Traverser, class OutputStream>
      30             : struct translate_sort_expression_traverser: public Traverser<translate_sort_expression_traverser<Traverser, OutputStream> >
      31             : {
      32             :   typedef Traverser<translate_sort_expression_traverser<Traverser, OutputStream> > super;
      33             :   using super::enter;
      34             :   using super::leave;
      35             :   using super::apply;
      36             : 
      37             :   OutputStream& out;
      38             :   const native_translations& m_native;
      39             :   const std::map<data::structured_sort, std::string>& m_struct_names;
      40             : 
      41           0 :   translate_sort_expression_traverser(OutputStream& out_, const native_translations& nt, const std::map<data::structured_sort, std::string>& snm)
      42           0 :     : out(out_)
      43           0 :     , m_native(nt)
      44           0 :     , m_struct_names(snm)
      45           0 :   {}
      46             : 
      47           0 :   void apply(const data::basic_sort& s)
      48             :   {
      49           0 :     auto find_result = m_native.sorts.find(s);
      50           0 :     if(find_result != m_native.sorts.end())
      51             :     {
      52           0 :       out << find_result->second;
      53           0 :       return;
      54             :     }
      55             : 
      56           0 :     out << translate_identifier(s.name());
      57             :   }
      58             : 
      59           0 :   void apply(const data::container_sort& s)
      60             :   {
      61           0 :     out << "(" << pp(s.container_name()) << " ";
      62           0 :     super::apply(s.element_sort());
      63           0 :     out << ")";
      64           0 :   }
      65             : 
      66           0 :   void apply(const data::structured_sort& s)
      67             :   {
      68           0 :     auto find_result = m_struct_names.find(s);
      69           0 :     if(find_result != m_struct_names.end())
      70             :     {
      71           0 :       out << find_result->second;
      72             :     }
      73             :     else
      74             :     {
      75           0 :       throw translation_error("Cannot translate structured sort " + pp(s));
      76             :     }
      77           0 :   }
      78             : 
      79           0 :   void apply(const data::function_sort& s)
      80             :   {
      81           0 :     throw translation_error("Cannot translate function sort " + pp(s));
      82             :   }
      83             : };
      84             : 
      85             : template <template <class> class Traverser, class OutputStream>
      86             : translate_sort_expression_traverser<Traverser, OutputStream>
      87           0 : make_translate_sort_expression_traverser(OutputStream& out, const native_translations& nt,
      88             :   const std::map<data::structured_sort, std::string>& snm)
      89             : {
      90           0 :   return translate_sort_expression_traverser<Traverser, OutputStream>(out, nt, snm);
      91             : }
      92             : 
      93             : } // namespace detail
      94             : 
      95             : template <typename T, typename OutputStream>
      96           0 : void translate_sort_expression(const T& x, OutputStream& o, const native_translations& nt,
      97             :   const std::map<data::structured_sort, std::string>& snm = detail::empty_name_map())
      98             : {
      99           0 :   detail::make_translate_sort_expression_traverser<data::sort_expression_traverser>(o, nt, snm).apply(x);
     100           0 : }
     101             : 
     102             : } // namespace smt
     103             : } // namespace mcrl2
     104             : 
     105             : #endif