michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/builtin_cmds): display congr lemma arg mask

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-07 12:55:50 -08:00
parent df94864809
commit 3dc8f72c32
2 changed files with 13 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/frontends/lean/builtin_cmds.cpp
View file

@ -1291,7 +1291,19 @@ static environment congr_lemma_cmd(parser & p) {
auto r = cm.mk_congr_simp(e); auto r = cm.mk_congr_simp(e);
if (!r) if (!r)
throw parser_error("failed to generated congruence lemma", pos); throw parser_error("failed to generated congruence lemma", pos);
p.regular_stream() << r->get_proof() << "\n:\n" << r->get_type() << "\n";; auto out = p.regular_stream();
out << "[";
bool first = true;
for (auto k : r->get_arg_kinds()) {
if (!first) out << ", "; else first = false;
switch (k) {
case congr_lemma_manager::congr_arg_kind::Fixed: out << "fixed"; break;
case congr_lemma_manager::congr_arg_kind::Eq: out << "eq"; break;
case congr_lemma_manager::congr_arg_kind::Cast: out << "cast"; break;
}
}
out << "]\n";
out << r->get_proof() << "\n:\n" << r->get_type() << "\n";;
type_checker tc(env); type_checker tc(env);
expr type = tc.check(r->get_proof(), ls).first; expr type = tc.check(r->get_proof(), ls).first;
if (!tc.is_def_eq(type, r->get_type()).first) if (!tc.is_def_eq(type, r->get_type()).first)

6
src/library/congr_lemma_manager.cpp
View file

@ -95,10 +95,6 @@ class congr_lemma_manager::imp {
} }
optional<result> mk_congr_simp(expr const & fn, buffer<param_info> const & pinfos, buffer<congr_arg_kind> const & kinds) { optional<result> mk_congr_simp(expr const & fn, buffer<param_info> const & pinfos, buffer<congr_arg_kind> const & kinds) {
for (unsigned i = 0; i < kinds.size(); i++)
std::cout << (unsigned)kinds[i] << " ";
std::cout << "\n";
expr fn_type = whnf(infer(fn)); expr fn_type = whnf(infer(fn));
name e_name("e"); name e_name("e");
buffer<expr> lhss; buffer<expr> lhss;
@ -142,8 +138,6 @@ class congr_lemma_manager::imp {
eqs.push_back(none_expr()); eqs.push_back(none_expr());
break; break;
}} }}
// std::cout << lhss.back() << "\n";
// std::cout << rhss.back() << "\n\n";
fn_type = whnf(instantiate(binding_body(fn_type), lhs)); fn_type = whnf(instantiate(binding_body(fn_type), lhs));
} }
expr lhs = mk_app(fn, lhss); expr lhs = mk_app(fn, lhss);