Implement total order on expressions

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

src/kernel/expr.cpp

@@ -111,6 +111,12 @@ name value::get_unicode_name() const { return get_name(); }
 bool value::normalize(unsigned, expr const *, expr &) const { return false; }
 void value::display(std::ostream & out) const { out << get_name(); }
 bool value::operator==(value const & other) const { return typeid(*this) == typeid(other); }
+bool value::operator<(value const & other) const {
+    if (get_name() == other.get_name())
+        return lt(other);
+    else
+        return get_name() < other.get_name();
+}
 format value::pp() const { return format(get_name()); }
 format value::pp(bool unicode) const { return unicode ? format(get_unicode_name()) : pp(); }
 unsigned value::hash() const { return get_name().hash(); }

src/kernel/expr.h

@@ -221,6 +221,13 @@ public:
 class value {
     void dealloc() { delete this; }
     MK_LEAN_RC();
+protected:
+    /**
+        \brief Auxiliary method used for implementing a total order on semantic
+        attachments. It is invoked by operator<, and it is only invoked when
+        <tt>get_name() == other.get_name()</tt>
+    */
+    virtual bool lt(value const &) const { return false; }
 public:
     value():m_rc(0) {}
     virtual ~value() {}
@@ -229,6 +236,7 @@ public:
     virtual name get_unicode_name() const;
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const;
     virtual bool operator==(value const & other) const;
+    bool operator<(value const & other) const;
     virtual void display(std::ostream & out) const;
     virtual format pp() const;
     virtual format pp(bool unicode) const;

src/kernel/level.cpp

@@ -181,6 +181,27 @@ bool operator==(level const & l1, level const & l2) {
     return false;
 }
 
+bool operator<(level const & l1, level const & l2) {
+    if (kind(l1) != kind(l2)) return kind(l1) < kind(l2);
+    switch (kind(l1)) {
+    case level_kind::UVar: return uvar_name(l1) < uvar_name(l2);
+    case level_kind::Lift:
+        if (lift_of(l1)  != lift_of(l2))
+            return lift_of(l1) < lift_of(l2);
+        else
+            return lift_offset(l1) < lift_offset(l2);
+    case level_kind::Max:
+        if (max_size(l1) != max_size(l2))
+            return max_size(l1) < max_size(l2);
+        for (unsigned i = 0; i < max_size(l1); i++)
+            if (max_level(l1, i) != max_level(l2, i))
+                return max_level(l1, i) < max_level(l2, i);
+        return false;
+    }
+    lean_unreachable();
+    return false;
+}
+
 std::ostream & operator<<(std::ostream & out, level const & l) {
     switch (kind(l)) {
     case level_kind::UVar: out << uvar_name(l);                        return out;

src/kernel/level.h

@@ -51,6 +51,7 @@ public:
 
     friend bool operator==(level const & l1, level const & l2);
     friend bool operator!=(level const & l1, level const & l2) { return !operator==(l1, l2); }
+    friend bool operator<(level const & l1, level const & l2);
     friend void swap(level & l1, level & l2) { std::swap(l1, l2); }
 
     friend std::ostream & operator<<(std::ostream & out, level const & l);

src/library/CMakeLists.txt

@@ -1,5 +1,6 @@
 add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp
   printer.cpp formatter.cpp context_to_lambda.cpp
   state.cpp update_expr.cpp kernel_exception_formatter.cpp
-  reduce.cpp light_checker.cpp placeholder.cpp ho_unifier.cpp)
+  reduce.cpp light_checker.cpp placeholder.cpp ho_unifier.cpp
+  expr_lt.cpp)
 target_link_libraries(library ${LEAN_LIBS})

src/library/arith/int.cpp

@@ -23,6 +23,10 @@ expr mk_int_type() { return Int; }
 
 class int_value_value : public value {
     mpz m_val;
+protected:
+    virtual bool lt(value const & other) const {
+        return m_val < static_cast<int_value_value const &>(other).m_val;
+    }
 public:
     int_value_value(mpz const & v):m_val(v) {}
     virtual ~int_value_value() {}

src/library/arith/nat.cpp

@@ -22,6 +22,10 @@ expr mk_nat_type() { return Nat; }
 
 class nat_value_value : public value {
     mpz m_val;
+protected:
+    virtual bool lt(value const & other) const {
+        return m_val < static_cast<nat_value_value const &>(other).m_val;
+    }
 public:
     nat_value_value(mpz const & v):m_val(v) { lean_assert(v >= 0); }
     virtual ~nat_value_value() {}

src/library/arith/real.cpp

@@ -26,6 +26,10 @@ expr mk_real_type() { return Real; }
 */
 class real_value_value : public value {
     mpq m_val;
+protected:
+    virtual bool lt(value const & other) const {
+        return m_val < static_cast<real_value_value const &>(other).m_val;
+    }
 public:
     real_value_value(mpq const & v):m_val(v) {}
     virtual ~real_value_value() {}

src/library/expr_lt.cpp

@@ -0,0 +1,80 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/expr.h"
+
+namespace lean {
+bool is_lt(expr const & a, expr const & b) {
+    if (is_eqp(a, b))         return false;
+    if (!a && b)              return true;  // the null expression is the smallest one
+    if (a && !b)              return false;
+    if (a.kind() != b.kind()) return a.kind() < b.kind();
+    if (a == b)               return false;
+    if (is_var(a))            return var_idx(a) < var_idx(b);
+    switch (a.kind()) {
+    case expr_kind::Var:
+        lean_unreachable(); return true; // LCOV_EXCL_LINE
+    case expr_kind::Constant:
+        return const_name(a) < const_name(b);
+    case expr_kind::App:
+        if (num_args(a) != num_args(b))
+            return num_args(a) < num_args(b);
+        for (unsigned i = 0; i < num_args(a); i++) {
+            if (arg(a, i) != arg(b, i))
+                return is_lt(arg(a, i), arg(b, i));
+        }
+        return false;
+    case expr_kind::Eq:
+        if (eq_lhs(a) != eq_lhs(b))
+            return is_lt(eq_lhs(a), eq_lhs(b));
+        else
+            return is_lt(eq_rhs(a), eq_rhs(b));
+    case expr_kind::Lambda:   // Remark: we ignore get_abs_name because we want alpha-equivalence
+    case expr_kind::Pi:
+        if (abst_domain(a) != abst_domain(b))
+            return is_lt(abst_domain(a), abst_domain(b));
+        else
+            return is_lt(abst_body(a), abst_body(b));
+    case expr_kind::Type:
+        return ty_level(a) < ty_level(b);
+    case expr_kind::Value:
+        return to_value(a) < to_value(b);
+    case expr_kind::Let:
+        if (let_type(a) != let_type(b)) {
+            return is_lt(let_type(a), let_type(b));
+        } else if (let_value(a) != let_value(b)){
+            return is_lt(let_value(a), let_value(b));
+        } else {
+            return is_lt(let_body(a), let_body(b));
+        }
+    case expr_kind::MetaVar:
+        if (metavar_idx(a) != metavar_idx(b)) {
+            return metavar_idx(a) < metavar_idx(b);
+        } else {
+            auto it1  = metavar_ctx(a).begin();
+            auto it2  = metavar_ctx(b).begin();
+            auto end1 = metavar_ctx(a).end();
+            auto end2 = metavar_ctx(b).end();
+            for (; it1 != end1 && it2 != end2; ++it1, ++it2) {
+                if (it1->kind() != it2->kind()) {
+                    return it1->kind() < it2->kind();
+                } else if (it1->s() != it2->s()) {
+                    return it1->s() < it2->s();
+                } else if (it1->is_inst()) {
+                    if (it1->v() != it2->v())
+                        return is_lt(it1->v(), it2->v());
+                } else {
+                    if (it1->n() != it2->n())
+                        return it1->n() < it2->n();
+                }
+            }
+            return false;
+        }
+    }
+    lean_unreachable();  // LCOV_EXCL_LINE
+    return false;        // LCOV_EXCL_LINE
+}
+}

src/library/expr_lt.h

@@ -0,0 +1,16 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/expr.h"
+namespace lean {
+/** \brief Total order on expressions */
+bool is_lt(expr const & a, expr const & b);
+inline bool operator<(expr const & a, expr const & b)  { return is_lt(a, b); }
+inline bool operator>(expr const & a, expr const & b)  { return is_lt(b, a); }
+inline bool operator<=(expr const & a, expr const & b) { return !is_lt(b, a); }
+inline bool operator>=(expr const & a, expr const & b) { return !is_lt(a, b); }
+}

src/tests/library/CMakeLists.txt

@@ -10,3 +10,6 @@ add_test(formatter ${CMAKE_CURRENT_BINARY_DIR}/formatter)
 add_executable(max_sharing max_sharing.cpp)
 target_link_libraries(max_sharing ${EXTRA_LIBS})
 add_test(max_sharing ${CMAKE_CURRENT_BINARY_DIR}/max_sharing)
+add_executable(expr_lt expr_lt.cpp)
+target_link_libraries(expr_lt ${EXTRA_LIBS})
+add_test(expr_lt ${CMAKE_CURRENT_BINARY_DIR}/expr_lt)

src/tests/library/expr_lt.cpp

@@ -0,0 +1,71 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/test.h"
+#include "kernel/abstract.h"
+#include "kernel/builtin.h"
+#include "library/expr_lt.h"
+#include "library/arith/nat.h"
+#include "library/arith/int.h"
+#include "library/arith/real.h"
+using namespace lean;
+
+static void lt(expr const & e1, expr const & e2, bool expected) {
+    lean_assert((e1 < e2) == expected);
+    lean_assert((e1 < e2) == !(e1 == e2 || e1 > e2));
+    lean_assert((e1 < e2) == (e2 > e1));
+}
+
+static void tst1() {
+    lt(iVal(1), iVal(1), false);
+    lt(iVal(1), iVal(2), true);
+    lt(rVal(1), rVal(1), false);
+    lt(rVal(1), rVal(2), true);
+    lt(nVal(1), nVal(1), false);
+    lt(nVal(1), nVal(2), true);
+    lt(Var(0), Var(0), false);
+    lt(Var(0), Var(1), true);
+    lt(False, True, true);
+    lt(False, False, false);
+    lt(Bool, Int, true);
+    lt(Const("a"), Const("b"), true);
+    lt(Const("a"), Const("a"), false);
+    lt(Var(1), Const("a"), true);
+    lt(expr(), Var(0), true);
+    lt(Eq(Var(0), Var(1)), Eq(Var(1), Var(1)), true);
+    lt(Eq(Var(1), Var(0)), Eq(Var(1), Var(1)), true);
+    lt(Eq(Var(1), Var(1)), Eq(Var(1), Var(1)), false);
+    lt(Eq(Var(2), Var(1)), Eq(Var(1), Var(1)), false);
+    lt(Const("f")(Var(0), Const("a")), Const("g")(Var(0), Const("a")), true);
+    lt(Const("f")(Var(0), Const("a")), Const("f")(Var(1), Const("a")), true);
+    lt(Const("f")(Var(0), Const("a")), Const("f")(Var(0), Const("b")), true);
+    lt(Const("f")(Var(0), Const("a")), Const("f")(Var(0), Const("a")), false);
+    lt(Const("g")(Var(0), Const("a")), Const("f")(Var(0), Const("a")), false);
+    lt(Const("f")(Var(1), Const("a")), Const("f")(Var(0), Const("a")), false);
+    lt(Const("f")(Var(0), Const("b")), Const("f")(Var(0), Const("a")), false);
+    lt(Type(level()), Type(level()+1), true);
+    lt(Type(level("u")), Type(level("z")), true);
+    lt(Type(level("u") + 1), Type(level("u") + 2), true);
+    lt(Type(level("u") + 1), Type(level("u") + 1), false);
+    lt(Type(max({level("u"), level("v")})), Type(max({level("u"), level("z")})), true);
+    lt(Type(max({level("u"), level("v")})), Type(max({level("u"), level("v")})), false);
+    lt(mk_lambda("x", Int, Var(0)), mk_lambda("y", Real, Var(0)), true);
+    lt(mk_lambda("x", Int, Var(0)), mk_lambda("y", Real, Var(10)), true);
+    lt(mk_lambda("x", Bool, Var(100)), mk_lambda("y", Real, Var(10)), true);
+    lt(mk_lambda("x", Int, Var(0)), mk_lambda("y", Int, Var(0)), false);
+    lt(mk_let("x", Int, iVal(10), Var(0)), mk_let("y", Real, rVal(10), Var(0)), true);
+    lt(mk_let("x", Int, iVal(10), Var(0)), mk_let("y", Int, iVal(20), Var(0)), true);
+    lt(mk_let("x", Int, iVal(10), Var(0)), mk_let("y", Int, iVal(10), Var(1)), true);
+    lt(mk_let("x", Int, iVal(10), Var(0)), mk_let("y", Int, iVal(10), Var(0)), false);
+    lt(mk_pi("x", Int, Int), mk_pi("y", Real, Bool), true);
+    lt(mk_pi("x", Int, Int), mk_pi("y", Int, Real), true);
+    lt(mk_pi("x", Int, Int), mk_pi("y", Int, Int), false);
+}
+
+int main() {
+    tst1();
+    return has_violations() ? 1 : 0;
+}