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

feat(shell/lean): add --index option

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-14 17:44:07 -07:00
parent a4e8389695
commit 343407b1b6
7 changed files with 105 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/decl_cmds.cpp
View file

@ -82,6 +82,7 @@ static environment declare_var(parser & p, environment env,
} else {
name const & ns = get_namespace(env);
name full_n = ns + n;
p.add_decl_index(full_n, pos);
if (is_axiom)
env = module::add(env, check(env, mk_axiom(full_n, ls, type)));
else
@ -185,7 +186,8 @@ struct decl_modifiers {
};
environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
name n = p.check_id_next("invalid declaration, identifier expected");
auto n_pos = p.pos();
name n = p.check_id_next("invalid declaration, identifier expected");
check_atomic(n);
decl_modifiers modifiers;
name real_n; // real name for this declaration
@ -258,6 +260,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
real_n = ns + n;
}
p.add_decl_index(real_n, n_pos);
if (in_section(env)) {
buffer<expr> section_ps;
collect_section_locals(type, value, p, section_ps);

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

@ -121,6 +121,16 @@ optional<std::tuple<level_param_names, expr, expr>> parser::find_cached_definiti
return optional<std::tuple<level_param_names, expr, expr>>();
}
void parser::add_decl_index(name const & n, pos_info const & pos) {
if (m_index)
m_index->add_decl(get_stream_name(), pos, n);
}
void parser::add_ref_index(name const & n, pos_info const & pos) {
if (m_index)
m_index->add_ref(get_stream_name(), pos, n);
}
expr parser::mk_sorry(pos_info const & p) {
m_used_sorry = true;
{
@ -923,6 +933,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
if (m_env.find(new_id)) {
auto r = save_pos(mk_constant(new_id, ls), p);
save_type_info(r);
add_ref_index(new_id, p);
return r;
} else {
for (name const & ns : get_namespaces(m_env)) {
@ -930,6 +941,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
if (m_env.find(new_id)) {
auto r = save_pos(mk_constant(new_id, ls), p);
save_type_info(r);
add_ref_index(new_id, p);
return r;
}
}
@ -950,6 +962,8 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
new_as.push_back(copy_with_new_pos(mk_constant(e, ls), p));
}
r = save_pos(mk_choice(new_as.size(), new_as.data()), p);
if (is_constant(*r))
add_ref_index(const_name(*r), p);
save_overload(*r);
}
if (!r && m_no_undef_id_error)
@ -1285,9 +1299,10 @@ void parser::save_type_info(expr const & e) {
}
bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions,
unsigned num_threads, definitions_cache * cache) {
unsigned num_threads, definitions_cache * cache, declaration_index * index) {
parser p(env, ios, in, strm_name, use_exceptions, num_threads);
p.set_cache(cache);
p.set_index(index);
bool r = p();
ios = p.ios();
env = p.env();
@ -1295,10 +1310,10 @@ bool parse_commands(environment & env, io_state & ios, std::istream & in, char c
}
bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads,
definitions_cache * cache) {
definitions_cache * cache, declaration_index * index) {
std::ifstream in(fname);
if (in.bad() || in.fail())
throw exception(sstream() << "failed to open file '" << fname << "'");
return parse_commands(env, ios, in, fname, use_exceptions, num_threads, cache);
return parse_commands(env, ios, in, fname, use_exceptions, num_threads, cache, index);
}
}

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

@ -21,6 +21,7 @@ Author: Leonardo de Moura
#include "library/io_state_stream.h"
#include "library/kernel_bindings.h"
#include "library/definitions_cache.h"
#include "library/declaration_index.h"
#include "frontends/lean/scanner.h"
#include "frontends/lean/elaborator.h"
#include "frontends/lean/local_decls.h"
@ -94,6 +95,8 @@ class parser {
// cache support
definitions_cache * m_cache;
// index support
declaration_index * m_index;
void display_warning_pos(unsigned line, unsigned pos);
void display_warning_pos(pos_info p);
@ -183,6 +186,10 @@ public:
optional<std::tuple<level_param_names, expr, expr>> find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value);
void erase_cached_definition(name const & n) { if (m_cache) m_cache->erase(n); }
void set_index(declaration_index * i) { m_index = i; }
void add_decl_index(name const & n, pos_info const & pos);
void add_ref_index(name const & n, pos_info const & pos);
environment const & env() const { return m_env; }
io_state const & ios() const { return m_ios; }
local_level_decls const & get_local_level_decls() const { return m_local_level_decls; }
@ -325,8 +332,9 @@ public:
bool operator()() { return parse_commands(); }
};
bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, unsigned num_threads,
definitions_cache * cache = nullptr);
bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name,
bool use_exceptions, unsigned num_threads, definitions_cache * cache = nullptr,
declaration_index * index = nullptr);
bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads,
definitions_cache * cache = nullptr);
definitions_cache * cache = nullptr, declaration_index * index = nullptr);
}

2
src/library/CMakeLists.txt
View file

@ -7,6 +7,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
standard_kernel.cpp hott_kernel.cpp
unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp
explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp
match.cpp definitions_cache.cpp)
match.cpp definitions_cache.cpp declaration_index.cpp)
target_link_libraries(library ${LEAN_LIBS})

