From 4e496b78d5e73545fa4f9a807155113d8e6b0561 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 20 May 2017 20:34:18 -0700 Subject: [PATCH] feat(library/equations_compiler): unpack auxiliary definition We still need to unpack auxiliary lemmas, and propagate information in the frontend. --- src/frontends/lean/definition_cmds.cpp | 4 +- src/library/app_builder.h | 4 ++ .../equations_compiler/pack_mutual.cpp | 42 +++++++----- src/library/equations_compiler/pack_mutual.h | 2 + src/library/equations_compiler/wf_rec.cpp | 65 +++++++++++++++++-- tmp/even_odd.lean | 5 ++ 6 files changed, 97 insertions(+), 25 deletions(-) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 546b4b7584..ff93781ff9 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -123,7 +123,7 @@ expr parse_mutual_definition(parser & p, buffer & lp_names, buffer & 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 & lp_names, buffer & params, diff --git a/src/library/app_builder.h b/src/library/app_builder.h index fac8b60a31..fe1b9a115f 100644 --- a/src/library/app_builder.h +++ b/src/library/app_builder.h @@ -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 diff --git a/src/library/equations_compiler/pack_mutual.cpp b/src/library/equations_compiler/pack_mutual.cpp index 1795216cb5..1e4dc0d55b 100644 --- a/src/library/equations_compiler/pack_mutual.cpp +++ b/src/library/equations_compiler/pack_mutual.cpp @@ -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 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(); } - 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 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 { diff --git a/src/library/equations_compiler/pack_mutual.h b/src/library/equations_compiler/pack_mutual.h index 75638df424..dcfddcd18c 100644 --- a/src/library/equations_compiler/pack_mutual.h +++ b/src/library/equations_compiler/pack_mutual.h @@ -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(); } diff --git a/src/library/equations_compiler/wf_rec.cpp b/src/library/equations_compiler/wf_rec.cpp index 43eb323f1b..61887b1d57 100644 --- a/src/library/equations_compiler/wf_rec.cpp +++ b/src/library/equations_compiler/wf_rec.cpp @@ -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 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 fn_names = header.m_fn_names; + type_context ctx = mk_type_context(); + buffer 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); } }; diff --git a/tmp/even_odd.lean b/tmp/even_odd.lean index 9652cd0279..852e0e5886 100644 --- a/tmp/even_odd.lean +++ b/tmp/even_odd.lean @@ -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