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

fix(library/tactic): memory leak that only happens when compiling with clang++

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-29 11:07:06 -07:00
parent 6891f48c67
commit 15f270d9f3
4 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/tactic/proof_state.cpp
View file

@ -69,7 +69,7 @@ format proof_state::pp(environment const & env, formatter const & fmt, options c
return r;
}
goals map_goals(proof_state const & s, std::function<optional<goal>(name const & gn, goal const & g)> const & f) {
goals map_goals(proof_state const & s, std::function<optional<goal>(name const & gn, goal const & g)> f) {
return map_filter(s.get_goals(), [=](std::pair<name, goal> const & in, std::pair<name, goal> & out) -> bool {
check_interrupted();
optional<goal> new_goal = f(in.first, in.second);

2
src/library/tactic/proof_state.h
View file

@ -80,7 +80,7 @@ proof_state to_proof_state(environment const & env, expr const & mvar, options c
/** \brief Try to extract a proof from the given proof state */
optional<expr> to_proof(proof_state const & s);
goals map_goals(proof_state const & s, std::function<optional<goal>(name const & gn, goal const & g)> const & f);
goals map_goals(proof_state const & s, std::function<optional<goal>(name const & gn, goal const & g)> f);
io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s);
UDATA_DEFS_CORE(goals)

4
src/library/tactic/tactic.cpp
View file

@ -18,7 +18,7 @@ Author: Leonardo de Moura
#include "library/io_state_stream.h"
namespace lean {
tactic tactic01(std::function<optional<proof_state>(environment const &, io_state const & ios, proof_state const &)> const & f) {
tactic tactic01(std::function<optional<proof_state>(environment const &, io_state const & ios, proof_state const &)> f) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
return mk_proof_state_seq([=]() {
auto r = f(env, ios, s);
@ -30,7 +30,7 @@ tactic tactic01(std::function<optional<proof_state>(environment const &, io_stat
});
}
tactic tactic1(std::function<proof_state(environment const &, io_state const & ios, proof_state const &)> const & f) {
tactic tactic1(std::function<proof_state(environment const &, io_state const & ios, proof_state const &)> f) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
return mk_proof_state_seq([=]() {
auto r = f(env, ios, s);

8
src/library/tactic/tactic.h
View file

@ -24,8 +24,8 @@ inline optional<tactic> some_tactic(tactic && t) { return optional<tactic>(std::
template<typename F> inline proof_state_seq mk_proof_state_seq(F && f) { return mk_lazy_list<proof_state>(std::forward<F>(f)); }
tactic tactic01(std::function<optional<proof_state>(environment const &, io_state const & ios, proof_state const &)> const & f);
tactic tactic1(std::function<proof_state(environment const &, io_state const & ios, proof_state const &)> const & f);
tactic tactic01(std::function<optional<proof_state>(environment const &, io_state const & ios, proof_state const &)> f);
tactic tactic1(std::function<proof_state(environment const &, io_state const & ios, proof_state const &)> f);
/** \brief Return a "do nothing" tactic (aka skip). */
tactic id_tactic();
@ -115,9 +115,9 @@ typedef std::function<bool(environment const & env, io_state const & ios, proof_
\brief Return a tactic that applies the predicate \c p to the input state.
If \c p returns true, then applies \c t1. Otherwise, applies \c t2.
*/
tactic cond(proof_state_pred const & p, tactic const & t1, tactic const & t2);
tactic cond(proof_state_pred p, tactic const & t1, tactic const & t2);
/** \brief Syntax-sugar for cond(p, t, id_tactic()) */
inline tactic when(proof_state_pred const & p, tactic const & t) { return cond(p, t, id_tactic()); }
inline tactic when(proof_state_pred p, tactic const & t) { return cond(p, t, id_tactic()); }
/**
\brief Return a tactic that applies \c t only to the goal named \c gname.
The tactic fails if the input state does not have a goal named \c gname.