max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/rfl_lemmas): move rfl lemma rewrite procedure to library

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-12 12:42:14 -07:00
parent af78fd0a3c
commit d980aa3724
3 changed files with 65 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
src/library/rfl_lemmas.cpp
View file

@ -191,8 +191,67 @@ format pp_rfl_lemmas(rfl_lemmas const & lemmas, formatter const & fmt) {
return r;
}
static bool instantiate_emetas(type_context & ctx, list<expr> const & _emetas, list<bool> const & _instances) {
buffer<expr> emetas;
buffer<bool> instances;
to_buffer(_emetas, emetas);
to_buffer(_instances, instances);
lean_assert(emetas.size() == instances.size());
for (unsigned i = 0; i < emetas.size(); ++i) {
expr m = emetas[i];
unsigned mvar_idx = emetas.size() - 1 - i;
expr m_type = ctx.instantiate_mvars(ctx.infer(m));
lean_assert(!has_metavar(m_type));
if (ctx.get_tmp_mvar_assignment(mvar_idx)) continue;
if (instances[i]) {
if (auto v = ctx.mk_class_instance(m_type)) {
if (!ctx.is_def_eq(m, *v)) {
lean_trace(name({"rfl_lemma", "failure"}),
tout() << "unable to assign instance for: " << m_type << "\n";);
return false;
} else {
lean_assert(ctx.get_tmp_mvar_assignment(mvar_idx));
continue;
}
} else {
lean_trace(name({"rfl_lemma", "failure"}),
tout() << "unable to synthesize instance for: " << m_type << "\n";);
return false;
}
} else {
lean_trace(name({"rfl_lemma", "failure"}),
tout() << "failed to assign: " << m << " : " << m_type << "\n";);
return false;
}
}
return true;
}
expr rfl_lemma_rewrite(type_context & ctx, expr const & e, rfl_lemma const & sl) {
type_context::tmp_mode_scope scope(ctx, sl.get_num_umeta(), sl.get_num_emeta());
if (!ctx.is_def_eq(e, sl.get_lhs())) return e;
lean_trace("rfl_lemma",
expr new_lhs = ctx.instantiate_mvars(sl.get_lhs());
expr new_rhs = ctx.instantiate_mvars(sl.get_rhs());
tout() << "(" << sl.get_id() << ") "
<< "[" << new_lhs << " --> " << new_rhs << "]\n";);
if (!instantiate_emetas(ctx, sl.get_emetas(), sl.get_instances())) return e;
for (unsigned i = 0; i < sl.get_num_umeta(); i++) {
if (!ctx.get_tmp_uvar_assignment(i)) return e;
}
return ctx.instantiate_mvars(sl.get_rhs());
}
void initialize_rfl_lemmas() {
register_trace_class("rfl_lemmas_cache");
register_trace_class("rfl_lemma");
register_trace_class(name{"rfl_lemma", "failure"});
g_rfl_lemmas_attributes = new std::vector<name>();
g_default_token = register_defeq_simp_attribute("defeq");
}

5
src/library/rfl_lemmas.h
View file

@ -59,6 +59,11 @@ rfl_lemmas_ptr get_rfl_lemmas(environment const & env, rfl_lemmas_token token);
format pp_rfl_lemmas(rfl_lemmas const & lemmas, formatter const & fmt);
class type_context;
/** \brief (Try to) apply the given rfl_lemma to `e` */
expr rfl_lemma_rewrite(type_context & ctx, expr const & e, rfl_lemma const & sl);
void initialize_rfl_lemmas();
void finalize_rfl_lemmas();
}

57
src/library/tactic/defeq_simplifier.cpp
View file

@ -259,60 +259,7 @@ class defeq_simplify_fn {
}
expr rewrite(expr const & e, rfl_lemma const & sl) {
type_context::tmp_mode_scope scope(m_ctx, sl.get_num_umeta(), sl.get_num_emeta());
if (!m_ctx.is_def_eq(e, sl.get_lhs())) return e;
lean_trace(name({"defeq_simplifier", "rewrite"}),
expr new_lhs = m_ctx.instantiate_mvars(sl.get_lhs());
expr new_rhs = m_ctx.instantiate_mvars(sl.get_rhs());
tout() << "(" << sl.get_id() << ") "
<< "[" << new_lhs << " --> " << new_rhs << "]\n";);
if (!instantiate_emetas(sl.get_emetas(), sl.get_instances())) return e;
for (unsigned i = 0; i < sl.get_num_umeta(); i++) {
if (!m_ctx.get_tmp_uvar_assignment(i)) return e;
}
return m_ctx.instantiate_mvars(sl.get_rhs());
}
bool instantiate_emetas(list<expr> const & _emetas, list<bool> const & _instances) {
buffer<expr> emetas;
buffer<bool> instances;
to_buffer(_emetas, emetas);
to_buffer(_instances, instances);
lean_assert(emetas.size() == instances.size());
for (unsigned i = 0; i < emetas.size(); ++i) {
expr m = emetas[i];
unsigned mvar_idx = emetas.size() - 1 - i;
expr m_type = m_ctx.instantiate_mvars(m_ctx.infer(m));
lean_assert(!has_metavar(m_type));
if (m_ctx.get_tmp_mvar_assignment(mvar_idx)) continue;
if (instances[i]) {
if (auto v = m_ctx.mk_class_instance(m_type)) {
if (!m_ctx.is_def_eq(m, *v)) {
lean_trace(name({"defeq_simplifier", "failure"}),
tout() << "unable to assign instance for: " << m_type << "\n";);
return false;
} else {
lean_assert(m_ctx.get_tmp_mvar_assignment(mvar_idx));
continue;
}
} else {
lean_trace(name({"defeq_simplifier", "failure"}),
tout() << "unable to synthesize instance for: " << m_type << "\n";);
return false;
}
} else {
lean_trace(name({"defeq_simplifier", "failure"}),
tout() << "failed to assign: " << m << " : " << m_type << "\n";);
return false;
}
}
return true;
return rfl_lemma_rewrite(m_ctx, e, sl);
}
expr whnf_eta(expr const & e) {
@ -370,8 +317,6 @@ void initialize_defeq_simplifier() {
DECLARE_VM_BUILTIN(name({"tactic", "defeq_simp_core"}), tactic_defeq_simp);
register_trace_class("defeq_simplifier");
register_trace_class(name({"defeq_simplifier", "rewrite"}));
register_trace_class(name({"defeq_simplifier", "failure"}));
register_trace_class(name({"defeq_simplifier", "canonize"}));
g_simplify_max_simp_rounds = new name{"defeq_simplify", "max_simp_rounds"};