feat(api): add total orders for lean_name, lean_univ and lean_expr APIs

src/api/expr.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/expr_lt.h"
 #include "api/univ.h"
 #include "api/expr.h"
 #include "api/string.h"
@@ -168,6 +169,22 @@ lean_bool lean_expr_eq(lean_expr e1, lean_expr e2, lean_bool * r, lean_exception
     LEAN_CATCH;
 }
 
+lean_bool lean_expr_lt(lean_expr e1, lean_expr e2, lean_bool * b, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(e1);
+    check_nonnull(e2);
+    *b = is_lt(to_expr_ref(e1), to_expr_ref(e2), false);
+    LEAN_CATCH;
+}
+
+lean_bool lean_expr_quick_lt(lean_expr e1, lean_expr e2, lean_bool * b, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(e1);
+    check_nonnull(e2);
+    *b = is_lt(to_expr_ref(e1), to_expr_ref(e2), true);
+    LEAN_CATCH;
+}
+
 static void check_expr_kind(lean_expr e, lean_expr_kind k, char const * msg) {
     check_nonnull(e);
     if (lean_expr_get_kind(e) != k)

src/api/lean_expr.h

@@ -86,6 +86,12 @@ void lean_macro_def_del(lean_macro_def m);
 lean_expr_kind lean_expr_get_kind(lean_expr e);
 /** \brief Store \c lean_true in \c r iff the two given expressions are equal. */
 lean_bool lean_expr_eq(lean_expr e1, lean_expr e2, lean_bool * r, lean_exception * ex);
+/** \brief Store true in \c b if \c e1 is smaller than \c e2 in the internal total order. */
+lean_bool lean_expr_lt(lean_expr e1, lean_expr e2, lean_bool * b, lean_exception * ex);
+/** \brief Store true in \c b if \c e1 is smaller than \c e2 in the internal total order.
+    Similar to #lean_expr_lt, but it is more efficient because it first compares
+    the hashcodes associated with \c e1 and \c e2. */
+lean_bool lean_expr_quick_lt(lean_expr e1, lean_expr e2, lean_bool * b, lean_exception * ex);
 
 /** \brief Store in \c i the de-Brujin index of the given variable.
     \pre lean_expr_get_kind(e) == LEAN_EXPR_VAR */

src/api/lean_name.h

@@ -44,6 +44,12 @@ lean_bool lean_name_eq(lean_name n1, lean_name n2);
 /** \brief Return the prefix of the given name.
     \pre !lean_name_is_anonymous(n)
 */
+/** \brief Return true if \c n1 is smaller than \c n2 in the internal total order. */
+lean_bool lean_name_lt(lean_name n1, lean_name n2);
+/** \brief Return true if \c n1 is smaller than \c n2 in the internal total order.
+    Similar to #lean_name_lt, but it is more efficient because it first compares
+    the hashcodes associated with \c n1 and \c n2. */
+lean_bool lean_name_quick_lt(lean_name n1, lean_name n2);
 lean_bool lean_name_get_prefix(lean_name n, lean_name * r, lean_exception * ex);
 /** \brief Store in \c r the suffix of the given name as a string.
     \pre lean_name_is_str(n)

src/api/lean_univ.h

@@ -63,6 +63,12 @@ lean_univ_kind lean_univ_get_kind(lean_univ u);
 
 /** \brief Store \c lean_true in \c r iff the two given universe object are equal. */
 lean_bool lean_univ_eq(lean_univ u1, lean_univ u2, lean_bool * r, lean_exception * ex);
+/** \brief Store true in \c b if \c u1 is smaller than \c u2 in the internal total order. */
+lean_bool lean_univ_lt(lean_univ u1, lean_univ u2, lean_bool * b, lean_exception * ex);
+/** \brief Store true in \c b if \c u1 is smaller than \c u2 in the internal total order.
+    Similar to #lean_univ_lt, but it is more efficient because it first compares
+    the hashcodes associated with \c u1 and \c u2. */
+lean_bool lean_univ_quick_lt(lean_univ u1, lean_univ u2, lean_bool * b, lean_exception * ex);
 /** \brief If \c r contains \c lean_true, then forall assignments \c A that assigns all parameters,
     globals and metavariables occuring in \c u1 and \c u2, we have that the
     universe level u1[A] is bigger or equal to u2[A]. */

src/api/name.cpp

@@ -63,6 +63,14 @@ lean_bool lean_name_eq(lean_name n1, lean_name n2) {
     return n1 && n2 && to_name_ref(n1) == to_name_ref(n2);
 }
 
+lean_bool lean_name_lt(lean_name n1, lean_name n2) {
+    return n1 && n2 && cmp(to_name_ref(n1), to_name_ref(n2)) < 0;
+}
+
+lean_bool lean_name_quick_lt(lean_name n1, lean_name n2) {
+    return n1 && n2 && quick_cmp(to_name_ref(n1), to_name_ref(n2)) < 0;
+}
+
 lean_bool lean_name_get_prefix(lean_name n, lean_name * r, lean_exception * ex) {
     LEAN_TRY;
     check_nonnull(n);

src/api/univ.cpp

@@ -117,6 +117,22 @@ lean_bool lean_univ_eq(lean_univ u1, lean_univ u2, lean_bool * r, lean_exception
     LEAN_CATCH;
 }
 
+lean_bool lean_univ_lt(lean_univ u1, lean_univ u2, lean_bool * b, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(u1);
+    check_nonnull(u2);
+    *b = is_lt(to_level_ref(u1), to_level_ref(u2), false);
+    LEAN_CATCH;
+}
+
+lean_bool lean_univ_quick_lt(lean_univ u1, lean_univ u2, lean_bool * b, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(u1);
+    check_nonnull(u2);
+    *b = is_lt(to_level_ref(u1), to_level_ref(u2), true);
+    LEAN_CATCH;
+}
+
 lean_bool lean_univ_geq(lean_univ u1, lean_univ u2, lean_bool * r, lean_exception * ex) {
     LEAN_TRY;
     check_nonnull(u1);