feat(library/equations_compiler): unpack auxiliary definition
We still need to unpack auxiliary lemmas, and propagate information in the frontend.
This commit is contained in:
Leonardo de Moura
parent
f742d9c9d8
commit
4e496b78d5
6 changed files with 97 additions and 25 deletions
|
|
@ -123,7 +123,7 @@ expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<expr> &
|
|||
expr fn_type = parse_inner_header(p, local_pp_name(pre_fn)).first;
|
||||
declaration_name_scope scope2(local_pp_name(pre_fn));
|
||||
declaration_name_scope scope3("_main");
|
||||
full_names.push_back(scope2.get_name());
|
||||
full_names.push_back(scope3.get_name());
|
||||
if (p.curr_is_token(get_period_tk())) {
|
||||
auto period_pos = p.pos();
|
||||
p.next();
|
||||
|
|
@ -169,7 +169,7 @@ environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
|
|||
tout() << val << "\n";
|
||||
// TODO(Leo)
|
||||
|
||||
return p.env();
|
||||
return elab.env();
|
||||
}
|
||||
|
||||
static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<expr> & params,
|
||||
|
|
|
|||
|
|
@ -53,6 +53,10 @@ inline expr mk_app(type_context & ctx, name const & c, expr const & a1, expr con
|
|||
return mk_app(ctx, c, {a1, a2, a3});
|
||||
}
|
||||
|
||||
inline expr mk_app(type_context & ctx, name const & c, expr const & a1, expr const & a2, expr const & a3, expr const & a4) {
|
||||
return mk_app(ctx, c, {a1, a2, a3, a4});
|
||||
}
|
||||
|
||||
expr mk_app(type_context & ctx, name const & c, unsigned mask_sz, bool const * mask, expr const * args);
|
||||
|
||||
/** \brief Shortcut for mk_app(c, total_nargs, mask, expl_nargs), where
|
||||
|
|
|
|||
|
|
@ -17,6 +17,29 @@ Author: Leonardo de Moura
|
|||
namespace lean {
|
||||
#define trace_debug_mutual(Code) lean_trace(name({"debug", "eqn_compiler", "mutual"}), scope_trace_env _scope(m_ctx.env(), m_ctx); Code)
|
||||
|
||||
static expr mk_mutual_arg(type_context & ctx, expr const & e, unsigned fidx, unsigned num_fns,
|
||||
expr psum_type, unsigned i) {
|
||||
if (i == num_fns - 1) {
|
||||
return e;
|
||||
} else {
|
||||
psum_type = ctx.relaxed_whnf(psum_type);
|
||||
buffer<expr> args;
|
||||
get_app_args(psum_type, args);
|
||||
tout() << ">> " << psum_type << "\n";
|
||||
lean_assert(args.size() == 2);
|
||||
if (i == fidx) {
|
||||
return mk_app(ctx, get_psum_inl_name(), args[0], args[1], e);
|
||||
} else {
|
||||
expr r = mk_mutual_arg(ctx, e, fidx, num_fns, args[1], i+1);
|
||||
return mk_app(ctx, get_psum_inr_name(), args[0], args[1], r);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
expr mk_mutual_arg(type_context & ctx, expr const & e, unsigned fidx, unsigned num_fns, expr const & psum_type) {
|
||||
return mk_mutual_arg(ctx, e, fidx, num_fns, psum_type, 0);
|
||||
}
|
||||
|
||||
struct pack_mutual_fn {
|
||||
type_context & m_ctx;
|
||||
|
||||
|
|
@ -88,25 +111,8 @@ struct pack_mutual_fn {
|
|||
return optional<unsigned>();
|
||||
}
|
||||
|
||||
expr mk_new_arg(expr const & e, unsigned fidx, unsigned i, expr psum_type) {
|
||||
if (i == m_ues.get_num_fns() - 1) {
|
||||
return e;
|
||||
} else {
|
||||
psum_type = m_ctx.relaxed_whnf(psum_type);
|
||||
buffer<expr> args;
|
||||
get_app_args(psum_type, args);
|
||||
lean_assert(args.size() == 2);
|
||||
if (i == fidx) {
|
||||
return mk_app(m_ctx, get_psum_inl_name(), args[0], args[1], e);
|
||||
} else {
|
||||
expr r = mk_new_arg(e, fidx, i+1, args[1]);
|
||||
return mk_app(m_ctx, get_psum_inr_name(), args[0], args[1], r);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
expr mk_new_arg(expr const & e, unsigned fidx) {
|
||||
return mk_new_arg(e, fidx, 0, m_new_domain);
|
||||
return mk_mutual_arg(m_ctx, e, fidx, m_ues.get_num_fns(), m_new_domain);
|
||||
}
|
||||
|
||||
virtual expr visit_app(expr const & e) override {
|
||||
|
|
|
|||
|
|
@ -11,6 +11,8 @@ namespace lean {
|
|||
The functions must be unary. */
|
||||
expr pack_mutual(type_context & ctx, expr const & eqns);
|
||||
|
||||
expr mk_mutual_arg(type_context & ctx, expr const & e, unsigned fidx, unsigned num_fns, expr const & psum_type);
|
||||
|
||||
void initialize_pack_mutual();
|
||||
void finalize_pack_mutual();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -265,16 +265,74 @@ struct wf_rec_fn {
|
|||
eqn_idx, m_header.m_is_private, locals.as_buffer(), new_lhs, new_rhs);
|
||||
eqn_idx++;
|
||||
}
|
||||
m_mctx = ctx.mctx();
|
||||
}
|
||||
|
||||
expr_pair mk_sigma(type_context & ctx, unsigned i, buffer<expr> const & args) {
|
||||
lean_assert(args.size() > 0);
|
||||
if (i == args.size() - 1) {
|
||||
return mk_pair(args[i], ctx.infer(args[i]));
|
||||
} else {
|
||||
expr as, as_type;
|
||||
std::tie(as, as_type) = mk_sigma(ctx, i+1, args);
|
||||
expr a = args[i];
|
||||
lean_assert(is_local(a));
|
||||
expr a_type = ctx.infer(a);
|
||||
level a_lvl = get_level(ctx, a_type);
|
||||
level as_lvl = get_level(ctx, as_type);
|
||||
as_type = ctx.mk_lambda(a, as_type);
|
||||
expr r_type = mk_app(mk_constant(get_psigma_name(), {a_lvl, as_lvl}), a_type, as_type);
|
||||
expr r = mk_app(mk_constant(get_psigma_mk_name(), {a_lvl, as_lvl}),
|
||||
a_type, as_type, a, as);
|
||||
return mk_pair(r, r_type);
|
||||
}
|
||||
}
|
||||
|
||||
expr unpack(expr const & packed_fn, expr const & eqns_before_pack) {
|
||||
equations_header const & header = get_equations_header(eqns_before_pack);
|
||||
list<name> fn_names = header.m_fn_names;
|
||||
type_context ctx = mk_type_context();
|
||||
buffer<expr> result_fns;
|
||||
expr packed_fn_type = ctx.relaxed_whnf(ctx.infer(packed_fn));
|
||||
expr packed_domain = binding_domain(packed_fn_type);
|
||||
unpack_eqns ues(ctx, eqns_before_pack);
|
||||
unsigned num_fns = ues.get_num_fns();
|
||||
for (unsigned fidx = 0; fidx < num_fns; fidx++) {
|
||||
unsigned arity = ues.get_arity_of(fidx);
|
||||
expr fn_type = ctx.infer(ues.get_fn(fidx));
|
||||
type_context::tmp_locals args(ctx);
|
||||
expr it = fn_type;
|
||||
for (unsigned i = 0; i < arity; i++) {
|
||||
it = ctx.relaxed_whnf(it);
|
||||
lean_assert(is_pi(it));
|
||||
expr arg = args.push_local_from_binding(it);
|
||||
it = instantiate(binding_body(it), arg);
|
||||
}
|
||||
expr sigma_mk = mk_sigma(ctx, 0, args.as_buffer()).first;
|
||||
expr packed_arg = mk_mutual_arg(ctx, sigma_mk, fidx, num_fns, packed_domain);
|
||||
expr fn_val = args.mk_lambda(mk_app(packed_fn, packed_arg));
|
||||
name fn_name = head(fn_names);
|
||||
fn_names = tail(fn_names);
|
||||
trace_debug_wf(tout() << fn_name << " := " << fn_val << "\n";);
|
||||
expr r;
|
||||
std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, header, fn_name, fn_type, fn_val);
|
||||
result_fns.push_back(r);
|
||||
/* TODO(Leo): unpack equations */
|
||||
}
|
||||
|
||||
return mk_equations_result(result_fns.size(), result_fns.data());
|
||||
}
|
||||
|
||||
expr operator()(expr eqns) {
|
||||
m_ref = eqns;
|
||||
m_header = get_equations_header(eqns);
|
||||
/* Make sure all functions are unary */
|
||||
eqns = pack_domain(eqns);
|
||||
expr before_pack = eqns;
|
||||
eqns = pack_domain(eqns);
|
||||
trace_debug_wf(tout() << "after pack_domain\n" << eqns << "\n";);
|
||||
|
||||
/* Make sure we have only one function */
|
||||
expr before_mutual = eqns;
|
||||
equations_header const & header = get_equations_header(eqns);
|
||||
if (header.m_num_fns > 1) {
|
||||
eqns = pack_mutual(eqns);
|
||||
|
|
@ -307,10 +365,7 @@ struct wf_rec_fn {
|
|||
mk_lemmas(fn, r.m_lemmas);
|
||||
}
|
||||
|
||||
|
||||
// TODO(Leo):
|
||||
throw exception("support for well-founded recursion has not been implemented yet, "
|
||||
"use 'set_option trace.eqn_compiler true' for additional information");
|
||||
return unpack(fn, before_pack);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -14,6 +14,11 @@ with odd : nat → bool
|
|||
| 0 := ff
|
||||
| (a+1) := even a
|
||||
|
||||
#eval even._main 3
|
||||
#eval even._main 4
|
||||
#eval odd._main 3
|
||||
#eval odd._main 4
|
||||
|
||||
mutual def f, g {α β : Type u} (f : α → β) (p : α × β)
|
||||
with f : Π n : nat, vector (α × β) n
|
||||
| 0 := vector.nil
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue