feat(library/abstract_expr_manager): compare exprs ignoring subsingletons

src/frontends/lean/builtin_cmds.cpp

@@ -43,6 +43,7 @@ Author: Leonardo de Moura
 #include "library/meng_paulson.h"
 #include "library/fun_info_manager.h"
 #include "library/congr_lemma_manager.h"
+#include "library/abstract_expr_manager.h"
 #include "library/definitional/projection.h"
 #include "library/simplifier/simp_rule_set.h"
 #include "library/blast/blast.h"
@@ -1365,6 +1366,46 @@ static environment normalizer_cmd(parser & p) {
     return env;
 }
 
+static environment abstract_expr_cmd(parser & p) {
+    unsigned o = p.parse_small_nat();
+    default_type_context ctx(p.env(), p.ios());
+    fun_info_manager fun_info(ctx);
+    abstract_expr_manager ae_manager(fun_info);
+
+    flycheck_information info(p.regular_stream());
+    if (info.enabled()) p.display_information_pos(p.cmd_pos());
+
+    expr e, a, b;
+    level_param_names ls, ls1, ls2;
+    switch (o) {
+    case 0: // weight
+        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;
+    case 2: // 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();
+}
+
 void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("open",              "create aliases for declarations, and use objects defined in other namespaces",
                         open_cmd));
@@ -1401,6 +1442,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("#decl_stats",       "(for debugging purposes) display declaration statistics", decl_stats_cmd));
     add_cmd(r, cmd_info("#relevant_thms",    "(for debugging purposes) select relevant theorems using Meng&Paulson heuristic", relevant_thms_cmd));
     add_cmd(r, cmd_info("#simplify",         "(for debugging purposes) simplify given expression", simplify_cmd));
+    add_cmd(r, cmd_info("#abstract_expr",    "(for debugging purposes) call abstract expr methods", abstract_expr_cmd));
 
     register_decl_cmds(r);
     register_inductive_cmd(r);

src/frontends/lean/token_table.cpp

@@ -121,7 +121,7 @@ void init_token_table(token_table & t) {
          "multiple_instances", "find_decl", "attribute", "persistent",
          "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
          "#compile", "#accessible", "#decl_stats", "#relevant_thms", "#simplify", "#app_builder", "#refl", "#symm",
-         "#trans", "#replace", "#congr", "#congr_simp", "#normalizer", nullptr};
+         "#trans", "#replace", "#congr", "#congr_simp", "#normalizer", "#abstract_expr", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

src/library/CMakeLists.txt

@@ -17,4 +17,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   composition_manager.cpp tc_multigraph.cpp noncomputable.cpp
   aux_recursors.cpp norm_num.cpp decl_stats.cpp meng_paulson.cpp
   norm_num.cpp class_instance_resolution.cpp type_context.cpp
-  tmp_type_context.cpp fun_info_manager.cpp congr_lemma_manager.cpp)
+  tmp_type_context.cpp fun_info_manager.cpp congr_lemma_manager.cpp
+  abstract_expr_manager.cpp)

src/library/abstract_expr_manager.cpp

@@ -0,0 +1,171 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#include "library/abstract_expr_manager.h"
+#include "util/safe_arith.h"
+
+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:
+    case expr_kind::Local:
+    case expr_kind::Meta:
+    case expr_kind::Sort:
+    case expr_kind::Var:
+    case expr_kind::Macro:        
+        return e.hash();
+    case expr_kind::Lambda:
+    case expr_kind::Pi:        
+        return ::lean::hash(hash(binding_domain(e)), hash(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 h = hash(f);
+        int i = -1;
+        for_each(f_info.get_params_info(), [&](param_info const & p_info) {
+                i++;
+                if (p_info.is_subsingleton()) return;
+                h = ::lean::hash(h, hash(args[i]));
+            });
+        return h;
+    }
+    lean_unreachable();
+}
+
+bool abstract_expr_manager::is_equal(expr const & a, expr const & b) {
+        if (is_eqp(a, b))          return true;
+        if (hash(a) != hash(b))    return false;
+        if (a.kind() != b.kind())  return false;
+        if (is_var(a))             return var_idx(a) == var_idx(b);
+        switch (a.kind()) {
+        case expr_kind::Var:
+            lean_unreachable(); // LCOV_EXCL_LINE
+        case expr_kind::Constant: case expr_kind::Sort:
+            return a == b;
+        case expr_kind::Meta: case expr_kind::Local:
+            return mlocal_name(a) == mlocal_name(b) && is_equal(mlocal_type(a), mlocal_type(b));
+        case expr_kind::Lambda: case expr_kind::Pi:
+            return is_equal(binding_domain(a), binding_domain(b)) && is_equal(binding_body(a), binding_body(b));
+        case expr_kind::Macro:
+            if (macro_def(a) != macro_def(b) || macro_num_args(a) != macro_num_args(b))
+                return false;
+            for (unsigned i = 0; i < macro_num_args(a); i++) {
+                if (!is_equal(macro_arg(a, i), macro_arg(b, i)))
+                    return false;
+            }
+            return true;
+        case expr_kind::App:
+            buffer<expr> a_args, b_args;
+            expr f_a = get_app_args(a, a_args);
+            expr f_b = get_app_args(b, b_args);
+            if (!is_equal(f_a, f_b)) return false;
+            if (a_args.size() != b_args.size()) return false;
+            fun_info f_info = m_fun_info_manager.get(f_a, a_args.size());
+            int i = -1;
+            bool not_equal = false;
+            for_each(f_info.get_params_info(), [&](param_info const & p_info) {
+                    i++;
+                    if (p_info.is_subsingleton()) return;
+                    if (!is_equal(a_args[i], b_args[i])) not_equal = true;
+                });
+            return !not_equal;
+        }
+        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

@@ -0,0 +1,27 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#pragma once
+#include "kernel/expr.h"
+#include "library/fun_info_manager.h"
+
+namespace lean {
+
+/** \brief Abstract expression manager, to allow comparing expressions while ignoring subsingletons. */
+
+class abstract_expr_manager {
+    fun_info_manager & m_fun_info_manager;
+
+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);
+};
+
+}

