From e1bc0a68e69784961ef703fdb8085eda0027aee9 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Fri, 24 Jun 2016 10:36:06 -0700 Subject: [PATCH] refactor(simplifier): port skeleton to new tactic framework Conflicts: library/init/meta/tactic.lean src/library/tactic/tactic_state.cpp --- library/init/meta/tactic.lean | 30 + src/CMakeLists.txt | 4 +- src/frontends/lean/old_attributes.cpp | 16 - src/frontends/lean/print_cmd.cpp | 19 +- src/library/CMakeLists.txt | 2 +- src/library/app_builder.cpp | 2 +- .../blast/actions/by_contradiction_action.cpp | 2 +- .../blast/backward/backward_lemmas.cpp | 14 +- src/library/blast/blast.cpp | 48 +- src/library/blast/blast.h | 22 +- src/library/blast/congruence_closure.cpp | 2 +- src/library/blast/forward/ematch.cpp | 2 +- src/library/blast/forward/pattern.cpp | 16 +- src/library/blast/forward/pattern.h | 2 +- .../blast/grinder/intro_elim_lemmas.cpp | 8 +- src/library/blast/simplifier/CMakeLists.txt | 2 - src/library/blast/simplifier/simplifier.cpp | 1216 ----------------- .../blast/simplifier/simplifier_actions.cpp | 149 -- .../blast/simplifier/simplifier_actions.h | 18 - .../simplifier/simplifier_strategies.cpp | 71 - .../blast/simplifier/simplifier_strategies.h | 15 - src/library/local_context.cpp | 12 +- .../old_tactic/tactic/norm_num_tactic.cpp | 4 +- ...e_context.cpp => old_tmp_type_context.cpp} | 38 +- ..._type_context.h => old_tmp_type_context.h} | 22 +- .../defeq_simplifier/defeq_simp_lemmas.cpp | 10 +- src/library/tactic/init_module.cpp | 3 + src/library/tactic/simplifier/CMakeLists.txt | 1 + .../{blast => tactic}/simplifier/ceqv.cpp | 26 +- .../{blast => tactic}/simplifier/ceqv.h | 6 +- .../simplifier/init_module.cpp | 10 +- .../simplifier/init_module.h | 2 - .../simplifier/simp_lemmas.cpp | 225 ++- .../simplifier/simp_lemmas.h | 27 +- src/library/tactic/simplifier/simplifier.cpp | 807 +++++++++++ .../{blast => tactic}/simplifier/simplifier.h | 27 +- src/library/tactic/tactic_state.cpp | 1 + src/library/type_context.cpp | 52 +- src/library/type_context.h | 19 + tests/lean/congr_print.lean.expected.out | 2 +- tests/lean/run/simp1.lean | 8 + tests/lean/run/simp2.lean | 13 + tests/lean/run/simp3.lean | 9 + tests/lean/rw_set2.lean.expected.out | 51 + 44 files changed, 1251 insertions(+), 1784 deletions(-) delete mode 100644 src/library/blast/simplifier/CMakeLists.txt delete mode 100644 src/library/blast/simplifier/simplifier.cpp delete mode 100644 src/library/blast/simplifier/simplifier_actions.cpp delete mode 100644 src/library/blast/simplifier/simplifier_actions.h delete mode 100644 src/library/blast/simplifier/simplifier_strategies.cpp delete mode 100644 src/library/blast/simplifier/simplifier_strategies.h rename src/library/{tmp_type_context.cpp => old_tmp_type_context.cpp} (75%) rename src/library/{tmp_type_context.h => old_tmp_type_context.h} (81%) create mode 100644 src/library/tactic/simplifier/CMakeLists.txt rename src/library/{blast => tactic}/simplifier/ceqv.cpp (91%) rename src/library/{blast => tactic}/simplifier/ceqv.h (77%) rename src/library/{blast => tactic}/simplifier/init_module.cpp (59%) rename src/library/{blast => tactic}/simplifier/init_module.h (92%) rename src/library/{blast => tactic}/simplifier/simp_lemmas.cpp (80%) rename src/library/{blast => tactic}/simplifier/simp_lemmas.h (87%) create mode 100644 src/library/tactic/simplifier/simplifier.cpp rename src/library/{blast => tactic}/simplifier/simplifier.h (51%) create mode 100644 tests/lean/run/simp1.lean create mode 100644 tests/lean/run/simp2.lean create mode 100644 tests/lean/run/simp3.lean diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index bada915132..b944cf985f 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -94,6 +94,7 @@ meta_constant unify_core : expr → expr → transparency → tactic unit /- Infer the type of the given expression. Remark: transparency does not affect type inference -/ meta_constant infer_type : expr → tactic expr + meta_constant get_local : name → tactic expr /- Return the hypothesis in the main goal. Fail if tactic_state does not have any goal left. -/ meta_constant local_context : tactic (list expr) @@ -133,6 +134,11 @@ meta_constant mk_instance : expr → tactic expr /- Simplify the given expression using [defeq] lemmas. The resulting expression is definitionally equal to the input. -/ meta_constant defeq_simp_core : expr → transparency → tactic expr +/- Simplify the given expression using [simp] and [congr] lemmas. + The result is the simplified expression along with a proof that the new + expression is equivalent to the old one. + Fails if no simplifications can be performed. -/ +meta_constant simplify : expr → tactic (prod expr expr) /- Change the target of the main goal. The input expression must be definitionally equal to the current target. -/ meta_constant change : expr → tactic unit @@ -234,6 +240,28 @@ defeq_simp_core e transparency.reducible meta_definition dsimp : tactic unit := target >>= defeq_simp >>= change +set_option unifier.conservative true +meta_definition simp : tactic unit := +do gs ← get_goals, + match gs with + | (g :: rest) := do + tgt ← target, + r ← simplify tgt, + new_tgt ← return (prod.pr1 r), + pf ← return (prod.pr2 r), + pf_type ← infer_type pf, + new_g ← mk_meta_var new_tgt, + ns ← return (match expr.is_eq pf_type with + | (option.some _) := "eq" + | option.none := "iff" + end), + g_pf ← mk_app (ns <.> "mpr") [pf, new_g], + g_pf_type ← infer_type g_pf, + unify g g_pf, + set_goals (new_g :: rest) + | _ := fail "simp called but no goals" + end + /- Return the number of goals that need to be solved -/ meta_definition num_goals : tactic nat := do gs ← get_goals, @@ -348,4 +376,6 @@ private meta_definition get_arity_aux : expr → tactic nat meta_definition get_arity (fn : expr) : tactic nat := infer_type fn >>= whnf >>= get_arity_aux +meta_definition triv : tactic unit := mk_const "trivial" >>= exact + end tactic diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c1eb48d1f2..68e4f98400 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -333,6 +333,8 @@ add_subdirectory(library/tactic) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/tactic/defeq_simplifier) set(LEAN_OBJS ${LEAN_OBJS} $) +add_subdirectory(library/tactic/simplifier) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/definitional) set(LEAN_OBJS ${LEAN_OBJS} $) # add_subdirectory(library/blast) @@ -349,8 +351,6 @@ set(LEAN_OBJS ${LEAN_OBJS} $) # set(LEAN_OBJS ${LEAN_OBJS} $) # add_subdirectory(library/blast/grinder) # set(LEAN_OBJS ${LEAN_OBJS} $) -# add_subdirectory(library/blast/simplifier) -# set(LEAN_OBJS ${LEAN_OBJS} $) # add_subdirectory(library/blast/forward) # set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/vm) diff --git a/src/frontends/lean/old_attributes.cpp b/src/frontends/lean/old_attributes.cpp index e4373bd440..3974fceb00 100644 --- a/src/frontends/lean/old_attributes.cpp +++ b/src/frontends/lean/old_attributes.cpp @@ -29,22 +29,6 @@ void initialize_old_attributes() { return env; }, [](environment const &, name const &) { return false; }); - register_prio_attribute("simp", "simplification lemma", - [](environment const & env, io_state const & ios, name const & d, unsigned prio, name const & ns, bool persistent) { - return env; - }, - [](environment const &, name const &) { return false; }, - [](environment const & env, name const & n) { - return LEAN_DEFAULT_PRIORITY; - }); - register_prio_attribute("congr", "congruence lemma", - [](environment const & env, io_state const & ios, name const & d, unsigned prio, name const & ns, bool persistent) { - return env; - }, - [](environment const &, name const &) { return false; }, - [](environment const & env, name const & n) { - return LEAN_DEFAULT_PRIORITY; - }); register_prio_attribute("forward", "forward chaining", [](environment const & env, io_state const & ios, name const & d, unsigned prio, name const & ns, bool persistent) { return env; diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index 25e22c468a..ca7438bc54 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -30,6 +30,7 @@ Author: Leonardo de Moura #include "library/legacy_type_context.h" #include "library/unification_hint.h" #include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h" +#include "library/tactic/simplifier/simp_lemmas.h" #include "library/reducible.h" #include "library/definitional/projection.h" #include "frontends/lean/parser.h" @@ -554,34 +555,28 @@ static void print_defeq_lemmas(parser & p) { } static void print_simp_rules(parser & p) { -/* type_checker tc(p.env()); auto out = regular(p.env(), p.ios(), tc); - blast::scope_debug scope(p.env(), p.ios()); - blast::simp_lemmas s; + simp_lemmas slss; name ns; if (p.curr_is_identifier()) { ns = p.get_name_val(); p.next(); - s = blast::get_simp_lemmas(ns); + slss = get_simp_lemmas(p.env(), ns); } else { - s = blast::get_simp_lemmas(); + slss = get_simp_lemmas(p.env()); } format header; if (!ns.is_anonymous()) header = format(" at namespace '") + format(ns) + format("'"); - out << s.pp_simp(out.get_formatter(), header); -*/ + out << slss.pp_simp(out.get_formatter(), header); } static void print_congr_rules(parser & p) { -/* type_checker tc(p.env()); auto out = regular(p.env(), p.ios(), tc); - blast::scope_debug scope(p.env(), p.ios()); - blast::simp_lemmas s = blast::get_simp_lemmas(); - out << s.pp_congr(out.get_formatter()); -*/ + simp_lemmas slss = get_simp_lemmas(p.env()); + out << slss.pp_congr(out.get_formatter()); } static void print_light_rules(parser & p) { diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 4de05017b4..0d60c12aa6 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -19,7 +19,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp unifier.cpp match.cpp class_instance_resolution.cpp old_type_context.cpp legacy_type_context.cpp old_type_checker.cpp old_converter.cpp old_default_converter.cpp old_util.cpp let.cpp metavar_closure.cpp old_local_context.cpp choice_iterator.cpp - tmp_type_context.cpp + old_tmp_type_context.cpp # light_lt_manager.cpp # proof_irrel_expr_manager.cpp diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 5088d3e3a0..38ab9e2adf 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -14,7 +14,7 @@ Author: Leonardo de Moura #include "library/constants.h" #include "library/cache_helper.h" #include "library/app_builder.h" -#include "library/tmp_type_context.h" +#include "library/old_tmp_type_context.h" #include "library/relation_manager.h" namespace lean { diff --git a/src/library/blast/actions/by_contradiction_action.cpp b/src/library/blast/actions/by_contradiction_action.cpp index cb3db4e054..3a8fc16ce4 100644 --- a/src/library/blast/actions/by_contradiction_action.cpp +++ b/src/library/blast/actions/by_contradiction_action.cpp @@ -35,7 +35,7 @@ action_result by_contradiction_action() { s.set_target(mk_arrow(not_target, mk_constant(get_false_name()))); return intros_action(1); } - blast_tmp_type_context tmp_tctx; + blast_old_tmp_type_context tmp_tctx; optional target_decidable = tmp_tctx->mk_class_instance(mk_app(mk_constant(get_decidable_name()), target)); if (!target_decidable) return action_result::failed(); expr href = s.mk_hypothesis(get_app_builder().mk_not(target)); diff --git a/src/library/blast/backward/backward_lemmas.cpp b/src/library/blast/backward/backward_lemmas.cpp index 3738ea860b..24518a1c03 100644 --- a/src/library/blast/backward/backward_lemmas.cpp +++ b/src/library/blast/backward/backward_lemmas.cpp @@ -11,7 +11,7 @@ Author: Leonardo de Moura #include "library/trace.h" #include "library/scoped_ext.h" #include "library/user_recursors.h" -#include "library/tmp_type_context.h" +#include "library/old_tmp_type_context.h" #include "library/attribute_manager.h" #include "library/blast/blast.h" #include "library/blast/backward/backward_lemmas.h" @@ -57,7 +57,7 @@ struct backward_config { typedef scoped_ext backward_ext; -static optional get_backward_target(tmp_type_context & ctx, expr type) { +static optional get_backward_target(old_tmp_type_context & ctx, expr type) { while (is_pi(type)) { expr local = ctx.mk_tmp_local(binding_domain(type)); type = ctx.whnf(instantiate(binding_body(type), local)); @@ -69,7 +69,7 @@ static optional get_backward_target(tmp_type_context & ctx, expr typ return optional(); } -static optional get_backward_target(tmp_type_context & ctx, name const & c) { +static optional get_backward_target(old_tmp_type_context & ctx, name const & c) { declaration const & d = ctx.env().get(c); buffer us; unsigned num_us = d.get_num_univ_params(); @@ -80,7 +80,7 @@ static optional get_backward_target(tmp_type_context & ctx, name con } environment add_backward_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent) { - tmp_type_context ctx(env, ios.get_options()); + old_tmp_type_context ctx(env, ios.get_options()); auto index = get_backward_target(ctx, c); if (!index || index->kind() != expr_kind::Constant) throw exception(sstream() << "invalid [intro] attribute for '" << c << "', head symbol of resulting type must be a constant"); @@ -130,7 +130,7 @@ unsigned backward_lemma_prio_fn::operator()(backward_lemma const & r) const { void backward_lemma_index::init() { m_index.clear(); buffer lemmas; - blast_tmp_type_context ctx; + blast_old_tmp_type_context ctx; auto const & s = backward_ext::get_state(env()); s.to_buffer(lemmas); unsigned i = lemmas.size(); @@ -148,7 +148,7 @@ void backward_lemma_index::init() { } void backward_lemma_index::insert(expr const & href) { - blast_tmp_type_context ctx; + blast_old_tmp_type_context ctx; expr href_type = ctx->infer(href); if (optional target = get_backward_target(*ctx, href_type)) { m_index.insert(*target, backward_lemma(gexpr(href))); @@ -156,7 +156,7 @@ void backward_lemma_index::insert(expr const & href) { } void backward_lemma_index::erase(expr const & href) { - blast_tmp_type_context ctx; + blast_old_tmp_type_context ctx; expr href_type = ctx->infer(href); if (optional target = get_backward_target(*ctx, href_type)) { m_index.erase(*target, backward_lemma(gexpr(href))); diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index b2a6c25951..8cc7094cfc 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -75,17 +75,17 @@ struct imp_extension_entry { unsigned proof_irrel_hash(expr const & e); bool proof_irrel_is_equal(expr const & e1, expr const & e2); -class tmp_tctx_pool : public tmp_type_context_pool { +class tmp_tctx_pool : public old_tmp_type_context_pool { public: - virtual tmp_type_context * mk_tmp_type_context() override; - virtual void recycle_tmp_type_context(tmp_type_context * tmp_tctx) override; + virtual old_tmp_type_context * mk_old_tmp_type_context() override; + virtual void recycle_old_tmp_type_context(old_tmp_type_context * tmp_tctx) override; }; class blastenv { friend class scope_assignment; friend class scope_unfold_macro_pred; - typedef std::vector tmp_type_context_pool; - typedef std::unique_ptr tmp_type_context_ptr; + typedef std::vector old_tmp_type_context_pool; + typedef std::unique_ptr old_tmp_type_context_ptr; typedef std::vector imp_extension_entries; environment m_env; @@ -111,8 +111,8 @@ class blastenv { name_map m_projection_info; is_relation_pred m_is_relation_pred; state m_curr_state; // current state - tmp_type_context_pool m_tmp_ctx_pool; - tmp_type_context_ptr m_tmp_ctx; // for app_builder and congr_lemma_manager + old_tmp_type_context_pool m_tmp_ctx_pool; + old_tmp_type_context_ptr m_tmp_ctx; // for app_builder and congr_lemma_manager app_builder m_app_builder; fun_info_manager m_fun_info_manager; congr_lemma_manager m_congr_lemma_manager; @@ -674,7 +674,7 @@ public: m_class_pred(mk_class_pred(env)), m_instance_pred(mk_instance_pred(env)), m_is_relation_pred(mk_is_relation_pred(env)), - m_tmp_ctx(mk_tmp_type_context()), + m_tmp_ctx(mk_old_tmp_type_context()), m_app_builder(*m_tmp_ctx), m_fun_info_manager(*m_tmp_ctx), m_congr_lemma_manager(m_app_builder, m_fun_info_manager), @@ -777,9 +777,9 @@ public: return m_tmp_ctx->mk_subsingleton_instance(type); } - tmp_type_context * mk_tmp_type_context(); + old_tmp_type_context * mk_old_tmp_type_context(); - void recycle_tmp_type_context(tmp_type_context * ctx) { + void recycle_old_tmp_type_context(old_tmp_type_context * ctx) { lean_assert(ctx); ctx->clear(); m_tmp_ctx_pool.push_back(ctx); @@ -1446,10 +1446,10 @@ scope_debug::~scope_debug() {} /** \brief We need to redefine infer_local and infer_metavar, because the types of hypotheses and blast meta-variables are stored in the blast state */ -class tmp_tctx : public tmp_type_context { +class tmp_tctx : public old_tmp_type_context { public: tmp_tctx(environment const & env, options const & o): - tmp_type_context(env, o) {} + old_tmp_type_context(env, o) {} virtual bool should_unfold_macro(expr const & e) const override { return get_unfold_macro_pred()(e); @@ -1483,8 +1483,8 @@ public: } }; -tmp_type_context * blastenv::mk_tmp_type_context() { - tmp_type_context * r; +old_tmp_type_context * blastenv::mk_old_tmp_type_context() { + old_tmp_type_context * r; if (m_tmp_ctx_pool.empty()) { r = new tmp_tctx(m_env, m_ios.get_options()); // Design decision: in the blast tactic, we only consider the instances that were @@ -1500,31 +1500,31 @@ tmp_type_context * blastenv::mk_tmp_type_context() { return r; } -tmp_type_context * tmp_tctx_pool::mk_tmp_type_context() { +old_tmp_type_context * tmp_tctx_pool::mk_old_tmp_type_context() { lean_assert(g_blastenv); - return g_blastenv->mk_tmp_type_context(); + return g_blastenv->mk_old_tmp_type_context(); } -void tmp_tctx_pool::recycle_tmp_type_context(tmp_type_context * tmp_tctx) { +void tmp_tctx_pool::recycle_old_tmp_type_context(old_tmp_type_context * tmp_tctx) { lean_assert(g_blastenv); - g_blastenv->recycle_tmp_type_context(tmp_tctx); + g_blastenv->recycle_old_tmp_type_context(tmp_tctx); } -blast_tmp_type_context::blast_tmp_type_context(unsigned num_umeta, unsigned num_emeta) { +blast_old_tmp_type_context::blast_old_tmp_type_context(unsigned num_umeta, unsigned num_emeta) { lean_assert(g_blastenv); - m_ctx = g_blastenv->mk_tmp_type_context(); + m_ctx = g_blastenv->mk_old_tmp_type_context(); m_ctx->clear(); m_ctx->set_next_uvar_idx(num_umeta); m_ctx->set_next_mvar_idx(num_emeta); } -blast_tmp_type_context::blast_tmp_type_context() { +blast_old_tmp_type_context::blast_old_tmp_type_context() { lean_assert(g_blastenv); - m_ctx = g_blastenv->mk_tmp_type_context(); + m_ctx = g_blastenv->mk_old_tmp_type_context(); } -blast_tmp_type_context::~blast_tmp_type_context() { - g_blastenv->recycle_tmp_type_context(m_ctx); +blast_old_tmp_type_context::~blast_old_tmp_type_context() { + g_blastenv->recycle_old_tmp_type_context(m_ctx); } expr internalize(expr const & e) { diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h index 4cd40eefa0..d12b59b477 100644 --- a/src/library/blast/blast.h +++ b/src/library/blast/blast.h @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include #include "kernel/environment.h" #include "library/io_state.h" -#include "library/tmp_type_context.h" +#include "library/old_tmp_type_context.h" #include "library/relation_manager.h" #include "library/congr_lemma_manager.h" #include "library/fun_info_manager.h" @@ -18,7 +18,7 @@ Author: Leonardo de Moura namespace lean { struct projection_info; class goal; -typedef std::unique_ptr tmp_type_context_ptr; +typedef std::unique_ptr old_tmp_type_context_ptr; namespace blast { /** \brief Create a blast-state universe meta-variable */ level mk_uref(unsigned idx); @@ -245,17 +245,17 @@ public: /** \brief Create a temporary type_context that is compatible with blast. This temporary type context can acces the type of blast hypotheses and meta-variables. */ -class blast_tmp_type_context { - tmp_type_context * m_ctx; +class blast_old_tmp_type_context { + old_tmp_type_context * m_ctx; public: - blast_tmp_type_context(unsigned num_umeta, unsigned num_emeta); - blast_tmp_type_context(); - ~blast_tmp_type_context(); + blast_old_tmp_type_context(unsigned num_umeta, unsigned num_emeta); + blast_old_tmp_type_context(); + ~blast_old_tmp_type_context(); - tmp_type_context const * operator->() const { return m_ctx; } - tmp_type_context * operator->() { return m_ctx; } - tmp_type_context const & operator*() const { return *m_ctx; } - tmp_type_context & operator*() { return *m_ctx; } + old_tmp_type_context const * operator->() const { return m_ctx; } + old_tmp_type_context * operator->() { return m_ctx; } + old_tmp_type_context const & operator*() const { return *m_ctx; } + old_tmp_type_context & operator*() { return *m_ctx; } }; class scope_curr_state { diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp index f403d31b50..7cc252f4e4 100644 --- a/src/library/blast/congruence_closure.cpp +++ b/src/library/blast/congruence_closure.cpp @@ -293,7 +293,7 @@ static optional to_ext_congr_lemma(name const & R, expr const & if (!all_distinct(lhs_args) || !all_distinct(rhs_args)) { return optional(); } - blast_tmp_type_context ctx(r.get_num_umeta(), r.get_num_emeta()); + blast_old_tmp_type_context ctx(r.get_num_umeta(), r.get_num_emeta()); if (!ctx->is_def_eq(fn, lhs_fn) || !ctx->is_def_eq(fn, rhs_fn)) { return optional(); } diff --git a/src/library/blast/forward/ematch.cpp b/src/library/blast/forward/ematch.cpp index f9ac634f9a..8f519d5c06 100644 --- a/src/library/blast/forward/ematch.cpp +++ b/src/library/blast/forward/ematch.cpp @@ -253,7 +253,7 @@ void finalize_ematch() {} struct ematch_fn { ematch_branch_extension_core & m_ext; instances_branch_extension & m_inst_ext; - blast_tmp_type_context m_ctx; + blast_old_tmp_type_context m_ctx; congruence_closure & m_cc; enum frame_kind { DefEqOnly, EqvOnly, Match, MatchSS /* match subsingleton */, Continue }; diff --git a/src/library/blast/forward/pattern.cpp b/src/library/blast/forward/pattern.cpp index a0bfe5a533..f899a05d0b 100644 --- a/src/library/blast/forward/pattern.cpp +++ b/src/library/blast/forward/pattern.cpp @@ -14,7 +14,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "library/kernel_serializer.h" #include "library/generic_exception.h" -#include "library/tmp_type_context.h" +#include "library/old_tmp_type_context.h" #include "library/annotation.h" #include "library/util.h" #include "library/scoped_ext.h" @@ -191,7 +191,7 @@ name_set const & get_no_patterns(environment const & env) { namespace blast { typedef rb_tree idx_metavar_set; -static bool is_higher_order(tmp_type_context & ctx, expr const & e) { +static bool is_higher_order(old_tmp_type_context & ctx, expr const & e) { /* Remark: it is too expensive to use ctx.relaxed_whnf here. */ return is_pi(ctx.whnf(ctx.infer(e))); } @@ -200,7 +200,7 @@ static bool is_higher_order(tmp_type_context & ctx, expr const & e) { create n idx_metavars (one for each a_i), store the meta-variables in mvars, and store in trackable and residue the subsets of these meta-variables as described in the beginning of this file. Then returns B (instantiated with the new meta-variables) */ -expr extract_trackable(tmp_type_context & ctx, expr const & type, +expr extract_trackable(old_tmp_type_context & ctx, expr const & type, buffer & mvars, buffer & inst_implicit_flags, idx_metavar_set & trackable, idx_metavar_set & residue) { @@ -286,7 +286,7 @@ expr extract_trackable(tmp_type_context & ctx, expr const & type, } struct mk_hi_lemma_fn { - tmp_type_context & m_ctx; + old_tmp_type_context & m_ctx; name_set const & m_no_patterns; expr m_H; unsigned m_num_uvars; @@ -301,7 +301,7 @@ struct mk_hi_lemma_fn { idx_metavar_set m_residue; unsigned m_num_steps; - mk_hi_lemma_fn(tmp_type_context & ctx, expr const & H, + mk_hi_lemma_fn(old_tmp_type_context & ctx, expr const & H, unsigned num_uvars, unsigned prio, unsigned max_steps, bool simp): m_ctx(ctx), m_no_patterns(no_pattern_ext::get_state(ctx.env())), m_H(H), m_num_uvars(num_uvars), m_priority(prio), m_max_steps(max_steps), @@ -623,7 +623,7 @@ struct mk_hi_lemma_fn { } }; -hi_lemma mk_hi_lemma_core(tmp_type_context & ctx, expr const & H, unsigned num_uvars, +hi_lemma mk_hi_lemma_core(old_tmp_type_context & ctx, expr const & H, unsigned num_uvars, unsigned priority, unsigned max_steps, bool simp) { try { bool erase_hints = false; @@ -640,14 +640,14 @@ hi_lemma mk_hi_lemma_core(tmp_type_context & ctx, expr const & H, unsigned num_u } hi_lemma mk_hi_lemma(expr const & H) { - blast_tmp_type_context ctx; + blast_old_tmp_type_context ctx; unsigned max_steps = get_config().m_pattern_max_steps; bool simp = false; return mk_hi_lemma_core(*ctx, H, 0, LEAN_DEFAULT_PRIORITY, max_steps, simp); } hi_lemma mk_hi_lemma(name const & c, unsigned priority, bool simp) { - blast_tmp_type_context ctx; + blast_old_tmp_type_context ctx; unsigned max_steps = get_config().m_pattern_max_steps; declaration const & d = env().get(c); buffer us; diff --git a/src/library/blast/forward/pattern.h b/src/library/blast/forward/pattern.h index 646c37fc57..8b0df88726 100644 --- a/src/library/blast/forward/pattern.h +++ b/src/library/blast/forward/pattern.h @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "util/rb_multi_map.h" #include "kernel/environment.h" #include "library/expr_lt.h" -#include "library/tmp_type_context.h" +#include "library/old_tmp_type_context.h" namespace lean { /** \brief Annotate \c e as a pattern hint */ diff --git a/src/library/blast/grinder/intro_elim_lemmas.cpp b/src/library/blast/grinder/intro_elim_lemmas.cpp index 2ab1cbe5bc..22c52ce7e8 100644 --- a/src/library/blast/grinder/intro_elim_lemmas.cpp +++ b/src/library/blast/grinder/intro_elim_lemmas.cpp @@ -11,7 +11,7 @@ Author: Leonardo de Moura #include "library/trace.h" #include "library/scoped_ext.h" #include "library/user_recursors.h" -#include "library/tmp_type_context.h" +#include "library/old_tmp_type_context.h" #include "library/attribute_manager.h" #include "library/blast/blast.h" #include "library/blast/grinder/intro_elim_lemmas.h" @@ -70,7 +70,7 @@ environment add_elim_lemma(environment const & env, io_state const & ios, name c return intro_elim_ext::add_entry(env, ios, intro_elim_entry(true, prio, c), ns, persistent); } -optional get_intro_target(tmp_type_context & ctx, name const & c) { +optional get_intro_target(old_tmp_type_context & ctx, name const & c) { declaration const & d = ctx.env().get(c); buffer us; unsigned num_us = d.get_num_univ_params(); @@ -90,7 +90,7 @@ optional get_intro_target(tmp_type_context & ctx, name const & c) { } environment add_intro_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent) { - tmp_type_context ctx(env, ios.get_options()); + old_tmp_type_context ctx(env, ios.get_options()); if (!get_intro_target(ctx, c)) throw exception(sstream() << "invalid [intro!] attribute for '" << c << "', head symbol of resulting type must be a constant"); return intro_elim_ext::add_entry(env, ios, intro_elim_entry(false, prio, c), ns, persistent); @@ -148,7 +148,7 @@ namespace blast { head_map mk_intro_lemma_index() { head_map r; buffer lemmas; - blast_tmp_type_context ctx; + blast_old_tmp_type_context ctx; get_intro_lemmas(env(), lemmas); unsigned i = lemmas.size(); while (i > 0) { diff --git a/src/library/blast/simplifier/CMakeLists.txt b/src/library/blast/simplifier/CMakeLists.txt deleted file mode 100644 index 4985882a89..0000000000 --- a/src/library/blast/simplifier/CMakeLists.txt +++ /dev/null @@ -1,2 +0,0 @@ -add_library(simplifier OBJECT init_module.cpp ceqv.cpp simplifier.cpp simp_lemmas.cpp - simplifier_actions.cpp simplifier_strategies.cpp) diff --git a/src/library/blast/simplifier/simplifier.cpp b/src/library/blast/simplifier/simplifier.cpp deleted file mode 100644 index d6b78589a3..0000000000 --- a/src/library/blast/simplifier/simplifier.cpp +++ /dev/null @@ -1,1216 +0,0 @@ -/* -Copyright (c) 2015 Daniel Selsam. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Daniel Selsam -*/ -#include -#include -#include "util/flet.h" -#include "util/freset.h" -#include "util/pair.h" -#include "util/interrupt.h" -#include "util/sexpr/option_declarations.h" -#include "kernel/abstract.h" -#include "kernel/expr_maps.h" -#include "kernel/instantiate.h" -#include "library/trace.h" -#include "library/constants.h" -#include "library/normalize.h" -#include "library/expr_lt.h" -#include "library/num.h" -#include "library/util.h" -#include "library/norm_num.h" -#include "library/attribute_manager.h" -#include "library/class_instance_resolution.h" -#include "library/relation_manager.h" -#include "library/app_builder.h" -#include "library/blast/blast.h" -#include "library/blast/trace.h" -#include "library/blast/blast_exception.h" -#include "library/blast/simplifier/simplifier.h" -#include "library/blast/simplifier/simp_lemmas.h" -#include "library/blast/simplifier/ceqv.h" - -#ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS -#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 1000 -#endif -#ifndef LEAN_DEFAULT_SIMPLIFY_TOP_DOWN -#define LEAN_DEFAULT_SIMPLIFY_TOP_DOWN false -#endif -#ifndef LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE -#define LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE true -#endif -#ifndef LEAN_DEFAULT_SIMPLIFY_MEMOIZE -#define LEAN_DEFAULT_SIMPLIFY_MEMOIZE true -#endif -#ifndef LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL -#define LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL true -#endif -#ifndef LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS -#define LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS false -#endif -#ifndef LEAN_DEFAULT_SIMPLIFY_FUSE -#define LEAN_DEFAULT_SIMPLIFY_FUSE false -#endif -#ifndef LEAN_DEFAULT_SIMPLIFY_NUMERALS -#define LEAN_DEFAULT_SIMPLIFY_NUMERALS false -#endif - -namespace lean { -namespace blast { - -using simp::result; - -/* Keys */ - -static unsigned g_ac_key; -static unsigned g_som_key; -static unsigned g_numeral_key; - -/* Options */ - -static name * g_simplify_max_steps = nullptr; -static name * g_simplify_top_down = nullptr; -static name * g_simplify_exhaustive = nullptr; -static name * g_simplify_memoize = nullptr; -static name * g_simplify_contextual = nullptr; -static name * g_simplify_expand_macros = nullptr; -static name * g_simplify_fuse = nullptr; -static name * g_simplify_numerals = nullptr; - -unsigned get_simplify_max_steps() { - return ios().get_options().get_unsigned(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS); -} - -bool get_simplify_top_down() { - return ios().get_options().get_bool(*g_simplify_top_down, LEAN_DEFAULT_SIMPLIFY_TOP_DOWN); -} - -bool get_simplify_exhaustive() { - return ios().get_options().get_bool(*g_simplify_exhaustive, LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE); -} - -bool get_simplify_memoize() { - return ios().get_options().get_bool(*g_simplify_memoize, LEAN_DEFAULT_SIMPLIFY_MEMOIZE); -} - -bool get_simplify_contextual() { - return ios().get_options().get_bool(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL); -} - -bool get_simplify_expand_macros() { - return ios().get_options().get_bool(*g_simplify_expand_macros, LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS); -} - -bool get_simplify_fuse() { - return ios().get_options().get_bool(*g_simplify_fuse, LEAN_DEFAULT_SIMPLIFY_FUSE); -} - -bool get_simplify_numerals() { - return ios().get_options().get_bool(*g_simplify_numerals, LEAN_DEFAULT_SIMPLIFY_NUMERALS); -} - -/* Miscellaneous helpers */ - -static bool is_add_app(expr const & e) { - return is_const_app(e, get_add_name(), 4); -} - -static bool is_mul_app(expr const & e) { - return is_const_app(e, get_mul_name(), 4); -} - -static bool is_neg_app(expr const & e) { - return is_const_app(e, get_neg_name(), 3); -} - -/* Main simplifier class */ - -class simplifier { - blast_tmp_type_context m_tmp_tctx; - name m_rel; - expr_predicate m_simp_pred; - - simp_lemmas m_srss; - simp_lemmas m_ctx_srss; - - /* Logging */ - unsigned m_num_steps{0}; - - /* Options */ - unsigned m_max_steps{get_simplify_max_steps()}; - bool m_top_down{get_simplify_top_down()}; - bool m_exhaustive{get_simplify_exhaustive()}; - bool m_memoize{get_simplify_memoize()}; - bool m_contextual{get_simplify_contextual()}; - bool m_expand_macros{get_simplify_expand_macros()}; - bool m_fuse{get_simplify_fuse()}; - bool m_numerals{get_simplify_numerals()}; - - /* Cache */ - struct key { - name m_rel; - expr m_e; - unsigned m_hash; - - key(name const & rel, expr const & e): - m_rel(rel), m_e(e), m_hash(hash(rel.hash(), abstract_hash(e))) { } - }; - - struct key_hash_fn { - unsigned operator()(key const & k) const { return k.m_hash; } - }; - - struct key_eq_fn { - bool operator()(key const & k1, key const & k2) const { - return k1.m_rel == k2.m_rel && abstract_is_equal(k1.m_e, k2.m_e); - } - }; - - typedef std::unordered_map simplify_cache; - simplify_cache m_cache; - optional cache_lookup(expr const & e); - void cache_save(expr const & e, result const & r); - - /* Mapping from subsingleton type to representative */ - expr_map m_subsingleton_elem_map; - optional normalize_subsingleton_args(expr const & e); - - /* Basic helpers */ - bool using_eq() { return m_rel == get_eq_name(); } - - bool is_dependent_fn(expr const & f) { - expr f_type = m_tmp_tctx->whnf(m_tmp_tctx->infer(f)); - lean_assert(is_pi(f_type)); - return has_free_vars(binding_body(f_type)); - } - - simp_lemmas add_to_srss(simp_lemmas const & _srss, buffer & ls) { - simp_lemmas srss = _srss; - for (unsigned i = 0; i < ls.size(); i++) { - expr & l = ls[i]; - blast_tmp_type_context tctx; - try { - // TODO(Leo,Daniel): should we allow the user to set the priority of local lemmas - srss = add(*tctx, srss, mlocal_name(l), tctx->infer(l), l, LEAN_DEFAULT_PRIORITY); - } catch (exception e) { - } - } - return srss; - } - - expr unfold_reducible_instances(expr const & e); - expr remove_unnecessary_casts(expr const & e); - - bool instantiate_emetas(blast_tmp_type_context & tmp_tctx, unsigned num_emeta, - list const & emetas, list const & instances); - - /* Results */ - result lift_from_eq(expr const & e_old, result const & r_eq); - result join(result const & r1, result const & r2); - result funext(result const & r, expr const & l); - result finalize(result const & r); - - /* Simplification */ - result simplify(expr const & e, simp_lemmas const & srss); - result simplify(expr const & e, bool is_root); - result simplify_lambda(expr const & e); - result simplify_pi(expr const & e); - result simplify_app(expr const & e); - result simplify_fun(expr const & e); - optional simplify_numeral(expr const & e); - - /* Proving */ - optional prove(expr const & thm); - optional prove(expr const & thm, simp_lemmas const & srss); - - /* Rewriting */ - result rewrite(expr const & e); - result rewrite(expr const & e, simp_lemmas const & srss); - result rewrite(expr const & e, simp_lemma const & sr); - - /* Congruence */ - result congr_fun_arg(result const & r_f, result const & r_arg); - result congr(result const & r_f, result const & r_arg); - result congr_fun(result const & r_f, expr const & arg); - result congr_arg(expr const & f, result const & r_arg); - result congr_funs(result const & r_f, buffer const & args); - - result try_congrs(expr const & e); - result try_congr(expr const & e, user_congr_lemma const & cr); - - template - optional synth_congr(expr const & e, F && simp); - - /* Fusion */ - result maybe_fuse(expr const & e, bool is_root); - result fuse(expr const & e); - expr_pair split_summand(expr const & e, expr const & f_mul, expr const & one); - - /* Apply whnf and eta-reduction - \remark We want (Sum n (fun x, f x)) and (Sum n f) to be the same. - \remark We may want to switch to eta-expansion later (see paper: "The Virtues of Eta-expansion"). - TODO(Daniel, Leo): should we add an option for disabling/enabling eta? */ - expr whnf_eta(expr const & e); - -public: - simplifier(name const & rel, expr_predicate const & simp_pred): m_rel(rel), m_simp_pred(simp_pred) { } - result operator()(expr const & e, simp_lemmas const & srss) { return simplify(e, srss); } -}; - -/* Cache */ - -optional simplifier::cache_lookup(expr const & e) { - /* cache_lookup is based on congr_lemma, and assumes \c e is an application */ - if (!is_app(e)) return optional(); - auto it = m_cache.find(key(m_rel, e)); - if (it == m_cache.end()) return optional(); - /* The cache ignores subsingletons, so we may need to - synthesize a congruence lemma. */ - expr e_old = it->first.m_e; - result r_old = it->second; - lean_assert(abstract_is_equal(e, e_old)); - if (e == e_old) return optional(r_old); - lean_assert(is_app(e_old)); - buffer new_args, old_args; - DEBUG_CODE(expr const & f_new =) get_app_args(e, new_args); - DEBUG_CODE(expr const & f_old =) get_app_args(e_old, old_args); - lean_assert(f_new == f_old); - auto congr_lemma = mk_specialized_congr_lemma(e); - if (!congr_lemma) return optional(); - expr proof = congr_lemma->get_proof(); - expr type = congr_lemma->get_type(); - - unsigned i = 0; - for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) { - lean_assert(ckind == congr_arg_kind::Cast || new_args[i] == old_args[i], static_cast(ckind), new_args[i], old_args[i]); - expr rfl; - switch (ckind) { - case congr_arg_kind::HEq: - lean_unreachable(); - case congr_arg_kind::Fixed: - proof = mk_app(proof, new_args[i]); - type = instantiate(binding_body(type), new_args[i]); - break; - case congr_arg_kind::FixedNoParam: - break; - case congr_arg_kind::Eq: - proof = mk_app(proof, new_args[i]); - type = instantiate(binding_body(type), new_args[i]); - rfl = get_app_builder().mk_eq_refl(old_args[i]); - proof = mk_app(proof, old_args[i], rfl); - type = instantiate(binding_body(type), old_args[i]); - type = instantiate(binding_body(type), rfl); - break; - case congr_arg_kind::Cast: - proof = mk_app(proof, new_args[i]); - type = instantiate(binding_body(type), new_args[i]); - proof = mk_app(proof, old_args[i]); - type = instantiate(binding_body(type), old_args[i]); - break; - } - i++; - }); - - lean_assert(is_eq(type)); - result r_congr = result(e_old, proof); - return optional(join(r_congr, r_old)); -} - -void simplifier::cache_save(expr const & e, result const & r) { - m_cache.insert(mk_pair(key(m_rel, e), r)); -} - -/* Results */ - -result simplifier::lift_from_eq(expr const & e_old, result const & r_eq) { - if (!r_eq.has_proof()) return r_eq; - lean_assert(r_eq.has_proof()); - /* r_eq.get_proof() : e_old = r_eq.get_new() */ - /* goal : e_old r_eq.get_new() */ - expr l = m_tmp_tctx->mk_tmp_local(m_tmp_tctx->infer(e_old)); - expr motive_local = get_app_builder().mk_app(m_rel, e_old, l); - /* motive = fun y, e_old y */ - expr motive = Fun(l, motive_local); - /* Rxx = x x */ - expr Rxx = get_app_builder().mk_refl(m_rel, e_old); - expr pf = get_app_builder().mk_eq_rec(motive, Rxx, r_eq.get_proof()); - return result(r_eq.get_new(), pf); -} - -result simplifier::join(result const & r1, result const & r2) { - /* Assumes that both results are with respect to the same relation */ - if (!r1.has_proof()) { - return r2; - } else if (!r2.has_proof()) { - lean_assert(r1.has_proof()); - return result(r2.get_new(), r1.get_proof()); - } else { - /* If they both have proofs, we need to glue them together with transitivity. */ - lean_assert(r1.has_proof() && r2.has_proof()); - expr trans = get_app_builder().mk_trans(m_rel, r1.get_proof(), r2.get_proof()); - return result(r2.get_new(), trans); - } -} - -result simplifier::funext(result const & r, expr const & l) { - // theorem funext {f₁ f₂ : Πx : A, B x} : (∀x, f₁ x = f₂ x) → f₁ = f₂ := - expr e = Fun(l, r.get_new()); - if (!r.has_proof()) return result(e); - expr pf = get_app_builder().mk_app(get_funext_name(), Fun(l, r.get_proof())); - return result(e, pf); -} - -result simplifier::finalize(result const & r) { - if (r.has_proof()) return r; - expr pf = get_app_builder().mk_refl(m_rel, r.get_new()); - return result(r.get_new(), pf); -} - -/* Whnf + Eta */ -expr simplifier::whnf_eta(expr const & e) { - return try_eta(whnf(e)); -} - -/* Simplification */ - -result simplifier::simplify(expr const & e, simp_lemmas const & srss) { - flet set_srss(m_srss, srss); - freset reset1(m_cache); - freset> reset2(m_subsingleton_elem_map); - return simplify(e, true); -} - -result simplifier::simplify(expr const & e, bool is_root) { - check_system("simplifier"); - m_num_steps++; - lean_trace_inc_depth("simplifier"); - lean_trace_d("simplifier", tout() << m_rel << ": " << e << "\n";); - - if (m_num_steps > m_max_steps) - throw blast_exception("simplifier failed, maximum number of steps exceeded", e); - - if (m_memoize) { - if (auto it = cache_lookup(e)) return *it; - } - - if (!m_simp_pred(e)) return result(e); - - if (m_numerals && using_eq()) { - if (auto r = simplify_numeral(e)) { - return *r; - } - } - - result r(e); - - if (m_top_down) r = join(r, rewrite(whnf_eta(r.get_new()))); - - r.update(whnf_eta(r.get_new())); - - switch (r.get_new().kind()) { - case expr_kind::Local: - case expr_kind::Meta: - case expr_kind::Sort: - case expr_kind::Constant: - // no-op - break; - case expr_kind::Var: - lean_unreachable(); - case expr_kind::Macro: - if (m_expand_macros) { - if (auto m = m_tmp_tctx->expand_macro(e)) r = join(r, simplify(whnf_eta(*m), is_root)); - } - break; - case expr_kind::Lambda: - if (using_eq()) r = join(r, simplify_lambda(r.get_new())); - break; - case expr_kind::Pi: - r = join(r, simplify_pi(r.get_new())); - break; - case expr_kind::App: - r = join(r, simplify_app(r.get_new())); - break; - case expr_kind::Let: - // whnf unfolds let-expressions - lean_unreachable(); - } - - if (!m_top_down) r = join(r, rewrite(whnf_eta(r.get_new()))); - - if (r.get_new() == e && !using_eq()) { - result r_eq; - { - flet use_eq(m_rel, get_eq_name()); - r_eq = simplify(r.get_new(), is_root); - } - r = join(r, lift_from_eq(r.get_new(), r_eq)); - } - - if (m_exhaustive && r.has_proof()) r = join(r, simplify(r.get_new(), is_root)); - - if (m_memoize) cache_save(e, r); - - if (m_fuse && using_eq()) r = join(r, maybe_fuse(r.get_new(), is_root)); - - return r; -} - -result simplifier::simplify_lambda(expr const & e) { - lean_assert(is_lambda(e)); - expr t = e; - - buffer ls; - while (is_lambda(t)) { - expr d = instantiate_rev(binding_domain(t), ls.size(), ls.data()); - expr l = m_tmp_tctx->mk_tmp_local(binding_name(t), d, binding_info(t)); - ls.push_back(l); - t = instantiate(binding_body(t), l); - } - - result r = simplify(t, false); - expr new_t = r.get_new(); - /* check if subsingleton, and normalize */ - expr new_t_type = m_tmp_tctx->infer(new_t); - if (m_tmp_tctx->mk_subsingleton_instance(new_t_type)) { - auto it = m_subsingleton_elem_map.find(new_t_type); - if (it != m_subsingleton_elem_map.end()) { - if (it->second != new_t) { - expr proof = get_app_builder().mk_app(get_subsingleton_elim_name(), new_t, it->second); - r = join(r, result(it->second, proof)); - } - } else { - m_subsingleton_elem_map.insert(mk_pair(new_t_type, new_t)); - } - } - - for (int i = ls.size() - 1; i >= 0; --i) r = funext(r, ls[i]); - return r; -} - -result simplifier::simplify_pi(expr const & e) { - lean_assert(is_pi(e)); - return try_congrs(e); -} - -expr simplifier::unfold_reducible_instances(expr const & e) { - buffer args; - expr f = get_app_args(e, args); - fun_info f_info = get_specialized_fun_info(e); - int i = -1; - for_each(f_info.get_params_info(), [&](param_info const & p_info) { - i++; - if (p_info.is_inst_implicit() && !p_info.is_subsingleton()) { - args[i] = blast::normalize(args[i]); - } - }); - return mk_app(f, args); -} - -result simplifier::simplify_app(expr const & _e) { - lean_assert(is_app(_e)); - expr e = unfold_reducible_instances(_e); - - /* (1) Try user-defined congruences */ - result r_user = try_congrs(e); - if (r_user.has_proof()) { - if (using_eq()) return join(r_user, simplify_fun(r_user.get_new())); - else return r_user; - } - - /* (2) Synthesize congruence lemma */ - if (using_eq()) { - optional r_args = synth_congr(e, [&](expr const & e) { - return simplify(e, false); - }); - if (r_args) return join(*r_args, simplify_fun(r_args->get_new())); - } - - /* (3) Fall back on generic binary congruence */ - if (using_eq()) { - expr const & f = app_fn(e); - expr const & arg = app_arg(e); - - // TODO(dhs): it is not clear if this recursive call should be considered - // a root or not, though does not matter since if + were being applied, - // we would have synthesized a congruence rule in step (2). - result r_f = simplify(f, false); - - if (is_dependent_fn(f)) { - if (r_f.has_proof()) return congr_fun(r_f, arg); - else return mk_app(r_f.get_new(), arg); - } else { - result r_arg = simplify(arg, false); - return congr_fun_arg(r_f, r_arg); - } - } - return result(e); -} - -result simplifier::simplify_fun(expr const & e) { - lean_assert(is_app(e)); - buffer args; - expr const & f = get_app_args(e, args); - result r_f = simplify(f, true); - return congr_funs(r_f, args); -} - -optional simplifier::simplify_numeral(expr const & e) { - if (is_num(e)) { return optional(result(e)); } - - try { - expr_pair r = mk_norm_num(*m_tmp_tctx, e); - return optional(result(r.first, r.second)); - } catch (exception e) { - return optional(); - } -} - -/* Proving */ - -optional simplifier::prove(expr const & thm) { - flet set_name(m_rel, get_iff_name()); - result r_cond = simplify(thm, true); - if (is_constant(r_cond.get_new()) && const_name(r_cond.get_new()) == get_true_name()) { - expr pf = get_app_builder().mk_app(get_iff_elim_right_name(), - finalize(r_cond).get_proof(), - mk_constant(get_true_intro_name())); - return some_expr(pf); - } - return none_expr(); -} - -optional simplifier::prove(expr const & thm, simp_lemmas const & srss) { - flet set_name(m_rel, get_iff_name()); - result r_cond = simplify(thm, srss); - if (is_constant(r_cond.get_new()) && const_name(r_cond.get_new()) == get_true_name()) { - expr pf = get_app_builder().mk_app(get_iff_elim_right_name(), - finalize(r_cond).get_proof(), - mk_constant(get_true_intro_name())); - return some_expr(pf); - } - return none_expr(); -} - -/* Rewriting */ - -result simplifier::rewrite(expr const & e) { - result r(e); - while (true) { - result r_ctx = rewrite(r.get_new(), m_ctx_srss); - result r_new = rewrite(r_ctx.get_new(), m_srss); - if (!r_ctx.has_proof() && !r_new.has_proof()) break; - r = join(join(r, r_ctx), r_new); - } - return r; -} - -result simplifier::rewrite(expr const & e, simp_lemmas const & srss) { - result r(e); - - simp_lemmas_for const * sr = srss.find(m_rel); - if (!sr) return r; - - list const * srs = sr->find_simp(e); - if (!srs) return r; - - for_each(*srs, [&](simp_lemma const & sr) { - result r_new = rewrite(r.get_new(), sr); - if (!r_new.has_proof()) return; - r = join(r, r_new); - }); - return r; -} - -result simplifier::rewrite(expr const & e, simp_lemma const & sr) { - blast_tmp_type_context tmp_tctx(sr.get_num_umeta(), sr.get_num_emeta()); - - if (!tmp_tctx->is_def_eq(e, sr.get_lhs())) return result(e); - - lean_trace(name({"simplifier", "rewrite"}), - expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs()); - expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs()); - tout() << "(" << sr.get_id() << ") " - << "[" << new_lhs << " --> " << new_rhs << "]\n";); - - if (!instantiate_emetas(tmp_tctx, sr.get_num_emeta(), sr.get_emetas(), sr.get_instances())) return result(e); - - for (unsigned i = 0; i < sr.get_num_umeta(); i++) { - if (!tmp_tctx->is_uvar_assigned(i)) return result(e); - } - - expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs()); - expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs()); - - if (sr.is_perm()) { - if (!is_light_lt(new_rhs, new_lhs)) - return result(e); - } - - expr pf = tmp_tctx->instantiate_uvars_mvars(sr.get_proof()); - return result(new_rhs, pf); -} - -/* Congruence */ - -result simplifier::congr_fun_arg(result const & r_f, result const & r_arg) { - if (!r_f.has_proof() && !r_arg.has_proof()) return result(mk_app(r_f.get_new(), r_arg.get_new())); - else if (!r_f.has_proof()) return congr_arg(r_f.get_new(), r_arg); - else if (!r_arg.has_proof()) return congr_fun(r_f, r_arg.get_new()); - else return congr(r_f, r_arg); -} - -result simplifier::congr(result const & r_f, result const & r_arg) { - lean_assert(r_f.has_proof() && r_arg.has_proof()); - // theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ - expr e = mk_app(r_f.get_new(), r_arg.get_new()); - expr pf = get_app_builder().mk_congr(r_f.get_proof(), r_arg.get_proof()); - return result(e, pf); -} - -result simplifier::congr_fun(result const & r_f, expr const & arg) { - lean_assert(r_f.has_proof()); - // theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a - expr e = mk_app(r_f.get_new(), arg); - expr pf = get_app_builder().mk_congr_fun(r_f.get_proof(), arg); - return result(e, pf); -} - -result simplifier::congr_arg(expr const & f, result const & r_arg) { - lean_assert(r_arg.has_proof()); - // theorem congr_arg {A B : Type} {a₁ a₂ : A} (f : A → B) : a₁ = a₂ → f a₁ = f a₂ - expr e = mk_app(f, r_arg.get_new()); - expr pf = get_app_builder().mk_congr_arg(f, r_arg.get_proof()); - return result(e, pf); -} - -/* Note: handles reflexivity */ -result simplifier::congr_funs(result const & r_f, buffer const & args) { - // congr_fun : ∀ {A : Type} {B : A → Type} {f g : Π (x : A), B x}, f = g → (∀ (a : A), f a = g a) - expr e = r_f.get_new(); - for (unsigned i = 0; i < args.size(); ++i) { - e = mk_app(e, args[i]); - } - if (!r_f.has_proof()) return result(e); - expr pf = r_f.get_proof(); - for (unsigned i = 0; i < args.size(); ++i) { - pf = get_app_builder().mk_app(get_congr_fun_name(), pf, args[i]); - } - return result(e, pf); -} - -result simplifier::try_congrs(expr const & e) { - simp_lemmas_for const * sr = get_simp_lemmas().find(m_rel); - if (!sr) return result(e); - - list const * crs = sr->find_congr(e); - if (!crs) return result(e); - - result r(e); - for_each(*crs, [&](user_congr_lemma const & cr) { - if (r.has_proof()) return; - r = try_congr(e, cr); - }); - return r; -} - -result simplifier::try_congr(expr const & e, user_congr_lemma const & cr) { - blast_tmp_type_context tmp_tctx(cr.get_num_umeta(), cr.get_num_emeta()); - - if (!tmp_tctx->is_def_eq(e, cr.get_lhs())) return result(e); - - lean_trace(name({"simplifier", "congruence"}), - expr new_lhs = tmp_tctx->instantiate_uvars_mvars(cr.get_lhs()); - expr new_rhs = tmp_tctx->instantiate_uvars_mvars(cr.get_rhs()); - diagnostic(env(), ios(), get_type_context()) - << "(" << cr.get_id() << ") " - << "[" << new_lhs << " =?= " << new_rhs << "]\n";); - - /* First, iterate over the congruence hypotheses */ - bool failed = false; - bool simplified = false; - list const & congr_hyps = cr.get_congr_hyps(); - for_each(congr_hyps, [&](expr const & m) { - if (failed) return; - buffer ls; - expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m)); - - while (is_pi(m_type)) { - expr d = instantiate_rev(binding_domain(m_type), ls.size(), ls.data()); - expr l = tmp_tctx->mk_tmp_local(d, binding_info(m_type)); - lean_assert(!has_metavar(l)); - ls.push_back(l); - m_type = instantiate(binding_body(m_type), l); - } - - expr h_rel, h_lhs, h_rhs; - lean_verify(is_simp_relation(env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel)); - { - flet set_name(m_rel, const_name(h_rel)); - - flet set_ctx_srss(m_ctx_srss, m_contextual ? add_to_srss(m_ctx_srss, ls) : m_ctx_srss); - - h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs); - lean_assert(!has_metavar(h_lhs)); - - result r_congr_hyp = simplify(h_lhs, m_srss); - if (r_congr_hyp.has_proof()) simplified = true; - r_congr_hyp = finalize(r_congr_hyp); - expr hyp = finalize(r_congr_hyp).get_proof(); - - if (!tmp_tctx->is_def_eq(m, Fun(ls, hyp))) failed = true; - } - }); - - if (failed || !simplified) return result(e); - - if (!instantiate_emetas(tmp_tctx, cr.get_num_emeta(), cr.get_emetas(), cr.get_instances())) return result(e); - - for (unsigned i = 0; i < cr.get_num_umeta(); i++) { - if (!tmp_tctx->is_uvar_assigned(i)) return result(e); - } - - expr e_s = tmp_tctx->instantiate_uvars_mvars(cr.get_rhs()); - expr pf = tmp_tctx->instantiate_uvars_mvars(cr.get_proof()); - return result(e_s, pf); -} - -bool simplifier::instantiate_emetas(blast_tmp_type_context & tmp_tctx, unsigned num_emeta, list const & emetas, - list const & instances) { - bool failed = false; - unsigned i = num_emeta; - for_each2(emetas, instances, [&](expr const & m, bool const & is_instance) { - i--; - if (failed) return; - expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m)); - lean_assert(!has_metavar(m_type)); - - if (tmp_tctx->is_mvar_assigned(i)) return; - - if (is_instance) { - if (auto v = tmp_tctx->mk_class_instance(m_type)) { - if (!tmp_tctx->assign(m, *v)) { - lean_trace(name({"simplifier", "failure"}), - tout() << "unable to assign instance for: " << m_type << "\n";); - failed = true; - return; - } - } else { - lean_trace(name({"simplifier", "failure"}), - tout() << "unable to synthesize instance for: " << m_type << "\n";); - failed = true; - return; - } - } - - if (tmp_tctx->is_mvar_assigned(i)) return; - - if (tmp_tctx->is_prop(m_type)) { - if (auto pf = prove(m_type)) { - lean_verify(tmp_tctx->is_def_eq(m, *pf)); - return; - } - } - - lean_trace(name({"simplifier", "failure"}), - tout() << "failed to assign: " << m << " : " << m_type << "\n";); - - failed = true; - return; - }); - - return !failed; -} - -/* Given a function application \c e, replace arguments that are subsingletons with a - representative */ -optional simplifier::normalize_subsingleton_args(expr const & e) { - buffer args; - get_app_args(e, args); - auto congr_lemma = mk_specialized_congr_lemma(e); - if (!congr_lemma) return optional(); - expr proof = congr_lemma->get_proof(); - expr type = congr_lemma->get_type(); - unsigned i = 0; - bool normalized = false; - for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) { - expr rfl; - switch (ckind) { - case congr_arg_kind::HEq: - lean_unreachable(); - case congr_arg_kind::Fixed: - proof = mk_app(proof, args[i]); - type = instantiate(binding_body(type), args[i]); - break; - case congr_arg_kind::FixedNoParam: - break; - case congr_arg_kind::Eq: - proof = mk_app(proof, args[i]); - type = instantiate(binding_body(type), args[i]); - rfl = get_app_builder().mk_eq_refl(args[i]); - proof = mk_app(proof, args[i], rfl); - type = instantiate(binding_body(type), args[i]); - type = instantiate(binding_body(type), rfl); - break; - case congr_arg_kind::Cast: - proof = mk_app(proof, args[i]); - type = instantiate(binding_body(type), args[i]); - expr const & arg_type = binding_domain(type); - expr new_arg; - auto it = m_subsingleton_elem_map.find(arg_type); - if (it != m_subsingleton_elem_map.end()) { - normalized = (it->second != args[i]); - new_arg = it->second; - } else { - new_arg = args[i]; - m_subsingleton_elem_map.insert(mk_pair(arg_type, args[i])); - } - proof = mk_app(proof, new_arg); - type = instantiate(binding_body(type), new_arg); - break; - } - i++; - }); - if (!normalized) return optional(); - lean_assert(is_eq(type)); - buffer type_args; - get_app_args(type, type_args); - expr e_new = type_args[2]; - return optional(result(e_new, proof)); -} - -template -optional simplifier::synth_congr(expr const & e, F && simp) { - static_assert(std::is_same::type, result>::value, - "synth_congr: simp must take expressions to results"); - lean_assert(is_app(e)); - buffer args; - expr f = get_app_args(e, args); - auto congr_lemma = mk_specialized_congr_lemma_for_simp(e); - if (!congr_lemma) return optional(); - expr proof = congr_lemma->get_proof(); - expr type = congr_lemma->get_type(); - unsigned i = 0; - bool has_proof = false; - bool has_cast = false; - for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) { - switch (ckind) { - case congr_arg_kind::HEq: - lean_unreachable(); - case congr_arg_kind::Fixed: - proof = mk_app(proof, args[i]); - type = instantiate(binding_body(type), args[i]); - break; - case congr_arg_kind::FixedNoParam: - break; - case congr_arg_kind::Eq: - proof = mk_app(proof, args[i]); - type = instantiate(binding_body(type), args[i]); - { - result r_arg = simp(args[i]); - if (r_arg.has_proof()) has_proof = true; - r_arg = finalize(r_arg); - proof = mk_app(proof, r_arg.get_new(), r_arg.get_proof()); - type = instantiate(binding_body(type), r_arg.get_new()); - type = instantiate(binding_body(type), r_arg.get_proof()); - } - break; - case congr_arg_kind::Cast: - proof = mk_app(proof, args[i]); - type = instantiate(binding_body(type), args[i]); - has_cast = true; - break; - } - i++; - }); - lean_assert(is_eq(type)); - buffer type_args; - get_app_args(type, type_args); - expr e_new = remove_unnecessary_casts(type_args[2]); - result r; - if (has_proof) r = result(e_new, proof); - else r = result(e_new); - - if (has_cast) { - if (auto r_norm = normalize_subsingleton_args(e_new)) - r = join(r, *r_norm); - } - return optional(r); -} - -expr simplifier::remove_unnecessary_casts(expr const & e) { - buffer args; - expr f = get_app_args(e, args); - fun_info f_info = get_specialized_fun_info(e); - int i = -1; - for_each(f_info.get_params_info(), [&](param_info const & p_info) { - i++; - if (p_info.is_subsingleton()) { - while (is_constant(get_app_fn(args[i]))) { - buffer cast_args; - expr f_cast = get_app_args(args[i], cast_args); - name n_f = const_name(f_cast); - if (n_f == get_eq_rec_name() || n_f == get_eq_drec_name() || n_f == get_eq_nrec_name()) { - lean_assert(cast_args.size() == 6); - expr major_premise = cast_args[5]; - expr f_major_premise = get_app_fn(major_premise); - if (is_constant(f_major_premise) && const_name(f_major_premise) == get_eq_refl_name()) - args[i] = cast_args[3]; - else - return; - } else { - return; - } - } - } - }); - return mk_app(f, args); -} - -/* Fusion */ - -result simplifier::maybe_fuse(expr const & e, bool is_root) { - if (!is_app(e)) return result(e); - if (is_root && is_add_app(e)) return fuse(e); - if (!is_root && is_add_app(e)) return result(e); - lean_assert(!is_add_app(e)); - /* At this point we know we are an application of something other than + */ - optional r = synth_congr(e, [&](expr const & arg) { - if (is_add_app(arg)) return fuse(arg); - else return result(arg); - }); - if (r) return *r; - else return result(e); -} - -result simplifier::fuse(expr const & e) { - lean_assert(is_add_app(e)); -// ios().get_diagnostic_channel() << "FUSE: " << e << "\n\n"; - flet no_recursive_fusion(m_fuse, false); - - /* Note: we assume all negations are on the outside of the summands */ - - /* Example - 1. Input (e): n1 * x1 * n2 * x2 + x3 + - (x1 * x2 * n3) + (- x3) + x4 - 2. Split summands: (n1 * n2) * (x1 * x2) + 1 * x3 + (- n3) * (x1 * x2) + (- 1) * x3 + 1 * x4 - 3. Group by variable (e_grp): ((n1 * n2) * (x1 * x2) + (- n3) * (x1 * x2)) + (1 * x3 + (-1) * x3) + x4 - 4. Introduce locals (e_grp_ls): ((n1 * n2) * l1 + (- n3) * l1) + (1 * l2 + (-1) * l2) + l3 - 5. Fuse (e_fused_ls): (n1 * n2 + (- n3)) * l1 + (1 + (- 1)) * l2 + 1 * l3 - 6. Simplify coefficients (e_simp_ls): (n1 * n2 + (- n3)) * l1 + l3 - 7. Instantiate locals (e_simp): (n1 * n2 + (- n3)) * (x1 * x2) + x4 - - Proofs - 1. Prove (1) == (3) using simplify with [ac] - 2. Prove (4) == (5) using simplify with [som] - 3. Prove (5) == (6) using simplify with [numeral] - 4. Prove (4) == (6) by transitivity of proofs (2) and (3) - 5. Prove (3) == (7) by instantiating proof (4) - 6. Prove (1) == (7) by transitivity of proofs (1) and (5) - */ - - /* Construct useful expressions */ - buffer args; - get_app_args(e, args); - expr T = args[0]; - expr f_add, f_mul, zero, one; - try { - f_add = get_app_builder().mk_partial_add(T); - f_mul = get_app_builder().mk_partial_mul(T); - zero = get_app_builder().mk_zero(T); - one = get_app_builder().mk_one(T); - expr left_distrib = get_app_builder().mk_partial_left_distrib(T); - } catch (app_builder_exception & ex) { - lean_trace(name({"simplifier", "failure"}), - tout() << "cannot synthesize necessary instances\n";); - return result(e); - } - - /* (1 ==> 2) Split each summand into (a) numerals and (b) variables */ - buffer numerals; - buffer variables; - expr s = e; - while (is_add_app(s)) { - buffer args; - expr f = get_app_args(s, args); - auto n_v = split_summand(args[2], f_mul, one); - numerals.push_back(n_v.first); - variables.push_back(n_v.second); - s = args[3]; - } - auto n_v = split_summand(s, f_mul, one); - numerals.push_back(n_v.first); - variables.push_back(n_v.second); - lean_assert(numerals.size() == variables.size()); - - /* (2 ==> 3, 4, 5) Group the summands by variable */ - expr_bi_struct_map > variable_to_numerals; - for (unsigned i = 0; i < numerals.size(); i++) { - auto it = variable_to_numerals.find(variables[i]); - if (it != variable_to_numerals.end()) it->second = cons(numerals[i], it->second); - else variable_to_numerals.insert({variables[i], list(numerals[i])}); - } - - expr e_grp = zero; - expr e_grp_ls = zero; - expr e_fused_ls = zero; - - buffer locals; - variables.clear(); - for (auto v_ns : variable_to_numerals) { - expr local; - if (!is_one(v_ns.first)) { - local = m_tmp_tctx->mk_tmp_local(T); - locals.push_back(local); - variables.push_back(v_ns.first); - } else { - local = v_ns.first; - } - - expr term = zero; - expr term_ls = zero; - expr term_fused_ls = zero; - for_each(v_ns.second, [&](expr const & n) { - term = mk_app(f_add, mk_app(f_mul, v_ns.first, n), term); - term_ls = mk_app(f_add, mk_app(f_mul, local, n), term_ls); - term_fused_ls = mk_app(f_add, n, term_fused_ls); - }); - e_grp = mk_app(f_add, term, e_grp); - e_grp_ls = mk_app(f_add, term_ls, e_grp_ls); - e_fused_ls = mk_app(f_add, mk_app(f_mul, term_fused_ls, local), e_fused_ls); - } - - /* Prove (1) == (3) using simplify with [ac] */ - flet no_simplify_numerals(m_numerals, false); - auto pf_1_3 = prove(get_app_builder().mk_eq(e, e_grp), - get_simp_lemmas(g_ac_key)); - - if (!pf_1_3) { - diagnostic(env(), ios(), get_type_context()) << e << "\n\n =?=\n\n" << e_grp << "\n"; - throw blast_exception("Failed to prove (1) == (3) during fusion", e); - } - - /* Prove (4) == (5) using simplify with [som] */ - auto pf_4_5 = prove(get_app_builder().mk_eq(e_grp_ls, e_fused_ls), - get_simp_lemmas(g_som_key)); - - if (!pf_4_5) { - diagnostic(env(), ios(), get_type_context()) << e_grp_ls << "\n\n =?=\n\n" << e_fused_ls << "\n"; - throw blast_exception("Failed to prove (4) == (5) during fusion", e); - } - - /* Prove (5) == (6) using simplify with [numeral] */ - flet simplify_numerals(m_numerals, true); - result r_simp_ls = simplify(e_fused_ls, get_simp_lemmas(g_numeral_key)); - - /* Prove (4) == (6) by transitivity of proofs (2) and (3) */ - expr pf_4_6; - if (!r_simp_ls.has_proof()) pf_4_6 = *pf_4_5; - else pf_4_6 = get_app_builder().mk_eq_trans(*pf_4_5, r_simp_ls.get_proof()); - - /* Prove (3) == (7) by instantiating proof (4) */ - expr pf_3_7 = mk_app(Fun(locals, pf_4_6), variables); - - /* Prove (1) == (7) by transitivity of proofs (1) and (5) */ - expr pf_1_7 = get_app_builder().mk_eq_trans(*pf_1_3, pf_3_7); - - return result(mk_app(Fun(locals, r_simp_ls.get_new()), variables), pf_1_7); -} - -expr_pair simplifier::split_summand(expr const & e, expr const & f_mul, expr const & one) { - /* [e] is a possibly negated, possibly null product, where some of the multiplicands are numerals - and the rest are treated as variables. This method does the following conversion: - - (x1 * n1 * x2 * n3) ==> (-1 * n1 * n3) * (x1 * x2) */ - expr s = e; - expr numeral = one; - expr variable = one; - if (is_neg_app(s)) { - buffer args; - get_app_args(s, args); - numeral = get_app_builder().mk_app(get_neg_name(), one); - s = args[2]; - } - while (is_mul_app(s)) { - buffer args; - get_app_args(s, args); - expr const & multiplicand = args[2]; - if (is_num(multiplicand)) { - numeral = mk_app(f_mul, multiplicand, numeral); - } else { - if (variable == one) variable = multiplicand; - else variable = mk_app(f_mul, multiplicand, variable); - } - s = args[3]; - } - if (is_num(s)) { - numeral = mk_app(f_mul, s, numeral); - } else { - if (variable == one) variable = s; - else variable = mk_app(f_mul, s, variable); - } - return mk_pair(numeral, variable); -} - -/* Setup and teardown */ - -void initialize_simplifier() { - register_trace_class("simplifier"); - register_trace_class(name({"simplifier", "rewrite"})); - register_trace_class(name({"simplifier", "congruence"})); - register_trace_class(name({"simplifier", "failure"})); - - g_ac_key = register_simp_lemmas({name{"simplifier", "prove"}, name{"simplifier", "unit"}, - name{"simplifier", "neg"}, name{"simplifier", "ac"}}); - g_som_key = register_simp_lemmas({name{"simplifier", "prove"}, name{"simplifier", "unit"}, - name{"simplifier", "neg"}, name{"simplifier", "ac"}, name{"simplifier", "distrib"}}); - g_numeral_key = register_simp_lemmas({name{"simplifier", "unit"}, name{"simplifier", "neg"}, name{"simplifier", "ac"}}); - - g_simplify_max_steps = new name{"simplify", "max_steps"}; - g_simplify_top_down = new name{"simplify", "top_down"}; - g_simplify_exhaustive = new name{"simplify", "exhaustive"}; - g_simplify_memoize = new name{"simplify", "memoize"}; - g_simplify_contextual = new name{"simplify", "contextual"}; - g_simplify_expand_macros = new name{"simplify", "expand_macros"}; - g_simplify_fuse = new name{"simplify", "fuse"}; - g_simplify_numerals = new name{"simplify", "numerals"}; - - register_unsigned_option(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS, - "(simplify) max allowed steps in simplification"); - register_bool_option(*g_simplify_top_down, LEAN_DEFAULT_SIMPLIFY_TOP_DOWN, - "(simplify) use top-down rewriting instead of bottom-up"); - register_bool_option(*g_simplify_exhaustive, LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE, - "(simplify) rewrite exhaustively"); - register_bool_option(*g_simplify_memoize, LEAN_DEFAULT_SIMPLIFY_MEMOIZE, - "(simplify) memoize simplifications"); - register_bool_option(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL, - "(simplify) use contextual simplification"); - register_bool_option(*g_simplify_expand_macros, LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS, - "(simplify) expand macros"); - register_bool_option(*g_simplify_fuse, LEAN_DEFAULT_SIMPLIFY_FUSE, - "(simplify) fuse addition in distrib structures"); - register_bool_option(*g_simplify_numerals, LEAN_DEFAULT_SIMPLIFY_NUMERALS, - "(simplify) simplify (+, *, -, /) over numerals"); -} - -void finalize_simplifier() { - delete g_simplify_numerals; - delete g_simplify_fuse; - delete g_simplify_expand_macros; - delete g_simplify_contextual; - delete g_simplify_memoize; - delete g_simplify_exhaustive; - delete g_simplify_top_down; - delete g_simplify_max_steps; -} - -/* Entry points */ -static bool simplify_all_pred(expr const &) { return true; } - -result simplify(name const & rel, expr const & e, simp_lemmas const & srss) { - return simplifier(rel, simplify_all_pred)(e, srss); -} - -result simplify(name const & rel, expr const & e, simp_lemmas const & srss, expr_predicate const & simp_pred) { - return simplifier(rel, simp_pred)(e, srss); -} - -}} diff --git a/src/library/blast/simplifier/simplifier_actions.cpp b/src/library/blast/simplifier/simplifier_actions.cpp deleted file mode 100644 index 77c2a4fe79..0000000000 --- a/src/library/blast/simplifier/simplifier_actions.cpp +++ /dev/null @@ -1,149 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "library/attribute_manager.h" -#include "library/constants.h" -#include "library/util.h" -#include "library/blast/blast.h" -#include "library/blast/trace.h" -#include "library/blast/options.h" -#include "library/blast/simplifier/simplifier.h" -#include "library/blast/simplifier/ceqv.h" - -namespace lean { -namespace blast { -static unsigned g_ext_id = 0; -struct simplifier_branch_extension : public branch_extension { - simp_lemmas m_simp_lemmas; - bool m_simp_target{false}; // true if target needs to be simplified again - simplifier_branch_extension() {} - simplifier_branch_extension(simplifier_branch_extension const & b): - m_simp_lemmas(b.m_simp_lemmas) {} - virtual ~simplifier_branch_extension() {} - virtual branch_extension * clone() override { return new simplifier_branch_extension(*this); } - virtual void initialized() override { m_simp_lemmas = ::lean::blast::get_simp_lemmas(); } - virtual void target_updated() override { m_simp_target = true; } - virtual void hypothesis_activated(hypothesis const &, hypothesis_idx) override { } - virtual void hypothesis_deleted(hypothesis const &, hypothesis_idx) override { } - simp_lemmas const & get_simp_lemmas() const { return m_simp_lemmas; } -}; - -void initialize_simplifier_actions() { - g_ext_id = register_branch_extension(new simplifier_branch_extension()); -} - -void finalize_simplifier_actions() { -} - -static simplifier_branch_extension & get_extension() { - return static_cast(curr_state().get_extension(g_ext_id)); -} - -static bool use_iff(expr const & target) { - return is_standard(env()) && is_prop(target); -} - -class simplify_target_proof_step_cell : public proof_step_cell { - bool m_iff; - expr m_eq_pr; -public: - simplify_target_proof_step_cell(bool iff, expr const & eq_pr): - m_iff(iff), m_eq_pr(eq_pr) {} - - virtual ~simplify_target_proof_step_cell() {} - - virtual action_result resolve(expr const & pr) const override { - try { - app_builder & b = get_app_builder(); - if (m_iff) - return action_result::solved(b.mk_app(get_iff_mpr_name(), m_eq_pr, pr)); - else - return action_result::solved(b.mk_app(get_eq_mpr_name(), m_eq_pr, pr)); - } catch (app_builder_exception &) { - return action_result::failed(); - } - } -}; - -action_result simplify_target_action() { - if (!get_config().m_simp) - return action_result::failed(); - auto & ext = get_extension(); - if (!ext.m_simp_target) - return action_result::failed(); // nothing to be done - ext.m_simp_target = false; - state & s = curr_state(); - expr target = s.get_target(); - bool iff = use_iff(target); - name rname = iff ? get_iff_name() : get_eq_name(); - auto r = simplify(rname, target, ext.get_simp_lemmas()); - if (r.get_new() == target) - return action_result::failed(); // did nothing - if (r.has_proof()) { - // Remark: we only need to create the proof step if a proof was generated. - // If a proof was not generated and the resulting expression is not - // structurally equal, then they are definitionally equal and no proof is - // needed - s.push_proof_step(new simplify_target_proof_step_cell(iff, r.get_proof())); - } - s.set_target(r.get_new()); - trace_action("simplify"); - return action_result::new_branch(); -} - -action_result simplify_hypothesis_action(hypothesis_idx hidx) { - if (!get_config().m_simp) - return action_result::failed(); - state & s = curr_state(); - if (s.has_target_forward_deps(hidx)) { - // We currently do not try to simplify a hypothesis if other - // hypotheses or target depends on it. - return action_result::failed(); - } - hypothesis const & h = s.get_hypothesis_decl(hidx); - if (!is_prop(h.get_type())) { - // We currently only simplify propositions. - return action_result::failed(); - } - auto & ext = get_extension(); - auto r = simplify(get_iff_name(), h.get_type(), ext.get_simp_lemmas()); - if (r.get_new() == h.get_type()) - return action_result::failed(); // did nothing - expr new_h_proof; - if (r.has_proof()) { - new_h_proof = get_app_builder().mk_app(get_iff_mp_name(), r.get_proof(), h.get_self()); - } else { - // they are definitionally equal - new_h_proof = h.get_self(); - } - if (!is_true(r.get_new())) - s.mk_hypothesis(r.get_new(), new_h_proof); - s.del_hypothesis(hidx); - return action_result::new_branch(); -} - -action_result add_simp_lemma_action(hypothesis_idx hidx) { - if (!get_config().m_simp) - return action_result::failed(); - blast_tmp_type_context ctx; - state & s = curr_state(); - hypothesis const & h = s.get_hypothesis_decl(hidx); - list ps = to_ceqvs(*ctx, h.get_type(), h.get_self()); - if (!ps) - return action_result::failed(); - auto & ext = get_extension(); - bool added = false; - for (auto const & p : ps) { - try { - ext.m_simp_lemmas = add(*ctx, ext.m_simp_lemmas, h.get_name(), p.first, p.second, LEAN_DEFAULT_PRIORITY); - added = true; - } catch (exception &) { - // TODO(Leo, Daniel): store event - } - } - return added ? action_result::new_branch() : action_result::failed(); -} -}} diff --git a/src/library/blast/simplifier/simplifier_actions.h b/src/library/blast/simplifier/simplifier_actions.h deleted file mode 100644 index 30f7d07ace..0000000000 --- a/src/library/blast/simplifier/simplifier_actions.h +++ /dev/null @@ -1,18 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/blast/hypothesis.h" -#include "library/blast/action_result.h" -namespace lean { -namespace blast { -action_result simplify_hypothesis_action(hypothesis_idx hidx); -action_result simplify_target_action(); -action_result add_simp_lemma_action(hypothesis_idx hidx); - -void initialize_simplifier_actions(); -void finalize_simplifier_actions(); -}} diff --git a/src/library/blast/simplifier/simplifier_strategies.cpp b/src/library/blast/simplifier/simplifier_strategies.cpp deleted file mode 100644 index 0b0237f052..0000000000 --- a/src/library/blast/simplifier/simplifier_strategies.cpp +++ /dev/null @@ -1,71 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "library/blast/strategy.h" -#include "library/blast/simplifier/simplifier_actions.h" -#include "library/blast/actions/simple_actions.h" -#include "library/blast/actions/intros_action.h" -#include "library/blast/actions/subst_action.h" -#include "library/blast/actions/no_confusion_action.h" - -namespace lean { -namespace blast { - -class simplifier_strategy_fn : public strategy_fn { - bool m_simp_target; - bool m_simp_hyps; - bool m_use_hyps; - - virtual char const * get_name() const override { return "simp"; } - - virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override { - Try(assumption_contradiction_actions(hidx)); - if (m_simp_hyps) { - Try(simplify_hypothesis_action(hidx)); - } - Try(no_confusion_action(hidx)); - Try(discard_action(hidx)); - if (m_use_hyps) - Try(subst_action(hidx)); - return action_result::new_branch(); - } - - virtual action_result hypothesis_post_activation(hypothesis_idx hidx) override { - if (m_use_hyps) - add_simp_lemma_action(hidx); - return action_result::new_branch(); - } - - virtual action_result next_action() override { - if (m_simp_hyps || m_use_hyps) { - Try(intros_action()); - Try(assumption_action()); - Try(activate_hypothesis()); - } - if (m_simp_target) { - Try(simplify_target_action()); - } - Try(trivial_action()); - return action_result::failed(); - } -public: - simplifier_strategy_fn(bool simp_target, bool simp_hyps, bool use_hyps): - m_simp_target(simp_target), m_simp_hyps(simp_hyps), - m_use_hyps(use_hyps) {} -}; - -strategy mk_simplify_target_strategy() { - return []() { return simplifier_strategy_fn(true, false, false)(); }; // NOLINT -} - -strategy mk_simplify_all_strategy() { - return []() { return simplifier_strategy_fn(true, true, false)(); }; // NOLINT -} - -strategy mk_simplify_using_hypotheses_strategy() { - return []() { return simplifier_strategy_fn(true, true, true)(); }; // NOLINT -} -}} diff --git a/src/library/blast/simplifier/simplifier_strategies.h b/src/library/blast/simplifier/simplifier_strategies.h deleted file mode 100644 index eed9d2c99d..0000000000 --- a/src/library/blast/simplifier/simplifier_strategies.h +++ /dev/null @@ -1,15 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/blast/strategy.h" - -namespace lean { -namespace blast { -strategy mk_simplify_target_strategy(); -strategy mk_simplify_all_strategy(); -strategy mk_simplify_using_hypotheses_strategy(); -}} diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp index b3a5138b81..668c0376d5 100644 --- a/src/library/local_context.cpp +++ b/src/library/local_context.cpp @@ -181,16 +181,16 @@ void local_context::clear(local_decl const & d) { bool local_context::is_subset_of(name_set const & ls) const { // TODO(Leo): we can improve performance by implementing the subset operation in the rb_map/rb_tree class - return !m_name2local_decl.find_if([&](name const & n, local_decl const &) { - return !ls.contains(n); - }); + return !static_cast(m_name2local_decl.find_if([&](name const & n, local_decl const &) { + return !ls.contains(n); + })); } bool local_context::is_subset_of(local_context const & ctx) const { // TODO(Leo): we can improve performance by implementing the subset operation in the rb_map/rb_tree class - return !m_name2local_decl.find_if([&](name const & n, local_decl const &) { - return !ctx.m_name2local_decl.contains(n); - }); + return !static_cast(m_name2local_decl.find_if([&](name const & n, local_decl const &) { + return !ctx.m_name2local_decl.contains(n); + })); } local_context local_context::remove(buffer const & locals) const { diff --git a/src/library/old_tactic/tactic/norm_num_tactic.cpp b/src/library/old_tactic/tactic/norm_num_tactic.cpp index 107ade9f3c..36c5ce4b33 100644 --- a/src/library/old_tactic/tactic/norm_num_tactic.cpp +++ b/src/library/old_tactic/tactic/norm_num_tactic.cpp @@ -8,7 +8,7 @@ Author: Robert Y. Lewis #include "library/reducible.h" #include "library/normalize.h" #include "library/norm_num.h" -#include "library/tmp_type_context.h" +#include "library/old_tmp_type_context.h" #include "library/tactic/expr_to_tactic.h" namespace lean { @@ -32,7 +32,7 @@ tactic norm_num_tactic() { buffer hyps; g.get_hyps(hyps); try { - tmp_type_context ctx(env, ios.get_options()); + old_tmp_type_context ctx(env, ios.get_options()); ctx.set_local_instances(to_list(hyps)); pair p = mk_norm_num(ctx, lhs); expr new_lhs = p.first; diff --git a/src/library/tmp_type_context.cpp b/src/library/old_tmp_type_context.cpp similarity index 75% rename from src/library/tmp_type_context.cpp rename to src/library/old_tmp_type_context.cpp index 1ee323bc74..e00ca822e0 100644 --- a/src/library/tmp_type_context.cpp +++ b/src/library/old_tmp_type_context.cpp @@ -4,26 +4,26 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "library/tmp_type_context.h" +#include "library/old_tmp_type_context.h" #include "library/idx_metavar.h" namespace lean { -void tmp_type_context::init(environment const & env, reducible_behavior b) { +void old_tmp_type_context::init(environment const & env, reducible_behavior b) { switch (b) { case UnfoldReducible: m_opaque_pred = mk_not_reducible_pred(env); break; case UnfoldSemireducible: m_opaque_pred = mk_irreducible_pred(env); break; } } -tmp_type_context::tmp_type_context(environment const & env, options const & o, reducible_behavior b): +old_tmp_type_context::old_tmp_type_context(environment const & env, options const & o, reducible_behavior b): old_type_context(env, o) { init(env, b); } -tmp_type_context::~tmp_type_context() { +old_tmp_type_context::~old_tmp_type_context() { } -void tmp_type_context::clear() { +void old_tmp_type_context::clear() { m_uassignment.clear(); m_eassignment.clear(); m_trail.clear(); @@ -31,27 +31,27 @@ void tmp_type_context::clear() { clear_infer_cache(); } -void tmp_type_context::set_next_uvar_idx(unsigned next_idx) { +void old_tmp_type_context::set_next_uvar_idx(unsigned next_idx) { lean_assert(m_uassignment.empty()); lean_assert(m_scopes.empty()); m_uassignment.resize(next_idx); } -void tmp_type_context::set_next_mvar_idx(unsigned next_idx) { +void old_tmp_type_context::set_next_mvar_idx(unsigned next_idx) { lean_assert(m_eassignment.empty()); lean_assert(m_scopes.empty()); m_eassignment.resize(next_idx); } -bool tmp_type_context::is_uvar(level const & l) const { +bool old_tmp_type_context::is_uvar(level const & l) const { return is_idx_metauniv(l); } -bool tmp_type_context::is_mvar(expr const & e) const { +bool old_tmp_type_context::is_mvar(expr const & e) const { return is_idx_metavar(e); } -optional tmp_type_context::get_assignment(level const & u) const { +optional old_tmp_type_context::get_assignment(level const & u) const { unsigned idx = to_meta_idx(u); // if the following assetion is violated, we have two options: // 1- We should create the meta-variable using mk_uvar @@ -61,7 +61,7 @@ optional tmp_type_context::get_assignment(level const & u) const { return m_uassignment[idx]; } -optional tmp_type_context::get_assignment(expr const & m) const { +optional old_tmp_type_context::get_assignment(expr const & m) const { unsigned idx = to_meta_idx(m); // if the following assetion is violated, we have two options: // 1- We should create the meta-variable using mk_mvar @@ -71,7 +71,7 @@ optional tmp_type_context::get_assignment(expr const & m) const { return m_eassignment[idx]; } -void tmp_type_context::update_assignment(level const & u, level const & v) { +void old_tmp_type_context::update_assignment(level const & u, level const & v) { unsigned idx = to_meta_idx(u); lean_assert(idx < m_uassignment.size()); // see comments above lean_assert(!m_uassignment[idx]); @@ -80,7 +80,7 @@ void tmp_type_context::update_assignment(level const & u, level const & v) { m_trail.emplace_back(trail_kind::Level, idx); } -void tmp_type_context::update_assignment(expr const & m, expr const & v) { +void old_tmp_type_context::update_assignment(expr const & m, expr const & v) { unsigned idx = to_meta_idx(m); lean_assert(idx < m_eassignment.size()); // see comments above // Remark: type class resolution may update an already assigned meta-variable with a @@ -93,19 +93,19 @@ void tmp_type_context::update_assignment(expr const & m, expr const & v) { m_trail.emplace_back(trail_kind::Expr, idx); } -level tmp_type_context::mk_uvar() { +level old_tmp_type_context::mk_uvar() { unsigned idx = m_uassignment.size(); m_uassignment.push_back(none_level()); return mk_idx_metauniv(idx); } -expr tmp_type_context::mk_mvar(expr const & type) { +expr old_tmp_type_context::mk_mvar(expr const & type) { unsigned idx = m_eassignment.size(); m_eassignment.push_back(none_expr()); return mk_idx_metavar(idx, type); } -void tmp_type_context::push_core() { +void old_tmp_type_context::push_core() { m_scopes.push_back(scope()); scope & s = m_scopes.back(); s.m_uassignment_sz = m_uassignment.size(); @@ -113,7 +113,7 @@ void tmp_type_context::push_core() { s.m_trail_sz = m_trail.size(); } -void tmp_type_context::pop_core() { +void old_tmp_type_context::pop_core() { lean_assert(!m_scopes.empty()); scope const & s = m_scopes.back(); unsigned old_sz = s.m_trail_sz; @@ -133,11 +133,11 @@ void tmp_type_context::pop_core() { m_scopes.pop_back(); } -unsigned tmp_type_context::get_num_check_points() const { +unsigned old_tmp_type_context::get_num_check_points() const { return m_scopes.size(); } -void tmp_type_context::commit() { +void old_tmp_type_context::commit() { lean_assert(!m_scopes.empty()); m_scopes.pop_back(); } diff --git a/src/library/tmp_type_context.h b/src/library/old_tmp_type_context.h similarity index 81% rename from src/library/tmp_type_context.h rename to src/library/old_tmp_type_context.h index 96bf2e05bd..3c4a4f4320 100644 --- a/src/library/tmp_type_context.h +++ b/src/library/old_tmp_type_context.h @@ -28,7 +28,7 @@ namespace lean { \remark The local context is set using the method set_context from type_context. */ -class tmp_type_context : public old_type_context { +class old_tmp_type_context : public old_type_context { name_predicate m_opaque_pred; std::vector> m_uassignment; std::vector> m_eassignment; @@ -43,8 +43,8 @@ class tmp_type_context : public old_type_context { std::vector m_scopes; void init(environment const & env, reducible_behavior b); public: - tmp_type_context(environment const & env, options const & o, reducible_behavior b = UnfoldReducible); - virtual ~tmp_type_context(); + old_tmp_type_context(environment const & env, options const & o, reducible_behavior b = UnfoldReducible); + virtual ~old_tmp_type_context(); /** \brief Reset the state: backtracking stack, indices and assignment. */ void clear(); @@ -91,23 +91,23 @@ public: } }; -class tmp_type_context_pool { +class old_tmp_type_context_pool { public: - virtual tmp_type_context * mk_tmp_type_context() =0; - virtual void recycle_tmp_type_context(tmp_type_context * tmp_tctx) =0; + virtual old_tmp_type_context * mk_old_tmp_type_context() =0; + virtual void recycle_old_tmp_type_context(old_tmp_type_context * tmp_tctx) =0; - virtual ~tmp_type_context_pool() {} + virtual ~old_tmp_type_context_pool() {} }; -class default_tmp_type_context_pool : public tmp_type_context_pool { +class default_old_tmp_type_context_pool : public old_tmp_type_context_pool { environment m_env; options m_options; public: - default_tmp_type_context_pool(environment const & env, options const & o): + default_old_tmp_type_context_pool(environment const & env, options const & o): m_env(env), m_options(o) {} - virtual tmp_type_context * mk_tmp_type_context() override { return new tmp_type_context(m_env, m_options); } - virtual void recycle_tmp_type_context(tmp_type_context * tmp_tctx) override { delete tmp_tctx; } + virtual old_tmp_type_context * mk_old_tmp_type_context() override { return new old_tmp_type_context(m_env, m_options); } + virtual void recycle_old_tmp_type_context(old_tmp_type_context * tmp_tctx) override { delete tmp_tctx; } }; } diff --git a/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp b/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp index 22ff95390c..0690b7fc19 100644 --- a/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp +++ b/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp @@ -13,8 +13,8 @@ Author: Daniel Selsam #include "library/util.h" #include "library/expr_lt.h" #include "library/scoped_ext.h" -#include "library/tmp_type_context.h" #include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h" +#include "library/old_tmp_type_context.h" namespace lean { @@ -37,7 +37,7 @@ struct defeq_simp_lemmas_state { defeq_simp_lemmas m_defeq_simp_lemmas; name_map m_decl_name_to_prio; // Note: redundant but convenient - void register_defeq_simp_lemma(tmp_type_context & tctx, name const & decl_name, unsigned priority) { + void register_defeq_simp_lemma(old_tmp_type_context & tctx, name const & decl_name, unsigned priority) { declaration const & d = tctx.env().get(decl_name); // TODO(dhs): once we refactor to register this attribute as "definitions-only", this can be an assert if (!d.is_definition()) { @@ -54,7 +54,7 @@ struct defeq_simp_lemmas_state { return register_defeq_simp_lemma_core(tctx, decl_name, ls, type, proof, priority); } - void register_defeq_simp_lemma_core(tmp_type_context & tctx, name const & decl_name, levels const & umetas, + void register_defeq_simp_lemma_core(old_tmp_type_context & tctx, name const & decl_name, levels const & umetas, expr const & type, expr const & proof, unsigned priority) { m_decl_name_to_prio.insert(decl_name, priority); expr rule = type; @@ -92,7 +92,7 @@ struct defeq_simp_lemmas_config { typedef defeq_simp_lemmas_state state; static void add_entry(environment const & env, io_state const & ios, state & s, entry const & e) { - tmp_type_context tctx(env, ios.get_options()); + old_tmp_type_context tctx(env, ios.get_options()); s.register_defeq_simp_lemma(tctx, e.m_decl_name, e.m_priority); } static name const & get_class_name() { @@ -134,7 +134,7 @@ defeq_simp_lemmas get_defeq_simp_lemmas(environment const & env, name const & ns if (_entries) { list entries = reverse(*_entries); for (auto const & e : entries) { - tmp_type_context tctx(env, get_dummy_ios().get_options()); + old_tmp_type_context tctx(env, get_dummy_ios().get_options()); s.register_defeq_simp_lemma(tctx, e.m_decl_name, e.m_priority); } } diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 927db5a4cd..cf84abdc17 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -19,6 +19,7 @@ Author: Leonardo de Moura #include "library/tactic/congr_lemma_tactics.h" #include "library/tactic/elaborate.h" #include "library/tactic/defeq_simplifier/init_module.h" +#include "library/tactic/simplifier/init_module.h" namespace lean { void initialize_tactic_module() { @@ -37,9 +38,11 @@ void initialize_tactic_module() { initialize_congr_lemma_tactics(); initialize_elaborate(); initialize_defeq_simplifier_module(); + initialize_simplifier_module(); } void finalize_tactic_module() { finalize_defeq_simplifier_module(); + finalize_simplifier_module(); finalize_elaborate(); finalize_congr_lemma_tactics(); finalize_fun_info_tactics(); diff --git a/src/library/tactic/simplifier/CMakeLists.txt b/src/library/tactic/simplifier/CMakeLists.txt new file mode 100644 index 0000000000..e8b1f07baa --- /dev/null +++ b/src/library/tactic/simplifier/CMakeLists.txt @@ -0,0 +1 @@ +add_library(simplifier OBJECT init_module.cpp ceqv.cpp simplifier.cpp simp_lemmas.cpp) diff --git a/src/library/blast/simplifier/ceqv.cpp b/src/library/tactic/simplifier/ceqv.cpp similarity index 91% rename from src/library/blast/simplifier/ceqv.cpp rename to src/library/tactic/simplifier/ceqv.cpp index 9e812ed2d0..a419c73023 100644 --- a/src/library/blast/simplifier/ceqv.cpp +++ b/src/library/tactic/simplifier/ceqv.cpp @@ -10,10 +10,10 @@ Author: Leonardo de Moura #include "library/constants.h" #include "library/util.h" #include "library/relation_manager.h" -#include "library/blast/simplifier/ceqv.h" +#include "library/tactic/simplifier/ceqv.h" namespace lean { -bool is_ceqv(tmp_type_context & tctx, expr e); +bool is_ceqv(type_context & tctx, expr e); bool is_simp_relation(environment const & env, name const & n) { return is_trans_relation(env, n) && is_refl_relation(env, n); @@ -22,7 +22,7 @@ bool is_simp_relation(environment const & env, name const & n) { /** \brief Auxiliary functional object for creating "conditional equations" */ class to_ceqvs_fn { environment const & m_env; - tmp_type_context & m_tctx; + type_context & m_tctx; static list mk_singleton(expr const & e, expr const & H) { return list(mk_pair(e, H)); @@ -41,7 +41,7 @@ class to_ceqvs_fn { list lift(expr const & local, list const & l) { lean_assert(is_local(local)); return map(l, [&](expr_pair const & e_H) { - return mk_pair(Pi(local, e_H.first), Fun(local, e_H.second)); + return mk_pair(m_tctx.mk_pi({local}, e_H.first), m_tctx.mk_lambda({local}, e_H.second)); }); } @@ -66,8 +66,8 @@ class to_ceqvs_fn { auto r2 = apply(arg2, H2, restricted); return append(r1, r2); } else if (is_pi(e)) { - // TODO(dhs): keep name? - expr local = m_tctx.mk_tmp_local(binding_domain(e), binding_info(e)); + type_context::tmp_locals local_factory(m_tctx); + expr local = local_factory.push_local_from_binding(e); expr new_e = instantiate(binding_body(e), local); expr new_H = mk_app(H, local); auto r = apply(new_e, new_H, restricted); @@ -82,8 +82,9 @@ class to_ceqvs_fn { } else if (is_standard(m_env) && is_ite(e, c, Hdec, A, arg1, arg2) && is_prop(e)) { // TODO(Leo): support HoTT mode if users request expr not_c = mk_app(mk_constant(get_not_name()), c); - expr Hc = m_tctx.mk_tmp_local(c); - expr Hnc = m_tctx.mk_tmp_local(not_c); + type_context::tmp_locals local_factory(m_tctx); + expr Hc = local_factory.push_local(name(), c); + expr Hnc = local_factory.push_local(name(), not_c); expr H1 = mk_app({mk_constant(get_implies_of_if_pos_name()), c, arg1, arg2, Hdec, e, Hc}); expr H2 = mk_app({mk_constant(get_implies_of_if_neg_name()), @@ -109,7 +110,7 @@ class to_ceqvs_fn { } } public: - to_ceqvs_fn(tmp_type_context & tctx):m_env(tctx.env()), m_tctx(tctx) {} + to_ceqvs_fn(type_context & tctx):m_env(tctx.env()), m_tctx(tctx) {} list operator()(expr const & e, expr const & H) { bool restricted = false; @@ -118,7 +119,7 @@ public: } }; -list to_ceqvs(tmp_type_context & tctx, expr const & e, expr const & H) { +list to_ceqvs(type_context & tctx, expr const & e, expr const & H) { return to_ceqvs_fn(tctx)(e, H); } @@ -140,7 +141,7 @@ bool is_simp_relation(environment const & env, expr const & e, expr & lhs, expr return is_simp_relation(env, e, rel, lhs, rhs); } -bool is_ceqv(tmp_type_context & tctx, expr e) { +bool is_ceqv(type_context & tctx, expr e) { if (has_expr_metavar(e)) return false; name_set to_find; @@ -158,6 +159,7 @@ bool is_ceqv(tmp_type_context & tctx, expr e) { environment const & env = tctx.env(); bool is_std = is_standard(env); buffer hypotheses; // arguments that are propositions + type_context::tmp_locals local_factory(tctx); while (is_pi(e)) { if (!to_find.empty()) { // Support for dependent types. @@ -165,7 +167,7 @@ bool is_ceqv(tmp_type_context & tctx, expr e) { // by matching the type. for_each(binding_domain(e), visitor_fn); } - expr local = tctx.mk_tmp_local(binding_domain(e)); + expr local = local_factory.push_local(name(), binding_domain(e)); if (binding_info(e).is_inst_implicit()) { // If the argument can be instantiated by type class resolution, then // we don't need to find it in the lhs diff --git a/src/library/blast/simplifier/ceqv.h b/src/library/tactic/simplifier/ceqv.h similarity index 77% rename from src/library/blast/simplifier/ceqv.h rename to src/library/tactic/simplifier/ceqv.h index b6e5868a8f..06939100d3 100644 --- a/src/library/blast/simplifier/ceqv.h +++ b/src/library/tactic/simplifier/ceqv.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "library/tmp_type_context.h" +#include "library/type_context.h" #include "library/expr_pair.h" namespace lean { @@ -14,7 +14,7 @@ bool is_simp_relation(environment const & env, expr const & e, expr & rel, expr a "conditional" rewriting rule. Any equivalence relation registered using the relation_manager is considered. */ -list to_ceqvs(tmp_type_context & tctx, expr const & e, expr const & H); -bool is_ceqv(tmp_type_context & tctx, expr e); +list to_ceqvs(type_context & tctx, expr const & e, expr const & H); +bool is_ceqv(type_context & tctx, expr e); bool is_permutation_ceqv(environment const & env, expr e); } diff --git a/src/library/blast/simplifier/init_module.cpp b/src/library/tactic/simplifier/init_module.cpp similarity index 59% rename from src/library/blast/simplifier/init_module.cpp rename to src/library/tactic/simplifier/init_module.cpp index 4841465f91..e6a2721ff2 100644 --- a/src/library/blast/simplifier/init_module.cpp +++ b/src/library/tactic/simplifier/init_module.cpp @@ -3,22 +3,18 @@ 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/blast/simplifier/simplifier_actions.h" -#include "library/blast/simplifier/simp_lemmas.h" -#include "library/blast/simplifier/simplifier.h" +#include "library/tactic/simplifier/simp_lemmas.h" +#include "library/tactic/simplifier/simplifier.h" namespace lean { -namespace blast { void initialize_simplifier_module() { initialize_simp_lemmas(); initialize_simplifier(); - initialize_simplifier_actions(); } void finalize_simplifier_module() { - finalize_simplifier_actions(); finalize_simplifier(); finalize_simp_lemmas(); } -}} +} diff --git a/src/library/blast/simplifier/init_module.h b/src/library/tactic/simplifier/init_module.h similarity index 92% rename from src/library/blast/simplifier/init_module.h rename to src/library/tactic/simplifier/init_module.h index 7b63f5b9d8..fcdafb04ad 100644 --- a/src/library/blast/simplifier/init_module.h +++ b/src/library/tactic/simplifier/init_module.h @@ -6,8 +6,6 @@ Author: Daniel Selsam #pragma once namespace lean { -namespace blast { void initialize_simplifier_module(); void finalize_simplifier_module(); } -} diff --git a/src/library/blast/simplifier/simp_lemmas.cpp b/src/library/tactic/simplifier/simp_lemmas.cpp similarity index 80% rename from src/library/blast/simplifier/simp_lemmas.cpp rename to src/library/tactic/simplifier/simp_lemmas.cpp index f67ccad1fc..17c7c77ad4 100644 --- a/src/library/blast/simplifier/simp_lemmas.cpp +++ b/src/library/tactic/simplifier/simp_lemmas.cpp @@ -8,17 +8,21 @@ Author: Leonardo de Moura #include #include "util/priority_queue.h" #include "util/sstream.h" +#include "util/flet.h" #include "kernel/error_msgs.h" #include "kernel/find_fn.h" #include "kernel/instantiate.h" #include "library/trace.h" #include "library/scoped_ext.h" #include "library/attribute_manager.h" -#include "library/blast/blast.h" -#include "library/blast/simplifier/ceqv.h" -#include "library/blast/simplifier/simp_lemmas.h" +#include "library/type_context.h" +#include "library/tactic/tactic_state.h" +#include "library/tactic/simplifier/ceqv.h" +#include "library/tactic/simplifier/simp_lemmas.h" namespace lean { + +/* The environment extension */ static name * g_class_name = nullptr; static std::string * g_key = nullptr; @@ -67,22 +71,29 @@ struct simp_config { typedef scoped_ext simp_ext; -void validate_simp(environment const & env, io_state const & ios, name const & n); -void validate_congr(environment const & env, io_state const & ios, name const & n); +/* Validation */ + +LEAN_THREAD_VALUE(bool, g_throw_ex, false); +void validate_simp(type_context & tctx, name const & n); +void validate_congr(type_context & tctx, name const & n); + +/* Registering simp/congr lemmas */ environment add_simp_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent) { - validate_simp(env, ios, c); + aux_type_context aux_ctx(env); + type_context & tctx = aux_ctx.get(); + validate_simp(tctx, c); return simp_ext::add_entry(env, ios, simp_entry(true, prio, c), ns, persistent); } environment add_congr_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent) { - validate_congr(env, ios, c); + aux_type_context aux_ctx(env); + type_context & tctx = aux_ctx.get(); + validate_congr(tctx, c); return simp_ext::add_entry(env, ios, simp_entry(false, prio, c), ns, persistent); } -bool is_simp_lemma(environment const & env, name const & c) { - return simp_ext::get_state(env).m_simp_lemmas.contains(c); -} +/* Getters/checkers */ unsigned get_simp_lemma_priority(environment const & env, name const & n) { if (auto r = simp_ext::get_state(env).m_simp_lemmas.get_prio(n)) @@ -91,29 +102,22 @@ unsigned get_simp_lemma_priority(environment const & env, name const & n) { return LEAN_DEFAULT_PRIORITY; } +bool is_simp_lemma(environment const & env, name const & c) { + return simp_ext::get_state(env).m_simp_lemmas.contains(c); +} + bool is_congr_lemma(environment const & env, name const & c) { return simp_ext::get_state(env).m_congr_lemmas.contains(c); } -void get_simp_lemmas(environment const & env, buffer & r) { +void get_simp_lemma_names(environment const & env, buffer & r) { return simp_ext::get_state(env).m_simp_lemmas.to_buffer(r); } -void get_congr_lemmas(environment const & env, buffer & r) { +void get_congr_lemma_names(environment const & env, buffer & r) { return simp_ext::get_state(env).m_congr_lemmas.to_buffer(r); } -static std::vector> * g_simp_lemma_ns = nullptr; - -unsigned register_simp_lemmas(std::initializer_list const & nss) { - unsigned r = g_simp_lemma_ns->size(); - g_simp_lemma_ns->push_back(std::vector(nss)); - return r; -} - -namespace blast { -LEAN_THREAD_VALUE(bool, g_throw_ex, false); - static void report_failure(sstream const & strm) { if (g_throw_ex){ throw exception(strm); @@ -123,26 +127,29 @@ static void report_failure(sstream const & strm) { } } -simp_lemmas add_core(tmp_type_context & tctx, simp_lemmas const & s, +simp_lemmas add_core(tmp_type_context & tmp_tctx, simp_lemmas const & s, name const & id, levels const & univ_metas, expr const & e, expr const & h, unsigned priority) { - list ceqvs = to_ceqvs(tctx, e, h); + list ceqvs = to_ceqvs(tmp_tctx.tctx(), e, h); if (is_nil(ceqvs)) { report_failure(sstream() << "invalid [simp] lemma '" << id << "'"); } - environment const & env = tctx.env(); + environment const & env = tmp_tctx.tctx().env(); simp_lemmas new_s = s; for (expr_pair const & p : ceqvs) { - expr rule = normalizer(tctx)(p.first); - expr proof = tctx.whnf(p.second); + /* We only clear the eassignment since we want to reuse the temporary universe metavariables associated + with the declaration. */ + tmp_tctx.clear_eassignment(); + expr rule = tmp_tctx.whnf(p.first); + expr proof = tmp_tctx.whnf(p.second); bool is_perm = is_permutation_ceqv(env, rule); buffer emetas; buffer instances; while (is_pi(rule)) { - expr mvar = tctx.mk_mvar(binding_domain(rule)); + expr mvar = tmp_tctx.mk_tmp_mvar(binding_domain(rule)); emetas.push_back(mvar); instances.push_back(binding_info(rule).is_inst_implicit()); - rule = tctx.whnf(instantiate(binding_body(rule), mvar)); + rule = tmp_tctx.whnf(instantiate(binding_body(rule), mvar)); proof = mk_app(proof, mvar); } expr rel, lhs, rhs; @@ -154,8 +161,9 @@ simp_lemmas add_core(tmp_type_context & tctx, simp_lemmas const & s, return new_s; } -simp_lemmas add(tmp_type_context & tctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, unsigned priority) { - return add_core(tctx, s, id, list(), e, h, priority); +simp_lemmas add(type_context & tctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, unsigned priority) { + tmp_type_context tmp_tctx(tctx); + return add_core(tmp_tctx, s, id, list(), e, h, priority); } simp_lemmas join(simp_lemmas const & s1, simp_lemmas const & s2) { @@ -166,17 +174,17 @@ simp_lemmas join(simp_lemmas const & s1, simp_lemmas const & s2) { return new_s1; } -static simp_lemmas add_core(tmp_type_context & tctx, simp_lemmas const & s, name const & cname, unsigned priority) { - declaration const & d = tctx.env().get(cname); +static simp_lemmas add_core(tmp_type_context & tmp_tctx, simp_lemmas const & s, name const & cname, unsigned priority) { + declaration const & d = tmp_tctx.tctx().env().get(cname); buffer us; unsigned num_univs = d.get_num_univ_params(); for (unsigned i = 0; i < num_univs; i++) { - us.push_back(tctx.mk_uvar()); + us.push_back(tmp_tctx.mk_tmp_univ_mvar()); } levels ls = to_list(us); - expr e = tctx.whnf(instantiate_type_univ_params(d, ls)); + expr e = tmp_tctx.whnf(instantiate_type_univ_params(d, ls)); expr h = mk_constant(cname, ls); - return add_core(tctx, s, cname, ls, e, h, priority); + return add_core(tmp_tctx, s, cname, ls, e, h, priority); } // Return true iff lhs is of the form (B (x : ?m1), ?m2) or (B (x : ?m1), ?m2 x), @@ -222,30 +230,30 @@ static bool is_valid_congr_hyp_rhs(expr const & rhs, name_set & found_mvars) { return true; } -simp_lemmas add_congr_core(tmp_type_context & tctx, simp_lemmas const & s, name const & n, unsigned prio) { - declaration const & d = tctx.env().get(n); +simp_lemmas add_congr_core(tmp_type_context & tmp_tctx, simp_lemmas const & s, name const & n, unsigned prio) { + declaration const & d = tmp_tctx.tctx().env().get(n); buffer us; unsigned num_univs = d.get_num_univ_params(); for (unsigned i = 0; i < num_univs; i++) { - us.push_back(tctx.mk_uvar()); + us.push_back(tmp_tctx.mk_tmp_univ_mvar()); } levels ls = to_list(us); - expr rule = normalizer(tctx)(instantiate_type_univ_params(d, ls)); + expr rule = tmp_tctx.whnf(instantiate_type_univ_params(d, ls)); expr proof = mk_constant(n, ls); buffer emetas; buffer instances, explicits; while (is_pi(rule)) { - expr mvar = tctx.mk_mvar(binding_domain(rule)); + expr mvar = tmp_tctx.mk_tmp_mvar(binding_domain(rule)); emetas.push_back(mvar); explicits.push_back(is_explicit(binding_info(rule))); instances.push_back(binding_info(rule).is_inst_implicit()); - rule = tctx.whnf(instantiate(binding_body(rule), mvar)); + rule = tmp_tctx.whnf(instantiate(binding_body(rule), mvar)); proof = mk_app(proof, mvar); } expr rel, lhs, rhs; - if (!is_simp_relation(tctx.env(), rule, rel, lhs, rhs) || !is_constant(rel)) { + if (!is_simp_relation(tmp_tctx.tctx().env(), rule, rel, lhs, rhs) || !is_constant(rel)) { report_failure(sstream() << "invalid [congr] lemma, '" << n << "' resulting type is not of the form t ~ s, where '~' is a transitive and reflexive relation"); } @@ -292,13 +300,14 @@ simp_lemmas add_congr_core(tmp_type_context & tctx, simp_lemmas const & s, name if (explicits[i] && !found_mvars.contains(mlocal_name(mvar))) { buffer locals; expr type = mlocal_type(mvar); + type_context::tmp_locals local_factory(tmp_tctx.tctx()); while (is_pi(type)) { - expr local = tctx.mk_tmp_local(binding_domain(type)); + expr local = local_factory.push_local_from_binding(type); locals.push_back(local); type = instantiate(binding_body(type), local); } expr h_rel, h_lhs, h_rhs; - if (!is_simp_relation(tctx.env(), type, h_rel, h_lhs, h_rhs) || !is_constant(h_rel)) + if (!is_simp_relation(tmp_tctx.tctx().env(), type, h_rel, h_lhs, h_rhs) || !is_constant(h_rel)) continue; unsigned j = 0; for (expr const & local : locals) { @@ -330,6 +339,20 @@ simp_lemmas add_congr_core(tmp_type_context & tctx, simp_lemmas const & s, name return new_s; } +void validate_simp(type_context & tctx, name const & n) { + simp_lemmas s; + flet set_ex(g_throw_ex, true); + tmp_type_context tmp_tctx(tctx); + add_core(tmp_tctx, s, n, LEAN_DEFAULT_PRIORITY); +} + +void validate_congr(type_context & tctx, name const & n) { + simp_lemmas s; + flet set_ex(g_throw_ex, true); + tmp_type_context tmp_tctx(tctx); + add_congr_core(tmp_tctx, s, n, LEAN_DEFAULT_PRIORITY); +} + simp_lemma_core::simp_lemma_core(name const & id, levels const & umetas, list const & emetas, list const & instances, expr const & lhs, expr const & rhs, expr const & proof, unsigned priority): @@ -573,70 +596,43 @@ format simp_lemmas::pp(formatter const & fmt) const { return pp(fmt, format(), true, true); } -struct simp_lemmas_cache { - simp_lemmas m_main_cache; - std::vector> m_key_cache; -}; - -LEAN_THREAD_PTR(simp_lemmas_cache, g_simp_lemmas_cache); - -scope_simp::scope_simp() { - m_old_cache = g_simp_lemmas_cache; - g_simp_lemmas_cache = nullptr; -} - -scope_simp::~scope_simp() { - delete g_simp_lemmas_cache; - g_simp_lemmas_cache = m_old_cache; -} - -simp_lemmas get_simp_lemmas_core() { +simp_lemmas get_simp_lemmas(environment const & env) { simp_lemmas r; buffer simp_lemmas, congr_lemmas; - blast_tmp_type_context ctx; - auto const & s = simp_ext::get_state(env()); + aux_type_context aux_ctx(env); + type_context & tctx = aux_ctx.get(); + auto const & s = simp_ext::get_state(env); s.m_simp_lemmas.to_buffer(simp_lemmas); s.m_congr_lemmas.to_buffer(congr_lemmas); unsigned i = simp_lemmas.size(); while (i > 0) { --i; - ctx->clear(); - r = add_core(*ctx, r, simp_lemmas[i], *s.m_simp_lemmas.get_prio(simp_lemmas[i])); + tmp_type_context tmp_tctx(tctx); + r = add_core(tmp_tctx, r, simp_lemmas[i], *s.m_simp_lemmas.get_prio(simp_lemmas[i])); } i = congr_lemmas.size(); while (i > 0) { --i; - ctx->clear(); - r = add_congr_core(*ctx, r, congr_lemmas[i], *s.m_congr_lemmas.get_prio(congr_lemmas[i])); + tmp_type_context tmp_tctx(tctx); + r = add_congr_core(tmp_tctx, r, congr_lemmas[i], *s.m_congr_lemmas.get_prio(congr_lemmas[i])); } return r; } -static simp_lemmas_cache & get_cache() { - if (!g_simp_lemmas_cache) { - g_simp_lemmas_cache = new simp_lemmas_cache(); - g_simp_lemmas_cache->m_main_cache = get_simp_lemmas_core(); - } - return *g_simp_lemmas_cache; -} - -simp_lemmas get_simp_lemmas() { - return get_cache().m_main_cache; -} - template -simp_lemmas get_simp_lemmas_core(NSS const & nss) { +simp_lemmas get_simp_lemmas_core(environment const & env, NSS const & nss) { simp_lemmas r; - blast_tmp_type_context ctx; + aux_type_context aux_ctx(env); + type_context & tctx = aux_ctx.get(); for (name const & ns : nss) { - list const * entries = simp_ext::get_entries(env(), ns); + list const * entries = simp_ext::get_entries(env, ns); if (entries) { for (auto const & e : *entries) { bool is_simp; unsigned prio; name n; std::tie(is_simp, prio, n) = e; if (is_simp) { - ctx->clear(); - r = add_core(*ctx, r, n, prio); + tmp_type_context tmp_tctx(tctx); + r = add_core(tmp_tctx, r, n, prio); } } } @@ -644,44 +640,38 @@ simp_lemmas get_simp_lemmas_core(NSS const & nss) { return r; } -simp_lemmas get_simp_lemmas(std::initializer_list const & nss) { - return get_simp_lemmas_core(nss); +simp_lemmas get_simp_lemmas(environment const & env, std::initializer_list const & nss) { + return get_simp_lemmas_core(env, nss); } -simp_lemmas get_simp_lemmas(name const & ns) { - return get_simp_lemmas({ns}); +simp_lemmas get_simp_lemmas(environment const & env, name const & ns) { + return get_simp_lemmas(env, {ns}); } -simp_lemmas get_simp_lemmas(unsigned key) { - simp_lemmas_cache & cache = get_cache(); - if (key >= g_simp_lemma_ns->size()) - throw exception("invalid simp lemma cache key"); - if (key >= cache.m_key_cache.size()) - cache.m_key_cache.resize(key+1); - if (!cache.m_key_cache[key]) - cache.m_key_cache[key] = get_simp_lemmas_core((*g_simp_lemma_ns)[key]); - return *cache.m_key_cache[key]; -} -} - -void validate_simp(environment const & env, io_state const & ios, name const & n) { - blast::simp_lemmas s; - tmp_type_context ctx(env, ios.get_options()); - flet set_ex(blast::g_throw_ex, true); - blast::add_core(ctx, s, n, LEAN_DEFAULT_PRIORITY); -} - -void validate_congr(environment const & env, io_state const & ios, name const & n) { - blast::simp_lemmas s; - tmp_type_context ctx(env, ios.get_options()); - flet set_ex(blast::g_throw_ex, true); - blast::add_congr_core(ctx, s, n, LEAN_DEFAULT_PRIORITY); +vm_obj tactic_simp(vm_obj const & e, vm_obj const & s0) { + tactic_state const & s = to_tactic_state(s0); + try { + // TODO(dhs): use type_context_scope for this + metavar_context mctx_tmp = s.mctx(); + type_context tctx = mk_type_context_for(s, mctx_tmp, transparency_mode::Reducible); + simp_lemmas lemmas = get_simp_lemmas(s.env()); + expr target = *(s.get_main_goal()); +// name rel = (is_standard(s.env()) && tctx.is_prop(target)) ? get_iff_name() : get_eq_name(); + name rel = get_iff_name(); + simp_result result = simplify(tctx, rel, lemmas, to_expr(e)); + if (result.has_proof()) { + return mk_tactic_success(mk_vm_pair(to_obj(result.get_new()), to_obj(result.get_proof())), s); + } else { + return mk_tactic_exception("simp tactic failed to simplify", s); + } + } catch (exception & e) { + return mk_tactic_exception(e, s); + } } void initialize_simp_lemmas() { g_class_name = new name("simp"); g_key = new std::string("SIMP"); - g_simp_lemma_ns = new std::vector>(); simp_ext::initialize(); register_prio_attribute("simp", "simplification lemma", @@ -704,13 +694,12 @@ void initialize_simp_lemmas() { return LEAN_DEFAULT_PRIORITY; }); - blast::g_simp_lemmas_cache = nullptr; + DECLARE_VM_BUILTIN(name({"tactic", "simplify"}), tactic_simp); } void finalize_simp_lemmas() { simp_ext::finalize(); delete g_key; delete g_class_name; - delete g_simp_lemma_ns; } } diff --git a/src/library/blast/simplifier/simp_lemmas.h b/src/library/tactic/simplifier/simp_lemmas.h similarity index 87% rename from src/library/blast/simplifier/simp_lemmas.h rename to src/library/tactic/simplifier/simp_lemmas.h index 9e59367bc0..a90263c4cb 100644 --- a/src/library/blast/simplifier/simp_lemmas.h +++ b/src/library/tactic/simplifier/simp_lemmas.h @@ -7,25 +7,26 @@ Author: Leonardo de Moura #pragma once #include "kernel/environment.h" #include "library/io_state.h" -#include "library/tmp_type_context.h" +#include "library/type_context.h" #include "library/head_map.h" -#include "library/blast/gexpr.h" namespace lean { + environment add_simp_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent); environment add_congr_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent); unsigned get_simp_lemma_priority(environment const & env, name const & n); + bool is_simp_lemma(environment const & env, name const & n); bool is_congr_lemma(environment const & env, name const & n); -void get_simp_lemmas(environment const & env, buffer & r); -void get_congr_lemmas(environment const & env, buffer & r); +void get_simp_lemma_names(environment const & env, buffer & r); +void get_congr_lemma_names(environment const & env, buffer & r); + void initialize_simp_lemmas(); void finalize_simp_lemmas(); /** Generate a unique id for a set of namespaces containing [simp] and [congr] lemmas */ unsigned register_simp_lemmas(std::initializer_list const & nss); -namespace blast { class simp_lemmas; class simp_lemma_core { protected: @@ -66,7 +67,7 @@ class simp_lemma : public simp_lemma_core { list const & instances, expr const & lhs, expr const & rhs, expr const & proof, bool is_perm, unsigned priority); - friend simp_lemmas add_core(tmp_type_context & tctx, simp_lemmas const & s, name const & id, + friend simp_lemmas add_core(tmp_type_context & tmp_tctx, simp_lemmas const & s, name const & id, levels const & univ_metas, expr const & e, expr const & h, unsigned priority); public: friend bool operator==(simp_lemma const & r1, simp_lemma const & r2); @@ -154,19 +155,11 @@ public: ~scope_simp(); }; -simp_lemmas add(tmp_type_context & tctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, unsigned priority); +simp_lemmas add(type_context & tctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, unsigned priority); simp_lemmas join(simp_lemmas const & s1, simp_lemmas const & s2); /** \brief Get (active) simplification lemmas. */ -simp_lemmas get_simp_lemmas(); +simp_lemmas get_simp_lemmas(environment const & env); /** \brief Get simplification lemmas in the given namespace. */ -simp_lemmas get_simp_lemmas(name const & ns); -/** \brief Get simplification lemmas in the given namespaces. */ -// simp_lemmas get_simp_lemmas(std::initializer_list const & nss); -/** \brief Get simplification lemmas in the namespaces registered at key. - The key is created using procedure #register_simp_lemmas at initialization time. - This is more efficient than get_simp_lemmas(std::initializer_list const & nss), because - results are cached. */ -simp_lemmas get_simp_lemmas(unsigned key); -} +simp_lemmas get_simp_lemmas(environment const & env, name const & ns); } diff --git a/src/library/tactic/simplifier/simplifier.cpp b/src/library/tactic/simplifier/simplifier.cpp new file mode 100644 index 0000000000..e884aa4e06 --- /dev/null +++ b/src/library/tactic/simplifier/simplifier.cpp @@ -0,0 +1,807 @@ +/* +Copyright (c) 2015 Daniel Selsam. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Daniel Selsam +*/ +#include +#include +#include "util/flet.h" +#include "util/freset.h" +#include "util/pair.h" +#include "util/optional.h" +#include "util/interrupt.h" +#include "util/sexpr/option_declarations.h" +#include "kernel/abstract.h" +#include "kernel/expr_maps.h" +#include "kernel/instantiate.h" +#include "library/trace.h" +#include "library/constants.h" +#include "library/normalize.h" +#include "library/expr_lt.h" +#include "library/num.h" +#include "library/util.h" +#include "library/norm_num.h" +#include "library/attribute_manager.h" +#include "library/class_instance_resolution.h" +#include "library/relation_manager.h" +#include "library/app_builder.h" +#include "library/congr_lemma.h" +#include "library/fun_info.h" +#include "library/tactic/simplifier/simplifier.h" +#include "library/tactic/simplifier/simp_lemmas.h" +#include "library/tactic/simplifier/ceqv.h" +#include "library/tactic/app_builder_tactics.h" + +#ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS +#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 1000 +#endif +#ifndef LEAN_DEFAULT_SIMPLIFY_TOP_DOWN +#define LEAN_DEFAULT_SIMPLIFY_TOP_DOWN false +#endif +#ifndef LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE +#define LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE true +#endif +#ifndef LEAN_DEFAULT_SIMPLIFY_MEMOIZE +#define LEAN_DEFAULT_SIMPLIFY_MEMOIZE true +#endif +#ifndef LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL +#define LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL true +#endif +#ifndef LEAN_DEFAULT_SIMPLIFY_NUMERALS +#define LEAN_DEFAULT_SIMPLIFY_NUMERALS false +#endif + +namespace lean { + +/* Options */ + +static name * g_simplify_max_steps = nullptr; +static name * g_simplify_top_down = nullptr; +static name * g_simplify_exhaustive = nullptr; +static name * g_simplify_memoize = nullptr; +static name * g_simplify_contextual = nullptr; +static name * g_simplify_numerals = nullptr; + +unsigned get_simplify_max_steps(options const & o) { + return o.get_unsigned(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS); +} + +bool get_simplify_top_down(options const & o) { + return o.get_bool(*g_simplify_top_down, LEAN_DEFAULT_SIMPLIFY_TOP_DOWN); +} + +bool get_simplify_exhaustive(options const & o) { + return o.get_bool(*g_simplify_exhaustive, LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE); +} + +bool get_simplify_memoize(options const & o) { + return o.get_bool(*g_simplify_memoize, LEAN_DEFAULT_SIMPLIFY_MEMOIZE); +} + +bool get_simplify_contextual(options const & o) { + return o.get_bool(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL); +} + +bool get_simplify_numerals(options const & o) { + return o.get_bool(*g_simplify_numerals, LEAN_DEFAULT_SIMPLIFY_NUMERALS); +} + +/* Main simplifier class */ + +class simplifier { + type_context m_tctx; + name m_rel; + + simp_lemmas m_slss; + simp_lemmas m_ctx_slss; + + /* Logging */ + unsigned m_num_steps{0}; + + /* Options */ + unsigned m_max_steps; + bool m_top_down; + bool m_exhaustive; + bool m_memoize; + bool m_contextual; + bool m_numerals; + + /* Cache */ + struct key { + name m_rel; + expr m_e; + unsigned m_hash; + + key(name const & rel, expr const & e): + m_rel(rel), m_e(e), m_hash(hash(rel.hash(), e.hash())) { } + }; + + struct key_hash_fn { + unsigned operator()(key const & k) const { return k.m_hash; } + }; + + struct key_eq_fn { + bool operator()(key const & k1, key const & k2) const { + return k1.m_rel == k2.m_rel && k1.m_e == k2.m_e; + } + }; + + typedef std::unordered_map simplify_cache; + simplify_cache m_cache; + optional cache_lookup(expr const & e); + void cache_save(expr const & e, simp_result const & r); + + /* Basic helpers */ + bool using_eq() { return m_rel == get_eq_name(); } + + bool is_dependent_fn(expr const & f) { + expr f_type = m_tctx.whnf(m_tctx.infer(f)); + lean_assert(is_pi(f_type)); + return has_free_vars(binding_body(f_type)); + } + + simp_lemmas add_to_slss(simp_lemmas const & _slss, buffer const & ls) { + simp_lemmas slss = _slss; + for (unsigned i = 0; i < ls.size(); i++) { + expr const & l = ls[i]; + try { + // TODO(Leo,Daniel): should we allow the user to set the priority of local lemmas? + slss = add(m_tctx, slss, mlocal_name(l), m_tctx.infer(l), l, LEAN_DEFAULT_PRIORITY); + } catch (exception e) { + } + } + return slss; + } + + bool instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta, list const & emetas, list const & instances); + + /* Simp_Results */ + simp_result lift_from_eq(expr const & e_old, simp_result const & r_eq); + simp_result join(simp_result const & r1, simp_result const & r2); + simp_result finalize(simp_result const & r); + + /* Simplification */ + simp_result simplify(expr const & e); + simp_result simplify_lambda(expr const & e); + simp_result simplify_pi(expr const & e); + simp_result simplify_app(expr const & e); + simp_result simplify_fun(expr const & e); + optional simplify_numeral(expr const & e); + + /* Proving */ + optional prove(expr const & thm); + + /* Rewriting */ + simp_result rewrite(expr const & e); + simp_result rewrite(expr const & e, simp_lemmas const & slss); + simp_result rewrite(expr const & e, simp_lemma const & sr); + + /* Congruence */ + simp_result congr_fun_arg(simp_result const & r_f, simp_result const & r_arg); + simp_result congr(simp_result const & r_f, simp_result const & r_arg); + simp_result congr_fun(simp_result const & r_f, expr const & arg); + simp_result congr_arg(expr const & f, simp_result const & r_arg); + simp_result congr_funs(simp_result const & r_f, buffer const & args); + + simp_result try_congrs(expr const & e); + simp_result try_congr(expr const & e, user_congr_lemma const & cr); + + template + optional synth_congr(expr const & e, F && simp); + + expr remove_unnecessary_casts(expr const & e); + + /* Apply whnf and eta-reduction + \remark We want (Sum n (fun x, f x)) and (Sum n f) to be the same. + \remark We may want to switch to eta-expansion later (see paper: "The Virtues of Eta-expansion"). + TODO(Daniel, Leo): should we add an option for disabling/enabling eta? */ + expr whnf_eta(expr const & e); + +public: + simplifier(type_context & tctx, name const & rel, simp_lemmas const & slss): + m_tctx(tctx), m_rel(rel), m_slss(slss), + /* Options */ + m_max_steps(get_simplify_max_steps(tctx.get_options())), + m_top_down(get_simplify_top_down(tctx.get_options())), + m_exhaustive(get_simplify_exhaustive(tctx.get_options())), + m_memoize(get_simplify_memoize(tctx.get_options())), + m_contextual(get_simplify_contextual(tctx.get_options())), + m_numerals(get_simplify_numerals(tctx.get_options())) + { } + + simp_result operator()(expr const & e) { return simplify(e); } +}; + +/* Cache */ + +optional simplifier::cache_lookup(expr const & e) { + auto it = m_cache.find(key(m_rel, e)); + if (it == m_cache.end()) return optional(); + return optional(it->second); +} + +void simplifier::cache_save(expr const & e, simp_result const & r) { + m_cache.insert(mk_pair(key(m_rel, e), r)); +} + +/* Simp_Results */ + +simp_result simplifier::lift_from_eq(expr const & e_old, simp_result const & r_eq) { + if (!r_eq.has_proof()) return r_eq; + lean_assert(r_eq.has_proof()); + /* r_eq.get_proof() : e_old = r_eq.get_new() */ + /* goal : e_old r_eq.get_new() */ + type_context::tmp_locals local_factory(m_tctx); + expr local = local_factory.push_local(name(), m_tctx.infer(e_old)); + expr motive_local = mk_app(m_tctx, m_rel, e_old, local); + /* motive = fun y, e_old y */ + expr motive = local_factory.mk_lambda(motive_local); + /* Rxx = x x */ + expr Rxx = mk_refl(m_tctx, m_rel, e_old); + expr pf = mk_eq_rec(m_tctx, motive, Rxx, r_eq.get_proof()); + return simp_result(r_eq.get_new(), pf); +} + +simp_result simplifier::join(simp_result const & r1, simp_result const & r2) { + /* Assumes that both simp_results are with respect to the same relation */ + if (!r1.has_proof()) { + return r2; + } else if (!r2.has_proof()) { + lean_assert(r1.has_proof()); + return simp_result(r2.get_new(), r1.get_proof()); + } else { + /* If they both have proofs, we need to glue them together with transitivity. */ + lean_assert(r1.has_proof() && r2.has_proof()); + lean_trace(name({"simplifier"}), + expr pf1_type = m_tctx.infer(r1.get_proof()); + expr pf2_type = m_tctx.infer(r2.get_proof()); + tout() << "JOIN(" << r1.get_proof() << " : " << pf1_type + << ", " << r2.get_proof() << " : " << pf2_type << ")\n";); + + expr trans = mk_trans(m_tctx, m_rel, r1.get_proof(), r2.get_proof()); + return simp_result(r2.get_new(), trans); + } +} + +/* Whnf + Eta */ +expr simplifier::whnf_eta(expr const & e) { + return try_eta(m_tctx.whnf(e)); +} + +/* Simplification */ + +simp_result simplifier::simplify(expr const & e) { + check_system("simplifier"); + m_num_steps++; + lean_trace_inc_depth("simplifier"); + lean_trace_d("simplifier", tout() << m_rel << ": " << e << "\n";); + + if (m_num_steps > m_max_steps) + throw exception("simplifier failed, maximum number of steps exceeded"); + + if (m_memoize) { + if (auto it = cache_lookup(e)) return *it; + } + + if (m_numerals && using_eq()) { + if (auto r = simplify_numeral(e)) { + return *r; + } + } + + simp_result r(e); + + if (m_top_down) r = join(r, rewrite(whnf_eta(r.get_new()))); + + r.update(whnf_eta(r.get_new())); + + switch (r.get_new().kind()) { + case expr_kind::Local: + case expr_kind::Meta: + case expr_kind::Sort: + case expr_kind::Constant: + // no-op + break; + case expr_kind::Var: + lean_unreachable(); + case expr_kind::Macro: + break; + case expr_kind::Lambda: + if (using_eq()) r = join(r, simplify_lambda(r.get_new())); + break; + case expr_kind::Pi: + r = join(r, simplify_pi(r.get_new())); + break; + case expr_kind::App: + r = join(r, simplify_app(r.get_new())); + break; + case expr_kind::Let: + // whnf unfolds let-expressions + lean_unreachable(); + } + + if (!m_top_down) r = join(r, rewrite(whnf_eta(r.get_new()))); + + if (r.get_new() == e && !using_eq()) { + simp_result r_eq; + { + flet use_eq(m_rel, get_eq_name()); + r_eq = simplify(r.get_new()); + } + r = join(r, lift_from_eq(r.get_new(), r_eq)); + } + + if (m_exhaustive && r.has_proof()) r = join(r, simplify(r.get_new())); + + if (m_memoize) cache_save(e, r); + + return r; +} + +simp_result simplifier::simplify_lambda(expr const & e) { + lean_assert(is_lambda(e)); + expr t = e; + + type_context::tmp_locals local_factory(m_tctx); + + expr l = local_factory.push_local_from_binding(t); + t = instantiate(binding_body(t), l); + + simp_result r = simplify(t); + expr new_t = local_factory.mk_lambda(r.get_new()); + + if (r.has_proof()) { + expr lam_pf = local_factory.mk_lambda(r.get_proof()); + expr funext_pf = mk_app(m_tctx, get_funext_name(), lam_pf); + return simp_result(new_t, funext_pf); + } else { + return simp_result(new_t); + } +} + +simp_result simplifier::simplify_pi(expr const & e) { + lean_assert(is_pi(e)); + return try_congrs(e); +} + +simp_result simplifier::simplify_app(expr const & _e) { + lean_assert(is_app(_e)); + // TODO(dhs): normalize instances and subsingletons + expr e = _e; + + // (1) Try user-defined congruences + simp_result r_user = try_congrs(e); + if (r_user.has_proof()) { + if (using_eq()) return join(r_user, simplify_fun(r_user.get_new())); + else return r_user; + } + + // TODO(dhs): (2) Synthesize congruence lemma + + // (3) Fall back on generic binary congruence + if (using_eq()) { + expr const & f = app_fn(e); + expr const & arg = app_arg(e); + + simp_result r_f = simplify(f); + + if (is_dependent_fn(f)) { + if (r_f.has_proof()) return congr_fun(r_f, arg); + else return mk_app(r_f.get_new(), arg); + } else { + simp_result r_arg = simplify(arg); + return congr_fun_arg(r_f, r_arg); + } + } + return simp_result(e); +} + +simp_result simplifier::simplify_fun(expr const & e) { + lean_assert(is_app(e)); + buffer args; + expr const & f = get_app_args(e, args); + simp_result r_f = simplify(f); + return congr_funs(r_f, args); +} + +optional simplifier::simplify_numeral(expr const & e) { + if (is_num(e)) { return optional(simp_result(e)); } + try { + expr_pair r = mk_norm_num(m_tctx, e); + return optional(simp_result(r.first, r.second)); + } catch (exception e) { + return optional(); + } +} + +/* Proving */ + +simp_result simplifier::finalize(simp_result const & r) { + if (r.has_proof()) return r; + expr pf = mk_refl(m_tctx, m_rel, r.get_new()); + return simp_result(r.get_new(), pf); +} + +optional simplifier::prove(expr const & thm) { + flet set_name(m_rel, get_iff_name()); + simp_result r_cond = simplify(thm); + if (is_constant(r_cond.get_new()) && const_name(r_cond.get_new()) == get_true_name()) { + expr pf = mk_app(m_tctx, get_iff_elim_right_name(), + finalize(r_cond).get_proof(), + mk_constant(get_true_intro_name())); + return some_expr(pf); + } + return none_expr(); +} + +/* Rewriting */ + +simp_result simplifier::rewrite(expr const & e) { + simp_result r(e); + while (true) { + simp_result r_ctx = rewrite(r.get_new(), m_ctx_slss); + simp_result r_new = rewrite(r_ctx.get_new(), m_slss); + if (!r_ctx.has_proof() && !r_new.has_proof()) break; + r = join(join(r, r_ctx), r_new); + } + return r; +} + +simp_result simplifier::rewrite(expr const & e, simp_lemmas const & slss) { + simp_result r(e); + + simp_lemmas_for const * sr = slss.find(m_rel); + if (!sr) return r; + + list const * srs = sr->find_simp(e); + if (!srs) { + lean_trace(name({"simplifier", "try_rewrite"}), tout() << "no simp lemmas for: " << e << "\n";); + return r; + } + + for_each(*srs, [&](simp_lemma const & sr) { + simp_result r_new = rewrite(r.get_new(), sr); + if (!r_new.has_proof()) return; + r = join(r, r_new); + }); + return r; +} + +simp_result simplifier::rewrite(expr const & e, simp_lemma const & sl) { + tmp_type_context tmp_tctx(m_tctx, sl.get_num_umeta(), sl.get_num_emeta()); + lean_trace(name({"simplifier", "try_rewrite"}), tout() << e << " =?= " << sl.get_lhs() << "\n";); + + if (!tmp_tctx.is_def_eq(e, sl.get_lhs())) return simp_result(e); + + lean_trace(name({"simplifier", "rewrite"}), + expr new_lhs = tmp_tctx.instantiate_mvars(sl.get_lhs()); + expr new_rhs = tmp_tctx.instantiate_mvars(sl.get_rhs()); + tout() << "(" << sl.get_id() << ") " + << "[" << new_lhs << " --> " << new_rhs << "]\n";); + + if (!instantiate_emetas(tmp_tctx, sl.get_num_emeta(), sl.get_emetas(), sl.get_instances())) return simp_result(e); + + for (unsigned i = 0; i < sl.get_num_umeta(); i++) { + if (!tmp_tctx.is_uassigned(i)) return simp_result(e); + } + + expr new_lhs = tmp_tctx.instantiate_mvars(sl.get_lhs()); + expr new_rhs = tmp_tctx.instantiate_mvars(sl.get_rhs()); + + if (sl.is_perm()) { + // TODO(dhs): restore light-lt + if (!is_lt(new_rhs, new_lhs, false)) { + lean_trace(name({"simplifier", "perm"}), + tout() << "perm rejected: " << new_rhs << " !< " << new_lhs << "\n";); + return simp_result(e); + } + } + + expr pf = tmp_tctx.instantiate_mvars(sl.get_proof()); + return simp_result(new_rhs, pf); +} + +/* Congruence */ + +simp_result simplifier::congr_fun_arg(simp_result const & r_f, simp_result const & r_arg) { + if (!r_f.has_proof() && !r_arg.has_proof()) return simp_result(mk_app(r_f.get_new(), r_arg.get_new())); + else if (!r_f.has_proof()) return congr_arg(r_f.get_new(), r_arg); + else if (!r_arg.has_proof()) return congr_fun(r_f, r_arg.get_new()); + else return congr(r_f, r_arg); +} + +simp_result simplifier::congr(simp_result const & r_f, simp_result const & r_arg) { + lean_assert(r_f.has_proof() && r_arg.has_proof()); + // theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ + expr e = mk_app(r_f.get_new(), r_arg.get_new()); + expr pf = mk_congr(m_tctx, r_f.get_proof(), r_arg.get_proof()); + return simp_result(e, pf); +} + +simp_result simplifier::congr_fun(simp_result const & r_f, expr const & arg) { + lean_assert(r_f.has_proof()); + // theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a + expr e = mk_app(r_f.get_new(), arg); + expr pf = mk_congr_fun(m_tctx, r_f.get_proof(), arg); + return simp_result(e, pf); +} + +simp_result simplifier::congr_arg(expr const & f, simp_result const & r_arg) { + lean_assert(r_arg.has_proof()); + // theorem congr_arg {A B : Type} {a₁ a₂ : A} (f : A → B) : a₁ = a₂ → f a₁ = f a₂ + expr e = mk_app(f, r_arg.get_new()); + expr pf = mk_congr_arg(m_tctx, f, r_arg.get_proof()); + return simp_result(e, pf); +} + +/* Note: handles reflexivity */ +simp_result simplifier::congr_funs(simp_result const & r_f, buffer const & args) { + // congr_fun : ∀ {A : Type} {B : A → Type} {f g : Π (x : A), B x}, f = g → (∀ (a : A), f a = g a) + expr e = r_f.get_new(); + for (unsigned i = 0; i < args.size(); ++i) { + e = mk_app(e, args[i]); + } + if (!r_f.has_proof()) return simp_result(e); + expr pf = r_f.get_proof(); + for (unsigned i = 0; i < args.size(); ++i) { + pf = mk_app(m_tctx, get_congr_fun_name(), pf, args[i]); + } + return simp_result(e, pf); +} + +simp_result simplifier::try_congrs(expr const & e) { + simp_lemmas_for const * sls = m_slss.find(m_rel); + if (!sls) return simp_result(e); + + list const * cls = sls->find_congr(e); + if (!cls) return simp_result(e); + + simp_result r(e); + for_each(*cls, [&](user_congr_lemma const & cl) { + if (r.has_proof()) return; + r = try_congr(e, cl); + }); + return r; +} + +simp_result simplifier::try_congr(expr const & e, user_congr_lemma const & cl) { + tmp_type_context tmp_tctx(m_tctx, cl.get_num_umeta(), cl.get_num_emeta()); + if (!tmp_tctx.is_def_eq(e, cl.get_lhs())) return simp_result(e); + + lean_trace(name({"simplifier", "congruence"}), + expr new_lhs = tmp_tctx.instantiate_mvars(cl.get_lhs()); + expr new_rhs = tmp_tctx.instantiate_mvars(cl.get_rhs()); + diagnostic(m_tctx.env(), get_dummy_ios(), m_tctx) + << "(" << cl.get_id() << ") " + << "[" << new_lhs << " =?= " << new_rhs << "]\n";); + + /* First, iterate over the congruence hypotheses */ + bool failed = false; + bool simplified = false; + list const & congr_hyps = cl.get_congr_hyps(); + for_each(congr_hyps, [&](expr const & m) { + if (failed) return; + type_context::tmp_locals local_factory(m_tctx); + expr m_type = tmp_tctx.instantiate_mvars(tmp_tctx.infer(m)); + + while (is_pi(m_type)) { + expr l = local_factory.push_local_from_binding(m_type); + lean_assert(!has_metavar(l)); + m_type = instantiate(binding_body(m_type), l); + } + + expr h_rel, h_lhs, h_rhs; + lean_verify(is_simp_relation(m_tctx.env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel)); + { + flet set_name(m_rel, const_name(h_rel)); + + flet set_ctx_slss(m_ctx_slss, m_contextual ? add_to_slss(m_ctx_slss, local_factory.as_buffer()) : m_ctx_slss); + + h_lhs = tmp_tctx.instantiate_mvars(h_lhs); + lean_assert(!has_metavar(h_lhs)); + + // TODO(dhs): freset cache? + simp_result r_congr_hyp = simplify(h_lhs); + if (r_congr_hyp.has_proof()) simplified = true; + r_congr_hyp = finalize(r_congr_hyp); + expr hyp = finalize(r_congr_hyp).get_proof(); + + if (!tmp_tctx.is_def_eq(m, local_factory.mk_lambda(hyp))) failed = true; + } + }); + + if (failed || !simplified) return simp_result(e); + + if (!instantiate_emetas(tmp_tctx, cl.get_num_emeta(), cl.get_emetas(), cl.get_instances())) return simp_result(e); + + for (unsigned i = 0; i < cl.get_num_umeta(); i++) { + if (!tmp_tctx.is_uassigned(i)) return simp_result(e); + } + + expr e_s = tmp_tctx.instantiate_mvars(cl.get_rhs()); + expr pf = tmp_tctx.instantiate_mvars(cl.get_proof()); + return simp_result(e_s, pf); +} + +bool simplifier::instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta, list const & emetas, list const & instances) { + bool failed = false; + unsigned i = num_emeta; + for_each2(emetas, instances, [&](expr const & m, bool const & is_instance) { + i--; + if (failed) return; + expr m_type = tmp_tctx.instantiate_mvars(m_tctx.infer(m)); + lean_assert(!has_metavar(m_type)); + + if (tmp_tctx.is_eassigned(i)) return; + + if (is_instance) { + if (auto v = m_tctx.mk_class_instance(m_type)) { + if (!tmp_tctx.is_def_eq(m, *v)) { + lean_trace(name({"simplifier", "failure"}), + tout() << "unable to assign instance for: " << m_type << "\n";); + failed = true; + return; + } + } else { + lean_trace(name({"simplifier", "failure"}), + tout() << "unable to synthesize instance for: " << m_type << "\n";); + failed = true; + return; + } + } + + if (tmp_tctx.is_eassigned(i)) return; + + if (m_tctx.is_prop(m_type)) { + if (auto pf = prove(m_type)) { + lean_verify(tmp_tctx.is_def_eq(m, *pf)); + return; + } + } + + lean_trace(name({"simplifier", "failure"}), + tout() << "failed to assign: " << m << " : " << m_type << "\n";); + + failed = true; + return; + }); + + return !failed; +} + +template +optional simplifier::synth_congr(expr const & e, F && simp) { + static_assert(std::is_same::type, simp_result>::value, + "synth_congr: simp must take expressions to simp_results"); + lean_assert(is_app(e)); + buffer args; + expr f = get_app_args(e, args); + auto congr_lemma = mk_specialized_congr_simp(m_tctx, e); + if (!congr_lemma) return optional(); + expr proof = congr_lemma->get_proof(); + expr type = congr_lemma->get_type(); + unsigned i = 0; + bool has_proof = false; + bool has_cast = false; + for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) { + switch (ckind) { + case congr_arg_kind::HEq: + lean_unreachable(); + case congr_arg_kind::Fixed: + proof = mk_app(proof, args[i]); + type = instantiate(binding_body(type), args[i]); + break; + case congr_arg_kind::FixedNoParam: + break; + case congr_arg_kind::Eq: + proof = mk_app(proof, args[i]); + type = instantiate(binding_body(type), args[i]); + { + simp_result r_arg = simp(args[i]); + if (r_arg.has_proof()) has_proof = true; + r_arg = finalize(r_arg); + proof = mk_app(proof, r_arg.get_new(), r_arg.get_proof()); + type = instantiate(binding_body(type), r_arg.get_new()); + type = instantiate(binding_body(type), r_arg.get_proof()); + } + break; + case congr_arg_kind::Cast: + proof = mk_app(proof, args[i]); + type = instantiate(binding_body(type), args[i]); + has_cast = true; + break; + } + i++; + }); + lean_assert(is_eq(type)); + buffer type_args; + get_app_args(type, type_args); + expr e_new = remove_unnecessary_casts(type_args[2]); + simp_result r; + if (has_proof) r = simp_result(e_new, proof); + else r = simp_result(e_new); + + /* TODO(dhs): re-integrate + if (has_cast) { + if (auto r_norm = normalize_subsingleton_args(e_new)) + r = join(r, *r_norm); + } + */ + return optional(r); +} + +expr simplifier::remove_unnecessary_casts(expr const & e) { + buffer args; + expr f = get_app_args(e, args); + fun_info f_info = get_specialized_fun_info(m_tctx, e); + int i = -1; + for_each(f_info.get_params_info(), [&](param_info const & p_info) { + i++; + if (p_info.is_subsingleton()) { + while (is_constant(get_app_fn(args[i]))) { + buffer cast_args; + expr f_cast = get_app_args(args[i], cast_args); + name n_f = const_name(f_cast); + if (n_f == get_eq_rec_name() || n_f == get_eq_drec_name() || n_f == get_eq_nrec_name()) { + lean_assert(cast_args.size() == 6); + expr major_premise = cast_args[5]; + expr f_major_premise = get_app_fn(major_premise); + if (is_constant(f_major_premise) && const_name(f_major_premise) == get_eq_refl_name()) + args[i] = cast_args[3]; + else + return; + } else { + return; + } + } + } + }); + return mk_app(f, args); +} + +/* Setup and teardown */ + +void initialize_simplifier() { + register_trace_class("simplifier"); + register_trace_class(name({"simplifier", "rewrite"})); + register_trace_class(name({"simplifier", "congruence"})); + register_trace_class(name({"simplifier", "failure"})); + register_trace_class(name({"simplifier", "perm"})); + register_trace_class(name({"simplifier", "try_rewrite"})); + + g_simplify_max_steps = new name{"simplify", "max_steps"}; + g_simplify_top_down = new name{"simplify", "top_down"}; + g_simplify_exhaustive = new name{"simplify", "exhaustive"}; + g_simplify_memoize = new name{"simplify", "memoize"}; + g_simplify_contextual = new name{"simplify", "contextual"}; + g_simplify_numerals = new name{"simplify", "numerals"}; + + register_unsigned_option(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS, + "(simplify) max allowed steps in simplification"); + register_bool_option(*g_simplify_top_down, LEAN_DEFAULT_SIMPLIFY_TOP_DOWN, + "(simplify) use top-down rewriting instead of bottom-up"); + register_bool_option(*g_simplify_exhaustive, LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE, + "(simplify) rewrite exhaustively"); + register_bool_option(*g_simplify_memoize, LEAN_DEFAULT_SIMPLIFY_MEMOIZE, + "(simplify) memoize simplifications"); + register_bool_option(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL, + "(simplify) use contextual simplification"); + register_bool_option(*g_simplify_numerals, LEAN_DEFAULT_SIMPLIFY_NUMERALS, + "(simplify) simplify (+, *, -, /) over numerals"); +} + +void finalize_simplifier() { + delete g_simplify_numerals; + delete g_simplify_contextual; + delete g_simplify_memoize; + delete g_simplify_exhaustive; + delete g_simplify_top_down; + delete g_simplify_max_steps; +} + +/* Entry point */ +simp_result simplify(type_context & ctx, name const & rel, simp_lemmas const & simp_lemmas, expr const & e) { + return simplifier(ctx, rel, simp_lemmas)(e); +} + +} diff --git a/src/library/blast/simplifier/simplifier.h b/src/library/tactic/simplifier/simplifier.h similarity index 51% rename from src/library/blast/simplifier/simplifier.h rename to src/library/tactic/simplifier/simplifier.h index 57c0863c25..4059666565 100644 --- a/src/library/blast/simplifier/simplifier.h +++ b/src/library/tactic/simplifier/simplifier.h @@ -5,27 +5,22 @@ Author: Daniel Selsam */ #pragma once #include "kernel/expr_pair.h" -#include "library/blast/state.h" -#include "library/blast/simplifier/simp_lemmas.h" +#include "library/type_context.h" +#include "library/tactic/simplifier/simp_lemmas.h" namespace lean { -namespace blast { -namespace simp { - -/* Struct to store results of simplification */ -struct result { +struct simp_result { /* Invariant [m_pf : m_orig m_new] */ expr m_new; /* If proof is not provided, it is assumed to be reflexivity */ optional m_proof; - public: - result() {} - result(expr const & e): m_new(e) {} - result(expr const & e, expr const & proof): m_new(e), m_proof(proof) {} - result(expr const & e, optional const & proof): m_new(e), m_proof(proof) {} + simp_result() {} + simp_result(expr const & e): m_new(e) {} + simp_result(expr const & e, expr const & proof): m_new(e), m_proof(proof) {} + simp_result(expr const & e, optional const & proof): m_new(e), m_proof(proof) {} bool has_proof() const { return static_cast(m_proof); } @@ -35,16 +30,10 @@ public: /* The following assumes that [e] and [m_new] are definitionally equal */ void update(expr const & e) { m_new = e; } }; -} -// TODO(dhs): put this outside of blast module -typedef std::function expr_predicate; // NOLINT - -simp::result simplify(name const & rel, expr const & e, simp_lemmas const & srss); -simp::result simplify(name const & rel, expr const & e, simp_lemmas const & srss, expr_predicate const & simp_pred); +simp_result simplify(type_context & ctx, name const & rel, simp_lemmas const & simp_lemmas, expr const & e); void initialize_simplifier(); void finalize_simplifier(); } -} diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 16498538e6..433b9dfed7 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "library/type_context.h" #include "library/pp_options.h" #include "library/trace.h" +#include "library/util.h" #include "library/vm/vm_environment.h" #include "library/vm/vm_exceptional.h" #include "library/vm/vm_format.h" diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 017ba82d42..71451bc0b0 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -1357,7 +1357,7 @@ bool type_context::process_assignment(expr const & m, expr const & v) { For every metavariable `?M'@C'` occurring in `t`, `C'` is a subset of `C` */ optional const & e_decl = m_mctx.get_metavar_decl(e); - if (!e_decl || e_decl->get_context().is_subset_of(mvar_decl->get_context())) { + if (!e_decl || !e_decl->get_context().is_subset_of(mvar_decl->get_context())) { ok = false; return false; } @@ -2489,6 +2489,56 @@ optional type_context::mk_subsingleton_instance(expr const & type) { return r; } +tmp_type_context::tmp_type_context(type_context & tctx, unsigned num_umeta, unsigned num_emeta): m_tctx(tctx) { + m_tmp_uassignment.resize(num_umeta, none_level()); + m_tmp_eassignment.resize(num_emeta, none_expr()); +} + +bool tmp_type_context::is_def_eq(expr const & e1, expr const & e2) { + type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment); + return m_tctx.is_def_eq(e1, e2); +} + +expr tmp_type_context::infer(expr const & e) { + type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment); + return m_tctx.infer(e); +} + +expr tmp_type_context::whnf(expr const & e) { + // TODO(dhs): do I need to set the buffers for whnf? + type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment); + return m_tctx.whnf(e); +} + +level tmp_type_context::mk_tmp_univ_mvar() { + type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment); + return m_tctx.mk_tmp_univ_mvar(); +} + +expr tmp_type_context::mk_tmp_mvar(expr const & type) { + type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment); + return m_tctx.mk_tmp_mvar(type); +} + +bool tmp_type_context::is_uassigned(unsigned i) { + lean_assert(i < m_tmp_uassignment.size()); + return static_cast(m_tmp_uassignment[i]); +} + +bool tmp_type_context::is_eassigned(unsigned i) { + lean_assert(i < m_tmp_eassignment.size()); + return static_cast(m_tmp_eassignment[i]); +} + +void tmp_type_context::clear_eassignment() { + m_tmp_eassignment.clear(); +} + +expr tmp_type_context::instantiate_mvars(expr const & e) { + type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment); + return m_tctx.instantiate_mvars(e); +} + void initialize_type_context() { register_trace_class("class_instances"); register_trace_class(name({"type_context", "unification_hint"})); diff --git a/src/library/type_context.h b/src/library/type_context.h index 5b97bd3e5b..5e93975dbe 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -492,6 +492,25 @@ public: type_context * operator->() { return &m_ctx; } }; +class tmp_type_context { + type_context & m_tctx; + buffer> m_tmp_uassignment; + buffer> m_tmp_eassignment; + +public: + tmp_type_context(type_context & tctx, unsigned num_umeta = 0, unsigned num_emeta = 0); + type_context & tctx() const { return m_tctx; } + expr infer(expr const & e); + expr whnf(expr const & e); + bool is_def_eq(expr const & e1, expr const & e2); + level mk_tmp_univ_mvar(); + expr mk_tmp_mvar(expr const & type); + bool is_uassigned(unsigned i); + bool is_eassigned(unsigned i); + void clear_eassignment(); + expr instantiate_mvars(expr const & e); +}; + void initialize_type_context(); void finalize_type_context(); } diff --git a/tests/lean/congr_print.lean.expected.out b/tests/lean/congr_print.lean.expected.out index 056079352f..5ea232a9c0 100644 --- a/tests/lean/congr_print.lean.expected.out +++ b/tests/lean/congr_print.lean.expected.out @@ -1,2 +1,2 @@ -theorem perm.perm_erase_dup_of_perm : ∀ {A : Type} [H : decidable_eq A] {l₁ l₂ : list A}, l₁ ~ l₂ → erase_dup l₁ ~ erase_dup l₂ := +theorem perm.perm_erase_dup_of_perm [congr] : ∀ {A : Type} [H : decidable_eq A] {l₁ l₂ : list A}, l₁ ~ l₂ → erase_dup l₁ ~ erase_dup l₂ := λ A H l₁ l₂, sorry diff --git a/tests/lean/run/simp1.lean b/tests/lean/run/simp1.lean new file mode 100644 index 0000000000..3b2159fd12 --- /dev/null +++ b/tests/lean/run/simp1.lean @@ -0,0 +1,8 @@ +constants (A : Type.{1}) (f : A → A → A) (x y z : A) (g : A → A) +lemma foo [simp] : f x y = y := sorry +lemma bar [simp] : g y = z := sorry + +open tactic +set_option trace.simplifier true +example : g (f x y) = z := by simp >> triv +example : g (f x (f x y)) = z := by simp >> triv diff --git a/tests/lean/run/simp2.lean b/tests/lean/run/simp2.lean new file mode 100644 index 0000000000..6b9410f32e --- /dev/null +++ b/tests/lean/run/simp2.lean @@ -0,0 +1,13 @@ +import algebra.group +constants (A : Type.{1}) (A_cg : comm_group A) (x y z w : A) +attribute A_cg [instance] + +open tactic +open simplifier.ac + +example : x * y = y * x := by simp >> triv +example : x * y * z * w = ((w * z) * y) * x := by simp >> triv +example : x * y * z * w = ((z * w) * x) * y := by simp >> triv + +open simplifier.unit +example : x * y * z * 1 * w = ((z * w * 1) * x) * y := by simp >> triv diff --git a/tests/lean/run/simp3.lean b/tests/lean/run/simp3.lean new file mode 100644 index 0000000000..350b6e4c38 --- /dev/null +++ b/tests/lean/run/simp3.lean @@ -0,0 +1,9 @@ +import algebra.ring +constants (A : Type.{1}) (A_cr : comm_ring A) (x y z w : A) +attribute A_cr [instance] + +open tactic +open simplifier.unit simplifier.ac simplifier.distrib + +example : (x + y) * (z + w) = x * z + x * w + y * z + y * w * 1 + 0 := +by simp >> trace_state >> triv diff --git a/tests/lean/rw_set2.lean.expected.out b/tests/lean/rw_set2.lean.expected.out index e69de29bb2..c93d95946c 100644 --- a/tests/lean/rw_set2.lean.expected.out +++ b/tests/lean/rw_set2.lean.expected.out @@ -0,0 +1,51 @@ +simplification rules for iff +#1, ?M_1 ↔ ?M_1 ↦ true +#1, false ↔ ?M_1 ↦ ¬?M_1 +#1, ?M_1 ↔ false ↦ ¬?M_1 +#1, true ↔ ?M_1 ↦ ?M_1 +#1, ?M_1 ↔ true ↦ ?M_1 +#0, false ↔ true ↦ false +#0, true ↔ false ↦ false +#1, ¬?M_1 ↔ ?M_1 ↦ false +#1, ?M_1 ↔ ¬?M_1 ↦ false +#2, ?M_1 - ?M_2 ≤ ?M_1 ↦ true +#1, 0 ≤ ?M_1 ↦ true +#1, succ ?M_1 ≤ ?M_1 ↦ false +#1, pred ?M_1 ≤ ?M_1 ↦ true +#1, ?M_1 ≤ succ ?M_1 ↦ true +#1, ?M_1 ∧ ?M_1 ↦ ?M_1 +#1, ?M_1 ∧ ¬?M_1 ↦ false +#1, ¬?M_1 ∧ ?M_1 ↦ false +#1, false ∧ ?M_1 ↦ false +#1, ?M_1 ∧ false ↦ false +#1, true ∧ ?M_1 ↦ ?M_1 +#1, ?M_1 ∧ true ↦ ?M_1 +#3 perm, ?M_1 ∧ ?M_2 ∧ ?M_3 ↦ ?M_2 ∧ ?M_1 ∧ ?M_3 +#3, (?M_1 ∧ ?M_2) ∧ ?M_3 ↦ ?M_1 ∧ ?M_2 ∧ ?M_3 +#2 perm, ?M_1 ∧ ?M_2 ↦ ?M_2 ∧ ?M_1 +#2, ?M_2 == ?M_2 ↦ true +#2, ?M_1 - ?M_2 < succ ?M_1 ↦ true +#1, ?M_1 < 0 ↦ false +#1, ?M_1 < succ ?M_1 ↦ true +#1, 0 < succ ?M_1 ↦ true +#1, ?M_1 ∨ ?M_1 ↦ ?M_1 +#1, false ∨ ?M_1 ↦ ?M_1 +#1, ?M_1 ∨ false ↦ ?M_1 +#1, true ∨ ?M_1 ↦ true +#1, ?M_1 ∨ true ↦ true +#3 perm, ?M_1 ∨ ?M_2 ∨ ?M_3 ↦ ?M_2 ∨ ?M_1 ∨ ?M_3 +#3, (?M_1 ∨ ?M_2) ∨ ?M_3 ↦ ?M_1 ∨ ?M_2 ∨ ?M_3 +#2 perm, ?M_1 ∨ ?M_2 ↦ ?M_2 ∨ ?M_1 +#2, ?M_2 = ?M_2 ↦ true +#2, ¬?M_2 = ?M_2 ↦ false +#0, ¬false ↦ true +#0, ¬true ↦ false +simplification rules for eq +#1, g ?M_1 ↦ f ?M_1 + 1 +#2, g ?M_1 ↦ 1 +#2, f ?M_1 ↦ 0 +#3, ite false ?M_2 ?M_3 ↦ ?M_3 +#3, ite true ?M_2 ?M_3 ↦ ?M_2 +#4, ite ?M_1 ?M_4 ?M_4 ↦ ?M_4 +#1, 0 - ?M_1 ↦ 0 +#2, succ ?M_1 - succ ?M_2 ↦ ?M_1 - ?M_2