diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index c429b7294..1400830ae 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -233,7 +233,7 @@ 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) { + 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); diff --git a/src/frontends/lean/elaborator_context.cpp b/src/frontends/lean/elaborator_context.cpp index ee29c10c9..4cbaedb09 100644 --- a/src/frontends/lean/elaborator_context.cpp +++ b/src/frontends/lean/elaborator_context.cpp @@ -11,28 +11,46 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true #endif +#ifndef LEAN_DEFAULT_ELABORATOR_IGNORE_INSTANCES +#define LEAN_DEFAULT_ELABORATOR_IGNORE_INSTANCES false +#endif + namespace lean { // ========================================== // elaborator configuration options -static name * g_elaborator_local_instances = nullptr; +static name * g_elaborator_local_instances = nullptr; +static name * g_elaborator_ignore_instances = nullptr; + +name const & get_elaborator_ignore_instances_name() { + return *g_elaborator_ignore_instances; +} bool get_elaborator_local_instances(options const & opts) { return opts.get_bool(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES); } + +bool get_elaborator_ignore_instances(options const & opts) { + return opts.get_bool(*g_elaborator_ignore_instances, LEAN_DEFAULT_ELABORATOR_IGNORE_INSTANCES); +} // ========================================== elaborator_context::elaborator_context(environment const & env, io_state const & ios, local_decls const & lls, pos_info_provider const * pp, info_manager * info, bool check_unassigned): m_env(env), m_ios(ios), m_lls(lls), m_pos_provider(pp), m_info_manager(info), m_check_unassigned(check_unassigned) { m_use_local_instances = get_elaborator_local_instances(ios.get_options()); + m_ignore_instances = get_elaborator_ignore_instances(ios.get_options()); } void initialize_elaborator_context() { g_elaborator_local_instances = new name{"elaborator", "local_instances"}; + g_elaborator_ignore_instances = new name{"elaborator", "ignore_instances"}; register_bool_option(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES, "(lean elaborator) use local declarates as class instances"); + register_bool_option(*g_elaborator_ignore_instances, LEAN_DEFAULT_ELABORATOR_IGNORE_INSTANCES, + "(lean elaborator) if true, then elaborator does not perform class-instance resolution"); } void finalize_elaborator_context() { delete g_elaborator_local_instances; + delete g_elaborator_ignore_instances; } } diff --git a/src/frontends/lean/elaborator_context.h b/src/frontends/lean/elaborator_context.h index 065942fc1..1e892063c 100644 --- a/src/frontends/lean/elaborator_context.h +++ b/src/frontends/lean/elaborator_context.h @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "frontends/lean/info_manager.h" namespace lean { +name const & get_elaborator_ignore_instances_name(); /** \brief Environment for elaboration, it contains all the information that is "scope-indenpendent" */ class elaborator_context { environment m_env; @@ -21,6 +22,7 @@ class elaborator_context { // configuration bool m_check_unassigned; bool m_use_local_instances; + bool m_ignore_instances; friend class elaborator; public: elaborator_context(environment const & env, io_state const & ios, local_decls const & lls, diff --git a/src/frontends/lean/find_cmd.cpp b/src/frontends/lean/find_cmd.cpp index 11ee1b819..34bd1aff7 100644 --- a/src/frontends/lean/find_cmd.cpp +++ b/src/frontends/lean/find_cmd.cpp @@ -98,7 +98,12 @@ static void parse_filters(parser & p, buffer & pos_names, buffer pos_names, neg_names; parse_filters(p, pos_names, neg_names); environment env = p.env(); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index ad6d791b1..fc83b7d6b 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -67,9 +67,9 @@ bool get_parser_parallel_import(options const & opts) { } // ========================================== -parser::local_scope::local_scope(parser & p): +parser::local_scope::local_scope(parser & p, bool save_options): m_p(p), m_env(p.env()) { - m_p.push_local_scope(); + m_p.push_local_scope(save_options); } parser::local_scope::local_scope(parser & p, environment const & env): m_p(p), m_env(p.env()) { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index c2433bd9c..86b6336c5 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -359,7 +359,7 @@ public: expr parse_scoped_expr(buffer const & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); } struct local_scope { parser & m_p; environment m_env; - local_scope(parser & p); local_scope(parser & p, environment const & env); ~local_scope(); + local_scope(parser & p, bool save_options = false); local_scope(parser & p, environment const & env); ~local_scope(); }; bool has_locals() const { return !m_local_decls.empty() || !m_local_level_decls.empty(); } void add_local_level(name const & n, level const & l, bool is_variable = false); diff --git a/tests/lean/run/group6.lean b/tests/lean/run/group6.lean new file mode 100644 index 000000000..c824efa6b --- /dev/null +++ b/tests/lean/run/group6.lean @@ -0,0 +1,8 @@ +import algebra.group +open algebra + +find_decl _ * _ = 1 + +find_decl _ * _ = _ + +find_decl _⁻¹ * _ = _