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

feat(server): add command to get all holes in a file

Browse source
This commit is contained in:
Gabriel Ebner 2017-06-15 10:23:26 +02:00
parent b09fee680c
commit 437ab1fc27
5 changed files with 55 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontends/lean/info_manager.h
View file

@ -110,6 +110,7 @@ public:
void add_hole_info(pos_info const & begin_pos, pos_info const & end_pos, tactic_state const & s, expr const & hole_args);
line_info_data_set get_line_info_set(unsigned l) const;
rb_map<unsigned, line_info_data_set, unsigned_cmp> const & get_line_info_sets() const { return m_line_data; }
void instantiate_mvars(metavar_context const & mctx);
void merge(info_manager const & info);

49
src/frontends/lean/interactive.cpp
View file

@ -255,18 +255,11 @@ bool execute_hole_command(tactic_state const & s, name const & cmd_decl_name, ex
}
}
void get_hole_commands(module_info const & m_mod_info,
std::vector<info_manager> const & info_managers,
pos_info const & pos, json & j) {
optional<info_data> info = find_hole(m_mod_info, info_managers, pos);
if (!info)
throw exception("hole not found");
hole_info_data const & hole = to_hole_info_data(*info);
bool json_of_hole(hole_info_data const & hole, std::string const & file, json & j) {
tactic_state const & s = hole.get_tactic_state();
buffer<pair<name, std::string>> cmd_descrs;
get_hole_commands(s.env(), cmd_descrs);
if (cmd_descrs.empty())
throw exception("hole commands are not available");
if (cmd_descrs.empty()) return false;
std::vector<json> ds;
for (auto const & p : cmd_descrs) {
json d;
@ -275,11 +268,47 @@ void get_hole_commands(module_info const & m_mod_info,
ds.push_back(d);
}
j["results"] = ds;
j["file"] = m_mod_info.m_mod;
j["file"] = file;
j["start"]["line"] = hole.get_begin_pos().first;
j["start"]["column"] = hole.get_begin_pos().second;
j["end"]["line"] = hole.get_end_pos().first;
j["end"]["column"] = hole.get_end_pos().second;
return true;
}
void get_hole_commands(module_info const & m_mod_info,
std::vector<info_manager> const & info_managers,
pos_info const & pos, json & j) {
optional<info_data> info = find_hole(m_mod_info, info_managers, pos);
if (!info)
throw exception("hole not found");
hole_info_data const & hole = to_hole_info_data(*info);
if (!json_of_hole(hole, m_mod_info.m_mod, j)) {
throw exception("hole commands are not available");
}
}
void get_all_hole_commands(module_info const & m_mod_info,
std::vector<info_manager> const & info_managers,
json & j) {
std::vector<json> holes;
for (auto & infom : info_managers) {
if (infom.get_file_name() == m_mod_info.m_mod) {
infom.get_line_info_sets().for_each([&](unsigned, line_info_data_set const & S) {
S.for_each([&](unsigned, list<info_data> const & info_list) {
for (info_data const & info : info_list) {
if (hole_info_data const * hole = is_hole_info_data(info)) {
json j;
if (json_of_hole(*hole, m_mod_info.m_mod, j)) {
holes.push_back(j);
}
}
}
});
});
}
}
j["holes"] = holes;
}
void execute_hole_command(module_info const & m_mod_info,

3
src/frontends/lean/interactive.h
View file

@ -21,6 +21,9 @@ void report_info(environment const & env, options const & opts, io_state const &
void get_hole_commands(module_info const & m_mod_info,
std::vector<info_manager> const & info_managers,
pos_info const & pos, json & j);
void get_all_hole_commands(module_info const & m_mod_info,
std::vector<info_manager> const & info_managers,
json & j);
void execute_hole_command(module_info const & m_mod_info,
std::vector<info_manager> const & info_managers,
pos_info const & pos, std::string const & action, json & j);

11
src/shell/server.cpp
View file

@ -441,6 +441,8 @@ void server::handle_request(server::cmd_req const & req) {
handle_async_response(req, handle_hole(req));
} else if (command == "hole_commands") {
send_msg(handle_hole_commands(req));
} else if (command == "all_hole_commands") {
send_msg(handle_all_hole_commands(req));
} else if (command == "search") {
send_msg(handle_search(req));
} else if (command == "roi") {
@ -653,6 +655,15 @@ server::cmd_res server::handle_hole_commands(server::cmd_req const & req) {
return cmd_res(req.m_seq_num, j);
}
server::cmd_res server::handle_all_hole_commands(server::cmd_req const & req) {
std::string fn = req.m_payload.at("file_name");
auto mod_info = m_mod_mgr->get_module(fn);
std::vector<info_manager> im = get_info_managers(m_lt);
json j;
get_all_hole_commands(*mod_info, im, j);
return cmd_res(req.m_seq_num, j);
}
server::cmd_res server::handle_search(server::cmd_req const & req) {
std::string query = req.m_payload.at("query");

1
src/shell/server.h
View file

@ -99,6 +99,7 @@ class server : public module_vfs {
task<cmd_res> handle_info(cmd_req const & req);
task<cmd_res> handle_hole(cmd_req const & req);
cmd_res handle_hole_commands(cmd_req const & req);
cmd_res handle_all_hole_commands(cmd_req const & req);
cmd_res handle_search(cmd_req const & req);
cmd_res handle_roi(cmd_req const & req);