feat(frontends/lean/parser): make Import command use binary Lean files

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

src/CMakeLists.txt

@@ -218,7 +218,6 @@ add_subdirectory(frontends/lean)
 set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
 add_subdirectory(frontends/lua)
 set(LEAN_LIBS ${LEAN_LIBS} leanlua)
-add_subdirectory(extra)
 if("${MULTI_THREAD}" MATCHES "ON")
    set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}")
 else()
@@ -227,6 +226,7 @@ endif()
 set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage")
 set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS})
 add_subdirectory(shell)
+add_subdirectory(extra)
 
 add_subdirectory(tests/util)
 add_subdirectory(tests/util/numerics)

src/extra/CMakeLists.txt

@@ -1,9 +1,26 @@
+add_library(extra extra.cpp)
+
 file(GLOB LEANLIB "${LEAN_SOURCE_DIR}/extra/*.lean")
 FOREACH(FILE ${LEANLIB})
-   install_files(/library FILES ${FILE})
+  get_filename_component(BASENAME ${FILE} NAME_WE)
+  set(FNAME "${BASENAME}.olean")
+  add_custom_command(OUTPUT ${LEAN_BINARY_DIR}/extra/${FNAME}
+    COMMAND ${LEAN_BINARY_DIR}/shell/lean -o ${LEAN_BINARY_DIR}/extra/${FNAME} ${FILE}
+    COMMAND ${CMAKE_COMMAND} -E copy ${LEAN_BINARY_DIR}/extra/${FNAME} ${LEAN_BINARY_DIR}/shell/${FNAME}
+    DEPENDS ${FILE} ${LEAN_BINARY_DIR}/shell/lean)
+  add_custom_target(${FNAME}_extra DEPENDS ${LEAN_BINARY_DIR}/extra/${FNAME})
+  add_dependencies(extra ${FNAME}_extra)
+  install(FILES ${LEAN_BINARY_DIR}/extra/${FNAME} DESTINATION library)
 ENDFOREACH(FILE)
 
 file(GLOB LEANLIB "${LEAN_SOURCE_DIR}/extra/*.lua")
 FOREACH(FILE ${LEANLIB})
-   install_files(/library FILES ${FILE})
+  get_filename_component(FNAME ${FILE} NAME)
+  add_custom_command(OUTPUT ${LEAN_BINARY_DIR}/extra/${FNAME}
+    COMMAND ${CMAKE_COMMAND} -E copy ${FILE} ${LEAN_BINARY_DIR}/extra/${FNAME}
+    COMMAND ${CMAKE_COMMAND} -E copy ${FILE} ${LEAN_BINARY_DIR}/shell/${FNAME}
+    DEPENDS ${FILE})
+  add_custom_target("${FNAME}_extra" DEPENDS ${LEAN_BINARY_DIR}/extra/${FNAME})
+  add_dependencies(extra "${FNAME}_extra")
+  install(FILES ${LEAN_BINARY_DIR}/extra/${FNAME} DESTINATION library)
 ENDFOREACH(FILE)

src/extra/extra.cpp

@@ -0,0 +1,10 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+namespace lean {
+// this is just a placeholder for forcing CMake to build the olean files
+void open_extra() {}
+}

src/frontends/lean/coercion.cpp

@@ -0,0 +1,18 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "frontends/lean/coercion.h"
+#include "frontends/lean/frontend.h"
+
+namespace lean {
+void coercion_declaration::write(serializer & s) const {
+    s << "Coercion" << m_coercion;
+}
+static void read_coercion(environment const & env, io_state const &, deserializer & d) {
+    add_coercion(env, read_expr(d));
+}
+static object_cell::register_deserializer_fn coercion_ds("Coercion", read_coercion);
+}

src/frontends/lean/parser.cpp

