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

refactor(frontends/lean/local_context): do not use references in the local context

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-10 12:49:35 -07:00
parent 63c0510a05
commit 9ce356e515
3 changed files with 49 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -75,7 +75,6 @@ class elaborator {
type_checker_ptr m_tc[2];
// mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants
// representing the context where ?m was created.
mvar2meta m_mvar2meta;
local_context m_context; // current local context: a list of local constants
local_context m_full_context; // superset of m_context, it also contains non-contextual locals.
cache m_cache;
@ -305,8 +304,8 @@ public:
elaborator(elaborator_context & env, list<expr> const & ctx, name_generator const & ngen):
m_env(env),
m_ngen(ngen),
m_context(m_ngen, m_mvar2meta, ctx),
m_full_context(m_ngen, m_mvar2meta, ctx) {
m_context(m_ngen.next(), ctx),
m_full_context(m_ngen.next(), ctx) {
m_relax_main_opaque = false;
m_no_info = false;
m_tc[0] = mk_type_checker_with_hints(env.m_env, m_ngen.mk_child(), false);
@ -331,6 +330,18 @@ public:
expr whnf(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->whnf(e, s); }
expr mk_app(expr const & f, expr const & a, tag g) { return ::lean::mk_app(f, a).set_tag(g); }
/** \brief Convert the metavariable to the metavariable application that captures
the context where it was defined.
*/
optional<expr> mvar_to_meta(expr const & mvar) {
lean_assert(is_metavar(mvar));
name const & m = mlocal_name(mvar);
if (auto it = m_context.find_meta(m))
return it;
else
return m_full_context.find_meta(m);
}
/** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */
void save_type_data(expr const & e, expr const & r) {
if (!m_no_info && infom() && pip() && (is_constant(e) || is_local(e) || is_placeholder(e))) {
@ -443,16 +454,6 @@ public:
return m;
}
/** \brief Convert the metavariable to the metavariable application that captures
the context where it was defined.
*/
optional<expr> mvar_to_meta(expr mvar) {
if (auto it = m_mvar2meta.find(mlocal_name(mvar)))
return some_expr(*it);
else
return none_expr();
}
expr visit_expecting_type(expr const & e, constraint_seq & cs) {
if (is_placeholder(e) && !placeholder_type(e)) {
expr r = m_context.mk_type_meta(e.get_tag());
@ -610,7 +611,8 @@ public:
if (is_meta(new_a_type)) {
if (delay_factor < to_delay_factor(cnstr_group::DelayedChoice)) {
// postpone...
return lazy_list<constraints>(constraints(mk_delayed_coercion_cnstr(m, a, a_type, justification(), delay_factor+1)));
return lazy_list<constraints>(constraints(mk_delayed_coercion_cnstr(m, a, a_type, justification(),
delay_factor+1)));
} else {
// giveup...
return lazy_list<constraints>(constraints(mk_eq_cnstr(mvar, a, justification(), relax)));
@ -660,7 +662,8 @@ public:
}
/** \brief Given a term <tt>a : a_type</tt>, and an expected type generate a metavariable with a delayed coercion. */
pair<expr, constraint_seq> mk_delayed_coercion(expr const & a, expr const & a_type, expr const & expected_type, justification const & j) {
pair<expr, constraint_seq> mk_delayed_coercion(expr const & a, expr const & a_type, expr const & expected_type,
justification const & j) {
expr m = m_full_context.mk_meta(some_expr(expected_type), a.get_tag());
return to_ecs(m, mk_delayed_coercion_cnstr(m, a, a_type, j, to_delay_factor(cnstr_group::Basic)));
}
@ -1153,7 +1156,7 @@ public:
for_each(e, [&](expr const & e, unsigned) {
if (!is_metavar(e))
return has_metavar(e);
if (auto it = m_mvar2meta.find(mlocal_name(e))) {
if (auto it = mvar_to_meta(e)) {
expr meta = tmp_s.instantiate(*it);
expr meta_type = tmp_s.instantiate(type_checker(env()).infer(meta).first);
goal g(meta, meta_type);

17
src/frontends/lean/local_context.cpp
View file

@ -8,8 +8,10 @@ Author: Leonardo de Moura
#include "frontends/lean/local_context.h"
namespace lean {
local_context::local_context(name_generator & ngen, mvar2meta & m, list<expr> const & ctx):
m_ngen(ngen), m_mvar2meta(m) { set_ctx(ctx); }
local_context::local_context(name const & prefix, list<expr> const & ctx):
m_ngen(prefix) {
set_ctx(ctx);
}
void local_context::set_ctx(list<expr> const & ctx) {
m_ctx = ctx;
@ -22,7 +24,7 @@ void local_context::set_ctx(list<expr> const & ctx) {
}
}
expr local_context::pi_abstract_context(expr e, tag g) {
expr local_context::pi_abstract_context(expr e, tag g) const {
e = abstract_locals(e, m_ctx_buffer.size(), m_ctx_buffer.data());
unsigned i = m_ctx_domain_buffer.size();
while (i > 0) {
@ -33,7 +35,7 @@ expr local_context::pi_abstract_context(expr e, tag g) {
return e;
}
expr local_context::apply_context(expr const & f, tag g) {
expr local_context::apply_context(expr const & f, tag g) const {
expr r = f;
for (unsigned i = 0; i < m_ctx_buffer.size(); i++)
r = mk_app(r, m_ctx_buffer[i]).set_tag(g);
@ -71,6 +73,13 @@ void local_context::add_local(expr const & l) {
m_ctx_buffer.push_back(l);
}
optional<expr> local_context::find_meta(name const & n) const {
if (auto it = m_mvar2meta.find(n))
return some_expr(*it);
else
return none_expr();
}
list<expr> const & local_context::get_data() const {
return m_ctx;
}

27
src/frontends/lean/local_context.h
View file

@ -16,13 +16,13 @@ typedef name_map<expr> mvar2meta;
and creating metavariables in the scope of the local context efficiently
*/
class local_context {
name_generator & m_ngen;
mvar2meta & m_mvar2meta;
list<expr> m_ctx; // current local context: a list of local constants
buffer<expr> m_ctx_buffer; // m_ctx as a buffer
buffer<expr> m_ctx_domain_buffer; // m_ctx_domain_buffer[i] == abstract_locals(m_ctx_buffer[i], i, m_ctx_buffer.beg
name_generator m_ngen;
mvar2meta m_mvar2meta;
list<expr> m_ctx; // current local context: a list of local constants
buffer<expr> m_ctx_buffer; // m_ctx as a buffer
buffer<expr> m_ctx_domain_buffer; // m_ctx_domain_buffer[i] == abstract_locals(m_ctx_buffer[i], i, m_ctx_buffer.beg
public:
local_context(name_generator & ngen, mvar2meta & m, list<expr> const & ctx);
local_context(name const & prefix, list<expr> const & ctx);
void set_ctx(list<expr> const & ctx);
@ -31,13 +31,13 @@ public:
then the result is
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), e[x_1, ... x_n])</tt>.
*/
expr pi_abstract_context(expr e, tag g);
expr pi_abstract_context(expr e, tag g) const;
/** \brief Assuming \c m_ctx is
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
return <tt>(f l_1 ... l_n)</tt>.
*/
expr apply_context(expr const & f, tag g);
expr apply_context(expr const & f, tag g) const;
/** \brief Assuming \c m_ctx is
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
@ -78,10 +78,17 @@ public:
*/
expr mk_meta(optional<expr> const & type, tag g);
void add_local(expr const & l);
/** \brief Return context as a list */
list<expr> const & get_data() const;
/** \brief Return the metavariable application associated with the metavariable name
\c n. The metavariable application contains the context where \c n was created.
Return none if \c n was not created using this local context object.
*/
optional<expr> find_meta(name const & n) const;
void add_local(expr const & l);
/** \brief Scope object for restoring the content of the context */
class scope {
local_context & m_main;