feat(tactic): expose module docstrings as list

Author: Vtec234

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,43 @@ 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 string × 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 (option name × list string) :=
+      mod_docs.filter_map (λ d,
+        if d.1.is_none
+          then some ⟨none, d.2.map prod.snd⟩
+          else none),
+    /- Transform them to the expected format. -/
+    let mod_docs :=
+      mod_docs.map (λ d,
+        d.2.map (λ doc, (d.1, doc))),
+    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. */
-    optional<std::string> 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;
 };
@@ -167,16 +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);
-    if (ext.m_module_doc) {
-        *ext.m_module_doc += "\n" + doc;
-    } else {
-        ext.m_module_doc = doc;
-    }
+    ext.m_module_docs.emplace_back(pos, doc);
     auto new_env = update(env, ext);
-    return module::add_doc_string(new_env, doc);
+    return module::add_doc_string(new_env, doc, pos);
 }
 
 environment add_doc_string(environment const & env, name const & n, std::string doc) {
@@ -204,9 +202,7 @@ void get_module_doc_strings(environment const & env, buffer<mod_doc_entry> & res
     for (auto const & pr : mod_docs) {
         result.push_back({ optional<std::string>{ pr.first }, pr.second });
     }
-    if (ext.m_module_doc) {
-        result.push_back({ {}, *ext.m_module_doc });
-    }
+    result.push_back({ {}, ext.m_module_docs });
 }
 
 void initialize_documentation() {

src/library/documentation.h

@@ -6,13 +6,17 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <string>
+#include <utility>
+#include <vector>
 #include "kernel/environment.h"
+#include "util/message_definitions.h"
+
 namespace lean {
 struct mod_doc_entry {
     optional<std::string> m_mod_name;
-    std::string           m_doc;
+    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<mod_doc_entry> & result);

src/library/module.cpp

@@ -90,7 +90,7 @@ struct module_ext : public environment_extension {
      * 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::map<std::string, std::string> m_module_docs;
+    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;
@@ -425,23 +425,25 @@ struct mod_doc_modification : public modification {
     LEAN_MODIFICATION("mod_doc")
 
     std::string m_doc;
+    pos_info m_pos;
 
     mod_doc_modification() {}
-    /** A docstring for a declaration in the module. */
-    mod_doc_modification(std::string const & doc) : m_doc(doc) {}
+    /** 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;
+        s << m_doc << m_pos;
     }
 
     static std::shared_ptr<modification const> deserialize(deserializer & d) {
         std::string doc;
-        d >> doc;
-        return std::make_shared<mod_doc_modification>(doc);
+        pos_info pos;
+        d >> doc >> pos;
+        return std::make_shared<mod_doc_modification>(doc, pos);
     }
 };
 
@@ -535,11 +537,11 @@ 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) {
-    return add(env, std::make_shared<mod_doc_modification>(doc));
+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::map<std::string, std::string> const & get_doc_strings(environment const & env) {
+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;
 }
 
@@ -732,11 +734,7 @@ void import_module(modification_list const & modifications, std::string const &
             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);
-            if (ext.m_module_docs.count(file_name) != 0) {
-                ext.m_module_docs[file_name] += "\n" + mdm->m_doc;
-            } else {
-                ext.m_module_docs[file_name] = mdm->m_doc;
-            }
+            ext.m_module_docs[file_name].emplace_back(mdm->m_pos, mdm->m_doc);
             env = update(env, ext);
         }
     }

src/library/module.h

@@ -5,11 +5,11 @@ 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>
 #include <vector>
-#include <map>
 #include "util/serializer.h"
 #include "util/optional.h"
 #include "kernel/pos_info_provider.h"
@@ -145,10 +145,10 @@ environment add_and_perform(environment const & env, std::shared_ptr<modificatio
 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);
+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::map<std::string, std::string> const & get_doc_strings(environment const & env);
+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,8 +758,8 @@ 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 string × 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<mod_doc_entry> entries;
     get_module_doc_strings(s.env(), entries);
@@ -772,8 +772,18 @@ vm_obj tactic_module_doc_strings(vm_obj const & _s) {
             decl_name = mk_vm_some(to_obj(*d));
         else
             decl_name = mk_vm_none();
-        vm_obj doc = to_obj(entries[i].m_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);

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,5 +1,9 @@
 Makes foo.
 Makes foo of foo.
 Doesn't make foo.
-[(none, This module has a doc..
-..or two.)]
+[(none, [(⟨1, 0⟩, This module has a doc..), (⟨2, 0⟩, ..or two.)])]
+[(none, This module has a doc..),
+ (none, ..or two.),
+ ((some foo.b), Makes foo of foo.),
+ ((some two), Doesn't make foo.),
+ ((some foo.a), Makes foo.)]