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

remove(frontends/lean/server): FINDG command

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-01 19:41:46 -08:00
parent 22f3efc5be
commit d84a20d68b
5 changed files with 1 additions and 195 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
doc/server.org
View file

@ -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=.

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

@ -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<std::string> & pos
}
}
bool match_type(type_checker & tc, expr const & meta, expr const & expected_type, declaration const & d) {
goal g(meta, expected_type);
buffer<level> 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<bool>(r.pull());
} catch (exception&) {
return false;
}
}
static std::unique_ptr<type_checker> 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<std::string> pos_names, neg_names;
consume_pos_neg_strs(filters, pos_names, neg_names);
m_out << "-- BEGINFINDG";
optional<pair<environment, options>> 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<type_checker> 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<name> 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<unsigned> 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<unsigned, unsigned> 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;
}
}

21
tests/lean/interactive/commands.input
View file

@ -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

43
tests/lean/interactive/commands.input.expected.out
View file

@ -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

17
tests/lean/run/tactic14.lean
View file

@ -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