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

refactor(frontends/lean/info_manager): to allow cache to be used when producing info data, fixes #37, closes #45

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-17 12:14:42 -07:00
parent c6600bdaf4
commit 55b0a03e3d
14 changed files with 403 additions and 233 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/frontends/lean/decl_cmds.cpp
View file

@ -187,6 +187,7 @@ struct decl_modifiers {
environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
auto n_pos = p.pos();
unsigned start_line = n_pos.first;
name n = p.check_id_next("invalid declaration, identifier expected");
check_atomic(n);
decl_modifiers modifiers;
@ -246,6 +247,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
update_univ_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p);
ls = to_list(ls_buffer.begin(), ls_buffer.end());
}
unsigned end_line = p.pos().first;
if (p.used_sorry())
p.declare_sorry();
@ -277,6 +279,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
expr pre_value = value;
level_param_names new_ls;
bool found_cached = false;
if (p.are_info_lines_valid(start_line, end_line)) {
// we only use the cache if the information associated with the line is valid
if (auto it = p.find_cached_definition(real_n, pre_type, pre_value)) {
optional<certified_declaration> cd;
try {
@ -290,10 +294,11 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
found_cached = true;
} catch (exception&) {}
}
}
if (!found_cached) {
if (is_theorem) {
if (p.num_threads() > 1) {
if (!p.collecting_info() && p.num_threads() > 1) {
// add as axiom, and create a task to prove the theorem
p.add_delayed_theorem(env, real_n, ls, type, value);
std::tie(type, new_ls) = p.elaborate_type(type);

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

@ -307,7 +307,7 @@ class elaborator {
name_set m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned
bool m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent.
bool m_noinfo; // when true, we do not collect information when true, we set is to true whenever we find noinfo annotation.
std::vector<info_data> m_pre_info_data;
info_manager m_pre_info_data;
struct scope_ctx {
context::scope m_scope1;
@ -858,7 +858,7 @@ public:
}
if (!first) {
// we save the info data again for application of functions with strict implicit arguments
replace_info_data(get_app_fn(e), f);
save_info_data(get_app_fn(e), f);
}
}
expr d_type = binding_domain(f_type);
@ -904,33 +904,20 @@ public:
}
/** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */
void save_info_data_core(expr const & e, expr const & r, bool replace) {
void save_info_data(expr const & e, expr const & r) {
if (!m_noinfo && infom() && pip() && (is_constant(e) || is_local(e) || is_placeholder(e))) {
if (auto p = pip()->get_pos_info(e)) {
type_checker::scope scope(*m_tc[m_relax_main_opaque]);
expr t = m_tc[m_relax_main_opaque]->infer(r);
info_data d = mk_type_info(p->first, p->second, t);
if (replace) {
while (!m_pre_info_data.empty() && m_pre_info_data.back() == d)
m_pre_info_data.pop_back();
}
m_pre_info_data.push_back(d);
m_pre_info_data.add_type_info(p->first, p->second, t);
}
}
}
void save_info_data(expr const & e, expr const & r) {
save_info_data_core(e, r, false);
}
void replace_info_data(expr const & e, expr const & r) {
save_info_data_core(e, r, true);
}
void save_synth_data(expr const & e, expr const & r) {
if (!m_noinfo && infom() && pip() && is_placeholder(e)) {
if (auto p = pip()->get_pos_info(e)) {
m_pre_info_data.push_back(mk_synth_info(p->first, p->second, r));
m_pre_info_data.add_synth_info(p->first, p->second, r);
}
}
}
@ -1271,10 +1258,8 @@ public:
void copy_info_to_manager(substitution s) {
if (!infom())
return;
for (auto & p : m_pre_info_data)
p = p.instantiate(s);
// TODO(Leo): implement smarter append
infom()->append(m_pre_info_data, false);
m_pre_info_data.instantiate(s);
infom()->merge(m_pre_info_data);
m_pre_info_data.clear();
}

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

@ -4,34 +4,65 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include <vector>
#include "util/thread.h"
#include "library/choice.h"
#include "frontends/lean/info_manager.h"
#include "frontends/lean/pp_options.h"
namespace lean {
void info_data_cell::dealloc() { delete this; }
class info_data;
int info_data_cell::compare(info_data_cell const & d) const {
if (m_line != d.m_line)
return m_line < d.m_line ? -1 : 1;
class info_data_cell {
unsigned m_column;
MK_LEAN_RC();
void dealloc() { delete this; }
protected:
friend info_data;
virtual info_data_cell * instantiate(substitution &) const { return nullptr; }
public:
info_data_cell():m_column(0), m_rc(0) {}
info_data_cell(unsigned c):m_column(c), m_rc(0) {}
virtual ~info_data_cell() {}
unsigned get_column() const { return m_column; }
virtual void display(io_state_stream const & ios, unsigned line) const = 0;
virtual int compare(info_data_cell const & d) const {
if (m_column != d.m_column)
return m_column < d.m_column ? -1 : 1;
if (typeid(*this) != typeid(d))
return typeid(*this).before(typeid(d)) ? -1 : 1;
return 0;
}
info_data_cell * info_data_cell::instantiate(substitution &) const { return nullptr; }
struct tmp_info_data : public info_data_cell {
tmp_info_data(unsigned l, unsigned c):info_data_cell(l, c) {}
virtual void display(io_state_stream const &) const { lean_unreachable(); } // LCOV_EXCL_LINE
};
static info_data g_dummy(new tmp_info_data(0, 0));
class info_data {
private:
info_data_cell * m_ptr;
public:
info_data();
info_data(info_data_cell * c):m_ptr(c) { lean_assert(c); m_ptr->inc_ref(); }
info_data(info_data const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
info_data(info_data && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~info_data() { if (m_ptr) m_ptr->dec_ref(); }
friend void swap(info_data & a, info_data & b) { std::swap(a.m_ptr, b.m_ptr); }
info_data & operator=(info_data const & s) { LEAN_COPY_REF(s); }
info_data & operator=(info_data && s) { LEAN_MOVE_REF(s); }
int compare(info_data const & d) const { return m_ptr->compare(*d.m_ptr); }
int compare(info_data_cell const & d) const { return m_ptr->compare(d); }
info_data instantiate(substitution & s) const;
unsigned get_column() const { return m_ptr->get_column(); }
void display(io_state_stream const & ios, unsigned line) const { m_ptr->display(ios, line); }
};
struct tmp_info_data : public info_data_cell {
tmp_info_data(unsigned c):info_data_cell(c) {}
virtual void display(io_state_stream const &, unsigned) const { lean_unreachable(); } // LCOV_EXCL_LINE
};
static info_data g_dummy(new tmp_info_data(0));
info_data::info_data():info_data(g_dummy) {}
info_data info_data::instantiate(substitution & s) const {
if (auto r = m_ptr->instantiate(s)) {
return info_data(r);
@ -45,14 +76,14 @@ protected:
expr m_expr;
public:
type_info_data() {}
type_info_data(unsigned l, unsigned c, expr const & e):info_data_cell(l, c), m_expr(e) {}
type_info_data(unsigned c, expr const & e):info_data_cell(c), m_expr(e) {}
expr const & get_type() const {
return m_expr;
}
virtual void display(io_state_stream const & ios) const {
ios << "-- TYPE|" << get_line() << "|" << get_column() << "\n";
virtual void display(io_state_stream const & ios, unsigned line) const {
ios << "-- TYPE|" << line << "|" << get_column() << "\n";
ios << m_expr << endl;
ios << "-- ACK" << endl;
}
@ -62,15 +93,15 @@ public:
if (is_eqp(e, m_expr))
return nullptr;
else
return new type_info_data(get_line(), get_column(), e);
return new type_info_data(get_column(), e);
}
};
class synth_info_data : public type_info_data {
public:
synth_info_data(unsigned l, unsigned c, expr const & e):type_info_data(l, c, e) {}
virtual void display(io_state_stream const & ios) const {
ios << "-- SYNTH|" << get_line() << "|" << get_column() << "\n";
synth_info_data(unsigned c, expr const & e):type_info_data(c, e) {}
virtual void display(io_state_stream const & ios, unsigned line) const {
ios << "-- SYNTH|" << line << "|" << get_column() << "\n";
ios << m_expr << endl;
ios << "-- ACK" << endl;
}
@ -79,9 +110,9 @@ public:
class overload_info_data : public info_data_cell {
expr m_choices;
public:
overload_info_data(unsigned l, unsigned c, expr const & e):info_data_cell(l, c), m_choices(e) {}
virtual void display(io_state_stream const & ios) const {
ios << "-- OVERLOAD|" << get_line() << "|" << get_column() << "\n";
overload_info_data(unsigned c, expr const & e):info_data_cell(c), m_choices(e) {}
virtual void display(io_state_stream const & ios, unsigned line) const {
ios << "-- OVERLOAD|" << line << "|" << get_column() << "\n";
options os = ios.get_options();
os = os.update(get_pp_full_names_option_name(), true);
auto new_ios = ios.update_options(os);
@ -97,9 +128,9 @@ public:
class coercion_info_data : public info_data_cell {
expr m_coercion;
public:
coercion_info_data(unsigned l, unsigned c, expr const & e):info_data_cell(l, c), m_coercion(e) {}
virtual void display(io_state_stream const & ios) const {
ios << "-- COERCION|" << get_line() << "|" << get_column() << "\n";
coercion_info_data(unsigned c, expr const & e):info_data_cell(c), m_coercion(e) {}
virtual void display(io_state_stream const & ios, unsigned line) const {
ios << "-- COERCION|" << line << "|" << get_column() << "\n";
options os = ios.get_options();
os = os.update(get_pp_coercion_option_name(), true);
ios.update_options(os) << m_coercion << endl;
@ -107,105 +138,174 @@ public:
}
};
info_data mk_type_info(unsigned l, unsigned c, expr const & e) { return info_data(new type_info_data(l, c, e)); }
info_data mk_synth_info(unsigned l, unsigned c, expr const & e) { return info_data(new synth_info_data(l, c, e)); }
info_data mk_overload_info(unsigned l, unsigned c, expr const & e) { return info_data(new overload_info_data(l, c, e)); }
info_data mk_coercion_info(unsigned l, unsigned c, expr const & e) { return info_data(new coercion_info_data(l, c, e)); }
info_data mk_type_info(unsigned c, expr const & e) { return info_data(new type_info_data(c, e)); }
info_data mk_synth_info(unsigned c, expr const & e) { return info_data(new synth_info_data(c, e)); }
info_data mk_overload_info(unsigned c, expr const & e) { return info_data(new overload_info_data(c, e)); }
info_data mk_coercion_info(unsigned c, expr const & e) { return info_data(new coercion_info_data(c, e)); }
bool operator<(info_data const & i1, info_data const & i2) { return i1.compare(i2) < 0; }
bool operator==(info_data const & i1, info_data const & i2) { return i1.compare(i2) == 0; }
bool operator!=(info_data const & i1, info_data const & i2) { return i1.compare(i2) != 0; }
bool operator<(info_data const & i1, info_data_cell const & i2) { return i1.compare(i2) < 0; }
struct info_data_cmp {
int operator()(info_data const & i1, info_data const & i2) const { return i1.compare(i2); }
};
info_manager::info_manager():m_sorted_upto(0) {}
struct info_manager::imp {
typedef rb_tree<info_data, info_data_cmp> info_data_set;
mutex m_mutex;
std::vector<info_data_set> m_line_data;
std::vector<bool> m_line_valid;
unsigned m_available_upto;
void info_manager::sort_core() {
if (m_sorted_upto == m_data.size())
imp():m_available_upto(0) {}
void synch_line(unsigned l) {
lean_assert(l > 0);
if (l >= m_line_data.size()) {
m_line_data.resize(l+1);
m_line_valid.resize(l+1, true);
}
}
void add_type_info(unsigned l, unsigned c, expr const & e) {
lock_guard<mutex> lc(m_mutex);
synch_line(l);
m_line_data[l].insert(mk_type_info(c, e));
}
void add_synth_info(unsigned l, unsigned c, expr const & e) {
lock_guard<mutex> lc(m_mutex);
synch_line(l);
m_line_data[l].insert(mk_synth_info(c, e));
}
void add_overload_info(unsigned l, unsigned c, expr const & e) {
lock_guard<mutex> lc(m_mutex);
synch_line(l);
m_line_data[l].insert(mk_overload_info(c, e));
}
void add_coercion_info(unsigned l, unsigned c, expr const & e) {
lock_guard<mutex> lc(m_mutex);
synch_line(l);
m_line_data[l].insert(mk_coercion_info(c, e));
}
static info_data_set instantiate(info_data_set const & s, substitution & subst) {
info_data_set r;
s.for_each([&](info_data const & d) {
r.insert(d.instantiate(subst));
});
return r;
}
void instantiate(substitution const & s) {
lock_guard<mutex> lc(m_mutex);
substitution tmp_s = s;
unsigned sz = m_line_data.size();
for (unsigned i = 0; i < sz; i++) {
m_line_data[i] = instantiate(m_line_data[i], tmp_s);
}
}
void merge(info_manager::imp const & m) {
if (m.m_line_data.empty())
return;
std::stable_sort(m_data.begin() + m_sorted_upto, m_data.end());
m_sorted_upto = m_data.size();
}
/**
\brief Return index i <= m_sorted_upto s.t.
* forall j < i, m_data[j].pos < (line, column)
* forall i <= j < m_sorted_upto, m_data[j].pos >= (line, column)
*/
unsigned info_manager::find(unsigned line, unsigned column) {
tmp_info_data d(line, column);
unsigned low = 0;
unsigned high = m_sorted_upto;
while (true) {
// forall j < low, m_data[j] < d
// forall high <= j < m_sorted_upto, m_data[j] >= d
lean_assert(low <= high);
if (low == high)
return low;
unsigned mid = low + ((high - low)/2);
lean_assert(low <= mid && mid < high);
lean_assert(mid < m_sorted_upto);
info_data const & dmid = m_data[mid];
if (dmid < d) {
low = mid+1;
} else {
high = mid;
}
}
}
void info_manager::invalidate(unsigned sline) {
lock_guard<mutex> lc(m_mutex);
sort_core();
unsigned i = find(sline, 0);
m_data.resize(i);
if (m_data.size() < m_sorted_upto)
m_sorted_upto = m_data.size();
unsigned sz = m.m_line_data.size();
for (unsigned i = 1; i < sz; i++) {
info_data_set const & s = m.m_line_data[i];
s.for_each([&](info_data const & d) {
synch_line(i);
m_line_data[i].insert(d);
});
}
}
void info_manager::add_core(info_data const & d) {
if (m_data.empty()) {
m_sorted_upto = 1;
} else if (m_sorted_upto == m_data.size() && m_data.back() < d) {
m_sorted_upto++;
} else if (m_sorted_upto > 0 && d < m_data[m_sorted_upto-1]) {
m_sorted_upto = find(d.get_line(), d.get_column());
}
m_data.push_back(d);
}
void info_manager::add(info_data const & d) {
void insert_line(unsigned l) {
lock_guard<mutex> lc(m_mutex);
add_core(d);
synch_line(l);
if (m_available_upto > l - 1)
m_available_upto = l - 1;
m_line_data.push_back(info_data_set());
unsigned i = m_line_data.size();
while (i > l) {
--i;
m_line_data[i] = m_line_data[i-1];
m_line_valid[i] = m_line_valid[i-1];
}
m_line_valid[l] = false;
}
void info_manager::append(std::vector<info_data> & vs, bool remove_duplicates) {
void remove_line(unsigned l) {
lock_guard<mutex> lc(m_mutex);
std::stable_sort(vs.begin(), vs.end());
info_data prev;
bool first = true;
for (auto const & v : vs) {
if (!remove_duplicates || first || v != prev) {
prev = v;
add_core(v);
first = false;
}
lean_assert(l > 0);
if (l >= m_line_data.size())
return;
lean_assert(!m_line_data.empty());
for (unsigned i = l; i < m_line_data.size() - 1; i++) {
m_line_data[i] = m_line_data[i+1];
m_line_valid[i] = m_line_valid[i+1];
}
m_line_data.pop_back();
if (m_available_upto > l - 1)
m_available_upto = l - 1;
}
void info_manager::sort() {
void invalidate_line(unsigned l) {
lock_guard<mutex> lc(m_mutex);
sort_core();
synch_line(l);
if (m_available_upto > l - 1)
m_available_upto = l - 1;
m_line_data[l] = info_data_set();
m_line_valid[l] = false;
}
void info_manager::display(io_state_stream const & ios, unsigned line) {
void commit_upto(unsigned l, bool valid) {
lock_guard<mutex> lc(m_mutex);
sort_core();
unsigned i = find(line, 0);
for (; i < m_data.size(); i++) {
auto const & d = m_data[i];
if (d.get_line() > line)
break;
d.display(ios);
for (unsigned i = m_available_upto; i < l && i < m_line_valid.size(); i++)
m_line_valid[i] = valid;
m_available_upto = l;
}
bool is_available(unsigned l) {
lock_guard<mutex> lc(m_mutex);
return l < m_available_upto;
}
bool is_invalidated(unsigned l) {
lock_guard<mutex> lc(m_mutex);
if (l >= m_line_valid.size())
return false;
return !m_line_valid[l];
}
void display(io_state_stream const & ios, unsigned l) {
lock_guard<mutex> lc(m_mutex);
if (l >= m_line_data.size())
return;
m_line_data[l].for_each([&](info_data const & d) {
d.display(ios, l);
});
}
void clear() {
lock_guard<mutex> lc(m_mutex);
m_line_data.clear();
}
};
info_manager::info_manager():m_ptr(new imp()) {}
info_manager::~info_manager() {}
void info_manager::add_type_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_type_info(l, c, e); }
void info_manager::add_synth_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_synth_info(l, c, e); }
void info_manager::add_overload_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_overload_info(l, c, e); }
void info_manager::add_coercion_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_coercion_info(l, c, e); }
void info_manager::instantiate(substitution const & s) { m_ptr->instantiate(s); }
void info_manager::merge(info_manager const & m) { m_ptr->merge(*m.m_ptr); }
void info_manager::insert_line(unsigned l) { m_ptr->insert_line(l); }
void info_manager::remove_line(unsigned l) { m_ptr->remove_line(l); }
void info_manager::invalidate_line(unsigned l) { m_ptr->invalidate_line(l); }
void info_manager::commit_upto(unsigned l, bool valid) { m_ptr->commit_upto(l, valid); }
bool info_manager::is_available(unsigned l) const { return m_ptr->is_available(l); }
bool info_manager::is_invalidated(unsigned l) const { return m_ptr->is_invalidated(l); }
void info_manager::clear() { m_ptr->clear(); }
void info_manager::display(io_state_stream const & ios, unsigned line) { m_ptr->display(ios, line); }
}

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

@ -6,72 +6,31 @@ Author: Leonardo de Moura
*/
#pragma once
#include <vector>
#include "util/thread.h"
#include "kernel/expr.h"
#include "kernel/metavar.h"
#include "library/io_state_stream.h"
namespace lean {
class info_data;
class info_data_cell {
unsigned m_line;
unsigned m_column;
MK_LEAN_RC();
void dealloc();
protected:
friend info_data;
virtual info_data_cell * instantiate(substitution &) const;
public:
info_data_cell():m_line(0), m_column(0), m_rc(0) {}
info_data_cell(unsigned l, unsigned c):m_line(l), m_column(c) {}
virtual ~info_data_cell() {}
unsigned get_line() const { return m_line; }
unsigned get_column() const { return m_column; }
virtual int compare(info_data_cell const & d) const;
virtual void display(io_state_stream const & ios) const = 0;
};
class info_data {
private:
info_data_cell * m_ptr;
public:
info_data();
info_data(info_data_cell * c):m_ptr(c) { lean_assert(c); m_ptr->inc_ref(); }
info_data(info_data const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
info_data(info_data && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~info_data() { if (m_ptr) m_ptr->dec_ref(); }
friend void swap(info_data & a, info_data & b) { std::swap(a.m_ptr, b.m_ptr); }
info_data & operator=(info_data const & s) { LEAN_COPY_REF(s); }
info_data & operator=(info_data && s) { LEAN_MOVE_REF(s); }
void display(io_state_stream const & ios) const { m_ptr->display(ios); }
int compare(info_data const & d) const { return m_ptr->compare(*d.m_ptr); }
int compare(info_data_cell const & d) const { return m_ptr->compare(d); }
info_data instantiate(substitution & s) const;
unsigned get_line() const { return m_ptr->get_line(); }
unsigned get_column() const { return m_ptr->get_column(); }
};
bool operator==(info_data const & i1, info_data const & i2);
info_data mk_type_info(unsigned l, unsigned c, expr const & e);
info_data mk_synth_info(unsigned l, unsigned c, expr const & e);
info_data mk_overload_info(unsigned l, unsigned c, expr const & e);
info_data mk_coercion_info(unsigned l, unsigned c, expr const & e);
class info_manager {
typedef std::vector<info_data> data_vector;
mutex m_mutex;
unsigned m_sorted_upto;
data_vector m_data;
void add_core(info_data const & d);
unsigned find(unsigned line, unsigned column);
void sort_core();
struct imp;
std::unique_ptr<imp> m_ptr;
public:
info_manager();
void invalidate(unsigned sline);
void add(info_data const & d);
void append(std::vector<info_data> & v, bool remove_duplicates = true);
void sort();
~info_manager();
void add_type_info(unsigned l, unsigned c, expr const & e);
void add_synth_info(unsigned l, unsigned c, expr const & e);
void add_overload_info(unsigned l, unsigned c, expr const & e);
void add_coercion_info(unsigned l, unsigned c, expr const & e);
void instantiate(substitution const & s);
void merge(info_manager const & m);
void insert_line(unsigned l);
void remove_line(unsigned l);
void invalidate_line(unsigned l);
void commit_upto(unsigned l, bool valid);
bool is_available(unsigned l) const;
bool is_invalidated(unsigned l) const;
void clear();
void display(io_state_stream const & ios, unsigned line);
};
}

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

@ -131,6 +131,15 @@ void parser::add_ref_index(name const & n, pos_info const & pos) {
m_index->add_ref(get_stream_name(), pos, n);
}
bool parser::are_info_lines_valid(unsigned start_line, unsigned end_line) const {
if (!m_info_manager)
return true; // we are not tracking info
for (unsigned i = start_line; i <= end_line; i++)
if (m_info_manager->is_invalidated(i))
return false;
return true;
}
expr parser::mk_sorry(pos_info const & p) {
m_used_sorry = true;
{
@ -235,6 +244,8 @@ void parser::sync_command() {
// Keep consuming tokens until we find a Command or End-of-file
while (curr() != scanner::token_kind::CommandKeyword && curr() != scanner::token_kind::Eof)
next();
if (m_info_manager)
m_info_manager->commit_upto(m_scanner.get_line()+1, false);
}
tag parser::get_tag(expr e) {
@ -546,7 +557,7 @@ std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, li
parser_pos_provider pp = get_pos_provider();
elaborator_context env = mk_elaborator_context(pp, check_unassigned);
auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
m_pre_info_data.clear();
m_pre_info_manager.clear();
return r;
}
@ -557,7 +568,7 @@ std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<
parser_pos_provider pp = get_pos_provider();
elaborator_context env = mk_elaborator_context(pp, check_unassigned);
auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
m_pre_info_data.clear();
m_pre_info_manager.clear();
return r;
}
@ -566,7 +577,7 @@ std::tuple<expr, level_param_names> parser::elaborate_at(environment const & env
parser_pos_provider pp = get_pos_provider();
elaborator_context eenv = mk_elaborator_context(env, pp);
auto r = ::lean::elaborate(eenv, list<expr>(), e, relax);
m_pre_info_data.clear();
m_pre_info_manager.clear();
return r;
}
@ -575,7 +586,7 @@ std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name cons
parser_pos_provider pp = get_pos_provider();
elaborator_context eenv = mk_elaborator_context(pp);
auto r = ::lean::elaborate(eenv, n, t, v, is_opaque);
m_pre_info_data.clear();
m_pre_info_manager.clear();
return r;
}
@ -584,7 +595,7 @@ std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(enviro
parser_pos_provider pp = get_pos_provider();
elaborator_context eenv = mk_elaborator_context(env, lls, pp);
auto r = ::lean::elaborate(eenv, n, t, v, is_opaque);
m_pre_info_data.clear();
m_pre_info_manager.clear();
return r;
}
@ -1210,6 +1221,8 @@ bool parser::parse_commands() {
case scanner::token_kind::CommandKeyword:
parse_command();
save_snapshot();
if (m_info_manager)
m_info_manager->commit_upto(m_scanner.get_line(), true);
break;
case scanner::token_kind::ScriptBlock:
parse_script();
@ -1238,6 +1251,8 @@ bool parser::parse_commands() {
}
} catch (interrupt_parser) {}
save_snapshot();
if (m_info_manager)
m_info_manager->commit_upto(m_scanner.get_line()+1, true);
for (certified_declaration const & thm : m_theorem_queue.join()) {
m_env.replace(thm);
}
@ -1249,7 +1264,7 @@ void parser::add_delayed_theorem(environment const & env, name const & n, level_
}
void parser::save_snapshot() {
m_pre_info_data.clear();
m_pre_info_manager.clear();
if (!m_snapshot_vector)
return;
if (m_snapshot_vector->empty() || static_cast<int>(m_snapshot_vector->back().m_line) != m_scanner.get_line())
@ -1259,8 +1274,8 @@ void parser::save_snapshot() {
void parser::save_pre_info_data() {
// if elaborator failed, then m_pre_info_data contains type information before elaboration.
if (m_info_manager) {
m_info_manager->append(m_pre_info_data, false);
m_pre_info_data.clear();
m_info_manager->merge(m_pre_info_manager);
m_pre_info_manager.clear();
}
}
@ -1268,7 +1283,7 @@ void parser::save_overload(expr const & e) {
if (!m_info_manager || !is_choice(e))
return;
auto p = pos_of(e);
m_info_manager->add(mk_overload_info(p.first, p.second, e));
m_info_manager->add_overload_info(p.first, p.second, e);
}
void parser::save_type_info(expr const & e) {
@ -1288,13 +1303,13 @@ void parser::save_type_info(expr const & e) {
if (!d)
return;
auto p = pos_of(e);
m_pre_info_data.push_back(mk_type_info(p.first, p.second, d->get_type()));
m_pre_info_manager.add_type_info(p.first, p.second, d->get_type());
} else if (is_local(e)) {
auto p = pos_of(e);
expr t = mlocal_type(e);
if (is_meta(t))
return;
m_pre_info_data.push_back(mk_type_info(p.first, p.second, t));
m_pre_info_manager.add_type_info(p.first, p.second, t);
}
}

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

@ -91,7 +91,7 @@ class parser {
// info support
snapshot_vector * m_snapshot_vector;
info_manager * m_info_manager;
std::vector<info_data> m_pre_info_data; // type information before elaboration
info_manager m_pre_info_manager; // type information before elaboration
// cache support
definition_cache * m_cache;
@ -186,6 +186,9 @@ public:
optional<std::tuple<level_param_names, expr, expr>> find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value);
void erase_cached_definition(name const & n) { if (m_cache) m_cache->erase(n); }
bool are_info_lines_valid(unsigned start_line, unsigned end_line) const;
bool collecting_info() const { return m_info_manager; }
void set_index(declaration_index * i) { m_index = i; }
void add_decl_index(name const & n, pos_info const & pos);
void add_ref_index(name const & n, pos_info const & pos);

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

@ -68,7 +68,6 @@ unsigned server::file::find(unsigned linenum) {
server::server(environment const & env, io_state const & ios, unsigned num_threads):
m_env(env), m_ios(ios), m_out(ios.get_regular_channel().get_stream()),
m_num_threads(num_threads), m_empty_snapshot(m_env, m_ios.get_options()) {
m_thread_busy = false;
}
server::~server() {
@ -86,7 +85,6 @@ void server::reset_thread() {
m_thread_ptr->join();
m_thread_ptr.reset(nullptr);
}
m_thread_busy = false;
}
static std::string g_load("LOAD");
@ -98,6 +96,7 @@ static std::string g_check("CHECK");
static std::string g_info("INFO");
static std::string g_set("SET");
static std::string g_eval("EVAL");
static std::string g_wait("WAIT");
static bool is_command(std::string const & cmd, std::string const & line) {
return line.compare(0, cmd.size(), cmd) == 0;
@ -137,13 +136,10 @@ void server::process_from(unsigned linenum) {
snapshot & s = i == 0 ? m_empty_snapshot : m_file->m_snapshots[i-1];
std::string block;
lean_assert(s.m_line > 0);
m_file->m_info.invalidate(s.m_line-1);
for (unsigned j = s.m_line-1; j < m_file->m_lines.size(); j++) {
block += m_file->m_lines[j];
block += '\n';
}
// p.set_cache(&m_cache);
m_thread_busy = true;
m_thread_ptr.reset(new interruptible_thread([=]() {
try {
snapshot & s = i == 0 ? m_empty_snapshot : m_file->m_snapshots[i-1];
@ -151,8 +147,8 @@ void server::process_from(unsigned linenum) {
scoped_updt_options updt(m_ios, s.m_options);
parser p(s.m_env, m_ios, strm, m_file->m_fname.c_str(), false, 1, s.m_lds, s.m_eds, s.m_line,
&m_file->m_snapshots, &m_file->m_info);
p.set_cache(&m_cache);
p();
m_thread_busy = false;
std::cout << "DONE\n";
} catch (exception& ex) {}
}));
@ -210,6 +206,8 @@ void server::replace_line(unsigned linenum, std::string const & new_line) {
interrupt_thread();
check_file();
m_file->replace_line(linenum, new_line);
reset_thread();
m_file->m_info.invalidate_line(linenum+1);
process_from(linenum);
}
@ -217,6 +215,8 @@ void server::insert_line(unsigned linenum, std::string const & new_line) {
interrupt_thread();
check_file();
m_file->insert_line(linenum, new_line);
reset_thread();
m_file->m_info.insert_line(linenum+1);
process_from(linenum);
}
@ -224,6 +224,8 @@ void server::remove_line(unsigned linenum) {
interrupt_thread();
check_file();
m_file->remove_line(linenum);
reset_thread();
m_file->m_info.remove_line(linenum+1);
process_from(linenum);
}
@ -254,7 +256,7 @@ void server::set_option(std::string const & line) {
}
void server::show_info(unsigned linenum) {
if (m_thread_busy) {
if (!m_file->m_info.is_available(linenum)) {
m_out << "-- BEGININFO\n-- NAY\n-- ENDINFO" << std::endl;
return;
}
@ -270,7 +272,7 @@ void server::show_info(unsigned linenum) {
}
void server::eval(std::string const & line) {
if (m_thread_busy) {
if (!m_file->m_info.is_available(m_file->m_lines.size())) {
m_out << "-- BEGINEVAL\n-- NAY\n-- ENDEVAL" << std::endl;
return;
}
@ -322,6 +324,11 @@ bool server::operator()(std::istream & in) {
} else if (is_command(g_eval, line)) {
read_line(in, line);
eval(line);
} else if (is_command(g_wait, line)) {
if (m_thread_ptr) {
m_thread_ptr->join();
m_thread_ptr.reset(nullptr);
}
} else {
throw exception(sstream() << "unexpected command line: " << line);
}

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

@ -41,7 +41,6 @@ class server {
unsigned m_num_threads;
snapshot m_empty_snapshot;
definition_cache m_cache;
atomic<bool> m_thread_busy;
std::unique_ptr<interruptible_thread> m_thread_ptr;
void load_file(std::string const & fname);

5
src/library/definition_cache.cpp
View file

@ -145,6 +145,11 @@ void definition_cache::add(name const & n, expr const & pre_type, expr const & p
add_core(n, pre_type, pre_value, ls, type, value);
}
void definition_cache::erase(name const & n) {
lock_guard<mutex> lc(m_mutex);
m_definitions.erase(n);
}
optional<std::tuple<level_param_names, expr, expr>> definition_cache::find(name const & n, expr const & pre_type, expr const & pre_value) {
entry const * it;
{

2
src/library/definition_cache.h
View file

@ -35,6 +35,6 @@ public:
/** \brief Load the cache content from the given stream */
void load(std::istream & in);
/** \brief Remove the entry named \c n from the cache. */
void erase(name const & n) { m_definitions.erase(n); }
void erase(name const & n);
};
}

21
tests/lean/interactive/in1.input Normal file
View file

@ -0,0 +1,21 @@
VISIT simple.lean
WAIT
INFO 4
REPLACE 4
definition foo {A B : Type} (a : A) (b : B) := b
WAIT
INFO 4
INSERT 4
WAIT
INFO 5
REMOVE 4
WAIT
INFO 4
REPLACE 4
defition foo {A B : Type} (a : A) (b : B) := b
WAIT
REPLACE 4
definition foo {A B : Type} (a : A) (b : B) := b
WAIT
INFO 4

63
tests/lean/interactive/in1.input.expected.out Normal file
View file

@ -0,0 +1,63 @@
DONE
-- BEGININFO
-- TYPE|4|33
Type
-- ACK
-- TYPE|4|41
Type
-- ACK
-- TYPE|4|47
A
-- ACK
-- ENDINFO
DONE
-- BEGININFO
-- TYPE|4|33
Type
-- ACK
-- TYPE|4|41
Type
-- ACK
-- TYPE|4|47
B
-- ACK
-- ENDINFO
DONE
-- BEGININFO
-- TYPE|5|33
Type
-- ACK
-- TYPE|5|41
Type
-- ACK
-- TYPE|5|47
B
-- ACK
-- ENDINFO
DONE
-- BEGININFO
-- TYPE|4|33
Type
-- ACK
-- TYPE|4|41
Type
-- ACK
-- TYPE|4|47
B
-- ACK
-- ENDINFO
simple.lean:4:0: error: command expected
simple.lean:5:37: error: unknown identifier 'foo'
DONE
DONE
-- BEGININFO
-- TYPE|4|33
Type
-- ACK
-- TYPE|4|41
Type
-- ACK
-- TYPE|4|47
B
-- ACK
-- ENDINFO

8
tests/lean/interactive/simple.lean Normal file
View file

@ -0,0 +1,8 @@
import standard
namespace tst
definition foo {A B : Type} (a : A) (b : B) := a
definition boo {A : Type} (a : A) := foo a a
end tst
definition pr1 {A : Type} (a b : A) := a

2
tests/lean/interactive/test_single.sh
View file

@ -12,7 +12,7 @@ else
fi
f=$2
echo "-- testing $f"
$LEAN -i < $f > $f.produced.out
$LEAN --server < $f > $f.produced.out
if test -f $f.expected.out; then
if diff $f.produced.out $f.expected.out; then
echo "-- checked"