fix(library/expr_lt): make sure the builtin order is AC-compatible

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/expr.cpp

@@ -26,6 +26,20 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
+unsigned add_weight(unsigned w1, unsigned w2) {
+    unsigned r = w1 + w2;
+    if (r < w1)
+        r = std::numeric_limits<unsigned>::max(); // overflow
+    return r;
+}
+
+unsigned inc_weight(unsigned w) {
+    if (w < std::numeric_limits<unsigned>::max())
+        return w+1;
+    else
+        return w;
+}
+
 static expr g_dummy(mk_var(0));
 expr::expr():expr(g_dummy) {}
 
@@ -150,9 +164,9 @@ void expr_local::dealloc(buffer<expr_cell*> & todelete) {
 
 // Composite expressions
 expr_composite::expr_composite(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv,
-                               bool has_local, bool has_param_univ, unsigned d, unsigned fv_range):
+                               bool has_local, bool has_param_univ, unsigned w, unsigned fv_range):
     expr_cell(k, h, has_expr_mv, has_univ_mv, has_local, has_param_univ),
-    m_depth(d),
+    m_weight(w),
     m_free_var_range(fv_range) {}
 
 // Expr applications
@@ -164,10 +178,10 @@ expr_app::expr_app(expr const & fn, expr const & arg):
                    fn.has_univ_metavar() || arg.has_univ_metavar(),
                    fn.has_local()        || arg.has_local(),
                    fn.has_param_univ()   || arg.has_param_univ(),
