Add get_uvar method

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

src/kernel/environment.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <vector>
 #include <limits>
 #include <atomic>
+#include <sstream>
 #include "environment.h"
 #include "exception.h"
 #include "debug.h"
@@ -72,10 +73,10 @@ struct environment::imp {
     }
 
     bool is_ge(level const & l1, level const & l2) {
-        if (!has_parent())
-            return is_ge(l1, l2, 0);
-        else
+        if (has_parent())
             return m_parent->is_ge(l1, l2);
+        else
+            return is_ge(l1, l2, 0);
     }
 
     level add_var(name const & n) {
@@ -132,6 +133,21 @@ struct environment::imp {
         return r;
     }
 
+    level get_uvar(name const & n) const {
+        if (has_parent()) {
+            return m_parent->get_uvar(n);
+        } else {
+            auto it = std::find_if(m_uvars.begin(), m_uvars.end(), [&](level const & l) { return uvar_name(l) == n; });
+            if (it == m_uvars.end()) {
+                std::ostringstream s;
+                s << "unknown universe variable '" << n << "'";
+                throw exception (s.str());
+            } else {
+                return *it;
+            }
+        }
+    }
+
     void init_uvars() {
         m_uvars.push_back(level());
         m_uvar_distances.push_back(std::vector<unsigned>());
@@ -216,4 +232,8 @@ environment environment::parent() const {
     return environment(m_imp->m_parent);
 }
 
+level environment::get_uvar(name const & n) const {
+    return m_imp->get_uvar(n);
+}
+
 }

src/kernel/environment.h

@@ -48,6 +48,7 @@ public:
        Throw an exception if variable is not defined in this environment.
     */
     level get_uvar(name const & n) const;
+    level get_uvar(char const * n) const { return get_uvar(name(n)); }
 
     /**
        \brief Create a child environment. This environment will only allow "read-only" operations until

src/tests/kernel/environment.cpp

@@ -55,6 +55,7 @@ static void tst2() {
     environment parent = child.parent();
     parent.display_uvars(std::cout);
     lean_assert(parent.has_children());
+    std::cout << "uvar: " << child.get_uvar("u") << "\n";
 }
 
 int main() {