diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 95e18c53f..aa7dfcdf7 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -58,8 +58,8 @@ void expr_cell::dec_ref(expr & e, buffer & todelete) { } optional expr_cell::is_arrow() const { - // it is stored in bits 2-3 - unsigned r = (m_flags & (4+8)) >> 2; + // it is stored in bits 1-2 + unsigned r = (m_flags & (2+4)) >> 1; if (r == 0) { return optional(); } else if (r == 1) { @@ -71,7 +71,7 @@ optional expr_cell::is_arrow() const { } void expr_cell::set_is_arrow(bool flag) { - unsigned mask = flag ? 4 : 8; + unsigned mask = flag ? 2 : 4; m_flags |= mask; lean_assert(is_arrow() && *is_arrow() == flag); } @@ -98,9 +98,10 @@ void expr_mlocal::dealloc(buffer & todelete) { } // Composite expressions -expr_composite::expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ, unsigned d): +expr_composite::expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ, unsigned d, unsigned fv_range): expr_cell(k, h, has_mv, has_local, has_param_univ), - m_depth(d) {} + m_depth(d), + m_free_var_range(fv_range) {} // Expr applications expr_app::expr_app(expr const & fn, expr const & arg): @@ -108,7 +109,8 @@ expr_app::expr_app(expr const & fn, expr const & arg): fn.has_metavar() || arg.has_metavar(), fn.has_local() || arg.has_local(), fn.has_param_univ() || arg.has_param_univ(), - std::max(get_depth(fn), get_depth(arg)) + 1), + std::max(get_depth(fn), get_depth(arg)) + 1, + std::max(get_free_var_range(fn), get_free_var_range(arg))), m_fn(fn), m_arg(arg) {} void expr_app::dealloc(buffer & todelete) { dec_ref(m_fn, todelete); @@ -116,13 +118,16 @@ void expr_app::dealloc(buffer & todelete) { delete(this); } +static unsigned dec(unsigned k) { return k == 0 ? 0 : k - 1; } + // Expr binders (Lambda, Pi) expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const & b): expr_composite(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar(), t.has_local() || b.has_local(), t.has_param_univ() || b.has_param_univ(), - std::max(get_depth(t), get_depth(b)) + 1), + std::max(get_depth(t), get_depth(b)) + 1, + std::max(get_free_var_range(t), dec(get_free_var_range(b)))), m_name(n), m_domain(t), m_body(b) { @@ -147,7 +152,8 @@ expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & t.has_metavar() || v.has_metavar() || b.has_metavar(), t.has_local() || v.has_local() || b.has_local(), t.has_param_univ() || v.has_param_univ() || b.has_param_univ(), - std::max({get_depth(t), get_depth(v), get_depth(b)}) + 1), + std::max({get_depth(t), get_depth(v), get_depth(b)}) + 1, + std::max({get_free_var_range(t), dec(get_free_var_range(v)), dec(get_free_var_range(b))})), m_name(n), m_type(t), m_value(v), @@ -281,6 +287,21 @@ unsigned get_depth(expr const & e) { lean_unreachable(); // LCOV_EXCL_LINE } +unsigned get_free_var_range(expr const & e) { + switch (e.kind()) { + case expr_kind::Var: + return var_idx(e) + 1; + case expr_kind::Constant: case expr_kind::Sort: case expr_kind::Macro: + return 0; + case expr_kind::Meta: case expr_kind::Local: + return get_free_var_range(mlocal_type(e)); + case expr_kind::Lambda: case expr_kind::Pi: + case expr_kind::App: case expr_kind::Let: + return static_cast(e.raw())->m_free_var_range; + } + lean_unreachable(); // LCOV_EXCL_LINE +} + bool operator==(expr const & a, expr const & b) { return expr_eq_fn()(a, b); } expr update_app(expr const & e, expr const & new_fn, expr const & new_arg) { diff --git a/src/kernel/expr.h b/src/kernel/expr.h index c50e6762d..748b52445 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -45,8 +45,7 @@ protected: unsigned short m_kind; // The bits of the following field mean: // 0 - term is maximally shared - // 1 - term is closed - // 2-3 - term is an arrow (0 - not initialized, 1 - is arrow, 2 - is not arrow) + // 1-2 - term is an arrow (0 - not initialized, 1 - is arrow, 2 - is not arrow) // Remark: we use atomic_uchar because these flags are computed lazily (i.e., after the expression is created) atomic_uchar m_flags; unsigned m_has_mv:1; // term contains metavariables @@ -61,15 +60,11 @@ protected: void set_max_shared() { m_flags |= 1; } friend class max_sharing_fn; - bool is_closed() const { return (m_flags & 2) != 0; } - void set_closed() { m_flags |= 2; } - optional is_arrow() const; void set_is_arrow(bool flag); friend bool is_arrow(expr const & e); - friend class has_free_var_fn; - static void dec_ref(expr & c, buffer & todelete); + static void dec_ref(expr & c, buffer & todelete); public: expr_cell(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ); expr_kind kind() const { return static_cast(m_kind); } @@ -194,9 +189,11 @@ public: /** \brief Composite expressions */ class expr_composite : public expr_cell { unsigned m_depth; + unsigned m_free_var_range; friend unsigned get_depth(expr const & e); + friend unsigned get_free_var_range(expr const & e); public: - expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ, unsigned d); + expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ, unsigned d, unsigned fv_range); }; /** \brief Applications */ @@ -464,6 +461,17 @@ inline bool has_metavar(expr const & e) { return e.has_metavar(); } inline bool has_local(expr const & e) { return e.has_local(); } inline bool has_param_univ(expr const & e) { return e.has_param_univ(); } unsigned get_depth(expr const & e); +/** + \brief Return \c R s.t. the de Bruijn index of all free variables + occurring in \c e is in the interval [0, R). +*/ +unsigned get_free_var_range(expr const & e); +/** \brief Return true iff the given expression has free variables. */ +inline bool has_free_vars(expr const & e) { return get_free_var_range(e) > 0; } +/** \brief Return true iff the given expression does not have free variables. */ +inline bool closed(expr const & e) { return !has_free_vars(e); } +/** \brief Return true iff \c e contains a free variable >= low. */ +inline bool has_free_var_ge(expr const & e, unsigned low) { return get_free_var_range(e) > low; } // ======================================= diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 4ee956673..5d3415238 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -12,155 +12,6 @@ Author: Leonardo de Moura #include "kernel/for_each_fn.h" namespace lean { -/** - \brief Functional object for checking whether a kernel expression has free variables or not. - - \remark We assume that a metavariable contains free variables. - This is an approximation, since we don't know how the metavariable will be instantiated. -*/ -class has_free_vars_fn { -protected: - expr_cell_offset_set m_cached; - - bool apply(expr const & e, unsigned offset) { - // handle easy cases - switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Sort: case expr_kind::Macro: - return false; - case expr_kind::Var: - return var_idx(e) >= offset; - case expr_kind::App: case expr_kind::Let: - case expr_kind::Meta: case expr_kind::Local: - case expr_kind::Lambda: case expr_kind::Pi: - break; - } - - if (e.raw()->is_closed()) - return false; - - if (offset == 0) { - return apply_core(e, 0); - } else { - // The apply_core(e, 0) may seem redundant, but it allows us to - // mark nested closed expressions. - return apply_core(e, 0) && apply_core(e, offset); - } - } - - bool apply_core(expr const & e, unsigned offset) { - bool shared = false; - if (is_shared(e)) { - shared = true; - expr_cell_offset p(e.raw(), offset); - if (m_cached.find(p) != m_cached.end()) - return false; - } - - bool result = false; - - switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Sort: case expr_kind::Macro: - case expr_kind::Var: - lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Meta: case expr_kind::Local: - result = apply(mlocal_type(e), offset); - break; - case expr_kind::App: - result = apply(app_fn(e), offset) || apply(app_arg(e), offset); - break; - case expr_kind::Lambda: case expr_kind::Pi: - result = apply(binder_domain(e), offset) || apply(binder_body(e), offset + 1); - break; - case expr_kind::Let: - result = apply(let_type(e), offset) || apply(let_value(e), offset) || apply(let_body(e), offset + 1); - break; - } - - if (!result) { - if (offset == 0) - e.raw()->set_closed(); - if (shared) - m_cached.insert(expr_cell_offset(e.raw(), offset)); - } - - return result; - } -public: - has_free_vars_fn() {} - bool operator()(expr const & e) { return apply(e, 0); } -}; - -bool has_free_vars(expr const & e) { - return has_free_vars_fn()(e); -} - -/** - \brief Functional object for computing the range [0, R) of free variables occurring - in an expression. -*/ -class free_var_range_fn { - expr_map m_cached; - - static unsigned dec(unsigned s) { return (s == 0) ? 0 : s - 1; } - - unsigned apply(expr const & e) { - // handle easy cases - switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Sort: case expr_kind::Macro: - return 0; - case expr_kind::Var: - return var_idx(e) + 1; - case expr_kind::App: case expr_kind::Let: - case expr_kind::Meta: case expr_kind::Local: - case expr_kind::Lambda: case expr_kind::Pi: - break; - } - - if (e.raw()->is_closed()) - return 0; - - bool shared = false; - if (is_shared(e)) { - shared = true; - auto it = m_cached.find(e); - if (it != m_cached.end()) - return it->second; - } - - unsigned result = 0; - - switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Sort: case expr_kind::Macro: - case expr_kind::Var: - lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Meta: case expr_kind::Local: - result = apply(mlocal_type(e)); - break; - case expr_kind::App: - result = std::max(apply(app_fn(e)), apply(app_arg(e))); - break; - case expr_kind::Lambda: case expr_kind::Pi: - result = std::max(apply(binder_domain(e)), dec(apply(binder_body(e)))); - break; - case expr_kind::Let: - result = std::max({apply(let_type(e)), apply(let_value(e)), dec(apply(let_body(e)))}); - break; - } - - if (shared) - m_cached.insert(mk_pair(e, result)); - - return result; - } -public: - free_var_range_fn() {} - unsigned operator()(expr const & e) { return apply(e); } -}; - -unsigned free_var_range(expr const & e) { - return free_var_range_fn()(e); -} - /** \brief Functional object for checking whether a kernel expression has a free variable in the range [low, high) or not. */ @@ -169,7 +20,6 @@ protected: unsigned m_low; unsigned m_high; expr_cell_offset_set m_cached; - std::unique_ptr m_range_fn; // Return true iff m_low + offset <= vidx bool ge_lower(unsigned vidx, unsigned offset) const { @@ -205,7 +55,7 @@ protected: break; } - if (e.raw()->is_closed()) + if (closed(e)) return false; bool shared = false; @@ -255,10 +105,6 @@ bool has_free_var(expr const & e, unsigned low, unsigned high) { } bool has_free_var(expr const & e, unsigned i) { return has_free_var(e, i, i+1); } -bool has_free_var_ge(expr const & e, unsigned low) { - return has_free_var(e, low, std::numeric_limits::max()); -} - expr lower_free_vars(expr const & e, unsigned s, unsigned d) { if (d == 0 || closed(e)) return e; diff --git a/src/kernel/free_vars.h b/src/kernel/free_vars.h index a00d39a14..afde151fa 100644 --- a/src/kernel/free_vars.h +++ b/src/kernel/free_vars.h @@ -7,17 +7,6 @@ Author: Leonardo de Moura #pragma once #include "kernel/expr.h" namespace lean { -/** \brief Return true iff the given expression has free variables. */ -bool has_free_vars(expr const & a); -/** \brief Return true iff the given expression does not have free variables. */ -inline bool closed(expr const & a) { return !has_free_vars(a); } - -/** - \brief Return \c R s.t. the de Bruijn index of all free variables - occurring in \c e is in the interval [0, R). -*/ -unsigned free_var_range(expr const & e); - /** \brief Return true iff \c e constains a free variable (var i) s.t. \c i in [low, high). \pre low < high @@ -25,8 +14,6 @@ unsigned free_var_range(expr const & e); bool has_free_var(expr const & e, unsigned low, unsigned high); /** \brief Return true iff \c e contains the free variable (var i). */ bool has_free_var(expr const & e, unsigned i); -/** \brief Return true iff \c e contains a free variable >= low. */ -bool has_free_var_ge(expr const & e, unsigned low); /** \brief Lower the free variables >= s in \c e by \c d. That is, a free variable (var i) s.t.