From 7289e386cb24874dabaae261dbe2e20cdeb59fbe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 8 Sep 2015 16:51:32 -0700
Subject: [PATCH] feat(api/lean_expr): add lean_macro_def_eq and
 lean_macro_def_to_string

---
 src/api/expr.cpp    | 17 +++++++++++++++++
 src/api/lean_expr.h | 10 ++++++++--
 2 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/src/api/expr.cpp b/src/api/expr.cpp
index fd5d1b37ab..369ce91090 100644
--- a/src/api/expr.cpp
+++ b/src/api/expr.cpp
@@ -144,6 +144,23 @@ void lean_macro_def_del(lean_macro_def m) {
     delete to_macro_definition(m);
 }
 
+lean_bool lean_macro_def_eq(lean_macro_def m1, lean_macro_def m2, lean_bool * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(m1);
+    check_nonnull(m2);
+    *r = to_macro_definition_ref(m1) == to_macro_definition_ref(m2);
+    LEAN_CATCH;
+}
+
+lean_bool lean_macro_def_to_string(lean_macro_def m, char const ** r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(m);
+    std::ostringstream out;
+    to_macro_definition_ref(m).display(out);
+    *r = mk_string(out.str());
+    LEAN_CATCH;
+}
+
 lean_expr_kind lean_expr_get_kind(lean_expr e) {
     if (!e)
         return LEAN_EXPR_VAR;
diff --git a/src/api/lean_expr.h b/src/api/lean_expr.h
index ad820ed792..d9ead0868b 100644
--- a/src/api/lean_expr.h
+++ b/src/api/lean_expr.h
@@ -73,14 +73,20 @@ lean_bool lean_expr_mk_local_ext(lean_name n, lean_name pp_n, lean_expr t, lean_
 /** \brief Create a meta-variable (aka unification variable) with name \c n and type \c t, and store the result in \c r. */
 lean_bool lean_expr_mk_metavar(lean_name n, lean_expr t, lean_expr * r, lean_exception * ex);
 
+/** \brief Delete/dispose the given macro definition. */
+void lean_macro_def_del(lean_macro_def m);
+/** \brief Store \c lean_true in \c r iff the two given macro definitions are equal. */
+lean_bool lean_macro_def_eq(lean_macro_def m1, lean_macro_def m2, lean_bool * r, lean_exception * ex);
+/** \brief Store in \c r a (crude) string representation of the given macro definition.
+    \remark \c r must be deleted using #lean_string_del. */
+lean_bool lean_macro_def_to_string(lean_macro_def m, char const ** r, lean_exception * ex);
+
 /** \brief Store in \c r a (crude) string representation of the given expression.
     \remark \c r must be deleted using #lean_string_del.
     \remark To use the nicer pretty printer, we have an API that also takes a lean_environment object as argument. */
 lean_bool lean_expr_to_string(lean_expr e, char const ** r, lean_exception * ex);
 /** \brief Delete/dispose the given expression. */
 void lean_expr_del(lean_expr e);
-/** \brief Delete/dispose the given macro definition. */
-void lean_macro_def_del(lean_macro_def m);
 /** \brief Return the kind of the given expression.
     \remark Return LEAN_EXPR_VAR if e is null. */
 lean_expr_kind lean_expr_get_kind(lean_expr e);