refactor(shell/server): move auto-completion code to a separate file

src/frontends/lean/json.cpp

@@ -5,7 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Gabriel Ebner
 */
 #ifdef LEAN_SERVER
+
+#include "library/scoped_ext.h"
+#include "library/protected.h"
 #include "frontends/lean/json.h"
+#include "kernel/declaration.h"
+#include "library/type_context.h"
+#include "kernel/instantiate.h"
+#include "pp.h"
+#include "util.h"
 
 namespace lean {
 
@@ -29,6 +37,52 @@ json json_of_message(message const & msg) {
     return j;
 }
 
+#define LEAN_COMPLETE_CONSUME_IMPLICIT true // lean will add metavariables for implicit arguments in serialize_decl()
+
+json serialize_decl(name const & short_name, name const & long_name, environment const & env, options const & o) {
+    declaration const & d = env.get(long_name);
+    type_context tc(env);
+    auto fmter = mk_pretty_formatter_factory()(env, o, tc);
+    expr type = d.get_type();
+    if (LEAN_COMPLETE_CONSUME_IMPLICIT) {
+        while (true) {
+            if (!is_pi(type))
+                break;
+            if (!binding_info(type).is_implicit() && !binding_info(type).is_inst_implicit())
+                break;
+            std::string q("?");
+            q += binding_name(type).to_string();
+            expr m = mk_constant(name(q.c_str()));
+            type   = instantiate(binding_body(type), m);
+        }
+    }
+    json completion;
+    completion["text"] = short_name.to_string();
+    std::ostringstream ss;
+    ss << mk_pair(flatten(fmter(type)), o);
+    completion["type"] = ss.str();
+    return completion;
+}
+
+json serialize_decl(name const & d, environment const & env, options const & o) {
+    // using namespace override resolution rule
+    list<name> const & ns_list = get_namespaces(env);
+    for (name const & ns : ns_list) {
+        name new_d = d.replace_prefix(ns, name());
+        if (new_d != d &&
+            !new_d.is_anonymous() &&
+            (!new_d.is_atomic() || !is_protected(env, d))) {
+            return serialize_decl(new_d, d, env, o);
+        }
+    }
+    // if the alias is unique use it
+    if (auto it = is_uniquely_aliased(env, d)) {
+        return serialize_decl(*it, d, env, o);
+    } else {
+        return serialize_decl(d, d, env, o);
+    }
+}
+
 void json_message_stream::report(message_bucket_id const &, message const & msg) {
     m_out << json_of_message(msg) << std::endl;
 }

src/frontends/lean/json.h

@@ -17,6 +17,9 @@ json json_of_severity(message_severity sev);
 
 json json_of_message(message const & msg);
 
+json serialize_decl(name const & short_name, name const & long_name, environment const & env, options const & o);
+json serialize_decl(name const & d, environment const & env, options const & o);
+
 class json_message_stream : public message_buffer {
     std::ostream & m_out;
 public:

src/shell/CMakeLists.txt

@@ -1,4 +1,4 @@
-add_executable(lean lean.cpp server.cpp leandoc.cpp)
+add_executable(lean lean.cpp server.cpp completion.cpp leandoc.cpp)
 target_link_libraries(lean leanstatic)
 install(TARGETS lean DESTINATION bin)
 

src/shell/completion.cpp

@@ -0,0 +1,119 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Gabriel Ebner, Leonardo de Moura, Sebastian Ullrich
+*/
+#if defined(LEAN_SERVER)
+#include "shell/completion.h"
+#include "shell/server.h"
+#include "util/bitap_fuzzy_search.h"
+#include "library/protected.h"
+#include "library/scoped_ext.h"
+#include "frontends/lean/util.h"
+
+namespace lean {
+
+#define LEAN_FUZZY_MAX_ERRORS          3
+#define LEAN_FUZZY_MAX_ERRORS_FACTOR   3
+
+/** \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) {
+    if (n.is_atomic())
+        return optional<name>(n);
+    list<name> const & ns_list = get_namespaces(env);
+    for (name const & ns : ns_list) {
+        if (is_prefix_of(ns, n)) {
+            auto n_prime = n.replace_prefix(ns, name());
+            if (n_prime.is_atomic() && !is_protected(env, n))
+                return optional<name>(n_prime);
+            break;
+        }
+    }
+    if (auto it = is_uniquely_aliased(env, n))
+        if (it->is_atomic())
+            return it;
+    return optional<name>();
+}
+
+unsigned get_fuzzy_match_max_errors(unsigned prefix_sz) {
+    unsigned r = (prefix_sz / LEAN_FUZZY_MAX_ERRORS_FACTOR);
+    if (r > LEAN_FUZZY_MAX_ERRORS)
+        return LEAN_FUZZY_MAX_ERRORS;
+    return r;
+}
+
+optional<name> exact_prefix_match(environment const & env, std::string const & pattern, declaration const & d) {
+    if (auto it = is_essentially_atomic(env, d.get_name())) {
+        std::string it_str = it->to_string();
+        // if pattern "perfectly" matches beginning of declaration name, we just display d on the top of the list
+        if (it_str.compare(0, pattern.size(), pattern) == 0)
+            return it;
+    } else {
+        std::string d_str = d.get_name().to_string();
+        if (d_str.compare(0, pattern.size(), pattern) == 0)
+            return optional<name>(d.get_name());
+    }
+    return optional<name>();
+}
+
+std::vector<json> get_completions(std::string const & pattern, environment const & env, options const & opts) {
+    std::vector<json> completions;
+
+    unsigned max_results = get_auto_completion_max_results(opts);
+    unsigned max_errors = get_fuzzy_match_max_errors(pattern.size());
+    std::vector<pair<name, name>> exact_matches;
+    std::vector<pair<std::string, name>> selected;
+    bitap_fuzzy_search matcher(pattern, max_errors);
+    env.for_each_declaration([&](declaration const & d) {
+        if (is_projection(env, d.get_name()))
+            return;
+        if (auto it = exact_prefix_match(env, pattern, d)) {
+            exact_matches.emplace_back(*it, d.get_name());
+        } else {
+            std::string text = d.get_name().to_string();
+            if (matcher.match(text))
+                selected.emplace_back(text, d.get_name());
+        }
+    });
+    unsigned num_results = 0;
+    if (!exact_matches.empty()) {
+        std::sort(exact_matches.begin(), exact_matches.end(),
+                  [](pair<name, name> const & p1, pair<name, name> const & p2) {
+                      return p1.first.size() < p2.first.size();
+                  });
+        for (pair<name, name> const & p : exact_matches) {
+            completions.push_back(serialize_decl(p.first, p.second, env, opts));
+            num_results++;
+            if (num_results >= max_results)
+                break;
+        }
+    }
+    unsigned sz = selected.size();
+    if (sz == 1) {
+        completions.push_back(serialize_decl(selected[0].second, env, opts));
+    } else if (sz > 1) {
+        std::vector<pair<std::string, name>> next_selected;
+        for (unsigned k = 0; k <= max_errors && num_results < max_results; k++) {
+            bitap_fuzzy_search matcher(pattern, k);
+            for (auto const & s : selected) {
+                if (matcher.match(s.first)) {
+                    completions.push_back(serialize_decl(s.second, env, opts));
+                    num_results++;
+                    if (num_results >= max_results)
+                        break;
+                } else {
+                    next_selected.push_back(s);
+                }
+            }
+            std::swap(selected, next_selected);
+            next_selected.clear();
+        }
+    }
+
+    return completions;
+}
+
+}
+#endif

src/shell/completion.h

@@ -0,0 +1,18 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Gabriel Ebner, Leonardo de Moura, Sebastian Ullrich
+*/
+#pragma once
+#include <string>
+#include <vector>
+#include "kernel/environment.h"
+#include "util/sexpr/options.h"
+#include "frontends/lean/json.h"
+
+namespace lean {
+
+std::vector<json> get_completions(std::string const & pattern, environment const & env, options const & o);
+
+}

src/shell/server.cpp

@@ -11,28 +11,17 @@ Authors: Gabriel Ebner, Leonardo de Moura, Sebastian Ullrich
 #include <vector>
 #include <clocale>
 #include "util/sexpr/option_declarations.h"
-#include "util/bitap_fuzzy_search.h"
-#include "kernel/instantiate.h"
 #include "library/mt_task_queue.h"
 #include "library/st_task_queue.h"
-#include "library/protected.h"
-#include "library/scoped_ext.h"
-#include "library/type_context.h"
-#include "library/module.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/info_manager.h"
-#include "frontends/lean/definition_cmds.h"
-#include "frontends/lean/util.h"
 #include "shell/server.h"
+#include "shell/completion.h"
 
 #ifndef LEAN_DEFAULT_AUTO_COMPLETION_MAX_RESULTS
 #define LEAN_DEFAULT_AUTO_COMPLETION_MAX_RESULTS 100
 #endif
 
-#define LEAN_FUZZY_MAX_ERRORS          3
-#define LEAN_FUZZY_MAX_ERRORS_FACTOR   3
-#define LEAN_COMPLETE_CONSUME_IMPLICIT true // lean will add metavariables for implicit arguments in serialize_decl()
-
 namespace lean {
 static name * g_auto_completion_max_results = nullptr;
 
@@ -179,151 +168,15 @@ std::shared_ptr<snapshot const> server::get_closest_snapshot(module_id const & i
     return ret;
 }
 
-/** \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) {
-    if (n.is_atomic())
-        return optional<name>(n);
-    list<name> const & ns_list = get_namespaces(env);
-    for (name const & ns : ns_list) {
-        if (is_prefix_of(ns, n)) {
-            auto n_prime = n.replace_prefix(ns, name());
-            if (n_prime.is_atomic() && !is_protected(env, n))
-                return optional<name>(n_prime);
-            break;
-        }
-    }
-    if (auto it = is_uniquely_aliased(env, n))
-        if (it->is_atomic())
-            return it;
-    return optional<name>();
-}
-
-unsigned get_fuzzy_match_max_errors(unsigned prefix_sz) {
-    unsigned r = (prefix_sz / LEAN_FUZZY_MAX_ERRORS_FACTOR);
-    if (r > LEAN_FUZZY_MAX_ERRORS)
-        return LEAN_FUZZY_MAX_ERRORS;
-    return r;
-}
-
-optional<name> exact_prefix_match(environment const & env, std::string const & pattern, declaration const & d) {
-    if (auto it = is_essentially_atomic(env, d.get_name())) {
-        std::string it_str = it->to_string();
-        // if pattern "perfectly" matches beginning of declaration name, we just display d on the top of the list
-        if (it_str.compare(0, pattern.size(), pattern) == 0)
-            return it;
-    } else {
-        std::string d_str = d.get_name().to_string();
-        if (d_str.compare(0, pattern.size(), pattern) == 0)
-            return optional<name>(d.get_name());
-    }
-    return optional<name>();
-}
-
-json server::serialize_decl(name const & short_name, name const & long_name, environment const & env, options const & o) {
-    declaration const & d = env.get(long_name);
-    type_context tc(env);
-    io_state_stream out   = regular(env, m_ios, tc).update_options(o);
-    expr type = d.get_type();
-    if (LEAN_COMPLETE_CONSUME_IMPLICIT) {
-        while (true) {
-            if (!is_pi(type))
-                break;
-            if (!binding_info(type).is_implicit() && !binding_info(type).is_inst_implicit())
-                break;
-            std::string q("?");
-            q += binding_name(type).to_string();
-            expr m = mk_constant(name(q.c_str()));
-            type   = instantiate(binding_body(type), m);
-        }
-    }
-    json completion;
-    completion["text"] = short_name.to_string();
-    std::ostringstream ss;
-    ss << mk_pair(flatten(out.get_formatter()(type)), o);
-    completion["type"] = ss.str();
-    return completion;
-}
-
-json server::serialize_decl(name const & d, environment const & env, options const & o) {
-    // using namespace override resolution rule
-    list<name> const & ns_list = get_namespaces(env);
-    for (name const & ns : ns_list) {
-        name new_d = d.replace_prefix(ns, name());
-        if (new_d != d &&
-            !new_d.is_anonymous() &&
-            (!new_d.is_atomic() || !is_protected(env, d))) {
-            return serialize_decl(new_d, d, env, o);
-        }
-    }
-    // if the alias is unique use it
-    if (auto it = is_uniquely_aliased(env, d)) {
-        return serialize_decl(*it, d, env, o);
-    } else {
-        return serialize_decl(d, d, env, o);
-    }
-}
-
 json server::handle_complete(json const & req) {
     std::string fn = req["file_name"];
     std::string pattern = req["pattern"];
     unsigned line = req["line"];
-    std::vector<json> completions;
 
-    if (auto snap = get_closest_snapshot(fn, line)) {
-        environment const & env = snap->m_env;
-        options const & opts = snap->m_options;
-        unsigned max_results = get_auto_completion_max_results(opts);
-        unsigned max_errors = get_fuzzy_match_max_errors(pattern.size());
-        std::vector<pair<name, name>> exact_matches;
-        std::vector<pair<std::string, name>> selected;
-        bitap_fuzzy_search matcher(pattern, max_errors);
-        env.for_each_declaration([&](declaration const & d) {
-            if (is_projection(env, d.get_name()))
-                return;
-            if (auto it = exact_prefix_match(env, pattern, d)) {
-                exact_matches.emplace_back(*it, d.get_name());
-            } else {
-                std::string text = d.get_name().to_string();
-                if (matcher.match(text))
-                    selected.emplace_back(text, d.get_name());
-            }
-        });
-        unsigned num_results = 0;
-        if (!exact_matches.empty()) {
-            std::sort(exact_matches.begin(), exact_matches.end(),
-                      [](pair<name, name> const & p1, pair<name, name> const & p2) {
-                          return p1.first.size() < p2.first.size();
-                      });
-            for (pair<name, name> const & p : exact_matches) {
-                completions.push_back(serialize_decl(p.first, p.second, env, opts));
-                num_results++;
-                if (num_results >= max_results)
-                    break;
-            }
-        }
-        unsigned sz = selected.size();
-        if (sz == 1) {
-            completions.push_back(serialize_decl(selected[0].second, env, opts));
-        } else if (sz > 1) {
-            std::vector<pair<std::string, name>> next_selected;
-            for (unsigned k = 0; k <= max_errors && num_results < max_results; k++) {
-                bitap_fuzzy_search matcher(pattern, k);
-                for (auto const & s : selected) {
-                    if (matcher.match(s.first)) {
-                        completions.push_back(serialize_decl(s.second, env, opts));
-                        num_results++;
-                        if (num_results >= max_results)
-                            break;
-                    } else {
-                        next_selected.push_back(s);
-                    }
-                }
-                std::swap(selected, next_selected);
-                next_selected.clear();
-            }
-        }
-    }
+    std::vector<json> completions;
+    if (auto snap = get_closest_snapshot(fn, line))
+        completions = get_completions(pattern, snap->m_env, snap->m_options);
+
     json res;
     res["response"] = "ok";
     res["completions"] = completions;

src/shell/server.h

@@ -12,6 +12,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich
 #include "library/versioned_msg_buf.h"
 #include "library/module_mgr.h"
 #include "frontends/lean/json.h"
+#include "library/mt_task_queue.h"
 
 namespace lean {
 
@@ -19,6 +20,8 @@ namespace lean {
 mt_tq_prioritizer mk_interactive_prioritizer(module_id const & roi);
 #endif
 
+unsigned get_auto_completion_max_results(options const &);
+
 class server : public module_vfs {
     versioned_msg_buf m_msg_buf;
     task_queue * m_tq;
@@ -46,8 +49,6 @@ class server : public module_vfs {
     json handle_complete(json const & req);
     json handle_info(json const & req);
 
-    json serialize_decl(name const & short_name, name const & long_name, environment const & env, options const & o);
-    json serialize_decl(name const & d, environment const & env, options const & o);
 public:
     server(unsigned num_threads, environment const & intial_env, io_state const & ios);
     ~server();