diff --git a/src/library/compiler/CMakeLists.txt b/src/library/compiler/CMakeLists.txt index 187bda1ea3..05390a5e32 100644 --- a/src/library/compiler/CMakeLists.txt +++ b/src/library/compiler/CMakeLists.txt @@ -1,4 +1,4 @@ add_library(compiler OBJECT util.cpp eta_expansion.cpp simp_pr1_rec.cpp preprocess_rec.cpp compiler_step_visitor.cpp elim_recursors.cpp comp_irrelevant.cpp inliner.cpp rec_fn_macro.cpp erase_irrelevant.cpp reduce_arity.cpp - lambda_lifting.cpp init_module.cpp) + lambda_lifting.cpp simp_inductive.cpp init_module.cpp) diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp index 603504a1cf..0bef2f48af 100644 --- a/src/library/compiler/erase_irrelevant.cpp +++ b/src/library/compiler/erase_irrelevant.cpp @@ -19,6 +19,11 @@ Author: Leonardo de Moura namespace lean { static expr * g_neutral_expr = nullptr; static expr * g_unreachable_expr = nullptr; + +expr mk_neutral_expr() { + return *g_neutral_expr; +} + class erase_irrelevant_fn : public compiler_step_visitor { virtual expr visit_sort(expr const &) override { diff --git a/src/library/compiler/erase_irrelevant.h b/src/library/compiler/erase_irrelevant.h index c91ab6bfdf..f523ad1ccc 100644 --- a/src/library/compiler/erase_irrelevant.h +++ b/src/library/compiler/erase_irrelevant.h @@ -22,6 +22,8 @@ expr erase_irrelevant(environment const & env, expr const & e); bool is_neutral_expr(expr const & e); bool is_unreachable_expr(expr const & e); +expr mk_neutral_expr(); + void initialize_erase_irrelevant(); void finalize_erase_irrelevant(); } diff --git a/src/library/compiler/init_module.cpp b/src/library/compiler/init_module.cpp index d1c9e26223..ea57ada076 100644 --- a/src/library/compiler/init_module.cpp +++ b/src/library/compiler/init_module.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "library/compiler/inliner.h" #include "library/compiler/rec_fn_macro.h" #include "library/compiler/erase_irrelevant.h" +#include "library/compiler/simp_inductive.h" namespace lean { void initialize_compiler_module() { @@ -17,8 +18,10 @@ void initialize_compiler_module() { initialize_inliner(); initialize_rec_fn_macro(); initialize_erase_irrelevant(); + initialize_simp_inductive(); } void finalize_compiler_module() { + finalize_simp_inductive(); finalize_erase_irrelevant(); finalize_rec_fn_macro(); finalize_inliner(); diff --git a/src/library/compiler/preprocess_rec.cpp b/src/library/compiler/preprocess_rec.cpp index 617f44bfd5..bbdc99e362 100644 --- a/src/library/compiler/preprocess_rec.cpp +++ b/src/library/compiler/preprocess_rec.cpp @@ -21,6 +21,7 @@ Author: Leonardo de Moura #include "library/compiler/erase_irrelevant.h" #include "library/compiler/reduce_arity.h" #include "library/compiler/lambda_lifting.h" +#include "library/compiler/simp_inductive.h" namespace lean { class expand_aux_recursors_fn : public compiler_step_visitor { @@ -147,6 +148,9 @@ public: lean_trace(name({"compiler", "reduce_arity"}), tout() << "\n"; display(procs);); lambda_lifting(m_env, d.get_name(), procs); lean_trace(name({"compiler", "lambda_lifting"}), tout() << "\n"; display(procs);); + simp_inductive(m_env, procs); + lean_trace(name({"compiler", "simplify_inductive"}), tout() << "\n"; display(procs);); + display(procs); // TODO(Leo) } @@ -167,6 +171,7 @@ void initialize_preprocess_rec() { register_trace_class({"compiler", "erase_irrelevant"}); register_trace_class({"compiler", "reduce_arity"}); register_trace_class({"compiler", "lambda_lifting"}); + register_trace_class({"compiler", "simplify_inductive"}); g_tmp_prefix = new name(name::mk_internal_unique_name()); } diff --git a/src/library/compiler/simp_inductive.cpp b/src/library/compiler/simp_inductive.cpp new file mode 100644 index 0000000000..21086cd065 --- /dev/null +++ b/src/library/compiler/simp_inductive.cpp @@ -0,0 +1,185 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/instantiate.h" +#include "kernel/inductive/inductive.h" +#include "library/util.h" +#include "library/projection.h" +#include "library/constants.h" +#include "library/compiler/util.h" +#include "library/compiler/erase_irrelevant.h" +#include "library/compiler/compiler_step_visitor.h" + +namespace lean { +static name * g_cases = nullptr; +static name * g_cnstr = nullptr; +static name * g_proj = nullptr; + +static expr mk_constructor(unsigned cidx) { + return mk_constant(name(*g_cnstr, cidx)); +} + +static expr mk_proj(unsigned idx) { + return mk_constant(name(*g_proj, idx)); +} + +static expr mk_cases(unsigned n) { + return mk_constant(name(*g_cases, n)); +} + +static optional is_internal_symbol(expr const & e, name const & prefix) { + if (!is_constant(e)) + return optional(); + name const & n = const_name(e); + if (n.is_atomic() || !n.is_numeral()) + return optional(); + if (n.get_prefix() == prefix) + return optional(n.get_numeral()); + else + return optional(); +} + +optional is_internal_cnstr(expr const & e) { + return is_internal_symbol(e, *g_cnstr); +} + +optional is_internal_cases(expr const & e) { + return is_internal_symbol(e, *g_cases); +} + +optional is_internal_proj(expr const & e) { + return is_internal_symbol(e, *g_proj); +} + +class simp_inductive_fn : public compiler_step_visitor { + name_map> m_constructor_info; + + static bool ignore(name const & n) { + return n == get_nat_zero_name() || n == get_nat_succ_name() || n == get_nat_cases_on_name(); + } + + void get_constructor_info(name const & n, buffer & rel_fields) { + if (auto r = m_constructor_info.find(n)) { + to_buffer(*r, rel_fields); + } else { + get_constructor_relevant_fields(env(), n, rel_fields); + m_constructor_info.insert(n, to_list(rel_fields)); + } + } + + expr visit_minor_premise(expr e, buffer const & rel_fields) { + type_context::tmp_locals locals(ctx()); + for (unsigned i = 0; i < rel_fields.size(); i++) { + lean_assert(is_lambda(e)); + if (rel_fields[i]) { + expr l = locals.push_local_from_binding(e); + e = instantiate(binding_body(e), l); + } else { + e = instantiate(binding_body(e), mk_neutral_expr()); + } + } + e = visit(e); + return locals.mk_lambda(e); + } + + expr visit_cases_on(name const & fn, buffer & args) { + name const & I_name = fn.get_prefix(); + buffer cnames; + get_intro_rule_names(env(), I_name, cnames); + /* Process major premise */ + args[0] = visit(args[0]); + /* We distribute applications over cases_on minor premises in + previous preprocessing steps. */ + lean_assert(args.size() == cnames.size() + 1); + /* Process minor premises */ + for (unsigned i = 0; i < cnames.size(); i++) { + buffer rel_fields; + get_constructor_info(cnames[i], rel_fields); + args[i+1] = visit_minor_premise(args[i+1], rel_fields); + } + + return mk_app(mk_cases(cnames.size()), args); + } + + expr visit_constructor(name const & fn, buffer const & args) { + 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); + buffer rel_fields; + get_constructor_info(fn, rel_fields); + lean_assert(args.size() == nparams + rel_fields.size()); + buffer new_args; + for (unsigned i = 0; i < rel_fields.size(); i++) { + if (rel_fields[i]) { + new_args.push_back(visit(args[nparams + i])); + } + } + return mk_app(mk_constructor(cidx), new_args); + } + + expr visit_projection(name const & fn, buffer const & args) { + projection_info const & info = *get_projection_info(env(), fn); + expr major = visit(args[info.m_nparams]); + buffer rel_fields; + get_constructor_info(info.m_constructor, rel_fields); + lean_assert(info.m_i < rel_fields.size()); + lean_assert(rel_fields[info.m_i]); /* We already erased irrelevant information */ + /* Adjust projection index by ignoring irrelevant fields */ + unsigned j = 0; + for (unsigned i = 0; i < info.m_i; i++) { + if (rel_fields[i]) + j++; + } + expr r = mk_app(mk_proj(j), major); + /* Add additional arguments */ + for (unsigned i = info.m_nparams + 1; i < args.size(); i++) + r = mk_app(r, visit(args[i])); + return r; + } + + virtual expr visit_app(expr const & e) override { + buffer args; + expr const & fn = get_app_args(e, args); + if (is_constant(fn)) { + name const & n = const_name(fn); + if (!ignore(n)) { + if (is_cases_on_recursor(env(), n)) { + return visit_cases_on(n, args); + } else if (inductive::is_intro_rule(env(), n)) { + return visit_constructor(n, args); + } else if (is_projection(env(), n)) { + return visit_projection(n, args); + } + } + } + return compiler_step_visitor::visit_app(e); + } +public: + simp_inductive_fn(environment const & env):compiler_step_visitor(env) {} +}; + +expr simp_inductive(environment const & env, expr const & e) { + return simp_inductive_fn(env)(e); +} + +void simp_inductive(environment const & env, buffer> & procs) { + simp_inductive_fn fn(env); + for (auto & proc : procs) + proc.second = fn(proc.second); +} + +void initialize_simp_inductive() { + g_cases = new name("_cases"); + g_proj = new name("_proj"); + g_cnstr = new name("_cnstr"); +} + +void finalize_simp_inductive() { + delete g_cases; + delete g_proj; + delete g_cnstr; +} +} diff --git a/src/library/compiler/simp_inductive.h b/src/library/compiler/simp_inductive.h new file mode 100644 index 0000000000..5b0876f9fb --- /dev/null +++ b/src/library/compiler/simp_inductive.h @@ -0,0 +1,26 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/environment.h" + +namespace lean { +/** \brief Replaces cases_on, projections and constructor applications with _cases.idx, _proj.idx and _cnstr.idx + It also removes irrelevant fields from constructors. + \remark nat.cases_on, nat.succ and nat.zero are ignored. */ +expr simp_inductive(environment const & env, expr const & e); +void simp_inductive(environment const & env, buffer> & procs); + +/** \brief Return non-none idx iff \c e is of the form _cnstr.idx */ +optional is_internal_cnstr(expr const & e); +/** \brief Return non-none idx iff \c e is of the form _proj.idx */ +optional is_internal_proj(expr const & e); +/** \brief Return non-none n iff \c e is of the form _cases.n */ +optional is_internal_cases(expr const & e); + +void initialize_simp_inductive(); +void finalize_simp_inductive(); +}