feat(frontends/lean): add display_deps function, and --deps command line option

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/CMakeLists.txt

@@ -2,6 +2,7 @@ add_library(lean_frontend register_module.cpp token_table.cpp
 scanner.cpp parse_table.cpp parser_config.cpp parser.cpp
 parser_pos_provider.cpp builtin_cmds.cpp builtin_tactic_cmds.cpp
 builtin_exprs.cpp interactive.cpp notation_cmd.cpp calc.cpp
-decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp)
+decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp
+dependencies.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/dependencies.cpp

@@ -0,0 +1,55 @@
+/*
+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 "util/sstream.h"
+#include "util/lean_path.h"
+#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);
+        } catch (...) {}
+        if (t == scanner::token_kind::Eof)
+            return false;
+        if (t == scanner::token_kind::CommandKeyword && s.get_token_info().value() == import)
+            return true;
+    }
+}
+
+void display_deps(environment const & env, std::ostream & out, char const * fname) {
+    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;
+            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") {
+                m_name = rawname + ".olean";
+            }
+            display_path(out, m_name);
+            out << "\n";
+        }
+    }
+}
+}

src/frontends/lean/dependencies.h

@@ -0,0 +1,13 @@
+/*
+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 */
+void display_deps(environment const & env, std::ostream & out, char const * fname);
+}

src/shell/lean.cpp

@@ -27,6 +27,7 @@ Author: Leonardo de Moura
 #include "library/error_handling/error_handling.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/interactive.h"
+#include "frontends/lean/dependencies.h"
 #include "frontends/lua/register_modules.h"
 #include "version.h"
 #include "githash.h" // NOLINT
@@ -72,6 +73,7 @@ static void display_help(std::ostream & out) {
     std::cout << "  --interactive -i  read blocks of commands from the input stream\n";
     std::cout << "  --hott            use Homotopy Type Theory kernel and libraries\n";
     std::cout << "  --threads=num -r  number of threads used to process lean files\n";
+    std::cout << "  --deps            just print dependencies of a Lean input\n";
 #if defined(LEAN_USE_BOOST)
     std::cout << "  --tstack=num -s   thread stack size in Kb\n";
 #endif
@@ -105,6 +107,7 @@ static struct option g_long_options[] = {
     {"quiet",       no_argument,       0, 'q'},
     {"hott",        no_argument,       0, 'H'},
     {"threads",     required_argument, 0, 'r'},
+    {"deps",        no_argument,       0, 'D'},
 #if defined(LEAN_USE_BOOST)
     {"tstack",      required_argument, 0, 's'},
 #endif
@@ -112,9 +115,9 @@ static struct option g_long_options[] = {
 };
 
 #if defined(LEAN_USE_BOOST)
-static char const * g_opt_str = "Hiqlupgvhr:012c:012s:012t:012o:";
+static char const * g_opt_str = "DHiqlupgvhr:012c:012s:012t:012o:";
 #else
-static char const * g_opt_str = "Hiqlupgvhr:012c:012t:012o:";
+static char const * g_opt_str = "DHiqlupgvhr:012c:012t:012o:";
 #endif
 
 enum class lean_mode { Standard, HoTT };
@@ -126,6 +129,7 @@ int main(int argc, char ** argv) {
     unsigned trust_lvl   = 0;
     bool quiet           = false;
     bool interactive     = false;
+    bool only_deps       = false;
     lean_mode mode       = lean_mode::Standard;
     unsigned num_threads = 1;
     std::string output;
@@ -179,6 +183,9 @@ int main(int argc, char ** argv) {
         case 'q':
             quiet = true;
             break;
+        case 'D':
+            only_deps = true;
+            break;
         default:
             std::cerr << "Unknown command line option\n";
             display_help(std::cerr);
@@ -207,8 +214,11 @@ int main(int argc, char ** argv) {
                 }
             }
             if (k == input_kind::Lean) {
-                if (!parse_commands(env, ios, argv[i], false, num_threads))
+                if (only_deps) {
+                    display_deps(env, std::cout, argv[i]);
+                } else if (!parse_commands(env, ios, argv[i], false, num_threads)) {
                     ok = false;
+                }
             } else if (k == input_kind::Lua) {
                 try {
                     lean::system_import(argv[i]);

src/util/lean_path.cpp

@@ -100,6 +100,22 @@ static std::string fix_cygwin_path(std::string f) {
     }
     return f;
 }
+
+/** \brief Convert back to a cygwin_path */
+static std::string to_cygwin_path(std::string f) {
+    if (f.find('\\') != std::string::npos) {
+        if (f.size() > 2 && f[1] == ':') {
+            f = std::string("/cygdrive/") + f[0] + f.substr(2);
+        }
+        for (auto & c : f) {
+            if (c == g_sep)
+                c = g_bad_sep;
+            else if (c == ';')
+                c = ':';
+        }
+    }
+    return f;
+}
 #endif
 
 std::string normalize_path(std::string f) {
@@ -229,4 +245,12 @@ std::string find_file(name const & fname, std::initializer_list<char const *> co
 char const * get_lean_path() {
     return g_lean_path.c_str();
 }
+
+void display_path(std::ostream & out, std::string const & fname) {
+#if defined(LEAN_CYGWIN)
+    out << to_cygwin_path(fname);
+#else
+    out << fname;
+#endif
+}
 }

src/util/lean_path.h

@@ -32,4 +32,10 @@ bool is_lua_file(std::string const & fname);
 
 /** \brief Return a string that replaces hierachical name separator '::' with a path separator. */
 std::string name_to_file(name const & fname);
+
+/**
+    \brief Auxiliary function for displaying a path.
+    In some platforms it will fix the notation used to display the path.
+*/
+void display_path(std::ostream & out, std::string const & fname);
 }