From 24a15b6c46c72908a347cacf51b67cea55798768 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 24 Nov 2014 21:32:35 -0800 Subject: [PATCH] fix(frontends/lean): disable class-instance resolution when executing find_decl, fixes #343 --- src/frontends/lean/elaborator.cpp | 2 +- src/frontends/lean/elaborator_context.cpp | 20 +++++++++++++++++++- src/frontends/lean/elaborator_context.h | 2 ++ src/frontends/lean/find_cmd.cpp | 7 ++++++- src/frontends/lean/parser.cpp | 4 ++-- src/frontends/lean/parser.h | 2 +- tests/lean/run/group6.lean | 8 ++++++++ 7 files changed, 39 insertions(+), 6 deletions(-) create mode 100644 tests/lean/run/group6.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index c429b72943..1400830ae8 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 ee29c10c92..4cbaedb09f 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 065942fc1b..1e892063cf 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 11ee1b8199..34bd1aff7c 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 ad6d791b1e..fc83b7d6bd 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 c2433bd9ce..86b6336c5c 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 0000000000..c824efa6bf --- /dev/null +++ b/tests/lean/run/group6.lean @@ -0,0 +1,8 @@ +import algebra.group +open algebra + +find_decl _ * _ = 1 + +find_decl _ * _ = _ + +find_decl _⁻¹ * _ = _