chore(frontends/lean/info_manager): cleanup old code
This commit is contained in:
Leonardo de Moura
parent
5f87ec3356
commit
fd4fffea27
2 changed files with 12 additions and 174 deletions
|
|
@ -9,9 +9,13 @@ Author: Leonardo de Moura
|
|||
#include <set>
|
||||
#include <string>
|
||||
#include "util/lean_path.h"
|
||||
#include "kernel/type_checker.h"
|
||||
#include "library/choice.h"
|
||||
#include "library/scoped_ext.h"
|
||||
#include "library/pp_options.h"
|
||||
#include "library/vm/vm.h"
|
||||
#include "library/vm/vm_format.h"
|
||||
#include "library/compiler/vm_compiler.h"
|
||||
#include "frontends/lean/json.h"
|
||||
#include "frontends/lean/info_manager.h"
|
||||
|
||||
|
|
@ -55,137 +59,18 @@ public:
|
|||
#endif
|
||||
};
|
||||
|
||||
/*
|
||||
class extra_type_info_data : public info_data_cell {
|
||||
protected:
|
||||
expr m_expr;
|
||||
expr m_type;
|
||||
public:
|
||||
extra_type_info_data() {}
|
||||
extra_type_info_data(unsigned c, expr const & e, expr const & t):info_data_cell(c), m_expr(e), m_type(t) {}
|
||||
|
||||
virtual info_kind kind() const { return info_kind::ExtraType; }
|
||||
|
||||
virtual void get_message(io_state_stream const & ios, unsigned line) const {
|
||||
ios << "-- EXTRA_TYPE|" << line << "|" << get_column() << "\n";
|
||||
ios << m_expr << endl;
|
||||
ios << "--" << endl;
|
||||
ios << m_type << endl;
|
||||
ios << "-- ACK" << endl;
|
||||
}
|
||||
};
|
||||
|
||||
class synth_info_data : public type_info_data {
|
||||
public:
|
||||
synth_info_data(unsigned c, expr const & e):type_info_data(c, e) {}
|
||||
|
||||
virtual info_kind kind() const { return info_kind::Synth; }
|
||||
|
||||
virtual void get_message(io_state_stream const & ios, unsigned line) const {
|
||||
ios << "-- SYNTH|" << line << "|" << get_column() << "\n";
|
||||
ios << m_expr << endl;
|
||||
ios << "-- ACK" << endl;
|
||||
}
|
||||
|
||||
expr const & get_expr() const { return m_expr; }
|
||||
};
|
||||
|
||||
class overload_info_data : public info_data_cell {
|
||||
expr m_choices;
|
||||
public:
|
||||
overload_info_data(unsigned c, expr const & e):info_data_cell(c), m_choices(e) {}
|
||||
|
||||
virtual info_kind kind() const { return info_kind::Overload; }
|
||||
|
||||
virtual void get_message(io_state_stream const & ios, unsigned line) const {
|
||||
ios << "-- OVERLOAD|" << line << "|" << get_column() << "\n";
|
||||
options os = ios.get_options();
|
||||
os = os.update_if_undef(get_pp_full_names_name(), true);
|
||||
auto new_ios = ios.update_options(os);
|
||||
for (unsigned i = 0; i < get_num_choices(m_choices); i++) {
|
||||
if (i > 0)
|
||||
ios << "--\n";
|
||||
new_ios << get_choice(m_choices, i) << endl;
|
||||
}
|
||||
new_ios << "-- ACK" << endl;
|
||||
}
|
||||
};
|
||||
|
||||
class overload_notation_info_data : public info_data_cell {
|
||||
list<expr> m_alts;
|
||||
public:
|
||||
overload_notation_info_data(unsigned c, list<expr> const & as):info_data_cell(c), m_alts(as) {}
|
||||
|
||||
virtual info_kind kind() const { return info_kind::Overload; }
|
||||
|
||||
virtual void get_message(io_state_stream const & ios, unsigned line) const {
|
||||
ios << "-- OVERLOAD|" << line << "|" << get_column() << "\n";
|
||||
options os = ios.get_options();
|
||||
os = os.update_if_undef(get_pp_full_names_name(), true);
|
||||
os = os.update_if_undef(get_pp_notation_name(), false);
|
||||
auto new_ios = ios.update_options(os);
|
||||
bool first = true;
|
||||
for (expr const & e : m_alts) {
|
||||
if (first) first = false; else ios << "--\n";
|
||||
new_ios << e << endl;
|
||||
}
|
||||
new_ios << "-- ACK" << endl;
|
||||
}
|
||||
};
|
||||
|
||||
class coercion_info_data : public info_data_cell {
|
||||
expr m_expr;
|
||||
expr m_type;
|
||||
public:
|
||||
coercion_info_data(unsigned c, expr const & e, expr const & t):
|
||||
info_data_cell(c), m_expr(e), m_type(t) {}
|
||||
|
||||
virtual info_kind kind() const { return info_kind::Coercion; }
|
||||
|
||||
virtual void get_message(io_state_stream const & ios, unsigned line) const {
|
||||
ios << "-- COERCION|" << line << "|" << get_column() << "\n";
|
||||
options os = ios.get_options();
|
||||
os = os.update_if_undef(get_pp_coercions_name(), true);
|
||||
ios.update_options(os) << m_expr << endl << "--" << endl << m_type << endl;
|
||||
ios << "-- ACK" << endl;
|
||||
}
|
||||
};
|
||||
|
||||
class symbol_info_data : public info_data_cell {
|
||||
name m_symbol;
|
||||
public:
|
||||
symbol_info_data(unsigned c, name const & s):info_data_cell(c), m_symbol(s) {}
|
||||
|
||||
virtual info_kind kind() const { return info_kind::Symbol; }
|
||||
|
||||
virtual void get_message(io_state_stream const & ios, unsigned line) const {
|
||||
ios << "-- SYMBOL|" << line << "|" << get_column() << "\n";
|
||||
ios << m_symbol << "\n";
|
||||
ios << "-- ACK" << endl;
|
||||
}
|
||||
};
|
||||
*/
|
||||
#ifdef LEAN_SERVER
|
||||
void tactic_state_info_data::report(io_state_stream const &, json & record) const {
|
||||
std::ostringstream ss;
|
||||
ss << m_state.pp();
|
||||
record["state"] = ss.str();
|
||||
}
|
||||
#endif
|
||||
|
||||
info_data mk_type_info(expr const & e) { return info_data(new type_info_data(e)); }
|
||||
info_data mk_identifier_info(name const & full_id) { return info_data(new identifier_info_data(full_id)); }
|
||||
info_data mk_tactic_state_info(tactic_state const & s) { return info_data(new tactic_state_info_data(s)); }
|
||||
|
||||
/*info_data mk_extra_type_info(unsigned c, expr const & e, expr const & t) { return info_data(new extra_type_info_data(c, e, t)); }
|
||||
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_overload_notation_info(unsigned c, list<expr> const & a) { return info_data(new overload_notation_info_data(c, a)); }
|
||||
info_data mk_coercion_info(unsigned c, expr const & e, expr const & t) { return info_data(new coercion_info_data(c, e, t)); }
|
||||
info_data mk_symbol_info(unsigned c, name const & s) { return info_data(new symbol_info_data(c, s)); }
|
||||
*/
|
||||
|
||||
/*static bool is_tactic_type(expr const & e) {
|
||||
expr const * it = &e;
|
||||
while (is_pi(*it)) {
|
||||
it = &binding_body(*it);
|
||||
}
|
||||
return *it == get_tactic_type() || *it == get_tactic_expr_type() || *it == get_tactic_expr_list_type();
|
||||
}*/
|
||||
|
||||
void info_manager::add_info(unsigned l, unsigned c, info_data data) {
|
||||
line_info_data_set line_set = m_line_data[l];
|
||||
line_set.insert(c, cons<info_data>(data, line_set[c]));
|
||||
|
|
@ -233,41 +118,6 @@ void info_manager::add_tactic_state_info(unsigned l, unsigned c, tactic_state co
|
|||
add_info(l, c, mk_tactic_state_info(s));
|
||||
}
|
||||
|
||||
/*
|
||||
void info_manager::add_extra_type_info(unsigned l, unsigned c, expr const & e, expr const & t) {
|
||||
//if (is_tactic_type(t))
|
||||
// return;
|
||||
add_info(l, mk_extra_type_info(c, e, t));
|
||||
}
|
||||
|
||||
void info_manager::add_synth_info(unsigned l, unsigned c, expr const & e) {
|
||||
add_info(l, mk_synth_info(c, e));
|
||||
}
|
||||
|
||||
void info_manager::add_overload_info(unsigned l, unsigned c, expr const & e) {
|
||||
add_info(l, mk_overload_info(c, e));
|
||||
}
|
||||
|
||||
void info_manager::add_overload_notation_info(unsigned l, unsigned c, list<expr> const & a) {
|
||||
add_info(l, mk_overload_notation_info(c, a));
|
||||
}
|
||||
|
||||
void info_manager::add_coercion_info(unsigned l, unsigned c, expr const & e, expr const & t) {
|
||||
add_info(l, mk_coercion_info(c, e, t));
|
||||
}
|
||||
|
||||
void info_manager::add_symbol_info(unsigned l, unsigned c, name const & s) {
|
||||
add_info(l, mk_symbol_info(c, s));
|
||||
}
|
||||
|
||||
static bool is_tactic_id(name const & id) {
|
||||
if (id.is_atomic())
|
||||
return id == get_tactic_name();
|
||||
else
|
||||
return is_tactic_id(id.get_prefix());
|
||||
}
|
||||
*/
|
||||
|
||||
#ifdef LEAN_SERVER
|
||||
void info_manager::get_info_record(environment const & env, options const & o, io_state const & ios, unsigned line,
|
||||
unsigned col, json & record, std::function<bool (info_data const &)> pred) const {
|
||||
|
|
@ -295,5 +145,4 @@ scoped_info_manager::~scoped_info_manager() {
|
|||
info_manager * get_global_info_manager() {
|
||||
return g_info_m;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -40,11 +40,7 @@ public:
|
|||
tactic_state_info_data(tactic_state const & s):m_state(s) {}
|
||||
|
||||
#ifdef LEAN_SERVER
|
||||
virtual void report(io_state_stream const &, json & record) const override {
|
||||
std::ostringstream ss;
|
||||
ss << m_state.pp();
|
||||
record["state"] = ss.str();
|
||||
}
|
||||
virtual void report(io_state_stream const &, json & record) const override;
|
||||
#endif
|
||||
};
|
||||
|
||||
|
|
@ -91,13 +87,6 @@ public:
|
|||
void add_tactic_state_info(unsigned l, unsigned c, tactic_state const & s);
|
||||
void instantiate_mvars(metavar_context const & mctx);
|
||||
void merge(info_manager const & info);
|
||||
/*void add_extra_type_info(unsigned l, unsigned c, expr const & e, expr const & t);
|
||||
void add_synth_info(unsigned l, unsigned c, expr const & e);
|
||||
void add_overload_info(unsigned l, unsigned c, expr const & e);
|
||||
void add_overload_notation_info(unsigned l, unsigned c, list<expr> const & a);
|
||||
void add_coercion_info(unsigned l, unsigned c, expr const & e, expr const & t);
|
||||
void add_symbol_info(unsigned l, unsigned c, name const & n);
|
||||
*/
|
||||
|
||||
#ifdef LEAN_SERVER
|
||||
void get_info_record(environment const & env, options const & o, io_state const & ios, unsigned line,
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue