function_update.h

Go to the documentation of this file.

// Author(s): Jeroen Keiren
// 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_FUNCTION_UPDATE_H
#define MCRL2_DATA_FUNCTION_UPDATE_H
 
#include "functional"    // std::function
#include "mcrl2/utilities/exception.h"
#include "mcrl2/data/basic_sort.h"
#include "mcrl2/data/function_sort.h"
#include "mcrl2/data/function_symbol.h"
#include "mcrl2/data/application.h"
#include "mcrl2/data/data_equation.h"
#include "mcrl2/data/standard.h"
#include "mcrl2/data/bool.h"
 
namespace mcrl2 {
 
  namespace data {
 
      inline
      function_symbol_vector function_update_generate_constructors_code()
      {
        function_symbol_vector result;
        return result;
      }
      inline
      function_symbol_vector function_update_mCRL2_usable_constructors()
      {
        function_symbol_vector result;
        return result;
      }
      // The typedef is the sort that maps a function symbol to an function that rewrites it as well as a string of a function that can be used to implement it
      typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
      inline
      implementation_map function_update_cpp_implementable_constructors()
      {
        implementation_map result;
        return result;
      }
 
      inline
      const core::identifier_string& function_update_name()
      {
        static core::identifier_string function_update_name = core::identifier_string("@func_update");
        return function_update_name;
      }
 
      inline
      function_symbol function_update(const sort_expression& s, const sort_expression& t)
      {
        function_symbol function_update(function_update_name(), make_function_sort_(make_function_sort_(s, t), s, t, make_function_sort_(s, t)));
        return function_update;
      }
 
