feat(kernel/environment): universe variables now live in their own namespace

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

src/kernel/environment.cpp

@@ -342,12 +342,11 @@ level environment_cell::add_uvar_cnstr(name const & n, level const & l) {
     check_consistency(n, l, 0);
     if (it == uvs.end()) {
         r = add_uvar_core(n);
-        register_named_object(mk_uvar_cnstr(n, l));
     } else {
         // universe n already exists, we must check consistency of the new constraint.
         r = *it;
-        m_objects.push_back(mk_uvar_cnstr(n, l));
     }
+    m_objects.push_back(mk_uvar_cnstr(n, l));
     add_constraints(n, l, 0);
     return r;
 }

tests/lean/lua11.lean

@@ -30,20 +30,12 @@ import Int.
  assert(found2)
  print(bs)
  assert(not bs:in_builtin_set(Const("a")))
- assert(not pcall(function() M:in_builtin_set(Const("a")) end))
 
- local M   = env:find_object("M")
- assert(not M:has_type())
- assert(not pcall(function() M:get_type() end))
- assert(M:has_cnstr_level())
- print(M:get_cnstr_level())
  assert(not pcall(function() o1:get_cnstr_level() end))
- assert(not pcall(function() M:get_value() end))
  env:add_var("x", Const("Int"))
  env:add_definition("val", Const("Int"), Const("x"))
  assert(env:find_object("val"):get_value() == Const("x"))
  assert(env:find_object("val"):get_weight() == 1)
- assert(not pcall(function() M:get_weight() end))
  assert(env:find_object("congr"):is_opaque())
  assert(env:find_object("congr"):is_theorem())
  assert(env:find_object("refl"):is_axiom())

tests/lean/lua11.lean.expected.out

@@ -3,4 +3,3 @@
   Imported 'Int'
 Int::add
 builtinset Nat::numeral
-512

tests/lean/univ3.lean

@@ -0,0 +1,7 @@
+universe Z >= 0
+definition Z := 0
+eval Z
+definition TZ := (Type Z)
+eval TZ
+definition U := 1
+eval U

tests/lean/univ3.lean.expected.out

@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Defined: Z
+0
+  Defined: TZ
+(Type Z)
+  Defined: U
+1