From e0ef6b2e9a07aa04cccad2bbb2bcdce2a190ac54 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 22 Feb 2014 23:09:12 -0800 Subject: [PATCH] refactor(library): monotonic total order on terms Signed-off-by: Leonardo de Moura --- src/library/CMakeLists.txt | 6 +- src/library/expr_lt.cpp | 120 +++++++++++++++++++------------------ src/library/expr_lt.h | 3 + 3 files changed, 67 insertions(+), 62 deletions(-) diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 8dbbe9f5e..341a34c9e 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,6 +1,6 @@ -add_library(library deep_copy.cpp) -# kernel_bindings.cpp deep_copy.cpp -# context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp +add_library(library deep_copy.cpp expr_lt.cpp) +# kernel_bindings.cpp +# context_to_lambda.cpp placeholder.cpp substitution.cpp # fo_unify.cpp bin_op.cpp equality.cpp io_state_stream.cpp printer.cpp # hop_match.cpp) diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp index b44da29d0..da5da3932 100644 --- a/src/library/expr_lt.cpp +++ b/src/library/expr_lt.cpp @@ -5,14 +5,45 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/expr.h" +#include "library/expr_lt.h" namespace lean { -bool is_lt(expr const & a, expr const & b, bool use_hash); -static bool is_lt(optional const & a, optional const & b, bool use_hash) { - if (is_eqp(a, b)) return false; - else if (!a && b) return true; - else if (a && !b) return false; - else return is_lt(*a, *b, use_hash); +bool is_lt(level const & a, level const & b, bool use_hash) { + if (is_eqp(a, b)) return false; + if (kind(a) != kind(b)) return kind(a) < kind(b); + if (use_hash) { + if (hash(a) < hash(b)) return true; + if (hash(a) > hash(b)) return false; + } + if (a == b) return false; + switch (kind(a)) { + case level_kind::Zero: return true; + case level_kind::Succ: return is_lt(succ_of(a), succ_of(b), use_hash); + case level_kind::Param: return param_id(a) < param_id(b); + case level_kind::Meta: return meta_id(a) < meta_id(b); + case level_kind::Max: + if (max_lhs(a) != max_lhs(b)) + return is_lt(max_lhs(a), max_lhs(b), use_hash); + else + return is_lt(max_lhs(a), max_lhs(b), use_hash); + case level_kind::IMax: + if (imax_lhs(a) != imax_lhs(b)) + return is_lt(imax_lhs(a), imax_lhs(b), use_hash); + else + return is_lt(imax_lhs(a), imax_lhs(b), use_hash); + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +bool is_lt(levels const & as, levels const & bs, bool use_hash) { + if (is_nil(as)) + return !is_nil(bs); + if (is_nil(bs)) + return false; + if (car(as) == car(bs)) + return is_lt(cdr(as), cdr(bs), use_hash); + else + return is_lt(car(as), car(bs), use_hash); } bool is_lt(expr const & a, expr const & b, bool use_hash) { @@ -27,25 +58,19 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) { if (a.hash() > b.hash()) return false; } 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(); // LCOV_EXCL_LINE + return var_idx(a) < var_idx(b); 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), use_hash); - } - lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::HEq: - if (heq_lhs(a) != heq_lhs(b)) - return is_lt(heq_lhs(a), heq_lhs(b), use_hash); + if (const_name(a) != const_name(b)) + return const_name(a) < const_name(b); else - return is_lt(heq_rhs(a), heq_rhs(b), use_hash); + return is_lt(const_level_params(a), const_level_params(b), use_hash); + case expr_kind::App: + if (app_fn(a) != app_fn(b)) + return is_lt(app_fn(a), app_fn(b), use_hash); + else + return is_lt(app_arg(a), app_arg(b), use_hash); case expr_kind::Pair: if (pair_first(a) != pair_first(b)) return is_lt(pair_first(a), pair_first(b), use_hash); @@ -53,22 +78,15 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) { return is_lt(pair_second(a), pair_second(b), use_hash); else return is_lt(pair_type(a), pair_type(b), use_hash); - case expr_kind::Proj: - if (proj_first(a) != proj_first(b)) - return proj_first(a) && !proj_first(b); // first projection is smaller than the second one. + case expr_kind::Fst: case expr_kind::Snd: + return is_lt(proj_arg(a), proj_arg(b), use_hash); + case expr_kind::Sigma: case expr_kind::Lambda: case expr_kind::Pi: + if (binder_domain(a) != binder_domain(b)) + return is_lt(binder_domain(a), binder_domain(b), use_hash); else - return is_lt(proj_arg(a), proj_arg(b), use_hash); - case expr_kind::Sigma: - case expr_kind::Lambda: - case expr_kind::Pi: // Remark: we ignore get_abs_name because we want alpha-equivalence - if (abst_domain(a) != abst_domain(b)) - return is_lt(abst_domain(a), abst_domain(b), use_hash); - else - return is_lt(abst_body(a), abst_body(b), use_hash); - case expr_kind::Type: - return ty_level(a) < ty_level(b); - case expr_kind::Value: - return to_value(a) < to_value(b); + return is_lt(binder_body(a), binder_body(b), use_hash); + case expr_kind::Sort: + return is_lt(sort_level(a), sort_level(b), use_hash); case expr_kind::Let: if (let_type(a) != let_type(b)) { return is_lt(let_type(a), let_type(b), use_hash); @@ -77,29 +95,13 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) { } else { return is_lt(let_body(a), let_body(b), use_hash); } - case expr_kind::MetaVar: - if (metavar_name(a) != metavar_name(b)) { - return metavar_name(a) < metavar_name(b); - } else { - auto it1 = metavar_lctx(a).begin(); - auto it2 = metavar_lctx(b).begin(); - auto end1 = metavar_lctx(a).end(); - auto end2 = metavar_lctx(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(), use_hash); - } else { - if (it1->n() != it2->n()) - return it1->n() < it2->n(); - } - } - return it1 == end1 && it2 != end2; - } + case expr_kind::Local: case expr_kind::Meta: + if (mlocal_name(a) != mlocal_name(b)) + return mlocal_name(a) < mlocal_name(b); + else + return is_lt(mlocal_type(a), mlocal_type(b), use_hash); + case expr_kind::Macro: + return to_macro(a) < to_macro(b); } lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/src/library/expr_lt.h b/src/library/expr_lt.h index cbd70b437..301f650bf 100644 --- a/src/library/expr_lt.h +++ b/src/library/expr_lt.h @@ -19,4 +19,7 @@ inline bool operator<(expr const & a, expr const & b) { return is_lt(a, b, true inline bool operator>(expr const & a, expr const & b) { return is_lt(b, a, true); } inline bool operator<=(expr const & a, expr const & b) { return !is_lt(b, a, true); } inline bool operator>=(expr const & a, expr const & b) { return !is_lt(a, b, true); } + +bool is_lt(level const & a, level const & b, bool use_hash); +bool is_lt(levels const & as, levels const & bs, bool use_hash); }