From d84a20d68b3daa7c264cbb1fa89b29c5b19f05cb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 1 Mar 2016 19:41:46 -0800 Subject: [PATCH] remove(frontends/lean/server): FINDG command --- doc/server.org | 29 ------- src/frontends/lean/server.cpp | 86 +------------------ tests/lean/interactive/commands.input | 21 ----- .../interactive/commands.input.expected.out | 43 ---------- tests/lean/run/tactic14.lean | 17 ---- 5 files changed, 1 insertion(+), 195 deletions(-) delete mode 100644 tests/lean/interactive/commands.input delete mode 100644 tests/lean/interactive/commands.input.expected.out delete mode 100644 tests/lean/run/tactic14.lean diff --git a/doc/server.org b/doc/server.org index 29f2b9a27..7ad0a8005 100644 --- a/doc/server.org +++ b/doc/server.org @@ -354,32 +354,3 @@ The entries are of the form The types are printed without using line breaks. The command =FINDP= is mainly used to implement auto-completion. - -** Find declarations for "placeholder/goal" - -A declaration may contain placeholders/goals =_=. Some of these placeholders are instantiated automatically by Lean. -Others, must be manually filled by the user. The command =FINDG= generates a sequence of declarations that may be used to -"fill" a particular placeholder. This command is only available if the declaration containing =_= is type correct, and -lean "knows" what is the expected type for =_=. - -#+BEGIN_SRC -FINDG [line-number] [column-number] -[filters]* -#+END_SRC - -The character at the given =[line-number]= and =[column-number]= must be a =_=. -The command also accepts a sequence of filters of the form =+[id_1]= and =-[id_2]=. -Lean will only consider declarations whose name contains =id_1= and does not contain =id_2=. -Here is an example: - -#+BEGIN_SRC -FINDG 48 10 -+intro -and -elim -#+END_SRC - -For the command above, lean will print any declaration whose resultant type matches the type expected by =_=, and -whose name contains =intro= but does not contain =and= and =elim=. -Lean does not display "trivial" matches. We say a match is trivial if the resultant type of a declaration -matches anything. - -The output produced by =FINDG= uses the same format used by =FINDP=. diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 53ed64f31..49734347d 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -40,8 +40,7 @@ Author: Leonardo de Moura #define LEAN_FUZZY_MAX_ERRORS 3 #define LEAN_FUZZY_MAX_ERRORS_FACTOR 3 -#define LEAN_FIND_CONSUME_IMPLICIT true // lean will add metavariables for implicit arguments when printing the type of declarations in FINDP and FINDG -#define LEAN_FINDG_MAX_STEPS 128 // maximum number of steps per unification problem +#define LEAN_FIND_CONSUME_IMPLICIT true // lean will add metavariables for implicit arguments when printing the type of declarations in FINDP namespace lean { static name * g_auto_completion_max_results = nullptr; @@ -320,7 +319,6 @@ static std::string * g_show = nullptr; static std::string * g_valid = nullptr; static std::string * g_sleep = nullptr; static std::string * g_findp = nullptr; -static std::string * g_findg = nullptr; static bool is_command(std::string const & cmd, std::string const & line) { return line.compare(0, cmd.size(), cmd) == 0; @@ -745,80 +743,6 @@ void consume_pos_neg_strs(std::string const & filters, buffer & pos } } -bool match_type(type_checker & tc, expr const & meta, expr const & expected_type, declaration const & d) { - goal g(meta, expected_type); - buffer ls; - unsigned num_ls = d.get_num_univ_params(); - for (unsigned i = 0; i < num_ls; i++) - ls.push_back(mk_meta_univ(mk_fresh_name())); - expr dt = instantiate_type_univ_params(d, to_list(ls.begin(), ls.end())); - unsigned num_e = get_expect_num_args(tc, expected_type); - unsigned num_d = get_expect_num_args(tc, dt); - if (num_e > num_d) - return false; - for (unsigned i = 0; i < num_d - num_e; i++) { - dt = tc.whnf(dt).first; - expr meta = g.mk_meta(mk_fresh_name(), binding_domain(dt)); - dt = instantiate(binding_body(dt), meta); - } - // Remark: we ignore declarations where the resultant type is of the form - // (?M ...) because they unify with almost everything. They produce a lot of noise in the output. - // Perhaps we should have an option to enable/disable this kind of declaration. For now, we - // just ingore them. - if (is_meta(dt)) - return false; // matches anything - try { - unifier_config cfg; - cfg.m_max_steps = LEAN_FINDG_MAX_STEPS; - cfg.m_kind = unifier_kind::Cheap; - auto r = unify(tc.env(), dt, expected_type, substitution(), cfg); - return static_cast(r.pull()); - } catch (exception&) { - return false; - } -} - -static std::unique_ptr mk_find_goal_type_checker(environment const & env) { - return mk_opaque_type_checker(env); -} - -static name * g_tmp_prefix = nullptr; -void server::find_goal_matches(unsigned line_num, unsigned col_num, std::string const & filters) { - buffer pos_names, neg_names; - consume_pos_neg_strs(filters, pos_names, neg_names); - m_out << "-- BEGINFINDG"; - optional> env_opts = m_file->infom().get_closest_env_opts(line_num); - if (!env_opts) { - m_out << " NAY" << std::endl; - m_out << "-- ENDFINDG" << std::endl; - return; - } - if (line_num >= m_file->infom().get_processed_upto()) - m_out << " NAY"; - m_out << std::endl; - environment const & env = env_opts->first; - options const & opts = env_opts->second; - std::unique_ptr tc = mk_find_goal_type_checker(env); - if (auto meta = m_file->infom().get_meta_at(line_num, col_num)) { - if (is_meta(*meta)) { - if (auto type = m_file->infom().get_type_at(line_num, col_num)) { - env.for_each_declaration([&](declaration const & d) { - if (!is_projection(env, d.get_name()) && - std::all_of(pos_names.begin(), pos_names.end(), - [&](std::string const & pos) { return is_part_of(pos, d.get_name()); }) && - std::all_of(neg_names.begin(), neg_names.end(), - [&](std::string const & neg) { return !is_part_of(neg, d.get_name()); }) && - match_type(*tc.get(), *meta, *type, d)) { - if (optional alias = is_expr_aliased(env, d.get_name())) - display_decl(*alias, d.get_name(), env, opts); - else - display_decl(d.get_name(), d.get_name(), env, opts); - } - }); - }}} - m_out << "-- ENDFINDG" << std::endl; -} - void server::wait(optional ms) { m_out << "-- BEGINWAIT" << std::endl; if (!m_worker.wait(ms)) @@ -910,10 +834,6 @@ bool server::operator()(std::istream & in) { if (line.size() > 63) line.resize(63); find_pattern(line_num, line); - } else if (is_command(*g_findg, line)) { - pair line_col_num = get_line_col_num(line, *g_findg); - read_line(in, line); - find_goal_matches(line_col_num.first, line_col_num.second, line); } else { throw exception(sstream() << "unexpected command line: " << line); } @@ -936,7 +856,6 @@ void initialize_server() { g_auto_completion_max_results = new name{"auto_completion", "max_results"}; register_unsigned_option(*g_auto_completion_max_results, LEAN_DEFAULT_AUTO_COMPLETION_MAX_RESULTS, "(auto-completion) maximum number of results returned"); - g_tmp_prefix = new name(name::mk_internal_unique_name()); g_load = new std::string("LOAD"); g_save = new std::string("SAVE"); g_visit = new std::string("VISIT"); @@ -955,11 +874,9 @@ void initialize_server() { g_valid = new std::string("VALID"); g_sleep = new std::string("SLEEP"); g_findp = new std::string("FINDP"); - g_findg = new std::string("FINDG"); } void finalize_server() { delete g_auto_completion_max_results; - delete g_tmp_prefix; delete g_load; delete g_save; delete g_visit; @@ -978,6 +895,5 @@ void finalize_server() { delete g_valid; delete g_sleep; delete g_findp; - delete g_findg; } } diff --git a/tests/lean/interactive/commands.input b/tests/lean/interactive/commands.input deleted file mode 100644 index 4a33c31f4..000000000 --- a/tests/lean/interactive/commands.input +++ /dev/null @@ -1,21 +0,0 @@ -VISIT consume_args.lean -SYNC 9 -import logic data.nat.basic -open nat eq.ops - -definition a := true - -theorem tst (a b c : nat) : a + b + c = a + c + b := -calc a + b + c = a + (b + c) : _ - ... = a + (c + b) : {!add.comm} - ... = a + c + b : (!add.assoc)⁻¹ -WAIT -CLEAR_CACHE -WAIT -INFO 4 -WAIT -INFO 4 -FINDG 7 31 -+assoc -symm -WAIT -SHOW \ No newline at end of file diff --git a/tests/lean/interactive/commands.input.expected.out b/tests/lean/interactive/commands.input.expected.out deleted file mode 100644 index eee34128f..000000000 --- a/tests/lean/interactive/commands.input.expected.out +++ /dev/null @@ -1,43 +0,0 @@ --- BEGINWAIT --- ENDWAIT --- BEGINWAIT --- ENDWAIT --- BEGININFO --- TYPE|4|13 -Type₁ --- ACK --- TYPE|4|16 -Prop --- ACK --- IDENTIFIER|4|16 -true --- ACK --- ENDINFO --- BEGINWAIT --- ENDWAIT --- BEGININFO --- TYPE|4|13 -Type₁ --- ACK --- TYPE|4|16 -Prop --- ACK --- IDENTIFIER|4|16 -true --- ACK --- ENDINFO --- BEGINFINDG --- ENDFINDG --- BEGINWAIT --- ENDWAIT --- BEGINSHOW -import logic data.nat.basic -open nat eq.ops - -definition a := true - -theorem tst (a b c : nat) : a + b + c = a + c + b := -calc a + b + c = a + (b + c) : _ - ... = a + (c + b) : {!add.comm} - ... = a + c + b : (!add.assoc)⁻¹ --- ENDSHOW diff --git a/tests/lean/run/tactic14.lean b/tests/lean/run/tactic14.lean deleted file mode 100644 index adcc2113b..000000000 --- a/tests/lean/run/tactic14.lean +++ /dev/null @@ -1,17 +0,0 @@ -import logic -open tactic - -notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r - -definition basic_tac : tactic -:= repeat (apply @and.intro | assumption) - -set_begin_end_tactic basic_tac -- basic_tac is automatically applied to each element of a proof-qed block - -theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := -begin - assume Ha, or.elim H - (assume Hna, @absurd _ false Ha Hna) - (assume Hnb, @absurd _ false Hb Hnb), - now -end