feat(library/compiler, library/equations_compiler): avoid rec_fn_macro in the equation and bytecode compilers
This commit is contained in:
Leonardo de Moura
parent
eab962bbc6
commit
b95e710e8c
11 changed files with 130 additions and 136 deletions
|
|
@ -59,7 +59,7 @@ levels closure_helper::collect(levels const & ls) {
|
|||
return levels(r);
|
||||
}
|
||||
|
||||
expr closure_helper::collect(expr const & e) {
|
||||
expr closure_helper::collect(expr const & e, name_set const & except_locals) {
|
||||
lean_assert(!m_finalized_collection);
|
||||
return replace(e, [&](expr const & e, unsigned) {
|
||||
if (is_metavar(e)) {
|
||||
|
|
@ -76,7 +76,7 @@ expr closure_helper::collect(expr const & e) {
|
|||
}
|
||||
} else if (is_local(e)) {
|
||||
name const & id = mlocal_name(e);
|
||||
if (!m_found_local.contains(id)) {
|
||||
if (!m_found_local.contains(id) && !except_locals.contains(id)) {
|
||||
m_found_local.insert(id);
|
||||
m_params.push_back(e);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -54,8 +54,11 @@ public:
|
|||
level collect(level const & l);
|
||||
/* \pre finalize_collection has not been invoked */
|
||||
levels collect(levels const & ls);
|
||||
/* \pre finalize_collection has not been invoked */
|
||||
expr collect(expr const & e);
|
||||
/*
|
||||
\remark Locals at `except_locals` are not collected.
|
||||
\pre finalize_collection has not been invoked */
|
||||
expr collect(expr const & e, name_set const & except_locals);
|
||||
expr collect(expr const & e) { return collect(e, name_set()); }
|
||||
|
||||
/* \pre finalize_collection has not been invoked */
|
||||
void finalize_collection();
|
||||
|
|
|
|||
|
|
@ -18,7 +18,6 @@ Author: Leonardo de Moura
|
|||
#include "library/compiler/procedure.h"
|
||||
#include "library/compiler/comp_irrelevant.h"
|
||||
#include "library/compiler/compiler_step_visitor.h"
|
||||
#include "library/compiler/rec_fn_macro.h"
|
||||
|
||||
namespace lean {
|
||||
class elim_recursors_fn : public compiler_step_visitor {
|
||||
|
|
@ -114,7 +113,7 @@ protected:
|
|||
/* Create expr (rec_fn) for representing recursive calls. */
|
||||
expr aux_decl_type = ctx().infer(aux);
|
||||
name aux_decl_name = mk_compiler_unused_name(m_env, m_prefix, "_rec", m_idx);
|
||||
expr rec_fn = mk_rec_fn_macro(aux_decl_name, aux_decl_type);
|
||||
expr rec_fn = mk_constant(aux_decl_name, const_levels(fn));
|
||||
/* Create new locals for aux.
|
||||
The operating abstract_locals creates a lambda-abstraction around aux if it uses
|
||||
local constants. */
|
||||
|
|
|
|||
|
|
@ -17,7 +17,6 @@ Author: Leonardo de Moura
|
|||
#include "library/compiler/util.h"
|
||||
#include "library/compiler/nat_value.h"
|
||||
#include "library/compiler/comp_irrelevant.h"
|
||||
#include "library/compiler/rec_fn_macro.h"
|
||||
#include "library/compiler/compiler_step_visitor.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -65,8 +64,6 @@ class erase_irrelevant_fn : public compiler_step_visitor {
|
|||
return *g_neutral_expr;
|
||||
} else if (is_comp_irrelevant(e)) {
|
||||
return *g_neutral_expr;
|
||||
} else if (is_rec_fn_macro(e)) {
|
||||
return mk_constant(get_rec_fn_name(e));
|
||||
} else if (is_nat_value(e)) {
|
||||
return e;
|
||||
} else if (auto r = macro_def(e).expand(e, m_ctx)) {
|
||||
|
|
|
|||
|
|
@ -12,11 +12,7 @@ class abstract_context_cache;
|
|||
The parameters, motive and indices are also erased from cases_on applications.
|
||||
|
||||
\remark The resultant term cannot be type checked. So, any preprocessing step
|
||||
that requires type inference cannot be applied after this transformation.
|
||||
|
||||
\remark This procedure also replace occurrences of rec_fn_macro with constants.
|
||||
The rec_fn_macro is only used to make sure the result type checks.
|
||||
So, since the result will not type check anyway, there is no point in using them. */
|
||||
that requires type inference cannot be applied after this transformation. */
|
||||
expr erase_irrelevant(environment const & env, abstract_context_cache & cache, expr const & e);
|
||||
/** \brief Neutral auxiliary term. */
|
||||
bool is_neutral_expr(expr const & e);
|
||||
|
|
|
|||
|
|
@ -39,6 +39,8 @@ Author: Leonardo de Moura
|
|||
|
||||
namespace lean {
|
||||
class expand_aux_fn : public compiler_step_visitor {
|
||||
name_set m_decl_names; /* functions being compiled */
|
||||
|
||||
enum class recursor_kind { Aux, CasesOn, NotRecursor };
|
||||
/* We only expand auxiliary recursors and user-defined recursors.
|
||||
However, we don't unfold recursors of the form C.cases_on if C != eq. */
|
||||
|
|
@ -98,10 +100,16 @@ class expand_aux_fn : public compiler_step_visitor {
|
|||
return is_constant(e) && ::lean::is_inline(env(), const_name(e));
|
||||
}
|
||||
|
||||
bool is_function_being_compiled(expr const & e) const {
|
||||
expr const & f = get_app_fn(e);
|
||||
return is_constant(f) && m_decl_names.contains(const_name(f));
|
||||
}
|
||||
|
||||
bool should_unfold(expr const & e) {
|
||||
return
|
||||
(is_not_vm_function(e) && !ctx().is_proof(e) && !is_pack_unpack(e) && !is_noncomputable_const(e)) ||
|
||||
(is_inline(e));
|
||||
!is_function_being_compiled(e) &&
|
||||
((is_not_vm_function(e) && !ctx().is_proof(e) && !is_pack_unpack(e) && !is_noncomputable_const(e)) ||
|
||||
(is_inline(e)));
|
||||
}
|
||||
|
||||
expr unfold(expr const & e) {
|
||||
|
|
@ -150,11 +158,13 @@ class expand_aux_fn : public compiler_step_visitor {
|
|||
}
|
||||
|
||||
public:
|
||||
expand_aux_fn(environment const & env, abstract_context_cache & cache):compiler_step_visitor(env, cache) {}
|
||||
expand_aux_fn(environment const & env, name_set const & decl_names, abstract_context_cache & cache):
|
||||
compiler_step_visitor(env, cache),
|
||||
m_decl_names(decl_names) {}
|
||||
};
|
||||
|
||||
static expr expand_aux(environment const & env, abstract_context_cache & cache, expr const & e) {
|
||||
return expand_aux_fn(env, cache)(e);
|
||||
static expr expand_aux(environment const & env, name_set const & ns, abstract_context_cache & cache, expr const & e) {
|
||||
return expand_aux_fn(env, ns, cache)(e);
|
||||
}
|
||||
|
||||
static name * g_tmp_prefix = nullptr;
|
||||
|
|
@ -162,6 +172,7 @@ static name * g_tmp_prefix = nullptr;
|
|||
class preprocess_fn {
|
||||
environment m_env;
|
||||
context_cache m_cache;
|
||||
name_set m_decl_names; /* name of the functions being compiled */
|
||||
|
||||
bool check(declaration const & d, expr const & v) {
|
||||
bool memoize = true;
|
||||
|
|
@ -185,25 +196,6 @@ class preprocess_fn {
|
|||
}
|
||||
}
|
||||
|
||||
#if 0
|
||||
void dump_pos_info(expr const & v) {
|
||||
std::cout << v << "\n\n";
|
||||
for_each(v, [&](expr const & e, unsigned) {
|
||||
auto pip = get_pos_info_provider();
|
||||
if (!pip) return false;
|
||||
if (auto p = pip->get_pos_info(e))
|
||||
std::cout << "pos[" << ((unsigned)e.kind()) << "]: " << p->first << ":" << p->second << "\n"
|
||||
<< e << "\n";
|
||||
return true;
|
||||
});
|
||||
std::cout << "------------\n";
|
||||
}
|
||||
|
||||
void dump_pos_info(buffer<pair<name, expr>> & procs) {
|
||||
for (auto p : procs) dump_pos_info(p.second);
|
||||
}
|
||||
#endif
|
||||
|
||||
/* If type of d is a proposition or return a type, we don't need to compile it.
|
||||
We can just generate (fun args, neutral_expr)
|
||||
|
||||
|
|
@ -230,8 +222,16 @@ class preprocess_fn {
|
|||
}
|
||||
|
||||
public:
|
||||
preprocess_fn(environment const & env):
|
||||
m_env(env) {}
|
||||
preprocess_fn(environment const & env, declaration const & d):
|
||||
m_env(env) {
|
||||
m_decl_names.insert(d.get_name());
|
||||
}
|
||||
|
||||
preprocess_fn(environment const & env, buffer<declaration> const & ds):
|
||||
m_env(env) {
|
||||
for (declaration const & d : ds)
|
||||
m_decl_names.insert(d.get_name());
|
||||
}
|
||||
|
||||
void operator()(declaration const & d, buffer<procedure> & procs) {
|
||||
if (compile_irrelevant(d, procs))
|
||||
|
|
@ -241,7 +241,7 @@ public:
|
|||
v = inline_simple_definitions(m_env, m_cache, v);
|
||||
lean_cond_assert("compiler", check(d, v));
|
||||
lean_trace(name({"compiler", "inline"}), tout() << "\n" << v << "\n";);
|
||||
v = expand_aux(m_env, m_cache, v);
|
||||
v = expand_aux(m_env, m_decl_names, m_cache, v);
|
||||
lean_cond_assert("compiler", check(d, v));
|
||||
lean_trace(name({"compiler", "expand_aux"}), tout() << "\n" << v << "\n";);
|
||||
v = mark_comp_irrelevant_subterms(m_env, m_cache, v);
|
||||
|
|
@ -276,13 +276,14 @@ public:
|
|||
};
|
||||
|
||||
void preprocess(environment const & env, declaration const & d, buffer<procedure> & result) {
|
||||
return preprocess_fn(env)(d, result);
|
||||
return preprocess_fn(env, d)(d, result);
|
||||
}
|
||||
|
||||
void preprocess(environment const & env, buffer<declaration> const & ds, buffer<procedure> & result) {
|
||||
preprocess_fn F(env, ds);
|
||||
for (declaration const & d : ds) {
|
||||
buffer<procedure> procs;
|
||||
preprocess(env, d, procs);
|
||||
F(d, procs);
|
||||
result.append(procs);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -9,7 +9,6 @@ Author: Leonardo de Moura
|
|||
#include "kernel/free_vars.h"
|
||||
#include "kernel/for_each_fn.h"
|
||||
#include "library/trace.h"
|
||||
#include "library/compiler/rec_fn_macro.h"
|
||||
#include "library/compiler/procedure.h"
|
||||
#include "library/compiler/compiler_step_visitor.h"
|
||||
|
||||
|
|
@ -30,13 +29,6 @@ class remove_args_fn : public compiler_step_visitor {
|
|||
/* Mapping from auxiliary function name to bitvector of used arguments */
|
||||
name_map<std::vector<bool>> const & m_to_reduce;
|
||||
|
||||
virtual expr visit_macro(expr const & e) override {
|
||||
/* This module assumes rec_fn_macros have already been eliminated.
|
||||
Remark: the step erase_irrelevant eliminates all occurences. */
|
||||
lean_assert(!is_rec_fn_macro(e));
|
||||
return compiler_step_visitor::visit_macro(e);
|
||||
}
|
||||
|
||||
virtual expr visit_app(expr const & e) override {
|
||||
expr const & fn = get_app_fn(e);
|
||||
if (is_constant(fn)) {
|
||||
|
|
|
|||
|
|
@ -13,9 +13,6 @@ namespace lean {
|
|||
/** \brief Try to reduce the arity of auxiliary declarations in procs.
|
||||
It assumes all but the last entry are auxiliary declarations.
|
||||
|
||||
\remark This procedure assumes rec_fn_macro has already been eliminated.
|
||||
The procedure erase_irrelevant can be used to accomplish that.
|
||||
|
||||
\remark This step does not rely on type information. That is,
|
||||
the input expressions don't need to be type checkable. */
|
||||
void reduce_arity(environment const & env, abstract_context_cache & cache, buffer<procedure> & procs);
|
||||
|
|
|
|||
|
|
@ -39,8 +39,8 @@ expr get_as_pattern_rhs(expr const & e);
|
|||
|
||||
struct equations_header {
|
||||
unsigned m_num_fns{0}; /* number of functions being defined */
|
||||
names m_fn_names; /* local names for functions */
|
||||
names m_fn_actual_names; /* Full qualified name and/or private name */
|
||||
names m_fn_names; /* local names for functions */
|
||||
names m_fn_actual_names; /* Full qualified name and/or private name */
|
||||
bool m_is_private{false}; /* if true, it must be a private definition */
|
||||
bool m_is_lemma{false}; /* if true, equations are defining a lemma */
|
||||
bool m_is_meta{false}; /* the auxiliary declarations should be tagged as meta */
|
||||
|
|
|
|||
|
|
@ -22,38 +22,30 @@ Author: Leonardo de Moura
|
|||
#include "frontends/lean/elaborator.h"
|
||||
|
||||
namespace lean {
|
||||
static expr replace_rec_apps(type_context_old & ctx, expr const & e) {
|
||||
equations_header const & header = get_equations_header(e);
|
||||
names actual_names = header.m_fn_actual_names;
|
||||
unpack_eqns ues(ctx, e);
|
||||
buffer<expr> fns;
|
||||
buffer<expr> macro_fns;
|
||||
for (unsigned fidx = 0; fidx < ues.get_num_fns(); fidx++) {
|
||||
expr const & fn = ues.get_fn(fidx);
|
||||
fns.push_back(fn);
|
||||
macro_fns.push_back(mk_rec_fn_macro(head(actual_names), ctx.infer(fn)));
|
||||
actual_names = tail(actual_names);
|
||||
}
|
||||
for (unsigned fidx = 0; fidx < ues.get_num_fns(); fidx++) {
|
||||
buffer<expr> & eqns = ues.get_eqns_of(fidx);
|
||||
for (expr & eqn : eqns) {
|
||||
unpack_eqn ue(ctx, eqn);
|
||||
expr new_rhs = replace_locals(ue.rhs(), fns, macro_fns);
|
||||
ue.rhs() = new_rhs;
|
||||
eqn = ue.repack();
|
||||
}
|
||||
}
|
||||
expr r = ues.repack();
|
||||
lean_trace("eqn_compiler", tout() << "using unbounded recursion (meta-definition):\n" << r << "\n";);
|
||||
return r;
|
||||
}
|
||||
|
||||
static void split_rec_fns(type_context_old & ctx, expr const & e, buffer<expr> & result) {
|
||||
static local_context split_rec_fns(environment const & env, metavar_context & mctx, local_context const & lctx, expr const & e, buffer<expr> & aux_rec_fns, buffer<expr> & result) {
|
||||
equations_header const & header = get_equations_header(e);
|
||||
unpack_eqns ues(ctx, e);
|
||||
type_context_old ctx1(env, options(), mctx, lctx, transparency_mode::Semireducible); // TODO(Leo): fix options
|
||||
unpack_eqns ues1(ctx1, e);
|
||||
/* Create declarations for recursive functions at `new_lctx` */
|
||||
local_context new_lctx = lctx;
|
||||
for (unsigned fidx = 0; fidx < ues1.get_num_fns(); fidx++) {
|
||||
expr const & fn = ues1.get_fn(fidx);
|
||||
expr aux_rec_fn = new_lctx.mk_local_decl(name(mlocal_pp_name(fn), "_rec"), ctx1.infer(fn), local_info(fn));
|
||||
aux_rec_fns.push_back(aux_rec_fn);
|
||||
}
|
||||
|
||||
/* Split equations, and replace recursive calls with aux_rec_fns */
|
||||
type_context_old ctx2(env, options(), ctx1.mctx(), new_lctx, transparency_mode::Semireducible); // TODO(Leo): fix options
|
||||
unpack_eqns ues2(ctx2, e);
|
||||
names fn_names = header.m_fn_names;
|
||||
names fn_actual_names = header.m_fn_actual_names;
|
||||
for (unsigned fidx = 0; fidx < ues.get_num_fns(); fidx++) {
|
||||
buffer<expr> fns;
|
||||
for (unsigned fidx = 0; fidx < ues2.get_num_fns(); fidx++) {
|
||||
expr const & fn = ues2.get_fn(fidx);
|
||||
fns.push_back(fn);
|
||||
}
|
||||
for (unsigned fidx = 0; fidx < ues2.get_num_fns(); fidx++) {
|
||||
equations_header new_header = header;
|
||||
new_header.m_num_fns = 1;
|
||||
new_header.m_fn_names = names(head(fn_names));
|
||||
|
|
@ -61,22 +53,27 @@ static void split_rec_fns(type_context_old & ctx, expr const & e, buffer<expr> &
|
|||
fn_names = tail(fn_names);
|
||||
fn_actual_names = tail(fn_actual_names);
|
||||
buffer<expr> eqns;
|
||||
for (expr const & eqn : ues.get_eqns_of(fidx)) {
|
||||
eqns.push_back(ctx.mk_lambda(ues.get_fn(fidx), eqn));
|
||||
for (expr const & eqn : ues2.get_eqns_of(fidx)) {
|
||||
unpack_eqn ue(ctx2, eqn);
|
||||
expr new_rhs = replace_locals(ue.rhs(), fns, aux_rec_fns);
|
||||
ue.rhs() = new_rhs;
|
||||
eqns.push_back(ctx2.mk_lambda(ues2.get_fn(fidx), ue.repack()));
|
||||
}
|
||||
result.push_back(mk_equations(new_header, eqns.size(), eqns.data()));
|
||||
}
|
||||
|
||||
mctx = ctx2.mctx();
|
||||
return new_lctx;
|
||||
}
|
||||
|
||||
static expr fix_rec_apps(expr const & e, name_map<expr> const & name2new_type,
|
||||
buffer<expr> const & closure_params) {
|
||||
static expr fix_rec_apps(expr const & e, name_map<name> const & aux_rec_name2actual_name,
|
||||
levels const & closure_levels, buffer<expr> const & closure_params) {
|
||||
return replace(e, [&](expr const & t) {
|
||||
if (is_rec_fn_macro(t)) {
|
||||
if (auto new_type = name2new_type.find(get_rec_fn_name(t))) {
|
||||
return some_expr(mk_app(mk_rec_fn_macro(get_rec_fn_name(t), *new_type),
|
||||
closure_params));
|
||||
if (is_local(t)) {
|
||||
if (name const * actual_name = aux_rec_name2actual_name.find(mlocal_name(t))) {
|
||||
return some_expr(mk_app(mk_constant(*actual_name, closure_levels), closure_params));
|
||||
} else {
|
||||
throw exception("internal error, ill-formed mutual recursive definition");
|
||||
return none_expr();
|
||||
}
|
||||
} else {
|
||||
return none_expr();
|
||||
|
|
@ -87,12 +84,22 @@ static expr fix_rec_apps(expr const & e, name_map<expr> const & name2new_type,
|
|||
eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
|
||||
metavar_context & mctx, local_context const & lctx,
|
||||
expr const & e) {
|
||||
type_context_old ctx(env, mctx, lctx, elab.get_cache(), transparency_mode::Semireducible);
|
||||
|
||||
/* Replace recursive application with macro, and split mutual definition in n definitions. */
|
||||
expr e1 = replace_rec_apps(ctx, e);
|
||||
/* Split recursive equations by using new auxiliary `.rec` locals */
|
||||
buffer<expr> aux_rec_fns;
|
||||
buffer<expr> es;
|
||||
split_rec_fns(ctx, e1, es);
|
||||
local_context aux_lctx = split_rec_fns(env, mctx, lctx, e, aux_rec_fns, es);
|
||||
type_context_old ctx(env, mctx, aux_lctx, elab.get_cache(), transparency_mode::Semireducible);
|
||||
|
||||
/* Create set of auxiliary locals and mapping from auxiliary local to actual name */
|
||||
equations_header const & header = get_equations_header(e);
|
||||
name_set aux_rec_fn_names;
|
||||
name_map<name> aux_rec_fn_name2actual_name;
|
||||
names fn_actual_names = header.m_fn_actual_names;
|
||||
for (expr const & aux_rec_fn : aux_rec_fns) {
|
||||
aux_rec_fn_names.insert(mlocal_name(aux_rec_fn));
|
||||
aux_rec_fn_name2actual_name.insert(mlocal_name(aux_rec_fn), head(fn_actual_names));
|
||||
fn_actual_names = tail(fn_actual_names);
|
||||
}
|
||||
|
||||
if (is_recursive_eqns(ctx, e)) {
|
||||
/* We create auxiliary definitions when compiling mutually recursive equations. */
|
||||
|
|
@ -102,83 +109,84 @@ eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
|
|||
closure_helper helper(ctx);
|
||||
|
||||
/* 1. Compile pattern matching */
|
||||
|
||||
for (unsigned fidx = 0; fidx < es.size(); fidx++) {
|
||||
unpack_eqns ues(ctx, es[fidx]);
|
||||
auto R = elim_match(env, elab, mctx, lctx, es[fidx]);
|
||||
fns.push_back(helper.collect(R.m_fn));
|
||||
auto R = elim_match(env, elab, mctx, aux_lctx, es[fidx]);
|
||||
|
||||
/* We must not collect auxiliary locals in `aux_rec_fns` */
|
||||
fns.push_back(helper.collect(R.m_fn, aux_rec_fn_names));
|
||||
fn_types.push_back(helper.collect(ctx.infer(ues.get_fn(0))));
|
||||
for (list<expr> const & ts : R.m_counter_examples) {
|
||||
counter_examples.push_back(mk_app(ues.get_fn(0), ts));
|
||||
}
|
||||
}
|
||||
|
||||
helper.finalize_collection();
|
||||
|
||||
buffer<level> closure_lvl_params;
|
||||
buffer<expr> closure_params;
|
||||
helper.get_level_closure(closure_lvl_params);
|
||||
helper.get_expr_closure(closure_params);
|
||||
buffer<level> closure_lvl_args;
|
||||
buffer<expr> closure_args;
|
||||
helper.get_level_closure(closure_lvl_args);
|
||||
helper.get_expr_closure(closure_args);
|
||||
|
||||
names lvl_names;
|
||||
lvl_names = helper.get_norm_level_names();
|
||||
levels lvls = param_names_to_levels(lvl_names);
|
||||
buffer<expr> const & params = helper.get_norm_closure_params();
|
||||
|
||||
equations_header const & header = get_equations_header(e);
|
||||
names fn_names = header.m_fn_names;
|
||||
names fn_actual_names = header.m_fn_actual_names;
|
||||
bool zeta = get_eqn_compiler_zeta(elab.get_options());
|
||||
bool zeta = get_eqn_compiler_zeta(elab.get_options());
|
||||
|
||||
/* 2. Update fn_types.
|
||||
zeta-expand (if needed) and apply closures. */
|
||||
|
||||
name_map<expr> name2type;
|
||||
for (unsigned fidx = 0; fidx < es.size(); fidx++) {
|
||||
name fn_name = head(fn_actual_names);
|
||||
expr fn_type = fn_types[fidx];
|
||||
if (zeta) {
|
||||
fn_type = zeta_expand(lctx, fn_type);
|
||||
fn_type = zeta_expand(aux_lctx, fn_type);
|
||||
}
|
||||
fn_type = helper.mk_pi_closure(fn_type);
|
||||
fn_types[fidx] = fn_type;
|
||||
name2type.insert(fn_name, fn_type);
|
||||
fn_actual_names = tail(fn_actual_names);
|
||||
fn_types[fidx] = fn_type;
|
||||
}
|
||||
|
||||
/* 3. Fix recursive applications, declare definition, and private/alias info */
|
||||
|
||||
/* 3. Fix recursive applications, and create definitions */
|
||||
buffer<declaration> new_declarations;
|
||||
fn_actual_names = header.m_fn_actual_names;
|
||||
buffer<expr> result_fns;
|
||||
for (unsigned fidx = 0; fidx < es.size(); fidx++) {
|
||||
name fn_name = head(fn_actual_names);
|
||||
expr fn_type = fn_types[fidx];
|
||||
expr fn = fns[fidx];
|
||||
if (zeta) {
|
||||
fn = zeta_expand(lctx, fn);
|
||||
fn = zeta_expand(aux_lctx, fn);
|
||||
}
|
||||
fn = fix_rec_apps(fn, name2type, helper.get_norm_closure_params());
|
||||
fn = fix_rec_apps(fn, aux_rec_fn_name2actual_name, lvls, params);
|
||||
fn = helper.mk_lambda_closure(fn);
|
||||
|
||||
bool use_self_opt = true;
|
||||
bool is_meta = true;
|
||||
declaration d = mk_definition(env, fn_name, lvl_names, fn_type, fn, use_self_opt, is_meta);
|
||||
env = module::add(env, check(env, d));
|
||||
|
||||
expr result_fn = mk_app(mk_constant(fn_name, levels(closure_lvl_params)), closure_params);
|
||||
new_declarations.push_back(d);
|
||||
fn_actual_names = tail(fn_actual_names);
|
||||
}
|
||||
|
||||
env = module::add_meta(env, new_declarations);
|
||||
|
||||
/* 4. Create result and add private/alias info */
|
||||
buffer<expr> result_fns;
|
||||
names fn_names = header.m_fn_names;
|
||||
fn_actual_names = header.m_fn_actual_names;
|
||||
for (unsigned fidx = 0; fidx < es.size(); fidx++) {
|
||||
name fn_name = head(fn_actual_names);
|
||||
expr result_fn = mk_app(mk_constant(fn_name, levels(closure_lvl_args)), closure_args);
|
||||
|
||||
result_fns.push_back(result_fn);
|
||||
|
||||
if (header.m_is_private) {
|
||||
env = register_private_name(env, head(fn_names), fn_name);
|
||||
env = add_expr_alias(env, head(fn_names), fn_name);
|
||||
}
|
||||
|
||||
fn_names = tail(fn_names);
|
||||
fn_actual_names = tail(fn_actual_names);
|
||||
fn_names = tail(fn_names);
|
||||
fn_actual_names = tail(fn_actual_names);
|
||||
}
|
||||
|
||||
/* 4. Compile. Remark: we need a separate pass because we need to reserve the functions
|
||||
/* 5. Compile. Remark: we need a separate pass because we need to reserve the functions
|
||||
and their arities in the VM. */
|
||||
|
||||
buffer<declaration> new_decls;
|
||||
for (name const & n : header.m_fn_actual_names) {
|
||||
new_decls.push_back(env.get(n));
|
||||
|
|
@ -192,8 +200,9 @@ eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
|
|||
ss << " '" << n << "'";
|
||||
throw nested_exception(ss, ex);
|
||||
}
|
||||
|
||||
return { to_list(result_fns), to_list(counter_examples) };
|
||||
} else {
|
||||
} else {
|
||||
lean_assert(!is_recursive_eqns(ctx, e));
|
||||
/* If the equations are recursive, we simply compile each one of them and combine the
|
||||
results.
|
||||
|
|
|
|||
|
|
@ -977,7 +977,7 @@ void update_telescope(type_context_old & ctx, buffer<expr> const & vars, expr co
|
|||
}
|
||||
|
||||
/* Helper functor for mk_smart_unfolding_definition */
|
||||
struct replace_rec_fn_macro_fn : public replace_visitor {
|
||||
struct replace_aux_meta_fn : public replace_visitor {
|
||||
name const & m_fn_aux_name;
|
||||
expr const & m_new_fn;
|
||||
unsigned m_nargs_to_skip;
|
||||
|
|
@ -986,8 +986,8 @@ struct replace_rec_fn_macro_fn : public replace_visitor {
|
|||
virtual expr visit_app(expr const & e) override {
|
||||
buffer<expr> args;
|
||||
expr const & fn = get_app_args(e, args);
|
||||
if (is_rec_fn_macro(fn)) {
|
||||
if (args.size() >= m_nargs_to_skip && get_rec_fn_name(fn) == m_fn_aux_name) {
|
||||
if (is_constant(fn) && const_name(fn) == m_fn_aux_name) {
|
||||
if (args.size() >= m_nargs_to_skip) {
|
||||
m_found = true;
|
||||
for (unsigned i = m_nargs_to_skip; i < args.size(); i++) {
|
||||
expr & arg = args[i];
|
||||
|
|
@ -1013,7 +1013,7 @@ struct replace_rec_fn_macro_fn : public replace_visitor {
|
|||
}
|
||||
}
|
||||
|
||||
replace_rec_fn_macro_fn(name const & fn_aux_name, expr const & new_fn, unsigned nargs_to_skip):
|
||||
replace_aux_meta_fn(name const & fn_aux_name, expr const & new_fn, unsigned nargs_to_skip):
|
||||
m_fn_aux_name(fn_aux_name),
|
||||
m_new_fn(new_fn),
|
||||
m_nargs_to_skip(nargs_to_skip) {
|
||||
|
|
@ -1050,7 +1050,7 @@ environment mk_smart_unfolding_definition(environment const & env, options const
|
|||
expr new_fn = mk_app(mk_constant(n, ls), locals.size(), locals.data());
|
||||
helper_value = instantiate_value_univ_params(*aux_d, const_levels(fn));
|
||||
helper_value = apply_beta(helper_value, args.size(), args.data());
|
||||
replace_rec_fn_macro_fn proc(meta_aux_fn_name, new_fn, args.size());
|
||||
replace_aux_meta_fn proc(meta_aux_fn_name, new_fn, args.size());
|
||||
helper_value = proc(helper_value);
|
||||
if (!proc.m_found)
|
||||
throw exception("failed to generate helper declaration for smart unfolding, auxiliary meta declaration does not contain recursive application");
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue