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

feat(library/local_context): helper functions

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-05 09:08:11 -07:00
parent c1b06fe49a
commit 07388479e6
2 changed files with 34 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/library/local_context.cpp
View file

@ -136,6 +136,11 @@ optional<local_decl> local_context::get_local_decl_from_user_name(name const & n
return back_find_if([&](local_decl const & d) { return d.get_pp_name() == n; });
}
optional<local_decl> local_context::get_last_local_decl() const {
if (m_idx2local_decl.empty()) return optional<local_decl>();
return optional<local_decl>(m_idx2local_decl.max());
}
void local_context::for_each_after(local_decl const & d, std::function<void(local_decl const &)> const & fn) const {
m_idx2local_decl.for_each_greater(d.get_idx(), [&](unsigned, local_decl const & d) { return fn(d); });
}
@ -307,6 +312,26 @@ format local_context::pp(formatter const & fmt) const {
return r;
}
bool local_context::uses_user_name(name const & n) {
return static_cast<bool>(m_idx2local_decl.find_if([&](unsigned, local_decl const & d) { return d.get_pp_name() == n; }));
}
name local_context::get_unused_name(name const & prefix, unsigned & idx) {
while (true) {
name curr = prefix.append_after(idx);
idx++;
if (!uses_user_name(curr))
return curr;
}
}
name local_context::get_unused_name(name const & suggestion) {
if (!uses_user_name(suggestion))
return suggestion;
unsigned idx = 1;
return get_unused_name(suggestion, idx);
}
void initialize_local_context() {
g_local_prefix = new name(name::mk_internal_unique_name());
g_dummy_type = new expr(mk_constant(name::mk_internal_unique_name()));

9
src/library/local_context.h
View file

@ -100,6 +100,8 @@ public:
\remark This method is used to implement tactics such as 'revert'. */
optional<local_decl> get_local_decl_from_user_name(name const & n) const;
optional<local_decl> get_last_local_decl() const;
bool rename_user_name(name const & from, name const & to);
/** \brief Execute fn for each local declaration created after \c d. */
@ -110,6 +112,13 @@ public:
\pre \c d is in this local context. */
optional<local_decl> has_dependencies(local_decl const & d) const;
/** \brief Return an unused hypothesis "user name" with the given prefix, the suffix is an
unsigned >= idx. */
name get_unused_name(name const & prefix, unsigned & idx);
name get_unused_name(name const & suggestion);
/** \brief Return true iff the given name is a hypothesis "user name". */
bool uses_user_name(name const & n);
/** \brief Remove the given local decl.
\pre \c d is in this local context, is not frozen, and no other local decl depends on it. */
void clear(local_decl const & d);