src/util/list_fn.h

@@ -282,7 +282,7 @@ void for_each(list<T> const & l, F && f) {
 }
 
 /** \brief Given lists <tt>(a_0, ..., a_k)</tt> and <tt>(b_0, ..., b_k)</tt>, 
-    exec f(a_0,b_0); f(a_1,b_1); ... f(a_k,b_k)</tt>. */
+    exec f(a_0, b_0); f(a_1, b_1); ... f(a_k, b_k)</tt>. */
 template<typename T1, typename T2, typename F>
 void for_each2(list<T1> const & l1, list<T2> const & l2, F && f) {
     static_assert(std::is_same<typename std::result_of<F(T1 const &, T2 const &)>::type, void>::value,
@@ -298,6 +298,27 @@ void for_each2(list<T1> const & l1, list<T2> const & l2, F && f) {
     }
 }
 
+/** \brief Given lists <tt>(a_0, ..., a_k)</tt>, <tt>(b_0, ..., b_k)</tt>, 
+    and <tt>(c_0, ..., c_k)</tt>, 
+    exec f(a_0, b_0, c_0); f(a_1, b_1, c_1); ... f(a_k, b_k, c_k)</tt>. */
+template<typename T1, typename T2, typename T3, typename F>
+void for_each2(list<T1> const & l1, list<T2> const & l2, list<T3> const & l3, F && f) {
+    static_assert(std::is_same<typename std::result_of<F(T1 const &, T2 const &, T3 const &)>::type, void>::value,
+                  "for_each2: return type of f is not void");
+    typedef typename list<T1>::cell cell1;
+    typedef typename list<T2>::cell cell2;
+    typedef typename list<T3>::cell cell3;    
+    cell1 * it1 = l1.raw();
+    cell2 * it2 = l2.raw();
+    cell3 * it3 = l3.raw();    
+    while (it1 && it2 && it3) {
+        f(it1->head(), it2->head(), it3->head());
+        it1 = it1->tail().raw();
+        it2 = it2->tail().raw();
+        it3 = it3->tail().raw();        
+    }
+}
+
 /** \brief Compare two lists using the binary predicate p. */
 template<typename T, typename P>
 bool compare(list<T> const & l1, list<T> const & l2, P && p) {

tests/lean/abstract_expr1.lean

@@ -0,0 +1,11 @@
+#abstract_expr 0 @zero
+#abstract_expr 0 ℕ
+#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

@@ -0,0 +1,10 @@
+1
+1
+1
+3
+5
+1558663523
+3156312089
+1320171407
+1921459337
+1547633539

tests/lean/abstract_expr2.lean

@@ -0,0 +1,34 @@
+universes l1 l2 l3
+constants (f : Π (X Y U : Type) (x1 x2 : X) (y1 y2 : Y) (Hx : x1 = x2) (Hy : y1 = y2), U)
+constants (X : Type.{l1}) (Y : Type.{l2}) (U : Type.{l3})
+constants (x1 x2 : X) (y1 y2 : Y) (Hx1 Hx2 : x1 = x2) (Hy1 Hy2 : y1 = y2)
+
+#abstract_expr 0 f X Y U
+#abstract_expr 0 f X Y U x1
+#abstract_expr 0 f X Y U x1 x2
+#abstract_expr 0 f X Y U x1 x2 y1
+#abstract_expr 0 f X Y U x1 x2 y1 y2
+#abstract_expr 0 f X Y U x1 x2 y1 y2 Hx1
+#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
+#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 2 (f X Y U x1 x2 y1 y2 Hx1 Hy1), (f X Y U x1 x2 y1 y2)
+
+#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

@@ -0,0 +1,24 @@
+7
+9
+11
+13
+15
+16
+17
+17
+2197106003
+2230813415
+735509793
+2462481275
+3314094375
+3314094375
+3314094375
+3314094375
+0
+0
+1
+1
+1
+0
+0
+0

tests/lean/abstract_expr3.lean

@@ -0,0 +1,36 @@
+universes l1 l2
+constants (X : Type.{l1}) (P : X → Type.{l2}) (P_ss : ∀ x, subsingleton (P x))
+constants (x1 x2 : X) (px1a px1b : P x1) (px2a px2b : P x2)
+attribute P_ss [instance]
+constants (f : Π (x1 x2 : X), P x1 → P x2 → Prop)
+
+#abstract_expr 0 f
+#abstract_expr 0 f x1
+#abstract_expr 0 f x1 x2
+#abstract_expr 0 f x1 x2 px1a
+#abstract_expr 0 f x1 x2 px1b
+#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
+#abstract_expr 1 f x1 x2
+#abstract_expr 1 f x1 x2 px1a
+#abstract_expr 1 f x1 x2 px1b
+#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

@@ -0,0 +1,27 @@
+1
+3
+5
+6
+6
+7
+7
+3779869529
+643001557
+4235699031
+4235699031
+4235699031
+4235699031
+4235699031
+0
+0
+1
+0
+1
+0
+0
+1
+1
+0
+0
+1
+0