feat(tactic): make docstrings of imported modules accessible

doc/changes.md

@@ -31,6 +31,8 @@ This is the first community release of Lean 3.
 
  * Module documentation is now stored in .olean files to allow documentation to be automatically generated. (#54)
 
+ * Documentation of all imported modules is now exposed via the `olean_doc_strings` tactic. (#81)
+
 *Bug Fixes*
 
  * build: fix emscripten build in travis (#68)

library/init/meta/tactic.lean

@@ -543,7 +543,40 @@ It updates the environment in the tactic_state, and returns an expression of the
 where l_i's and a_j's are the collected dependencies.
 -/
 meta constant add_aux_decl (c : name) (type : expr) (val : expr) (is_lemma : bool) : tactic expr
-meta constant module_doc_strings : tactic (list (option name × string))
+
+/-- Returns a list of all top-level (`/-!`) docstrings in the active module and imported ones.
+The returned object is a list of modules, indexed by `(some filename)` for imported modules
+and `none` for the active one, where each module in the list is paired with a list
+of `(position_in_file, docstring)` pairs. -/
+meta constant olean_doc_strings : tactic (list (option string × (list (pos × string))))
+
+/-- Returns a list of docstrings in the active module. An entry in the list can be either:
+- a top-level (`/-!`) docstring, represented as `(none, docstring)`
+- a declaration-specific (`/--`) docstring, represented as `(some decl_name, docstring)` -/
+meta def module_doc_strings : tactic (list (option name × string)) :=
+  do
+    /- Obtain a list of top-level docs in current module. -/
+    mod_docs ← olean_doc_strings,
+    let mod_docs: list (list (option name × string)) :=
+      mod_docs.filter_map (λ d,
+        if d.1.is_none
+          then some (d.2.map
+            (λ pos_doc, ⟨none, pos_doc.2⟩))
+          else none),
+    let mod_docs := mod_docs.join,
+    /- Obtain list of declarations in current module. -/
+    e ← get_env,
+    let decls := environment.fold e ([]: list name)
+      (λ d acc, let n := d.to_name in
+      if (environment.decl_olean e n).is_none
+        then n::acc else acc),
+    /- Map declarations to those which have docstrings. -/
+    decls ← decls.mfoldl (λa n,
+      (doc_string n >>=
+        λ doc, pure $ (some n, doc) :: a)
+      <|> pure a) [],
+    pure (mod_docs ++ decls)
+
 /-- Set attribute `attr_name` for constant `c_name` with the given priority.
    If the priority is none, then use default -/
 meta constant set_basic_attribute (attr_name : name) (c_name : name) (persistent := ff) (prio : option nat := none) : tactic unit

src/frontends/lean/parser.cpp

@@ -2402,7 +2402,7 @@ std::string parser::parse_doc_block() {
 }
 
 void parser::parse_mod_doc_block() {
-    m_env = add_module_doc_string(m_env, m_scanner.get_str_val());
+    m_env = add_module_doc_string(m_env, m_scanner.get_str_val(), m_scanner.get_pos_info() );
     next();
 }
 

src/library/documentation.cpp

@@ -8,14 +8,16 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <functional>
 #include <cctype>
+#include <utility>
+#include <vector>
 #include "util/sstream.h"
 #include "library/module.h"
 #include "library/documentation.h"
 
 namespace lean {
 struct documentation_ext : public environment_extension {
-    /** Doc string for the current module being processed. It does not include imported doc strings. */
-    list<doc_entry>       m_module_doc;
+    /** Doc strings for the current module being processed. It does not include imported doc strings. */
+    std::vector<std::pair<pos_info, std::string>> m_module_docs;
     /** Doc strings for declarations (including imported ones). We store doc_strings for declarations in the .olean files. */
     name_map<std::string> m_doc_string_map;
 };
@@ -36,25 +38,16 @@ static environment update(environment const & env, documentation_ext const & ext
 struct doc_modification : public modification {
     LEAN_MODIFICATION("doc")
 
-    /** If non-empty, this is a doc on a declaration. Otherwise,
-      * it's a doc on the whole module. */
     name m_decl;
     std::string m_doc;
 
     doc_modification() {}
-    /** A docstring for the entire module. */
-    doc_modification(std::string const & doc) : m_decl(""), m_doc(doc) {}
     /** A docstring for a declaration in the module. */
     doc_modification(name const & decl, std::string const & doc) : m_decl(decl), m_doc(doc) {}
 
     void perform(environment & env) const override {
         auto ext = get_extension(env);
-        if (m_decl != "") {
-            ext.m_doc_string_map.insert(m_decl, m_doc);
-        }
-        // Note that we do NOT add anything to `m_module_doc` here, because `perform` is called
-        // when applying modifications from imported .olean modules whose doc strings are NOT
-        // part of the current module's documentation.
+        ext.m_doc_string_map.insert(m_decl, m_doc);
         env = update(env, ext);
     }
 
@@ -176,12 +169,12 @@ static std::string process_doc(std::string s) {
     return add_lean_suffix_to_code_blocks(s);
 }
 
-environment add_module_doc_string(environment const & env, std::string doc) {
+environment add_module_doc_string(environment const & env, std::string doc, pos_info pos) {
     doc = process_doc(doc);
     auto ext = get_extension(env);
-    ext.m_module_doc = cons(doc_entry(doc), ext.m_module_doc);
+    ext.m_module_docs.emplace_back(pos, doc);
     auto new_env = update(env, ext);
-    return module::add(new_env, std::make_shared<doc_modification>(doc));
+    return module::add_doc_string(new_env, doc, pos);
 }
 
 environment add_doc_string(environment const & env, name const & n, std::string doc) {
@@ -191,7 +184,6 @@ environment add_doc_string(environment const & env, name const & n, std::string
         throw exception(sstream() << "environment already contains a doc string for '" << n << "'");
     }
     ext.m_doc_string_map.insert(n, doc);
-    ext.m_module_doc = cons(doc_entry(n, doc), ext.m_module_doc);
     auto new_env = update(env, ext);
     return module::add(new_env, std::make_shared<doc_modification>(n, doc));
 }
@@ -204,10 +196,13 @@ optional<std::string> get_doc_string(environment const & env, name const & n) {
         return optional<std::string>();
 }
 
-void get_module_doc_strings(environment const & env, buffer<doc_entry> & result) {
+void get_module_doc_strings(environment const & env, buffer<mod_doc_entry> & result) {
     auto ext = get_extension(env);
-    to_buffer(ext.m_module_doc, result);
-    std::reverse(result.begin(), result.end());
+    auto const & mod_docs = module::get_doc_strings(env);
+    for (auto const & pr : mod_docs) {
+        result.push_back({ optional<std::string>{ pr.first }, pr.second });
+    }
+    result.push_back({ {}, ext.m_module_docs });
 }
 
 void initialize_documentation() {

src/library/documentation.h

@@ -6,21 +6,20 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <string>
+#include <utility>
+#include <vector>
 #include "kernel/environment.h"
+#include "util/message_definitions.h"
+
 namespace lean {
-class doc_entry {
-    optional<name> m_decl_name;
-    std::string    m_doc;
-public:
-    doc_entry(std::string const & doc):m_doc(doc) {}
-    doc_entry(name const & decl_name, std::string const & doc):m_decl_name(decl_name), m_doc(doc) {}
-    optional<name> const & get_decl_name() const { return m_decl_name; }
-    std::string const & get_doc() const { return m_doc; }
+struct mod_doc_entry {
+    optional<std::string> m_mod_name;
+    std::vector<std::pair<pos_info, std::string>> m_docs;
 };
-environment add_module_doc_string(environment const & env, std::string doc);
+environment add_module_doc_string(environment const & env, std::string doc, pos_info pos);
 environment add_doc_string(environment const & env, name const & n, std::string);
 optional<std::string> get_doc_string(environment const & env, name const & n);
-void get_module_doc_strings(environment const & env, buffer<doc_entry> & result);
+void get_module_doc_strings(environment const & env, buffer<mod_doc_entry> & result);
 void initialize_documentation();
 void finalize_documentation();
 }

src/library/module.cpp

@@ -86,6 +86,11 @@ struct module_ext : public environment_extension {
     list<name>        m_module_decls;
     name_set          m_module_defs;
     name_set          m_imported;
+    /** Top-level doc strings for modules which have them. Lean doesn't have a notion
+     * of module different from that of a source file, so we use file names to index
+     * the docstring map. */
+    // TODO(Vtec234): lean::rb_map misbehaves here for some reason
+    std::unordered_map<std::string, std::vector<std::pair<pos_info, std::string>>> m_module_docs;
     // Map from declaration name to olean file where it was defined
     name_map<std::string>     m_decl2olean;
     name_map<pos_info>        m_decl2pos_info;
@@ -416,6 +421,32 @@ struct quot_modification : public modification {
     }
 };
 
+struct mod_doc_modification : public modification {
+    LEAN_MODIFICATION("mod_doc")
+
+    std::string m_doc;
+    pos_info m_pos;
+
+    mod_doc_modification() {}
+    /** A module-level docstring. */
+    mod_doc_modification(std::string const & doc, pos_info pos) : m_doc(doc), m_pos(pos) {}
+
+    void perform(environment & env) const override {
+        // No-op. See `import_module` for actual action
+    }
+
+    void serialize(serializer & s) const override {
+        s << m_doc << m_pos;
+    }
+
+    static std::shared_ptr<modification const> deserialize(deserializer & d) {
+        std::string doc;
+        pos_info pos;
+        d >> doc >> pos;
+        return std::make_shared<mod_doc_modification>(doc, pos);
+    }
+};
+
 namespace module {
 environment add(environment const & env, std::shared_ptr<modification const> const & modf) {
     module_ext ext = get_extension(env);
@@ -506,6 +537,14 @@ environment add(environment const & env, certified_declaration const & d) {
     return add_decl_pos_info(new_env, _d.get_name());
 }
 
+environment add_doc_string(environment const & env, std::string const & doc, pos_info pos) {
+    return add(env, std::make_shared<mod_doc_modification>(doc, pos));
+}
+
+std::unordered_map<std::string, std::vector<std::pair<pos_info, std::string>>> const & get_doc_strings(environment const & env) {
+    return get_extension(env).m_module_docs;
+}
+
 bool is_definition(environment const & env, name const & n) {
     module_ext const & ext = get_extension(env);
     return ext.m_module_defs.contains(n);
@@ -693,6 +732,10 @@ void import_module(modification_list const & modifications, std::string const &
             env = add_decl_olean(env, dm->m_decl.get_name(), file_name);
         } else if (auto im = dynamic_cast<inductive_modification const *>(m.get())) {
             env = add_decl_olean(env, im->m_decl.get_decl().m_name, file_name);
+        } else if (auto mdm = dynamic_cast<mod_doc_modification const *>(m.get())) {
+            auto ext = get_extension(env);
+            ext.m_module_docs[file_name].emplace_back(mdm->m_pos, mdm->m_doc);
+            env = update(env, ext);
         }
     }
 }
@@ -724,13 +767,15 @@ void initialize_module() {
     inductive_modification::init();
     quot_modification::init();
     pos_info_mod::init();
+    mod_doc_modification::init();
 }
 
 void finalize_module() {
     quot_modification::finalize();
     pos_info_mod::finalize();
     inductive_modification::finalize();
     decl_modification::finalize();
+    mod_doc_modification::finalize();
     delete g_object_readers;
     delete g_ext;
 }

src/library/module.h

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <unordered_map>
 #include <string>
 #include <iostream>
 #include <utility>
@@ -143,6 +144,12 @@ environment add_and_perform(environment const & env, std::shared_ptr<modificatio
 /** \brief Add the given declaration to the environment, and mark it to be exported. */
 environment add(environment const & env, certified_declaration const & d);
 
+/** \brief Adds a module-level doc to the current module. */
+environment add_doc_string(environment const & env, std::string const & doc, pos_info pos);
+
+/** \brief Returns the map of module-level docs indexed by source file name. */
+std::unordered_map<std::string, std::vector<std::pair<pos_info, std::string>>> const & get_doc_strings(environment const & env);
+
 /** \brief Return true iff \c n is a definition added to the current module using #module::add */
 bool is_definition(environment const & env, name const & n);
 

src/library/tactic/tactic_state.cpp

@@ -758,22 +758,32 @@ vm_obj tactic_add_doc_string(vm_obj const & n, vm_obj const & doc, vm_obj const
     }
 }
 
-/* meta constant module_doc_strings : tactic (list (option name × string)) */
-vm_obj tactic_module_doc_strings(vm_obj const & _s) {
+/* meta constant olean_doc_strings : tactic (list (option string × (list (pos × string)))) */
+vm_obj tactic_olean_doc_strings(vm_obj const & _s) {
     tactic_state const & s  = tactic::to_state(_s);
-    buffer<doc_entry> entries;
+    buffer<mod_doc_entry> entries;
     get_module_doc_strings(s.env(), entries);
     unsigned i = entries.size();
     vm_obj r   = mk_vm_simple(0);
     while (i > 0) {
         --i;
         vm_obj decl_name;
-        if (auto d = entries[i].get_decl_name())
+        if (auto d = entries[i].m_mod_name)
             decl_name = mk_vm_some(to_obj(*d));
         else
             decl_name = mk_vm_none();
-        vm_obj doc = to_obj(entries[i].get_doc());
-        vm_obj e   = mk_vm_pair(decl_name, doc);
+        vm_obj lst = mk_vm_simple(0);
+        unsigned j = entries[i].m_docs.size();
+        while (j > 0) {
+            --j;
+            auto const& doc = entries[i].m_docs[j];
+            vm_obj line = mk_vm_nat(doc.first.first);
+            vm_obj column = mk_vm_nat(doc.first.second);
+            vm_obj pos = mk_vm_constructor(0, line, column); // pos_info
+            vm_obj doc_obj = mk_vm_pair(pos, to_obj(doc.second));
+            lst = mk_vm_constructor(1, doc_obj, lst);
+        }
+        vm_obj e   = mk_vm_pair(decl_name, lst);
         r          = mk_vm_constructor(1, e, r);
     }
     return tactic::mk_success(r, s);
@@ -1065,7 +1075,7 @@ void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic", "set_env"}),              tactic_set_env);
     DECLARE_VM_BUILTIN(name({"tactic", "doc_string"}),           tactic_doc_string);
     DECLARE_VM_BUILTIN(name({"tactic", "add_doc_string"}),       tactic_add_doc_string);
-    DECLARE_VM_BUILTIN(name({"tactic", "module_doc_strings"}),   tactic_module_doc_strings);
+    DECLARE_VM_BUILTIN(name({"tactic", "olean_doc_strings"}),    tactic_olean_doc_strings);
     DECLARE_VM_BUILTIN(name({"tactic", "open_namespaces"}),      tactic_open_namespaces);
     DECLARE_VM_BUILTIN(name({"tactic", "decl_name"}),            tactic_decl_name);
     DECLARE_VM_BUILTIN(name({"tactic", "add_aux_decl"}),         tactic_add_aux_decl);

src/shell/leandoc.cpp

@@ -229,23 +229,20 @@ void gen_doc(environment const & env, options const & _opts, std::ostream & out)
     options opts     = _opts.update_if_undef(name{"pp", "width"}, 100);
     auto fmt_factory = lean::mk_pretty_formatter_factory();
     auto fmt         = fmt_factory(env, opts, ctx);
-    buffer<doc_entry> entries;
-    get_module_doc_strings(env, entries);
-    for (doc_entry const & entry : entries) {
-        if (auto decl_name = entry.get_decl_name()) {
-            if (has_brief(entry.get_doc())) {
+
+    env.for_each_declaration([&] (declaration const & d) {
+         if (auto doc = get_doc_string(env, d.get_name())) {
+            if (has_brief(*doc)) {
                 std::string brief, body;
-                std::tie(brief, body) = split_brief_body(entry.get_doc());
-                gen_decl_doc(out, env, fmt, *decl_name, optional<std::string>(brief));
+                std::tie(brief, body) = split_brief_body(*doc);
+                gen_decl_doc(out, env, fmt, d.get_name(), optional<std::string>(brief));
                 print_block(out, body);
             } else {
-                gen_decl_doc(out, env, fmt, *decl_name, optional<std::string>());
-                print_block(out, entry.get_doc());
+                gen_decl_doc(out, env, fmt, d.get_name(), optional<std::string>());
+                print_block(out, *doc);
             }
-        } else {
-            print_block(out, entry.get_doc());
         }
         out << "\n";
-    }
+    });
 }
 }

tests/lean/doc_strings.lean

@@ -14,4 +14,5 @@ open tactic
 run_cmd doc_string `foo.a >>= trace
 run_cmd doc_string `foo.b >>= trace
 run_cmd doc_string `two >>= trace
+run_cmd olean_doc_strings >>= trace
 run_cmd module_doc_strings >>= trace

tests/lean/doc_strings.lean.expected.out

@@ -1,8 +1,9 @@
 Makes foo.
 Makes foo of foo.
 Doesn't make foo.
+[(none, [(⟨1, 0⟩, This module has a doc..), (⟨2, 0⟩, ..or two.)])]
 [(none, This module has a doc..),
  (none, ..or two.),
- ((some foo.a), Makes foo.),
  ((some foo.b), Makes foo of foo.),
- ((some two), Doesn't make foo.)]
+ ((some two), Doesn't make foo.),
+ ((some foo.a), Makes foo.)]