Add more tests. Fix bug in universe implication test.

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

src/kernel/environment.cpp

@@ -40,26 +40,26 @@ struct environment::imp {
     }
 
     /** \brief Return true iff l1 >= l2 + k */
-    bool is_implied(level const & l1, level const & l2, int k) {
+    bool is_ge(level const & l1, level const & l2, int k) {
         switch (kind(l2)) {
         case level_kind::UVar:
             switch (kind(l1)) {
             case level_kind::UVar: {
                 unsigned d = m_uvar_distances[uvar_idx(l1)][uvar_idx(l2)];
-                return k >= 0 && d != uninit && d >= static_cast<unsigned>(k);
+                return d != uninit && (k < 0 || (k >= 0 && d >= static_cast<unsigned>(k)));
             }
-            case level_kind::Lift: return is_implied(lift_of(l1), l2, sub(k, lift_offset(l1)));
+            case level_kind::Lift: return is_ge(lift_of(l1), l2, sub(k, lift_offset(l1)));
-            case level_kind::Max:  return is_implied(max_level1(l1), l2, k) || is_implied(max_level2(l1), l2, k);
+            case level_kind::Max:  return is_ge(max_level1(l1), l2, k) || is_ge(max_level2(l1), l2, k);
             }
-        case level_kind::Lift: return is_implied(l1, lift_of(l2), add(k, lift_offset(l2)));
+        case level_kind::Lift: return is_ge(l1, lift_of(l2), add(k, lift_offset(l2)));
-        case level_kind::Max:  return is_implied(l1, max_level1(l2), k) && is_implied(l1, max_level2(l2), k);
+        case level_kind::Max:  return is_ge(l1, max_level1(l2), k) && is_ge(l1, max_level2(l2), k);
         }
         lean_unreachable();
         return false;
     }
 
-    bool is_implied(level const & l1, level const & l2) {
+    bool is_ge(level const & l1, level const & l2) {
-        return is_implied(l1, l2, 0);
+        return is_ge(l1, l2, 0);
     }
 
     level add_var(name const & n) {
@@ -151,8 +151,8 @@ level environment::define_uvar(name const & n, level const & l) {
     return m_imp->define_uvar(n, l);
 }
 
-bool environment::is_implied(level const & l1, level const & l2) const {
+bool environment::is_ge(level const & l1, level const & l2) const {
-    return m_imp->is_implied(l1, l2);
+    return m_imp->is_ge(l1, l2);
 }
 
 void environment::display_uvars(std::ostream & out) const {

src/kernel/environment.h

@@ -36,7 +36,7 @@ public:
        \brief Return true iff the constraint l1 >= l2 is implied by the constraints
        in the environment.
     */
-    bool is_implied(level const & l1, level const & l2) const;
+    bool is_ge(level const & l1, level const & l2) const;
 
     void display_uvars(std::ostream & out) const;
 };

src/kernel/level.cpp

@@ -85,4 +85,14 @@ std::ostream & operator<<(std::ostream & out, level const & l) {
     }
     return out;
 }
+
+level max(std::initializer_list<level> const & l) {
+    lean_assert(l.size() >= 1);
+    auto it = l.begin();
+    level r = *it;
+    ++it;
+    for (; it != l.end(); ++it)
+        r = max(r, *it);
+    return r;
+}
 }

src/kernel/level.h

@@ -46,6 +46,7 @@ public:
     friend std::ostream & operator<<(std::ostream & out, level const & l);
 };
 inline level max(level const & l1, level const & l2) { return level(l1, l2); }
+       level max(std::initializer_list<level> const & l);
 inline level operator+(level const & l, unsigned k)  { return level(l, k); }
 inline bool is_uvar(level const & l) { return kind(l) == level_kind::UVar;  }
 inline bool is_lift(level const & l) { return kind(l) == level_kind::Lift; }

src/tests/kernel/level.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <locale>
 #include "environment.h"
+#include "exception.h"
 #include "test.h"
 using namespace lean;
 
@@ -16,12 +17,68 @@ static void tst1() {
     level l3 = env.define_uvar("l3", max(l2, l1 + 3));
     level l4 = env.define_uvar("l4", max(l1 + 8, max(l2 + 2, l3 + 20)));
     env.display_uvars(std::cout);
-    lean_assert(env.is_implied(l4 + 10, l3 + 30));
+    lean_assert(env.is_ge(l4 + 10, l3 + 30));
-    lean_assert(!env.is_implied(l4 + 9, l3 + 30));
+    lean_assert(!env.is_ge(l4 + 9, l3 + 30));
+}
+
+static void tst2() {
+    environment env;
+    level l1 = env.define_uvar("l1", level());
+    try {
+        level l2 = env.define_uvar("l1", level());
+        lean_unreachable();
+    }
+    catch (exception ex) {
+        std::cout << "ok\n";
+    }
+}
+
+static void tst3() {
+    environment env;
+    level l1 = env.define_uvar("l1", level());
+    level l2 = env.define_uvar("l2", level(l1, (1<<30) + 1024));
+    try {
+        level l3 = env.define_uvar("l3", level(l2, 1<<30));
+        lean_unreachable();
+    }
+    catch (exception ex) {
+        std::cout << "ok\n";
+    }
+}
+
+static void tst4() {
+    environment env;
+    level l1 = env.define_uvar("l1", level() + 1);
+    level l2 = env.define_uvar("l2", level() + 1);
+    level l3 = env.define_uvar("l3", max(l1, l2) + 1);
+    level l4 = env.define_uvar("l4", l3 + 1);
+    level l5 = env.define_uvar("l5", l3 + 1);
+    level l6 = env.define_uvar("l6", max(l4, l5) + 1);
+    lean_assert(!env.is_ge(l5 + 1, l6));
+    lean_assert(env.is_ge(l6, l5));
+    lean_assert(env.is_ge(l6, max({l1, l2, l3, l4, l5})));
+    lean_assert(env.is_ge(l6, l6));
+    lean_assert(!env.is_ge(l5, l4));
+    lean_assert(env.is_ge(max({l1, l2, l4, l5}), max({l1, l2, l3, l4, l5})));
+    lean_assert(env.is_ge(max({l4, l5}), max({l1, l2, l3})));
+    lean_assert(!env.is_ge(max({l1, l2, l5}), max({l1, l2, l3, l4, l5})));
+    lean_assert(!env.is_ge(max({l2, l4}), max({l1, l2, l3, l4, l5})));
+    lean_assert(env.is_ge(max(l2, l3) + 1, max(l1, l1+1)));
+    lean_assert(env.is_ge(max(l2, l3) + 1, max(l1+2, l1+1)));
+    lean_assert(env.is_ge(max(l2, l3) + 1, max(l2+2, l1+1)));
+    lean_assert(!env.is_ge(max(l4, l5) + 1, max(l2+4, l1+1)));
+    lean_assert(!env.is_ge(max(l6, l5), max(l2+4, l1+1)));
+    lean_assert(env.is_ge(max(l6, l5), max(l2+3, l1+1)));
+    lean_assert(!env.is_ge(max(l6, l5), max(l2, l1+1)+3));
+    lean_assert(env.is_ge(max(l6+1, l5), max(l2, l1+1)+3));
+    env.display_uvars(std::cout);
 }
 
 int main() {
     continue_on_violation(true);
     tst1();
+    tst2();
+    tst3();
+    tst4();
     return has_violations() ? 1 : 0;
 }