-                   std::max(get_depth(fn), get_depth(arg)) + 1,
+                   inc_weight(add_weight(get_weight(fn), get_weight(arg))),
                    std::max(get_free_var_range(fn), get_free_var_range(arg))),
     m_fn(fn), m_arg(arg) {
-    m_hash = ::lean::hash(m_hash, m_depth);
+    m_hash = ::lean::hash(m_hash, m_weight);
 }
 void expr_app::dealloc(buffer<expr_cell*> & todelete) {
     dec_ref(m_fn, todelete);
@@ -195,11 +209,11 @@ expr_binding::expr_binding(expr_kind k, name const & n, expr const & t, expr con
                    t.has_univ_metavar()   || b.has_univ_metavar(),
                    t.has_local()          || b.has_local(),
                    t.has_param_univ()     || b.has_param_univ(),
-                   std::max(get_depth(t), get_depth(b)) + 1,
+                   inc_weight(add_weight(get_weight(t), get_weight(b))),
                    std::max(get_free_var_range(t), dec(get_free_var_range(b)))),
     m_binder(n, t, i),
     m_body(b) {
-    m_hash = ::lean::hash(m_hash, m_depth);
+    m_hash = ::lean::hash(m_hash, m_weight);
     lean_assert(k == expr_kind::Lambda || k == expr_kind::Pi);
 }
 void expr_binding::dealloc(buffer<expr_cell*> & todelete) {
@@ -245,13 +259,10 @@ bool macro_definition::operator<(macro_definition const & other) const {
         return get_name() < other.get_name();
 }
 
-static unsigned max_depth(unsigned num, expr const * args) {
+static unsigned add_weight(unsigned num, expr const * args) {
     unsigned r = 0;
-    for (unsigned i = 0; i < num; i++) {
-        unsigned d = get_depth(args[i]);
-        if (d > r)
-            r = d;
-    }
+    for (unsigned i = 0; i < num; i++)
+        r = add_weight(r, get_weight(args[i]));
     return r;
 }
 
@@ -272,7 +283,7 @@ expr_macro::expr_macro(macro_definition const & m, unsigned num, expr const * ar
                    std::any_of(args, args+num, [](expr const & e) { return e.has_univ_metavar(); }),
                    std::any_of(args, args+num, [](expr const & e) { return e.has_local(); }),
                    std::any_of(args, args+num, [](expr const & e) { return e.has_param_univ(); }),
-                   max_depth(num, args) + 1,
+                   inc_weight(add_weight(num, args)),
                    get_free_var_range(num, args)),
     m_definition(m),
     m_num_args(num) {
@@ -471,14 +482,14 @@ expr mk_Type() {
 expr Prop = mk_Prop();
 expr Type = mk_Type();
 
-unsigned get_depth(expr const & e) {
+unsigned get_weight(expr const & e) {
     switch (e.kind()) {
     case expr_kind::Var:  case expr_kind::Constant: case expr_kind::Sort:
     case expr_kind::Meta: case expr_kind::Local:
         return 1;
     case expr_kind::Lambda: case expr_kind::Pi:  case expr_kind::Macro:
     case expr_kind::App:
-        return static_cast<expr_composite*>(e.raw())->m_depth;
+        return static_cast<expr_composite*>(e.raw())->m_weight;
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }

src/kernel/expr.h

@@ -200,13 +200,13 @@ public:
 /** \brief Composite expressions */
 class expr_composite : public expr_cell {
 protected:
-    unsigned m_depth;
+    unsigned m_weight;
     unsigned m_free_var_range;
-    friend unsigned get_depth(expr const & e);
+    friend unsigned get_weight(expr const & e);
     friend unsigned get_free_var_range(expr const & e);
 public:
     expr_composite(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv, bool has_local,
-                   bool has_param_univ, unsigned d, unsigned fv_range);
+                   bool has_param_univ, unsigned w, unsigned fv_range);
 };
 
 /** \brief Metavariables and local constants */
@@ -589,7 +589,7 @@ inline bool has_univ_metavar(expr const & e) { return e.has_univ_metavar(); }
 bool has_expr_metavar_strict(expr const & e);
 inline bool has_local(expr const & e) { return e.has_local(); }
 inline bool has_param_univ(expr const & e) { return e.has_param_univ(); }
-unsigned get_depth(expr const & e);
+unsigned get_weight(expr const & e);
 /**
    \brief Return \c R s.t. the de Bruijn index of all free variables
    occurring in \c e is in the interval <tt>[0, R)</tt>.

src/library/expr_lt.cpp

@@ -10,10 +10,10 @@ Author: Leonardo de Moura
 namespace lean {
 bool is_lt(expr const & a, expr const & b, bool use_hash) {
     if (is_eqp(a, b))                    return false;
-    unsigned da = get_depth(a);
-    unsigned db = get_depth(b);
-    if (da < db)                         return true;
-    if (da > db)                         return false;
+    unsigned wa = get_weight(a);
+    unsigned wb = get_weight(b);
+    if (wa < wb)                         return true;
+    if (wa > wb)                         return false;
     if (a.kind() != b.kind())            return a.kind() < b.kind();
     if (use_hash) {
         if (a.hash() < b.hash())         return true;

src/library/kernel_bindings.cpp

@@ -581,8 +581,8 @@ static int binding_info(lua_State * L) { return push_binder_info(L, binding_info
 
 static int expr_occurs(lua_State * L) { return push_boolean(L, occurs(to_expr(L, 1), to_expr(L, 2))); }
 static int expr_is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_expr(L, 1), to_expr(L, 2))); }
-static int expr_hash(lua_State * L) { return push_integer(L, to_expr(L, 1).hash()); }
-static int expr_depth(lua_State * L) { return push_integer(L, get_depth(to_expr(L, 1))); }
+static int expr_hash(lua_State * L)   { return push_integer(L, to_expr(L, 1).hash()); }
+static int expr_weight(lua_State * L) { return push_integer(L, get_weight(to_expr(L, 1))); }
 static int expr_is_lt(lua_State * L) {
     int nargs = lua_gettop(L);
     return push_boolean(L, is_lt(to_expr(L, 1), to_expr(L, 2), nargs == 3 && lua_toboolean(L, 3)));
@@ -630,7 +630,7 @@ static const struct luaL_Reg expr_m[] = {
     {"fn",               safe_function<expr_fn>},
     {"fields",           safe_function<expr_fields>},
     {"data",             safe_function<expr_fields>},
-    {"depth",            safe_function<expr_depth>},
+    {"weight",           safe_function<expr_weight>},
     {"binding_name",     safe_function<binding_name>},
     {"binding_domain",   safe_function<binding_domain>},
     {"binding_body",     safe_function<binding_body>},

src/tests/kernel/expr.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <utility>
 #include <vector>
+#include <limits>
 #include "util/test.h"
 #include "kernel/expr.h"
 #include "kernel/expr_sets.h"
@@ -68,11 +69,11 @@ static expr mk_dag(unsigned depth, bool _closed = false) {
 }
 
 static void tst2() {
-    expr r1 = mk_dag(20);
-    expr r2 = mk_dag(20);
+    expr r1 = mk_dag(40);
+    expr r2 = mk_dag(40);
     lean_assert(r1 == r2);
-    std::cout << get_depth(r1) << "\n";
-    lean_assert_eq(get_depth(r1), 41);
+    std::cout << get_weight(r1) << "\n";
+    lean_assert(get_weight(r1) == std::numeric_limits<unsigned>::max());
 }
 
 static expr mk_big(expr f, unsigned depth, unsigned val) {

tests/lua/expr3.lua

@@ -95,5 +95,5 @@ assert(a:occurs(f(a)))
 enable_expr_caching(false)
 assert(not f(a):is_eqp(f(a)))
 assert(f(a):arg():is_eqp(a))
-assert(f(a):depth() == 2)
+assert(f(a):weight() == 3)
 print(f(a):hash())

tests/lua/order.lua

@@ -0,0 +1,8 @@
+local mul = Const("mul")
+local div = Const("div")
+local z   = Const("z")
+local x   = Const("x")
+local y   = Const("y")
+local t1  = mul(z, mul(div(x, y), y))
+local t2  = mul(div(x, y), mul(z, y))
+assert(t1 < t2)