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

fix(frontends/lean/dependencies): dependency generation

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-29 14:13:31 -07:00
parent b15f1bb8c7
commit 634363c5ec
1 changed files with 15 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -12,43 +12,33 @@ Author: Leonardo de Moura
#include "frontends/lean/scanner.h"
namespace lean {
/**
\brief Keep scanning the input until finds an import or an Eof.
If \c import return true, otherwise return false
*/
bool consume_until_import(environment const & env, scanner & s) {
name import("import");
scanner::token_kind t;
while (true) {
try {
t = s.scan(env);
if (t == scanner::token_kind::Eof)
return false;
if (t == scanner::token_kind::CommandKeyword && s.get_token_info().value() == import)
return true;
} catch (...) {}
}
}
void display_deps(environment const & env, std::ostream & out, char const * fname) {
name import("import");
std::ifstream in(fname);
if (in.bad() || in.fail())
throw exception(sstream() << "failed to open file '" << fname << "'");
scanner s(in, fname);
while (consume_until_import(env, s)) {
while (true) {
auto t = s.scan(env);
if (t != scanner::token_kind::Identifier)
break;
bool import_args = false;
while (true) {
scanner::token_kind t;
try {
t = s.scan(env);
} catch (exception &) {}
if (t == scanner::token_kind::Eof) {
return;
} else if (t == scanner::token_kind::CommandKeyword && s.get_token_info().value() == import) {
import_args = true;
} else if (import_args == true && t == scanner::token_kind::Identifier) {
std::string m_name = find_file(name_to_file(s.get_name_val()), {".lean", ".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") {
if (ext == ".lean")
m_name = rawname + ".olean";
}
display_path(out, m_name);
out << "\n";
} else {
import_args = false;
}
}
}