max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(kernel/expr): hide get_weight and get_depth

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-03 10:51:24 -07:00
parent d2f169a211
commit 7f142ac7e3
3 changed files with 1 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/expr.h
View file

@ -145,10 +145,6 @@ bool has_univ_mvar(expr const & e);
inline bool has_mvar(expr const & e) { return has_expr_mvar(e) || has_univ_mvar(e); }
bool has_fvar(expr const & e);
bool has_univ_param(expr const & e);
unsigned expr_get_weight(object * e);
inline unsigned get_weight(expr const & e) { return expr_get_weight(e.raw()); }
unsigned expr_get_depth(object * e);
inline unsigned get_depth(expr const & e) { return expr_get_depth(e.raw()); }
unsigned expr_get_loose_bvar_range(object * e);
inline unsigned get_loose_bvar_range(expr const & e) { return expr_get_loose_bvar_range(e.raw()); }

8
src/library/expr_lt.cpp
View file

@ -10,10 +10,6 @@ Author: Leonardo de Moura
namespace lean {
bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const * lctx) {
if (is_eqp(a, b)) return false;
unsigned wa = get_weight(a);
unsigned wb = get_weight(b);
if (wa < wb) return true;
if (wa > wb) return false;
if (a.kind() != b.kind()) return a.kind() < b.kind();
if (use_hash) {
if (hash(a) < hash(b)) return true;
@ -126,10 +122,6 @@ bool is_lt_no_level_params(levels const & as, levels const & bs) {
bool is_lt_no_level_params(expr const & a, expr const & b) {
if (is_eqp(a, b)) return false;
unsigned wa = get_weight(a);
unsigned wb = get_weight(b);
if (wa < wb) return true;
if (wa > wb) return false;
if (a.kind() != b.kind()) return a.kind() < b.kind();
switch (a.kind()) {
case expr_kind::Lit:

2
src/library/type_context.h
View file

@ -520,7 +520,7 @@ private:
std::function<bool(name const & e)> const * m_transparency_pred{nullptr}; // NOLINT
static bool is_equiv_cache_target(expr const & e1, expr const & e2) {
return !has_metavar(e1) && !has_metavar(e2) && (get_weight(e1) > 1 || get_weight(e2) > 1);
return !has_metavar(e1) && !has_metavar(e2) && (!is_atomic(e1) || !is_atomic(e2));
}
bool is_cached_equiv(expr const & e1, expr const & e2) {
return is_equiv_cache_target(e1, e2) && m_cache->get_equiv(m_transparency_mode, e1, e2);