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

feat(emacs,frontends/lean/parser,shell/server): more accurate info command using server-side parsing

Browse source
This commit is contained in:
Sebastian Ullrich 2016-12-27 00:16:28 +01:00 • committed by Leonardo de Moura
parent f719991c71
commit c9a8c02fdc
12 changed files with 141 additions and 76 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/emacs/lean-info.el
View file

@ -45,15 +45,13 @@
(defun lean-get-info-record-at-point (cont)
"Get info-record at the current point"
;; TODO(sullrich): finding the start position should go into the server
(let ((pos (lean-find-hname-beg)))
(lean-server-send-command
'info (list :file_name (buffer-file-name)
:line (line-number-at-pos pos)
:column (lean-line-offset pos))
(cl-function
(lambda (&key record)
(funcall cont record))))))
(lean-server-send-command
'info (list :file_name (buffer-file-name)
:line (line-number-at-pos)
:column (lean-line-offset))
(cl-function
(lambda (&key record)
(funcall cont record)))))
(cl-defun lean-find-definition-cont (&key file line column)
(when (fboundp 'xref-push-marker-stack) (xref-push-marker-stack))

65
src/frontends/lean/parser.cpp
View file

@ -210,48 +210,19 @@ parser::parser(environment const & env, io_state const & ios,
parser::~parser() {
}
void parser::scan() {
if (m_info_at) {
m_curr = m_scanner.scan(m_env);
pos_info p = pos();
if (p.first == m_info_at_line) {
if (curr_is_identifier()) {
name const & id = get_name_val();
if (p.second <= m_info_at_col && m_info_at_col < p.second + id.utf8_size()) {
auto out = mk_message(INFORMATION);
bool ok = true;
try {
bool show_value = false;
ok = print_id_info(*this, out, id, show_value, p);
} catch (exception &) {
ok = false;
}
if (!ok)
out << "unknown identifier '" << id << "'\n";
out.report();
m_info_at = false;
}
} else if (curr_is_keyword()) {
name const & tk = get_token_info().token();
if (p.second <= m_info_at_col && m_info_at_col < p.second + tk.utf8_size()) {
auto out = mk_message(INFORMATION);
try {
print_token_info(*this, out, tk);
} catch (exception &) {}
out.report();
m_info_at = false;
}
} else if (curr_is_command()) {
name const & tk = get_token_info().token();
if (p.second <= m_info_at_col && m_info_at_col < p.second + tk.utf8_size()) {
(mk_message(INFORMATION) << "'" << tk << "' is a command").report();
m_info_at = false;
}
}
}
} else {
m_curr = m_scanner.scan(m_env);
bool parser::check_break_at_pos(pos_info const & p, name const & tk) {
if (m_break_at_pos && p.first == m_break_at_pos->first && p.second <= m_break_at_pos->second) {
std::string s = tk.to_string();
if (utf8_char_pos(s.c_str(), m_break_at_pos->second - p.second))
return true;
}
return false;
}
void parser::scan() {
if (curr_is_identifier() && check_break_at_pos(pos(), get_name_val()))
throw break_at_pos_exception(pos(), get_name_val());
m_curr = m_scanner.scan(m_env);
}
expr parser::mk_sorry(pos_info const & p) {
@ -302,7 +273,7 @@ void parser::protected_call(std::function<void()> && f, std::function<void()> &&
m_env = ex.get_env();
ex.get_exception().rethrow();
}
} catch (show_goal_exception) {
} catch (break_at_pos_exception) {
throw;
} catch (parser_exception & ex) {
CATCH(report_message(ex), throw);
@ -1288,6 +1259,13 @@ static pair<notation::transition, parse_table> const * get_non_skip(list<pair<no
expr parser::parse_notation(parse_table t, expr * left) {
lean_assert(curr() == scanner::token_kind::Keyword);
auto p = pos();
auto first_token = get_token_info().value();
auto check_break = [&]() {
if (check_break_at_pos(pos(), get_token_info().value())) {
// info is stored at position of first notation token
throw break_at_pos_exception(p, first_token);
}
};
buffer<expr> args;
buffer<notation::action_kind> kinds;
buffer<list<expr>> nargs; // nary args
@ -1309,6 +1287,7 @@ expr parser::parse_notation(parse_table t, expr * left) {
auto r = t.find(get_token_info().value());
if (!r)
break;
check_break();
pair<notation::transition, parse_table> const * curr_pair = nullptr;
if (tail(r)) {
// There is more than one possible actions.
@ -1345,12 +1324,14 @@ expr parser::parse_notation(parse_table t, expr * left) {
r_args.push_back(parse_expr(a.rbp()));
name sep = utf8_trim(a.get_sep().to_string()); // remove padding
while (curr_is_token(sep)) {
check_break();
next();
r_args.push_back(parse_expr(a.rbp()));
}
}
if (terminator) {
if (curr_is_token(*terminator)) {
check_break();
next();
} else {
throw parser_error(sstream() << "invalid composite expression, '" << *terminator << "' expected", pos());

12
src/frontends/lean/parser.h
View file

@ -77,12 +77,13 @@ struct snapshot {
typedef std::vector<std::shared_ptr<snapshot const>> snapshot_vector;
class show_goal_exception : public std::exception {
class break_at_pos_exception : public std::exception {
public:
pos_info m_pos;
tactic_state m_state;
pos_info m_token_pos;
name m_token;
show_goal_exception(pos_info const & pos, tactic_state const & goal) : m_pos(pos), m_state(goal) {}
break_at_pos_exception(pos_info const & token_pos, name const & token):
m_token_pos(token_pos), m_token(token) {}
};
enum class id_behavior {
@ -139,6 +140,7 @@ class parser : public abstract_parser {
// info support
snapshot_vector * m_snapshot_vector;
name_set m_old_buckets_from_snapshot;
optional<pos_info> m_break_at_pos;
// curr command token
name m_cmd_token;
@ -237,6 +239,8 @@ public:
std::shared_ptr<snapshot const> const & s = {}, snapshot_vector * sv = nullptr);
~parser();
void set_break_at_pos(pos_info const & pos) { m_break_at_pos = some(pos); }
bool check_break_at_pos(pos_info const & p, name const & tk);
void enable_show_goal(pos_info const & pos);
void enable_show_info(pos_info const & pos);

95
src/shell/server.cpp
View file

@ -11,6 +11,7 @@ Authors: Gabriel Ebner, Leonardo de Moura, Sebastian Ullrich
#include <vector>
#include <clocale>
#include "util/sexpr/option_declarations.h"
#include "util/utf8.h"
#include "library/mt_task_queue.h"
#include "library/st_task_queue.h"
#include "frontends/lean/parser.h"
@ -245,7 +246,7 @@ void server::handle_request(server::cmd_req const & req) {
} else if (command == "complete") {
return handle_complete(req);
} else if (command == "info") {
return send_msg(handle_info(req));
return handle_info(req);
}
send_msg(cmd_res(req.m_seq_num, std::string("unknown command")));
@ -293,7 +294,7 @@ std::shared_ptr<snapshot const> get_closest_snapshot(std::shared_ptr<module_info
auto snapshots = mod_info.get()->m_result.get().m_snapshots;
auto ret = snapshots.size() ? snapshots.front() : std::shared_ptr<snapshot>();
for (auto & snap : snapshots) {
if (snap->m_pos.first <= line)
if (snap->m_pos.first < line)
ret = snap;
}
return ret;
@ -352,29 +353,85 @@ void server::handle_complete(cmd_req const & req) {
get_global_task_queue()->submit<auto_complete_task>(this, req.m_seq_num, pattern, mod_info, line);
}
server::cmd_res server::handle_info(server::cmd_req const & req) {
std::string fn = req.m_payload.at("file_name");
unsigned line = req.m_payload.at("line");
unsigned col = req.m_payload.at("column");
class server::info_task : public task<unit> {
server * m_server;
unsigned m_seq_num;
std::shared_ptr<module_info const> m_mod_info;
auto opts = m_ios.get_options();
auto env = m_initial_env;
if (auto mod = m_mod_mgr->get_module(fn)->m_result.peek()) {
if (mod->m_loaded_module->m_env)
env = *mod->m_loaded_module->m_env;
if (!mod->m_snapshots.empty()) opts = mod->m_snapshots.back()->m_options;
public:
info_task(server * server, unsigned seq_num, std::shared_ptr<module_info const> const & mod_info):
m_server(server), m_seq_num(seq_num), m_mod_info(mod_info) {}
// TODO(gabriel): find cleaner way to give it high prio
task_kind get_kind() const override { return task_kind::parse; }
virtual bool is_tiny() const override { return true; }
void description(std::ostream & out) const override {
out << "info at (" << get_pos().first << ", " << get_pos().second << ")";
}
json record;
for (auto & infom : m_msg_buf->get_info_managers()) {
if (infom.get_file_name() == fn) {
infom.get_info_record(env, opts, m_ios, line, col, record);
std::vector<generic_task_result> get_dependencies() override {
return {m_mod_info->m_result};
}
// TODO(gabriel): handle cancellation
unit execute() override {
try {
pos_info pos = get_pos();
std::istringstream in(*m_mod_info->m_lean_contents);
json j;
if (auto snap = get_closest_snapshot(m_mod_info, pos.first)) {
snapshot s = *snap;
s.m_sub_buckets.clear(); // HACK
try {
bool use_exceptions = true;
parser p(s.m_env, get_global_ios(), mk_dummy_loader(), in, get_module_id(),
use_exceptions, std::make_shared<snapshot>(s), nullptr);
p.set_break_at_pos(pos);
p();
} catch (break_at_pos_exception & e) {
lean_assert(e.m_token_pos.first == pos.first);
auto opts = m_server->m_ios.get_options();
auto env = m_server->m_initial_env;
if (auto mod = m_mod_info->m_result.peek()) {
if (mod->m_loaded_module->m_env)
env = *mod->m_loaded_module->m_env;
if (!mod->m_snapshots.empty()) opts = mod->m_snapshots.back()->m_options;
}
json record;
for (auto & infom : m_server->m_msg_buf->get_info_managers()) {
if (infom.get_file_name() == get_module_id()) {
infom.get_info_record(env, opts, m_server->m_ios, e.m_token_pos.first, e.m_token_pos.second,
record);
}
}
j["record"] = record;
}
}
m_server->send_msg(cmd_res(m_seq_num, j));
} catch (throwable & ex) {
m_server->send_msg(cmd_res(m_seq_num, std::string(ex.what())));
}
return {};
}
};
json res;
res["record"] = record;
return { req.m_seq_num, res };
void server::handle_info(server::cmd_req const & req) {
std::string fn = req.m_payload.at("file_name");
pos_info pos = {req.m_payload.at("line"), req.m_payload.at("column")};
scope_message_context scope_msg_ctx(message_bucket_id { "_server", 0 });
scoped_task_context scope_task_ctx(fn, pos);
auto mod_info = m_mod_mgr->get_module(fn);
get_global_task_queue()->submit<info_task>(this, req.m_seq_num, mod_info);
}
std::tuple<std::string, module_src, time_t> server::load_module(module_id const & id, bool can_use_olean) {

3
src/shell/server.h
View file

@ -55,7 +55,8 @@ class server : public module_vfs {
cmd_res handle_sync(cmd_req const & req);
class auto_complete_task;
void handle_complete(cmd_req const & req);
cmd_res handle_info(cmd_req const & req);
class info_task;
void handle_info(cmd_req const & req);
public:
server(unsigned num_threads, environment const & intial_env, io_state const & ios);

14
src/util/utf8.cpp
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include <cstdlib>
#include <string>
#include "util/debug.h"
#include "util/optional.h"
namespace lean {
bool is_utf8_next(unsigned char c) { return (c & 0xC0) == 0x80; }
@ -40,6 +41,19 @@ size_t utf8_strlen(char const * str) {
return r;
}
optional<size_t> utf8_char_pos(char const * str, size_t char_idx) {
size_t r = 0;
while (*str != 0) {
if (char_idx == 0)
return some<size_t>(r);
char_idx--;
unsigned sz = get_utf8_size(*str);
r += sz;
str += sz;
}
return optional<size_t>();
}
char const * get_utf8_last_char(char const * str) {
char const * r;
lean_assert(*str != 0);

2
src/util/utf8.h
View file

@ -6,11 +6,13 @@ Author: Leonardo de Moura
*/
#pragma once
#include <string>
#include "util/optional.h"
namespace lean {
bool is_utf8_next(unsigned char c);
unsigned get_utf8_size(unsigned char c);
size_t utf8_strlen(char const * str);
optional<size_t> utf8_char_pos(char const * str, size_t char_idx);
char const * get_utf8_last_char(char const * str);
std::string utf8_trim(std::string const & s);
}

2
tests/lean/interactive/info.input
View file

@ -1,2 +1,2 @@
{"seq_num": 0, "command": "sync", "file_name": "f", "content": "definition f := tt"}
{"seq_num": 1, "command": "info", "file_name": "f", "line": 1, "column": 16}
{"seq_num": 1, "command": "info", "file_name": "f", "line": 1, "column": 17}

2
tests/lean/interactive/info_notation.input Normal file
View file

@ -0,0 +1,2 @@
{"seq_num": 0, "command": "sync", "file_name": "f", "content": "def f := [tt]"}
{"seq_num": 1, "command": "info", "file_name": "f", "line": 1, "column": 12}

2
tests/lean/interactive/info_notation.input.expected.out Normal file
View file

@ -0,0 +1,2 @@
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"full-id":"list.cons","source":{"column":10,"file":"/library/init/core.lean","line":189},"type":"Π {T : Type}, T → list T → list T"},"response":"ok","seq_num":1}

2
tests/lean/interactive/info_notation1.input Normal file
View file

@ -0,0 +1,2 @@
{"seq_num": 0, "command": "sync", "file_name": "f", "content": "def f := [tt]++[]"}
{"seq_num": 1, "command": "info", "file_name": "f", "line": 1, "column": 13}

2
tests/lean/interactive/info_notation1.input.expected.out Normal file
View file

@ -0,0 +1,2 @@
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"full-id":"append","source":{"column":4,"file":"/library/init/core.lean","line":251},"type":"Π {α : Type} [_inst_1 : has_append α], α → α → α"},"response":"ok","seq_num":1}