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

refactor(frontends/lean/tactic_hint): simplify tactic_hints

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-07 11:34:58 -07:00
parent 90ece4dd1b
commit 531de7990d
3 changed files with 19 additions and 51 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/frontends/lean/elaborator.cpp
View file

@ -939,10 +939,12 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
try_using(subst, mvar, ps, *local_hint, show_failure); try_using(subst, mvar, ps, *local_hint, show_failure);
} else { } else {
// using tactic_hints // using tactic_hints
for (tactic_hint_entry const & tentry : get_tactic_hints(env())) { for (expr const & pre_tac : get_tactic_hints(env())) {
bool show_failure = false; if (auto tac = pre_tactic_to_tactic(pre_tac, mvar)) {
if (try_using(subst, mvar, ps, tentry.get_tactic(), show_failure)) bool show_failure = false;
return; if (try_using(subst, mvar, ps, *tac, show_failure))
return;
}
} }
} }
} }

46
src/frontends/lean/tactic_hint.cpp
View file

@ -10,7 +10,6 @@ Author: Leonardo de Moura
#include "library/scoped_ext.h" #include "library/scoped_ext.h"
#include "library/kernel_serializer.h" #include "library/kernel_serializer.h"
#include "library/tactic/tactic.h" #include "library/tactic/tactic.h"
#include "library/tactic/expr_to_tactic.h"
#include "frontends/lean/tactic_hint.h" #include "frontends/lean/tactic_hint.h"
#include "frontends/lean/cmd_table.h" #include "frontends/lean/cmd_table.h"
#include "frontends/lean/parser.h" #include "frontends/lean/parser.h"
@ -18,37 +17,17 @@ Author: Leonardo de Moura
#include "frontends/lean/tokens.h" #include "frontends/lean/tokens.h"
namespace lean { namespace lean {
typedef list<tactic_hint_entry> tactic_hint_entries; typedef list<expr> tactic_hints;
struct tactic_hint_state {
tactic_hint_entries m_tactics;
};
static name * g_class_name = nullptr; static name * g_class_name = nullptr;
static std::string * g_key = nullptr; static std::string * g_key = nullptr;
struct tactic_hint_config { struct tactic_hint_config {
typedef tactic_hint_state state; typedef tactic_hints state;
typedef tactic_hint_entry entry; typedef expr entry;
typedef tactic_hint_entries entries;
static entries add(entries const & l, entry const & e) { static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
return cons(e, filter(l, [&](entry const & e1) { return e1.m_pre_tactic != e.m_pre_tactic; })); s = cons(e, filter(s, [&](expr const & e1) { return e1 != e; }));
}
static void add_entry_core(state & s, entry const & e) {
s.m_tactics = add(s.m_tactics, e);
}
static void add_entry(environment const & env, io_state const &, state & s, entry const & e) {
if (!e.m_compiled) {
entry new_e(e);
new_e.m_tactic = expr_to_tactic(env, e.m_pre_tactic, nullptr);
new_e.m_compiled = true;
add_entry_core(s, new_e);
} else {
add_entry_core(s, e);
}
} }
static name const & get_class_name() { static name const & get_class_name() {
@ -60,16 +39,17 @@ struct tactic_hint_config {
} }
static void write_entry(serializer & s, entry const & e) { static void write_entry(serializer & s, entry const & e) {
s << e.m_pre_tactic; s << e;
} }
static entry read_entry(deserializer & d) { static entry read_entry(deserializer & d) {
entry e; entry e;
d >> e.m_pre_tactic; d >> e;
return e; return e;
} }
static optional<unsigned> get_fingerprint(entry const & e) { static optional<unsigned> get_fingerprint(entry const & e) {
return some(e.m_pre_tactic.hash()); return some(e.hash());
} }
}; };
@ -88,9 +68,8 @@ void finalize_tactic_hint() {
delete g_class_name; delete g_class_name;
} }
list<tactic_hint_entry> get_tactic_hints(environment const & env) { list<expr> const & get_tactic_hints(environment const & env) {
tactic_hint_state const & s = tactic_hint_ext::get_state(env); return tactic_hint_ext::get_state(env);
return s.m_tactics;
} }
expr parse_tactic_name(parser & p) { expr parse_tactic_name(parser & p) {
@ -108,8 +87,7 @@ expr parse_tactic_name(parser & p) {
environment tactic_hint_cmd(parser & p) { environment tactic_hint_cmd(parser & p) {
expr pre_tac = parse_tactic_name(p); expr pre_tac = parse_tactic_name(p);
tactic tac = expr_to_tactic(p.env(), pre_tac, nullptr); return tactic_hint_ext::add_entry(p.env(), get_dummy_ios(), pre_tac);
return tactic_hint_ext::add_entry(p.env(), get_dummy_ios(), tactic_hint_entry(pre_tac, tac));
} }
void register_tactic_hint_cmd(cmd_table & r) { void register_tactic_hint_cmd(cmd_table & r) {

14
src/frontends/lean/tactic_hint.h
View file

@ -9,19 +9,7 @@ Author: Leonardo de Moura
#include "frontends/lean/cmd_table.h" #include "frontends/lean/cmd_table.h"
namespace lean { namespace lean {
class tactic_hint_entry { list<expr> const & get_tactic_hints(environment const & env);
friend struct tactic_hint_config;
expr m_pre_tactic;
tactic m_tactic;
bool m_compiled;
public:
tactic_hint_entry():m_compiled(false) {}
tactic_hint_entry(expr const & pre_tac, tactic const & tac):
m_pre_tactic(pre_tac), m_tactic(tac), m_compiled(true) {}
expr const & get_pre_tactic() const { return m_pre_tactic; }
tactic const & get_tactic() const { return m_tactic; }
};
list<tactic_hint_entry> get_tactic_hints(environment const & env);
class parser; class parser;
expr parse_tactic_name(parser & p); expr parse_tactic_name(parser & p);
void register_tactic_hint_cmd(cmd_table & r); void register_tactic_hint_cmd(cmd_table & r);