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

feat(frontends/lean/server): add 'FINDP' command

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-02 12:57:20 -07:00
parent b4a80f83af
commit bbdb13172e
7 changed files with 138 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/frontends/lean/info_manager.cpp
View file

@ -473,6 +473,28 @@ struct info_manager::imp {
}
}
optional<pair<environment, options>> get_closest_env_opts(unsigned linenum) {
lock_guard<mutex> lc(m_mutex);
auto it = m_env_info.begin();
if (it == m_env_info.end())
return optional<pair<environment, options>>();
if (it->m_line > linenum)
return optional<pair<environment, options>>(it->m_env, it->m_options);
while (true) {
lean_assert(it != m_env_info.end() && it->m_line <= linenum);
auto next = it;
next++;
if (next == m_env_info.end() || next->m_line > linenum)
return optional<pair<environment, options>>(mk_pair(it->m_env, it->m_options));
it = next;
}
}
unsigned get_processed_upto() {
lock_guard<mutex> lc(m_mutex);
return m_processed_upto;
}
void clear() {
lock_guard<mutex> lc(m_mutex);
if (m_block_new_info)
@ -508,9 +530,15 @@ void info_manager::clear() { m_ptr->clear(); }
optional<pair<environment, options>> info_manager::get_final_env_opts() const {
return m_ptr->get_final_env_opts();
}
optional<pair<environment, options>> info_manager::get_closest_env_opts(unsigned linenum) const {
return m_ptr->get_closest_env_opts(linenum);
}
void info_manager::display(environment const & env, io_state const & ios, unsigned line) const {
m_ptr->display(env, ios, line);
}
unsigned info_manager::get_processed_upto() const {
return m_ptr->m_processed_upto;
}
void info_manager::block_new_info(bool f) {
m_ptr->block_new_info(f);
}

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

@ -35,8 +35,10 @@ public:
bool is_invalidated(unsigned l) const;
void save_environment_options(unsigned l, environment const & env, options const & o);
optional<pair<environment, options>> get_final_env_opts() const;
optional<pair<environment, options>> get_closest_env_opts(unsigned linenum) const;
void clear();
void display(environment const & env, io_state const & ios, unsigned line) const;
void block_new_info(bool f);
unsigned get_processed_upto() const;
};
}

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

