fix(frontends/lean): disable class-instance resolution when executing find_decl, fixes #343

src/frontends/lean/elaborator.cpp

@@ -233,7 +233,7 @@ optional<name> elaborator::mk_mvar_suffix(expr const & b) {
 */
 expr elaborator::mk_placeholder_meta(optional<name> const & suffix, optional<expr> 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);

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_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<level> 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;
 }
 }

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<level> const & lls,

src/frontends/lean/find_cmd.cpp

@@ -98,7 +98,12 @@ static void parse_filters(parser & p, buffer<std::string> & pos_names, buffer<st
 
 environment find_cmd(parser & p) {
     expr e; level_param_names ls;
+    {
+        bool save_options = true;
+        parser::local_scope scope(p, save_options);
+        p.set_option(get_elaborator_ignore_instances_name(), true);
         std::tie(e, ls) = parse_local_expr(p);
+    }
     buffer<std::string> pos_names, neg_names;
     parse_filters(p, pos_names, neg_names);
     environment env = p.env();

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()) {

src/frontends/lean/parser.h

@@ -359,7 +359,7 @@ public:
     expr parse_scoped_expr(buffer<expr> 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);

tests/lean/run/group6.lean

@@ -0,0 +1,8 @@
+import algebra.group
+open algebra
+
+find_decl _ * _ = 1
+
+find_decl _ * _ = _
+
+find_decl _⁻¹ * _ = _