expression_traits.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// 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_EXPRESSION_TRAITS_H
#define MCRL2_DATA_EXPRESSION_TRAITS_H
 
#include "mcrl2/core/term_traits.h"
#include "mcrl2/data/bool.h"
#include "mcrl2/data/exists.h"
#include "mcrl2/data/forall.h"
 
namespace mcrl2
{
 
namespace core
{
 
template <>
struct term_traits<data::data_expression>
{
  typedef data::data_expression term_type;
 
  typedef data::variable variable_type;
 
  typedef data::variable_list variable_sequence_type;
 
  static inline
  const term_type& true_()
  {
    return data::sort_bool::true_();
  }
 
  static inline
  const term_type& false_()
  {
    return data::sort_bool::false_();
  }
 
  static inline
  term_type not_(const term_type& p)
  {
    return data::sort_bool::not_(p);
  }
 
  static inline
  void make_not_(term_type& result, const term_type& p)
  {
    data::sort_bool::make_not_(result, p);
  }
 
  static inline
  term_type and_(const term_type& p, const term_type& q)
  {
    return data::sort_bool::and_(p, q);
  }
 
  static inline
  void make_and_(term_type& result, const term_type& p, const term_type& q)
  {
    data::sort_bool::make_and_(result, p, q);
  }
 
  static inline
  term_type or_(const term_type& p, const term_type& q)
  {
    return data::sort_bool::or_(p, q);
  }
 
  static inline
  void make_or_(term_type& result, const term_type& p, const term_type& q)
  {
    data::sort_bool::make_or_(result, p, q);
  }
 
  static inline
  term_type imp(const term_type& p, const term_type& q)
  {
    return data::sort_bool::implies(p, q);
  }
 
  static inline
  void make_imp(term_type& result, const term_type& p, const term_type& q)
  {
    data::sort_bool::make_implies(result, p, q);
  }
 
  static inline
  term_type forall(const variable_sequence_type& d, const term_type& p)
  {
    return data::forall(d, p);
  }
 
  static inline
  void make_forall(term_type& result, const variable_sequence_type& d, const term_type& p)
  {
    return data::make_forall(result, d, p);
  }
 
  static inline
  term_type exists(const variable_sequence_type& d, const term_type& p)
  {
    return data::exists(d, p);
  }
 
  static inline
  void make_exists(term_type& result, const variable_sequence_type& d, const term_type& p)
  {
    return data::make_exists(result, d, p);
  }
 
  static inline
  bool is_true(const term_type& t)
  {
    return t == data::sort_bool::true_();
  }
 
  static inline
  bool is_false(const term_type& t)
  {
    return t == data::sort_bool::false_();
  }
 
  static inline
  bool is_not(const term_type& t)
  {
    return data::sort_bool::is_not_application(t);
  }
 
  static inline
  bool is_and(const term_type& t)
  {
    return data::sort_bool::is_and_application(t);
  }
 
  static inline
  bool is_or(const term_type& t)
  {
    return data::sort_bool::is_or_application(t);
  }
 
  static inline
  bool is_imp(const term_type& t)
  {
    return data::sort_bool::is_implies_application(t);
  }
 
  static inline
  bool is_forall(const term_type& t)
  {
    return data::is_forall(t);
  }
 
  static inline
  bool is_exists(const term_type& t)
  {
    return data::is_exists(t);
  }
 
  static inline
  bool is_lambda(const term_type& t)
  {
    return data::is_lambda(t);
  }
 
  static inline
  const term_type& variable2term(const variable_type& v)
  {
    return v;
  }
 
  static inline
  bool is_variable(const term_type& t)
  {
    return data::is_variable(t);
  }
 
  static inline
  const term_type& argument(const term_type& t, const std::size_t n)
  {
    assert(data::is_application(t));
    const data::application& a=atermpp::down_cast<data::application>(t);
    assert(a.size()>n);
    data::application::const_iterator i=a.begin();
    for(std::size_t j=0; j<n; ++j, ++i)
    {
      assert(i!=a.end());
    }
    assert(i!=a.end());
    return *i;
  }
 
  static inline
  const term_type& left(const term_type& t)
  {
    assert(data::is_application(t));
    const data::application& a=atermpp::down_cast<data::application>(t);
    assert(a.size() == 2);
    return *(a.begin());
  }
 
  static inline
  const term_type& right(const term_type& t)
  {
    assert(data::is_application(t));
    const data::application& a=atermpp::down_cast<data::application>(t);
    assert(a.size() == 2);
    return *(++(a.begin()));
  }
 
  static inline
  const term_type& not_arg(const term_type& t)
  {
    assert(is_not(t));
    assert(data::is_application(t));
    const data::application& a=atermpp::down_cast<data::application>(t);
    assert(a.size() == 1);
    return *(a.begin());
  }
 
  static inline
  std::string pp(const term_type& t)
  {
    return data::pp(t);
  }
};
 
} // namespace core
 
namespace data
{
template < typename Expression >
struct expression_traits : public core::term_traits< Expression >
{
  // Type of expression that represents variables
  typedef mcrl2::data::variable variable_type;
 
  static bool is_true(const data_expression& e)
  {
    return sort_bool::is_true_function_symbol(e);
  }
 
  static bool is_false(const data_expression& e)
  {
    return sort_bool::is_false_function_symbol(e);
  }
 
  static bool is_application(const data_expression& e)
  {
    return data::is_application(e);
  }
 
  static bool is_abstraction(const data_expression& e)
  {
    return data::is_abstraction(e);
  }
 
  static const data_expression& head(const data_expression& e)
  {
    return atermpp::down_cast<mcrl2::data::application>(e).head();
  }
 
  static const data_expression_list& variables(const data_expression& a)
  {
    return atermpp::container_cast<data_expression_list>(atermpp::down_cast<abstraction>(a).variables());
  }
 
  static const data_expression& body(const data_expression& a)
  {
    return atermpp::down_cast<const abstraction>(a).body();
  }
 
  static data_expression replace_body(const data_expression& variable_binder, const data_expression& new_body)
  {
    const abstraction& a=atermpp::down_cast<const abstraction>(variable_binder);
    return abstraction(a.binding_operator(), a.variables(), new_body);
  }
 
  template < typename Container >
  static application application(const data_expression& e, const Container& arguments)
  {
    return application(e, arguments);
  }
 
  static const data_expression& false_()
  {
    return sort_bool::false_();
  }
 
  static const data_expression& true_()
  {
    return sort_bool::true_();
  }
 
  static data_expression and_(const data_expression& e1, const data_expression& e2)
  {
    return sort_bool::and_(e1, e2);
  }
 
  static data_expression or_(const data_expression& e1, const data_expression& e2)
  {
    return sort_bool::or_(e1, e2);
  }
};
 
} // namespace data
 
} // namespace mcrl2
 
#endif // MCRL2_DATA_EXPRESSION_TRAITS_H