      inline
      bool is_function_update_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == function_update_name();
        }
        return false;
      }
 
      inline
      application function_update(const sort_expression& s, const sort_expression& t, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return function_update(s, t)(arg0, arg1, arg2);
      }
 
      inline
      void make_function_update(data_expression& result, const sort_expression& s, const sort_expression& t, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, function_update(s, t),arg0, arg1, arg2);
      }
 
      inline
      bool is_function_update_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_function_update_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& function_update_stable_name()
      {
        static core::identifier_string function_update_stable_name = core::identifier_string("@func_update_stable");
        return function_update_stable_name;
      }
 
      inline
      function_symbol function_update_stable(const sort_expression& s, const sort_expression& t)
      {
        function_symbol function_update_stable(function_update_stable_name(), make_function_sort_(make_function_sort_(s, t), s, t, make_function_sort_(s, t)));
        return function_update_stable;
      }
 
      inline
      bool is_function_update_stable_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == function_update_stable_name();
        }
        return false;
      }
 
      inline
      application function_update_stable(const sort_expression& s, const sort_expression& t, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return function_update_stable(s, t)(arg0, arg1, arg2);
      }
 
      inline
      void make_function_update_stable(data_expression& result, const sort_expression& s, const sort_expression& t, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, function_update_stable(s, t),arg0, arg1, arg2);
      }
 
      inline
      bool is_function_update_stable_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_function_update_stable_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& is_not_a_function_update_name()
      {
        static core::identifier_string is_not_a_function_update_name = core::identifier_string("@is_not_an_update");
        return is_not_a_function_update_name;
      }
 
      inline
      function_symbol is_not_a_function_update(const sort_expression& s, const sort_expression& t)
      {
        function_symbol is_not_a_function_update(is_not_a_function_update_name(), make_function_sort_(make_function_sort_(s, t), sort_bool::bool_()));
        return is_not_a_function_update;
      }
 
      inline
      bool is_is_not_a_function_update_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == is_not_a_function_update_name();
        }
        return false;
      }
 
      inline
      application is_not_a_function_update(const sort_expression& s, const sort_expression& t, const data_expression& arg0)
      {
        return is_not_a_function_update(s, t)(arg0);
      }
 
      inline
      void make_is_not_a_function_update(data_expression& result, const sort_expression& s, const sort_expression& t, const data_expression& arg0)
      {
        make_application(result, is_not_a_function_update(s, t),arg0);
      }
 
      inline
      bool is_is_not_a_function_update_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_is_not_a_function_update_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void is_not_a_function_update_manual_implementation(data_expression& result, const data_expression& arg0);
 
 
      inline
      void is_not_a_function_update_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==is_not_a_function_update());
        is_not_a_function_update_manual_implementation(result, a[0]);
      }
 
 
      inline
      const core::identifier_string& if_always_else_name()
      {
        static core::identifier_string if_always_else_name = core::identifier_string("@if_always_else");
        return if_always_else_name;
      }
 
      inline
      function_symbol if_always_else(const sort_expression& s, const sort_expression& t)
      {
        function_symbol if_always_else(if_always_else_name(), make_function_sort_(sort_bool::bool_(), make_function_sort_(s, t), make_function_sort_(s, t), make_function_sort_(s, t)));
        return if_always_else;
      }
 
      inline
      bool is_if_always_else_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e).name() == if_always_else_name();
        }
        return false;
      }
 
      inline
      application if_always_else(const sort_expression& s, const sort_expression& t, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return if_always_else(s, t)(arg0, arg1, arg2);
      }
 
      inline
      void make_if_always_else(data_expression& result, const sort_expression& s, const sort_expression& t, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, if_always_else(s, t),arg0, arg1, arg2);
      }
 
      inline
      bool is_if_always_else_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_if_always_else_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      void if_always_else_manual_implementation(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2);
 
 
      inline
      void if_always_else_application(data_expression& result, const data_expression& a1)
      {
        assert(is_application(a1));
        const application& a=atermpp::down_cast<application>(a1);
        // assert(a.head()==if_always_else());
        if_always_else_manual_implementation(result, a[0], a[1], a[2]);
      }
 
      inline
      function_symbol_vector function_update_generate_functions_code(const sort_expression& s, const sort_expression& t)
      {
        function_symbol_vector result;
        result.push_back(function_update(s, t));
        result.push_back(function_update_stable(s, t));
        result.push_back(is_not_a_function_update(s, t));
        result.push_back(if_always_else(s, t));
        return result;
      }
      
      inline
      function_symbol_vector function_update_generate_constructors_and_functions_code(const sort_expression& s, const sort_expression& t)
      {
        function_symbol_vector result=function_update_generate_functions_code(s, t);
        for(const function_symbol& f: function_update_generate_constructors_code())
        {
          result.push_back(f);
        }
        return result;
      }
      
      inline
      function_symbol_vector function_update_mCRL2_usable_mappings(const sort_expression& s, const sort_expression& t)
      {
        function_symbol_vector result;
        result.push_back(function_update(s, t));
        result.push_back(function_update_stable(s, t));
        result.push_back(is_not_a_function_update(s, t));
        result.push_back(if_always_else(s, t));
        return result;
      }
 
 
      // The typedef is the sort that maps a function symbol to an function that rewrites it as well as a string of a function that can be used to implement it
      typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
      inline
      implementation_map function_update_cpp_implementable_mappings(const sort_expression& s, const sort_expression& t)
      {
        implementation_map result;
        result[is_not_a_function_update(s, t)]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(is_not_a_function_update_application,"is_not_a_function_update_manual_implementation");
        result[if_always_else(s, t)]=std::pair<std::function<void(data_expression&, const data_expression&)>, std::string>(if_always_else_application,"if_always_else_manual_implementation");
        return result;
      }
      inline
      const data_expression& arg1(const data_expression& e)
      {
        assert(is_function_update_application(e) || is_function_update_stable_application(e) || is_is_not_a_function_update_application(e) || is_if_always_else_application(e));
        return atermpp::down_cast<application>(e)[0];
      }
 
      inline
      const data_expression& arg2(const data_expression& e)
      {
        assert(is_function_update_application(e) || is_function_update_stable_application(e) || is_if_always_else_application(e));
        return atermpp::down_cast<application>(e)[1];
      }
 
      inline
      const data_expression& arg3(const data_expression& e)
      {
        assert(is_function_update_application(e) || is_function_update_stable_application(e) || is_if_always_else_application(e));
        return atermpp::down_cast<application>(e)[2];
      }
 
      inline
      data_equation_vector function_update_generate_equations_code(const sort_expression& s, const sort_expression& t)
      {
        variable vx("x",s);
        variable vy("y",s);
        variable vv("v",t);
        variable vw("w",t);
        variable vf("f",make_function_sort_(s, t));
 
        data_equation_vector result;
        result.push_back(data_equation(variable_list({vf, vv, vx}), is_not_a_function_update(s, t, vf), function_update(s, t, vf, vx, vv), if_always_else(s, t, equal_to(vf(vx), vv), vf, function_update_stable(s, t, vf, vx, vv))));
        result.push_back(data_equation(variable_list({vf, vv, vw, vx}), function_update(s, t, function_update_stable(s, t, vf, vx, vw), vx, vv), if_always_else(s, t, equal_to(vf(vx), vv), vf, function_update_stable(s, t, vf, vx, vv))));
        result.push_back(data_equation(variable_list({vf, vv, vw, vx, vy}), less(vy, vx), function_update(s, t, function_update_stable(s, t, vf, vy, vw), vx, vv), function_update_stable(s, t, function_update(s, t, vf, vx, vv), vy, vw)));
        result.push_back(data_equation(variable_list({vf, vv, vw, vx, vy}), less(vx, vy), function_update(s, t, function_update_stable(s, t, vf, vy, vw), vx, vv), if_always_else(s, t, equal_to(vf(vx), vv), function_update_stable(s, t, vf, vy, vw), function_update_stable(s, t, function_update_stable(s, t, vf, vy, vw), vx, vv))));
        result.push_back(data_equation(variable_list({vf, vv, vx, vy}), not_equal_to(vx, vy), function_update_stable(s, t, vf, vx, vv)(vy), vf(vy)));
        result.push_back(data_equation(variable_list({vf, vv, vx}), function_update_stable(s, t, vf, vx, vv)(vx), vv));
        result.push_back(data_equation(variable_list({vf, vv, vx, vy}), function_update(s, t, vf, vx, vv)(vy), if_(equal_to(vx, vy), vv, vf(vy))));
        return result;
      }
 
  } // namespace data
 
} // namespace mcrl2
 
#include "mcrl2/data/detail/function_update.h" // This file contains the manual implementations of rewrite functions.
#endif // MCRL2_DATA_FUNCTION_UPDATE_H