From 96fa8856bc0e192446f39bdfcf06c5365d548112 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Sep 2016 14:06:42 -0700 Subject: [PATCH] feat(library/equations_compiler): add mk_nonrec --- src/frontends/lean/decl_util.cpp | 31 ++++++++------- src/frontends/lean/decl_util.h | 4 +- src/frontends/lean/definition_cmds.cpp | 6 +-- src/library/equations_compiler/compiler.cpp | 2 +- src/library/equations_compiler/elim_match.cpp | 32 +++++++++++++++ src/library/equations_compiler/elim_match.h | 2 + src/library/equations_compiler/equations.cpp | 5 ++- src/library/equations_compiler/equations.h | 13 ++++--- .../equations_compiler/structural_rec.cpp | 2 +- src/library/equations_compiler/util.cpp | 39 +++++++++++++------ src/library/equations_compiler/util.h | 2 +- 11 files changed, 96 insertions(+), 42 deletions(-) diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp index 0fa51a45d4..08a3faed42 100644 --- a/src/frontends/lean/decl_util.cpp +++ b/src/frontends/lean/decl_util.cpp @@ -268,6 +268,7 @@ struct definition_info { name m_prefix; bool m_is_private{false}; bool m_is_meta{false}; + bool m_is_noncomputable{false}; bool m_is_lemma{false}; bool m_aux_lemmas{false}; unsigned m_next_match_idx{1}; @@ -276,19 +277,20 @@ struct definition_info { MK_THREAD_LOCAL_GET_DEF(definition_info, get_definition_info); declaration_info_scope::declaration_info_scope(environment const & env, bool is_private, bool is_meta, - bool is_lemma, bool aux_lemmas) { + bool is_noncomputable, bool is_lemma, bool aux_lemmas) { definition_info & info = get_definition_info(); lean_assert(info.m_prefix.is_anonymous()); - info.m_prefix = is_private ? name() : get_namespace(env); - info.m_is_private = is_private; - info.m_is_meta = is_meta; - info.m_is_lemma = is_lemma; - info.m_aux_lemmas = aux_lemmas; + info.m_prefix = is_private ? name() : get_namespace(env); + info.m_is_private = is_private; + info.m_is_meta = is_meta; + info.m_is_noncomputable = is_noncomputable; + info.m_is_lemma = is_lemma; + info.m_aux_lemmas = aux_lemmas; info.m_next_match_idx = 1; } -declaration_info_scope::declaration_info_scope(environment const & env, bool is_private, def_cmd_kind k): - declaration_info_scope(env, is_private, k == MetaDefinition, k == Theorem, k == Definition) {} +declaration_info_scope::declaration_info_scope(environment const & env, bool is_private, bool is_noncomputable, def_cmd_kind k): + declaration_info_scope(env, is_private, k == MetaDefinition, is_noncomputable, k == Theorem, k == Definition) {} declaration_info_scope::~declaration_info_scope() { definition_info & info = get_definition_info(); @@ -297,12 +299,13 @@ declaration_info_scope::~declaration_info_scope() { equations_header mk_equations_header(list const & ns) { equations_header h; - h.m_num_fns = length(ns); - h.m_fn_names = ns; - h.m_is_private = get_definition_info().m_is_private; - h.m_is_meta = get_definition_info().m_is_meta; - h.m_is_lemma = get_definition_info().m_is_lemma; - h.m_aux_lemmas = get_definition_info().m_aux_lemmas; + h.m_num_fns = length(ns); + h.m_fn_names = ns; + h.m_is_private = get_definition_info().m_is_private; + h.m_is_meta = get_definition_info().m_is_meta; + h.m_is_noncomputable = get_definition_info().m_is_noncomputable; + h.m_is_lemma = get_definition_info().m_is_lemma; + h.m_aux_lemmas = get_definition_info().m_aux_lemmas; return h; } diff --git a/src/frontends/lean/decl_util.h b/src/frontends/lean/decl_util.h index 5738cf0a15..1dcb6db9db 100644 --- a/src/frontends/lean/decl_util.h +++ b/src/frontends/lean/decl_util.h @@ -77,8 +77,8 @@ environment add_local_ref(parser & p, environment const & env, name const & c_na nested definitions. */ class declaration_info_scope { public: - declaration_info_scope(environment const & env, bool is_private, bool is_meta, bool is_lemma, bool aux_lemmas); - declaration_info_scope(environment const & env, bool is_private, def_cmd_kind k); + declaration_info_scope(environment const & env, bool is_private, bool is_meta, bool is_noncomputable, bool is_lemma, bool aux_lemmas); + declaration_info_scope(environment const & env, bool is_private, bool is_noncomputable, def_cmd_kind k); ~declaration_info_scope(); }; diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 866219b13b..cf9368c844 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -130,11 +130,11 @@ expr parse_mutual_definition(parser & p, buffer & lp_names, buffer & return r; } -environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, bool is_private, bool /* is_protected */, bool /* is_noncomputable */, +environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, bool is_private, bool /* is_protected */, bool is_noncomputable, decl_attributes /* attrs */) { buffer lp_names; buffer fns, params; - declaration_info_scope scope(p.env(), is_private, kind); + declaration_info_scope scope(p.env(), is_private, is_noncomputable, kind); expr val = parse_mutual_definition(p, lp_names, fns, params); if (p.used_sorry()) p.declare_sorry(); elaborator elab(p.env(), p.get_options(), metavar_context(), local_context()); @@ -333,7 +333,7 @@ environment xdefinition_cmd_core(parser & p, def_cmd_kind kind, bool is_private, buffer params; expr fn, val; auto header_pos = p.pos(); - declaration_info_scope scope(p.env(), is_private, kind); + declaration_info_scope scope(p.env(), is_private, is_noncomputable, kind); std::tie(fn, val) = parse_definition(p, lp_names, params, kind == def_cmd_kind::Example); if (p.used_sorry()) p.declare_sorry(); elaborator elab(p.env(), p.get_options(), metavar_context(), local_context()); diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp index 78fc3846a9..03c24b6360 100644 --- a/src/library/equations_compiler/compiler.cpp +++ b/src/library/equations_compiler/compiler.cpp @@ -22,7 +22,7 @@ expr compile_equations(environment & env, options const & opts, metavar_context trace_compiler(tout() << "recursive: " << is_recursive_eqns(ctx, eqns) << "\n";); if (equations_num_fns(eqns) == 1) { if (!is_recursive_eqns(ctx, eqns)) { - return elim_match(env, opts, mctx, lctx, eqns).m_fn; + return mk_nonrec(env, opts, mctx, lctx, eqns); } else if (optional r = try_structural_rec(env, opts, mctx, lctx, eqns)) { return *r; } diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 2a14e51467..ff30f5e98a 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -1151,6 +1151,38 @@ elim_match_result elim_match(environment & env, options const & opts, metavar_co return r; } +expr mk_nonrec(environment & env, options const & opts, metavar_context & mctx, + local_context const & lctx, expr const & eqns) { + equations_header header = get_equations_header(eqns); + auto R = elim_match(env, opts, mctx, lctx, eqns); + type_context ctx1(env, opts, mctx, lctx, transparency_mode::Semireducible); + expr fn_type = ctx1.infer(R.m_fn); + expr fn; + std::tie(env, fn) = mk_aux_definition(env, mctx, lctx, header.m_is_private, header.m_is_lemma, header.m_is_noncomputable, + head(header.m_fn_names), fn_type, R.m_fn); + name fn_name = const_name(get_app_fn(fn)); + unsigned eqn_idx = 1; + type_context ctx2(env, opts, mctx, lctx, transparency_mode::Semireducible); + for (expr type : R.m_lemmas) { + type_context::tmp_locals locals(ctx2); + type = ctx2.relaxed_whnf(type); + while (is_pi(type)) { + expr local = locals.push_local_from_binding(type); + type = instantiate(binding_body(type), local); + } + lean_assert(is_eq(type)); + expr lhs = app_arg(app_fn(type)); + expr rhs = app_arg(type); + buffer lhs_args; + get_app_args(lhs, lhs_args); + expr new_lhs = mk_app(fn, lhs_args); + env = mk_equation_lemma(env, opts, mctx, ctx2.lctx(), fn_name, + eqn_idx, header.m_is_private, locals.as_buffer(), new_lhs, rhs); + eqn_idx++; + } + return fn; +} + void initialize_elim_match() { register_trace_class({"eqn_compiler", "elim_match"}); register_trace_class({"debug", "eqn_compiler", "elim_match"}); diff --git a/src/library/equations_compiler/elim_match.h b/src/library/equations_compiler/elim_match.h index 3e59f0aeea..258a0547ab 100644 --- a/src/library/equations_compiler/elim_match.h +++ b/src/library/equations_compiler/elim_match.h @@ -13,6 +13,8 @@ struct elim_match_result { elim_match_result(expr const & fn, list const & lemmas):m_fn(fn), m_lemmas(lemmas) {} }; elim_match_result elim_match(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx, expr const & eqns); +expr mk_nonrec(environment & env, options const & opts, metavar_context & mctx, + local_context const & lctx, expr const & eqns); void initialize_elim_match(); void finalize_elim_match(); } diff --git a/src/library/equations_compiler/equations.cpp b/src/library/equations_compiler/equations.cpp index 9d5eac0e88..076edd37fe 100644 --- a/src/library/equations_compiler/equations.cpp +++ b/src/library/equations_compiler/equations.cpp @@ -51,7 +51,7 @@ public: virtual optional expand(expr const &, abstract_type_context &) const { throw_eqs_ex(); } virtual void write(serializer & s) const { s << *g_equations_opcode << m_header.m_num_fns << m_header.m_is_private << m_header.m_is_meta - << m_header.m_is_lemma << m_header.m_aux_lemmas; + << m_header.m_is_noncomputable << m_header.m_is_lemma << m_header.m_aux_lemmas; write_list(s, m_header.m_fn_names); } equations_header const & get_header() const { return m_header; } @@ -229,7 +229,8 @@ void initialize_equations() { register_macro_deserializer(*g_equations_opcode, [](deserializer & d, unsigned num, expr const * args) { equations_header h; - d >> h.m_num_fns >> h.m_is_private >> h.m_is_meta >> h.m_is_lemma >> h.m_aux_lemmas; + d >> h.m_num_fns >> h.m_is_private >> h.m_is_meta >> h.m_is_noncomputable + >> h.m_is_lemma >> h.m_aux_lemmas; h.m_fn_names = read_list(d); if (num == 0 || h.m_num_fns == 0) throw corrupted_stream_exception(); diff --git a/src/library/equations_compiler/equations.h b/src/library/equations_compiler/equations.h index 2953bbb1c7..6b041d05c2 100644 --- a/src/library/equations_compiler/equations.h +++ b/src/library/equations_compiler/equations.h @@ -28,12 +28,13 @@ expr mk_inaccessible(expr const & e); bool is_inaccessible(expr const & e); struct equations_header { - unsigned m_num_fns{0}; /* number of functions being defined */ - list m_fn_names; /* names for functions */ - bool m_is_private{false}; /* if true, it must be a private definition */ - bool m_is_lemma{false}; /* if true, equations are defining a lemma */ - bool m_is_meta{false}; /* the auxiliary declarations should be tagged as meta */ - bool m_aux_lemmas{false}; /* if true, we must create equation lemmas and induction principle */ + unsigned m_num_fns{0}; /* number of functions being defined */ + list m_fn_names; /* names for functions */ + bool m_is_private{false}; /* if true, it must be a private definition */ + bool m_is_lemma{false}; /* if true, equations are defining a lemma */ + bool m_is_meta{false}; /* the auxiliary declarations should be tagged as meta */ + bool m_is_noncomputable{false}; /* if true, equation is not computable and code should not be generated */ + bool m_aux_lemmas{false}; /* if true, we must create equation lemmas and induction principle */ equations_header() {} equations_header(unsigned num_fns):m_num_fns(num_fns) {} }; diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp index 255194dd43..a0c50f46da 100644 --- a/src/library/equations_compiler/structural_rec.cpp +++ b/src/library/equations_compiler/structural_rec.cpp @@ -610,7 +610,7 @@ struct structural_rec_fn { } else { expr r; std::tie(m_env, r) = mk_aux_definition(m_env, m_mctx, m_lctx, m_header.m_is_private, m_header.m_is_lemma, - head(m_header.m_fn_names), m_fn_type, new_fn); + m_header.m_is_noncomputable, head(m_header.m_fn_names), m_fn_type, new_fn); return r; } } diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 0a600ca49d..af2f3c97ac 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -28,13 +28,22 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_EQN_COMPILER_DSIMP true #endif +#ifndef LEAN_DEFAULT_EQN_COMPILER_LEMMAS +#define LEAN_DEFAULT_EQN_COMPILER_LEMMAS true +#endif + namespace lean { -static name * g_eqn_compiler_dsimp = nullptr; +static name * g_eqn_compiler_dsimp = nullptr; +static name * g_eqn_compiler_lemmas = nullptr; static bool get_eqn_compiler_dsimp(options const & o) { return o.get_bool(*g_eqn_compiler_dsimp, LEAN_DEFAULT_EQN_COMPILER_DSIMP); } +static bool get_eqn_compiler_lemmas(options const & o) { + return o.get_bool(*g_eqn_compiler_lemmas, LEAN_DEFAULT_EQN_COMPILER_LEMMAS); +} + [[ noreturn ]] void throw_ill_formed_eqns() { throw exception("ill-formed match/equations expression"); } @@ -228,7 +237,8 @@ static pair mk_def_name(environment const & env, bool is_priv } pair mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx, - bool is_private, bool is_lemma, name const & c, expr const & type, expr const & value) { + bool is_private, bool is_lemma, bool is_noncomputable, + name const & c, expr const & type, expr const & value) { environment new_env = env; name new_c; std::tie(new_env, new_c) = mk_def_name(env, is_private, c); @@ -236,7 +246,7 @@ pair mk_aux_definition(environment const & env, metavar_conte std::tie(new_env, r) = is_lemma ? mk_aux_lemma(new_env, mctx, lctx, new_c, type, value) : mk_aux_definition(new_env, mctx, lctx, new_c, type, value); - if (!is_lemma) { + if (!is_lemma && !is_noncomputable) { try { declaration d = new_env.get(new_c); new_env = vm_compile(new_env, d); @@ -397,7 +407,14 @@ static expr prove_eqn_lemma_core(type_context & ctx, buffer const & Hs, ex expr const & c = ite_args[0]; expr c_lhs, c_rhs; lean_verify(is_eq(c, c_lhs, c_rhs)); - if (ctx.is_def_eq(c_lhs, c_rhs)) { + if (auto H = find_if_neg_hypothesis(ctx, c, Hs)) { + expr lhs_else = ite_args[4]; + expr A = ite_args[2]; + level A_lvl = get_level(ctx, A); + expr H1 = mk_app(mk_constant(get_if_neg_name(), {A_lvl}), {c, ite_args[1], *H, A, ite_args[3], lhs_else}); + expr H2 = prove_eqn_lemma_core(ctx, Hs, lhs_else, rhs); + return mk_app(mk_constant(get_eq_trans_name(), {A_lvl}), {A, lhs, lhs_else, rhs, H1, H2}); + } else if (ctx.is_def_eq(c_lhs, c_rhs)) { expr H = mk_eq_refl(ctx, c_lhs); expr lhs_then = ite_args[3]; expr A = ite_args[2]; @@ -406,13 +423,6 @@ static expr prove_eqn_lemma_core(type_context & ctx, buffer const & Hs, ex expr H2 = prove_eqn_lemma_core(ctx, Hs, lhs_then, rhs); expr eq_trans = mk_constant(get_eq_trans_name(), {A_lvl}); return mk_app(eq_trans, {A, lhs, lhs_then, rhs, H1, H2}); - } else if (auto H = find_if_neg_hypothesis(ctx, c, Hs)) { - expr lhs_else = ite_args[4]; - expr A = ite_args[2]; - level A_lvl = get_level(ctx, A); - expr H1 = mk_app(mk_constant(get_if_neg_name(), {A_lvl}), {c, ite_args[1], *H, A, ite_args[3], lhs_else}); - expr H2 = prove_eqn_lemma_core(ctx, Hs, lhs_else, rhs); - return mk_app(mk_constant(get_eq_trans_name(), {A_lvl}), {A, lhs, lhs_else, rhs, H1, H2}); } } @@ -439,6 +449,7 @@ static expr prove_eqn_lemma(type_context & ctx, buffer const & Hs, expr co environment mk_equation_lemma(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx, name const & f_name, unsigned eqn_idx, bool is_private, buffer const & Hs, expr const & lhs, expr const & rhs) { + if (!get_eqn_compiler_lemmas(opts)) return env; type_context ctx(env, opts, mctx, lctx, transparency_mode::Semireducible); expr type = ctx.mk_pi(Hs, mk_eq(ctx, lhs, rhs)); expr proof = prove_eqn_lemma(ctx, Hs, lhs, rhs); @@ -447,14 +458,18 @@ environment mk_equation_lemma(environment const & env, options const & opts, met } void initialize_eqn_compiler_util() { - g_eqn_compiler_dsimp = new name{"eqn_compiler", "dsimp"}; + g_eqn_compiler_dsimp = new name{"eqn_compiler", "dsimp"}; + g_eqn_compiler_lemmas = new name{"eqn_compiler", "lemmas"}; register_bool_option(*g_eqn_compiler_dsimp, LEAN_DEFAULT_EQN_COMPILER_DSIMP, "(equation compiler) use defeq simplifier to cleanup types of " "automatically synthesized equational lemmas"); + register_bool_option(*g_eqn_compiler_lemmas, LEAN_DEFAULT_EQN_COMPILER_LEMMAS, + "(equation compiler) generate equation lemmas and induction principle"); g_eqn_sanitizer_token = register_defeq_simp_attribute("eqn_sanitizer"); } void finalize_eqn_compiler_util() { delete g_eqn_compiler_dsimp; + delete g_eqn_compiler_lemmas; } } diff --git a/src/library/equations_compiler/util.h b/src/library/equations_compiler/util.h index 0808690145..4b272edb73 100644 --- a/src/library/equations_compiler/util.h +++ b/src/library/equations_compiler/util.h @@ -76,7 +76,7 @@ expr erase_inaccessible_annotations(expr const & e); list erase_inaccessible_annotations(list const & es); pair mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx, - bool is_private, bool is_lemma, name const & c, expr const & type, expr const & value); + bool is_private, bool is_lemma, bool is_noncomputable, name const & n, expr const & type, expr const & value); environment mk_equation_lemma(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx, name const & f_name, unsigned eqn_idx, bool is_private,