@@ -2176,6 +2176,11 @@ class parser::imp {
                     if (is_begin_import(obj)) {
                         lean_assert(num_imports > 0);
                         num_imports--;
+                        if (num_imports == 0)
+                            to_display.push_back(obj);
+                    } else if (is_begin_builtin_import(obj)) {
+                        lean_assert(num_imports > 0);
+                        num_imports--;
                     } else if (is_end_import(obj)) {
                         num_imports++;
                     } else if (is_hidden_object(obj)) {
@@ -2187,7 +2192,11 @@ class parser::imp {
                 }
                 std::reverse(to_display.begin(), to_display.end());
                 for (auto obj : to_display) {
-                    regular(m_io_state) << obj << endl;
+                    if (is_begin_import(obj)) {
+                        regular(m_io_state) << "Import \"" << *get_imported_module(obj) << "\"" << endl;
+                    } else {
+                        regular(m_io_state) << obj << endl;
+                    }
                 }
             } else if (opt_id == g_options_kwd) {
                 regular(m_io_state) << pp(m_io_state.get_options()) << endl;
@@ -2384,26 +2393,12 @@ class parser::imp {
             regular(m_io_state) << "  Set: " << id << endl;
     }
 
-    bool import_lean_file(std::string const & fname) {
+    optional<std::string> find_lua_file(std::string const & fname) {
-        std::ifstream in(fname);
-        if (!in.is_open())
-            throw parser_error(sstream() << "invalid import command, failed to open file '" << fname << "'", m_last_cmd_pos);
-        if (!m_env->mark_imported(fname.c_str())) {
-            // module already imported
-            return false;
-        }
         try {
-            script_state state; // Empty state object for the imported module
+            return some(find_file(fname, {".lua"}));
-            io_state ios = m_io_state;
+        } catch (...) {
-            ios.set_option(g_parser_verbose, false);
+            return optional<std::string>();
-            parser import_parser(m_env, ios, in, &state, true /* use exceptions */, false /* not interactive */);
-            import_parser();
-        } catch (interrupted &) {
-            throw;
-        } catch (exception &) {
-            throw parser_error(sstream() << "failed to import file '" << fname << "'", m_last_cmd_pos);
         }
-        return true;
     }
 
     void parse_import() {
@@ -2415,17 +2410,14 @@ class parser::imp {
         } else {
             fname  = check_string_next("invalid import command, string (i.e., file name) or identifier expected");
         }
-        std::string ffname = find_file(fname);
         bool r = false;
-        if (is_lean_file(ffname)) {
+        if (auto lua_fname = find_lua_file(fname)) {
-            r = import_lean_file(ffname);
-        } else if (is_lua_file(ffname)) {
             if (!m_script_state)
-                throw parser_error(sstream() << "failed to import Lua file '" << fname << "', parser does not have an intepreter", m_last_cmd_pos);
+                throw parser_error(sstream() << "failed to import Lua file '" << *lua_fname << "', parser does not have an intepreter",
-            r = m_script_state->import_explicit(ffname.c_str());
+                                   m_last_cmd_pos);
+            r = m_script_state->import_explicit(lua_fname->c_str());
         } else {
-            // assume is a Lean file
+            r = m_env->import(fname, m_io_state);
-            r = import_lean_file(ffname);
         }
         if (m_verbose) {
             if (r)

src/kernel/environment.cpp

@@ -48,6 +48,7 @@ public:
     virtual ~import_command() {}
     virtual char const * keyword() const { return "Import"; }
     virtual void write(serializer & s) const { s << "Import" << m_mod_name; }
+    std::string const & get_module() const { return m_mod_name; }
 };
 static void read_import(environment const & env, io_state const & ios, deserializer & d) {
     std::string n = d.read_string();
@@ -73,7 +74,19 @@ public:
 };
 
 bool is_begin_import(object const & obj) {
-    return dynamic_cast<import_command const*>(obj.cell()) || dynamic_cast<begin_import_mark const*>(obj.cell());
+    return dynamic_cast<import_command const*>(obj.cell());
+}
+
+optional<std::string> get_imported_module(object const & obj) {
+    if (is_begin_import(obj)) {
+        return optional<std::string>(static_cast<import_command const*>(obj.cell())->get_module());
+    } else {
+        return optional<std::string>();
+    }
+}
+
+bool is_begin_builtin_import(object const & obj) {
+    return dynamic_cast<begin_import_mark const*>(obj.cell());
 }
 
 bool is_end_import(object const & obj) {
@@ -548,31 +561,35 @@ void environment_cell::export_objects(std::string const & fname) {
     s << g_olean_end_file;
 }
 
-bool environment_cell::import(std::string const & fname, io_state const & ios) {
+bool environment_cell::load_core(std::string const & fname, io_state const & ios, optional<std::string> const & mod_name) {
-    std::string full_fname = realpath(find_file(fname, {".olean"}).c_str());
+    if (!mod_name || mark_imported_core(fname)) {
-    if (mark_imported_core(full_fname)) {
         std::ifstream in(fname);
+        if (!in.good())
+            throw exception(sstream() << "failed to open file '" << fname << "'");
         deserializer d(in);
         std::string header;
         d >> header;
         if (header != g_olean_header)
-            throw exception(sstream() << "file '" << full_fname << "' does not seem to be a valid object Lean file");
+            throw exception(sstream() << "file '" << fname << "' does not seem to be a valid object Lean file");
         unsigned major, minor;
         // Perhaps we should enforce the right version number
         d >> major >> minor;
         try {
-            add_neutral_object(new import_command(fname));
+            if (mod_name)
+                add_neutral_object(new import_command(*mod_name));
             while (true) {
                 std::string k;
                 d >> k;
                 if (k == g_olean_end_file) {
-                    add_neutral_object(new end_import_mark());
+                    if (mod_name)
+                        add_neutral_object(new end_import_mark());
                     return true;
                 }
                 read_object(env(), ios, k, d);
             }
         } catch (...) {
-            add_neutral_object(new end_import_mark());
+            if (mod_name)
+                add_neutral_object(new end_import_mark());
             throw;
         }
     } else {
@@ -580,6 +597,14 @@ bool environment_cell::import(std::string const & fname, io_state const & ios) {
     }
 }
 
+bool environment_cell::import(std::string const & fname, io_state const & ios) {
+    return load_core(realpath(find_file(fname, {".olean"}).c_str()), ios, optional<std::string>(fname));
+}
+
+void environment_cell::load(std::string const & fname, io_state const & ios) {
+    load_core(fname, ios, optional<std::string>());
+}
+
 environment_cell::environment_cell():
     m_num_children(0) {
     init_uvars();

src/kernel/environment.h

@@ -78,7 +78,7 @@ class environment_cell {
 
     bool already_imported(name const & n) const;
     bool mark_imported_core(name n);
-
+    bool load_core(std::string const & fname, io_state const & ios, optional<std::string> const & mod_name);
 
 public:
     environment_cell();
@@ -322,6 +322,8 @@ public:
 
     bool import(std::string const & fname, io_state const & ios);
 
+    void load(std::string const & fname, io_state const & ios);
+
     /**
        \brief Execute function \c fn. Any object created by \c fn
        is not exported by the environment.
@@ -393,6 +395,13 @@ public:
 
 /** \brief Return true iff the given object marks the begin of the of a sequence of imported objects. */
 bool is_begin_import(object const & obj);
+/** \brief Return true iff the given object marks the begin of the of a sequence of builtin imported objects. */
+bool is_begin_builtin_import(object const & obj);
 /** \brief Return true iff the given object marks the end of the of a sequence of imported objects. */
 bool is_end_import(object const & obj);
+/**
+    \brief Return the module imported by the given import object.
+    Return none if \c obj is not an import object.
+*/
+optional<std::string> get_imported_module(object const & obj);
 }

src/shell/CMakeLists.txt

@@ -13,28 +13,6 @@ target_link_libraries(lean ${EXTRA_LIBS})
 
 install(TARGETS lean DESTINATION bin)
 
-function(add_extra_dependency indir file)
-  get_filename_component(FNAME ${file} NAME)
-  add_custom_command(OUTPUT ${LEAN_BINARY_DIR}/shell/${indir}/${FNAME}
-    COMMAND ${CMAKE_COMMAND} -E copy ${file} ${LEAN_BINARY_DIR}/shell/${indir}/${FNAME}
-    MAIN_DEPENDENCY ${file})
-  add_custom_target("${FNAME}_extra" DEPENDS ${LEAN_BINARY_DIR}/shell/${indir}/${FNAME})
-  add_dependencies(lean "${FNAME}_extra")
-endfunction()
-
-function(add_extra_module indir)
-  file(GLOB EXTRA_LUA_FILES "${LEAN_SOURCE_DIR}/extra/${indir}/*.lua")
-  foreach(FILE ${EXTRA_LUA_FILES})
-    add_extra_dependency(${indir} ${FILE})
-  endforeach(FILE)
-  file(GLOB EXTRA_LEAN_FILES "${LEAN_SOURCE_DIR}/extra/${indir}/*.lean")
-  foreach(FILE ${EXTRA_LEAN_FILES})
-    add_extra_dependency(${indir} ${FILE})
-  endforeach(FILE)
-endfunction()
-
-add_extra_module(.)
-
 add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
 add_test(example1_stdin2 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "-l" "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
 add_test(example1_stdin3 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "--lean" "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")

src/shell/lean.cpp

@@ -197,7 +197,7 @@ int main(int argc, char ** argv) {
                     ok = false;
             } else if (k == input_kind::OLean) {
                 try {
-                    env->import(std::string(argv[i]), ios);
+                    env->load(std::string(argv[i]), ios);
                 } catch (lean::exception & ex) {
                     std::cerr << "Failed to load binary file '" << argv[i] << "': " << ex.what() << "\n";
                     ok = false;

tests/lean/cast1.lean

@@ -1,4 +1,4 @@
-Import "cast.lean"
+Import cast
 
 Variable vector : Type -> Nat -> Type
 Axiom N0 (n : Nat) : n + 0 = n

tests/lean/cast1.lean.expected.out

@@ -1,6 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Imported 'cast.lean'
+  Imported 'cast'
   Assumed: vector
   Assumed: N0
   Proved: V0

tests/lean/cast2.lean

@@ -1,4 +1,4 @@
-Import "cast.lean"
+Import cast
 Variable A : Type
 Variable B : Type
 Variable A' : Type

tests/lean/cast2.lean.expected.out

@@ -1,6 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Imported 'cast.lean'
+  Imported 'cast'
   Assumed: A
   Assumed: B
   Assumed: A'

tests/lean/cast3.lean

@@ -1,4 +1,4 @@
-Import "cast.lean"
+Import cast
 
 Variables A A' B B' : Type
 Variable x : A

tests/lean/cast3.lean.expected.out

@@ -1,6 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Imported 'cast.lean'
+  Imported 'cast'
   Assumed: A
   Assumed: A'
   Assumed: B

tests/lean/macro.lean

@@ -1,11 +0,0 @@
-(**
-macro("IdMacro",
-      { macro_arg.Expr },
-      function (env, e)
-         return e
-      end
-)
-**)
-
-Show IdMacro 10.
-Import "module.lean"

tests/lean/macro.lean.expected.out

@@ -1,5 +0,0 @@
-  Set: pp::colors
-  Set: pp::unicode
-10
-Error (line: 2, pos: 5) unknown identifier 'IdMacro'
-Error (line: 11, pos: 0) failed to import file './module.lean'

tests/lean/mod1.lean

@@ -1,14 +1,11 @@
-Import simple
+Import cast
-Import simple
+Import cast
 (**
    local env = environment() -- create new environment
    parse_lean_cmds([[
-      Import "simple.lean"
+      Import cast
-      Import "simple.lean"
+      Import cast
-      Check x + y
+      Check @cast
-      Variable z : Int
-      Check z
    ]], env)
-   -- Remark: z is not defined in the main environment
 **)
-Check z
+Check @cast

tests/lean/mod1.lean.expected.out

@@ -1,10 +1,8 @@
   Set: pp::colors
   Set: pp::unicode
-  Imported 'simple'
+  Imported 'cast'
-  Skipped 'simple'
+  Skipped 'cast'
-  Imported 'simple.lean'
+  Imported 'cast'
-  Skipped 'simple.lean'
+  Skipped 'cast'
-x + y : ℤ
+@cast : Π (A B : (Type U)), A == B → A → B
-  Assumed: z
+@cast : Π (A B : (Type U)), A == B → A → B
-z : ℤ
-Error (line: 14, pos: 6) unknown identifier 'z'

tests/lean/module.lean

@@ -1,2 +0,0 @@
-(* The following command should fail because the IdMacro is not defined *)
-Show IdMacro 20.

tests/lean/module.lean.expected.out

@@ -1,3 +0,0 @@
-  Set: pp::colors
-  Set: pp::unicode
-Error (line: 2, pos: 5) unknown identifier 'IdMacro'

tests/lean/norm_bug1.lean

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

tests/lean/norm_bug1.lean.expected.out

@@ -1,6 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Imported 'cast.lean'
+  Imported 'cast'
   Set: pp::colors
   Defined: TypeM
   Defined: TypeU

tests/lean/type_inf_bug1.lean

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

tests/lean/type_inf_bug1.lean.expected.out

@@ -1,6 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Imported 'cast.lean'
+  Imported 'cast'
   Set: pp::colors
   Defined: TypeM
   Defined: TypeU