michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

perf(kernel/expr): inline get_free_var_range, and cache its value for local and metavars

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-17 08:51:46 +01:00
parent 9fcb31bd5e
commit 9289717169
2 changed files with 23 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/kernel/expr.cpp
View file

@ -108,8 +108,9 @@ expr_const::expr_const(name const & n, levels const & ls):
// Expr metavariables and local variables
expr_mlocal::expr_mlocal(bool is_meta, name const & n, expr const & t):
expr_cell(is_meta ? expr_kind::Meta : expr_kind::Local, n.hash(), is_meta || t.has_expr_metavar(), t.has_univ_metavar(),
!is_meta || t.has_local(), t.has_param_univ()),
expr_composite(is_meta ? expr_kind::Meta : expr_kind::Local, n.hash(), is_meta || t.has_expr_metavar(), t.has_univ_metavar(),
!is_meta || t.has_local(), t.has_param_univ(),
1, get_free_var_range(t)),
m_name(n),
m_type(t) {}
void expr_mlocal::dealloc(buffer<expr_cell*> & todelete) {
@ -449,22 +450,6 @@ 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:
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::Macro:
return static_cast<expr_composite*>(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); }
bool is_bi_equal(expr const & a, expr const & b) { return expr_eq_fn(true)(a, b); }

34
src/kernel/expr.h
View file

@ -193,8 +193,20 @@ public:
levels const & get_levels() const { return m_levels; }
};
/** \brief Composite expressions */
class expr_composite : public expr_cell {
protected:
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_expr_mv, bool has_univ_mv, bool has_local,
bool has_param_univ, unsigned d, unsigned fv_range);
};
/** \brief Metavariables and local constants */
class expr_mlocal : public expr_cell {
class expr_mlocal : public expr_composite {
protected:
name m_name;
expr m_type;
@ -248,18 +260,6 @@ public:
binder_info const & get_info() const { return m_bi; }
};
/** \brief Composite expressions */
class expr_composite : public expr_cell {
protected:
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_expr_mv, bool has_univ_mv, bool has_local,
bool has_param_univ, unsigned d, unsigned fv_range);
};
/** \brief Applications */
class expr_app : public expr_composite {
expr m_fn;
@ -586,7 +586,13 @@ 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 <tt>[0, R)</tt>.
*/
unsigned get_free_var_range(expr const & e);
inline 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: return 0;
default: return static_cast<expr_composite*>(e.raw())->m_free_var_range;
}
}
/** \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. */