rewrite.h

Go to the documentation of this file.

// Author(s): Muck van Weerdenburg
// 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)
//
 
#ifndef MCRL2_DATA_DETAIL_REWRITE_H
#define MCRL2_DATA_DETAIL_REWRITE_H
 
#include "mcrl2/data/detail/enumerator_identifier_generator.h"
#include "mcrl2/data/rewrite_strategy.h"
#include "mcrl2/data/selection.h"
#include "mcrl2/data/substitutions/mutable_indexed_substitution.h"
 
namespace mcrl2
{
namespace data
{
namespace detail
{
 
class Rewriter
{
  protected:
    enumerator_identifier_generator m_generator;  //name for variables.
 
    Rewriter& operator=(const Rewriter& other) = default;
 
    Rewriter(const Rewriter& other) = default;
 
  public:
    typedef mutable_indexed_substitution<> substitution_type;
 
    used_data_equation_selector data_equation_selector;
    Rewriter(const data_specification& data_spec, const used_data_equation_selector& eq_selector):
          data_equation_selector(eq_selector),
          m_data_specification_for_enumeration(data_spec)
    {
    }
 
    virtual ~Rewriter()
    {
    }
 
    data::enumerator_identifier_generator& identifier_generator()
    {
      return m_generator;
    }
 
    virtual rewrite_strategy getStrategy() = 0;
 
    virtual data_expression rewrite(const data_expression& term, substitution_type& sigma) = 0;
 
    virtual void rewrite(data_expression& result, const data_expression& term, substitution_type& sigma) = 0;
 
    data_expression operator() (const data_expression& term, substitution_type& sigma)
    {
      return rewrite(term,sigma);
    }
 
    virtual std::shared_ptr<detail::Rewriter> clone() = 0;
 
  public:
  /* The functions below are public, because they are used in the compiling jitty rewriter */
    void existential_quantifier_enumeration(
         data_expression& result,
         const abstraction& t,
         substitution_type& sigma);
    void existential_quantifier_enumeration(
         data_expression& result,
         const variable_list& vl,
         const data_expression& t1,
         const bool t1_is_normal_form,
         substitution_type& sigma);
 
    void universal_quantifier_enumeration(
         data_expression& result,
         const abstraction& t,
         substitution_type& sigma);
    void universal_quantifier_enumeration(
         data_expression& result,
         const variable_list& vl,
         const data_expression& t1,
         const bool t1_is_normal_form,
         substitution_type& sigma);
 
  /* The functions below exist temporarily in the transformation of the jittyc rewriter to a rewrite_stack */
  /* They ought to be removed. */
    data_expression existential_quantifier_enumeration(     // TODO: THIS SHOULD BE REMOVED IN DUE TIME. 
         const abstraction& t,
         substitution_type& sigma)
    {
      data_expression result;
      existential_quantifier_enumeration(result, t, sigma);
      return result;
    }
    data_expression existential_quantifier_enumeration(      // TODO: THIS SHOULD BE REMOVED IN DUE TIME. 
         const variable_list& vl,
         const data_expression& t1,
         const bool t1_is_normal_form,
         substitution_type& sigma)
    {
      data_expression result;
      existential_quantifier_enumeration(result, vl, t1, t1_is_normal_form, sigma);
      return result;
    }
 
    data_expression universal_quantifier_enumeration(         // TODO: THIS SHOULD BE REMOVED IN DUE TIME. 
         const abstraction& t,
         substitution_type& sigma)
    {
      data_expression result;
      universal_quantifier_enumeration(result, t, sigma);
      return result;
    }
 
    data_expression  universal_quantifier_enumeration(          // TODO: THIS SHOULD BE REMOVED IN DUE TIME. 
         const variable_list& vl,
         const data_expression& t1,
         const bool t1_is_normal_form,
         substitution_type& sigma)
    {
      data_expression result;
      universal_quantifier_enumeration(result, vl, t1, t1_is_normal_form, sigma);
      return result;
    }
 
    // Rewrite a where expression where the subdataexpressions are in internal format.
    // It yields a term without a where expression. The result is passed back in the variable result. 
    void rewrite_where(data_expression& result,
                       const where_clause& term,
                       substitution_type& sigma);
 
    data_expression rewrite_where(const where_clause& term,    // TODO: THIS SHOULD BE REMOVED IN DUE TIME. 
                                  substitution_type& sigma);
 
    // Rewrite an expression with a lambda as outermost symbol. The expression is in internal format.
    // Bound variables are replaced by new variables to avoid a clash with variables in the right hand sides
    // of sigma.
 
    void rewrite_single_lambda(
                      data_expression& result,
                      const variable_list& vl,
                      const data_expression& body,
                      const bool body_in_normal_form,
                      substitution_type& sigma);
 
    data_expression rewrite_single_lambda(                    // TODO: THIS SHOULD BE REMOVED IN DUE TIME. 
                      const variable_list& vl,
                      const data_expression& body,
                      const bool body_in_normal_form,
                      substitution_type& sigma)
    { 
      data_expression result;
      rewrite_single_lambda(result, vl, body, body_in_normal_form, sigma);
      return result;
    }
 
    void rewrite_lambda_application(
                      data_expression& result,
                      const data_expression& t,
                      substitution_type& sigma);
 
    data_expression rewrite_lambda_application(
                      const data_expression& t,
                      substitution_type& sigma);
 
    void rewrite_lambda_application(
                      data_expression& result,
                      const abstraction& lambda_term,
                      const application& t,
                      substitution_type& sigma);
 
    virtual void thread_initialise()
    {
    }
 
  protected:
 
    mcrl2::data::data_specification m_data_specification_for_enumeration;
 
    void quantifier_enumeration(
          data_expression& result,
          const variable_list& vl,
          const data_expression& t1,
          const bool t1_is_normal_form,
          substitution_type& sigma,
          const binder_type& binder,
          data_expression (*lazy_op)(const data_expression&, const data_expression&),
          const data_expression& identity_element,
          const data_expression& absorbing_element);
 
};
 
std::shared_ptr<detail::Rewriter> createRewriter(
             const data_specification& DataSpec,
             const used_data_equation_selector& equations_selector,
             const rewrite_strategy Strategy = jitty);
 
void CheckRewriteRule(const data_equation& data_eqn);
 
bool isValidRewriteRule(const data_equation& data_eqn);
 
 
// This function calculates the cumulated length of all
// potential function arguments.
inline std::size_t getArity(const data::function_symbol& op)
{
  sort_expression sort = op.sort();
  std::size_t arity = 0;
 
  while (is_function_sort(sort))
  {
    const function_sort fsort(sort);
    const sort_expression_list& sort_dom = fsort.domain();
    arity += sort_dom.size();
    sort = fsort.codomain();
  }
  return arity;
}
 
// This function calculates the number of direct function arguments.
inline std::size_t get_direct_arity(const data::function_symbol& op)
{
  sort_expression sort = op.sort();
  if (is_function_sort(sort))
  {
    return atermpp::down_cast<function_sort>(sort).domain().size();
  }
  return 0;
}
 
} // namespace detail
} // namespace data
} // namespace mcrl2
 
#endif