Line data    Source code

       1             : // Author(s): Muck van Weerdenburg
       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             : #ifndef MCRL2_DATA_DETAIL_REWRITE_JITTY_H
      11             : #define MCRL2_DATA_DETAIL_REWRITE_JITTY_H
      12             : 
      13             : #include "mcrl2/data/detail/rewrite.h"
      14             : #include "mcrl2/data/detail/rewrite/rewrite_stack.h"
      15             : #include "mcrl2/data/detail/rewrite/strategy_rule.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : namespace data
      20             : {
      21             : namespace detail
      22             : {
      23             : 
      24             : struct jitty_variable_assignment_for_a_rewrite_rule
      25             : {
      26             :   const variable& var;
      27             :   const data_expression& term;
      28             :   bool variable_is_a_normal_form;
      29             : 
      30     1216980 :    jitty_variable_assignment_for_a_rewrite_rule(const variable& m_var,  const data_expression& m_term, bool m_nf)
      31     1216980 :    : var(m_var),
      32     1216980 :      term(m_term),
      33     1216980 :      variable_is_a_normal_form(m_nf)
      34     1216980 :   {}
      35             : };
      36             : 
      37             : struct jitty_assignments_for_a_rewrite_rule
      38             : {
      39             :   std::size_t size;
      40             :   jitty_variable_assignment_for_a_rewrite_rule* assignment;
      41             : 
      42      716025 :   jitty_assignments_for_a_rewrite_rule(jitty_variable_assignment_for_a_rewrite_rule* a)
      43      716025 :    : size(0),
      44      716025 :      assignment(a)
      45      716025 :   {}
      46             : 
      47             : };
      48             : 
      49             : class RewriterJitty: public Rewriter
      50             : {
      51             :   public:
      52             :     friend class jitty_argument_rewriter;
      53             : 
      54             :     typedef Rewriter::substitution_type substitution_type;
      55             : 
      56             :     RewriterJitty(const data_specification& data_spec, const used_data_equation_selector& );
      57             :     
      58             :     // The copy constructor.
      59           0 :     RewriterJitty(const RewriterJitty& other) = default;
      60             : 
      61             :     // The assignment operator.
      62             :     RewriterJitty& operator=(const RewriterJitty& other) = delete;
      63             : 
      64             :     virtual ~RewriterJitty();
      65             : 
      66             :     rewrite_strategy getStrategy();
      67             : 
      68             :     data_expression rewrite(const data_expression& term, substitution_type& sigma);
      69             : 
      70             :     void rewrite(data_expression& result, const data_expression& term, substitution_type& sigma);
      71             : 
      72           0 :     std::shared_ptr<detail::Rewriter> clone()
      73             :     {
      74           0 :       return std::shared_ptr<Rewriter>(new RewriterJitty(*this));
      75             :     }
      76             : 
      77     6109040 :     const function_symbol& this_term_is_in_normal_form() 
      78             :     {
      79     6109040 :       return this_term_is_in_normal_form_symbol;
      80             :     }
      81             : 
      82             :   protected:
      83             : 
      84             :     // A dedicated function symbol that indicates that a term is in normal form. It has name "Rewritten@@term".
      85             :     // The function symbol below is used to administrate that a term is in normal form. It is put around a term.
      86             :     // Terms with this auxiliary function symbol cannot be printed using the pretty printer for data expressions.
      87             :     function_symbol this_term_is_in_normal_form_symbol;
      88             :     bool rewriting_in_progress;
      89             : 
      90             :     class rewrite_stack m_rewrite_stack;     // Stack for intermediate rewrite results.
      91             : 
      92             :     std::vector<data_expression> rhs_for_constants_cache; // Cache that contains normal forms for constants. 
      93             :     std::map< function_symbol, data_equation_list > jitty_eqns;
      94             :     std::vector<strategy> jitty_strat;
      95             : 
      96             :     atermpp::detail::thread_aterm_pool* m_thread_aterm_pool; // Store an explicit reference to the thread aterm pool.
      97             : 
      98             : 
      99             :     template <class ITERATOR>
     100             :     void apply_cpp_code_to_higher_order_term(
     101             :                   data_expression& result,
     102             :                   const application& t,
     103             :                   const std::function<data_expression(const data_expression&)> rewrite_cpp_code,
     104             :                   ITERATOR begin,
     105             :                   ITERATOR end,
     106             :                   substitution_type& sigma);
     107             : 
     108             : 
     109             :     void rewrite_aux(data_expression& result, const data_expression& term, substitution_type& sigma);
     110             : 
     111             :     void rewrite_aux_function_symbol(
     112             :                       data_expression& result,
     113             :                       const function_symbol& op,
     114             :                       const application& term,
     115             :                       substitution_type& sigma);
     116             : 
     117             :     void rewrite_aux_const_function_symbol(
     118             :                       data_expression& result,
     119             :                       const function_symbol& op,
     120             :                       substitution_type& sigma);
     121             : 
     122             :     /// \brief Auxiliary function to take care that the array jitty_strat is sufficiently large
     123             :     ///        to access element i.
     124             :     void make_jitty_strat_sufficiently_larger(const std::size_t i);
     125             : 
     126             :     strategy create_a_cpp_function_based_strategy(const function_symbol& f, const data_specification& data_spec);
     127             :     strategy create_a_rewriting_based_strategy(const function_symbol& f, const data_equation_list& rules1);
     128             :     strategy create_strategy(const function_symbol& f, const data_equation_list& rules1, const data_specification& data_spec);
     129             :     void rebuild_strategy(const data_specification& data_spec, const mcrl2::data::used_data_equation_selector& equation_selector);
     130             : 
     131             :     data_expression remove_normal_form_function(const data_expression& t);
     132             :     void subst_values(
     133             :             data_expression& result,
     134             :             const jitty_assignments_for_a_rewrite_rule& assignments,
     135             :             const data_expression& t,
     136             :             data::enumerator_identifier_generator& generator);
     137             :      
     138        2148 :     void thread_initialise()
     139             :     {
     140        2148 :       m_thread_aterm_pool = &atermpp::detail::g_thread_term_pool();
     141        2148 :     }
     142             : };
     143             : 
     144             : /// \brief removes auxiliary expressions this_term_is_in_normal_form from data_expressions that are being rewritten.
     145             : /// \details The function below is intended to remove the auxiliary function this_term_is_in_normal_form from a term
     146             : ///          such that it can for instance be pretty printed. This auxiliary function is used internally in terms
     147             : ///          when rewriting to avoid to rewrite too often.
     148             : data_expression remove_normal_form_function(const data_expression& t);
     149             : 
     150             : } // namespace detail
     151             : } // namespace data
     152             : } // namespace mcrl2
     153             : 
     154             : #endif