From fd4fffea27c442b12a45f664a8680ebb47482ca3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 30 Dec 2016 18:59:15 -0800 Subject: [PATCH] chore(frontends/lean/info_manager): cleanup old code --- src/frontends/lean/info_manager.cpp | 173 ++-------------------------- src/frontends/lean/info_manager.h | 13 +-- 2 files changed, 12 insertions(+), 174 deletions(-) diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 8e01236295..69469614dc 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -9,9 +9,13 @@ Author: Leonardo de Moura #include #include #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 m_alts; -public: - overload_notation_info_data(unsigned c, list 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 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(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 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 pred) const { @@ -295,5 +145,4 @@ scoped_info_manager::~scoped_info_manager() { info_manager * get_global_info_manager() { return g_info_m; } - } diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index 83a2e99d03..4175d589a0 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -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 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,