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

refactor(kernel/free_vars): use get_free_var_range to improve has_free_var_in_range performance

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-17 12:18:19 -07:00
parent dc864bf7b9
commit 4ae958af56
1 changed files with 25 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

53
src/kernel/free_vars.cpp
View file

@ -21,43 +21,31 @@ protected:
unsigned m_high; unsigned m_high;
expr_cell_offset_set m_cached; expr_cell_offset_set m_cached;
// Return true iff m_low + offset <= vidx bool apply(expr const & e, unsigned offset) {
bool ge_lower(unsigned vidx, unsigned offset) const { unsigned range = get_free_var_range(e);
if (range == 0) {
lean_assert(closed(e));
return false;
}
unsigned low1 = m_low + offset; unsigned low1 = m_low + offset;
if (low1 < m_low) if (low1 < m_low)
return false; // overflow, vidx can't be >= max unsigned return false; // overflow, vidx can't be >= max unsigned
return vidx >= low1; if (range <= low1) {
} return false;
} else {
// Return true iff vidx < m_high + offset lean_assert(range > low1);
bool lt_upper(unsigned vidx, unsigned offset) const {
unsigned high1 = m_high + offset; unsigned high1 = m_high + offset;
if (high1 < m_high) if (high1 < m_high)
return true; // overflow, vidx is always < max unsigned return true; // overflow, vidx is always < max unsigned
return vidx < high1; if (range <= high1)
return true;
// At this point, e contains a free variables in the range [0, range),
// and it definitely contains Var(range-1).
// Moreover [low1, high1) is a proper subset of [0, range), i.e., range > high1
if (is_var(e))
return var_idx(e) < high1;
} }
// Return true iff m_low + offset <= vidx < m_high + offset
bool in_interval(unsigned vidx, unsigned offset) const {
return ge_lower(vidx, offset) && lt_upper(vidx, offset);
}
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 in_interval(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 (closed(e))
return false;
bool shared = false; bool shared = false;
if (is_shared(e)) { if (is_shared(e)) {
shared = true; shared = true;
@ -101,7 +89,12 @@ public:
}; };
bool has_free_var(expr const & e, unsigned low, unsigned high) { bool has_free_var(expr const & e, unsigned low, unsigned high) {
return high > low && !closed(e) && has_free_var_in_range_fn(low, high)(e); unsigned range = get_free_var_range(e);
if (high <= low || range <= low)
return false;
if (range <= high)
return true;
return has_free_var_in_range_fn(low, high)(e);
} }
bool has_free_var(expr const & e, unsigned i) { return has_free_var(e, i, i+1); } bool has_free_var(expr const & e, unsigned i) { return has_free_var(e, i, i+1); }