feat(frontends/lean): add 'find_decl' command

src/emacs/lean-syntax.el

@@ -15,7 +15,7 @@
     "alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix"
     "calc_trans" "calc_subst" "calc_refl" "calc_symm"
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
-    "using" "namespace" "instance" "class" "section" "fields"
+    "using" "namespace" "instance" "class" "section" "fields" "find_decl"
     "set_option" "add_rewrite" "extends" "include" "omit" "classes" "instances" "coercions" "raw")
   "lean keywords")
 

src/frontends/lean/CMakeLists.txt

@@ -5,7 +5,7 @@ server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
 inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp
 begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp
 theorem_queue.cpp structure_cmd.cpp info_manager.cpp info_annotation.cpp
-local_context.cpp choice_iterator.cpp
+local_context.cpp choice_iterator.cpp find_cmd.cpp
 placeholder_elaborator.cpp coercion_elaborator.cpp info_tactic.cpp
 proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp
 calc_proof_elaborator.cpp type_util.cpp elaborator_exception.cpp)

src/frontends/lean/builtin_cmds.cpp

@@ -28,6 +28,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/notation_cmd.h"
 #include "frontends/lean/inductive_cmd.h"
 #include "frontends/lean/structure_cmd.h"
+#include "frontends/lean/find_cmd.h"
 #include "frontends/lean/begin_end_ext.h"
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/class.h"
@@ -239,16 +240,6 @@ environment end_scoped_cmd(parser & p) {
     }
 }
 
-/** \brief Auxiliary function for check/eval */
-static std::tuple<expr, level_param_names> parse_local_expr(parser & p) {
-    expr e   = p.parse_expr();
-    list<expr> ctx = p.locals_to_context();
-    level_param_names new_ls;
-    std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx);
-    level_param_names ls = to_level_param_names(collect_univ_params(e));
-    return std::make_tuple(e, ls);
-}
-
 environment check_cmd(parser & p) {
     expr e; level_param_names ls;
     std::tie(e, ls) = parse_local_expr(p);
@@ -575,8 +566,9 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("coercion",     "add a new coercion", coercion_cmd));
     add_cmd(r, cmd_info("reducible",    "mark definitions as reducible/irreducible for automation", reducible_cmd));
     add_cmd(r, cmd_info("irreducible",  "mark definitions as irreducible for automation", irreducible_cmd));
+    add_cmd(r, cmd_info("find_decl",    "find definitions and/or theorems", find_cmd));
     add_cmd(r, cmd_info("#erase_cache", "erase cached definition (for debugging purposes)", erase_cache_cmd));
-    add_cmd(r, cmd_info("#projections", "generate projections for inductive datatype (for debugging)", projections_cmd));
+    add_cmd(r, cmd_info("#projections", "generate projections for inductive datatype (for debugging purposes)", projections_cmd));
 
     register_decl_cmds(r);
     register_inductive_cmd(r);

src/frontends/lean/find_cmd.cpp

@@ -0,0 +1,86 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <string>
+#include "kernel/instantiate.h"
+#include "library/unifier.h"
+#include "library/type_util.h"
+#include "library/reducible.h"
+#include "frontends/lean/parser.h"
+#include "frontends/lean/util.h"
+#include "frontends/lean/tokens.h"
+
+namespace lean {
+bool match_pattern(type_checker & tc, expr const & pattern, declaration const & d) {
+    name_generator ngen = tc.mk_ngen();
+     buffer<level> ls;
+    unsigned num_ls = length(d.get_univ_params());
+    for (unsigned i = 0; i < num_ls; i++)
+        ls.push_back(mk_meta_univ(ngen.next()));
+    expr dt        = instantiate_type_univ_params(d, to_list(ls.begin(), ls.end()));
+
+    unsigned num_e = get_expect_num_args(tc, pattern);
+    unsigned num_d = get_expect_num_args(tc, dt);
+    if (num_e > num_d)
+        return false;
+    for (unsigned i = 0; i < num_d - num_e; i++) {
+        dt         = tc.whnf(dt).first;
+        expr local = mk_local(ngen.next(), binding_domain(dt));
+        dt         = instantiate(binding_body(dt), local);
+    }
+    try {
+        unifier_config cfg;
+        cfg.m_max_steps            = 128;
+        cfg.m_cheap                = true;
+        cfg.m_ignore_context_check = true;
+        auto r = unify(tc.env(), pattern, dt, tc.mk_ngen(), true, substitution(), cfg);
+        return static_cast<bool>(r.pull());
+    } catch (exception&) {
+        return false;
+    }
+}
+
+static void parse_filters(parser & p, buffer<std::string> & pos_names, buffer<std::string> & neg_names) {
+    name plus("+"); name minus("-");
+    while (p.curr_is_token(get_comma_tk())) {
+        p.next();
+        if (p.curr_is_token(plus)) {
+            p.next();
+            pos_names.push_back(p.check_id_next("invalid find_decl command, identifier expected").to_string());
+        } else if (p.curr_is_token(minus)) {
+            p.next();
+            neg_names.push_back(p.check_id_next("invalid find_decl command, identifier expected").to_string());
+        } else {
+            pos_names.push_back(p.check_id_next("invalid find_decl command, '+', '-', or identifier expected").to_string());
+        }
+    }
+}
+
+environment find_cmd(parser & p) {
+    expr e; level_param_names ls;
+    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();
+    auto tc = mk_opaque_type_checker(env, p.mk_ngen());
+    p.regular_stream() << "find_decl result:\n";
+    bool found = false;
+    env.for_each_declaration([&](declaration const & d) {
+            if (std::all_of(pos_names.begin(), pos_names.end(),
+                            [&](std::string const & pos) { return is_part_of(pos, d.get_name()); }) &&
+                std::all_of(neg_names.begin(), neg_names.end(),
+                            [&](std::string const & neg) { return !is_part_of(neg, d.get_name()); }) &&
+                match_pattern(*tc.get(), e, d)) {
+                found = true;
+                p.regular_stream() << " " << get_decl_short_name(d.get_name(), env) << " : " << d.get_type() << endl;
+            }
+        });
+    if (!found)
+        p.regular_stream() << "no matches\n";
+    return env;
+}
+
+}

