diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp index 51da8061ac..37dc834eef 100644 --- a/src/library/compiler/preprocess.cpp +++ b/src/library/compiler/preprocess.cpp @@ -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 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 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 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(), v); + name n = get_real_name(d.get_name()); + v = elim_recursors(m_env, m_cache, n, v, procs); + procs.emplace_back(n, optional(), 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);); diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp index a5f1577a64..804d4105fc 100644 --- a/src/library/compiler/vm_compiler.cpp +++ b/src/library/compiler/vm_compiler.cpp @@ -365,34 +365,16 @@ static environment vm_compile(environment const & env, buffer const & } environment vm_compile(environment const & env, buffer 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 procs; environment new_env = preprocess(env, ds, procs); return vm_compile(new_env, procs, optimize_bytecode); } -static optional try_reuse_aux_meta_code(environment const & env, name const & d_name) { - name aux_name = mk_meta_rec_name(d_name); - optional v_decl = get_vm_decl(env, aux_name); - if (!v_decl || !v_decl->is_bytecode()) - return optional(); - /* 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(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 infos; infos.push_back(info); return vm_compile(env, infos, optimize_bytecode); diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp index 5c218d55f6..62e25e9e2a 100644 --- a/src/library/equations_compiler/compiler.cpp +++ b/src/library/equations_compiler/compiler.cpp @@ -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() {