24
src/library/declaration_index.cpp Normal file
View file

@ -0,0 +1,24 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/declaration_index.h"
namespace lean {
void declaration_index::add_decl(std::string const fname, pos_info const & p, name const & n) {
m_entries.emplace_back(entry_kind::Declaration, fname, p, n);
}
void declaration_index::add_ref(std::string const fname, pos_info const & p, name const & n) {
m_entries.emplace_back(entry_kind::Reference, fname, p, n);
}
void declaration_index::save(std::ostream & out) const {
entry_kind k; std::string fname; pos_info p; name n;
for (auto const & e : m_entries) {
std::tie(k, fname, p, n) = e;
out << (k == entry_kind::Declaration ? "d" : "r") << "|" << fname << "|" << p.first
<< "|" << p.second << "|" << n << std::endl;
}
}
}

26
src/library/declaration_index.h Normal file
View file

@ -0,0 +1,26 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <iostream>
#include <vector>
#include <utility>
#include <string>
#include "util/name.h"
#include "kernel/pos_info_provider.h"
namespace lean {
/** \brief Datastructure for storing where a given declaration was defined. */
class declaration_index {
enum class entry_kind { Declaration, Reference };
typedef std::tuple<entry_kind, std::string, pos_info, name> entry;
std::vector<entry> m_entries;
public:
void add_decl(std::string const fname, pos_info const & p, name const & n);
void add_ref(std::string const fname, pos_info const & p, name const & n);
void save(std::ostream & out) const;
};
}

23
src/shell/lean.cpp
View file

@ -25,6 +25,7 @@ Author: Leonardo de Moura
#include "library/module.h"
#include "library/io_state_stream.h"
#include "library/definitions_cache.h"
#include "library/declaration_index.h"
#include "library/error_handling/error_handling.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/pp.h"
@ -49,6 +50,7 @@ using lean::pos_info;
using lean::pos_info_provider;
using lean::optional;
using lean::expr;
using lean::declaration_index;
enum class input_kind { Unspecified, Lean, Lua };
@ -83,6 +85,7 @@ static void display_help(std::ostream & out) {
std::cout << " --deps just print dependencies of a Lean input\n";
std::cout << " --flycheck print structured error message for flycheck\n";
std::cout << " --cache=file -c load/save cached definitions from/to the given file\n";
std::cout << " --index=file -i store index for declared symbols in the given file\n";
std::cout << " --permissive -P save .olean files even when errors were found\n";
#if defined(LEAN_USE_BOOST)
std::cout << " --tstack=num -s thread stack size in Kb\n";
@ -121,6 +124,7 @@ static struct option g_long_options[] = {
{"deps", no_argument, 0, 'D'},
{"flycheck", no_argument, 0, 'F'},
{"permissive", no_argument, 0, 'P'},
{"index", no_argument, 0, 'i'},
#if defined(LEAN_USE_BOOST)
{"tstack", required_argument, 0, 's'},
#endif
@ -128,9 +132,9 @@ static struct option g_long_options[] = {
};
#if defined(LEAN_USE_BOOST)
static char const * g_opt_str = "PFDHSqlupgvhj:012k:012s:012t:012o:c:";
static char const * g_opt_str = "PFDHSqlupgvhj:012k:012s:012t:012o:c:i:";
#else
static char const * g_opt_str = "PFDHSqlupgvhj:012k:012t:012o:c:";
static char const * g_opt_str = "PFDHSqlupgvhj:012k:012t:012o:c:i:";
#endif
enum class lean_mode { Standard, HoTT };
@ -157,8 +161,10 @@ int main(int argc, char ** argv) {
lean_mode mode = lean_mode::Standard;
unsigned num_threads = 1;
bool use_cache = false;
bool gen_index = false;
std::string output;
std::string cache_name;
std::string index_name;
input_kind default_k = input_kind::Lean; // default
while (true) {
int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL);
@ -210,6 +216,9 @@ int main(int argc, char ** argv) {
cache_name = optarg;
use_cache = true;
break;
case 'i':
index_name = optarg;
gen_index = true;
case 't':
trust_lvl = atoi(optarg);
break;
@ -246,6 +255,10 @@ int main(int argc, char ** argv) {
if (!in.bad() && !in.fail())
cache.load(in);
}
declaration_index index;
declaration_index * index_ptr = nullptr;
if (gen_index)
index_ptr = &index;
try {
bool ok = true;
@ -263,7 +276,7 @@ int main(int argc, char ** argv) {
if (k == input_kind::Lean) {
if (only_deps) {
display_deps(env, std::cout, argv[i]);
} else if (!parse_commands(env, ios, argv[i], false, num_threads, cache_ptr)) {
} else if (!parse_commands(env, ios, argv[i], false, num_threads, cache_ptr, index_ptr)) {
ok = false;
}
} else if (k == input_kind::Lua) {
@ -287,6 +300,10 @@ int main(int argc, char ** argv) {
std::ofstream out(cache_name, std::ofstream::binary);
cache.save(out);
}
if (gen_index) {
std::ofstream out(index_name);
index.save(out);
}
if (export_objects && (permissive || ok)) {
std::ofstream out(output, std::ofstream::binary);
export_module(out, env);