118 lines
3.8 KiB
C++
118 lines
3.8 KiB
C++
/*
|
|
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
*/
|
|
#include <string>
|
|
#include "util/sstream.h"
|
|
#include "kernel/type_checker.h"
|
|
#include "library/scoped_ext.h"
|
|
#include "library/kernel_serializer.h"
|
|
#include "library/tactic/tactic.h"
|
|
#include "library/tactic/expr_to_tactic.h"
|
|
#include "frontends/lean/tactic_hint.h"
|
|
#include "frontends/lean/cmd_table.h"
|
|
#include "frontends/lean/parser.h"
|
|
#include "frontends/lean/class.h"
|
|
|
|
namespace lean {
|
|
typedef list<tactic_hint_entry> tactic_hint_entries;
|
|
|
|
struct tactic_hint_state {
|
|
typedef rb_map<name, tactic_hint_entries, name_quick_cmp> class_tactics;
|
|
class_tactics m_class_tactics;
|
|
tactic_hint_entries m_tactics;
|
|
};
|
|
|
|
struct tactic_hint_config {
|
|
typedef tactic_hint_state state;
|
|
typedef tactic_hint_entry entry;
|
|
typedef tactic_hint_entries entries;
|
|
|
|
static entries add(entries const & l, entry const & e) {
|
|
return cons(e, filter(l, [&](entry const & e1) { return e1.m_pre_tactic != e.m_pre_tactic; }));
|
|
}
|
|
|
|
static void add_entry_core(state & s, entry const & e) {
|
|
if (e.m_class.is_anonymous())
|
|
s.m_tactics = add(s.m_tactics, e);
|
|
else if (auto it = s.m_class_tactics.find(e.m_class))
|
|
s.m_class_tactics.insert(e.m_class, add(*it, e));
|
|
else
|
|
s.m_class_tactics.insert(e.m_class, entries(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 g_class_name("tactic_hint");
|
|
return g_class_name;
|
|
}
|
|
|
|
static std::string const & get_serialization_key() {
|
|
static std::string g_key("tachint");
|
|
return g_key;
|
|
}
|
|
|
|
static void write_entry(serializer & s, entry const & e) {
|
|
s << e.m_class << e.m_pre_tactic;
|
|
}
|
|
|
|
static entry read_entry(deserializer & d) {
|
|
entry e;
|
|
d >> e.m_class >> e.m_pre_tactic;
|
|
return e;
|
|
}
|
|
};
|
|
|
|
template class scoped_ext<tactic_hint_config>;
|
|
typedef scoped_ext<tactic_hint_config> tactic_hint_ext;
|
|
|
|
list<tactic_hint_entry> get_tactic_hints(environment const & env, name const & c) {
|
|
tactic_hint_state const & s = tactic_hint_ext::get_state(env);
|
|
return ptr_to_list(s.m_class_tactics.find(c));
|
|
}
|
|
|
|
list<tactic_hint_entry> get_tactic_hints(environment const & env) {
|
|
tactic_hint_state const & s = tactic_hint_ext::get_state(env);
|
|
return s.m_tactics;
|
|
}
|
|
|
|
expr parse_tactic_name(parser & p) {
|
|
auto pos = p.pos();
|
|
name pre_tac = p.check_constant_next("invalid tactic name, constant expected");
|
|
expr pre_tac_type = p.env().get(pre_tac).get_type();
|
|
if (!is_constant(pre_tac_type) || const_name(pre_tac_type) != name({"tactic", "tactic"}))
|
|
throw parser_error(sstream() << "invalid tactic name, '" << pre_tac << "' is not a tactic", pos);
|
|
return mk_constant(pre_tac);
|
|
}
|
|
|
|
static name g_lbracket("[");
|
|
static name g_rbracket("]");
|
|
|
|
environment tactic_hint_cmd(parser & p) {
|
|
name cls;
|
|
if (p.curr_is_token(g_lbracket)) {
|
|
p.next();
|
|
cls = get_class_name(p.env(), p.parse_expr());
|
|
p.check_token_next(g_rbracket, "invalid tactic hint, ']' expected");
|
|
}
|
|
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(), tactic_hint_entry(cls, pre_tac, tac));
|
|
}
|
|
|
|
void register_tactic_hint_cmd(cmd_table & r) {
|
|
add_cmd(r, cmd_info("tactic_hint", "add a new tactic hint", tactic_hint_cmd));
|
|
}
|
|
}
|