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

feat(library/compiler): treat f._meta_rec applications as f applications

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-17 09:48:14 -07:00
parent b1e80f8f4d
commit 3ebf1db2dc
3 changed files with 37 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/library/compiler/preprocess.cpp
View file

@ -221,6 +221,16 @@ class preprocess_fn {
}
}
expr remove_meta_rec(expr const & e) {
return replace(e, [&](expr const & c, unsigned) {
if (is_constant(c)) {
if (optional<name> new_c = is_meta_rec_name(const_name(c)))
return some_expr(mk_constant(*new_c, const_levels(c)));
}
return none_expr();
});
}
void exec_new_compiler(constant_info const & d) {
name n = d.get_name();
expr v = d.get_value();
@ -247,16 +257,23 @@ class preprocess_fn {
m_env = module::add(m_env, simp_decl);
}
name get_real_name(name const & n) {
if (optional<name> new_n = is_meta_rec_name(n))
return *new_n;
else
return n;
}
public:
preprocess_fn(environment const & env, constant_info const & d):
m_env(env) {
m_decl_names.insert(d.get_name());
m_decl_names.insert(get_real_name(d.get_name()));
}
preprocess_fn(environment const & env, buffer<constant_info> const & ds):
m_env(env) {
for (constant_info const & d : ds)
m_decl_names.insert(d.get_name());
m_decl_names.insert(get_real_name(d.get_name()));
}
environment const & env() const { return m_env; }
@ -267,6 +284,7 @@ public:
return m_env;
exec_new_compiler(d);
expr v = d.get_value();
v = remove_meta_rec(v);
lean_trace(name({"compiler", "input"}), tout() << "\n" << v << "\n";);
v = inline_simple_definitions(m_env, m_cache, v);
lean_cond_assert("compiler", check(d, v));
@ -281,8 +299,9 @@ public:
v = eta_expand(m_env, m_cache, v);
lean_cond_assert("compiler", check(d, v));
lean_trace(name({"compiler", "eta_expansion"}), tout() << "\n" << v << "\n";);
v = elim_recursors(m_env, m_cache, d.get_name(), v, procs);
procs.emplace_back(d.get_name(), optional<pos_info>(), v);
name n = get_real_name(d.get_name());
v = elim_recursors(m_env, m_cache, n, v, procs);
procs.emplace_back(n, optional<pos_info>(), v);
lean_cond_assert("compiler", check(d, procs.back().m_code));
lean_trace(name({"compiler", "elim_recursors"}), tout() << "\n"; display(procs););
erase_irrelevant(procs);
@ -291,13 +310,13 @@ public:
lean_trace(name({"compiler", "reduce_arity"}), tout() << "\n"; display(procs););
erase_trivial_structures(m_env, m_cache, procs);
lean_trace(name({"compiler", "erase_trivial_structures"}), tout() << "\n"; display(procs););
lambda_lifting(m_env, m_cache, d.get_name(), procs);
lambda_lifting(m_env, m_cache, n, procs);
lean_trace(name({"compiler", "lambda_lifting"}), tout() << "\n"; display(procs););
simp_inductive(m_env, m_cache, procs);
lean_trace(name({"compiler", "simplify_inductive"}), tout() << "\n"; display(procs););
elim_unused_lets(m_env, m_cache, procs);
lean_trace(name({"compiler", "elim_unused_lets"}), tout() << "\n"; display(procs););
extract_values(m_env, m_cache, d.get_name(), procs);
extract_values(m_env, m_cache, n, procs);
lean_trace(name({"compiler", "extract_values"}), tout() << "\n"; display(procs););
old_cse(m_env, m_cache, procs);
lean_trace(name({"compiler", "cse"}), tout() << "\n"; display(procs););

26
src/library/compiler/vm_compiler.cpp
View file

@ -365,34 +365,16 @@ static environment vm_compile(environment const & env, buffer<procedure> const &
}
environment vm_compile(environment const & env, buffer<constant_info> const & ds, bool optimize_bytecode) {
for (constant_info const & info : ds) {
if (!info.is_definition() || is_noncomputable(env, info.get_name()) || is_vm_builtin_function(info.get_name()))
return env;
}
buffer<procedure> procs;
environment new_env = preprocess(env, ds, procs);
return vm_compile(new_env, procs, optimize_bytecode);
}
static optional<environment> try_reuse_aux_meta_code(environment const & env, name const & d_name) {
name aux_name = mk_meta_rec_name(d_name);
optional<vm_decl> v_decl = get_vm_decl(env, aux_name);
if (!v_decl || !v_decl->is_bytecode())
return optional<environment>();
/* If we already compiled d_name._meta_rec (which is a meta definition),
we reuse the generated code.
The goal is to have a predictable runtime cost model for Lean and avoid
the overhead generated by the equation compiler when using well founded recursion
and structural recursion.
*/
return optional<environment>(add_vm_code(env, d_name, v_decl->get_arity(),
v_decl->get_code_size(), v_decl->get_code(),
v_decl->get_args_info(), v_decl->get_pos_info()));
}
environment vm_compile(environment const & env, constant_info const & info, bool optimize_bytecode) {
if (!info.is_definition() || is_noncomputable(env, info.get_name()) || is_vm_builtin_function(info.get_name()))
return env;
if (auto new_env = try_reuse_aux_meta_code(env, info.get_name()))
return *new_env;
buffer<constant_info> infos;
infos.push_back(info);
return vm_compile(env, infos, optimize_bytecode);

10
src/library/equations_compiler/compiler.cpp
View file

@ -377,7 +377,11 @@ expr compile_equations(environment & env, elaborator & elab, metavar_context & m
!header.m_is_noncomputable &&
/* Remark: we don't need special compilation scheme for non recursive equations */
is_recursive_eqns(ctx, eqns)) {
/* We compile non-meta recursive definitions as meta definitions first.
/* Compile equations but do not generate code since we will use `brec_on` or `well_founded.fix`. */
equations_header new_header = header;
new_header.m_gen_code = false;
expr result = compile_equations_main(env, elab, mctx, lctx, update_equations(eqns, new_header), true);
/* Then, we compile the equations again using `meta` and generate code.
The motivations are:
- Clear execution cost semantics for recursive functions.
- Auxiliary meta definition may assist recursive definition unfolding in the type_context_old object.
@ -389,8 +393,10 @@ expr compile_equations(environment & env, elaborator & elab, metavar_context & m
expr aux_eqns = remove_wf_annotation_from_equations(update_equations(eqns, aux_header));
aux_eqns = unfold_auxiliary_fns(env, header.m_fn_actual_names, aux_eqns);
compile_equations_main(env, elab, mctx, lctx, aux_eqns, false);
return result;
} else {
return compile_equations_main(env, elab, mctx, lctx, eqns, true);
}
return compile_equations_main(env, elab, mctx, lctx, eqns, true);
}
void initialize_compiler() {