@ -1235,6 +1235,7 @@ bool parser::parse_commands() {
display_warning_pos(pos());
regular_stream() << " imported file uses 'sorry'" << endl;
}
commit_info(1);
while (!done) {
protected_call([&]() {
check_interrupted();

94
src/frontends/lean/server.cpp
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "util/sstream.h"
#include "util/exception.h"
#include "util/sexpr/option_declarations.h"
#include "library/aliases.h"
#include "frontends/lean/server.h"
#include "frontends/lean/parser.h"
@ -255,6 +256,7 @@ static std::string g_options("OPTIONS");
static std::string g_show("SHOW");
static std::string g_valid("VALID");
static std::string g_sleep("SLEEP");
static std::string g_findp("FINDP");
static bool is_command(std::string const & cmd, std::string const & line) {
return line.compare(0, cmd.size(), cmd) == 0;
@ -404,6 +406,94 @@ void server::show(bool valid) {
m_out << "-- ENDSHOW" << std::endl;
}
static name string_to_name(std::string const & str) {
name result;
std::string id_part;
for (unsigned i = 0; i < str.size(); i++) {
if (str[i] == '.') {
result = name(result, id_part.c_str());
id_part.clear();
} else {
id_part.push_back(str[i]);
}
}
return name(result, id_part.c_str());
}
// Return true iff the last part of p is a prefix of the last part of n
static bool is_last_prefix_of(name const & p, name const & n) {
if (p.is_string() && n.is_string()) {
char const * it1 = p.get_string();
char const * it2 = n.get_string();
if (!it1 || !it2)
return false;
while (*it1 && *it2 && *it1 == *it2) {
++it1;
++it2;
}
return *it1 == 0;
} else {
return false;
}
}
// Auxiliary function for find_prefix
// 1) If p is atomic, then we just check if p is a prefix of the last component of n.
// 2) Otherwise, we check if p.get_prefix() == n.get_prefix(), and
// p.get_string() is a prefix of n.get_string()
static bool is_findp_prefix_of(name const & p, name const & n) {
if (p.is_atomic())
return is_last_prefix_of(p, n);
else
return p.get_prefix() == n.get_prefix() && is_last_prefix_of(p, n);
}
void server::display_decl(name const & short_name, name const & long_name, environment const & env, options const & o) {
declaration const & d = env.get(long_name);
io_state_stream out = regular(env, m_ios).update_options(o);
out << short_name << "|" << mk_pair(flatten(out.get_formatter()(d.get_type())), o) << "\n";
}
void server::find_prefix(unsigned linenum, std::string const & prefix) {
check_file();
m_out << "-- BEGINFINDP";
unsigned upto = m_file->infom().get_processed_upto();
optional<pair<environment, options>> env_opts = m_file->infom().get_closest_env_opts(linenum);
if (!env_opts) {
m_out << " NAY" << std::endl;
m_out << "-- ENDFINDP" << std::endl;
return;
}
if (upto < linenum)
m_out << " STALE";
environment const & env = env_opts->first;
options opts = env_opts->second;
opts = join(opts, m_ios.get_options());
m_out << std::endl;
name p = string_to_name(prefix);
name_set already_added;
for_each_expr_alias(env, [&](name const & n, list<name> const & ds) {
if (is_findp_prefix_of(p, n)) {
unsigned num = length(ds);
if (num == 1) {
display_decl(n, head(ds), env, opts);
already_added.insert(car(ds));
} else if (num > 1) {
m_out << n << "\n";
for (name const & d : ds) {
display_decl(d, d, env, opts);
already_added.insert(d);
}
}
}
});
env.for_each_declaration([&](declaration const & d) {
if (!already_added.contains(d.get_name()) && is_findp_prefix_of(p, d.get_name()))
display_decl(d.get_name(), d.get_name(), env, opts);
});
m_out << "-- ENDFINDP" << std::endl;
}
bool server::operator()(std::istream & in) {
for (std::string line; std::getline(in, line);) {
try {
@ -452,6 +542,10 @@ bool server::operator()(std::istream & in) {
unsigned ms = get_linenum(line, g_sleep);
chrono::milliseconds d(ms);
this_thread::sleep_for(d);
} else if (is_command(g_findp, line)) {
unsigned linenum = get_linenum(line, g_findp);
read_line(in, line);
find_prefix(linenum, line);
} else {
throw exception(sstream() << "unexpected command line: " << line);
}

2
src/frontends/lean/server.h
View file

@ -82,6 +82,8 @@ class server {
void set_option(std::string const & line);
void eval_core(environment const & env, options const & o, std::string const & line);
void eval(std::string const & line);
void display_decl(name const & short_name, name const & long_name, environment const & env, options const & o);
void find_prefix(unsigned linenum, std::string const & prefix);
unsigned find(unsigned linenum);
void read_line(std::istream & in, std::string & line);
void interrupt_worker();

9
src/library/aliases.cpp
View file

@ -88,6 +88,10 @@ struct aliases_ext : public environment_extension {
m_scopes = tail(m_scopes);
}
void for_each_expr_alias(std::function<void(name const &, list<name> const &)> const & fn) {
m_state.m_aliases.for_each(fn);
}
static environment using_namespace(environment const & env, io_state const &, name const &) {
// do nothing, aliases are treated in a special way in the frontend.
return env;
@ -204,6 +208,11 @@ environment add_aliases(environment const & env, name const & prefix, name const
return update(env, ext);
}
void for_each_expr_alias(environment const & env, std::function<void(name const &, list<name> const &)> const & fn) {
aliases_ext ext = get_extension(env);
ext.for_each_expr_alias(fn);
}
static int add_expr_alias(lua_State * L) {
return push_environment(L, add_expr_alias(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3)));
}

2
src/library/aliases.h
View file

@ -50,5 +50,7 @@ optional<name> get_level_alias(environment const & env, name const & n);
environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,
unsigned num_exceptions = 0, name const * exceptions = nullptr);
void for_each_expr_alias(environment const & env, std::function<void(name const &, list<name> const &)> const & fn);
void open_aliases(lua_State * L);
}