Add module_info.get_all

library/init/meta/module_info.lean

@@ -11,6 +11,8 @@ meta constant module_info : Type
 
 namespace module_info
 
+meta constant get_all : list module_info
+
 /-- The absolute path to the `.lean` file containing the module (e.g. `".../data/dlist.lean"`). -/
 @[reducible] meta def module_id := string
 /-- The name of the module, as used in an import command (e.g. `data.dlist`). -/
@@ -130,4 +132,4 @@ meta def for_decl_of_imported_module_name
    (mod_nam : module_name) (decl : name) (cur_mod := "") : environment :=
 for_decl_of_imported_module (resolve_module_name mod_nam cur_mod) decl
 
-end environment
+end environment

src/library/vm/vm_list.h

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/expr.h"
 #include "library/vm/vm.h"
+#include <vector>
 
 namespace lean {
 list<name> to_list_name(vm_obj const & o);
@@ -45,6 +46,14 @@ inline vm_obj tail(vm_obj const & o) { lean_assert(!is_nil(o)); return cfield(o,
 inline vm_obj mk_vm_nil() { return mk_vm_simple(0); }
 inline vm_obj mk_vm_cons(vm_obj const & h, vm_obj const & t) { return mk_vm_constructor(1, h, t); }
 
+template<typename T>
+vm_obj to_obj(std::vector<T> const & ls) {
+    vm_obj obj = mk_vm_nil();
+    for (auto i = ls.size(); i > 0; i--)
+        obj = mk_vm_cons(to_obj(ls[i - 1]), obj);
+    return obj;
+}
+
 template<typename A, typename F>
 list<A> to_list(vm_obj const & o, F const & fn) {
     if (is_simple(o)) {

src/library/vm/vm_module_info.cpp

@@ -10,6 +10,7 @@ Author: Gabriel Ebner
 #include "library/util.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_module_info.h"
+#include "library/vm/vm_list.h"
 #include "library/vm/vm_string.h"
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_environment.h"
@@ -31,6 +32,10 @@ static vm_obj module_info_id(vm_obj const & mi_) {
     return to_obj(to_module_info(mi_)->m_id);
 }
 
+static vm_obj module_info_get_all() {
+    return to_obj(get_global_module_mgr()->get_all_modules());
+}
+
 static vm_obj environment_import_dependencies(vm_obj const & env_, vm_obj const & mi_) {
     auto & mod_info = to_module_info(mi_);
     auto env = to_env(env_);
@@ -70,6 +75,7 @@ void initialize_vm_module_info() {
     DECLARE_VM_BUILTIN(name({"module_info", "resolve_module_name"}),   module_info_resolve_module_name);
     DECLARE_VM_BUILTIN(name({"module_info", "of_module_id"}),          module_info_of_module_id);
     DECLARE_VM_BUILTIN(name({"module_info", "id"}),                    module_info_id);
+    DECLARE_VM_BUILTIN(name({"module_info", "get_all"}),               module_info_get_all);
     DECLARE_VM_BUILTIN(name({"environment", "import_dependencies"}),   environment_import_dependencies);
     DECLARE_VM_BUILTIN(name({"environment", "import_only"}),           environment_import_only);
     DECLARE_VM_BUILTIN(name({"environment", "import_only_until_decl"}), environment_import_only_until_decl);

tests/lean/module_info.lean

@@ -1,5 +1,7 @@
 open tactic
 
+run_cmd guard (module_info.get_all ≠ [] : bool)
+
 #eval (module_info.resolve_module_name `data.dlist).backn 10
 
 #eval (environment.from_imported_module_name `data.dlist).contains `dlist
@@ -25,4 +27,4 @@ exact `("imported")
 -- double imports will just fail
 #eval do
 e ← get_env,
-set_env_core $ e.import' (module_info.of_module_name `data.dlist)
+set_env_core $ e.import' (module_info.of_module_name `data.dlist)