refactor(library/app_builder): throw exception instead of returning none_expr
This commit is contained in:
Leonardo de Moura
parent
0061d595d0
commit
1d1f043192
5 changed files with 210 additions and 236 deletions
|
|
@ -1206,9 +1206,10 @@ static environment refl_cmd(parser & p) {
|
|||
name relname = p.check_constant_next("invalid #refl command, constant expected");
|
||||
expr e; level_param_names ls;
|
||||
std::tie(e, ls) = parse_local_expr(p);
|
||||
if (auto r = b.mk_refl(relname, e)) {
|
||||
check_expr_and_print(p, *r);
|
||||
} else {
|
||||
try {
|
||||
expr r = b.mk_refl(relname, e);
|
||||
check_expr_and_print(p, r);
|
||||
} catch (app_builder_exception &) {
|
||||
throw parser_error(sstream() << "failed to build refl proof", pos);
|
||||
}
|
||||
return env;
|
||||
|
|
@ -1221,9 +1222,10 @@ static environment symm_cmd(parser & p) {
|
|||
name relname = p.check_constant_next("invalid #symm command, constant expected");
|
||||
expr e; level_param_names ls;
|
||||
std::tie(e, ls) = parse_local_expr(p);
|
||||
if (auto r = b.mk_symm(relname, e)) {
|
||||
check_expr_and_print(p, *r);
|
||||
} else {
|
||||
try {
|
||||
expr r = b.mk_symm(relname, e);
|
||||
check_expr_and_print(p, r);
|
||||
} catch (app_builder_exception &) {
|
||||
throw parser_error(sstream() << "failed to build symm proof", pos);
|
||||
}
|
||||
return env;
|
||||
|
|
@ -1238,9 +1240,10 @@ static environment trans_cmd(parser & p) {
|
|||
std::tie(H1, ls) = parse_local_expr(p);
|
||||
p.check_token_next(get_comma_tk(), "invalid #trans command, ',' expected");
|
||||
std::tie(H2, ls) = parse_local_expr(p);
|
||||
if (auto r = b.mk_trans(relname, H1, H2)) {
|
||||
check_expr_and_print(p, *r);
|
||||
} else {
|
||||
try {
|
||||
expr r = b.mk_trans(relname, H1, H2);
|
||||
check_expr_and_print(p, r);
|
||||
} catch (app_builder_exception &) {
|
||||
throw parser_error(sstream() << "failed to build trans proof", pos);
|
||||
}
|
||||
return env;
|
||||
|
|
|
|||
|
|
@ -242,25 +242,25 @@ struct app_builder::imp {
|
|||
m_ctx->set_next_mvar_idx(e.m_num_emeta);
|
||||
}
|
||||
|
||||
optional<expr> mk_app(name const & c, unsigned nargs, expr const * args) {
|
||||
expr mk_app(name const & c, unsigned nargs, expr const * args) {
|
||||
optional<entry> e = get_entry(c, nargs);
|
||||
if (!e)
|
||||
return none_expr();
|
||||
throw app_builder_exception();
|
||||
init_ctx_for(*e);
|
||||
unsigned i = nargs;
|
||||
for (auto m : e->m_expl_args) {
|
||||
if (i == 0)
|
||||
return none_expr();
|
||||
throw app_builder_exception();
|
||||
--i;
|
||||
if (!m_ctx->assign(m, args[i]))
|
||||
return none_expr();
|
||||
throw app_builder_exception();
|
||||
}
|
||||
if (!check_all_assigned(*e))
|
||||
return none_expr();
|
||||
return some_expr(m_ctx->instantiate_uvars_mvars(e->m_app));
|
||||
throw app_builder_exception();
|
||||
return m_ctx->instantiate_uvars_mvars(e->m_app);
|
||||
}
|
||||
|
||||
optional<expr> mk_app(name const & c, std::initializer_list<expr> const & it) {
|
||||
expr mk_app(name const & c, std::initializer_list<expr> const & it) {
|
||||
return mk_app(c, it.size(), it.begin());
|
||||
}
|
||||
|
||||
|
|
@ -273,14 +273,14 @@ struct app_builder::imp {
|
|||
return nargs;
|
||||
}
|
||||
|
||||
optional<expr> mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args) {
|
||||
expr mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args) {
|
||||
unsigned nargs = get_nargs(mask_sz, mask);
|
||||
if (key::is_simple(mask, mask + mask_sz)) {
|
||||
return mk_app(c, nargs, args);
|
||||
} else {
|
||||
optional<entry> e = get_entry(c, mask_sz, mask);
|
||||
if (!e)
|
||||
return none_expr();
|
||||
throw app_builder_exception();
|
||||
init_ctx_for(*e);
|
||||
unsigned i = mask_sz;
|
||||
unsigned j = nargs;
|
||||
|
|
@ -291,13 +291,13 @@ struct app_builder::imp {
|
|||
--j;
|
||||
expr const & m = head(it);
|
||||
if (!m_ctx->assign(m, args[j]))
|
||||
return none_expr();
|
||||
throw app_builder_exception();
|
||||
it = tail(it);
|
||||
}
|
||||
}
|
||||
if (!check_all_assigned(*e))
|
||||
return none_expr();
|
||||
return some_expr(m_ctx->instantiate_uvars_mvars(e->m_app));
|
||||
throw app_builder_exception();
|
||||
return m_ctx->instantiate_uvars_mvars(e->m_app);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -308,73 +308,73 @@ struct app_builder::imp {
|
|||
return some_level(sort_level(Type));
|
||||
}
|
||||
|
||||
optional<expr> mk_eq(expr const & a, expr const & b) {
|
||||
expr mk_eq(expr const & a, expr const & b) {
|
||||
expr A = m_ctx->infer(a);
|
||||
auto lvl = get_level(A);
|
||||
if (!lvl)
|
||||
return none_expr();
|
||||
return some_expr(::lean::mk_app(mk_constant(get_eq_name(), {*lvl}), A, a, b));
|
||||
throw app_builder_exception();
|
||||
return ::lean::mk_app(mk_constant(get_eq_name(), {*lvl}), A, a, b);
|
||||
}
|
||||
|
||||
optional<expr> mk_iff(expr const & a, expr const & b) {
|
||||
return some_expr(::lean::mk_app(mk_constant(get_iff_name()), a, b));
|
||||
expr mk_iff(expr const & a, expr const & b) {
|
||||
return ::lean::mk_app(mk_constant(get_iff_name()), a, b);
|
||||
}
|
||||
|
||||
optional<expr> mk_eq_refl(expr const & a) {
|
||||
expr mk_eq_refl(expr const & a) {
|
||||
expr A = m_ctx->infer(a);
|
||||
auto lvl = get_level(A);
|
||||
if (!lvl)
|
||||
return none_expr();
|
||||
return some_expr(::lean::mk_app(mk_constant(get_eq_refl_name(), {*lvl}), A, a));
|
||||
throw app_builder_exception();
|
||||
return ::lean::mk_app(mk_constant(get_eq_refl_name(), {*lvl}), A, a);
|
||||
}
|
||||
|
||||
optional<expr> mk_iff_refl(expr const & a) {
|
||||
return some_expr(::lean::mk_app(mk_constant(get_iff_refl_name()), a));
|
||||
expr mk_iff_refl(expr const & a) {
|
||||
return ::lean::mk_app(mk_constant(get_iff_refl_name()), a);
|
||||
}
|
||||
|
||||
optional<expr> mk_eq_symm(expr const & H) {
|
||||
expr mk_eq_symm(expr const & H) {
|
||||
expr p = m_ctx->whnf(m_ctx->infer(H));
|
||||
expr lhs, rhs;
|
||||
if (!is_eq(p, lhs, rhs))
|
||||
return none_expr();
|
||||
throw app_builder_exception();
|
||||
expr A = m_ctx->infer(lhs);
|
||||
auto lvl = get_level(A);
|
||||
if (!lvl)
|
||||
return none_expr();
|
||||
return some_expr(::lean::mk_app(mk_constant(get_eq_symm_name(), {*lvl}), A, lhs, rhs, H));
|
||||
throw app_builder_exception();
|
||||
return ::lean::mk_app(mk_constant(get_eq_symm_name(), {*lvl}), A, lhs, rhs, H);
|
||||
}
|
||||
|
||||
optional<expr> mk_iff_symm(expr const & H) {
|
||||
expr mk_iff_symm(expr const & H) {
|
||||
expr p = m_ctx->whnf(m_ctx->infer(H));
|
||||
expr lhs, rhs;
|
||||
if (!is_iff(p, lhs, rhs))
|
||||
return none_expr();
|
||||
return some_expr(::lean::mk_app(mk_constant(get_iff_symm_name()), lhs, rhs, H));
|
||||
throw app_builder_exception();
|
||||
return ::lean::mk_app(mk_constant(get_iff_symm_name()), lhs, rhs, H);
|
||||
}
|
||||
|
||||
optional<expr> mk_eq_trans(expr const & H1, expr const & H2) {
|
||||
expr mk_eq_trans(expr const & H1, expr const & H2) {
|
||||
expr p1 = m_ctx->whnf(m_ctx->infer(H1));
|
||||
expr p2 = m_ctx->whnf(m_ctx->infer(H2));
|
||||
expr lhs1, rhs1, lhs2, rhs2;
|
||||
if (!is_eq(p1, lhs1, rhs1) || !is_eq(p2, lhs2, rhs2))
|
||||
return none_expr();
|
||||
throw app_builder_exception();
|
||||
expr A = m_ctx->infer(lhs1);
|
||||
auto lvl = get_level(A);
|
||||
if (!lvl)
|
||||
return none_expr();
|
||||
return some_expr(::lean::mk_app({mk_constant(get_eq_trans_name(), {*lvl}), A, lhs1, rhs1, rhs2, H1, H2}));
|
||||
throw app_builder_exception();
|
||||
return ::lean::mk_app({mk_constant(get_eq_trans_name(), {*lvl}), A, lhs1, rhs1, rhs2, H1, H2});
|
||||
}
|
||||
|
||||
optional<expr> mk_iff_trans(expr const & H1, expr const & H2) {
|
||||
expr mk_iff_trans(expr const & H1, expr const & H2) {
|
||||
expr p1 = m_ctx->whnf(m_ctx->infer(H1));
|
||||
expr p2 = m_ctx->whnf(m_ctx->infer(H2));
|
||||
expr lhs1, rhs1, lhs2, rhs2;
|
||||
if (!is_iff(p1, lhs1, rhs1) || !is_iff(p2, lhs2, rhs2))
|
||||
return none_expr();
|
||||
return some_expr(::lean::mk_app({mk_constant(get_iff_trans_name()), lhs1, rhs1, rhs2, H1, H2}));
|
||||
throw app_builder_exception();
|
||||
return ::lean::mk_app({mk_constant(get_iff_trans_name()), lhs1, rhs1, rhs2, H1, H2});
|
||||
}
|
||||
|
||||
optional<expr> mk_rel(name const & n, expr const & lhs, expr const & rhs) {
|
||||
expr mk_rel(name const & n, expr const & lhs, expr const & rhs) {
|
||||
if (n == get_eq_name()) {
|
||||
return mk_eq(lhs, rhs);
|
||||
} else if (n == get_iff_name()) {
|
||||
|
|
@ -385,7 +385,7 @@ struct app_builder::imp {
|
|||
}
|
||||
}
|
||||
|
||||
optional<expr> mk_refl(name const & relname, expr const & a) {
|
||||
expr mk_refl(name const & relname, expr const & a) {
|
||||
if (relname == get_eq_name()) {
|
||||
return mk_eq_refl(a);
|
||||
} else if (relname == get_iff_name()) {
|
||||
|
|
@ -393,11 +393,11 @@ struct app_builder::imp {
|
|||
} else if (auto info = m_refl_getter(relname)) {
|
||||
return mk_app(info->m_name, 1, &a);
|
||||
} else {
|
||||
return none_expr();
|
||||
throw app_builder_exception();
|
||||
}
|
||||
}
|
||||
|
||||
optional<expr> mk_symm(name const & relname, expr const & H) {
|
||||
expr mk_symm(name const & relname, expr const & H) {
|
||||
if (relname == get_eq_name()) {
|
||||
return mk_eq_symm(H);
|
||||
} else if (relname == get_iff_name()) {
|
||||
|
|
@ -405,11 +405,11 @@ struct app_builder::imp {
|
|||
} else if (auto info = m_symm_getter(relname)) {
|
||||
return mk_app(info->m_name, 1, &H);
|
||||
} else {
|
||||
return none_expr();
|
||||
throw app_builder_exception();
|
||||
}
|
||||
}
|
||||
|
||||
optional<expr> mk_trans(name const & relname, expr const & H1, expr const & H2) {
|
||||
expr mk_trans(name const & relname, expr const & H1, expr const & H2) {
|
||||
if (relname == get_eq_name()) {
|
||||
return mk_eq_trans(H1, H2);
|
||||
} else if (relname == get_iff_name()) {
|
||||
|
|
@ -418,52 +418,52 @@ struct app_builder::imp {
|
|||
expr args[2] = {H1, H2};
|
||||
return mk_app(info->m_name, 2, args);
|
||||
} else {
|
||||
return none_expr();
|
||||
throw app_builder_exception();
|
||||
}
|
||||
}
|
||||
|
||||
optional<expr> mk_eq_rec(expr const & motive, expr const & H1, expr const & H2) {
|
||||
expr mk_eq_rec(expr const & motive, expr const & H1, expr const & H2) {
|
||||
expr p = m_ctx->whnf(m_ctx->infer(H2));
|
||||
expr lhs, rhs;
|
||||
if (!is_eq(p, lhs, rhs))
|
||||
return none_expr();
|
||||
throw app_builder_exception();
|
||||
expr A = m_ctx->infer(lhs);
|
||||
auto A_lvl = get_level(A);
|
||||
expr mtype = m_ctx->whnf(m_ctx->infer(motive));
|
||||
if (!is_pi(mtype) || !is_sort(binding_body(mtype)))
|
||||
return none_expr();
|
||||
throw app_builder_exception();
|
||||
level l_1 = sort_level(binding_body(mtype));
|
||||
name const & eqrec = is_standard(m_ctx->env()) ? get_eq_rec_name() : get_eq_nrec_name();
|
||||
return some_expr(::lean::mk_app({mk_constant(eqrec, {l_1, *A_lvl}), A, lhs, motive, H1, rhs, H2}));
|
||||
return ::lean::mk_app({mk_constant(eqrec, {l_1, *A_lvl}), A, lhs, motive, H1, rhs, H2});
|
||||
}
|
||||
|
||||
optional<expr> mk_eq_drec(expr const & motive, expr const & H1, expr const & H2) {
|
||||
expr mk_eq_drec(expr const & motive, expr const & H1, expr const & H2) {
|
||||
expr p = m_ctx->whnf(m_ctx->infer(H2));
|
||||
expr lhs, rhs;
|
||||
if (!is_eq(p, lhs, rhs))
|
||||
return none_expr();
|
||||
throw app_builder_exception();
|
||||
expr A = m_ctx->infer(lhs);
|
||||
auto A_lvl = get_level(A);
|
||||
expr mtype = m_ctx->whnf(m_ctx->infer(motive));
|
||||
if (!is_pi(mtype) || !is_pi(binding_body(mtype)) || !is_sort(binding_body(binding_body(mtype))))
|
||||
return none_expr();
|
||||
throw app_builder_exception();
|
||||
level l_1 = sort_level(binding_body(binding_body(mtype)));
|
||||
name const & eqrec = is_standard(m_ctx->env()) ? get_eq_drec_name() : get_eq_rec_name();
|
||||
return some_expr(::lean::mk_app({mk_constant(eqrec, {l_1, *A_lvl}), A, lhs, motive, H1, rhs, H2}));
|
||||
return ::lean::mk_app({mk_constant(eqrec, {l_1, *A_lvl}), A, lhs, motive, H1, rhs, H2});
|
||||
}
|
||||
|
||||
optional<expr> mk_congr_arg(expr const & f, expr const & H) {
|
||||
expr mk_congr_arg(expr const & f, expr const & H) {
|
||||
// TODO(Leo): efficient version
|
||||
|
||||
return mk_app(get_congr_arg_name(), {f, H});
|
||||
}
|
||||
|
||||
optional<expr> mk_congr_fun(expr const & H, expr const & a) {
|
||||
expr mk_congr_fun(expr const & H, expr const & a) {
|
||||
// TODO(Leo): efficient version
|
||||
return mk_app(get_congr_fun_name(), {H, a});
|
||||
}
|
||||
|
||||
optional<expr> mk_congr(expr const & H1, expr const & H2) {
|
||||
expr mk_congr(expr const & H1, expr const & H2) {
|
||||
// TODO(Leo): efficient version
|
||||
return mk_app(get_congr_name(), {H1, H2});
|
||||
}
|
||||
|
|
@ -483,83 +483,83 @@ app_builder::app_builder(tmp_type_context & ctx):
|
|||
|
||||
app_builder::~app_builder() {}
|
||||
|
||||
optional<expr> app_builder::mk_app(name const & c, unsigned nargs, expr const * args) {
|
||||
expr app_builder::mk_app(name const & c, unsigned nargs, expr const * args) {
|
||||
return m_ptr->mk_app(c, nargs, args);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args) {
|
||||
expr app_builder::mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args) {
|
||||
return m_ptr->mk_app(c, mask_sz, mask, args);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_rel(name const & n, expr const & lhs, expr const & rhs) {
|
||||
expr app_builder::mk_rel(name const & n, expr const & lhs, expr const & rhs) {
|
||||
return m_ptr->mk_rel(n, lhs, rhs);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_eq(expr const & lhs, expr const & rhs) {
|
||||
expr app_builder::mk_eq(expr const & lhs, expr const & rhs) {
|
||||
return m_ptr->mk_eq(lhs, rhs);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_iff(expr const & lhs, expr const & rhs) {
|
||||
expr app_builder::mk_iff(expr const & lhs, expr const & rhs) {
|
||||
return m_ptr->mk_iff(lhs, rhs);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_refl(name const & relname, expr const & a) {
|
||||
expr app_builder::mk_refl(name const & relname, expr const & a) {
|
||||
return m_ptr->mk_refl(relname, a);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_eq_refl(expr const & a) {
|
||||
expr app_builder::mk_eq_refl(expr const & a) {
|
||||
return m_ptr->mk_eq_refl(a);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_iff_refl(expr const & a) {
|
||||
expr app_builder::mk_iff_refl(expr const & a) {
|
||||
return m_ptr->mk_iff_refl(a);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_symm(name const & relname, expr const & H) {
|
||||
expr app_builder::mk_symm(name const & relname, expr const & H) {
|
||||
return m_ptr->mk_symm(relname, H);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_eq_symm(expr const & H) {
|
||||
expr app_builder::mk_eq_symm(expr const & H) {
|
||||
return m_ptr->mk_eq_symm(H);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_iff_symm(expr const & H) {
|
||||
expr app_builder::mk_iff_symm(expr const & H) {
|
||||
return m_ptr->mk_iff_symm(H);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_trans(name const & relname, expr const & H1, expr const & H2) {
|
||||
expr app_builder::mk_trans(name const & relname, expr const & H1, expr const & H2) {
|
||||
return m_ptr->mk_trans(relname, H1, H2);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_eq_trans(expr const & H1, expr const & H2) {
|
||||
expr app_builder::mk_eq_trans(expr const & H1, expr const & H2) {
|
||||
return m_ptr->mk_eq_trans(H1, H2);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_iff_trans(expr const & H1, expr const & H2) {
|
||||
expr app_builder::mk_iff_trans(expr const & H1, expr const & H2) {
|
||||
return m_ptr->mk_iff_trans(H1, H2);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_eq_rec(expr const & C, expr const & H1, expr const & H2) {
|
||||
expr app_builder::mk_eq_rec(expr const & C, expr const & H1, expr const & H2) {
|
||||
return m_ptr->mk_eq_rec(C, H1, H2);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_eq_drec(expr const & C, expr const & H1, expr const & H2) {
|
||||
expr app_builder::mk_eq_drec(expr const & C, expr const & H1, expr const & H2) {
|
||||
return m_ptr->mk_eq_drec(C, H1, H2);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_congr_arg(expr const & f, expr const & H) {
|
||||
expr app_builder::mk_congr_arg(expr const & f, expr const & H) {
|
||||
return m_ptr->mk_congr_arg(f, H);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_congr_fun(expr const & H, expr const & a) {
|
||||
expr app_builder::mk_congr_fun(expr const & H, expr const & a) {
|
||||
return m_ptr->mk_congr_fun(H, a);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_congr(expr const & H1, expr const & H2) {
|
||||
expr app_builder::mk_congr(expr const & H1, expr const & H2) {
|
||||
return m_ptr->mk_congr(H1, H2);
|
||||
}
|
||||
|
||||
optional<expr> app_builder::mk_sorry(expr const & type) {
|
||||
expr app_builder::mk_sorry(expr const & type) {
|
||||
return mk_app(get_sorry_name(), type);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -12,6 +12,12 @@ Author: Leonardo de Moura
|
|||
#include "library/tmp_type_context.h"
|
||||
|
||||
namespace lean {
|
||||
class app_builder_exception : public exception {
|
||||
public:
|
||||
// We may provide more information in the future.
|
||||
app_builder_exception():exception("app_builder_exception") {}
|
||||
};
|
||||
|
||||
/** \brief Helper for creating simple applications where some arguments are inferred using
|
||||
type inference.
|
||||
|
||||
|
|
@ -38,51 +44,51 @@ public:
|
|||
/** \brief Create an application (d.{_ ... _} _ ... _ args[0] ... args[nargs-1]).
|
||||
The missing arguments and universes levels are inferred using type inference.
|
||||
|
||||
\remark The method returns none_expr if: not all arguments can be inferred;
|
||||
\remark The method throwns an app_builder_exception if: not all arguments can be inferred;
|
||||
or constraints are created during type inference; or an exception is thrown
|
||||
during type inference.
|
||||
|
||||
\remark This methods uses just higher-order pattern matching.
|
||||
*/
|
||||
optional<expr> mk_app(name const & c, unsigned nargs, expr const * args);
|
||||
expr mk_app(name const & c, unsigned nargs, expr const * args);
|
||||
|
||||
optional<expr> mk_app(name const & c, std::initializer_list<expr> const & args) {
|
||||
expr mk_app(name const & c, std::initializer_list<expr> const & args) {
|
||||
return mk_app(c, args.size(), args.begin());
|
||||
}
|
||||
|
||||
optional<expr> mk_app(name const & c, expr const & a1) {
|
||||
expr mk_app(name const & c, expr const & a1) {
|
||||
return mk_app(c, {a1});
|
||||
}
|
||||
|
||||
optional<expr> mk_app(name const & c, expr const & a1, expr const & a2) {
|
||||
expr mk_app(name const & c, expr const & a1, expr const & a2) {
|
||||
return mk_app(c, {a1, a2});
|
||||
}
|
||||
|
||||
optional<expr> mk_app(name const & c, expr const & a1, expr const & a2, expr const & a3) {
|
||||
expr mk_app(name const & c, expr const & a1, expr const & a2, expr const & a3) {
|
||||
return mk_app(c, {a1, a2, a3});
|
||||
}
|
||||
|
||||
optional<expr> mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args);
|
||||
expr mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args);
|
||||
|
||||
/** \brief Similar to mk_app(n, lhs, rhs), but handles eq and iff more efficiently. */
|
||||
optional<expr> mk_rel(name const & n, expr const & lhs, expr const & rhs);
|
||||
optional<expr> mk_eq(expr const & lhs, expr const & rhs);
|
||||
optional<expr> mk_iff(expr const & lhs, expr const & rhs);
|
||||
expr mk_rel(name const & n, expr const & lhs, expr const & rhs);
|
||||
expr mk_eq(expr const & lhs, expr const & rhs);
|
||||
expr mk_iff(expr const & lhs, expr const & rhs);
|
||||
|
||||
/** \brief Similar a reflexivity proof for the given relation */
|
||||
optional<expr> mk_refl(name const & relname, expr const & a);
|
||||
optional<expr> mk_eq_refl(expr const & a);
|
||||
optional<expr> mk_iff_refl(expr const & a);
|
||||
expr mk_refl(name const & relname, expr const & a);
|
||||
expr mk_eq_refl(expr const & a);
|
||||
expr mk_iff_refl(expr const & a);
|
||||
|
||||
/** \brief Similar a symmetry proof for the given relation */
|
||||
optional<expr> mk_symm(name const & relname, expr const & H);
|
||||
optional<expr> mk_eq_symm(expr const & H);
|
||||
optional<expr> mk_iff_symm(expr const & H);
|
||||
expr mk_symm(name const & relname, expr const & H);
|
||||
expr mk_eq_symm(expr const & H);
|
||||
expr mk_iff_symm(expr const & H);
|
||||
|
||||
/** \brief Similar a transitivity proof for the given relation */
|
||||
optional<expr> mk_trans(name const & relname, expr const & H1, expr const & H2);
|
||||
optional<expr> mk_eq_trans(expr const & H1, expr const & H2);
|
||||
optional<expr> mk_iff_trans(expr const & H1, expr const & H2);
|
||||
expr mk_trans(name const & relname, expr const & H1, expr const & H2);
|
||||
expr mk_eq_trans(expr const & H1, expr const & H2);
|
||||
expr mk_iff_trans(expr const & H1, expr const & H2);
|
||||
|
||||
/** \brief Create a (non-dependent) eq.rec application.
|
||||
C is the motive. The expected types for C, H1 and H2 are
|
||||
|
|
@ -93,7 +99,7 @@ public:
|
|||
@eq.rec A a C H1 b H2
|
||||
In the HoTT library, we actually create an eq.nrec application
|
||||
since eq.rec is a dependent eliminator in HoTT. */
|
||||
optional<expr> mk_eq_rec(expr const & C, expr const & H1, expr const & H2);
|
||||
expr mk_eq_rec(expr const & C, expr const & H1, expr const & H2);
|
||||
|
||||
/** \brief Create a (dependent) eq.drec application.
|
||||
C is the motive. The expected types for C, H1 and H2 are
|
||||
|
|
@ -104,14 +110,14 @@ public:
|
|||
@eq.drec A a C H1 b H2
|
||||
In the HoTT library, we actually create an eq.rec application
|
||||
because eq.rec is a dependent eliminator in HoTT. */
|
||||
optional<expr> mk_eq_drec(expr const & C, expr const & H1, expr const & H2);
|
||||
expr mk_eq_drec(expr const & C, expr const & H1, expr const & H2);
|
||||
|
||||
optional<expr> mk_congr_arg(expr const & f, expr const & H);
|
||||
optional<expr> mk_congr_fun(expr const & H, expr const & a);
|
||||
optional<expr> mk_congr(expr const & H1, expr const & H2);
|
||||
expr mk_congr_arg(expr const & f, expr const & H);
|
||||
expr mk_congr_fun(expr const & H, expr const & a);
|
||||
expr mk_congr(expr const & H1, expr const & H2);
|
||||
|
||||
/** \brief Create (@sorry type) */
|
||||
optional<expr> mk_sorry(expr const & type);
|
||||
expr mk_sorry(expr const & type);
|
||||
|
||||
/** \brief Set the local instances. This method is relevant when we want to expose local class instances
|
||||
to the app_builder.
|
||||
|
|
|
|||
|
|
@ -192,17 +192,11 @@ void simplifier::cache_save(expr const & e, result const & r) {
|
|||
|
||||
result simplifier::lift_from_eq(expr const & x, result const & r) {
|
||||
lean_assert(!r.is_none());
|
||||
|
||||
expr l = m_tmp_tctx->mk_tmp_local(m_tmp_tctx->infer(x));
|
||||
auto motive_local = m_app_builder.mk_app(m_rel, x, l);
|
||||
lean_assert(motive_local);
|
||||
|
||||
expr motive = Fun(l, *motive_local);
|
||||
|
||||
auto Rxx = m_app_builder.mk_refl(m_rel, x);
|
||||
lean_assert(Rxx);
|
||||
|
||||
auto pf = m_app_builder.mk_eq_rec(motive, *Rxx, r.get_proof());
|
||||
expr motive_local = m_app_builder.mk_app(m_rel, x, l);
|
||||
expr motive = Fun(l, motive_local);
|
||||
expr Rxx = m_app_builder.mk_refl(m_rel, x);
|
||||
expr pf = m_app_builder.mk_eq_rec(motive, Rxx, r.get_proof());
|
||||
return result(r.get_new(), pf);
|
||||
}
|
||||
|
||||
|
|
@ -213,28 +207,23 @@ result simplifier::join(result const & r1, result const & r2) {
|
|||
} else if (r2.is_none()) {
|
||||
return r1;
|
||||
} else {
|
||||
auto trans = m_app_builder.mk_trans(m_rel, r1.get_proof(), r2.get_proof());
|
||||
lean_assert(trans);
|
||||
return result(r2.get_new(), *trans);
|
||||
expr trans = m_app_builder.mk_trans(m_rel, r1.get_proof(), r2.get_proof());
|
||||
return result(r2.get_new(), trans);
|
||||
}
|
||||
}
|
||||
|
||||
result simplifier::funext(result const & r, expr const & l) {
|
||||
// theorem funext {f₁ f₂ : Πx : A, B x} : (∀x, f₁ x = f₂ x) → f₁ = f₂ :=
|
||||
lean_assert(!r.is_none());
|
||||
expr e = Fun(l, r.get_new());
|
||||
if (auto pf = m_app_builder.mk_app(get_funext_name(), Fun(l, r.get_proof())))
|
||||
return result(e, *pf);
|
||||
else
|
||||
throw blast_exception("failed on [funext] matching", e);
|
||||
expr e = Fun(l, r.get_new());
|
||||
expr pf = m_app_builder.mk_app(get_funext_name(), Fun(l, r.get_proof()));
|
||||
return result(e, pf);
|
||||
}
|
||||
|
||||
result simplifier::finalize(result const & r) {
|
||||
if (!r.is_none()) return r;
|
||||
if (auto pf = m_app_builder.mk_refl(m_rel, r.get_new()))
|
||||
return result(r.get_new(), *pf);
|
||||
else
|
||||
throw blast_exception("failed on [refl] matching", r.get_new());
|
||||
expr pf = m_app_builder.mk_refl(m_rel, r.get_new());
|
||||
return result(r.get_new(), pf);
|
||||
}
|
||||
|
||||
/* Simplification */
|
||||
|
|
@ -477,9 +466,8 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
|
|||
flet<name> set_name(m_rel, get_iff_name());
|
||||
result r_cond = simplify(m_type);
|
||||
if (is_constant(r_cond.get_new()) && const_name(r_cond.get_new()) == get_true_name()) {
|
||||
auto pf = m_app_builder.mk_app(name("iff", "elim_right"), finalize(r_cond).get_proof(), mk_constant(get_true_intro_name()));
|
||||
lean_assert(pf);
|
||||
bool success = tmp_tctx->is_def_eq(m, *pf);
|
||||
expr pf = m_app_builder.mk_app(name("iff", "elim_right"), finalize(r_cond).get_proof(), mk_constant(get_true_intro_name()));
|
||||
bool success = tmp_tctx->is_def_eq(m, pf);
|
||||
lean_assert(success);
|
||||
continue;
|
||||
}
|
||||
|
|
@ -516,31 +504,25 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
|
|||
result simplifier::congr(result const & r_f, result const & r_arg) {
|
||||
lean_assert(!r_f.is_none() && !r_arg.is_none());
|
||||
// theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂
|
||||
expr e = mk_app(r_f.get_new(), r_arg.get_new());
|
||||
if (auto pf = m_app_builder.mk_app(get_congr_name(), r_f.get_proof(), r_arg.get_proof()))
|
||||
return result(e, *pf);
|
||||
else
|
||||
throw blast_exception("failed on [congr] matching", e);
|
||||
expr e = mk_app(r_f.get_new(), r_arg.get_new());
|
||||
expr pf = m_app_builder.mk_app(get_congr_name(), r_f.get_proof(), r_arg.get_proof());
|
||||
return result(e, pf);
|
||||
}
|
||||
|
||||
result simplifier::congr_fun(result const & r_f, expr const & arg) {
|
||||
lean_assert(!r_f.is_none());
|
||||
// theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a
|
||||
expr e = mk_app(r_f.get_new(), arg);
|
||||
if (auto pf = m_app_builder.mk_app(get_congr_fun_name(), r_f.get_proof(), arg))
|
||||
return result(e, *pf);
|
||||
else
|
||||
throw blast_exception("failed on [congr_fun] matching", e);
|
||||
expr e = mk_app(r_f.get_new(), arg);
|
||||
expr pf = m_app_builder.mk_app(get_congr_fun_name(), r_f.get_proof(), arg);
|
||||
return result(e, pf);
|
||||
}
|
||||
|
||||
result simplifier::congr_arg(expr const & f, result const & r_arg) {
|
||||
lean_assert(!r_arg.is_none());
|
||||
// theorem congr_arg {A B : Type} {a₁ a₂ : A} (f : A → B) : a₁ = a₂ → f a₁ = f a₂
|
||||
expr e = mk_app(f, r_arg.get_new());
|
||||
if (auto pf = m_app_builder.mk_app(get_congr_arg_name(), f, r_arg.get_proof()))
|
||||
return result(e, *pf);
|
||||
else
|
||||
throw blast_exception("failed on [congr_arg] matching", e);
|
||||
expr e = mk_app(f, r_arg.get_new());
|
||||
expr pf = m_app_builder.mk_app(get_congr_arg_name(), f, r_arg.get_proof());
|
||||
return result(e, pf);
|
||||
}
|
||||
|
||||
result simplifier::congr_funs(result const & r_f, buffer<expr> const & args) {
|
||||
|
|
@ -549,10 +531,8 @@ result simplifier::congr_funs(result const & r_f, buffer<expr> const & args) {
|
|||
expr e = r_f.get_new();
|
||||
expr pf = r_f.get_proof();
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
e = mk_app(e, args[i]);
|
||||
auto p = m_app_builder.mk_app(get_congr_fun_name(), pf, args[i]);
|
||||
if (p) pf = *p;
|
||||
else throw blast_exception("failed on [congr_fun] matching", e);
|
||||
e = mk_app(e, args[i]);
|
||||
pf = m_app_builder.mk_app(get_congr_fun_name(), pf, args[i]);
|
||||
}
|
||||
return result(e, pf);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -43,9 +43,9 @@ class congr_lemma_manager::imp {
|
|||
/** \brief (Try to) cast expression \c e to the given type using the equations \c eqs.
|
||||
\c deps contains the indices of the relevant equalities.
|
||||
\remark deps is sorted. */
|
||||
optional<expr> cast(expr const & e, expr const & type, list<unsigned> const & deps, buffer<optional<expr>> const & eqs) {
|
||||
expr cast(expr const & e, expr const & type, list<unsigned> const & deps, buffer<optional<expr>> const & eqs) {
|
||||
if (!deps)
|
||||
return some_expr(e);
|
||||
return e;
|
||||
unsigned d = head(deps);
|
||||
auto major = eqs[d];
|
||||
if (!major) {
|
||||
|
|
@ -65,10 +65,8 @@ class congr_lemma_manager::imp {
|
|||
motive = Fun(rhs, Fun(*major, type));
|
||||
// We compute new_type by replacing rhs with lhs and *major with eq.refl(lhs) in type.
|
||||
new_type = instantiate(abstract_local(type, rhs), lhs);
|
||||
auto refl = m_builder.mk_eq_refl(lhs);
|
||||
if (!refl)
|
||||
return none_expr();
|
||||
new_type = instantiate(abstract_local(new_type, *major), *refl);
|
||||
expr refl = m_builder.mk_eq_refl(lhs);
|
||||
new_type = instantiate(abstract_local(new_type, *major), refl);
|
||||
} else {
|
||||
// type does not depend on the *major.
|
||||
// So, the motive is just (fun rhs, type), and
|
||||
|
|
@ -77,13 +75,11 @@ class congr_lemma_manager::imp {
|
|||
motive = Fun(rhs, type);
|
||||
new_type = instantiate(abstract_local(type, rhs), lhs);
|
||||
}
|
||||
auto minor = cast(e, new_type, tail(deps), eqs);
|
||||
if (!minor)
|
||||
return none_expr();
|
||||
expr minor = cast(e, new_type, tail(deps), eqs);
|
||||
if (use_drec) {
|
||||
return m_builder.mk_eq_drec(motive, *minor, *major);
|
||||
return m_builder.mk_eq_drec(motive, minor, *major);
|
||||
} else {
|
||||
return m_builder.mk_eq_rec(motive, *minor, *major);
|
||||
return m_builder.mk_eq_rec(motive, minor, *major);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -92,8 +88,8 @@ class congr_lemma_manager::imp {
|
|||
return std::find(kinds.begin(), kinds.end(), congr_arg_kind::Cast) != kinds.end();
|
||||
}
|
||||
|
||||
optional<expr> mk_simple_congr_proof(expr const & fn, buffer<expr> const & lhss,
|
||||
buffer<optional<expr>> const & eqs, buffer<congr_arg_kind> const & kinds) {
|
||||
expr mk_simple_congr_proof(expr const & fn, buffer<expr> const & lhss,
|
||||
buffer<optional<expr>> const & eqs, buffer<congr_arg_kind> const & kinds) {
|
||||
unsigned i = 0;
|
||||
for (; i < kinds.size(); i++) {
|
||||
if (kinds[i] != congr_arg_kind::Fixed)
|
||||
|
|
@ -104,22 +100,20 @@ class congr_lemma_manager::imp {
|
|||
return m_builder.mk_eq_refl(g);
|
||||
lean_assert(kinds[i] == congr_arg_kind::Eq);
|
||||
lean_assert(eqs[i]);
|
||||
optional<expr> pr = m_builder.mk_congr_arg(g, *eqs[i]);
|
||||
if (!pr) return none_expr();
|
||||
expr pr = m_builder.mk_congr_arg(g, *eqs[i]);
|
||||
i++;
|
||||
for (; i < kinds.size(); i++) {
|
||||
if (kinds[i] == congr_arg_kind::Eq) {
|
||||
pr = m_builder.mk_congr(*pr, *eqs[i]);
|
||||
pr = m_builder.mk_congr(pr, *eqs[i]);
|
||||
} else {
|
||||
lean_assert(kinds[i] == congr_arg_kind::Fixed);
|
||||
pr = m_builder.mk_congr_fun(*pr, lhss[i]);
|
||||
pr = m_builder.mk_congr_fun(pr, lhss[i]);
|
||||
}
|
||||
if (!pr) return none_expr();
|
||||
}
|
||||
return pr;
|
||||
}
|
||||
|
||||
optional<expr> mk_congr_proof(unsigned i, expr const & lhs, expr const & rhs, buffer<optional<expr>> const & eqs) {
|
||||
expr mk_congr_proof(unsigned i, expr const & lhs, expr const & rhs, buffer<optional<expr>> const & eqs) {
|
||||
if (i == eqs.size()) {
|
||||
return m_builder.mk_eq_refl(rhs);
|
||||
} else if (!eqs[i]) {
|
||||
|
|
@ -130,81 +124,72 @@ class congr_lemma_manager::imp {
|
|||
lean_verify(is_eq(mlocal_type(major), x_1, x_2));
|
||||
lean_assert(is_local(x_1));
|
||||
lean_assert(is_local(x_2));
|
||||
auto motive_eq = m_builder.mk_eq(lhs, rhs);
|
||||
if (!motive_eq) return none_expr();
|
||||
expr motive = Fun(x_2, Fun(major, *motive_eq));
|
||||
expr motive_eq = m_builder.mk_eq(lhs, rhs);
|
||||
expr motive = Fun(x_2, Fun(major, motive_eq));
|
||||
// We compute the new_rhs by replacing x_2 with x_1 and major with (eq.refl x_1) in rhs.
|
||||
expr new_rhs = instantiate(abstract_local(rhs, x_2), x_1);
|
||||
auto x1_refl = m_builder.mk_eq_refl(x_1);
|
||||
if (!x1_refl) return none_expr();
|
||||
new_rhs = instantiate(abstract_local(new_rhs, major), *x1_refl);
|
||||
auto minor = mk_congr_proof(i+1, lhs, new_rhs, eqs);
|
||||
if (!minor) return none_expr();
|
||||
return m_builder.mk_eq_drec(motive, *minor, major);
|
||||
expr x1_refl = m_builder.mk_eq_refl(x_1);
|
||||
new_rhs = instantiate(abstract_local(new_rhs, major), x1_refl);
|
||||
expr minor = mk_congr_proof(i+1, lhs, new_rhs, eqs);
|
||||
return m_builder.mk_eq_drec(motive, minor, major);
|
||||
}
|
||||
}
|
||||
|
||||
optional<result> mk_congr_simp(expr const & fn, buffer<param_info> const & pinfos, buffer<congr_arg_kind> const & kinds) {
|
||||
expr fn_type = whnf(infer(fn));
|
||||
name e_name("e");
|
||||
buffer<expr> lhss;
|
||||
buffer<expr> rhss; // it contains the right-hand-side argument
|
||||
buffer<optional<expr>> eqs; // for Eq args, it contains the equality
|
||||
buffer<expr> hyps; // contains lhss + rhss + eqs
|
||||
for (unsigned i = 0; i < pinfos.size(); i++) {
|
||||
if (!is_pi(fn_type)) {
|
||||
return optional<result>();
|
||||
}
|
||||
expr lhs = m_ctx.mk_tmp_local(binding_name(fn_type), binding_domain(fn_type));
|
||||
lhss.push_back(lhs);
|
||||
hyps.push_back(lhs);
|
||||
switch (kinds[i]) {
|
||||
case congr_arg_kind::Eq: {
|
||||
expr rhs = m_ctx.mk_tmp_local(binding_name(fn_type), binding_domain(fn_type));
|
||||
expr eq_type;
|
||||
if (auto it = m_builder.mk_eq(lhs, rhs))
|
||||
eq_type = *it;
|
||||
else
|
||||
return optional<result>();
|
||||
rhss.push_back(rhs);
|
||||
expr eq = m_ctx.mk_tmp_local(e_name.append_after(eqs.size()+1), eq_type);
|
||||
eqs.push_back(some_expr(eq));
|
||||
hyps.push_back(rhs);
|
||||
hyps.push_back(eq);
|
||||
break;
|
||||
}
|
||||
case congr_arg_kind::Fixed:
|
||||
rhss.push_back(lhs);
|
||||
eqs.push_back(none_expr());
|
||||
break;
|
||||
case congr_arg_kind::Cast: {
|
||||
expr rhs_type = mlocal_type(lhs);
|
||||
rhs_type = instantiate_rev(abstract_locals(rhs_type, lhss.size()-1, lhss.data()), rhss.size(), rhss.data());
|
||||
auto rhs = cast(lhs, rhs_type, pinfos[i].get_dependencies(), eqs);
|
||||
if (!rhs) {
|
||||
try {
|
||||
expr fn_type = whnf(infer(fn));
|
||||
name e_name("e");
|
||||
buffer<expr> lhss;
|
||||
buffer<expr> rhss; // it contains the right-hand-side argument
|
||||
buffer<optional<expr>> eqs; // for Eq args, it contains the equality
|
||||
buffer<expr> hyps; // contains lhss + rhss + eqs
|
||||
for (unsigned i = 0; i < pinfos.size(); i++) {
|
||||
if (!is_pi(fn_type)) {
|
||||
return optional<result>();
|
||||
}
|
||||
rhss.push_back(*rhs);
|
||||
eqs.push_back(none_expr());
|
||||
break;
|
||||
}}
|
||||
fn_type = whnf(instantiate(binding_body(fn_type), lhs));
|
||||
}
|
||||
expr lhs = mk_app(fn, lhss);
|
||||
expr rhs = mk_app(fn, rhss);
|
||||
auto eq = m_builder.mk_eq(lhs, rhs);
|
||||
if (!eq)
|
||||
expr lhs = m_ctx.mk_tmp_local(binding_name(fn_type), binding_domain(fn_type));
|
||||
lhss.push_back(lhs);
|
||||
hyps.push_back(lhs);
|
||||
switch (kinds[i]) {
|
||||
case congr_arg_kind::Eq: {
|
||||
expr rhs = m_ctx.mk_tmp_local(binding_name(fn_type), binding_domain(fn_type));
|
||||
expr eq_type = m_builder.mk_eq(lhs, rhs);
|
||||
rhss.push_back(rhs);
|
||||
expr eq = m_ctx.mk_tmp_local(e_name.append_after(eqs.size()+1), eq_type);
|
||||
eqs.push_back(some_expr(eq));
|
||||
hyps.push_back(rhs);
|
||||
hyps.push_back(eq);
|
||||
break;
|
||||
}
|
||||
case congr_arg_kind::Fixed:
|
||||
rhss.push_back(lhs);
|
||||
eqs.push_back(none_expr());
|
||||
break;
|
||||
case congr_arg_kind::Cast: {
|
||||
expr rhs_type = mlocal_type(lhs);
|
||||
rhs_type = instantiate_rev(abstract_locals(rhs_type, lhss.size()-1, lhss.data()), rhss.size(), rhss.data());
|
||||
expr rhs = cast(lhs, rhs_type, pinfos[i].get_dependencies(), eqs);
|
||||
rhss.push_back(rhs);
|
||||
eqs.push_back(none_expr());
|
||||
break;
|
||||
}}
|
||||
fn_type = whnf(instantiate(binding_body(fn_type), lhs));
|
||||
}
|
||||
expr lhs = mk_app(fn, lhss);
|
||||
expr rhs = mk_app(fn, rhss);
|
||||
expr eq = m_builder.mk_eq(lhs, rhs);
|
||||
expr congr_type = Pi(hyps, eq);
|
||||
expr congr_proof;
|
||||
if (has_cast(kinds)) {
|
||||
congr_proof = mk_congr_proof(0, lhs, rhs, eqs);
|
||||
} else {
|
||||
congr_proof = mk_simple_congr_proof(fn, lhss, eqs, kinds);
|
||||
}
|
||||
congr_proof = Fun(hyps, congr_proof);
|
||||
return optional<result>(congr_type, congr_proof, to_list(kinds));
|
||||
} catch (app_builder_exception &) {
|
||||
return optional<result>();
|
||||
expr congr_type = Pi(hyps, *eq);
|
||||
optional<expr> congr_proof;
|
||||
if (has_cast(kinds)) {
|
||||
congr_proof = mk_congr_proof(0, lhs, rhs, eqs);
|
||||
} else {
|
||||
congr_proof = mk_simple_congr_proof(fn, lhss, eqs, kinds);
|
||||
}
|
||||
if (!congr_proof) return optional<result>();
|
||||
congr_proof = Fun(hyps, *congr_proof);
|
||||
return optional<result>(congr_type, *congr_proof, to_list(kinds));
|
||||
}
|
||||
|
||||
public:
|
||||
|
|
|
|||
Loading…
Reference in a new issue