From 22988bb95d2de5daafb7ce522ddf63e43ff95423 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 4 Mar 2017 13:54:44 -0800 Subject: [PATCH] feat(library/compiler): avoid pack/unpack overhead produced by the inductive_compiler in the code generator TODO: make sure the user is not manually using cases_on for the auxiliary datatype generated by the inductive_compiler to destruct nested inductives. --- src/library/compiler/erase_irrelevant.cpp | 24 ++++++++- src/library/compiler/eta_expansion.cpp | 7 ++- src/library/compiler/inliner.cpp | 2 +- src/library/compiler/preprocess.cpp | 65 ++++++++++++++--------- src/library/compiler/simp_inductive.cpp | 18 ++++++- src/library/compiler/util.cpp | 9 ++++ src/library/compiler/util.h | 4 ++ 7 files changed, 97 insertions(+), 32 deletions(-) diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp index f2582a8e2b..c584a40293 100644 --- a/src/library/compiler/erase_irrelevant.cpp +++ b/src/library/compiler/erase_irrelevant.cpp @@ -10,7 +10,9 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/constants.h" #include "library/normalize.h" +#include "library/inverse.h" #include "library/aux_recursors.h" +#include "library/inductive_compiler/ginductive.h" #include "library/compiler/util.h" #include "library/compiler/nat_value.h" #include "library/compiler/comp_irrelevant.h" @@ -157,6 +159,9 @@ class erase_irrelevant_fn : public compiler_step_visitor { unsigned nindices = *inductive::get_num_indices(env(), I_name); unsigned arity = nparams + 1 /* typeformer/motive */ + nindices + 1 /* major premise */ + nminors; lean_assert(args.size() >= arity); + /* TODO(Leo, Daniel): we need a way to check whether the user is trying to cases_on + on an auxiliary datatype + */ buffer cnames; get_intro_rule_names(env(), I_name, cnames); expr * minors = args.data() + nparams + 1 + nindices + 1; @@ -348,6 +353,19 @@ class erase_irrelevant_fn : public compiler_step_visitor { } } + expr visit_pack_unpack(expr const & fn, buffer const & args) { + optional info = has_inverse(env(), const_name(fn)); + if (!info || info->m_arity > args.size()) { + /* This line should only be reached if there is bug in the inductive compiler */ + throw exception(sstream() << "code generation failed, information for auxiliary definition '" << const_name(fn) << + "' generated by inductive compiler is missing or is incorrect"); + } + /* The inductive compiler pack/unpack functions are the identity function from + the point of view of the code generator. */ + expr r = args[info->m_arity - 1]; + return visit(mk_app(r, args.size() - info->m_arity, args.data() + info->m_arity)); + } + virtual expr visit_app(expr const & e) override { if (is_comp_irrelevant(e)) return *g_neutral_expr; @@ -359,7 +377,9 @@ class erase_irrelevant_fn : public compiler_step_visitor { return visit(beta_reduce(e)); } else if (is_constant(fn)) { name const & n = const_name(fn); - if (n == get_eq_rec_name()) { + if (is_ginductive_intro_rule(env(), n) && ir_to_simulated_ir_offset(env(), n) > 0) { + throw exception(sstream() << "code generation failed, auxiliary internal constructor '" << n << "' is being used"); + } else if (n == get_eq_rec_name()) { return visit_eq_rec(args); } else if (n == get_acc_cases_on_name()) { return visit_acc_cases_on(args); @@ -383,6 +403,8 @@ class erase_irrelevant_fn : public compiler_step_visitor { return visit_subtype_tag(args); } else if (n == get_subtype_elt_of_name()) { return visit_subtype_elt_of(args); + } else if (is_ginductive_pack(env(), n) || is_ginductive_unpack(env(), n)) { + return visit_pack_unpack(fn, args); } } return compiler_step_visitor::visit_app(e); diff --git a/src/library/compiler/eta_expansion.cpp b/src/library/compiler/eta_expansion.cpp index 5fcc1d77b9..a8f6291985 100644 --- a/src/library/compiler/eta_expansion.cpp +++ b/src/library/compiler/eta_expansion.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/constants.h" #include "library/projection.h" #include "library/aux_recursors.h" +#include "library/inductive_compiler/ginductive.h" #include "library/compiler/util.h" #include "library/compiler/compiler_step_visitor.h" #include "library/compiler/comp_irrelevant.h" @@ -20,13 +21,14 @@ Author: Leonardo de Moura namespace lean { class eta_expand_fn : public compiler_step_visitor { bool is_projection(name const & n) { return ::lean::is_projection(env(), n); } - bool is_constructor(name const & n) { return static_cast(inductive::is_intro_rule(env(), n)); } + bool is_constructor(name const & n) { return static_cast(is_ginductive_intro_rule(env(), n)); } bool is_cases_on(name const & n) { return is_cases_on_recursor(env(), n); } bool is_rec(name const & n) { return static_cast(inductive::is_elim_rule(env(), n)); } bool is_no_confusion(name const & n) { return ::lean::is_no_confusion(env(), n); } bool is_quot_mk(name const & n) { return n == get_quot_mk_name(); } bool is_quot_lift(name const & n) { return n == get_quot_lift_name(); } bool is_subtype_elt_of(name const & n) { return n == get_subtype_elt_of_name(); } + bool is_pack_unpack(name const & n) { return is_ginductive_pack(env(), n) || is_ginductive_unpack(env(), n); } /* Return true if the type of e is of the form Pi (a_1 : A_1) ... (a_n : B_n), C @@ -113,7 +115,8 @@ class eta_expand_fn : public compiler_step_visitor { is_rec(fn_name) || is_cases_on(fn_name) || is_no_confusion(fn_name) || is_quot_mk(fn_name) || is_quot_lift(fn_name) || - is_subtype_elt_of(fn_name)) { + is_subtype_elt_of(fn_name) || + is_pack_unpack(fn_name)) { if (revisit) return visit(eta_expand(r)); else diff --git a/src/library/compiler/inliner.cpp b/src/library/compiler/inliner.cpp index 4bb4a5aa12..752f6bac00 100644 --- a/src/library/compiler/inliner.cpp +++ b/src/library/compiler/inliner.cpp @@ -115,7 +115,7 @@ class inline_simple_definitions_fn : public compiler_step_visitor { if (!is_constant(fn)) return default_visit_app(e); name const & n = const_name(fn); - if (is_vm_builtin_function(n)) + if (is_vm_builtin_function(n) || is_pack_unpack(env(), e)) return default_visit_app(e); if (is_cases_on_recursor(env(), n) || is_nonrecursive_recursor(n)) return visit_cases_on_app(e); diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp index c2d74f6f51..911e594f65 100644 --- a/src/library/compiler/preprocess.cpp +++ b/src/library/compiler/preprocess.cpp @@ -83,46 +83,54 @@ class expand_aux_fn : public compiler_step_visitor { } } - virtual expr visit_constant(expr const & e) override { - type_context::nozeta_scope scope(ctx()); - name const & n = const_name(e); - declaration d = env().get(n); - if (!d.is_definition() || d.is_theorem()) - return e; - if (::lean::is_aux_recursor(env(), n) || is_user_defined_recursor(env(), n) || - is_projection(env(), n) || is_no_confusion(env(), n)) - return e; - if (!is_vm_function(env(), n)) { - check_computable(e); - if (auto r = unfold_term(env(), e)) { - return visit(*r); - } - } - return e; - } - bool is_not_vm_function(expr const & e) { expr const & fn = get_app_fn(e); if (!is_constant(fn)) return false; name const & n = const_name(fn); declaration d = env().get(n); - if (!d.is_definition() || d.is_theorem() || is_projection(env(), n) || is_no_confusion(env(), n)) + if (!d.is_definition() || d.is_theorem() || is_projection(env(), n) || is_no_confusion(env(), n) || + ::lean::is_aux_recursor(env(), n) || is_user_defined_recursor(env(), n)) return false; return !is_vm_function(env(), n); } + bool is_pack_unpack(expr const & e) { + return ::lean::is_pack_unpack(m_env, e); + } + + bool should_unfold(expr const & e) { + return is_not_vm_function(e) && !ctx().is_proof(e) && !is_pack_unpack(e); + } + + expr unfold(expr const & e) { + check_computable(e); + if (auto r = unfold_term(env(), e)) { + return visit(*r); + } else { + throw exception(sstream() << "failed to generate bytecode, VM does not have code for '" << get_app_fn(e) << "'"); + } + } + + virtual expr visit_constant(expr const & e) override { + type_context::nozeta_scope scope(ctx()); + if (should_unfold(e)) + return visit(unfold(e)); + else + return e; + } + virtual expr visit_app(expr const & e) override { type_context::nozeta_scope scope(ctx()); switch (get_recursor_app_kind(e)) { case recursor_kind::NotRecursor: { - if (is_not_vm_function(e) && !ctx().is_proof(e)) { - check_computable(e); - if (auto r = unfold_term(env(), e)) { - return visit(copy_tag(e, expr(*r))); - } + if (should_unfold(e)) + return visit(unfold(e)); + expr new_e; + { + type_context::transparency_scope scope(ctx(), transparency_mode::Reducible); + new_e = copy_tag(e, ctx().whnf_head_pred(e, [&](expr const & e) { return is_macro(e); })); } - expr new_e = copy_tag(e, ctx().whnf_head_pred(e, [&](expr const & e) { return is_macro(e); })); if (is_eqp(new_e, e)) return compiler_step_visitor::visit_app(new_e); else @@ -131,7 +139,12 @@ class expand_aux_fn : public compiler_step_visitor { case recursor_kind::CasesOn: return visit_cases_on(e); case recursor_kind::Aux: - return compiler_step_visitor::visit(copy_tag(e, ctx().whnf_head_pred(e, [&](expr const & e) { return is_aux_recursor(e) || is_macro(e); }))); + expr new_e; + { + type_context::transparency_scope scope(ctx(), transparency_mode::Reducible); + new_e = copy_tag(e, ctx().whnf_head_pred(e, [&](expr const & e) { return is_aux_recursor(e) || is_macro(e); })); + } + return compiler_step_visitor::visit(new_e); } lean_unreachable(); } diff --git a/src/library/compiler/simp_inductive.cpp b/src/library/compiler/simp_inductive.cpp index 077ef7d783..98ec091ac1 100644 --- a/src/library/compiler/simp_inductive.cpp +++ b/src/library/compiler/simp_inductive.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/normalize.h" #include "library/constants.h" #include "library/vm/vm.h" +#include "library/inductive_compiler/ginductive.h" #include "library/compiler/util.h" #include "library/compiler/erase_irrelevant.h" #include "library/compiler/compiler_step_visitor.h" @@ -163,6 +164,7 @@ class simp_inductive_fn : public compiler_step_visitor { args[0] = visit(args[0]); unsigned num_reachable = 0; optional reachable_case; + unsigned last_reachable_idx = 0; /* Process minor premises */ for (unsigned i = 0; i < cnames.size(); i++) { buffer rel_fields; @@ -176,7 +178,8 @@ class simp_inductive_fn : public compiler_step_visitor { args[i+1] = new_minor; if (!p.second) { num_reachable++; - reachable_case = p.first; + last_reachable_idx = i+1; + reachable_case = p.first; } } @@ -188,7 +191,15 @@ class simp_inductive_fn : public compiler_step_visitor { } else if (is_builtin) { return mk_app(mk_constant(fn), args); } else { - return mk_app(mk_cases(cnames.size()), args); + if (last_reachable_idx != cnames.size()) { + /* Compress number of cases by removing the tail of unreachable cases */ + buffer new_args; + new_args.append(last_reachable_idx+1, args.data()); + new_args.append(args.size() - cnames.size() - 1, args.data() + cnames.size() + 1); + return mk_app(mk_cases(last_reachable_idx), new_args); + } else { + return mk_app(mk_cases(cnames.size()), args); + } } } @@ -199,6 +210,9 @@ class simp_inductive_fn : public compiler_step_visitor { new_args.push_back(visit(arg)); return mk_app(mk_constant(fn), new_args); } else { + /* The following invariant should hold since erase_irrelevant rejected code + where it doesn't hold. */ + lean_assert(ir_to_simulated_ir_offset(env(), fn) == 0); name I_name = *inductive::is_intro_rule(env(), fn); unsigned nparams = *inductive::get_num_params(env(), I_name); unsigned cidx = get_constructor_idx(env(), fn); diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp index 48ae589791..251bab8815 100644 --- a/src/library/compiler/util.cpp +++ b/src/library/compiler/util.cpp @@ -8,12 +8,21 @@ Author: Leonardo de Moura #include "kernel/find_fn.h" #include "kernel/type_checker.h" #include "kernel/inductive/inductive.h" +#include "library/inverse.h" #include "library/aux_recursors.h" #include "library/util.h" +#include "library/inductive_compiler/ginductive.h" #include "library/vm/vm.h" #include "library/type_context.h" namespace lean { +bool is_pack_unpack(environment const & env, expr const & e) { + expr const & fn = get_app_fn(e); + if (!is_constant(fn)) return false; + name const & n = const_name(fn); + return is_ginductive_pack(env, n) || is_ginductive_unpack(env, n); +} + name mk_fresh_name(environment const & env, name const & prefix, char const * suffix, unsigned & idx) { while (true) { name curr(prefix, suffix); diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h index 3fd363546d..215fba3a2e 100644 --- a/src/library/compiler/util.h +++ b/src/library/compiler/util.h @@ -31,4 +31,8 @@ bool is_recursive_rec_app(environment const & env, expr const & e); /** \brief Return true iff \c n is an auxiliary cases_on recursor */ bool is_cases_on_recursor(environment const & env, name const & n); + +/** \brief Return true iff \c e is pack/unpack-application where pack/unpack + are auxiliary functions generated by the inductive compiler */ +bool is_pack_unpack(environment const & env, expr const & e); }