diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index d81edf19f6..7b1d36f50e 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -11,9 +11,9 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp relation_manager.cpp export.cpp user_recursors.cpp idx_metavar.cpp composition_manager.cpp tc_multigraph.cpp noncomputable.cpp aux_recursors.cpp norm_num.cpp trace.cpp - attribute_manager.cpp error_handling.cpp unification_hint.cpp + attribute_manager.cpp error_handling.cpp unification_hint.cpp local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp lazy_abstraction.cpp - fun_info.cpp + fun_info.cpp congr_lemma.cpp # Legacy -- The following files will be eventually deleted normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp unifier.cpp match.cpp class_instance_resolution.cpp old_type_context.cpp @@ -21,6 +21,6 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp old_util.cpp let.cpp metavar_closure.cpp old_local_context.cpp choice_iterator.cpp tmp_type_context.cpp - # fun_info_manager.cpp congr_lemma_manager.cpp abstract_expr_manager.cpp light_lt_manager.cpp + # abstract_expr_manager.cpp light_lt_manager.cpp # proof_irrel_expr_manager.cpp ) diff --git a/src/library/congr_lemma_manager.cpp b/src/library/congr_lemma.cpp similarity index 73% rename from src/library/congr_lemma_manager.cpp rename to src/library/congr_lemma.cpp index d459433c59..7f53c901e5 100644 --- a/src/library/congr_lemma_manager.cpp +++ b/src/library/congr_lemma.cpp @@ -1,5 +1,5 @@ /* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura @@ -8,12 +8,14 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "library/util.h" #include "library/trace.h" -#include "library/locals.h" #include "library/constants.h" -#include "library/replace_visitor.h" -#include "library/relation_manager.h" +#include "library/locals.h" +#include "library/congr_lemma.h" #include "library/expr_unsigned_map.h" -#include "library/congr_lemma_manager.h" +#include "library/relation_manager.h" +#include "library/cache_helper.h" +#include "library/app_builder.h" +#include "library/fun_info.h" namespace lean { bool congr_lemma::all_eq_kind() const { @@ -21,12 +23,9 @@ bool congr_lemma::all_eq_kind() const { [](congr_arg_kind k) { return k == congr_arg_kind::Eq; }); } -struct congr_lemma_manager::imp { - app_builder & m_builder; - fun_info_manager & m_fmanager; - old_type_context & m_ctx; - typedef expr_unsigned key; - typedef expr_unsigned_map cache; +struct congr_lemma_cache { + typedef expr_unsigned_map cache; + environment m_env; cache m_simp_cache; cache m_simp_cache_spec; cache m_cache; @@ -34,6 +33,28 @@ struct congr_lemma_manager::imp { cache m_hcache; cache m_rel_cache[2]; relation_info_getter m_relation_info_getter; + congr_lemma_cache(environment const & env): + m_env(env), + m_relation_info_getter(mk_relation_info_getter(env)) {} + environment const & env() const { return m_env; } +}; + +typedef cache_compatibility_helper congr_lemma_cache_helper; + +MK_THREAD_LOCAL_GET_DEF(congr_lemma_cache_helper, get_clch); + +congr_lemma_cache & get_congr_lemma_cache_for(type_context const & ctx) { + return get_clch().get_cache_for(ctx); +} + +struct congr_lemma_manager { + typedef expr_unsigned key; + typedef congr_lemma result; + type_context & m_ctx; + congr_lemma_cache & m_cache; + + congr_lemma_manager(type_context & ctx): + m_ctx(ctx), m_cache(get_congr_lemma_cache_for(ctx)) {} expr infer(expr const & e) { return m_ctx.infer(e); } expr whnf(expr const & e) { return m_ctx.whnf(e); } @@ -61,24 +82,24 @@ struct congr_lemma_manager::imp { // Since the type depends on the major, we must use dependent elimination. // and the motive just abstract rhs and *major use_drec = true; - motive = Fun(rhs, Fun(*major, type)); + motive = m_ctx.mk_lambda({rhs, *major}, type); // We compute new_type by replacing rhs with lhs and *major with eq.refl(lhs) in type. new_type = instantiate(abstract_local(type, rhs), lhs); - expr refl = m_builder.mk_eq_refl(lhs); + expr refl = mk_eq_refl(m_ctx, lhs); new_type = instantiate(abstract_local(new_type, *major), refl); } else { // type does not depend on the *major. // So, the motive is just (fun rhs, type), and // new_type just replaces rhs with lhs. use_drec = false; - motive = Fun(rhs, type); + motive = m_ctx.mk_lambda({rhs}, type); new_type = instantiate(abstract_local(type, rhs), lhs); } expr minor = cast(e, new_type, tail(deps), eqs); if (use_drec) { - return m_builder.mk_eq_drec(motive, minor, *major); + return mk_eq_drec(m_ctx, motive, minor, *major); } else { - return m_builder.mk_eq_rec(motive, minor, *major); + return mk_eq_rec(m_ctx, motive, minor, *major); } } } @@ -99,17 +120,17 @@ struct congr_lemma_manager::imp { } expr g = mk_app(fn, i, lhss.data()); if (i == kinds.size()) - return m_builder.mk_eq_refl(g); + return mk_eq_refl(m_ctx, g); lean_assert(kinds[i] == congr_arg_kind::Eq); lean_assert(eqs[i]); - expr pr = m_builder.mk_congr_arg(g, *eqs[i]); + expr pr = mk_congr_arg(m_ctx, g, *eqs[i]); i++; for (; i < kinds.size(); i++) { if (kinds[i] == congr_arg_kind::Eq) { - pr = m_builder.mk_congr(pr, *eqs[i]); + pr = ::lean::mk_congr(m_ctx, pr, *eqs[i]); } else { lean_assert(kinds[i] == congr_arg_kind::Fixed); - pr = m_builder.mk_congr_fun(pr, lhss[i]); + pr = mk_congr_fun(m_ctx, pr, lhss[i]); } } return pr; @@ -120,7 +141,7 @@ struct congr_lemma_manager::imp { \remark This is an auxiliary method used by mk_congr_simp. */ expr mk_congr_proof(unsigned i, expr const & lhs, expr const & rhs, buffer> const & eqs) { if (i == eqs.size()) { - return m_builder.mk_eq_refl(rhs); + return mk_eq_refl(m_ctx, rhs); } else if (!eqs[i]) { return mk_congr_proof(i+1, lhs, rhs, eqs); } else { @@ -129,14 +150,14 @@ struct congr_lemma_manager::imp { lean_verify(is_eq(mlocal_type(major), x_1, x_2)); lean_assert(is_local(x_1)); lean_assert(is_local(x_2)); - expr motive_eq = m_builder.mk_eq(lhs, rhs); - expr motive = Fun(x_2, Fun(major, motive_eq)); + expr motive_eq = mk_eq(m_ctx, lhs, rhs); + expr motive = m_ctx.mk_lambda({x_2, major}, motive_eq); // We compute the new_rhs by replacing x_2 with x_1 and major with (eq.refl x_1) in rhs. expr new_rhs = instantiate(abstract_local(rhs, x_2), x_1); - expr x1_refl = m_builder.mk_eq_refl(x_1); + expr x1_refl = mk_eq_refl(m_ctx, x_1); new_rhs = instantiate(abstract_local(new_rhs, major), x1_refl); expr minor = mk_congr_proof(i+1, lhs, new_rhs, eqs); - return m_builder.mk_eq_drec(motive, minor, major); + return mk_eq_drec(m_ctx, motive, minor, major); } } @@ -158,6 +179,7 @@ struct congr_lemma_manager::imp { how the resulting term looks like. */ optional mk_congr_simp(expr const & fn, buffer const & pinfos, buffer const & kinds) { try { + type_context::tmp_locals locals(m_ctx); expr fn_type = relaxed_whnf(infer(fn)); name e_name("e"); buffer lhss; @@ -169,15 +191,15 @@ struct congr_lemma_manager::imp { trace_too_many_arguments(fn, pinfos.size()); return optional(); } - expr lhs = m_ctx.mk_tmp_local(binding_name(fn_type), binding_domain(fn_type)); + expr lhs = locals.push_local_from_binding(fn_type); lhss.push_back(lhs); hyps.push_back(lhs); switch (kinds[i]) { case congr_arg_kind::Eq: { - expr rhs = m_ctx.mk_tmp_local(binding_name(fn_type), binding_domain(fn_type)); - expr eq_type = m_builder.mk_eq(lhs, rhs); + expr rhs = locals.push_local_from_binding(fn_type); + expr eq_type = mk_eq(m_ctx, lhs, rhs); rhss.push_back(rhs); - expr eq = m_ctx.mk_tmp_local(e_name.append_after(eqs.size()+1), eq_type); + expr eq = locals.push_local(e_name.append_after(eqs.size()+1), eq_type); eqs.push_back(some_expr(eq)); hyps.push_back(rhs); hyps.push_back(eq); @@ -193,9 +215,10 @@ struct congr_lemma_manager::imp { lean_unreachable(); // TODO(Leo): not implemented yet break; case congr_arg_kind::Cast: { - expr rhs_type = mlocal_type(lhs); - rhs_type = instantiate_rev(abstract_locals(rhs_type, lhss.size()-1, lhss.data()), rhss.size(), rhss.data()); - expr rhs = cast(lhs, rhs_type, pinfos[i].get_dependencies(), eqs); + expr rhs_type = m_ctx.infer(lhs); + rhs_type = instantiate_rev(abstract_locals(rhs_type, lhss.size()-1, lhss.data()), + rhss.size(), rhss.data()); + expr rhs = cast(lhs, rhs_type, pinfos[i].get_back_deps(), eqs); rhss.push_back(rhs); eqs.push_back(none_expr()); break; @@ -204,15 +227,15 @@ struct congr_lemma_manager::imp { } expr lhs = mk_app(fn, lhss); expr rhs = mk_app(fn, rhss); - expr eq = m_builder.mk_eq(lhs, rhs); - expr congr_type = Pi(hyps, eq); + expr eq = mk_eq(m_ctx, lhs, rhs); + expr congr_type = m_ctx.mk_pi(hyps, eq); expr congr_proof; if (has_cast(kinds)) { congr_proof = mk_congr_proof(0, lhs, rhs, eqs); } else { congr_proof = mk_simple_congr_proof(fn, lhss, eqs, kinds); } - congr_proof = Fun(hyps, congr_proof); + congr_proof = m_ctx.mk_lambda(hyps, congr_proof); return optional(congr_type, congr_proof, to_list(kinds)); } catch (app_builder_exception &) { trace_app_builder_failure(fn); @@ -230,6 +253,7 @@ struct congr_lemma_manager::imp { optional mk_congr(expr const & fn, optional const & simp_lemma, buffer const & pinfos, buffer const & kinds) { try { + type_context::tmp_locals locals(m_ctx); expr fn_type1 = whnf(infer(fn)); expr fn_type2 = fn_type1; name e_name("e"); @@ -243,7 +267,7 @@ struct congr_lemma_manager::imp { trace_too_many_arguments(fn, pinfos.size()); return optional(); } - expr lhs = m_ctx.mk_tmp_local(binding_name(fn_type1), binding_domain(fn_type1)); + expr lhs = locals.push_local_from_binding(fn_type1); expr rhs; lhss.push_back(lhs); hyps.push_back(lhs); @@ -251,10 +275,10 @@ struct congr_lemma_manager::imp { switch (kinds[i]) { case congr_arg_kind::Eq: { lean_assert(m_ctx.is_def_eq(binding_domain(fn_type1), binding_domain(fn_type2))); - rhs = m_ctx.mk_tmp_local(binding_name(fn_type2), binding_domain(fn_type2)); - expr eq_type = m_builder.mk_eq(lhs, rhs); + rhs = locals.push_local_from_binding(fn_type2); + expr eq_type = mk_eq(m_ctx, lhs, rhs); rhss.push_back(rhs); - expr eq = m_ctx.mk_tmp_local(e_name.append_after(eqs.size()+1), eq_type); + expr eq = locals.push_local(e_name.append_after(eqs.size()+1), eq_type); eqs.push_back(some_expr(eq)); hyps.push_back(rhs); hyps.push_back(eq); @@ -273,7 +297,7 @@ struct congr_lemma_manager::imp { lean_unreachable(); // TODO(Leo): not implemented yet break; case congr_arg_kind::Cast: { - rhs = m_ctx.mk_tmp_local(binding_name(fn_type2), binding_domain(fn_type2)); + rhs = locals.push_local_from_binding(fn_type2); rhss.push_back(rhs); eqs.push_back(none_expr()); hyps.push_back(rhs); @@ -291,8 +315,8 @@ struct congr_lemma_manager::imp { lean_verify(is_eq(type1, lhs1, rhs1)); // build proof2 expr rhs2 = mk_app(fn, rhss); - expr eq = m_builder.mk_eq(lhs1, rhs2); - expr congr_type = Pi(hyps, eq); + expr eq = mk_eq(m_ctx, lhs1, rhs2); + expr congr_type = m_ctx.mk_pi(hyps, eq); // build proof that rhs1 = rhs2 unsigned i; for (i = 0; i < kinds.size(); i++) { @@ -301,26 +325,26 @@ struct congr_lemma_manager::imp { } if (i == kinds.size()) { // rhs1 and rhs2 are definitionally equal - expr congr_proof = Fun(hyps, pr1); + expr congr_proof = m_ctx.mk_lambda(hyps, pr1); return optional(congr_type, congr_proof, to_list(kinds)); } buffer rhss1; get_app_args_at_most(rhs1, rhss.size(), rhss1); lean_assert(rhss.size() == rhss1.size()); expr a = mk_app(fn, i, rhss1.data()); - expr pr2 = m_builder.mk_eq_refl(a); + expr pr2 = mk_eq_refl(m_ctx, a); for (; i < kinds.size(); i++) { if (kinds[i] == congr_arg_kind::Cast && !pinfos[i].is_prop()) { lean_assert(pinfos[i].is_subsingleton()); expr r1 = rhss1[i]; expr r2 = rhss[i]; - expr r1_eq_r2 = m_builder.mk_app(get_subsingleton_elim_name(), r1, r2); - pr2 = m_builder.mk_congr(pr2, r1_eq_r2); + expr r1_eq_r2 = mk_app(m_ctx, get_subsingleton_elim_name(), r1, r2); + pr2 = ::lean::mk_congr(m_ctx, pr2, r1_eq_r2); } else { - pr2 = m_builder.mk_congr_fun(pr2, rhss[i]); + pr2 = mk_congr_fun(m_ctx, pr2, rhss[i]); } } - expr congr_proof = Fun(hyps, m_builder.mk_eq_trans(pr1, pr2)); + expr congr_proof = m_ctx.mk_lambda(hyps, mk_eq_trans(m_ctx, pr1, pr2)); return optional(congr_type, congr_proof, to_list(kinds)); } catch (app_builder_exception &) { trace_app_builder_failure(fn); @@ -329,10 +353,10 @@ struct congr_lemma_manager::imp { } optional mk_congr_simp(expr const & fn, unsigned nargs, fun_info const & finfo) { - auto r = m_simp_cache.find(key(fn, nargs)); - if (r != m_simp_cache.end()) + auto r = m_cache.m_simp_cache.find(key(fn, nargs)); + if (r != m_cache.m_simp_cache.end()) return optional(r->second); - list const & result_deps = finfo.get_result_dependencies(); + list const & result_deps = finfo.get_result_deps(); buffer kinds; buffer pinfos; to_buffer(finfo.get_params_info(), pinfos); @@ -342,7 +366,7 @@ struct congr_lemma_manager::imp { kinds[i] = congr_arg_kind::Fixed; } else if (pinfos[i].is_subsingleton()) { // See comment at mk_congr. - if (!pinfos[i].is_prop() && pinfos[i].is_dep()) + if (!pinfos[i].is_prop() && pinfos[i].has_fwd_deps()) kinds[i] = congr_arg_kind::Fixed; else kinds[i] = congr_arg_kind::Cast; @@ -353,7 +377,7 @@ struct congr_lemma_manager::imp { } for (unsigned i = 0; i < pinfos.size(); i++) { for (unsigned j = i+1; j < pinfos.size(); j++) { - auto j_deps = pinfos[j].get_dependencies(); + auto j_deps = pinfos[j].get_back_deps(); if (std::find(j_deps.begin(), j_deps.end(), i) != j_deps.end() && kinds[j] == congr_arg_kind::Eq) { // We must fix i because there is a j that depends on i, @@ -365,7 +389,7 @@ struct congr_lemma_manager::imp { } auto new_r = mk_congr_simp(fn, pinfos, kinds); if (new_r) { - m_simp_cache.insert(mk_pair(key(fn, nargs), *new_r)); + m_cache.m_simp_cache.insert(mk_pair(key(fn, nargs), *new_r)); return new_r; } else if (has_cast(kinds)) { // remove casts and try again @@ -375,7 +399,7 @@ struct congr_lemma_manager::imp { } auto new_r = mk_congr_simp(fn, pinfos, kinds); if (new_r) { - m_simp_cache.insert(mk_pair(key(fn, nargs), *new_r)); + m_cache.m_simp_cache.insert(mk_pair(key(fn, nargs), *new_r)); return new_r; } else { return new_r; @@ -385,9 +409,14 @@ struct congr_lemma_manager::imp { } } + optional mk_congr_simp(expr const & fn, unsigned nargs) { + fun_info finfo = get_fun_info(m_ctx, fn, nargs); + return mk_congr_simp(fn, nargs, finfo); + } + optional mk_congr(expr const & fn, unsigned nargs, fun_info const & finfo) { - auto r = m_cache.find(key(fn, nargs)); - if (r != m_cache.end()) + auto r = m_cache.m_cache.find(key(fn, nargs)); + if (r != m_cache.m_cache.end()) return optional(r->second); optional simp_lemma = mk_congr_simp(fn, nargs); if (!simp_lemma) @@ -404,24 +433,24 @@ struct congr_lemma_manager::imp { lean_assert(kinds.size() == pinfos.size()); bool has_cast = false; for (unsigned i = 0; i < kinds.size(); i++) { - if (!pinfos[i].is_prop() && pinfos[i].is_subsingleton() && pinfos[i].is_dep()) { + if (!pinfos[i].is_prop() && pinfos[i].is_subsingleton() && pinfos[i].has_fwd_deps()) { kinds[i] = congr_arg_kind::Fixed; } if (kinds[i] == congr_arg_kind::Cast) has_cast = true; } if (!has_cast) { - m_cache.insert(mk_pair(key(fn, nargs), *simp_lemma)); + m_cache.m_cache.insert(mk_pair(key(fn, nargs), *simp_lemma)); return simp_lemma; // simp_lemma will be identical to regular congr lemma } auto new_r = mk_congr(fn, simp_lemma, pinfos, kinds); if (new_r) - m_cache.insert(mk_pair(key(fn, nargs), *new_r)); + m_cache.m_cache.insert(mk_pair(key(fn, nargs), *new_r)); return new_r; } void pre_specialize(expr const & a, expr & g, unsigned & prefix_sz, unsigned & num_rest_args) { - fun_info finfo = m_fmanager.get_specialized(a); + fun_info finfo = get_specialized_fun_info(m_ctx, a); prefix_sz = 0; for (param_info const & pinfo : finfo.get_params_info()) { if (!pinfo.specialized()) @@ -445,31 +474,33 @@ struct congr_lemma_manager::imp { expr mk_hcongr_proof(expr type) { expr A, B, a, b; if (is_eq(type, a, b)) { - return m_builder.mk_eq_refl(a); + return mk_eq_refl(m_ctx, a); } else if (is_heq(type, A, a, B, b)) { - return m_builder.mk_heq_refl(a); + return mk_heq_refl(m_ctx, a); } else { + type_context::tmp_locals locals(m_ctx); lean_assert(is_pi(type) && is_pi(binding_body(type)) && is_pi(binding_body(binding_body(type)))); - expr a = m_ctx.mk_tmp_local(binding_name(type), binding_domain(type)); + expr a = locals.push_local_from_binding(type); type = instantiate(binding_body(type), a); - expr b = m_ctx.mk_tmp_local(binding_name(type), binding_domain(type)); + expr b = locals.push_local_from_binding(type); expr motive = instantiate(binding_body(type), b); type = instantiate(binding_body(type), a); - expr eq_pr = m_ctx.mk_tmp_local(binding_name(motive), binding_domain(motive)); + expr eq_pr = locals.push_local_from_binding(motive); type = binding_body(type); motive = binding_body(motive); lean_assert(closed(type) && closed(motive)); expr minor = mk_hcongr_proof(type); expr major = eq_pr; if (is_heq(mlocal_type(eq_pr))) - major = m_builder.mk_eq_of_heq(eq_pr); + major = mk_eq_of_heq(m_ctx, eq_pr); motive = Fun(b, motive); - return Fun({a, b, eq_pr}, m_builder.mk_eq_rec(motive, minor, major)); + return m_ctx.mk_lambda({a, b, eq_pr}, mk_eq_rec(m_ctx, motive, minor, major)); } } optional mk_hcongr_core(expr const & fn, unsigned nargs) { try { + type_context::tmp_locals locals(m_ctx); expr fn_type_lhs = relaxed_whnf(infer(fn)); expr fn_type_rhs = fn_type_lhs; name e_name("e"); @@ -483,19 +514,19 @@ struct congr_lemma_manager::imp { trace_too_many_arguments(fn, nargs); return optional(); } - expr lhs = m_ctx.mk_tmp_local(binding_name(fn_type_lhs), binding_domain(fn_type_lhs)); + expr lhs = locals.push_local_from_binding(fn_type_lhs); lhss.push_back(lhs); hyps.push_back(lhs); - expr rhs = m_ctx.mk_tmp_local(binding_name(fn_type_rhs).append_after("'"), binding_domain(fn_type_rhs)); + expr rhs = locals.push_local(binding_name(fn_type_rhs).append_after("'"), binding_domain(fn_type_rhs)); rhss.push_back(rhs); hyps.push_back(rhs); expr eq_type; if (binding_domain(fn_type_lhs) == binding_domain(fn_type_rhs)) { - eq_type = m_builder.mk_eq(lhs, rhs); + eq_type = mk_eq(m_ctx, lhs, rhs); kinds.push_back(congr_arg_kind::Eq); } else { - eq_type = m_builder.mk_heq(lhs, rhs); + eq_type = mk_heq(m_ctx, lhs, rhs); kinds.push_back(congr_arg_kind::HEq); } - expr h_eq = m_ctx.mk_tmp_local(e_name.append_after(i), eq_type); + expr h_eq = locals.push_local(e_name.append_after(i), eq_type); eqs.push_back(h_eq); hyps.push_back(h_eq); fn_type_lhs = relaxed_whnf(instantiate(binding_body(fn_type_lhs), lhs)); fn_type_rhs = relaxed_whnf(instantiate(binding_body(fn_type_rhs), rhs)); @@ -504,11 +535,11 @@ struct congr_lemma_manager::imp { expr rhs = mk_app(fn, rhss); expr eq_type; if (fn_type_lhs == fn_type_rhs) { - eq_type = m_builder.mk_eq(lhs, rhs); + eq_type = mk_eq(m_ctx, lhs, rhs); } else { - eq_type = m_builder.mk_heq(lhs, rhs); + eq_type = mk_heq(m_ctx, lhs, rhs); } - expr result_type = Pi(hyps, eq_type); + expr result_type = m_ctx.mk_pi(hyps, eq_type); expr result_proof = mk_hcongr_proof(result_type); return optional(result_type, result_proof, to_list(kinds)); } catch (app_builder_exception &) { @@ -517,20 +548,8 @@ struct congr_lemma_manager::imp { } } -public: - imp(app_builder & b, fun_info_manager & fm): - m_builder(b), m_fmanager(fm), m_ctx(fm.ctx()), - m_relation_info_getter(mk_relation_info_getter(fm.ctx().env())) {} - - old_type_context & ctx() { return m_ctx; } - - optional mk_congr_simp(expr const & fn, unsigned nargs) { - fun_info finfo = m_fmanager.get(fn, nargs); - return mk_congr_simp(fn, nargs, finfo); - } - optional mk_congr_simp(expr const & fn) { - fun_info finfo = m_fmanager.get(fn); + fun_info finfo = get_fun_info(m_ctx, fn); return mk_congr_simp(fn, finfo.get_arity(), finfo); } @@ -539,24 +558,24 @@ public: expr g; unsigned prefix_sz, num_rest_args; pre_specialize(a, g, prefix_sz, num_rest_args); key k(g, num_rest_args); - auto it = m_simp_cache_spec.find(k); - if (it != m_simp_cache_spec.end()) + auto it = m_cache.m_simp_cache_spec.find(k); + if (it != m_cache.m_simp_cache_spec.end()) return optional(it->second); auto r = mk_congr_simp(g, num_rest_args); if (!r) return optional(); result new_r = mk_specialize_result(*r, prefix_sz); - m_simp_cache_spec.insert(mk_pair(k, new_r)); + m_cache.m_simp_cache_spec.insert(mk_pair(k, new_r)); return optional(new_r); } optional mk_congr(expr const & fn, unsigned nargs) { - fun_info finfo = m_fmanager.get(fn, nargs); + fun_info finfo = get_fun_info(m_ctx, fn, nargs); return mk_congr(fn, nargs, finfo); } optional mk_congr(expr const & fn) { - fun_info finfo = m_fmanager.get(fn); + fun_info finfo = get_fun_info(m_ctx, fn); return mk_congr(fn, finfo.get_arity(), finfo); } @@ -565,30 +584,30 @@ public: expr g; unsigned prefix_sz, num_rest_args; pre_specialize(a, g, prefix_sz, num_rest_args); key k(g, num_rest_args); - auto it = m_cache_spec.find(k); - if (it != m_cache_spec.end()) + auto it = m_cache.m_cache_spec.find(k); + if (it != m_cache.m_cache_spec.end()) return optional(it->second); auto r = mk_congr(g, num_rest_args); if (!r) { return optional(); } result new_r = mk_specialize_result(*r, prefix_sz); - m_cache_spec.insert(mk_pair(k, new_r)); + m_cache.m_cache_spec.insert(mk_pair(k, new_r)); return optional(new_r); } optional mk_hcongr(expr const & fn, unsigned nargs) { - auto r = m_hcache.find(key(fn, nargs)); - if (r != m_hcache.end()) + auto r = m_cache.m_hcache.find(key(fn, nargs)); + if (r != m_cache.m_hcache.end()) return optional(r->second); auto new_r = mk_hcongr_core(fn, nargs); if (new_r) - m_hcache.insert(mk_pair(key(fn, nargs), *new_r)); + m_cache.m_hcache.insert(mk_pair(key(fn, nargs), *new_r)); return new_r; } optional mk_hcongr(expr const & fn) { - fun_info finfo = m_fmanager.get(fn); + fun_info finfo = get_fun_info(m_ctx, fn); return mk_hcongr(fn, finfo.get_arity()); } @@ -606,14 +625,15 @@ public: if (!is_constant(R)) return optional(); name const & R_name = const_name(R); - auto info = m_relation_info_getter(R_name); + auto info = m_cache.m_relation_info_getter(R_name); if (!info) return optional(); unsigned arity = info->get_arity(); key k(R, arity); - auto r = m_rel_cache[is_iff].find(k); - if (r != m_rel_cache[is_iff].end()) + auto r = m_cache.m_rel_cache[is_iff].find(k); + if (r != m_cache.m_rel_cache[is_iff].end()) return optional(r->second); + type_context::tmp_locals locals(m_ctx); buffer hyps; buffer kinds; expr a1, b1, a2, b2; @@ -623,19 +643,19 @@ public: R_type = relaxed_whnf(R_type); if (!is_pi(R_type)) return optional(); - expr h = m_ctx.mk_tmp_local(binding_name(R_type), binding_domain(R_type)); + expr h = locals.push_local_from_binding(R_type); if (i == info->get_lhs_pos()) { a1 = h; - a2 = m_ctx.mk_tmp_local(binding_name(R_type), binding_domain(R_type)); - H1 = m_ctx.mk_tmp_local("H1", m_builder.mk_rel(R_name, a1, a2)); + a2 = locals.push_local_from_binding(R_type); + H1 = locals.push_local("H1", mk_rel(m_ctx, R_name, a1, a2)); hyps.push_back(a1); hyps.push_back(a2); hyps.push_back(H1); kinds.push_back(congr_arg_kind::Eq); } else if (i == info->get_rhs_pos()) { b1 = h; - b2 = m_ctx.mk_tmp_local(binding_name(R_type), binding_domain(R_type)); - H2 = m_ctx.mk_tmp_local("H2", m_builder.mk_rel(R_name, b1, b2)); + b2 = locals.push_local_from_binding(R_type); + H2 = locals.push_local("H2", mk_rel(m_ctx, R_name, b1, b2)); hyps.push_back(b1); hyps.push_back(b2); hyps.push_back(H2); @@ -646,27 +666,29 @@ public: } R_type = instantiate(binding_body(R_type), h); } - expr lhs = m_builder.mk_rel(R_name, a1, b1); - expr rhs = m_builder.mk_rel(R_name, a2, b2); + expr lhs = mk_rel(m_ctx, R_name, a1, b1); + expr rhs = mk_rel(m_ctx, R_name, a2, b2); // (H1 : R a1 a2) -> (H2 : R b1 b2) -> (R a1 b1 <-> R a2 b2) - expr type = is_iff ? m_builder.mk_iff(lhs, rhs) : m_builder.mk_eq(lhs, rhs); - type = Pi(hyps, type); + expr type = is_iff ? mk_iff(m_ctx, lhs, rhs) : mk_eq(m_ctx, lhs, rhs); + type = m_ctx.mk_pi(hyps, type); /* Proof: iff.intro (λ H : R a1 b1, trans (symm H1) (trans H H2)) (λ H : R a2 b2, trans H1 (trans H (symm H2))) */ expr H; - H = m_ctx.mk_tmp_local(lhs); - expr p1 = Fun(H, m_builder.mk_trans(R_name, m_builder.mk_symm(R_name, H1), m_builder.mk_trans(R_name, H, H2))); - H = m_ctx.mk_tmp_local(rhs); - expr p2 = Fun(H, m_builder.mk_trans(R_name, H1, m_builder.mk_trans(R_name, H, m_builder.mk_symm(R_name, H2)))); - expr pr = m_builder.mk_app(get_iff_intro_name(), p1, p2); + H = locals.push_local("lhs", lhs); + expr p1 = m_ctx.mk_lambda({H}, mk_trans(m_ctx, R_name, mk_symm(m_ctx, R_name, H1), + mk_trans(m_ctx, R_name, H, H2))); + H = locals.push_local("rhs", rhs); + expr p2 = m_ctx.mk_lambda({H}, mk_trans(m_ctx, R_name, H1, mk_trans(m_ctx, R_name, H, + mk_symm(m_ctx, R_name, H2)))); + expr pr = mk_app(m_ctx, get_iff_intro_name(), p1, p2); if (!is_iff) - pr = m_builder.mk_app(get_propext_name(), pr); - pr = Fun(hyps, pr); + pr = mk_app(m_ctx, get_propext_name(), pr); + pr = m_ctx.mk_lambda(hyps, pr); result res(type, pr, to_list(kinds)); - m_rel_cache[is_iff].insert(mk_pair(k, res)); + m_cache.m_rel_cache[is_iff].insert(mk_pair(k, res)); return optional(res); } catch (app_builder_exception &) { trace_app_builder_failure(R); @@ -681,59 +703,45 @@ public: optional mk_rel_eq_congr(expr const & R) { return mk_rel_congr(R, false); } - - unsigned get_specialization_prefix_size(expr const & fn, unsigned nargs) { - return m_fmanager.get_specialization_prefix_size(fn, nargs); - } }; -congr_lemma_manager::congr_lemma_manager(app_builder & b, fun_info_manager & fm): - m_ptr(new imp(b, fm)) { +optional mk_congr_simp(type_context & ctx, expr const & fn) { + return congr_lemma_manager(ctx).mk_congr_simp(fn); } -congr_lemma_manager::~congr_lemma_manager() { +optional mk_congr_simp(type_context & ctx, expr const & fn, unsigned nargs) { + return congr_lemma_manager(ctx).mk_congr_simp(fn, nargs); } -old_type_context & congr_lemma_manager::ctx() { return m_ptr->ctx(); } - -auto congr_lemma_manager::mk_congr_simp(expr const & fn) -> optional { - return m_ptr->mk_congr_simp(fn); -} -auto congr_lemma_manager::mk_congr_simp(expr const & fn, unsigned nargs) -> optional { - return m_ptr->mk_congr_simp(fn, nargs); -} -auto congr_lemma_manager::mk_specialized_congr_simp(expr const & a) -> optional { - return m_ptr->mk_specialized_congr_simp(a); -} -auto congr_lemma_manager::mk_congr(expr const & fn) -> optional { - return m_ptr->mk_congr(fn); -} -auto congr_lemma_manager::mk_congr(expr const & fn, unsigned nargs) -> optional { - return m_ptr->mk_congr(fn, nargs); -} -auto congr_lemma_manager::mk_specialized_congr(expr const & fn) -> optional { - return m_ptr->mk_specialized_congr(fn); -} -auto congr_lemma_manager::mk_hcongr(expr const & fn) -> optional { - return m_ptr->mk_hcongr(fn); -} -auto congr_lemma_manager::mk_hcongr(expr const & fn, unsigned nargs) -> optional { - return m_ptr->mk_hcongr(fn, nargs); -} -auto congr_lemma_manager::mk_rel_iff_congr(expr const & R) -> optional { - return m_ptr->mk_rel_iff_congr(R); -} -auto congr_lemma_manager::mk_rel_eq_congr(expr const & R) -> optional { - return m_ptr->mk_rel_eq_congr(R); -} -unsigned congr_lemma_manager::get_specialization_prefix_size(expr const & fn, unsigned nargs) { - return m_ptr->get_specialization_prefix_size(fn, nargs); +optional mk_specialized_congr_simp(type_context & ctx, expr const & a) { + return congr_lemma_manager(ctx).mk_specialized_congr_simp(a); } -void initialize_congr_lemma_manager() { - register_trace_class("congruence_manager"); +optional mk_congr(type_context & ctx, expr const & fn) { + return congr_lemma_manager(ctx).mk_congr(fn); } -void finalize_congr_lemma_manager() { +optional mk_congr(type_context & ctx, expr const & fn, unsigned nargs) { + return congr_lemma_manager(ctx).mk_congr(fn, nargs); +} + +optional mk_specialized_congr(type_context & ctx, expr const & a) { + return congr_lemma_manager(ctx).mk_specialized_congr(a); +} + +optional mk_hcongr(type_context & ctx, expr const & fn) { + return congr_lemma_manager(ctx).mk_hcongr(fn); +} + +optional mk_hcongr(type_context & ctx, expr const & fn, unsigned nargs) { + return congr_lemma_manager(ctx).mk_hcongr(fn, nargs); +} + +optional mk_rel_iff_congr(type_context & ctx, expr const & R) { + return congr_lemma_manager(ctx).mk_rel_iff_congr(R); +} + +optional mk_rel_eq_congr(type_context & ctx, expr const & R) { + return congr_lemma_manager(ctx).mk_rel_eq_congr(R); } } diff --git a/src/library/congr_lemma_manager.h b/src/library/congr_lemma.h similarity index 50% rename from src/library/congr_lemma_manager.h rename to src/library/congr_lemma.h index e77acccf17..ace11693c7 100644 --- a/src/library/congr_lemma_manager.h +++ b/src/library/congr_lemma.h @@ -1,13 +1,11 @@ /* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Copyright (c) 2016 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include -#include "library/app_builder.h" -#include "library/fun_info_manager.h" +#include "library/type_context.h" namespace lean { enum class congr_arg_kind { @@ -40,41 +38,27 @@ public: bool all_eq_kind() const; }; -class congr_lemma_manager { - struct imp; - std::unique_ptr m_ptr; -public: - congr_lemma_manager(app_builder & b, fun_info_manager & fm); - ~congr_lemma_manager(); - typedef congr_lemma result; +optional mk_congr_simp(type_context & ctx, expr const & fn); +optional mk_congr_simp(type_context & ctx, expr const & fn, unsigned nargs); +/* Create a specialized theorem using (a prefix of) the arguments of the given application. */ +optional mk_specialized_congr_simp(type_context & ctx, expr const & a); - old_type_context & ctx(); - unsigned get_specialization_prefix_size(expr const & fn, unsigned nargs); +optional mk_congr(type_context & ctx, expr const & fn); +optional mk_congr(type_context & ctx, expr const & fn, unsigned nargs); +/* Create a specialized theorem using (a prefix of) the arguments of the given application. */ +optional mk_specialized_congr(type_context & ctx, expr const & a); - optional mk_congr_simp(expr const & fn); - optional mk_congr_simp(expr const & fn, unsigned nargs); - /* Create a specialized theorem using (a prefix of) the arguments of the given application. */ - optional mk_specialized_congr_simp(expr const & a); +optional mk_hcongr(type_context & ctx, expr const & fn); +optional mk_hcongr(type_context & ctx, expr const & fn, unsigned nargs); - optional mk_congr(expr const & fn); - optional mk_congr(expr const & fn, unsigned nargs); - /* Create a specialized theorem using (a prefix of) the arguments of the given application. */ - optional mk_specialized_congr(expr const & a); +/** \brief If R is an equivalence relation, construct the congruence lemma - optional mk_hcongr(expr const & fn); - optional mk_hcongr(expr const & fn, unsigned nargs); + R a1 a2 -> R b1 b2 -> (R a1 b1) <-> (R a2 b2) */ +optional mk_rel_iff_congr(type_context & ctx, expr const & R); - /** \brief If R is an equivalence relation, construct the congruence lemma +/** \brief Similar to previous one. + It returns none if propext is not available. - R a1 a2 -> R b1 b2 -> (R a1 b1) <-> (R a2 b2) */ - optional mk_rel_iff_congr(expr const & R); - - /** \brief Similar to previous one. - It returns none if propext is not available. - - R a1 a2 -> R b1 b2 -> (R a1 b1) = (R a2 b2) */ - optional mk_rel_eq_congr(expr const & R); -}; -void initialize_congr_lemma_manager(); -void finalize_congr_lemma_manager(); + R a1 a2 -> R b1 b2 -> (R a1 b1) = (R a2 b2) */ +optional mk_rel_eq_congr(type_context & ctx, expr const & R); }