src/frontends/lean/find_cmd.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+namespace lean {
+class parser;
+environment find_cmd(parser & p);
+}

src/frontends/lean/server.cpp

@@ -22,6 +22,7 @@ Author: Leonardo de Moura
 #include "library/tactic/goal.h"
 #include "frontends/lean/server.h"
 #include "frontends/lean/parser.h"
+#include "frontends/lean/util.h"
 
 // #define LEAN_SERVER_DIAGNOSTIC
 
@@ -560,13 +561,6 @@ void server::display_decl(name const & short_name, name const & long_name, envir
     out << short_name << "|" << mk_pair(flatten(out.get_formatter()(type)), o) << "\n";
 }
 
-optional<name> is_uniquely_aliased(environment const & env, name const & n) {
-    if (auto it = is_expr_aliased(env, n))
-        if (length(get_expr_aliases(env, *it)) == 1)
-            return it;
-    return optional<name>();
-}
-
 /** \brief Return an (atomic) name if \c n can be referenced by this atomic
     name in the given environment. */
 optional<name> is_essentially_atomic(environment const & env, name const & n) {
@@ -721,19 +715,6 @@ void consume_pos_neg_strs(std::string const & filters, buffer<std::string> & pos
     }
 }
 
-bool is_part_of(std::string const & p, name n) {
-    while (true) {
-        if (n.is_string()) {
-            std::string s(n.get_string());
-            if (s.find(p) != std::string::npos)
-                return true;
-        }
-        if (n.is_atomic() || n.is_anonymous())
-            return false;
-        n = n.get_prefix();
-    }
-}
-
 bool match_type(type_checker & tc, expr const & meta, expr const & expected_type, declaration const & d) {
     name_generator ngen = tc.mk_ngen();
     goal g(meta, expected_type);

src/frontends/lean/token_table.cpp

@@ -86,7 +86,7 @@ void init_token_table(token_table & t) {
          "inductive", "record", "structure", "module", "universe", "universes",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
-         "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
+         "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "find_decl",
          "include", "omit", "#erase_cache", "#projections", nullptr};
 
     pair<char const *, char const *> aliases[] =

src/frontends/lean/util.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/scoped_ext.h"
 #include "library/locals.h"
 #include "library/explicit.h"
+#include "library/aliases.h"
 #include "library/placeholder.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "frontends/lean/parser.h"
@@ -384,4 +385,34 @@ pair<expr, justification> update_meta(expr const & meta, substitution s) {
     }
     return mk_pair(mk_app(mvar, args), j);
 }
+
+std::tuple<expr, level_param_names> parse_local_expr(parser & p) {
+    expr e   = p.parse_expr();
+    list<expr> ctx = p.locals_to_context();
+    level_param_names new_ls;
+    std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx);
+    level_param_names ls = to_level_param_names(collect_univ_params(e));
+    return std::make_tuple(e, ls);
+}
+
+optional<name> is_uniquely_aliased(environment const & env, name const & n) {
+    if (auto it = is_expr_aliased(env, n))
+        if (length(get_expr_aliases(env, *it)) == 1)
+            return it;
+    return optional<name>();
+}
+
+name get_decl_short_name(name const & d, environment const & env) {
+    // using namespace override resolution rule
+    list<name> const & ns_list = get_namespaces(env);
+    for (name const & ns : ns_list) {
+        if (is_prefix_of(ns, d) && ns != d)
+            return d.replace_prefix(ns, name());
+    }
+    // if the alias is unique use it
+    if (auto it = is_uniquely_aliased(env, d))
+        return *it;
+    else
+        return d;
+}
 }

