From 0aa2d9b35af6674250966110dc6695bdb32ca13e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 2 Nov 2021 09:43:48 +0000 Subject: [PATCH 01/11] Add module_info.get_all --- src/library/vm/vm_module_info.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/library/vm/vm_module_info.cpp b/src/library/vm/vm_module_info.cpp index f497c38b57..791634e06b 100644 --- a/src/library/vm/vm_module_info.cpp +++ b/src/library/vm/vm_module_info.cpp @@ -31,6 +31,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(et_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_); @@ -65,11 +69,13 @@ static vm_obj environment_import_only_until_decl(vm_obj const & env_, vm_obj con } return to_obj(env); } + 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); From a145a05d6d81fac2644455bc2abc0e3bc0d0c4fa Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 2 Nov 2021 09:45:47 +0000 Subject: [PATCH 02/11] Update module_info.lean --- library/init/meta/module_info.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/library/init/meta/module_info.lean b/library/init/meta/module_info.lean index 0f4e65a663..e386b38264 100644 --- a/library/init/meta/module_info.lean +++ b/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 \ No newline at end of file +end environment From 230457af580125b501d00dccb7b0c8b0a2639341 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 2 Nov 2021 09:47:11 +0000 Subject: [PATCH 03/11] Update module_info.lean --- tests/lean/module_info.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tests/lean/module_info.lean b/tests/lean/module_info.lean index a06864f2ed..3a87a470ca 100644 --- a/tests/lean/module_info.lean +++ b/tests/lean/module_info.lean @@ -1,5 +1,7 @@ open tactic +#eval module_info.get_all + #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) \ No newline at end of file +set_env_core $ e.import' (module_info.of_module_name `data.dlist) From 76765db8b436628b8d9a5720f52f90e1ff21c056 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 2 Nov 2021 09:48:00 +0000 Subject: [PATCH 04/11] Update vm_module_info.cpp --- src/library/vm/vm_module_info.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/vm/vm_module_info.cpp b/src/library/vm/vm_module_info.cpp index 791634e06b..1d25664a94 100644 --- a/src/library/vm/vm_module_info.cpp +++ b/src/library/vm/vm_module_info.cpp @@ -32,7 +32,7 @@ static vm_obj module_info_id(vm_obj const & mi_) { } static vm_obj module_info_get_all() { - return to_obj(et_global_module_mgr()->get_all_modules()); + return to_obj(get_global_module_mgr()->get_all_modules()); } static vm_obj environment_import_dependencies(vm_obj const & env_, vm_obj const & mi_) { From c5d73e2d9a2d18a6a1093ef7b1a5029321e74d1a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 4 Nov 2021 14:26:30 +0000 Subject: [PATCH 05/11] Add a vector to object conversion --- src/library/vm/vm_list.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/library/vm/vm_list.h b/src/library/vm/vm_list.h index 4d90fd5c32..947ac32da3 100644 --- a/src/library/vm/vm_list.h +++ b/src/library/vm/vm_list.h @@ -45,6 +45,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 +vm_obj to_obj(vector const & ls) { + vm_obj obj = mk_vm_nil(); + for (unsigned i = ls.size(); i > 0; i--) + obj = mk_vm_cons(to_obj(ls[i - 1]), obj); + return obj; +} + template list to_list(vm_obj const & o, F const & fn) { if (is_simple(o)) { From a1272f5116ae8592998c4be10cc3263e8ef73ec7 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 4 Nov 2021 14:28:44 +0000 Subject: [PATCH 06/11] auto --- src/library/vm/vm_list.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/vm/vm_list.h b/src/library/vm/vm_list.h index 947ac32da3..8a11583f4f 100644 --- a/src/library/vm/vm_list.h +++ b/src/library/vm/vm_list.h @@ -48,7 +48,7 @@ inline vm_obj mk_vm_cons(vm_obj const & h, vm_obj const & t) { return mk_vm_cons template vm_obj to_obj(vector const & ls) { vm_obj obj = mk_vm_nil(); - for (unsigned i = ls.size(); i > 0; i--) + for (auto i = ls.size(); i > 0; i--) obj = mk_vm_cons(to_obj(ls[i - 1]), obj); return obj; } From 2c2882fe54c4db8f796dd9f5d1beafdda575fb5d Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 4 Nov 2021 15:03:12 +0000 Subject: [PATCH 07/11] Update src/library/vm/vm_list.h --- src/library/vm/vm_list.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/vm/vm_list.h b/src/library/vm/vm_list.h index 8a11583f4f..064f8ee762 100644 --- a/src/library/vm/vm_list.h +++ b/src/library/vm/vm_list.h @@ -46,7 +46,7 @@ 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 -vm_obj to_obj(vector const & ls) { +vm_obj to_obj(std::vector 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); From d34003eb89b65de85f3bfc5437f0533109726948 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 4 Nov 2021 15:49:31 +0000 Subject: [PATCH 08/11] Update vm_module_info.cpp --- src/library/vm/vm_module_info.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/library/vm/vm_module_info.cpp b/src/library/vm/vm_module_info.cpp index 1d25664a94..759c867136 100644 --- a/src/library/vm/vm_module_info.cpp +++ b/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" From c04eaa9600d486198a12a361a429337b50a5fca6 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 4 Nov 2021 16:37:10 +0000 Subject: [PATCH 09/11] Update vm_list.h --- src/library/vm/vm_list.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/library/vm/vm_list.h b/src/library/vm/vm_list.h index 064f8ee762..1922a0e010 100644 --- a/src/library/vm/vm_list.h +++ b/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 namespace lean { list to_list_name(vm_obj const & o); From 06a862da5613023b00449b3326b4e6446b0f272a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 4 Nov 2021 16:37:24 +0000 Subject: [PATCH 10/11] Update src/library/vm/vm_module_info.cpp --- src/library/vm/vm_module_info.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/library/vm/vm_module_info.cpp b/src/library/vm/vm_module_info.cpp index 759c867136..c1c088bf25 100644 --- a/src/library/vm/vm_module_info.cpp +++ b/src/library/vm/vm_module_info.cpp @@ -70,7 +70,6 @@ static vm_obj environment_import_only_until_decl(vm_obj const & env_, vm_obj con } return to_obj(env); } - void initialize_vm_module_info() { DECLARE_VM_BUILTIN(name({"module_info", "resolve_module_name"}), module_info_resolve_module_name); From 29aa29b7108d15a576f3628fc5e70709c6b7e780 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 5 Nov 2021 10:26:58 +0000 Subject: [PATCH 11/11] Update tests/lean/module_info.lean --- tests/lean/module_info.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/module_info.lean b/tests/lean/module_info.lean index 3a87a470ca..cd942029ee 100644 --- a/tests/lean/module_info.lean +++ b/tests/lean/module_info.lean @@ -1,6 +1,6 @@ open tactic -#eval module_info.get_all +run_cmd guard (module_info.get_all ≠ [] : bool) #eval (module_info.resolve_module_name `data.dlist).backn 10