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

refactor(frontends/lean/local_context): remove name_generator from local_context

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-25 09:44:34 -07:00
parent 354c456639
commit 09162e5fea
4 changed files with 29 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -162,8 +162,8 @@ public:
elaborator(elaborator_context & env, name_generator const & ngen):
m_env(env),
m_ngen(ngen),
m_context(m_ngen.next()),
m_full_context(m_ngen.next()),
m_context(),
m_full_context(),
m_unifier_config(env.m_ios.get_options(), true /* use exceptions */, true /* discard */) {
m_relax_main_opaque = false;
m_no_info = false;
@ -291,7 +291,7 @@ public:
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());
expr r = m_context.mk_type_meta(m_ngen, e.get_tag());
save_placeholder_info(e, r);
return r;
} else {
@ -318,7 +318,7 @@ public:
expr visit_choice(expr const & e, optional<expr> const & t, constraint_seq & cs) {
lean_assert(is_choice(e));
// Possible optimization: try to lookahead and discard some of the alternatives.
expr m = m_full_context.mk_meta(t, e.get_tag());
expr m = m_full_context.mk_meta(m_ngen, t, e.get_tag());
register_meta(m);
bool relax = m_relax_main_opaque;
auto fn = [=](expr const & meta, expr const & /* type */, substitution const & /* s */,
@ -333,7 +333,7 @@ public:
expr visit_by(expr const & e, optional<expr> const & t, constraint_seq & cs) {
lean_assert(is_by(e));
expr tac = visit(get_by_arg(e), cs);
expr m = m_context.mk_meta(t, e.get_tag());
expr m = m_context.mk_meta(m_ngen, t, e.get_tag());
register_meta(m);
m_local_tactic_hints.insert(mlocal_name(get_app_fn(m)), tac);
return m;
@ -342,7 +342,7 @@ public:
expr visit_proof_qed(expr const & e, optional<expr> const & t, constraint_seq & cs) {
lean_assert(is_proof_qed_annotation(e));
pair<expr, constraint_seq> ecs = visit(get_annotation_arg(e));
expr m = m_full_context.mk_meta(t, e.get_tag());
expr m = m_full_context.mk_meta(m_ngen, t, e.get_tag());
register_meta(m);
constraint c = mk_proof_qed_cnstr(env(), m, ecs.first, ecs.second, m_unifier_config, m_relax_main_opaque);
cs += c;
@ -427,7 +427,7 @@ public:
});
return choose(std::make_shared<coercion_elaborator>(*this, f, choices, coes, false));
};
f = m_full_context.mk_meta(none_expr(), f.get_tag());
f = m_full_context.mk_meta(m_ngen, none_expr(), f.get_tag());
register_meta(f);
cs += mk_choice_cnstr(f, choice_fn, to_delay_factor(cnstr_group::Basic), true, j, relax);
lean_assert(is_meta(f));
@ -492,7 +492,7 @@ public:
justification const & j) {
bool relax = m_relax_main_opaque;
type_checker & tc = *m_tc[relax];
expr m = m_full_context.mk_meta(some_expr(expected_type), a.get_tag());
expr m = m_full_context.mk_meta(m_ngen, some_expr(expected_type), a.get_tag());
register_meta(m);
constraint c = mk_coercion_cnstr(tc, *this, m, a, a_type, j, to_delay_factor(cnstr_group::Basic), relax);
return to_ecs(m, c);

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

@ -35,9 +35,8 @@ expr abstract_locals(expr const & e, list<expr> const & locals) {
});
}
local_context::local_context(name const & prefix):m_ngen(prefix) {}
local_context::local_context(name const & prefix, list<expr> const & ctx):
m_ngen(prefix) {
local_context::local_context() {}
local_context::local_context(list<expr> const & ctx) {
set_ctx(ctx);
}
@ -71,26 +70,26 @@ expr local_context::apply_context(expr const & f, tag g) const {
return apply_context_core(f, m_ctx, g);
}
expr local_context::mk_type_metavar(tag g) {
name n = m_ngen.next();
expr s = mk_sort(mk_meta_univ(m_ngen.next())).set_tag(g);
expr local_context::mk_type_metavar(name_generator & ngen, tag g) {
name n = ngen.next();
expr s = mk_sort(mk_meta_univ(ngen.next())).set_tag(g);
expr t = pi_abstract_context(s, g);
return ::lean::mk_metavar(n, t).set_tag(g);
}
expr local_context::mk_type_meta(tag g) {
return apply_context(mk_type_metavar(g), g);
expr local_context::mk_type_meta(name_generator & ngen, tag g) {
return apply_context(mk_type_metavar(ngen, g), g);
}
expr local_context::mk_metavar(optional<expr> const & type, tag g) {
name n = m_ngen.next();
expr r_type = type ? *type : mk_type_meta(g);
expr local_context::mk_metavar(name_generator & ngen, optional<expr> const & type, tag g) {
name n = ngen.next();
expr r_type = type ? *type : mk_type_meta(ngen, g);
expr t = pi_abstract_context(r_type, g);
return ::lean::mk_metavar(n, t).set_tag(g);
}
expr local_context::mk_meta(optional<expr> const & type, tag g) {
expr mvar = mk_metavar(type, g);
expr local_context::mk_meta(name_generator & ngen, optional<expr> const & type, tag g) {
expr mvar = mk_metavar(ngen, type, g);
expr meta = apply_context(mvar, g);
return meta;
}

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

@ -13,12 +13,11 @@ namespace lean {
and creating metavariables in the scope of the local context efficiently
*/
class local_context {
name_generator m_ngen;
list<expr> m_ctx; // current local context: a list of local constants
list<expr> m_ctx_abstracted; // m_ctx where elements have been abstracted
public:
local_context(name const & prefix);
local_context(name const & prefix, list<expr> const & ctx);
local_context();
local_context(list<expr> const & ctx);
void set_ctx(list<expr> const & ctx);
@ -41,7 +40,7 @@ public:
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u})</tt>,
where \c ?u is a fresh universe metavariable.
*/
expr mk_type_metavar(tag g);
expr mk_type_metavar(name_generator & ngen, tag g);
/** \brief Assuming \c m_ctx is
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
@ -51,7 +50,7 @@ public:
\remark The type of the resulting expression is <tt>Type.{?u}</tt>
*/
expr mk_type_meta(tag g);
expr mk_type_meta(name_generator & ngen, tag g);
/** \brief Given <tt>type[l_1, ..., l_n]</tt> and assuming \c m_ctx is
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
@ -63,7 +62,7 @@ public:
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u})</tt>,
and \c ?u is a fresh universe metavariable.
*/
expr mk_metavar(optional<expr> const & type, tag g);
expr mk_metavar(name_generator & ngen, optional<expr> const & type, tag g);
/** \brief Given <tt>type[l_1, ..., l_n]</tt> and assuming \c m_ctx is
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
@ -72,7 +71,7 @@ public:
\see mk_metavar
*/
expr mk_meta(optional<expr> const & type, tag g);
expr mk_meta(name_generator & ngen, optional<expr> const & type, tag g);
/** \brief Return context as a list */
list<expr> const & get_data() const;

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

@ -31,7 +31,7 @@ struct placeholder_context {
m_ios(ios),
m_ngen(prefix),
m_tc(mk_type_checker(env, m_ngen.mk_child(), relax)),
m_ctx(m_ngen.next(), ctx),
m_ctx(ctx),
m_relax(relax),
m_use_local_instances(use_local_instances) {
}
@ -245,7 +245,7 @@ constraint mk_placeholder_cnstr(std::shared_ptr<placeholder_context> const & C,
pair<expr, constraint> mk_placeholder_elaborator(std::shared_ptr<placeholder_context> const & C,
bool is_strict, optional<expr> const & type, tag g) {
expr m = C->m_ctx.mk_meta(type, g);
expr m = C->m_ctx.mk_meta(C->m_ngen, type, g);
constraint c = mk_placeholder_cnstr(C, m, is_strict);
return mk_pair(m, c);
}
@ -304,7 +304,7 @@ pair<expr, constraint> mk_placeholder_elaborator(
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);
expr m = C->m_ctx.mk_meta(type, g);
expr m = C->m_ctx.mk_meta(C->m_ngen, type, g);
constraint c = mk_placeholder_root_cnstr(C, m, is_strict, cfg, to_delay_factor(cnstr_group::Basic));
return mk_pair(m, c);
}