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

refactor(frontends/lean): implement show goal function using exceptions

Browse source
This commit is contained in:
Gabriel Ebner 2016-10-21 16:01:59 -04:00 • committed by Leonardo de Moura
parent fa3475fa66
commit 47e6fd091f
6 changed files with 36 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2303,9 +2303,7 @@ void elaborator::show_goal(tactic_state const & s, expr const & start_ref, expr
return;
if (curr_pos->first < line || (curr_pos->first == line && curr_pos->second < col))
return;
m_show_goal_pos = optional<pos_info>();
get_global_ios().report(message(provider->get_file_name(), *curr_pos, INFORMATION,
(sstream() << mk_pair(s.pp(get_global_ios().get_formatter_factory()), get_global_ios().get_options())).str()));
throw show_goal_exception(*curr_pos, s);
}
/* Apply the given tactic to the state 's'.
@ -2509,6 +2507,12 @@ void elaborator::ensure_no_unassigned_metavars(expr const & e) {
if (!has_expr_metavar(e)) return false;
if (is_metavar_decl_ref(e) && !mctx.is_assigned(e)) {
tactic_state s = mk_tactic_state_for(e);
if (m_show_goal_pos && get_pos_info_provider()) {
if (auto pos = get_pos_info_provider()->get_pos_info(e)) {
if (pos == m_show_goal_pos)
throw show_goal_exception(*pos, s);
}
}
throw_unsolved_tactic_state(s, "don't know how to synthesize placeholder", e);
}
return true;

8
src/frontends/lean/opt_cmd.cpp
View file

@ -32,14 +32,6 @@ bool has_show_goal(options const & opts, unsigned & line, unsigned & col) {
return has_show(opts, "show_goal", line, col);
}
options set_show_hole(options const & opts, unsigned line, unsigned col) {
return set_line_col(opts.update(name("show_hole"), true), line, col);
}
bool has_show_hole(options const & opts, unsigned & line, unsigned & col) {
return has_show(opts, "show_hole", line, col);
}
options set_show_info(options const & opts, unsigned line, unsigned col) {
return set_line_col(opts.update(name("show_info"), true), line, col);
}

3
src/frontends/lean/opt_cmd.h
View file

@ -13,9 +13,6 @@ namespace lean {
options set_show_goal(options const & opts, unsigned line, unsigned col);
bool has_show_goal(options const & opts, unsigned & line, unsigned & col);
options set_show_hole(options const & _opts, unsigned line, unsigned col);
bool has_show_hole(options const & opts, unsigned & line, unsigned & col);
options set_show_info(options const & opts, unsigned line, unsigned col);
bool has_show_info(options const & opts, unsigned & line, unsigned & col);

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

@ -151,19 +151,19 @@ parser::all_id_local_scope::all_id_local_scope(parser & p):
static name * g_tmp_prefix = nullptr;
void parser::init_stop_at(options const & opts) {
unsigned col;
m_info_at = false;
m_stop_at = false;
if (has_show_goal(opts, m_stop_at_line, col)) {
m_stop_at = true;
} else if (has_show_hole(opts, m_stop_at_line, col)) {
m_stop_at = true;
} else if (has_show_info(opts, m_info_at_line, m_info_at_col)) {
m_info_at = true;
m_stop_at = true;
m_stop_at_line = m_info_at_line;
}
void parser::enable_show_goal(pos_info const & pos) {
m_stop_at = true;
m_stop_at_line = pos.first;
m_ios.set_options(set_show_goal(m_ios.get_options(), pos.first, pos.second));
}
void parser::enable_show_info(pos_info const & pos) {
m_stop_at = true;
m_stop_at_line = pos.first;
m_info_at = true;
m_info_at_line = pos.first;
m_info_at_col = pos.second;
m_ios.set_options(set_show_info(m_ios.get_options(), pos.first, pos.second));
}
class parser_message_stream : public message_stream {
@ -202,7 +202,6 @@ parser::parser(environment const & env, io_state const & ios,
m_ignore_noncomputable = false;
m_ios.set_message_channel(std::make_shared<parser_message_stream>(this, m_ios.get_message_channel_ptr()));
m_profile = ios.get_options().get_bool("profile", false);
init_stop_at(ios.get_options());
if (num_threads > 1 && m_profile)
throw exception("option --profile cannot be used when theorems are compiled in parallel");
m_in_quote = false;
@ -212,6 +211,8 @@ parser::parser(environment const & env, io_state const & ios,
m_id_behavior = id_behavior::ErrorIfUndef;
m_found_errors = false;
m_used_sorry = false;
m_info_at = false;
m_stop_at = false;
updt_options();
m_next_tag_idx = 0;
m_next_inst_idx = 1;
@ -328,6 +329,8 @@ void parser::protected_call(std::function<void()> && f, std::function<void()> &&
m_env = ex.get_env();
ex.get_exception().rethrow();
}
} catch (show_goal_exception) {
throw;
} catch (parser_exception & ex) {
CATCH(ios().report(ex), throw);
} catch (parser_error & ex) {

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

@ -17,6 +17,7 @@ Author: Leonardo de Moura
#include "library/io_state.h"
#include "library/io_state_stream.h"
#include "library/message_builder.h"
#include "library/tactic/tactic_state.h"
#include "frontends/lean/scanner.h"
#include "frontends/lean/local_decls.h"
#include "frontends/lean/local_level_decls.h"
@ -71,6 +72,14 @@ struct snapshot {
typedef std::vector<snapshot> snapshot_vector;
class show_goal_exception : public std::exception {
public:
pos_info m_pos;
tactic_state m_state;
show_goal_exception(pos_info const & pos, tactic_state const & goal) : m_pos(pos), m_state(goal) {}
};
enum class keep_theorem_mode { All, DiscardImported, DiscardAll };
enum class id_behavior {
@ -200,8 +209,6 @@ class parser : public abstract_parser {
friend class parser_message_stream;
void add_message(message const & msg) { m_messages = cons(msg, m_messages); }
void init_stop_at(options const & opts);
void replace_theorem(certified_declaration const & thm);
environment reveal_theorems_core(buffer<name> const & ds, bool all);
public:
@ -211,6 +218,9 @@ public:
snapshot const * s = nullptr, snapshot_vector * sv = nullptr);
~parser();
void enable_show_goal(pos_info const & pos);
void enable_show_info(pos_info const & pos);
bool ignore_noncomputable() const { return m_ignore_noncomputable; }
void set_ignore_noncomputable() { m_ignore_noncomputable = true; }

23
src/shell/lean.cpp
View file

@ -117,8 +117,6 @@ static void display_help(std::ostream & out) {
std::cout << "Frontend query interface:\n";
std::cout << " --line=value line number for query\n";
std::cout << " --col=value column number for query\n";
std::cout << " --goal display goal at close to given position\n";
std::cout << " --hole display type of the \"hole\" in the given posivition\n";
std::cout << " --info display information about identifier or token in the given posivition\n";
std::cout << "Exporting data:\n";
std::cout << " --export=file -E export final environment as textual low-level file\n";
@ -151,8 +149,6 @@ static struct option g_long_options[] = {
#endif
{"line", required_argument, 0, 'L'},
{"col", required_argument, 0, 'O'},
{"goal", no_argument, 0, 'G'},
{"hole", no_argument, 0, 'Z'},
{"info", no_argument, 0, 'I'},
{"dir", required_argument, 0, 'T'},
#ifdef LEAN_DEBUG
@ -265,9 +261,6 @@ int main(int argc, char ** argv) {
optional<std::string> export_txt;
optional<std::string> export_all_txt;
optional<std::string> base_dir;
bool show_goal = false;
bool show_hole = false;
bool show_info = false;
while (true) {
int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL);
if (c == -1)
@ -338,15 +331,6 @@ int main(int argc, char ** argv) {
case 'O':
column = atoi(optarg);
break;
case 'G':
show_goal = true;
break;
case 'Z':
show_hole = true;
break;
case 'I':
show_info = true;
break;
case 'E':
export_txt = std::string(optarg);
break;
@ -371,13 +355,6 @@ int main(int argc, char ** argv) {
#if defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
#endif
if (show_hole && line && column) {
opts = set_show_hole(opts, *line, *column);
} else if (show_goal && line && column) {
opts = set_show_goal(opts, *line, *column);
} else if (show_info && line && column) {
opts = set_show_info(opts, *line, *column);
}
#if !defined(LEAN_MULTI_THREAD)
lean_assert(num_threads == 1);