From 3703938e558f69d84087147e59998442d76ebc2d Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 12 Nov 2015 16:30:22 -0800 Subject: [PATCH] feat(library/abstract_expr_manager): compare exprs ignoring subsingletons --- src/frontends/lean/builtin_cmds.cpp | 42 +++++ src/frontends/lean/token_table.cpp | 2 +- src/library/CMakeLists.txt | 3 +- src/library/abstract_expr_manager.cpp | 171 ++++++++++++++++++++ src/library/abstract_expr_manager.h | 27 ++++ src/util/list_fn.h | 23 ++- tests/lean/abstract_expr1.lean | 11 ++ tests/lean/abstract_expr1.lean.expected.out | 10 ++ tests/lean/abstract_expr2.lean | 34 ++++ tests/lean/abstract_expr2.lean.expected.out | 24 +++ tests/lean/abstract_expr3.lean | 36 +++++ tests/lean/abstract_expr3.lean.expected.out | 27 ++++ 12 files changed, 407 insertions(+), 3 deletions(-) create mode 100644 src/library/abstract_expr_manager.cpp create mode 100644 src/library/abstract_expr_manager.h create mode 100644 tests/lean/abstract_expr1.lean create mode 100644 tests/lean/abstract_expr1.lean.expected.out create mode 100644 tests/lean/abstract_expr2.lean create mode 100644 tests/lean/abstract_expr2.lean.expected.out create mode 100644 tests/lean/abstract_expr3.lean create mode 100644 tests/lean/abstract_expr3.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 87937c48aa..900353b399 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 7f7613d2ea..e0a11662bf 100644 --- a/src/frontends/lean/token_table.cpp +++ b/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 aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 50ce1b8a4b..8adc13649b 100644 --- a/src/library/CMakeLists.txt +++ b/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) diff --git a/src/library/abstract_expr_manager.cpp b/src/library/abstract_expr_manager.cpp new file mode 100644 index 0000000000..ece1f2da63 --- /dev/null +++ b/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 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 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 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 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 +} + +} diff --git a/src/library/abstract_expr_manager.h b/src/library/abstract_expr_manager.h new file mode 100644 index 0000000000..83ebeb6a4f --- /dev/null +++ b/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); +}; + +} diff --git a/src/util/list_fn.h b/src/util/list_fn.h index 0fa16d8cdf..38a2514c16 100644 --- a/src/util/list_fn.h +++ b/src/util/list_fn.h @@ -282,7 +282,7 @@ void for_each(list const & l, F && f) { } /** \brief Given lists (a_0, ..., a_k) and (b_0, ..., b_k), - exec f(a_0,b_0); f(a_1,b_1); ... f(a_k,b_k). */ + exec f(a_0, b_0); f(a_1, b_1); ... f(a_k, b_k). */ template void for_each2(list const & l1, list const & l2, F && f) { static_assert(std::is_same::type, void>::value, @@ -298,6 +298,27 @@ void for_each2(list const & l1, list const & l2, F && f) { } } +/** \brief Given lists (a_0, ..., a_k), (b_0, ..., b_k), + and (c_0, ..., c_k), + exec f(a_0, b_0, c_0); f(a_1, b_1, c_1); ... f(a_k, b_k, c_k). */ +template +void for_each2(list const & l1, list const & l2, list const & l3, F && f) { + static_assert(std::is_same::type, void>::value, + "for_each2: return type of f is not void"); + typedef typename list::cell cell1; + typedef typename list::cell cell2; + typedef typename list::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 bool compare(list const & l1, list const & l2, P && p) { diff --git a/tests/lean/abstract_expr1.lean b/tests/lean/abstract_expr1.lean new file mode 100644 index 0000000000..80e3653b2b --- /dev/null +++ b/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 diff --git a/tests/lean/abstract_expr1.lean.expected.out b/tests/lean/abstract_expr1.lean.expected.out new file mode 100644 index 0000000000..a3b454b5d9 --- /dev/null +++ b/tests/lean/abstract_expr1.lean.expected.out @@ -0,0 +1,10 @@ +1 +1 +1 +3 +5 +1558663523 +3156312089 +1320171407 +1921459337 +1547633539 diff --git a/tests/lean/abstract_expr2.lean b/tests/lean/abstract_expr2.lean new file mode 100644 index 0000000000..a3f9ee50f5 --- /dev/null +++ b/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) diff --git a/tests/lean/abstract_expr2.lean.expected.out b/tests/lean/abstract_expr2.lean.expected.out new file mode 100644 index 0000000000..366f9b8350 --- /dev/null +++ b/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 diff --git a/tests/lean/abstract_expr3.lean b/tests/lean/abstract_expr3.lean new file mode 100644 index 0000000000..adee07c750 --- /dev/null +++ b/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 diff --git a/tests/lean/abstract_expr3.lean.expected.out b/tests/lean/abstract_expr3.lean.expected.out new file mode 100644 index 0000000000..ac478f8138 --- /dev/null +++ b/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