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

feat(compiler/inliner): simplify cases_on and nonrecursive recursor applications when possible

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-09 13:24:20 -07:00
parent bc81d0957f
commit 79bf13e3ed
1 changed files with 49 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
src/compiler/inliner.cpp
View file

@ -4,9 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/inductive/inductive.h"
#include "library/util.h"
#include "library/module.h"
#include "library/trace.h"
#include "library/normalize.h"
#include "compiler/util.h"
#include "compiler/compiler_step_visitor.h"
namespace lean {
@ -94,12 +97,57 @@ class inline_simple_definitions_fn : public compiler_step_visitor {
return compiler_step_visitor::visit_app(e);
}
bool is_nonrecursive_recursor(name const & n) {
if (auto I_name = inductive::is_elim_rule(env(), n)) {
return !is_recursive_datatype(env(), *I_name);
}
return false;
}
/* Try to reduce cases_on (and nonrecursive recursor) application
if major became a constructor */
expr visit_cases_on_app(expr const & e_0) {
expr e = default_visit_app(e_0);
buffer<expr> args;
expr const & fn = get_app_args(e, args);
lean_assert(is_constant(fn));
bool is_cases_on = is_cases_on_recursor(env(), const_name(fn));
name const & rec_name = const_name(fn);
name const & I_name = rec_name.get_prefix();
unsigned nparams = *inductive::get_num_params(env(), I_name);
unsigned nindices = *inductive::get_num_indices(env(), I_name);
unsigned major_idx;
if (is_cases_on) {
major_idx = nparams + 1 + nindices;
} else {
major_idx = *inductive::get_elim_major_idx(env(), rec_name);
}
expr major = beta_reduce(args[major_idx]);
if (is_constructor_app(env(), major)) {
/* Major premise became a constructor. So, we should reduce. */
expr new_e = e;
if (is_cases_on) {
/* unfold cases_on */
if (auto r = unfold_term(env(), new_e))
new_e = *r;
else
return e;
}
/* reduce */
if (auto r = ctx().norm_ext(new_e))
return compiler_step_visitor::visit(beta_reduce(*r));
}
return e;
}
virtual expr visit_app(expr const & e) override {
expr const & fn = get_app_fn(e);
if (!is_constant(fn))
return default_visit_app(e);
unsigned nargs = get_app_num_args(e);
name const & n = const_name(fn);
if (is_cases_on_recursor(env(), n) || is_nonrecursive_recursor(n))
return visit_cases_on_app(e);
unsigned nargs = get_app_num_args(e);
declaration d = env().get(n);
if (!d.is_definition() || d.is_theorem())
return default_visit_app(e);