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

refactor(library/app_builder): change app_builder constructor

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-04 16:33:24 -08:00
parent 98b79373cc
commit f84f024b92
2 changed files with 21 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/library/app_builder.cpp
View file

@ -16,7 +16,8 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
struct app_builder::imp { struct app_builder::imp {
std::unique_ptr<tmp_type_context> m_ctx; tmp_type_context * m_ctx;
bool m_ctx_owner;
struct entry { struct entry {
unsigned m_num_umeta; unsigned m_num_umeta;
@ -107,15 +108,26 @@ struct app_builder::imp {
symm_info_getter m_symm_getter; symm_info_getter m_symm_getter;
trans_info_getter m_trans_getter; trans_info_getter m_trans_getter;
imp(std::unique_ptr<tmp_type_context> && ctx): imp(tmp_type_context & ctx, bool owner):
m_ctx(std::move(ctx)), m_ctx(&ctx),
m_ctx_owner(owner),
m_refl_getter(mk_refl_info_getter(m_ctx->env())), m_refl_getter(mk_refl_info_getter(m_ctx->env())),
m_symm_getter(mk_symm_info_getter(m_ctx->env())), m_symm_getter(mk_symm_info_getter(m_ctx->env())),
m_trans_getter(mk_trans_info_getter(m_ctx->env())) { m_trans_getter(mk_trans_info_getter(m_ctx->env())) {
} }
imp(environment const & env, io_state const & ios, reducible_behavior b): imp(environment const & env, io_state const & ios, reducible_behavior b):
imp(std::unique_ptr<tmp_type_context>(new tmp_type_context(env, ios, b))) { imp(*new tmp_type_context(env, ios, b), true) {
}
imp(tmp_type_context & ctx):
imp(ctx, false) {
}
~imp() {
lean_assert(m_ctx);
if (m_ctx_owner)
delete m_ctx;
} }
levels mk_metavars(declaration const & d, buffer<expr> & mvars, buffer<optional<expr>> & inst_args) { levels mk_metavars(declaration const & d, buffer<expr> & mvars, buffer<optional<expr>> & inst_args) {
@ -445,8 +457,8 @@ app_builder::app_builder(environment const & env, reducible_behavior b):
app_builder(env, get_dummy_ios(), b) { app_builder(env, get_dummy_ios(), b) {
} }
app_builder::app_builder(std::unique_ptr<tmp_type_context> && ctx): app_builder::app_builder(tmp_type_context & ctx):
m_ptr(new imp(std::move(ctx))) { m_ptr(new imp(ctx)) {
} }
app_builder::~app_builder() {} app_builder::~app_builder() {}

5
src/library/app_builder.h
View file

@ -32,8 +32,9 @@ class app_builder {
public: public:
app_builder(environment const & env, io_state const & ios, reducible_behavior b = UnfoldReducible); app_builder(environment const & env, io_state const & ios, reducible_behavior b = UnfoldReducible);
app_builder(environment const & env, reducible_behavior b = UnfoldReducible); app_builder(environment const & env, reducible_behavior b = UnfoldReducible);
app_builder(std::unique_ptr<tmp_type_context> && ctx); app_builder(tmp_type_context & ctx);
~app_builder(); ~app_builder();
/** \brief Create an application (d.{_ ... _} _ ... _ args[0] ... args[nargs-1]). /** \brief Create an application (d.{_ ... _} _ ... _ args[0] ... args[nargs-1]).
The missing arguments and universes levels are inferred using type inference. The missing arguments and universes levels are inferred using type inference.
@ -108,7 +109,7 @@ public:
/** \brief Set the local instances. This method is relevant when we want to expose local class instances /** \brief Set the local instances. This method is relevant when we want to expose local class instances
to the app_builder. to the app_builder.
\remark When the constructor app_builder(std::unique_ptr<tmp_type_context> && ctx) is used \remark When the constructor app_builder(tmp_type_context & ctx) is used
the initialization can be performed outside. */ the initialization can be performed outside. */
void set_local_instances(list<expr> const & insts); void set_local_instances(list<expr> const & insts);
}; };