src/frontends/lean/util.h

@@ -99,4 +99,12 @@ inline justification mk_type_mismatch_jst(expr const & v, expr const & v_type, e
     Return the updated expression and a justification for all substitutions.
 */
 pair<expr, justification> update_meta(expr const & meta, substitution s);
+
+/** \brief Auxiliary function for check/eval/find_decl */
+std::tuple<expr, level_param_names> parse_local_expr(parser & p);
+
+optional<name> is_uniquely_aliased(environment const & env, name const & n);
+
+/** \brief Get declaration 'short-name' that can uniquely identify it. */
+name get_decl_short_name(name const & d, environment const & env);
 }

src/library/unifier.cpp

@@ -69,6 +69,7 @@ unifier_config::unifier_config(bool use_exceptions, bool discard):
     m_expensive_classes(LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES),
     m_discard(discard) {
     m_cheap = false;
+    m_ignore_context_check = false;
 }
 
 unifier_config::unifier_config(options const & o, bool use_exceptions, bool discard):
@@ -78,6 +79,7 @@ unifier_config::unifier_config(options const & o, bool use_exceptions, bool disc
     m_expensive_classes(get_unifier_expensive_classes(o)),
     m_discard(discard) {
     m_cheap = false;
+    m_ignore_context_check = false;
 }
 
 // If \c e is a metavariable ?m or a term of the form (?m l_1 ... l_n) where
@@ -735,7 +737,11 @@ struct unifier_fn {
         if (!m || is_meta(rhs))
             return Continue;
         expr bad_local;
-        auto status = occurs_context_check(m_subst, rhs, *m, locals, bad_local);
+        occurs_check_status status;
+        if (m_config.m_ignore_context_check)
+            status = occurs_check_status::Ok;
+        else
+            status = occurs_context_check(m_subst, rhs, *m, locals, bad_local);
         if (status == occurs_check_status::FailLocal || status == occurs_check_status::FailCircular) {
             // Try to normalize rhs
             // Example:  ?M := f (pr1 (pair 0 ?M))

src/library/unifier.h

@@ -43,6 +43,9 @@ struct unifier_config {
     // If m_cheap is true, then expensive case-analysis is not performed (e.g., delta).
     // Default is m_cheap == false
     bool     m_cheap;
+    // If m_ignore_context_check == true, then occurs-check is skipped.
+    // Default is m_ignore_context_check == false
+    bool     m_ignore_context_check;
     unifier_config(bool use_exceptions = false, bool discard = false);
     explicit unifier_config(options const & o, bool use_exceptions = false, bool discard = false);
 };

src/util/name.cpp

@@ -401,6 +401,19 @@ name name::replace_prefix(name const & prefix, name const & new_prefix) const {
         return name(p, get_numeral());
 }
 
+bool is_part_of(std::string const & p, name n) {
+    while (true) {
+        if (n.is_string()) {
+            std::string s(n.get_string());
+            if (s.find(p) != std::string::npos)
+                return true;
+        }
+        if (n.is_atomic() || n.is_anonymous())
+            return false;
+        n = n.get_prefix();
+    }
+}
+
 name string_to_name(std::string const & str) {
     static_assert(*(lean_name_separator+1) == 0, "this function assumes the length of lean_name_separator is 1");
     name result;

src/util/name.h

@@ -163,6 +163,9 @@ struct name_eq { bool operator()(name const & n1, name const & n2) const { retur
 struct name_cmp { int operator()(name const & n1, name const & n2) const { return cmp(n1, n2); } };
 struct name_quick_cmp { int operator()(name const & n1, name const & n2) const { return quick_cmp(n1, n2); } };
 
+/** \brief Return true if \c p is part of \c n */
+bool is_part_of(std::string const & p, name n);
+
 /**
    \brief Return true iff the two given names are independent.
    That \c a is not a prefix of \c b, nor \c b is a prefix of \c a

tests/lean/run/find_cmd.lean

@@ -0,0 +1,12 @@
+import data.nat data.int
+open nat
+
+find_decl _ < succ _, +imp, -le
+
+find_decl _ < _ + _
+
+find_decl _ = succ _
+
+find_decl _ < succ _, +pos
+
+find_decl _ < succ _, pos