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

chore(frontends/lean): remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-08 15:24:53 -07:00
parent fabfe32ca5
commit 81a694e73c
6 changed files with 4 additions and 116 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/CMakeLists.txt
View file

@ -2,8 +2,7 @@ add_library(lean_frontend OBJECT tokens.cpp
token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp
parser.cpp builtin_cmds.cpp builtin_exprs.cpp
notation_cmd.cpp decl_cmds.cpp util.cpp
inductive_cmds.cpp dependencies.cpp
pp.cpp structure_cmd.cpp structure_instance.cpp
inductive_cmds.cpp pp.cpp structure_cmd.cpp structure_instance.cpp
init_module.cpp type_util.cpp decl_attributes.cpp
prenum.cpp print_cmd.cpp elaborator.cpp
match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp

81
src/frontends/lean/dependencies.cpp
View file

@ -1,81 +0,0 @@
/*
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 <utility>
#include <fstream>
#include <string>
#include "runtime/sstream.h"
#include "util/lean_path.h"
#include "frontends/lean/scanner.h"
namespace lean {
bool display_deps(search_path const & path, environment const & env, std::ostream & out, std::ostream & err, char const * fname) {
name import("import");
name prelude("prelude");
name period(".");
std::ifstream in(fname);
if (in.bad() || in.fail()) {
err << "failed to open file '" << fname << "'" << std::endl;
return false;
}
scanner s(in, fname);
optional<unsigned> k;
std::string base = dirname(fname);
bool import_prefix = false;
bool import_args = false;
bool ok = true;
bool is_prelude = false;
auto display_dep = [&](optional<unsigned> const & k, name const & f) {
import_args = true;
try {
std::string m_name = find_file(path, base, k, name_to_file(f), {".lean", ".hlean", ".olean", ".lua"});
int last_idx = m_name.find_last_of(".");
std::string rawname = m_name.substr(0, last_idx);
std::string ext = m_name.substr(last_idx);
if (ext == ".lean" || ext == ".hlean")
m_name = rawname + ".olean";
out << m_name;
import_prefix = true;
out << "\n";
} catch (exception & new_ex) {
err << "error: file '" << name_to_file(s.get_name_val()) << "' not found in the LEAN_PATH" << std::endl;
ok = false;
}
};
while (true) {
token_kind t = token_kind::Identifier;
try {
t = s.scan(env);
} catch (exception &) {
continue;
}
if (t == token_kind::Eof) {
if (!is_prelude)
display_dep(optional<unsigned>(), name("init"));
return ok;
} else if (t == token_kind::CommandKeyword && s.get_token_info().value() == prelude) {
is_prelude = true;
} else if (t == token_kind::CommandKeyword && s.get_token_info().value() == import) {
k = optional<unsigned>();
import_prefix = true;
} else if (import_prefix && t == token_kind::Keyword && s.get_token_info().value() == period) {
if (!k)
k = 0;
else
k = *k + 1;
} else if ((import_prefix || import_args) && t == token_kind::Identifier) {
display_dep(k, s.get_name_val());
k = optional<unsigned>();
} else {
import_args = false;
import_prefix = false;
}
}
}
}

13
src/frontends/lean/dependencies.h
View file

@ -1,13 +0,0 @@
/*
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 <fstream>
#include "kernel/environment.h"
namespace lean {
/** \brief Display in \c out all files the .lean file \c fname depends on */
bool display_deps(search_path const &, environment const & env, std::ostream & out, std::ostream & err, char const * fname);
}

2
src/frontends/lean/json.cpp
View file

@ -10,6 +10,8 @@ Author: Gabriel Ebner
#include "library/protected.h"
#include "kernel/declaration.h"
#include "library/type_context.h"
#include "library/protected.h"
#include "library/scoped_ext.h"
#include "kernel/instantiate.h"
#include "frontends/lean/pp.h"
#include "frontends/lean/util.h"

1
src/library/derive_attribute.cpp
View file

@ -16,6 +16,7 @@ Author: Leonardo de Moura
#include "library/type_context.h"
#include "library/app_builder.h"
#include "library/class.h"
#include "library/module.h"
#include "library/protected.h"
#include "library/sorry.h"

20
src/shell/lean.cpp
View file

@ -39,7 +39,6 @@ Author: Leonardo de Moura
#include "library/time_task.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/pp.h"
#include "frontends/lean/dependencies.h"
#include "frontends/lean/json.h"
#include "frontends/lean/util.h"
#include "library/trace.h"
@ -431,7 +430,6 @@ int main(int argc, char ** argv) {
bool make_mode = false;
bool recursive = false;
unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL+1;
bool only_deps = false;
bool test_suite = false;
unsigned num_threads = 0;
#if defined(LEAN_MULTI_THREAD)
@ -492,9 +490,6 @@ int main(int argc, char ** argv) {
case 'q':
opts = opts.update(lean::get_verbose_opt_name(), false);
break;
case 'd':
only_deps = true;
break;
case 'D':
try {
opts = set_config_option(opts, optarg);
@ -669,21 +664,6 @@ int main(int argc, char ** argv) {
bool ok = true;
if (only_deps) {
for (auto & mod_fn : module_args) {
try {
if (!display_deps(path.get_path(), env, std::cout, std::cerr, mod_fn.c_str()))
ok = false;
} catch (lean::exception &ex) {
ok = false;
lean::message_builder(env, ios, mod_fn, lean::pos_info(1, 1), lean::ERROR).set_exception(
ex).report();
}
}
return ok ? 0 : 1;
}
struct input_mod {
module_id m_id;
std::shared_ptr<module_info const> m_mod_info;