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

perf(library/print): improve is_used_name

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-15 18:57:05 -08:00
parent c6290f01d0
commit 6c07ca5d41
2 changed files with 16 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/library/print.cpp
View file

@ -16,12 +16,20 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
bool is_used_name(expr const & t, name const & n) { bool is_used_name(expr const & t, name const & n) {
return static_cast<bool>( bool found = false;
find(t, [&](expr const & e, unsigned) { for_each(t, [&](expr const & e, unsigned) {
return (is_constant(e) && const_name(e) == n) // t has a constant named n if (found) return false; // already found
|| (is_local(e) && (mlocal_name(e) == n || local_pp_name(e) == n)) // t has a local constant named n if ((is_constant(e) && const_name(e) == n) // t has a constant named n
|| (is_let(e) && get_let_var_name(e) == n); || (is_local(e) && (mlocal_name(e) == n || local_pp_name(e) == n)) // t has a local constant named n
})); || (is_let(e) && get_let_var_name(e) == n)) {
found = true;
return false; // found it
}
if (is_local(e) || is_metavar(e))
return false; // do not search their types
return true; // continue search
});
return false;
} }
name pick_unused_name(expr const & t, name const & s) { name pick_unused_name(expr const & t, name const & s) {

4
tests/lean/place_eqn.lean.expected.out
View file

@ -8,5 +8,5 @@ a : ℕ
place_eqn.lean:3:0: error: failed to add declaration 'foo' to environment, value has metavariables place_eqn.lean:3:0: error: failed to add declaration 'foo' to environment, value has metavariables
λ (a : ℕ), λ (a : ℕ),
nat.brec_on a nat.brec_on a
(λ (a_1 : ℕ) (b : nat.below a_1), (λ (a : ℕ) (b : nat.below a),
nat.cases_on a_1 (λ (b_1 : nat.below 0), ?M_1) (λ (a_2 : ℕ) (b_1 : nat.below (succ a_2)), ?M_2) b) nat.cases_on a (λ (b : nat.below 0), ?M_1) (λ (a : ℕ) (b : nat.below (succ a)), ?M_2) b)