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

feat(frontends/lean/server): instantiate implicit arguments with metavariables when generating FINDP and FINDG output

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-06 13:17:26 -07:00
parent 87d7391d7a
commit 1bc31d7df0
1 changed files with 17 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -31,6 +31,10 @@ Author: Leonardo de Moura
#define DIAG(CODE)
#endif
#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
namespace lean {
server::file::file(std::istream & in, std::string const & fname):m_fname(fname) {
for (std::string line; std::getline(in, line);) {
@ -492,7 +496,19 @@ void server::show(bool valid) {
void server::display_decl(name const & short_name, name const & long_name, environment const & env, options const & o) {
declaration const & d = env.get(long_name);
io_state_stream out = regular(env, m_ios).update_options(o);
out << short_name << "|" << mk_pair(flatten(out.get_formatter()(d.get_type())), o) << "\n";
expr type = d.get_type();
if (LEAN_FIND_CONSUME_IMPLICIT) {
name_generator ngen("M");
while (true) {
if (!is_pi(type))
break;
if (!binding_info(type).is_implicit())
break;
expr m = mk_metavar(ngen.next(), binding_domain(type));
type = instantiate(binding_body(type), m);
}
}
out << short_name << "|" << mk_pair(flatten(out.get_formatter()(type)), o) << "\n";
}
optional<name> is_uniquely_aliased(environment const & env, name const & n) {
@ -539,9 +555,6 @@ void server::display_decl(name const & d, environment const & env, options const
}
}
#define LEAN_FUZZY_MAX_ERRORS 4
#define LEAN_FUZZY_MAX_ERRORS_FACTOR 3
unsigned get_fuzzy_match_max_errors(unsigned prefix_sz) {
unsigned r = (prefix_sz / LEAN_FUZZY_MAX_ERRORS_FACTOR);
if (r > LEAN_FUZZY_MAX_ERRORS)