feat(frontends/lean/parser): improve Import command

- The extension does not have to be provided.
- It can also import Lua files.
- Hierachical names can be used instead of strings.

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

src/frontends/lean/parser.cpp

@@ -2373,10 +2373,7 @@ class parser::imp {
             regular(m_io_state) << "  Set: " << id << endl;
     }
 
-    void parse_import() {
+    void import_lean_file(std::string const & fname) {
-        next();
-        std::string fname  = check_string_next("invalid import command, string (i.e., file name) expected");
-        fname = find_file(fname.c_str());
         std::ifstream in(fname);
         if (!in.is_open())
             throw parser_error(sstream() << "invalid import command, failed to open file '" << fname << "'", m_last_cmd_pos);
@@ -2395,6 +2392,28 @@ class parser::imp {
         }
     }
 
+    void parse_import() {
+        next();
+        std::string fname;
+        if (curr_is_identifier()) {
+            fname = name_to_file(curr_name());
+            next();
+        } else {
+            fname  = check_string_next("invalid import command, string (i.e., file name) or identifier expected");
+        }
+        fname = find_file(fname);
+        if (is_lean_file(fname)) {
+            import_lean_file(fname);
+        } else if (is_lua_file(fname)) {
+            if (!m_script_state)
+                throw parser_error(sstream() << "failed to import Lua file '" << fname << "', parser does not have an intepreter", m_last_cmd_pos);
+            m_script_state->import_explicit(fname.c_str());
+        } else {
+            // assume is a Lean file
+            import_lean_file(fname);
+        }
+    }
+
     void parse_help() {
         next();
         if (curr() == scanner::token::CommandId) {

src/util/lean_path.cpp

@@ -10,6 +10,8 @@ Author: Leonardo de Moura
 #include <vector>
 #include "util/exception.h"
 #include "util/sstream.h"
+#include "util/name.h"
+#include "util/optional.h"
 
 namespace lean {
 #if defined(LEAN_WINDOWS)
@@ -115,14 +117,57 @@ struct init_lean_path {
     }
 };
 static init_lean_path g_init_lean_path;
+static std::string    g_sep_str(1, g_sep);
 
-std::string find_file(char const * fname) {
+bool has_file_ext(std::string const & fname, char const * ext) {
-    std::string nfname = normalize_path(std::string(fname));
+    unsigned ext_len = strlen(ext);
-    for (auto path : g_lean_path_vector) {
+    return fname.size() > ext_len && fname.substr(fname.size() - ext_len, ext_len) == ext;
-        std::string file = path + g_sep + nfname;
+}
+
+bool is_lean_file(std::string const & fname) {
+    return has_file_ext(fname, ".lean");
+}
+
+bool is_olean_file(std::string const & fname) {
+    return has_file_ext(fname, ".olean");
+}
+
+bool is_lua_file(std::string const & fname) {
+    return has_file_ext(fname, ".lua");
+}
+
+bool is_known_file_ext(std::string const & fname) {
+    return is_lean_file(fname) || is_olean_file(fname) || is_lua_file(fname);
+}
+
+optional<std::string> check_file(std::string const & path, std::string const & fname, char const * ext = nullptr) {
+    std::string file = path + g_sep + fname;
+    if (ext)
+        file += ext;
     std::ifstream ifile(file);
     if (ifile)
-            return file;
+        return optional<std::string>(file);
+    else
+        return optional<std::string>();
+}
+
+std::string name_to_file(name const & fname) {
+    return fname.to_string(g_sep_str.c_str());
+}
+
+std::string find_file(std::string fname) {
+    bool is_known = is_known_file_ext(fname);
+    fname = normalize_path(fname);
+    for (auto path : g_lean_path_vector) {
+        if (is_known) {
+            if (auto r = check_file(path, fname))
+                return *r;
+        } else {
+            for (auto ext : { ".olean", ".lean", ".lua" }) {
+                if (auto r = check_file(path, fname, ext))
+                    return *r;
+            }
+        }
     }
     throw exception(sstream() << "file '" << fname << "' not found in the LEAN_PATH");
 }

src/util/lean_path.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <string>
+#include "util/name.h"
 namespace lean {
 /**
    \brief Return the LEAN_PATH string
@@ -15,5 +16,15 @@ char const * get_lean_path();
    \brief Search the file \c fname in the LEAN_PATH. Throw an
    exception if the file was not found.
 */
-std::string find_file(char const * fname);
+std::string find_file(std::string fname);
+
+/** \brief Return true iff fname ends with ".lean" */
+bool is_lean_file(std::string const & fname);
+/** \brief Return true iff fname ends with ".olean" */
+bool is_olean_file(std::string const & fname);
+/** \brief Return true iff fname ends with ".lua" */
+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);
 }

src/util/name.cpp

@@ -53,11 +53,11 @@ struct name::imp {
 
     imp(bool s, imp * p):m_rc(1), m_is_string(s), m_hash(0), m_prefix(p) { if (p) p->inc_ref(); }
 
-    static void display_core(std::ostream & out, imp * p) {
+    static void display_core(std::ostream & out, imp * p, char const * sep) {
         lean_assert(p != nullptr);
         if (p->m_prefix) {
-            display_core(out, p->m_prefix);
+            display_core(out, p->m_prefix, sep);
-            out << lean_name_separator;
+            out << sep;
         }
         if (p->m_is_string)
             out << p->m_str;
@@ -65,11 +65,11 @@ struct name::imp {
             out << p->m_k;
     }
 
-    static void display(std::ostream & out, imp * p) {
+    static void display(std::ostream & out, imp * p, char const * sep = lean_name_separator) {
         if (p == nullptr)
             out << anonymous_str;
         else
-            display_core(out, p);
+            display_core(out, p, sep);
     }
 
     friend void copy_limbs(imp * p, buffer<name::imp *> & limbs) {
@@ -330,9 +330,9 @@ bool name::is_safe_ascii() const {
     return true;
 }
 
-std::string name::to_string() const {
+std::string name::to_string(char const * sep) const {
     std::ostringstream s;
-    imp::display(s, m_ptr);
+    imp::display(s, m_ptr, sep);
     return s.str();
 }
 

src/util/name.h

@@ -90,7 +90,7 @@ public:
     */
     name get_prefix() const;
     /** \brief Convert this hierarchical name into a string. */
-    std::string to_string() const;
+    std::string to_string(char const * sep = lean_name_separator) const;
     /** \brief Size of the this name (in characters). */
     size_t size() const;
     unsigned hash() const;

src/util/script_state.cpp

@@ -119,13 +119,20 @@ struct script_state::imp {
         ::lean::dostring(m_state, str);
     }
 
-    void import(char const * fname) {
+    void import_explicit(std::string const & fname) {
-        std::string fname_str(find_file(fname));
+        if (m_imported_modules.find(fname) == m_imported_modules.end()) {
-        if (m_imported_modules.find(fname_str) == m_imported_modules.end()) {
+            dofile(fname.c_str());
-            dofile(fname_str.c_str());
+            m_imported_modules.insert(fname);
-            m_imported_modules.insert(fname_str);
         }
     }
+
+    void import_explicit(char const * fname) {
+        import_explicit(std::string(fname));
+    }
+
+    void import(char const * fname) {
+        return import_explicit(find_file(fname));
+    }
 };
 
 script_state to_script_state(lua_State * L) {
@@ -158,6 +165,10 @@ void script_state::import(char const * str) {
     m_ptr->import(str);
 }
 
+void script_state::import_explicit(char const * str) {
+    m_ptr->import_explicit(str);
+}
+
 mutex & script_state::get_mutex() {
     return m_ptr->m_mutex;
 }

src/util/script_state.h

@@ -46,9 +46,14 @@ public:
     void dostring(char const * str);
     /**
        \brief Import file \c fname from the LEAN_PATH.
-       If the file was already included, then it nothing happens.
+       If the file was already included, then nothing happens.
     */
     void import(char const * fname);
+    /**
+       \brief Import file \c fname. \c fname is the explicit path to the file.
+       If the file was already included, then nothing happens.
+    */
+    void import_explicit(char const * fname);
 
     /**
        \brief Execute \c f in the using the internal Lua State.

tests/lean/cast4.lean

@@ -1,4 +1,4 @@
-Import "cast.lean"
+Import cast
 SetOption pp::colors false
 
 Definition TypeM := (Type M)

tests/lean/discharge.lean

@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+Import tactic
 Check @Discharge
 Theorem T (a b : Bool) : a => b => b => a.
    apply Discharge.

tests/lean/disj1.lean

@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+Import tactic
 
 Theorem T1 (a b : Bool) : a \/ b => b \/ a.
     apply Discharge.

tests/lean/mod1.lean

@@ -1,5 +1,5 @@
-Import "simple.lean"
+Import simple
-Import "simple.lean"
+Import simple
 (**
    local env = environment() -- create new environment
    parse_lean_cmds([[

tests/lean/norm_tac.lean

@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+Import tactic
 SetOption pp::implicit true
 SetOption pp::coercion true
 SetOption pp::notation false