refactor(library/kernel_bindings): rename empty_environment ==> bare_environment in the Lua API

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

src/library/kernel_bindings.cpp

@@ -1106,7 +1106,7 @@ static int environment_add(lua_State * L) {
         return push_environment(L, to_environment(L, 1).add(to_certified_declaration(L, 2)));
 }
 static int environment_replace(lua_State * L) { return push_environment(L, to_environment(L, 1).replace(to_certified_declaration(L, 2))); }
-static int mk_empty_environment(lua_State * L) {
+static int mk_bare_environment(lua_State * L) {
     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 prop_proof_irrel = get_bool_named_param(L, 1, "prop_proof_irrel", true);
@@ -1206,7 +1206,7 @@ static void open_environment(lua_State * L) {
     lua_setfield(L, -2, "__index");
     setfuncs(L, environment_m, 0);
 
-    SET_GLOBAL_FUN(mk_empty_environment,   "empty_environment");
+    SET_GLOBAL_FUN(mk_bare_environment,    "bare_environment");
     SET_GLOBAL_FUN(mk_environment,         "environment");
     SET_GLOBAL_FUN(environment_pred,       "is_environment");
     SET_GLOBAL_FUN(get_environment,        "get_environment");

tests/lua/def1.lua

@@ -41,7 +41,7 @@ assert(not d3:opaque())
 assert(d3:weight() == 100)
 assert(d3:module_idx() == 10)
 assert(not d3:use_conv_opt())
-local env = empty_environment()
+local env = bare_environment()
 local d4  = mk_definition(env, "bool", Type, Bool)
 assert(d4:weight() == 1)
 local d5  = mk_definition(env, "bool", Type, Bool, {opaque=false, weight=100, module_idx=3, use_conv_opt=true})

tests/lua/env1.lua

@@ -1,4 +1,4 @@
-local env = empty_environment()
+local env = bare_environment()
 assert(is_environment(env))
 assert(not env:is_global_level("U"))
 local env2 = env:add_global_level("U")

tests/lua/env2.lua

@@ -1,9 +1,9 @@
-assert(not empty_environment({eta=false}):eta())
-assert(empty_environment({eta=true}):eta())
-assert(not empty_environment({prop_proof_irrel=false}):prop_proof_irrel())
-assert(empty_environment({prop_proof_irrel=true}):prop_proof_irrel())
-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)
+assert(not bare_environment({eta=false}):eta())
+assert(bare_environment({eta=true}):eta())
+assert(not bare_environment({prop_proof_irrel=false}):prop_proof_irrel())
+assert(bare_environment({prop_proof_irrel=true}):prop_proof_irrel())
+assert(bare_environment({impredicative=true}):impredicative())
+assert(not bare_environment({impredicative=false}):impredicative())
+assert(bare_environment({trust_lvl=10}):trust_lvl() == 10)
+assert(bare_environment({trust_lvl=0}):trust_lvl() == 0)
+assert(bare_environment():trust_lvl() == 0)

tests/lua/env3.lua

@@ -9,12 +9,12 @@ local And = Const("And")
 local p   = Const("p")
 local q   = Const("q")
 
-local env = init(empty_environment())
+local env = init(bare_environment())
 local t   = type_checker(env)
 assert(t:is_def_eq(p, q))
 assert(t:is_def_eq(And(p, q), And(q, p)))
 
-env = init(empty_environment({prop_proof_irrel=false}))
+env = init(bare_environment({prop_proof_irrel=false}))
 t   = type_checker(env)
 assert(not t:is_def_eq(p, q))
 assert(not t:is_def_eq(And(p, q), And(q, p)))

tests/lua/env4.lua

@@ -1,4 +1,4 @@
-local env = empty_environment()
+local env = bare_environment()
 env = add_decl(env, mk_var_decl("A", Bool))
 local c1  = type_check(env, mk_axiom("p", Const("A")))
 local c2  = type_check(env, mk_axiom("q", Const("A")))

tests/lua/env5.lua

@@ -1,4 +1,4 @@
-local env    = empty_environment()
+local env    = bare_environment()
 local l_name = name("l")
 local l      = mk_param_univ(l_name)
 local U_l    = mk_sort(l)

tests/lua/env6.lua

@@ -1,4 +1,4 @@
-local env = empty_environment()
+local env = bare_environment()
 env = add_decl(env, mk_var_decl("A", Bool))
 local A   = Const("A")
 local x   = Const("x")

tests/lua/env7.lua

@@ -1,4 +1,4 @@
-local env1 = empty_environment()
+local env1 = bare_environment()
 local env2 = add_decl(env1, mk_var_decl("A", Type))
 assert(env2:is_descendant(env1))
 assert(env2:is_descendant(env2))

tests/lua/env9.lua

@@ -1,11 +1,11 @@
-local env = empty_environment()
+local env = bare_environment()
 -- Trust level is set to 0 by default. Then, we must type check a
 -- definition, before adding it to the environment
 assert(not pcall(function() env:add(mk_var_decl("A", Bool)) end))
 -- The function check produces a "certified declaration".
 env:add(check(env, mk_var_decl("A", Bool)))
 
-local env = empty_environment({trust_level = 10000000})
+local env = bare_environment({trust_level = 10000000})
 -- Now, env has trust_level > LEAN_BELIEVER_TRUST_LEVEL, then we can
 -- add declarations without type checking them.
 env:add(mk_var_decl("A", Bool))

tests/lua/eta.lua

@@ -1,4 +1,4 @@
-local env = empty_environment()
+local env = bare_environment()
 env = add_decl(env, mk_var_decl("f", mk_arrow(Bool, mk_arrow(Bool, Bool))))
 local f   = Const("f")
 local x   = Const("x")

tests/lua/hott1.lua

@@ -3,7 +3,7 @@
 --    Type.{0} is predicative
 --    No proof irrelevance for Type.{0}
 --    Proof irrelevance for Id types
-local env = empty_environment({prop_proof_irrel=false, impredicative=false, cls_proof_irrel={"Id"}})
+local env = bare_environment({prop_proof_irrel=false, impredicative=false, cls_proof_irrel={"Id"}})
 assert(not env:prop_proof_irrel())
 assert(not env:impredicative())
 assert(env:cls_proof_irrel():head() == name("Id"))

tests/lua/ind2.lua

@@ -102,7 +102,7 @@ bad_add_inductive(env,
                   "zero2", Nat2,
                   "succ2", Pi(a, Nat2, mk_arrow(eq(Nat2, a, a), Nat2)))
 
-local env      = empty_environment()
+local env      = bare_environment()
 bad_add_inductive(env, -- Environment does not support inductive datatypes
                   "nat", Type,
                   "zero", Nat,

tests/lua/jst1.lua

@@ -1,7 +1,7 @@
 assert(is_justification(justification()))
 assert(justification():is_none())
 assert(justification("simple"):is_asserted())
-local env = empty_environment()
+local env = bare_environment()
 local f = Const("f")
 local g = Const("g")
 local a = Const("a")

tests/lua/let1.lua

@@ -1,5 +1,5 @@
 assert(not mk_let("a", Type, Var(0), Var(0)):closed())
-local env = empty_environment()
+local env = bare_environment()
 local A   = Const("A")
 env = add_decl(env, mk_var_decl("A", Type))
 env = add_decl(env, mk_var_decl("g", mk_arrow(A, mk_arrow(A, A))))

tests/lua/res1.lua

@@ -77,7 +77,7 @@ function assert_some_axioms(env)
    return env
 end
 
-local env = empty_environment({trust_lvl=1})
+local env = bare_environment({trust_lvl=1})
 env = init_env(env)
 env = assert_some_axioms(env)
 
@@ -116,7 +116,7 @@ print(tostring(Pr4) .. " : " .. tostring(tc:check(Pr4)))
 
 print("----------------")
 print("Type checking again, but using trust_lvl=0, macros will be expanded during type checking")
-local env = empty_environment({trust_lvl=0})
+local env = bare_environment({trust_lvl=0})
 env = init_env(env)
 env = assert_some_axioms(env)
 local tc  = type_checker(env)

tests/lua/tc1.lua

@@ -1,4 +1,4 @@
-local env = empty_environment()
+local env = bare_environment()
 local g   = name_generator("tst")
 local tc  = type_checker(env, g)
 assert(is_type_checker(tc))

tests/lua/tc2.lua

@@ -1,4 +1,4 @@
-local env = empty_environment()
+local env = bare_environment()
 local l      = mk_param_univ("l")
 local A      = Const("A")
 local a      = Const("a")

tests/lua/tc3.lua

@@ -1,4 +1,4 @@
-local env = empty_environment()
+local env = bare_environment()
 local t1  = mk_lambda("A", Type, mk_lambda("a", Var(0), Var(0)), binder_info(true))
 local t2  = mk_lambda("A", Type, mk_lambda("a", Var(0), Var(0)))
 print(t1)

tests/lua/tc4.lua

@@ -1,4 +1,4 @@
-local env = empty_environment()
+local env = bare_environment()
 env = add_decl(env, mk_var_decl("or", mk_arrow(Bool, Bool, Bool)))
 env = add_decl(env, mk_var_decl("A", Bool))
 local Or = Const("or")

tests/lua/tc5.lua

@@ -1,4 +1,4 @@
-local env = empty_environment()
+local env = bare_environment()
 env = add_decl(env, mk_var_decl("A", Bool))
 env = add_decl(env, mk_var_decl("T", Type))
 env = add_decl(env, mk_definition("B2", Type, Bool, {opaque=false}))
@@ -42,6 +42,6 @@ assert(not pcall(function()
 
 assert(tc:check(mk_pi("x", Bool, Var(0))) == Bool)
 
-local env = empty_environment({impredicative=false})
+local env = bare_environment({impredicative=false})
 local tc = type_checker(env)
 assert(tc:check(mk_pi("x", Bool, Var(0))) == Type)

tests/lua/threads/th2.lua

@@ -11,7 +11,7 @@ code = [[
 ]]
 S1:dostring(code)
 S2:dostring(code)
-local e = empty_environment()
+local e = bare_environment()
 e = add_decl(e, mk_var_decl("N", Type))
 code2 = [[
   e, prefix = ...

tests/lua/threads/th5.lua

@@ -9,7 +9,7 @@ local val = 10
 S:eval([[ local f = ...; assert(f(1) == 11) ]], function (x) return x + val end)
 S:eval([[ local o = ...; assert(o == name("a")) ]], name("a"))
 S:eval([[ local o = ...; assert(o == Const("a")) ]], Const("a"))
-S:eval([[ local o = ...; assert(is_environment(o)) ]], empty_environment())
+S:eval([[ local o = ...; assert(is_environment(o)) ]], bare_environment())
 S:eval([[ local o = ...; assert(o == mpz(100)) ]], mpz(100))
 S:eval([[ local o = ...; assert(o == mpq(100)/3) ]], mpq(100)/3)
 S:eval([[ local o = ...; assert(is_options(o)) ]], options())