From 4421069e347211d977d4a5eafc96bc0621bedee1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Dec 2014 19:43:31 -0800 Subject: [PATCH] refactor(library/tactic): rename placeholder_elaborator to class_instance_synth --- src/frontends/lean/elaborator.cpp | 8 +-- src/library/tactic/CMakeLists.txt | 2 +- ...laborator.cpp => class_instance_synth.cpp} | 55 +++++++++---------- ...er_elaborator.h => class_instance_synth.h} | 11 ++-- src/library/tactic/init_module.cpp | 6 +- 5 files changed, 41 insertions(+), 41 deletions(-) rename src/library/tactic/{placeholder_elaborator.cpp => class_instance_synth.cpp} (88%) rename src/library/tactic/{placeholder_elaborator.h => class_instance_synth.h} (87%) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 314d133f1e..cf7efcf309 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -36,7 +36,7 @@ Author: Leonardo de Moura #include "library/choice_iterator.h" #include "library/pp_options.h" #include "library/tactic/expr_to_tactic.h" -#include "library/tactic/placeholder_elaborator.h" +#include "library/tactic/class_instance_synth.h" #include "library/error_handling/error_handling.h" #include "library/definitional/equations.h" #include "frontends/lean/local_decls.h" @@ -238,9 +238,9 @@ optional elaborator::mk_mvar_suffix(expr const & b) { expr elaborator::mk_placeholder_meta(optional const & suffix, optional const & type, tag g, bool is_strict, bool is_inst_implicit, constraint_seq & cs) { if (is_inst_implicit && !m_ctx.m_ignore_instances) { - auto ec = mk_placeholder_elaborator(env(), ios(), m_context, - m_ngen.next(), suffix, m_relax_main_opaque, use_local_instances(), - is_strict, type, g, m_unifier_config, m_ctx.m_pos_provider); + auto ec = mk_class_instance_elaborator( + env(), ios(), m_context, m_ngen.next(), suffix, m_relax_main_opaque, + use_local_instances(), is_strict, type, g, m_unifier_config, m_ctx.m_pos_provider); register_meta(ec.first); cs += ec.second; return ec.first; diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 06756c71b7..800d5de8c3 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -3,6 +3,6 @@ apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp exact_tactic.cpp unfold_tactic.cpp generalize_tactic.cpp inversion_tactic.cpp whnf_tactic.cpp revert_tactic.cpp assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp util.cpp -placeholder_elaborator.cpp init_module.cpp) +class_instance_synth.cpp init_module.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/placeholder_elaborator.cpp b/src/library/tactic/class_instance_synth.cpp similarity index 88% rename from src/library/tactic/placeholder_elaborator.cpp rename to src/library/tactic/class_instance_synth.cpp index 5729133fdf..a8d6744b57 100644 --- a/src/library/tactic/placeholder_elaborator.cpp +++ b/src/library/tactic/class_instance_synth.cpp @@ -43,7 +43,7 @@ static name * g_class_instance_max_depth = nullptr; [[ noreturn ]] void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); } [[ noreturn ]] void throw_class_exception(expr const & m, pp_fn const & fn) { throw_generic_exception(m, fn); } -void initialize_placeholder_elaborator() { +void initialize_class_instance_elaborator() { g_class_unique_class_instances = new name{"class", "unique_instances"}; g_class_trace_instances = new name{"class", "trace_instances"}; g_class_instance_max_depth = new name{"class", "instance_max_depth"}; @@ -59,7 +59,7 @@ void initialize_placeholder_elaborator() { "(class) max allowed depth in class-instance resolution"); } -void finalize_placeholder_elaborator() { +void finalize_class_instance_elaborator() { delete g_class_unique_class_instances; delete g_class_trace_instances; delete g_class_instance_max_depth; @@ -77,8 +77,8 @@ unsigned get_class_instance_max_depth(options const & o) { return o.get_unsigned(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH); } -/** \brief Context for handling placeholder metavariable choice constraint */ -struct placeholder_context { +/** \brief Context for handling class-instance metavariable choice constraint */ +struct class_instance_context { io_state m_ios; name_generator m_ngen; type_checker_ptr m_tc; @@ -89,8 +89,8 @@ struct placeholder_context { unsigned m_max_depth; char const * m_fname; optional m_pos; - placeholder_context(environment const & env, io_state const & ios, - name const & prefix, bool relax, bool use_local_instances): + class_instance_context(environment const & env, io_state const & ios, + name const & prefix, bool relax, bool use_local_instances): m_ios(ios), m_ngen(prefix), m_tc(mk_type_checker(env, m_ngen.mk_child(), relax)), @@ -121,12 +121,11 @@ struct placeholder_context { unsigned get_max_depth() const { return m_max_depth; } }; -pair mk_placeholder_elaborator(std::shared_ptr const & C, local_context const & ctx, +pair mk_class_instance_elaborator(std::shared_ptr const & C, local_context const & ctx, optional const & type, tag g, unsigned depth); -/** \brief Whenever the elaborator finds a placeholder '_' or introduces an - implicit argument, it creates a metavariable \c ?m. It also creates a - delayed choice constraint (?m in fn). +/** \brief Choice function \c fn for synthesizing class instances. + The function \c fn produces a stream of alternative solutions for ?m. In this case, \c fn will do the following: @@ -134,8 +133,8 @@ pair mk_placeholder_elaborator(std::shared_ptr m_C; +struct class_instance_elaborator : public choice_iterator { + std::shared_ptr m_C; local_context m_ctx; expr m_meta; // elaborated type of the metavariable @@ -151,10 +150,10 @@ struct placeholder_elaborator : public choice_iterator { unsigned m_depth; bool m_displayed_trace_header; - placeholder_elaborator(std::shared_ptr const & C, local_context const & ctx, - expr const & meta, expr const & meta_type, - list const & local_insts, list const & instances, - justification const & j, unsigned depth): + class_instance_elaborator(std::shared_ptr const & C, local_context const & ctx, + expr const & meta, expr const & meta_type, + list const & local_insts, list const & instances, + justification const & j, unsigned depth): choice_iterator(), m_C(C), m_ctx(ctx), m_meta(meta), m_meta_type(meta_type), m_local_instances(local_insts), m_instances(instances), m_jst(j), m_depth(depth) { if (m_depth > m_C->get_max_depth()) { @@ -216,7 +215,7 @@ struct placeholder_elaborator : public choice_iterator { type = tc.whnf(type).first; if (!is_pi(type)) break; - pair ac = mk_placeholder_elaborator(m_C, m_ctx, some_expr(binding_domain(type)), g, m_depth+1); + pair ac = mk_class_instance_elaborator(m_C, m_ctx, some_expr(binding_domain(type)), g, m_depth+1); expr arg = ac.first; cs.push_back(ac.second); r = mk_app(r, arg, g); @@ -268,7 +267,7 @@ struct placeholder_elaborator : public choice_iterator { } }; -constraint mk_placeholder_cnstr(std::shared_ptr const & C, local_context const & ctx, expr const & m, unsigned depth) { +constraint mk_class_instance_cnstr(std::shared_ptr const & C, local_context const & ctx, expr const & m, unsigned depth) { environment const & env = C->env(); justification j = mk_failed_to_synthesize_jst(env, m); auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const &, name_generator const &) { @@ -282,7 +281,7 @@ constraint mk_placeholder_cnstr(std::shared_ptr const & C, if (empty(local_insts) && empty(insts)) return lazy_list(); // nothing to be done // we are always strict with placeholders associated with classes - return choose(std::make_shared(C, ctx, meta, meta_type, local_insts, insts, j, depth)); + return choose(std::make_shared(C, ctx, meta, meta_type, local_insts, insts, j, depth)); } else { // do nothing, type is not a class... return lazy_list(constraints()); @@ -294,10 +293,10 @@ constraint mk_placeholder_cnstr(std::shared_ptr const & C, owner, j, relax); } -pair mk_placeholder_elaborator(std::shared_ptr const & C, local_context const & ctx, - optional const & type, tag g, unsigned depth) { +pair mk_class_instance_elaborator(std::shared_ptr const & C, local_context const & ctx, + optional const & type, tag g, unsigned depth) { expr m = ctx.mk_meta(C->m_ngen, type, g); - constraint c = mk_placeholder_cnstr(C, ctx, m, depth); + constraint c = mk_class_instance_cnstr(C, ctx, m, depth); return mk_pair(m, c); } @@ -321,8 +320,8 @@ static bool has_expr_metavar_relaxed(expr const & e) { return found; } -constraint mk_placeholder_root_cnstr(std::shared_ptr const & C, local_context const & _ctx, - expr const & m, bool is_strict, unifier_config const & cfg, delay_factor const & factor) { +constraint mk_class_instance_root_cnstr(std::shared_ptr const & C, local_context const & _ctx, + expr const & m, bool is_strict, unifier_config const & cfg, delay_factor const & factor) { environment const & env = C->env(); justification j = mk_failed_to_synthesize_jst(env, m); @@ -337,7 +336,7 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr const expr new_meta = mj.first; justification new_j = mj.second; unsigned depth = 0; - constraint c = mk_placeholder_cnstr(C, ctx, new_meta, depth); + constraint c = mk_class_instance_cnstr(C, ctx, new_meta, depth); unifier_config new_cfg(cfg); new_cfg.m_discard = false; new_cfg.m_use_exceptions = false; @@ -414,17 +413,17 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr const /** \brief Create a metavariable, and attach choice constraint for generating solutions using class-instances */ -pair mk_placeholder_elaborator( +pair mk_class_instance_elaborator( environment const & env, io_state const & ios, local_context const & ctx, name const & prefix, optional const & suffix, bool relax, bool use_local_instances, bool is_strict, optional const & type, tag g, unifier_config const & cfg, pos_info_provider const * pip) { - auto C = std::make_shared(env, ios, prefix, relax, use_local_instances); + auto C = std::make_shared(env, ios, prefix, relax, use_local_instances); expr m = ctx.mk_meta(C->m_ngen, suffix, type, g); C->set_main_meta(m); if (pip) C->set_pos(pip->get_file_name(), pip->get_pos_info(m)); - constraint c = mk_placeholder_root_cnstr(C, ctx, m, is_strict, cfg, delay_factor()); + constraint c = mk_class_instance_root_cnstr(C, ctx, m, is_strict, cfg, delay_factor()); return mk_pair(m, c); } } diff --git a/src/library/tactic/placeholder_elaborator.h b/src/library/tactic/class_instance_synth.h similarity index 87% rename from src/library/tactic/placeholder_elaborator.h rename to src/library/tactic/class_instance_synth.h index 9de3ffbdda..ae9c1e52a0 100644 --- a/src/library/tactic/placeholder_elaborator.h +++ b/src/library/tactic/class_instance_synth.h @@ -8,11 +8,12 @@ Author: Leonardo de Moura #include "kernel/expr.h" #include "library/io_state.h" #include "library/unifier.h" -#include "library/local_context.h" namespace lean { +class local_context; + /** \brief Create a metavariable, and attach choice constraint for generating - solutions using class-instances and tactic-hints. + solutions using class-instances. \param ctx Local context where placeholder is located \param prefix Prefix for metavariables that will be created by this procedure @@ -26,12 +27,12 @@ namespace lean { \param type Expected type for the placeholder (if known) \param tag To be associated with new metavariables and expressions (for error localization). */ -pair mk_placeholder_elaborator( +pair mk_class_instance_elaborator( environment const & env, io_state const & ios, local_context const & ctx, name const & prefix, optional const & suffix, bool relax_opaque, bool use_local_instances, bool is_strict, optional const & type, tag g, unifier_config const & cfg, pos_info_provider const * pip); -void initialize_placeholder_elaborator(); -void finalize_placeholder_elaborator(); +void initialize_class_instance_elaborator(); +void finalize_class_instance_elaborator(); } diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 9e21b3ebba..345b01e970 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -19,7 +19,7 @@ Author: Leonardo de Moura #include "library/tactic/revert_tactic.h" #include "library/tactic/inversion_tactic.h" #include "library/tactic/assert_tactic.h" -#include "library/tactic/placeholder_elaborator.h" +#include "library/tactic/class_instance_synth.h" namespace lean { void initialize_tactic_module() { @@ -38,11 +38,11 @@ void initialize_tactic_module() { initialize_revert_tactic(); initialize_inversion_tactic(); initialize_assert_tactic(); - initialize_placeholder_elaborator(); + initialize_class_instance_elaborator(); } void finalize_tactic_module() { - finalize_placeholder_elaborator(); + finalize_class_instance_elaborator(); finalize_assert_tactic(); finalize_inversion_tactic(); finalize_revert_tactic();