From 2fc0e5fa05030bf7cf0f927d46fa6f712212a2bf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 30 Aug 2016 18:33:24 -0700 Subject: [PATCH] feat(library/equations_compiler/structural_rec): add aux definition --- src/frontends/lean/definition_cmds.cpp | 2 ++ src/library/aux_definition.cpp | 16 +++++---- src/library/aux_definition.h | 8 +++-- .../equations_compiler/structural_rec.cpp | 35 +++++++++++++++--- src/library/equations_compiler/util.cpp | 36 +++++++++++++++++++ src/library/equations_compiler/util.h | 5 ++- 6 files changed, 88 insertions(+), 14 deletions(-) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index ec25604193..9f941f7f32 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -105,6 +105,7 @@ expr parse_mutual_definition(parser & p, def_cmd_kind k, buffer & lp_names // TODO(leo, dhs): make use of attributes expr fn_type = parse_inner_header(p, local_pp_name(pre_fn)).first; declaration_name_scope scope2(local_pp_name(pre_fn)); + declaration_name_scope scope3("_main"); full_names.push_back(scope2.get_name()); if (p.curr_is_token(get_none_tk())) { auto none_pos = p.pos(); @@ -158,6 +159,7 @@ static expr_pair parse_definition(parser & p, buffer & lp_names, buffer eqns; diff --git a/src/library/aux_definition.cpp b/src/library/aux_definition.cpp index f834ae9b61..110f847476 100644 --- a/src/library/aux_definition.cpp +++ b/src/library/aux_definition.cpp @@ -120,7 +120,7 @@ struct mk_aux_definition_fn { } } - pair operator()(name const & c, expr const & type, expr const & value) { + pair operator()(name const & c, expr const & type, expr const & value, optional const & is_meta) { expr new_type = collect(m_ctx.instantiate_mvars(type)); expr new_value = collect(m_ctx.instantiate_mvars(value)); buffer norm_params; @@ -131,7 +131,11 @@ struct mk_aux_definition_fn { expr def_value = m_ctx.mk_lambda(norm_params, new_value); bool use_conv_opt = true; environment const & env = m_ctx.env(); - declaration d = mk_definition_inferring_trusted(env, c, to_list(m_level_params), def_type, def_value, use_conv_opt); + declaration d; + if (is_meta) + d = mk_definition(env, c, to_list(m_level_params), def_type, def_value, use_conv_opt, !*is_meta); + else + d = mk_definition_inferring_trusted(env, c, to_list(m_level_params), def_type, def_value, use_conv_opt); environment new_env = module::add(env, check(env, d)); buffer ls; for (name const & n : m_level_params) { @@ -153,15 +157,15 @@ struct mk_aux_definition_fn { }; pair mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx, - name const & c, expr const & type, expr const & value) { + name const & c, expr const & type, expr const & value, optional const & is_meta) { type_context ctx(env, options(), mctx, lctx, transparency_mode::All); - return mk_aux_definition_fn(ctx)(c, type, value); + return mk_aux_definition_fn(ctx)(c, type, value, is_meta); } pair mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx, - name const & c, expr const & value) { + name const & c, expr const & value, optional const & is_meta) { type_context ctx(env, options(), mctx, lctx, transparency_mode::All); expr type = ctx.infer(value); - return mk_aux_definition_fn(ctx)(c, type, value); + return mk_aux_definition_fn(ctx)(c, type, value, is_meta); } } diff --git a/src/library/aux_definition.h b/src/library/aux_definition.h index 6884db9688..1641fbb852 100644 --- a/src/library/aux_definition.h +++ b/src/library/aux_definition.h @@ -15,12 +15,14 @@ namespace lean { where l_i's and a_j's are the collected dependencies. - The function also computes whether the new definition should be tagged as trusted or not. + If is_meta is none, then function also computes whether the new definition should be tagged as trusted or not. The updated environment is an extension of ctx.env() */ pair mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx, - name const & c, expr const & type, expr const & value); + name const & c, expr const & type, expr const & value, + optional const & is_meta = optional()); /** \brief Similar to mk_aux_definition, but the type of value is inferred using ctx. */ pair mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx, - name const & c, expr const & value); + name const & c, expr const & value, + optional const & is_meta = optional()); } diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp index 5d852c82af..7b357f36aa 100644 --- a/src/library/equations_compiler/structural_rec.cpp +++ b/src/library/equations_compiler/structural_rec.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/app_builder.h" #include "library/replace_visitor_with_tc.h" +#include "library/equations_compiler/equations.h" #include "library/equations_compiler/util.h" #include "library/equations_compiler/structural_rec.h" #include "library/equations_compiler/elim_match.h" @@ -27,6 +28,8 @@ struct structural_rec_fn { metavar_context m_mctx; local_context m_lctx; + equations_header m_header; + expr m_fn_type; unsigned m_arity; unsigned m_arg_pos; buffer m_indices_pos; @@ -457,7 +460,8 @@ struct structural_rec_fn { tout() << "\n";); return none_expr(); } - m_arity = ues.get_arity_of(0); + m_fn_type = ctx.infer(ues.get_fn(0)); + m_arity = ues.get_arity_of(0); if (!find_rec_arg(ctx, ues)) return none_expr(); expr fn = ues.get_fn(0); trace_struct(tout() << "using structural recursion on argument #" << (m_arg_pos+1) << @@ -493,7 +497,7 @@ struct structural_rec_fn { return std::find(m_indices_pos.begin(), m_indices_pos.end(), idx) != m_indices_pos.end(); } - expr mk_brec_on(expr const & aux_fn, list const & aux_lemmas) { + expr mk_function(expr const & aux_fn) { type_context ctx = mk_type_context(); type_context::tmp_locals locals(ctx); buffer fn_args; @@ -541,14 +545,37 @@ struct structural_rec_fn { brec_on_args.push_back(F); expr new_fn = ctx.mk_lambda(fn_args, mk_app(mk_app(brec_on_fn, brec_on_args), extra_args)); lean_trace("eqn_compiler", tout() << "result:\n" << new_fn << "\ntype:\n" << ctx.infer(new_fn) << "\n";); - return new_fn; + if (m_header.m_is_meta) { + /* We don't create auxiliary definitions for meta-definitions because we don't create lemmas + for them. */ + return new_fn; + } else { + expr r; + std::tie(m_env, r) = mk_aux_definition(m_env, m_mctx, m_lctx, m_header.m_is_private, head(m_header.m_fn_names), + m_fn_type, new_fn); + return r; + } + } + + void mk_lemmas(expr const & fn, expr const & aux_fn, list const & lemmas) { + for (expr_pair const & p : lemmas) { + expr type, proof; + std::tie(type, proof) = p; + // TODO(Leo) + } } optional operator()(expr const & eqns) { + m_header = get_equations_header(eqns); auto new_eqns = elim_recursion(eqns); if (!new_eqns) return none_expr(); elim_match_result R = elim_match(m_env, m_opts, m_mctx, m_lctx, *new_eqns); - return some_expr(mk_brec_on(R.m_fn, R.m_lemmas)); + expr fn = mk_function(R.m_fn); + if (m_header.m_lemmas) { + lean_assert(!m_header.m_is_meta); + mk_lemmas(fn, R.m_fn, R.m_lemmas); + } + return some_expr(fn); } }; diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 6a853af457..11c3ff4e91 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -9,6 +9,9 @@ Author: Leonardo de Moura #include "kernel/find_fn.h" #include "kernel/inductive/inductive.h" #include "library/util.h" +#include "library/private.h" +#include "library/aux_definition.h" +#include "library/scope_pos_info_provider.h" #include "library/equations_compiler/equations.h" #include "library/equations_compiler/util.h" @@ -172,4 +175,37 @@ bool is_recursive_eqns(type_context & ctx, expr const & e) { } return false; } + +static pair mk_def_name(environment const & env, bool is_private, name const & c) { + if (is_private) { + unsigned h = 31; + if (auto pinfo = get_pos_info_provider()) { + h = hash(pinfo->get_some_pos().first, pinfo->get_some_pos().second); + char const * fname = pinfo->get_file_name(); + h = hash_str(strlen(fname), fname, h); + } + return add_private_name(env, c, optional(h)); + } else { + return mk_pair(env, c); + } +} + +pair mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx, + bool is_private, 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); + return mk_aux_definition(new_env, mctx, lctx, new_c, type, value); +} + +pair mk_equation_lemma(environment const & env, metavar_context const & mctx, local_context const & lctx, + bool is_private, 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); + expr r; + std::tie(new_env, r) = mk_aux_definition(new_env, mctx, lctx, new_c, type, value); + // TODO(Leo): add simp (and dsimp) rule + return mk_pair(new_env, r); +} } diff --git a/src/library/equations_compiler/util.h b/src/library/equations_compiler/util.h index 5d533a0e83..37f8d0f6fe 100644 --- a/src/library/equations_compiler/util.h +++ b/src/library/equations_compiler/util.h @@ -72,6 +72,9 @@ public: equations. */ bool is_recursive_eqns(type_context & ctx, expr const & e); +pair mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx, + bool is_private, name const & c, expr const & type, expr const & value); - +pair mk_equation_lemma(environment const & env, metavar_context const & mctx, local_context const & lctx, + bool is_private, name const & c, expr const & type, expr const & value); }