michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/kernel_bindings): used 'named' parameters in import_modules API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-29 11:03:44 -07:00
parent ade5d99023
commit bfa9b90af0
4 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/kernel_bindings.cpp
View file

@ -1170,12 +1170,12 @@ static int import_modules(environment const & env, lua_State * L, int s) {
to_string_buffer(L, s, mnames);
unsigned num_threads = 1;
bool keep_proofs = false;
if (nargs > s)
num_threads = lua_tonumber(L, s+1);
if (nargs > s+1)
keep_proofs = lua_toboolean(L, s+2);
if (nargs > s+2 && is_io_state(L, s+3))
return push_environment(L, import_modules(env, mnames.size(), mnames.data(), num_threads, keep_proofs, to_io_state(L, s+3)));
if (nargs > s) {
num_threads = get_uint_named_param(L, s+1, "num_threads", num_threads);
keep_proofs = get_bool_named_param(L, s+1, "keep_proofs", keep_proofs);
}
if (nargs > s+1 && is_io_state(L, s+2))
return push_environment(L, import_modules(env, mnames.size(), mnames.data(), num_threads, keep_proofs, to_io_state(L, s+2)));
else
return push_environment(L, import_modules(env, mnames.size(), mnames.data(), num_threads, keep_proofs, get_io_state(L)));
}

2
tests/lua/mod1.lua
View file

@ -8,7 +8,7 @@ assert(env:get("H2"):is_theorem())
env = add_decl(env, mk_definition("B", Bool, A))
env:export("mod1_mod.olean")
local env2 = import_modules("mod1_mod.olean", 1, true)
local env2 = import_modules("mod1_mod.olean", {keep_proofs=true})
assert(env2:get("A"):type() == Bool)
assert(env2:get("A"):is_var_decl())
assert(env2:get("H1"):type() == A)

2
tests/lua/mod5.lua
View file

@ -13,7 +13,7 @@ function mk_module(midx, imports)
for i = 1, #imports do
imp_names[#imp_names + 1] = mod_name(imports[i])
end
local env = import_modules(imp_names, NumThreads)
local env = import_modules(imp_names, {num_threads=NumThreads})
if #imports == 0 then
env = add_decl(env, mk_var_decl(const_name(midx), Bool))
env = add_decl(env, mk_var_decl("and", mk_arrow(Bool, Bool, Bool)))

2
tests/lua/slow/mod2.lua
View file

@ -37,7 +37,7 @@ end
print("importing...")
local initt = os.clock()
local env2 = import_modules(mod_names, 4, true)
local env2 = import_modules(mod_names, {num_threads=4, keep_proofs=true})
print(string.format("elapsed time: %.2f\n", os.clock() - initt))
for i = 1, NumMods do
for j = 1, NumThs do