Modify Doxygen file to extract all elements even the undocumented ones. Disable warnings for undocumented entities. Add extra comments.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/Doxyfile

@@ -346,7 +346,7 @@ LOOKUP_CACHE_SIZE      = 0
 # Private class members and static file members will be hidden unless
 # the EXTRACT_PRIVATE and EXTRACT_STATIC tags are set to YES
 
-EXTRACT_ALL            = NO
+EXTRACT_ALL            = YES
 
 # If the EXTRACT_PRIVATE tag is set to YES all private members of a class
 # will be included in the documentation.
@@ -607,7 +607,7 @@ WARNINGS               = YES
 # for undocumented members. If EXTRACT_ALL is set to YES then this flag will
 # automatically be disabled.
 
-WARN_IF_UNDOCUMENTED   = YES
+WARN_IF_UNDOCUMENTED   = NO
 
 # If WARN_IF_DOC_ERROR is set to YES, doxygen will generate warnings for
 # potential errors in the documentation, such as not documenting some

src/kernel/builtin.cpp

@@ -74,6 +74,9 @@ static name g_true_name("true");
 static name g_false_name("false");
 static name g_true_u_name("\u22A4"); // ⊤
 static name g_false_u_name("\u22A5"); // ⊥
+/**
+   \brief Semantic attachments for Boolean values.
+*/
 class bool_value_value : public value {
     bool m_val;
 public:
@@ -112,6 +115,10 @@ bool is_false(expr const & e) {
 // If-then-else builtin operator
 static name   g_if_name("if");
 static format g_if_fmt(g_if_name);
+/**
+   \brief Semantic attachment for if-then-else operator with type
+   <code>Pi (A : Type), Bool -> A -> A -> A</code>
+*/
 class if_fn_value : public value {
     expr m_type;
 public:

src/kernel/builtin.h

@@ -107,7 +107,7 @@ expr mk_exists_fn();
 inline expr mk_exists(expr const & A, expr const & P) { return mk_app(mk_exists_fn(), A, P); }
 inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); }
 
-/** \brief Homogeneous equality. It has type: <tt>Pi (A : Type), A -> A -> Bool */
+/** \brief Homogeneous equality. It has type: <tt>Pi (A : Type), A -> A -> Bool</tt> */
 expr mk_homo_eq_fn();
 /** \brief Return the term (homo_eq A l r) */
 inline expr mk_homo_eq(expr const & A, expr const & l, expr const & r) { return mk_app(mk_homo_eq_fn(), A, l, r); }

src/kernel/for_each.h

@@ -9,6 +9,14 @@ Author: Leonardo de Moura
 #include "kernel/expr_sets.h"
 
 namespace lean {
+/**
+   \brief Template for implementing expression visitors.
+   The argument \c F must be a function object containing the method
+   <code>
+   void operator()(expr const & e, unsigned offset)
+   </code>
+   The \c offset is the number of binders under which \c e occurs.
+*/
 template<typename F>
 class for_each_fn {
     expr_cell_offset_set m_visited;

src/kernel/type_checker.h

@@ -12,6 +12,10 @@ Author: Leonardo de Moura
 namespace lean {
 class environment;
 class normalizer;
+/**
+   \brief Lean Type Checker. It can also be used to infer types, universes and check whether a
+   type \c A is convertible to a type \c B.
+*/
 class type_checker {
     class imp;
     std::unique_ptr<imp> m_ptr;

src/kernel/value.h

@@ -8,7 +8,9 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 namespace lean {
-// Some value subclasses that capture common implementation patterns.
+/**
+   \brief Base class for values that have a hierarchical attached to it.
+*/
 class named_value : public value {
     name m_name;
 public:
@@ -17,6 +19,10 @@ public:
     virtual name get_name() const { return m_name; }
 };
 
+/**
+   \brief Base class for values that have a hierarchical name and a type
+   attached to it.
+*/
 class const_value : public named_value {
     expr m_type;
 public:
@@ -25,6 +31,10 @@ public:
     virtual expr get_type() const { return m_type; }
 };
 
+/**
+   \brief Base class for values that have a hierarchical name attached to it, and
+   have type Type().
+*/
 class type_value : public named_value {
 public:
     type_value(name const & n):named_value(n) {}

src/library/arith/int.cpp

@@ -11,6 +11,9 @@ Author: Leonardo de Moura
 #include "library/arith/num_type.h"
 
 namespace lean {
+/**
+   \brief Semantic attachment for Int type.
+*/
 class int_type_value : public num_type_value {
 public:
     int_type_value():num_type_value("Int", "\u2124") /* ℤ */ {}
@@ -49,6 +52,10 @@ mpz const & int_value_numeral(expr const & e) {
     return static_cast<int_value_value const &>(to_value(e)).get_num();
 }
 
+/**
+   \brief Template for semantic attachments that are binary operators of
+   the form Int -> Int -> Int
+*/
 template<char const * Name, typename F>
 class int_bin_op : public const_value {
 public:
@@ -108,6 +115,9 @@ MK_CONSTANT(int_ge_fn, name({"Int", "ge"}));
 MK_CONSTANT(int_lt_fn, name({"Int", "lt"}));
 MK_CONSTANT(int_gt_fn, name({"Int", "gt"}));
 
+/**
+   \brief Semantic attachment for the Nat to Int coercion.
+*/
 class nat_to_int_value : public const_value {
 public:
     nat_to_int_value():const_value("nat_to_int", Nat >> Int) {}

src/library/arith/nat.cpp

@@ -10,6 +10,9 @@ Author: Leonardo de Moura
 #include "library/arith/num_type.h"
 
 namespace lean {
+/**
+   \brief Semantic attachment for Nat type
+*/
 class nat_type_value : public num_type_value {
 public:
     nat_type_value():num_type_value("Nat", "\u2115") /* ℕ */ {}
@@ -48,6 +51,10 @@ mpz const & nat_value_numeral(expr const & e) {
     return static_cast<nat_value_value const &>(to_value(e)).get_num();
 }
 
+/**
+   \brief Template for semantic attachments that are binary operators of
+   the form Nat -> Nat -> Nat
+*/
 template<char const * Name, typename F>
 class nat_bin_op : public const_value {
 public:
@@ -63,15 +70,21 @@ public:
 };
 
 constexpr char nat_add_name[] = "add";
+/** \brief Evaluator for + : Nat -> Nat -> Nat */
 struct nat_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 + v2; }; };
 typedef nat_bin_op<nat_add_name, nat_add_eval> nat_add_value;
 MK_BUILTIN(nat_add_fn, nat_add_value);
 
 constexpr char nat_mul_name[] = "mul";
+/** \brief Evaluator for * : Nat -> Nat -> Nat */
 struct nat_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; };
 typedef nat_bin_op<nat_mul_name, nat_mul_eval> nat_mul_value;
 MK_BUILTIN(nat_mul_fn, nat_mul_value);
 
+/**
+   \brief Semantic attachment for less than or equal to operator with type
+   <code>Nat -> Nat -> Bool</code>
+*/
 class nat_le_value : public const_value {
 public:
     nat_le_value():const_value(name{"Nat", "le"}, Nat >> (Nat >> Bool)) {}

src/library/arith/real.cpp

@@ -19,6 +19,11 @@ public:
 expr const Real = mk_value(*(new real_type_value()));
 expr mk_real_type() { return Real; }
 
+/**
+   \brief Semantic attachment for "Real" values.
+   It is actually for rational values. We should eventually rename it to
+   rat_value_value
+*/
 class real_value_value : public value {
     mpq m_val;
 public:
@@ -50,6 +55,10 @@ mpq const & real_value_numeral(expr const & e) {
     return static_cast<real_value_value const &>(to_value(e)).get_num();
 }
 
+/**
+   \brief Template for semantic attachments that are binary operators of
+   the form Real -> Real -> Real
+*/
 template<char const * Name, typename F>
 class real_bin_op : public const_value {
 public:
@@ -65,16 +74,19 @@ public:
 };
 
 constexpr char real_add_name[] = "add";
+/** \brief Evaluator for + : Real -> Real -> Real */
 struct real_add_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 + v2; }; };
 typedef real_bin_op<real_add_name, real_add_eval> real_add_value;
 MK_BUILTIN(real_add_fn, real_add_value);
 
 constexpr char real_mul_name[] = "mul";
+/** \brief Evaluator for * : Real -> Real -> Real */
 struct real_mul_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 * v2; }; };
 typedef real_bin_op<real_mul_name, real_mul_eval> real_mul_value;
 MK_BUILTIN(real_mul_fn, real_mul_value);
 
 constexpr char real_div_name[] = "div";
+/** \brief Evaluator for / : Real -> Real -> Real */
 struct real_div_eval {
     mpq operator()(mpq const & v1, mpq const & v2) {
         if (v2.is_zero())
@@ -86,6 +98,10 @@ struct real_div_eval {
 typedef real_bin_op<real_div_name, real_div_eval> real_div_value;
 MK_BUILTIN(real_div_fn, real_div_value);
 
+/**
+   \brief Semantic attachment for less than or equal to operator with type
+   <code>Real -> Real -> Bool</code>
+*/
 class real_le_value : public const_value {
 public:
     real_le_value():const_value(name{"Real", "le"}, Real >> (Real >> Bool)) {}

src/library/formatter.h

@@ -53,7 +53,7 @@ public:
     void set_interrupt(bool flag) { m_cell->set_interrupt(flag); }
 };
 /**
-   \brief Create a simple formatter object based on #printer class.
+   \brief Create a simple formatter object based on \c print function.
 */
 formatter mk_simple_formatter();
 }

src/library/metavar.cpp

@@ -44,6 +44,10 @@ unsigned metavar_idx(expr const & n) {
     return const_name(n).get_numeral();
 }
 
+/**
+   \brief Auxiliary exception used to sign that a metavariable was
+   found in an expression.
+*/
 struct found_metavar {};
 
 bool has_metavar(expr const & e) {

src/library/state.h

@@ -42,12 +42,20 @@ public:
     void set_interrupt(bool flag) { m_formatter.set_interrupt(flag); }
 };
 
+/**
+   \brief Wrapper for the state object that provides access to the
+   state's regular channel
+*/
 struct regular {
     state const & m_state;
     regular(state const & s):m_state(s) {}
     void flush() { m_state.get_regular_channel().get_stream().flush(); }
 };
 
+/**
+   \brief Wrapper for the state object that provides access to the
+   state's diagnostic channel
+*/
 struct diagnostic {
     state const & m_state;
     diagnostic(state const & s):m_state(s) {}

src/util/ascii.cpp

@@ -7,7 +7,9 @@ Author: Leonardo de Moura
 #include <initializer_list>
 namespace lean {
 static char g_safe_ascii[256];
-
+/**
+   \brief Initializer for the \c g_safe_ascii table of "safe" ASCII characters.
+*/
 class init_safe_ascii {
     void set(int i, bool v) { g_safe_ascii[static_cast<unsigned char>(i)] = v; }
 public:

src/util/numerics/gmp_init.cpp

@@ -28,6 +28,11 @@ extern "C" void cxx_free(void * p, size_t) {
     free(p);
 }
 
+/**
+   \brief Auxiliary class for initializing the GMP memory allocation
+   functions. We overhide the default ones because we want to sign
+   the C++ exception std::bad_alloc when we run out-of-memory.
+*/
 class gmp_init {
 public:
     gmp_init() {

src/util/numerics/mpbq.h

@@ -249,6 +249,11 @@ public:
 
     friend void display_decimal(std::ostream & out, mpbq const & a, unsigned prec);
 
+    /**
+       \brief Auxiliary wrapper object to used control how a mpbq number is displayed in
+       a stream. When wrapped with this object, the numberal will be displayed in decimal
+       notation using at most \c m_prec decimal digits.
+    */
     class decimal {
         mpbq const & m_val;
         unsigned     m_prec;

src/util/scoped_map.h

@@ -136,6 +136,10 @@ public:
         return m_map.end();
     }
 
+    /**
+       \brief Auxiliary class for automatically performing a \c push
+       in the constructor and a \c pop in the destructor.
+    */
     class mk_scope {
         scoped_map & m_map;
     public:

src/util/sexpr/format.cpp

@@ -229,6 +229,11 @@ format wrap(format const & f1, format const & f2) {
                   f2};
 }
 
+/**
+   \brief Auxiliary exception used to sign that the amount of
+   available space was exhausted. It is used in \c space_upto_line_break and
+   \c space_upto_line_break_list_exceeded
+*/
 struct space_exceeded {};
 
 // Return true iff the space upto line break fits in the available space.