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

feat(library/blast/grinder): add tracing for suspicious event

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-08 15:53:43 -08:00
parent 81b093271d
commit f0c42defc8
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/blast/grinder/intro_elim_lemmas.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include "util/sstream.h" #include "util/sstream.h"
#include "util/priority_queue.h" #include "util/priority_queue.h"
#include "kernel/instantiate.h" #include "kernel/instantiate.h"
#include "library/trace.h"
#include "library/scoped_ext.h" #include "library/scoped_ext.h"
#include "library/user_recursors.h" #include "library/user_recursors.h"
#include "library/tmp_type_context.h" #include "library/tmp_type_context.h"
@ -134,7 +135,8 @@ head_map<gexpr> mk_intro_lemma_index() {
ctx->clear(); ctx->clear();
optional<name> target = get_intro_target(*ctx, lemmas[i]); optional<name> target = get_intro_target(*ctx, lemmas[i]);
if (!target) { if (!target) {
// TODO(Leo): generate event lean_trace(name({"blast", "event"}),
tout() << "discarding [intro] lemma '" << lemmas[i] << "', failed to find target type\n";);
} else { } else {
r.insert(head_index(*target), gexpr(lemmas[i])); r.insert(head_index(*target), gexpr(lemmas[i]));
} }
@ -151,7 +153,8 @@ name_map<name> mk_elim_lemma_index() {
recursor_info info = get_recursor_info(env(), lemma); recursor_info info = get_recursor_info(env(), lemma);
r.insert(info.get_type_name(), lemma); r.insert(info.get_type_name(), lemma);
} catch (exception &) { } catch (exception &) {
// TODO(Leo): generate event lean_trace(name({"blast", "event"}),
tout() << "discarding [elim] lemma '" << lemma << "', failed to compute recursor information\n";);
} }
} }
return r; return r;