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

feat(library/kernel_bindings): add optional arguments to empty_environment Lua API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-07 17:06:27 -07:00
parent 4c5f88e63b
commit 62db010ba3
2 changed files with 31 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/library/kernel_bindings.cpp
View file

@ -841,22 +841,30 @@ static int environment_get(lua_State * L) { return push_definition(L, to_environ
static int environment_add(lua_State * L) { return push_environment(L, to_environment(L, 1).add(to_certified_definition(L, 2))); } static int environment_add(lua_State * L) { return push_environment(L, to_environment(L, 1).add(to_certified_definition(L, 2))); }
static int environment_replace(lua_State * L) { return push_environment(L, to_environment(L, 1).replace(to_certified_definition(L, 2))); } static int environment_replace(lua_State * L) { return push_environment(L, to_environment(L, 1).replace(to_certified_definition(L, 2))); }
static int mk_empty_environment(lua_State * L) { static int mk_empty_environment(lua_State * L) {
return push_environment(L, environment()); unsigned trust_lvl = get_uint_named_param(L, 1, "trust_lvl", 0);
trust_lvl = get_uint_named_param(L, 1, "trust_level", trust_lvl);
bool proof_irrel = get_bool_named_param(L, 1, "proof_irrel", true);
proof_irrel = get_bool_named_param(L, 1, "proof_irrelevance", proof_irrel);
bool eta = get_bool_named_param(L, 1, "eta", true);
bool impredicative = get_bool_named_param(L, 1, "impredicative", true);
return push_environment(L, environment(trust_lvl, proof_irrel, eta, impredicative));
} }
static const struct luaL_Reg environment_m[] = { static const struct luaL_Reg environment_m[] = {
{"__gc", environment_gc}, // never throws {"__gc", environment_gc}, // never throws
{"is_descendant", safe_function<environment_is_descendant>}, {"is_descendant", safe_function<environment_is_descendant>},
{"trust_lvl", safe_function<environment_trust_lvl>}, {"trust_lvl", safe_function<environment_trust_lvl>},
{"proof_irrel", safe_function<environment_proof_irrel>}, {"trust_level", safe_function<environment_trust_lvl>},
{"eta", safe_function<environment_eta>}, {"proof_irrel", safe_function<environment_proof_irrel>},
{"impredicative", safe_function<environment_impredicative>}, {"proof_irrelevance", safe_function<environment_proof_irrel>},
{"add_global_level", safe_function<environment_add_global_level>}, {"eta", safe_function<environment_eta>},
{"is_global_level", safe_function<environment_is_global_level>}, {"impredicative", safe_function<environment_impredicative>},
{"find", safe_function<environment_find>}, {"add_global_level", safe_function<environment_add_global_level>},
{"get", safe_function<environment_get>}, {"is_global_level", safe_function<environment_is_global_level>},
{"add", safe_function<environment_add>}, {"find", safe_function<environment_find>},
{"replace", safe_function<environment_replace>}, {"get", safe_function<environment_get>},
{"add", safe_function<environment_add>},
{"replace", safe_function<environment_replace>},
{0, 0} {0, 0}
}; };

10
tests/lua/env2.lua Normal file
View file

@ -0,0 +1,10 @@
assert(not empty_environment({eta=false}):eta())
assert(empty_environment({eta=true}):eta())
assert(not empty_environment({proof_irrel=false}):proof_irrel())
assert(not empty_environment({proof_irrel=false}):proof_irrelevance())
assert(empty_environment({proof_irrel=true}):proof_irrelevance())
assert(empty_environment({impredicative=true}):impredicative())
assert(not empty_environment({impredicative=false}):impredicative())
assert(empty_environment({trust_lvl=10}):trust_lvl() == 10)
assert(empty_environment({trust_lvl=0}):trust_lvl() == 0)
assert(empty_environment():trust_lvl() == 0)