From 09162e5fea19597ac314c826caed19784f3d4391 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Sep 2014 09:44:34 -0700 Subject: [PATCH] refactor(frontends/lean/local_context): remove name_generator from local_context --- src/frontends/lean/elaborator.cpp | 16 ++++++------ src/frontends/lean/local_context.cpp | 25 +++++++++---------- src/frontends/lean/local_context.h | 13 +++++----- src/frontends/lean/placeholder_elaborator.cpp | 6 ++--- 4 files changed, 29 insertions(+), 31 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 368b989b6..29504fc02 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -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 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 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 const & t, constraint_seq & cs) { lean_assert(is_proof_qed_annotation(e)); pair 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(*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); diff --git a/src/frontends/lean/local_context.cpp b/src/frontends/lean/local_context.cpp index 196e31c88..476fa61b9 100644 --- a/src/frontends/lean/local_context.cpp +++ b/src/frontends/lean/local_context.cpp @@ -35,9 +35,8 @@ expr abstract_locals(expr const & e, list const & locals) { }); } -local_context::local_context(name const & prefix):m_ngen(prefix) {} -local_context::local_context(name const & prefix, list const & ctx): - m_ngen(prefix) { +local_context::local_context() {} +local_context::local_context(list 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 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 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 const & type, tag g) { - expr mvar = mk_metavar(type, g); +expr local_context::mk_meta(name_generator & ngen, optional const & type, tag g) { + expr mvar = mk_metavar(ngen, type, g); expr meta = apply_context(mvar, g); return meta; } diff --git a/src/frontends/lean/local_context.h b/src/frontends/lean/local_context.h index 0a0dfdd5e..c97a962bb 100644 --- a/src/frontends/lean/local_context.h +++ b/src/frontends/lean/local_context.h @@ -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 m_ctx; // current local context: a list of local constants list m_ctx_abstracted; // m_ctx where elements have been abstracted public: - local_context(name const & prefix); - local_context(name const & prefix, list const & ctx); + local_context(); + local_context(list const & ctx); void set_ctx(list const & ctx); @@ -41,7 +40,7 @@ public: (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), 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 [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], @@ -51,7 +50,7 @@ public: \remark The type of the resulting expression is Type.{?u} */ - expr mk_type_meta(tag g); + expr mk_type_meta(name_generator & ngen, tag g); /** \brief Given type[l_1, ..., l_n] and assuming \c m_ctx is [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], @@ -63,7 +62,7 @@ public: (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), and \c ?u is a fresh universe metavariable. */ - expr mk_metavar(optional const & type, tag g); + expr mk_metavar(name_generator & ngen, optional const & type, tag g); /** \brief Given type[l_1, ..., l_n] and assuming \c m_ctx is [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], @@ -72,7 +71,7 @@ public: \see mk_metavar */ - expr mk_meta(optional const & type, tag g); + expr mk_meta(name_generator & ngen, optional const & type, tag g); /** \brief Return context as a list */ list const & get_data() const; diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index 66d44ebe8..55bd9c1a6 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -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 const & C, pair mk_placeholder_elaborator(std::shared_ptr const & C, bool is_strict, optional 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 mk_placeholder_elaborator( name const & prefix, bool relax, bool use_local_instances, bool is_strict, optional const & type, tag g, unifier_config const & cfg) { auto C = std::make_shared(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); }