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

perf(frontends/lean/placeholder_elaborator): reuse local_context, this

Browse source 
is possible now because local_context is a mainly "functional object"
This commit is contained in:
Leonardo de Moura 2014-09-25 10:11:41 -07:00
parent 2e2d2d21f1
commit b8eb65aac2
3 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/elaborator.cpp
View file

@ -275,7 +275,7 @@ public:
solutions using class-instances and tactic-hints.
*/
expr mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, constraint_seq & cs) {
auto ec = mk_placeholder_elaborator(env(), ios(), m_context.get_data(),
auto ec = mk_placeholder_elaborator(env(), ios(), m_context,
m_ngen.next(), m_relax_main_opaque, use_local_instances(),
is_strict, type, g, m_unifier_config);
cs += ec.second;

4
src/frontends/lean/placeholder_elaborator.cpp
View file

@ -27,7 +27,7 @@ struct placeholder_context {
local_context m_ctx;
bool m_relax;
bool m_use_local_instances;
placeholder_context(environment const & env, io_state const & ios, list<expr> const & ctx,
placeholder_context(environment const & env, io_state const & ios, local_context const & ctx,
name const & prefix, bool relax, bool use_local_instances):
m_ios(ios),
m_ngen(prefix),
@ -301,7 +301,7 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const
solutions using class-instances and tactic-hints.
*/
pair<expr, constraint> mk_placeholder_elaborator(
environment const & env, io_state const & ios, list<expr> const & ctx,
environment const & env, io_state const & ios, local_context const & ctx,
name const & prefix, bool relax, bool use_local_instances,
bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg) {
auto C = std::make_shared<placeholder_context>(env, ios, ctx, prefix, relax, use_local_instances);

3
src/frontends/lean/placeholder_elaborator.h
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include "kernel/expr.h"
#include "library/io_state.h"
#include "frontends/lean/local_context.h"
namespace lean {
/** \brief Create a metavariable, and attach choice constraint for generating
@ -24,7 +25,7 @@ namespace lean {
\param tag To be associated with new metavariables and expressions (for error localization).
*/
pair<expr, constraint> mk_placeholder_elaborator(
environment const & env, io_state const & ios, list<expr> const & ctx,
environment const & env, io_state const & ios, local_context const & ctx,
name const & prefix, bool relax_opaque, bool use_local_instances,
bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg);
}