max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/equations_compiler/structural_rec): add aux definition

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-30 18:33:24 -07:00
parent 253fcdcc51
commit 2fc0e5fa05
6 changed files with 88 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/definition_cmds.cpp
View file

@ -105,6 +105,7 @@ expr parse_mutual_definition(parser & p, def_cmd_kind k, buffer<name> & 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<name> & lp_names, buffer<ex
p.next();
val = p.parse_expr();
} else if (p.curr_is_token(get_bar_tk()) || p.curr_is_token(get_none_tk())) {
declaration_name_scope scope2("_main");
fn = mk_local(mlocal_name(fn), local_pp_name(fn), mlocal_type(fn), mk_rec_info(true));
p.add_local(fn);
buffer<expr> eqns;

16
src/library/aux_definition.cpp
View file

@ -120,7 +120,7 @@ struct mk_aux_definition_fn {
}
}
pair<environment, expr> operator()(name const & c, expr const & type, expr const & value) {
pair<environment, expr> operator()(name const & c, expr const & type, expr const & value, optional<bool> const & is_meta) {
expr new_type = collect(m_ctx.instantiate_mvars(type));
expr new_value = collect(m_ctx.instantiate_mvars(value));
buffer<expr> 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<level> ls;
for (name const & n : m_level_params) {
@ -153,15 +157,15 @@ struct mk_aux_definition_fn {
};
pair<environment, expr> 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<bool> 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<environment, expr> 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<bool> 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);
}
}

8
src/library/aux_definition.h
View file

@ -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<environment, expr> 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<bool> const & is_meta = optional<bool>());
/** \brief Similar to mk_aux_definition, but the type of value is inferred using ctx. */
pair<environment, expr> 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<bool> const & is_meta = optional<bool>());
}

35
src/library/equations_compiler/structural_rec.cpp
View file

@ -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<unsigned> 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<expr_pair> const & aux_lemmas) {
expr mk_function(expr const & aux_fn) {
type_context ctx = mk_type_context();
type_context::tmp_locals locals(ctx);
buffer<expr> 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<expr_pair> const & lemmas) {
for (expr_pair const & p : lemmas) {
expr type, proof;
std::tie(type, proof) = p;
// TODO(Leo)
}
}
optional<expr> 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);
}
};

36
src/library/equations_compiler/util.cpp
View file

@ -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<environment, name> 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<unsigned>(h));
} else {
return mk_pair(env, c);
}
}
pair<environment, expr> 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<environment, expr> 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);
}
}

5
src/library/equations_compiler/util.h
View file

@ -72,6 +72,9 @@ public:
equations. */
bool is_recursive_eqns(type_context & ctx, expr const & e);
pair<environment, expr> 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<environment, expr> 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);
}