standard.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_STANDARD_H
#define MCRL2_DATA_STANDARD_H
 
#include "mcrl2/core/detail/construction_utility.h"
#include "mcrl2/data/abstraction.h"
#include "mcrl2/data/data_equation.h"
 
 
namespace mcrl2
{
 
namespace data
{
 
// predeclare
namespace sort_bool
{
const basic_sort& bool_();
const function_symbol& false_();
const function_symbol& true_();
application and_(const data_expression&,const data_expression&);
application not_(const data_expression&);
bool is_bool(const sort_expression&);
} // namespace sort_bool
 
namespace detail
{
 
template < typename Derived >
struct symbol : public core::detail::singleton_identifier< Derived >
{
  static bool is_symbol(const core::identifier_string& e)
  {
    return e == core::detail::singleton_identifier< Derived >::instance();
  }
 
  static bool is_application(const data_expression& e)
  {
    return data::is_application(e) ? is_application(atermpp::down_cast<application>(e)) : false;
  }
 
  static bool is_application(const application& e)
  {
    return is_function_symbol(e.head());
  }
 
  static bool is_function_symbol(const data_expression& e)
  {
    return data::is_function_symbol(e) ? is_function_symbol(atermpp::down_cast<function_symbol>(e)) : false;
  }
 
  static bool is_function_symbol(const function_symbol& e)
  {
    return is_symbol(e.name());
  }
};
 
struct equal_symbol : public symbol< equal_symbol >
{
  static char const* initialise()
  {
    return "==";
  }
};
struct not_equal_symbol : public symbol< not_equal_symbol >
{
  static char const* initialise()
  {
    return "!=";
  }
};
struct if_symbol : public symbol< if_symbol >
{
  static char const* initialise()
  {
    return "if";
  }
};
struct less_symbol : public symbol< less_symbol >
{
  static char const* initialise()
  {
    return "<";
  }
};
struct less_equal_symbol : public symbol< less_equal_symbol >
{
  static char const* initialise()
  {
    return "<=";
  }
};
struct greater_symbol : public symbol< greater_symbol >
{
  static char const* initialise()
  {
    return ">";
  }
};
struct greater_equal_symbol : public symbol< greater_equal_symbol >
{
  static char const* initialise()
  {
    return ">=";
  }
};
} // namespace detail
 
inline function_symbol equal_to(const sort_expression& s)
{
  return function_symbol(detail::equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
}
 
template < typename DataExpression >
inline bool is_equal_to_function_symbol(const DataExpression& e)
{
  return detail::equal_symbol::is_function_symbol(e);
}
 
inline application equal_to(const data_expression& arg0, const data_expression& arg1)
{
  assert(arg0.sort() == arg1.sort());
  return equal_to(arg0.sort())(arg0, arg1);
}
 
template < typename DataExpression >
inline bool is_equal_to_application(const DataExpression& e)
{
  return detail::equal_symbol::is_application(e);
}
 
inline function_symbol not_equal_to(const sort_expression& s)
{
  return function_symbol(detail::not_equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
}
 
template < typename DataExpression >
inline bool is_not_equal_to_function_symbol(const DataExpression& e)
{
  return detail::not_equal_symbol::is_function_symbol(e);
}
 
inline application not_equal_to(const data_expression& arg0, const data_expression& arg1)
{
  assert(arg0.sort() == arg1.sort());
  return not_equal_to(arg0.sort())(arg0, arg1);
}
 
template < typename DataExpression >
inline bool is_not_equal_to_application(const DataExpression& e)
{
  return detail::not_equal_symbol::is_application(e);
}
 
inline function_symbol if_(const sort_expression& s)
{
  return function_symbol(detail::if_symbol::instance(), make_function_sort_(sort_bool::bool_(), s, s, s));
}
 
template < typename DataExpression >
inline bool is_if_function_symbol(const DataExpression& e)
{
  return detail::if_symbol::is_function_symbol(e);
}
 
inline application if_(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
{
  assert(sort_bool::is_bool(arg0.sort()));
  assert(arg1.sort() == arg2.sort());
 
  return if_(arg1.sort())(arg0, arg1, arg2);
}
 
template < typename DataExpression >
inline bool is_if_application(const DataExpression& e)
{
  return detail::if_symbol::is_application(e);
}
 
inline function_symbol less(const sort_expression& s)
{
  return function_symbol(detail::less_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
}
 
template < typename DataExpression >
inline bool is_less_function_symbol(const DataExpression& e)
{
  return detail::less_symbol::is_function_symbol(e);
}
 
inline application less(const data_expression& arg0, const data_expression& arg1)
{
  assert(arg0.sort() == arg1.sort());
  return less(arg0.sort())(arg0, arg1);
}
 
template < typename DataExpression >
inline bool is_less_application(const DataExpression& e)
{
  return detail::less_symbol::is_application(e);
}
 
inline function_symbol less_equal(const sort_expression& s)
{
  return function_symbol(detail::less_equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
}
 
template < typename DataExpression >
inline bool is_less_equal_function_symbol(const DataExpression& e)
{
  return detail::less_equal_symbol::is_function_symbol(e);
}
 
inline application less_equal(const data_expression& arg0, const data_expression& arg1)
{
  assert(arg0.sort() == arg1.sort());
  return less_equal(arg0.sort())(arg0, arg1);
}
 
template < typename DataExpression >
inline bool is_less_equal_application(const DataExpression& e)
{
  return detail::less_equal_symbol::is_application(e);
}
 
inline function_symbol greater(const sort_expression& s)
{
  return function_symbol(detail::greater_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
}
 
template < typename DataExpression >
inline bool is_greater_function_symbol(const DataExpression& e)
{
  return detail::greater_symbol::is_function_symbol(e);
}
 
inline application greater(const data_expression& arg0, const data_expression& arg1)
{
  assert(arg0.sort() == arg1.sort());
  return greater(arg0.sort())(arg0, arg1);
}
 
template < typename DataExpression >
inline bool is_greater_application(const DataExpression& e)
{
  return detail::greater_symbol::is_application(e);
}
 
inline function_symbol greater_equal(const sort_expression& s)
{
  return function_symbol(detail::greater_equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
}
 
template < typename DataExpression >
inline bool is_greater_equal_function_symbol(const DataExpression& e)
{
  return detail::greater_equal_symbol::is_function_symbol(e);
}
 
inline application greater_equal(const data_expression& arg0, const data_expression& arg1)
{
  assert(arg0.sort() == arg1.sort());
  return greater_equal(arg0.sort())(arg0, arg1);
}
 
template < typename DataExpression >
inline bool is_greater_equal_application(const DataExpression& e)
{
  return detail::greater_equal_symbol::is_application(e);
}
 
inline function_symbol_vector standard_generate_functions_code(const sort_expression& s)
{
  function_symbol_vector result;
  result.push_back(equal_to(s));
  result.push_back(not_equal_to(s));
  result.push_back(if_(s));
  result.push_back(less(s));
  result.push_back(less_equal(s));
  result.push_back(greater_equal(s));
  result.push_back(greater(s));
 
  return result;
}
 
inline data_equation_vector standard_generate_equations_code(const sort_expression& s)
{
  data_equation_vector result;
  variable b("b", sort_bool::bool_());
  variable x("x", s);
  variable y("y", s);
  result.push_back(data_equation(variable_list({x}), equal_to(x, x), sort_bool::true_()));
  result.push_back(data_equation(variable_list({x, y}), not_equal_to(x, y), sort_bool::not_(equal_to(x, y))));
  result.push_back(data_equation(variable_list({x, y}), if_(sort_bool::true_(), x, y), x));
  result.push_back(data_equation(variable_list({x, y}), if_(sort_bool::false_(), x, y), y));
  result.push_back(data_equation(variable_list({b, x}), if_(b, x, x), x));
  result.push_back(data_equation(variable_list({x}), less(x,x), sort_bool::false_()));
  result.push_back(data_equation(variable_list({x}), less_equal(x,x), sort_bool::true_()));
  result.push_back(data_equation(variable_list({x, y}), greater_equal(x,y), less_equal(y,x)));
  result.push_back(data_equation(variable_list({x, y}), greater(x,y), less(y,x)));
 
  // For a function sort, add the equation f==g iff forall x.f(x)==g(x). This equation is not in the Specification and Analysis of Communicating Systems of 2014.
  if (is_function_sort(s))
  {
    const function_sort& fs = atermpp::down_cast<function_sort>(s);
    variable_vector xvars,yvars;
    std::size_t index=0;
    for(const sort_expression& sort: fs.domain())
    {
      std::stringstream xs;
      xs << "x" << index;
      ++index;
      variable x(xs.str(),sort);
      xvars.push_back(x);
    }
    variable f("f",s);
    variable g("g",s);
    variable_list xvar_list=variable_list(xvars.begin(),xvars.end());
    result.push_back(data_equation(variable_list({ f, g }) + xvar_list,
                                   equal_to(f,g),
                                   abstraction(forall_binder(),xvar_list,
                                      equal_to(
                                          application(f,xvars.begin(),xvars.end()),
                                          application(g,xvars.begin(),xvars.end())))));
  }
 
  return result;
}
 
} // namespace data
} // namespace mcrl2
 
#endif // MCRL2_DATA_STANDARD_H