From a52c9f4e2b8400dbdb4994ab6ea88ce23780a1a3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Jul 2014 09:43:16 -0700 Subject: [PATCH] feat(library/unifier): add option 'unifier.unfold_opaque', remove option 'unifier.use_exceptions' (the user should not be able to change this) Signed-off-by: Leonardo de Moura --- library/standard/bit.lean | 21 ++++++++------ src/frontends/lean/elaborator.cpp | 4 +-- src/kernel/converter.cpp | 6 ++++ src/kernel/converter.h | 2 ++ src/kernel/declaration.h | 6 ++-- src/library/module.cpp | 1 + src/library/unifier.cpp | 46 +++++++++++++++---------------- src/library/unifier.h | 17 ++++++++---- tests/lean/run/tactic23.lean | 8 ++++-- tests/lua/unify3.lua | 33 +--------------------- tests/lua/unify5.lua | 4 +-- tests/lua/unify6.lua | 3 +- tests/lua/unify7.lua | 3 +- 13 files changed, 72 insertions(+), 82 deletions(-) diff --git a/library/standard/bit.lean b/library/standard/bit.lean index 227b14496..778517d73 100644 --- a/library/standard/bit.lean +++ b/library/standard/bit.lean @@ -24,15 +24,20 @@ theorem cond_b1 {A : Type} (t e : A) : cond b1 t e = t definition bor (a b : bit) := bit_rec (bit_rec b0 b1 b) b1 a -theorem bor_b1_left (a : bit) : bor b1 a = b1 -:= refl (bor b1 a) +section + -- create section for setting temporary configuration option + set_option unifier.unfold_opaque true -theorem bor_b1_right (a : bit) : bor a b1 = b1 -:= bit_rec (refl (bor b0 b1)) (refl (bor b1 b1)) a + theorem bor_b1_left (a : bit) : bor b1 a = b1 + := refl (bor b1 a) -theorem bor_b0_left (a : bit) : bor b0 a = a -:= bit_rec (refl (bor b0 b0)) (refl (bor b0 b1)) a + theorem bor_b1_right (a : bit) : bor a b1 = b1 + := bit_rec (refl (bor b0 b1)) (refl (bor b1 b1)) a -theorem bor_b0_right (a : bit) : bor a b0 = a -:= bit_rec (refl (bor b0 b0)) (refl (bor b1 b0)) a + theorem bor_b0_left (a : bit) : bor b0 a = a + := bit_rec (refl (bor b0 b0)) (refl (bor b0 b1)) a + + theorem bor_b0_right (a : bit) : bor a b0 = a + := bit_rec (refl (bor b0 b0)) (refl (bor b1 b0)) a +end end diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index b5df409fe..c599c99e8 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -196,7 +196,7 @@ public: bool check_unassigned): m_env(env), m_ios(ios), m_plugin([](constraint const &, name_generator const &) { return lazy_list>(); }), - m_ngen(ngen), m_tc(env, m_ngen.mk_child(), mk_default_converter(m_env, optional(0))), + m_ngen(ngen), m_tc(env, m_ngen.mk_child(), mk_default_converter(m_env, true /* unfold opaque from the main module */)), m_pos_provider(pp) { m_check_unassigned = check_unassigned; m_use_local_instances = get_elaborator_local_instances(ios.get_options()); @@ -743,7 +743,7 @@ public: cs.append(m_constraints); m_constraints.clear(); return unify(m_env, cs.size(), cs.data(), m_ngen.mk_child(), m_plugin, - true, get_unifier_max_steps(m_ios.get_options())); + true, m_ios.get_options()); } void collect_metavars(expr const & e, buffer & mvars) { diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index d86e6210e..105cca3e1 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -484,4 +484,10 @@ std::unique_ptr mk_default_converter(environment const & env, optiona bool memoize, name_set const & extra_opaque) { return std::unique_ptr(new default_converter(env, mod_idx, memoize, extra_opaque)); } +std::unique_ptr mk_default_converter(environment const & env, bool unfold_opaque_main, bool memoize, name_set const & extra_opaque) { + if (unfold_opaque_main) + return mk_default_converter(env, optional(0), memoize, extra_opaque); + else + return mk_default_converter(env, optional(), memoize, extra_opaque); +} } diff --git a/src/kernel/converter.h b/src/kernel/converter.h index 1f16ca242..cd2dabe27 100644 --- a/src/kernel/converter.h +++ b/src/kernel/converter.h @@ -28,4 +28,6 @@ std::unique_ptr mk_default_converter(environment const & env, optional mod_idx = optional(), bool memoize = true, name_set const & extra_opaque = name_set()); +std::unique_ptr mk_default_converter(environment const & env, bool unfold_opaque_main, + bool memoize = true, name_set const & extra_opaque = name_set()); } diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 62bb30b19..ff65a27b3 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -22,10 +22,10 @@ namespace lean { to be transparent for any other opaque definition in module m1. */ typedef unsigned module_idx; +/** \brief The main module is the module being currently compiled. We always assigned it the index 0. */ +constexpr unsigned g_main_module_idx = 0; -/** - \brief Environment definitions, theorems, axioms and variable declarations. -*/ +/** \brief Environment definitions, theorems, axioms and variable declarations. */ class declaration { struct cell; cell * m_ptr; diff --git a/src/library/module.cpp b/src/library/module.cpp index ace7cbf62..45d3e589a 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -232,6 +232,7 @@ struct import_modules_fn { r->m_fname = fname; r->m_counter = imports.size(); r->m_module_idx = m_import_counter+1; // importate modules have idx > 0, we reserve idx 0 for new module + lean_assert(r->m_module_idx != g_main_module_idx); m_import_counter++; std::swap(r->m_obj_code, code); m_module_info.insert(mname, r); diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index ac362e564..24a754904 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -24,14 +24,10 @@ Author: Leonardo de Moura namespace lean { static name g_unifier_max_steps {"unifier", "max_steps"}; RegisterUnsignedOption(g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS, "(unifier) maximum number of steps"); -static name g_unifier_use_exceptions {"unifier", "use_exceptions"}; -RegisterBoolOption(g_unifier_use_exceptions, true, "(unifier) throw an exception when there are no more solutions"); -unsigned get_unifier_max_steps(options const & opts) { - return opts.get_unsigned(g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS); -} -bool get_unifier_use_exceptions(options const & opts) { - return opts.get_bool(g_unifier_use_exceptions, true); -} +static name g_unifier_unfold_opaque{"unifier", "unfold_opaque"}; +RegisterBoolOption(g_unifier_unfold_opaque, LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE, "(unifier) unfold opaque definitions from the current module"); +unsigned get_unifier_max_steps(options const & opts) { return opts.get_unsigned(g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS); } +bool get_unifier_unfold_opaque(options const & opts) { return opts.get_bool(g_unifier_unfold_opaque, LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE); } // If \c e is a metavariable ?m or a term of the form (?m l_1 ... l_n) where // l_1 ... l_n are distinct local variables, then return ?m, and store l_1 ... l_n in args. @@ -333,9 +329,9 @@ struct unifier_fn { unifier_fn(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, substitution const & s, unifier_plugin const & p, - bool use_exception, unsigned max_steps): + bool use_exception, unsigned max_steps, bool unfold_opaque): m_env(env), m_ngen(ngen), m_subst(s), m_plugin(p), - m_tc(env, m_ngen.mk_child(), mk_default_converter(env, optional(0))), + m_tc(env, m_ngen.mk_child(), mk_default_converter(env, unfold_opaque)), m_use_exception(use_exception), m_max_steps(max_steps), m_num_steps(0) { m_next_assumption_idx = 0; m_next_cidx = 0; @@ -1277,17 +1273,17 @@ lazy_list unify(std::shared_ptr u) { } lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - unifier_plugin const & p, bool use_exception, unsigned max_steps) { - return unify(std::make_shared(env, num_cs, cs, ngen, substitution(), p, use_exception, max_steps)); + unifier_plugin const & p, bool use_exception, unsigned max_steps, bool unfold_opaque) { + return unify(std::make_shared(env, num_cs, cs, ngen, substitution(), p, use_exception, max_steps, unfold_opaque)); } lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - unifier_plugin const & p, options const & o) { - return unify(env, num_cs, cs, ngen, p, get_unifier_use_exceptions(o), get_unifier_max_steps(o)); + unifier_plugin const & p, bool use_exception, options const & o) { + return unify(env, num_cs, cs, ngen, p, use_exception, get_unifier_max_steps(o), get_unifier_unfold_opaque(o)); } lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s, - unifier_plugin const & p, unsigned max_steps) { + unifier_plugin const & p, unsigned max_steps, bool unfold_opaque) { name_generator new_ngen(ngen); type_checker tc(env, new_ngen.mk_child()); expr _lhs = s.instantiate(lhs); @@ -1301,13 +1297,13 @@ lazy_list unify(environment const & env, expr const & lhs, expr co if (cs.empty()) { return lazy_list(s); } else { - return unify(std::make_shared(env, cs.size(), cs.data(), ngen, s, p, false, max_steps)); + return unify(std::make_shared(env, cs.size(), cs.data(), ngen, s, p, false, max_steps, unfold_opaque)); } } lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s, unifier_plugin const & p, options const & o) { - return unify(env, lhs, rhs, ngen, s, p, get_unifier_max_steps(o)); + return unify(env, lhs, rhs, ngen, s, p, get_unifier_max_steps(o), get_unifier_unfold_opaque(o)); } static int unify_simple(lua_State * L) { @@ -1368,6 +1364,7 @@ static void to_constraint_buffer(lua_State * L, int idx, buffer & cs lua_pop(L, 1); } +#if 0 static constraints to_constraints(lua_State * L, int idx) { buffer cs; to_constraint_buffer(L, idx, cs); @@ -1421,6 +1418,7 @@ static unifier_plugin to_unifier_plugin(lua_State * L, int idx) { return r; }); } +#endif static name g_tmp_prefix = name::mk_internal_unique_name(); @@ -1429,17 +1427,19 @@ static int unify(lua_State * L) { lazy_list r; environment const & env = to_environment(L, 1); if (is_expr(L, 2)) { - if (nargs == 6 && is_substitution(L, 5)) - r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), get_noop_unifier_plugin(), to_options(L, 6)); + if (nargs == 6) + r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), get_noop_unifier_plugin(), + to_options(L, 6)); else - r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), to_unifier_plugin(L, 6), to_options(L, 7)); + r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), get_noop_unifier_plugin(), + options()); } else { buffer cs; to_constraint_buffer(L, 2, cs); - if (nargs == 4 && is_options(L, 4)) - r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), get_noop_unifier_plugin(), to_options(L, 4)); + if (nargs == 4) + r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), get_noop_unifier_plugin(), false, to_options(L, 4)); else - r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_unifier_plugin(L, 4), to_options(L, 5)); + r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), get_noop_unifier_plugin(), false, options()); } return push_substitution_seq_it(L, r); } diff --git a/src/library/unifier.h b/src/library/unifier.h index 4c92f4a12..87a4f26ae 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -19,9 +19,13 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_UNIFIER_MAX_STEPS 10000 #endif +#ifndef LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE +#define LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE false +#endif + namespace lean { unsigned get_unifier_max_steps(options const & opts); -bool get_unifier_use_exceptions(options const & opts); +bool get_unifier_unfold_opaque(options const & opts); bool is_simple_meta(expr const & e); @@ -46,10 +50,13 @@ typedef std::function(constraint const &, name_generator unifier_plugin get_noop_unifier_plugin(); lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - unifier_plugin const & p = get_noop_unifier_plugin(), bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS); -lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, unifier_plugin const & p, options const & o); -lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s = substitution(), - unifier_plugin const & p = get_noop_unifier_plugin(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS); + unifier_plugin const & p = get_noop_unifier_plugin(), bool use_exception = true, + unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS, bool unfold_opaque = LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE); +lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, + unifier_plugin const & p, bool use_exception, options const & o); +lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, + substitution const & s = substitution(), unifier_plugin const & p = get_noop_unifier_plugin(), + unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS, bool unfold_opaque = LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE); lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s, unifier_plugin const & p, options const & o); diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean index 163cecb25..8e3ef3530 100644 --- a/tests/lean/run/tactic23.lean +++ b/tests/lean/run/tactic23.lean @@ -32,5 +32,9 @@ theorem T1 {p : nat → Bool} {a : nat } (H : p (a+2)) : ∃ x, p (succ x) definition is_zero (n : nat) := nat_rec true (λ n r, false) n -theorem T2 : ∃ a, (is_zero a) = true -:= by apply exists_intro; apply refl \ No newline at end of file +section + set_option unifier.unfold_opaque true + + theorem T2 : ∃ a, (is_zero a) = true + := by apply exists_intro; apply refl +end \ No newline at end of file diff --git a/tests/lua/unify3.lua b/tests/lua/unify3.lua index 572bc7068..0064a102f 100644 --- a/tests/lua/unify3.lua +++ b/tests/lua/unify3.lua @@ -13,35 +13,4 @@ local real_group = Const("real_group") local nat_group = Const("nat_group") local m = mk_metavar("m", mk_metavar("m_ty", mk_sort(mk_meta_univ("u")))) local cs = { mk_eq_cnstr(carrier(m), real) } -local o = options({"unifier", "use_exceptions"}, false) -print(o) -assert(not unify(env, cs, name_generator(), o)()) - -function hint(c, ngen) - local lhs = c:lhs() - local rhs = c:rhs() - local j = c:justification() - if lhs:is_app() and lhs:fn() == carrier and lhs:arg():is_meta() then - return - {{ mk_eq_cnstr(lhs:arg(), nat_group, j) }, -- first possible solution - { mk_eq_cnstr(lhs:arg(), real_group, j) }} - else - return nil - end -end - -function display_solutions(ss) - local n = 0 - for s in ss do - print("solution: ") - s:for_each_expr(function(n, v, j) - print(" " .. tostring(n) .. " := " .. tostring(v)) - end) - s:for_each_level(function(n, v, j) - print(" " .. tostring(n) .. " := " .. tostring(v)) - end) - n = n + 1 - end -end - -display_solutions(unify(env, cs, name_generator(), hint, o)) +assert(not unify(env, cs, name_generator())()) diff --git a/tests/lua/unify5.lua b/tests/lua/unify5.lua index 04d061f04..961ec3bf8 100644 --- a/tests/lua/unify5.lua +++ b/tests/lua/unify5.lua @@ -12,8 +12,6 @@ local m2 = mk_metavar("m2", N) local m3 = mk_metavar("m3", N) local m4 = mk_metavar("m4", N) -local o = options({"unifier", "use_exceptions"}, false) - function display_solutions(m, ss) local n = 0 for s in ss do @@ -34,4 +32,4 @@ cs = { mk_eq_cnstr(m1, f(m2, f(m3, m4))), mk_choice_cnstr(m4, function(m, e, s, ngen) return {a, b} end) } -display_solutions(m1, unify(env, cs, name_generator(), o)) +display_solutions(m1, unify(env, cs, name_generator())) diff --git a/tests/lua/unify6.lua b/tests/lua/unify6.lua index f65c577e1..cf3163ad7 100644 --- a/tests/lua/unify6.lua +++ b/tests/lua/unify6.lua @@ -3,7 +3,6 @@ local m1 = mk_meta_univ("m1") local m2 = mk_meta_univ("m2") local m3 = mk_meta_univ("m3") local l1 = mk_param_univ("l1") -local o = options({"unifier", "use_exceptions"}, false) function display_solutions(m, ss) local n = 0 @@ -24,4 +23,4 @@ cs = { mk_level_eq_cnstr(m1, max_univ(m2, max_univ(m2, l1, 1))), mk_level_eq_cnstr(m3+1, m2+1) } -display_solutions(m1, unify(env, cs, name_generator(), o)) +display_solutions(m1, unify(env, cs, name_generator())) diff --git a/tests/lua/unify7.lua b/tests/lua/unify7.lua index 9f6aae62d..2bb5e428b 100644 --- a/tests/lua/unify7.lua +++ b/tests/lua/unify7.lua @@ -10,8 +10,7 @@ print(env:infer_type(t)) local m = mk_metavar("m", mk_arrow(N, N, Type)) local cs = { mk_eq_cnstr(m(a, a), t) } -local o = options({"unifier", "use_exceptions"}, false) -ss = unify(env, cs, name_generator(), o) +ss = unify(env, cs, name_generator()) local n = 0 for s in ss do print("solution: " .. tostring(s:instantiate(m)))