fix(library/abstract_expr_manager): remove weight and lt

src/frontends/lean/builtin_cmds.cpp

@@ -1377,31 +1377,18 @@ static environment abstract_expr_cmd(parser & p) {
 
     expr e, a, b;
     level_param_names ls, ls1, ls2;
-    switch (o) {
+    if (o == 0) {
-    case 0: // weight
+        // hash
-        if (info.enabled()) p.regular_stream() << "abstract weight: " << endl;
-        std::tie(e, ls) = parse_local_expr(p);
-        p.regular_stream() << ae_manager.get_weight(e) << endl;
-        break;
-    case 1: // hash
         if (info.enabled()) p.regular_stream() << "abstract hash: " << endl;
         std::tie(e, ls) = parse_local_expr(p);
         p.regular_stream() << ae_manager.hash(e) << endl;
-        break;
+    } else {
-    case 2: // is_equal
+        // is_equal
         if (info.enabled()) p.regular_stream() << "abstract is_equal: " << endl;
         std::tie(a, ls1) = parse_local_expr(p);
         p.check_token_next(get_comma_tk(), "invalid #abstract_expr command, ',' expected");
         std::tie(b, ls2) = parse_local_expr(p);
         p.regular_stream() << ae_manager.is_equal(a, b) << endl;
-        break;
-    case 3: // is_lt
-        if (info.enabled()) p.regular_stream() << "abstract is_equal: " << endl;
-        std::tie(a, ls1) = parse_local_expr(p);
-        p.check_token_next(get_comma_tk(), "invalid #abstract_expr command, ',' expected");
-        std::tie(b, ls2) = parse_local_expr(p);
-        p.regular_stream() << ae_manager.is_lt(a, b) << endl;
-        break;
     }
     return p.env();
 }

src/library/abstract_expr_manager.cpp

@@ -9,36 +9,6 @@ Author: Daniel Selsam
 
 namespace lean {
 
-unsigned abstract_expr_manager::get_weight(expr const & e) {
-    switch (e.kind()) {
-    case expr_kind::Constant:
-    case expr_kind::Local:
-    case expr_kind::Meta:
-    case expr_kind::Sort:
-    case expr_kind::Var:
-    case expr_kind::Macro:
-        return ::lean::get_weight(e);
-    case expr_kind::Lambda:
-    case expr_kind::Pi:
-        return safe_add(1, safe_add(get_weight(binding_domain(e)), get_weight(binding_body(e))));
-    case expr_kind::App:
-        buffer<expr> args;
-        expr f = get_app_args(e, args);
-        fun_info f_info = m_fun_info_manager.get(f, args.size());
-        unsigned w = get_weight(f);
-        unsigned one = 1;
-        int i = -1;
-        for_each(f_info.get_params_info(), [&](param_info const & p_info) {
-                i++;
-                w = safe_add(w, one);
-                if (p_info.is_subsingleton()) return;
-                w = safe_add(w, get_weight(args[i]));
-            });
-        return w;
-    }
-    lean_unreachable();
-}
-
 unsigned abstract_expr_manager::hash(expr const & e) {
     switch (e.kind()) {
     case expr_kind::Constant:
@@ -108,65 +78,4 @@ bool abstract_expr_manager::is_equal(expr const & a, expr const & b) {
         lean_unreachable(); // LCOV_EXCL_LINE
 }
 
-bool abstract_expr_manager::is_lt(expr const & a, expr const & b) {
-    if (is_eqp(a, b))                    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 (is_equal(a, b))                  return false;
-    switch (a.kind()) {
-    case expr_kind::Var:
-    case expr_kind::Constant:
-    case expr_kind::Sort:
-        return a < b;
-    case expr_kind::Local: case expr_kind::Meta:
-        if (mlocal_name(a) != mlocal_name(b))
-            return mlocal_name(a) < mlocal_name(b);
-        else
-            return is_lt(mlocal_type(a), mlocal_type(b));
-    case expr_kind::Lambda: case expr_kind::Pi:
-        if (!is_equal(binding_domain(a), binding_domain(b)))
-            return is_lt(binding_domain(a), binding_domain(b));
-        else
-            return is_lt(binding_body(a), binding_body(b));
-    case expr_kind::Macro:
-        if (macro_def(a) != macro_def(b))
-            return macro_def(a) < macro_def(b);
-        if (macro_num_args(a) != macro_num_args(b))
-            return macro_num_args(a) < macro_num_args(b);
-        for (unsigned i = 0; i < macro_num_args(a); i++) {
-            if (!is_equal(macro_arg(a, i), macro_arg(b, i)))
-                return is_lt(macro_arg(a, i), macro_arg(b, i));
-        }
-        return false;
-    case expr_kind::App:
-        list<expr> a_args, b_args;
-        expr f_a = a;
-        expr f_b = b;
-        while (is_app(f_a) && is_app(f_b)) {
-            a_args = cons(app_arg(f_a), a_args);
-            b_args = cons(app_arg(f_b), b_args);
-            f_a = app_fn(f_a);
-            f_b = app_fn(f_b);
-        }
-        if (!is_equal(f_a, f_b)) return is_lt(f_a, f_b);
-        fun_info f_info = m_fun_info_manager.get(f_a, length(a_args));
-        bool lt = false;
-        bool gt = false;
-        for_each3(f_info.get_params_info(), a_args, b_args,
-                  [&](param_info const & p_info, expr const & a_arg, expr const & b_arg) {
-                if (lt || gt) return;
-                if (p_info.is_subsingleton()) return;
-                if (!is_equal(a_arg, b_arg)) {
-                    if (is_lt(a_arg, b_arg)) lt = true;
-                    else gt = true;
-                }
-            });
-        return lt;
-    }
-    lean_unreachable(); // LCOV_EXCL_LINE
-}
-
 }

src/library/abstract_expr_manager.h

@@ -18,10 +18,8 @@ public:
     abstract_expr_manager(fun_info_manager & f_info_manager):
         m_fun_info_manager(f_info_manager) { }
 
-    unsigned get_weight(expr const & e);
     unsigned hash(expr const & e);
     bool is_equal(expr const & a, expr const & b);
-    bool is_lt(expr const & a, expr const & b);
 };
 
 }

tests/lean/abstract_expr1.lean

@@ -3,9 +3,3 @@
 #abstract_expr 0 nat_has_zero
 #abstract_expr 0 @zero ℕ
 #abstract_expr 0 @zero ℕ nat_has_zero
-
-#abstract_expr 1 @zero
-#abstract_expr 1 ℕ
-#abstract_expr 1 nat_has_zero
-#abstract_expr 1 @zero ℕ
-#abstract_expr 1 @zero ℕ nat_has_zero

tests/lean/abstract_expr1.lean.expected.out

@@ -1,8 +1,3 @@
-1
-1
-1
-3
-5
 1558663523
 3156312089
 1320171407

tests/lean/abstract_expr2.lean

@@ -12,23 +12,8 @@ constants (x1 x2 : X) (y1 y2 : Y) (Hx1 Hx2 : x1 = x2) (Hy1 Hy2 : y1 = y2)
 #abstract_expr 0 f X Y U x1 x2 y1 y2 Hx1 Hy1
 #abstract_expr 0 f X Y U x1 x2 y1 y2 Hx2 Hy2
 
-#abstract_expr 1 f X Y U
+#abstract_expr 1 (f X Y U x1 x2 y1 y2), (f X Y U x1 x2 y1 y2 Hx2 Hy2)
-#abstract_expr 1 f X Y U x1
+#abstract_expr 1 (f X Y U x1 x2 y1 y2 Hx1 Hy1), (f X Y U x1 x2 y1 y2)
-#abstract_expr 1 f X Y U x1 x2
-#abstract_expr 1 f X Y U x1 x2 y1
-#abstract_expr 1 f X Y U x1 x2 y1 y2
-#abstract_expr 1 f X Y U x1 x2 y1 y2 Hx1
-#abstract_expr 1 f X Y U x1 x2 y1 y2 Hx1 Hy1
-#abstract_expr 1 f X Y U x1 x2 y1 y2 Hx2 Hy2
 
-#abstract_expr 2 (f X Y U x1 x2 y1 y2), (f X Y U x1 x2 y1 y2 Hx2 Hy2)
+#abstract_expr 1 (f X Y U x1 x2 y1 y2 Hx1), (f X Y U x1 x2 y1 y2 Hx2)
-#abstract_expr 2 (f X Y U x1 x2 y1 y2 Hx1 Hy1), (f X Y U x1 x2 y1 y2)
+#abstract_expr 1 (f X Y U x1 x2 y1 y2 Hx1 Hy1), (f X Y U x1 x2 y1 y2 Hx2 Hy2)
-
-#abstract_expr 2 (f X Y U x1 x2 y1 y2 Hx1), (f X Y U x1 x2 y1 y2 Hx2)
-#abstract_expr 2 (f X Y U x1 x2 y1 y2 Hx1 Hy1), (f X Y U x1 x2 y1 y2 Hx2 Hy2)
-
-#abstract_expr 3 (f X Y U x1 x2 y1 y2), (f X Y U x1 x2 y1 y2 Hx2 Hy2)
-#abstract_expr 3 (f X Y U x1 x2 y1 y2 Hx1 Hy1), (f X Y U x1 x2 y1 y2)
-
-#abstract_expr 3 (f X Y U x1 x2 y1 y2 Hx1), (f X Y U x1 x2 y1 y2 Hx2)
-#abstract_expr 3 (f X Y U x1 x2 y1 y2 Hx1 Hy1), (f X Y U x1 x2 y1 y2 Hx2 Hy2)

tests/lean/abstract_expr2.lean.expected.out

@@ -1,11 +1,3 @@
-7
-9
-11
-13
-15
-16
-17
-17
 2197106003
 2230813415
 735509793
@@ -18,7 +10,3 @@
 0
 1
 1
-1
-0
-0
-0

tests/lean/abstract_expr3.lean

@@ -12,25 +12,8 @@ constants (f : Π (x1 x2 : X), P x1 → P x2 → Prop)
 #abstract_expr 0 f x1 x2 px1a px2a
 #abstract_expr 0 f x1 x2 px1a px2b
 
-#abstract_expr 1 f
+#abstract_expr 1 f x1 x2, f x2 x1
-#abstract_expr 1 f x1
+#abstract_expr 1 f x1 x2, f x1 x2 px1a
-#abstract_expr 1 f x1 x2
+#abstract_expr 1 f x1 x2 px1a, f x1 x2 px1b
-#abstract_expr 1 f x1 x2 px1a
+#abstract_expr 1 f x1 x2 px1a px2a, f x1 x2 px1b
-#abstract_expr 1 f x1 x2 px1b
+#abstract_expr 1 f x1 x2 px1a px2a, f x1 x2 px1b px2b
-#abstract_expr 1 f x1 x2 px1a px2a
-#abstract_expr 1 f x1 x2 px1a px2b
-
-#abstract_expr 2 f x1 x2, f x2 x1
-#abstract_expr 2 f x1 x2, f x1 x2 px1a
-#abstract_expr 2 f x1 x2 px1a, f x1 x2 px1b
-#abstract_expr 2 f x1 x2 px1a px2a, f x1 x2 px1b
-#abstract_expr 2 f x1 x2 px1a px2a, f x1 x2 px1b px2b
-
-#abstract_expr 3 f x1, f x1
-#abstract_expr 3 f x1 x2, f x2 x1
-#abstract_expr 3 f x2 x1, f x1 x2
-#abstract_expr 3 f x1 x2, f x1 x2 px1a
-#abstract_expr 3 f x1 x2 px1a, f x1 x2 px1b
-#abstract_expr 3 f x1 x2 px1a px2a, f x1 x2 px1b
-#abstract_expr 3 f x1 x2 px1a, f x1 x2 px1b px2b
-#abstract_expr 3 f x1 x2 px1a px2a, f x1 x2 px1b px2b

tests/lean/abstract_expr3.lean.expected.out

@@ -1,10 +1,3 @@
-1
-3
-5
-6
-6
-7
-7
 3779869529
 643001557
 4235699031
@@ -17,11 +10,3 @@
 1
 0
 1
-0
-0
-1
-1
-0
-0
-1
-0