From 09708209a7cae583000693a082a86efd2f3c35e2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 26 Jul 2013 11:43:53 -0700
Subject: [PATCH] Improve documentation

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/Doxyfile                       |  6 +++---
 src/kernel/deep_copy.cpp           |  5 +++++
 src/kernel/deep_copy.h             |  4 ++++
 src/kernel/expr.h                  | 32 ++++++++++++++++++++----------
 src/kernel/free_vars.h             |  3 +++
 src/kernel/replace.h               |  4 ++--
 src/util/escaped.h                 |  6 ++++--
 src/util/interrupt.h               |  3 +++
 src/util/name.cpp                  |  3 +++
 src/util/numerics/mpbq.h           |  7 ++++++-
 src/util/numerics/numeric_traits.h |  4 ++++
 src/util/sexpr/sexpr.cpp           |  9 ++++++++-
 src/util/sexpr/sexpr.h             | 24 +++++++++++++++++++++-
 13 files changed, 90 insertions(+), 20 deletions(-)

diff --git a/src/Doxyfile b/src/Doxyfile
index 72ad862e58..e97603c515 100644
--- a/src/Doxyfile
+++ b/src/Doxyfile
@@ -648,7 +648,7 @@ WARN_LOGFILE           =
 # directories like "/usr/src/myproject". Separate the files or directories
 # with spaces.
 
-INPUT                  = 
+INPUT                  =
 
 # This tag can be used to specify the character encoding of the source files
 # that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is
@@ -680,7 +680,7 @@ RECURSIVE              = YES
 # Note that relative paths are relative to the directory from which doxygen is
 # run.
 
-EXCLUDE                =
+EXCLUDE                = tests
 
 # The EXCLUDE_SYMLINKS tag can be used to select whether or not files or
 # directories that are symbolic links (a Unix file system feature) are excluded
@@ -1165,7 +1165,7 @@ FORMULA_TRANSPARENT    = YES
 # output. When enabled you also need to install MathJax separately and
 # configure the path to it using the MATHJAX_RELPATH option.
 
-USE_MATHJAX            = NO
+USE_MATHJAX            = YES
 
 # When MathJax is enabled you need to specify the location relative to the
 # HTML output directory using the MATHJAX_RELPATH option. The destination
diff --git a/src/kernel/deep_copy.cpp b/src/kernel/deep_copy.cpp
index 36bb7d613c..22e1b07cc6 100644
--- a/src/kernel/deep_copy.cpp
+++ b/src/kernel/deep_copy.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "buffer.h"
 
 namespace lean {
+/** \brief Implements deep copy of kernel expressions. */
 class deep_copy_fn {
     expr_cell_map<expr> m_cache;
 
@@ -37,6 +38,10 @@ class deep_copy_fn {
         return r;
     }
 public:
+    /**
+        \brief Return a new expression that is equal to the given
+        argument, but does not share any memory cell with it.
+    */
     expr operator()(expr const & a) { return apply(a); }
 };
 
diff --git a/src/kernel/deep_copy.h b/src/kernel/deep_copy.h
index 1d2d5bc024..6c1091f066 100644
--- a/src/kernel/deep_copy.h
+++ b/src/kernel/deep_copy.h
@@ -8,5 +8,9 @@ Author: Leonardo de Moura
 #include "expr.h"
 
 namespace lean {
+/**
+    \brief Return a new expression that is equal to the given
+    argument, but does not share any memory cell with it.
+*/
 expr deep_copy(expr const & e);
 }
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 99a4e73ef1..25ed9f4a6d 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -136,14 +136,14 @@ public:
 
 // =======================================
 // Expr (internal) Representation
-// 1. Free variables
+/** \brief Free variables. They are encoded using de Bruijn's indices. */
 class expr_var : public expr_cell {
     unsigned m_vidx; // de Bruijn index
 public:
     expr_var(unsigned idx);
     unsigned get_vidx() const { return m_vidx; }
 };
-// 2. Constants
+/** \brief Constants. */
 class expr_const : public expr_cell {
     name     m_name;
     unsigned m_pos;  // position in the environment.
@@ -152,7 +152,7 @@ public:
     name const & get_name() const { return m_name; }
     unsigned     get_pos() const { return m_pos; }
 };
-// 3. Applications
+/** \brief Function Applications */
 class expr_app : public expr_cell {
     unsigned m_num_args;
     expr     m_args[0];
@@ -165,7 +165,7 @@ public:
     expr const * begin_args() const          { return m_args; }
     expr const * end_args() const            { return m_args + m_num_args; }
 };
-// 4. Abstraction
+/** \brief Super class for lambda abstraction and pi (functional spaces). */
 class expr_abstraction : public expr_cell {
     name     m_name;
     expr     m_type;
@@ -176,22 +176,22 @@ public:
     expr const & get_type() const { return m_type; }
     expr const & get_body() const { return m_body; }
 };
-// 5. Lambda
+/** \brief Lambda abstractions */
 class expr_lambda : public expr_abstraction {
 public:
     expr_lambda(name const & n, expr const & t, expr const & e);
 };
-// 6. Pi
+/** \brief (dependent) Functional spaces */
 class expr_pi : public expr_abstraction {
 public:
     expr_pi(name const & n, expr const & t, expr const & e);
 };
-// 7. Prop
+/** \brief Propositions */
 class expr_prop : public expr_cell {
 public:
     expr_prop():expr_cell(expr_kind::Prop, 17) {}
 };
-// 8. Type lvl
+/** \brief Type */
 class expr_type : public expr_cell {
     unsigned m_size;
     uvar     m_vars[0];
@@ -202,7 +202,7 @@ public:
     uvar const & get_var(unsigned idx) const { lean_assert(idx < m_size); return m_vars[idx]; }
     uvar const * get_vars() const { return m_vars; }
 };
-// 9. Numerals
+/** \brief Numerals (efficient encoding using GMP numbers) */
 class expr_numeral : public expr_cell {
     mpz   m_numeral;
 public:
@@ -337,13 +337,21 @@ typedef std::pair<expr_cell*, unsigned> expr_cell_offset;
 
 // =======================================
 // Auxiliary functionals
+/** \brief Functional object for hashing kernel expressions. */
 struct expr_hash { unsigned operator()(expr const & e) const { return e.hash(); } };
+/** \brief Functional object for testing pointer equality between kernel expressions. */
 struct expr_eqp { bool operator()(expr const & e1, expr const & e2) const { return eqp(e1, e2); } };
+/** \brief Functional object for hashing kernel expression cells. */
 struct expr_cell_hash { unsigned operator()(expr_cell * e) const { return e->hash(); } };
+/** \brief Functional object for testing pointer equality between kernel cell expressions. */
 struct expr_cell_eqp { bool operator()(expr_cell * e1, expr_cell * e2) const { return e1 == e2; } };
+/** \brief Functional object for hashing a pair (n,k) where n is a kernel expressions, and k is an offset. */
 struct expr_offset_hash { unsigned operator()(expr_offset const & p) const { return hash(p.first.hash(), p.second); } };
+/** \brief Functional object for comparing pairs (expression, offset). */
 struct expr_offset_eqp { unsigned operator()(expr_offset const & p1, expr_offset const & p2) const { return eqp(p1.first, p2.first) && p1.second == p2.second; } };
+/** \brief Functional object for hashing a pair (n,k) where n is a kernel cell expressions, and k is an offset. */
 struct expr_cell_offset_hash { unsigned operator()(expr_cell_offset const & p) const { return hash(p.first->hash(), p.second); } };
+/** \brief Functional object for comparing pairs (expression cell, offset). */
 struct expr_cell_offset_eqp { unsigned operator()(expr_cell_offset const & p1, expr_cell_offset const & p2) const { return p1 == p2; } };
 // =======================================
 
@@ -352,10 +360,14 @@ struct expr_cell_offset_eqp { unsigned operator()(expr_cell_offset const & p1, e
 std::ostream & operator<<(std::ostream & out, expr const & a);
 /**
    \brief Wrapper for iterating over application arguments.
-   If n is an application, it allows us to write
+
+   If \c n is an application, it allows us to write
+
+   \code
    for (expr const & arg : app_args(n)) {
    ... do something with argument
    }
+   \endcode
 */
 struct args {
     expr const & m_app;
diff --git a/src/kernel/free_vars.h b/src/kernel/free_vars.h
index 4e7ff1e231..48a021cc65 100644
--- a/src/kernel/free_vars.h
+++ b/src/kernel/free_vars.h
@@ -11,5 +11,8 @@ namespace lean {
    \brief Return true if the given expression has free variables.
 */
 bool has_free_vars(expr const & a);
+/**
+   \brief Return true if the given expression does not have free variables.
+*/
 inline bool closed(expr const & a) { return !has_free_vars(a); }
 }
diff --git a/src/kernel/replace.h b/src/kernel/replace.h
index b5a97c4f15..d94873c63b 100644
--- a/src/kernel/replace.h
+++ b/src/kernel/replace.h
@@ -10,9 +10,9 @@ Author: Leonardo de Moura
 #include "maps.h"
 namespace lean {
 /**
-   \brief Functional for applying F to the subexpressions of a given expression.
+   \brief Functional for applying <tt>F</tt> to the subexpressions of a given expression.
 
-   The signature of F is
+   The signature of \f$F\f$ is
    unsigned, expr -> expr
 
    F is invoked for each subexpression s of the input expression e.
diff --git a/src/util/escaped.h b/src/util/escaped.h
index cd1b27c803..2c4167eff5 100644
--- a/src/util/escaped.h
+++ b/src/util/escaped.h
@@ -9,7 +9,10 @@ Author: Leonardo de Moura
 #include <iostream>
 
 namespace lean {
-
+/**
+   \brief Helper class for printing quoted strings.
+   For example, the string <tt>foo\"bla</tt> is displayed as <tt>"foo\"bla"</tt>.
+*/
 class escaped {
     char const * m_str;
     bool         m_trim_nl; // if true -> eliminate '\n' in the end of m_str.
@@ -19,5 +22,4 @@ public:
     escaped(char const * str, bool trim_nl = false, unsigned indent = 0):m_str(str), m_trim_nl(trim_nl), m_indent(indent) {}
     friend std::ostream & operator<<(std::ostream & out, escaped const & s);
 };
-
 }
diff --git a/src/util/interrupt.h b/src/util/interrupt.h
index a54acee088..48f519010c 100644
--- a/src/util/interrupt.h
+++ b/src/util/interrupt.h
@@ -26,6 +26,9 @@ void reset_interrupt();
 */
 bool interrupted();
 
+/**
+   \brief Exception used to sign lean interruptions.
+*/
 class interrupt : public std::exception {
 public:
     virtual char const * what() const noexcept { return "interrupted"; }
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 5655afff6a..d8480a1f40 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -17,6 +17,9 @@ namespace lean {
 
 constexpr char const * anonymous_str = "[anonymous]";
 
+/**
+   \brief Actual implementation of hierarchical names.
+*/
 struct name::imp {
     MK_LEAN_RC()
     bool     m_is_string;
diff --git a/src/util/numerics/mpbq.h b/src/util/numerics/mpbq.h
index 2078e62547..b899e9b7d4 100644
--- a/src/util/numerics/mpbq.h
+++ b/src/util/numerics/mpbq.h
@@ -11,7 +11,12 @@ Author: Leonardo de Moura
 
 namespace lean {
 
-// Multiple precision binary rationals
+/**
+    \brief Multiple precision binary rationals.
+
+    A binary rational is a rational number of the form:
+    \f$   \frac{a}{2^k}  \f$
+*/
 class mpbq {
     mpz      m_num;
     unsigned m_k;
diff --git a/src/util/numerics/numeric_traits.h b/src/util/numerics/numeric_traits.h
index 9106017ea5..7f7f9ef0ce 100644
--- a/src/util/numerics/numeric_traits.h
+++ b/src/util/numerics/numeric_traits.h
@@ -8,6 +8,10 @@ Author: Leonardo de Moura
 
 namespace lean {
 
+/**
+   \brief Template specializations define traits for native and lean
+   numeric types.
+*/
 template<typename T>
 class numeric_traits {
 };
diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp
index 1bc79821ef..5f9ca09e75 100644
--- a/src/util/sexpr/sexpr.cpp
+++ b/src/util/sexpr/sexpr.cpp
@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include "mpq.h"
 
 namespace lean {
-
+/** \brief Base class used to represent S-expression cells. */
 struct sexpr_cell {
     void dealloc();
     MK_LEAN_RC()
@@ -23,6 +23,7 @@ struct sexpr_cell {
     sexpr_cell(sexpr_kind k, unsigned h):m_rc(1), m_kind(k), m_hash(h) {}
 };
 
+/** \brief S-expression cell: string atom */
 struct sexpr_string : public sexpr_cell {
     std::string m_value;
     sexpr_string(char const * v):
@@ -33,6 +34,7 @@ struct sexpr_string : public sexpr_cell {
         m_value(v) {}
 };
 
+/** \brief S-expression cell: int atom */
 struct sexpr_int : public sexpr_cell {
     int m_value;
     sexpr_int(int v):
@@ -40,6 +42,7 @@ struct sexpr_int : public sexpr_cell {
         m_value(v) {}
 };
 
+/** \brief S-expression cell: double atom */
 struct sexpr_double : public sexpr_cell {
     double m_value;
     sexpr_double(double v):
@@ -47,6 +50,7 @@ struct sexpr_double : public sexpr_cell {
         m_value(v) {}
 };
 
+/** \brief S-expression cell: hierarchical name atom */
 struct sexpr_name : public sexpr_cell {
     name m_value;
     sexpr_name(name const & v):
@@ -54,6 +58,7 @@ struct sexpr_name : public sexpr_cell {
         m_value(v) {}
 };
 
+/** \brief S-expression cell: multi-precision integer atom */
 struct sexpr_mpz : public sexpr_cell {
     mpz m_value;
     sexpr_mpz(mpz const & v):
@@ -61,6 +66,7 @@ struct sexpr_mpz : public sexpr_cell {
         m_value(v) {}
 };
 
+/** \brief S-expression cell: multi-precision rational atom */
 struct sexpr_mpq : public sexpr_cell {
     mpq m_value;
     sexpr_mpq(mpq const & v):
@@ -68,6 +74,7 @@ struct sexpr_mpq : public sexpr_cell {
         m_value(v) {}
 };
 
+/** \brief S-expression cell: cons cell (aka pair) */
 struct sexpr_cons : public sexpr_cell {
     sexpr m_head;
     sexpr m_tail;
diff --git a/src/util/sexpr/sexpr.h b/src/util/sexpr/sexpr.h
index ce214115d3..cc6423744e 100644
--- a/src/util/sexpr/sexpr.h
+++ b/src/util/sexpr/sexpr.h
@@ -65,6 +65,7 @@ public:
     mpz const & get_mpz() const;
     mpq const & get_mpq() const;
 
+    /** \brief Hash code for this S-expression*/
     unsigned hash() const;
 
     sexpr & operator=(sexpr const & s);
@@ -74,18 +75,30 @@ public:
 
     friend void swap(sexpr & a, sexpr & b) { std::swap(a.m_ptr, b.m_ptr); }
 
-    // Pointer equality
+    /** \brief Pointer equality */
     friend bool eqp(sexpr const & a, sexpr const & b) { return a.m_ptr == b.m_ptr; }
 
     friend std::ostream & operator<<(std::ostream & out, sexpr const & s);
 
 };
 
+/** \brief Return the nil S-expression */
 inline sexpr nil() { return sexpr(); }
+/** \brief Return a cons-cell (aka pair) composed of \c head and \c tail */
 inline sexpr cons(sexpr const & head, sexpr const & tail) { return sexpr(head, tail); }
+/**
+    \brief Return the first argument of the given cons cell (aka pair).
+    \pre is_cons(s)
+*/
 inline sexpr const & car(sexpr const & s) { return head(s); }
+/**
+    \brief Return the second argument of the given cons cell (aka pair).
+    \pre is_cons(s)
+*/
 inline sexpr const & cdr(sexpr const & s) { return tail(s); }
+/** \brief Return true iff \c s is not an atom (i.e., it is not a cons cell). */
 inline bool is_atom(sexpr const & s)   { return s.kind() != sexpr_kind::CONS; }
+/** \brief Return true iff \c s is not a cons cell. */
 inline bool is_cons(sexpr const & s)   { return s.kind() == sexpr_kind::CONS; }
 inline bool is_string(sexpr const & s) { return s.kind() == sexpr_kind::STRING; }
 inline bool is_int(sexpr const & s)    { return s.kind() == sexpr_kind::INT; }
@@ -101,10 +114,19 @@ inline name const & to_name(sexpr const & s) { return s.get_name(); }
 inline mpz const & to_mpz(sexpr const & s) { return s.get_mpz(); }
 inline mpq const & to_mpq(sexpr const & s) { return s.get_mpq(); }
 
+/** \brief Return true iff \c s is nil or \c s is a cons cell where \c is_list(tail(s)). */
 bool is_list(sexpr const & s);
+/**
+    \brief Return the length of the given list.
+    \pre is_list(s)
+*/
 unsigned length(sexpr const & s);
+/** \brief Alias for #length. */
 inline unsigned len(sexpr const & s) { return length(s); }
 
+/** \brief Return true iff the two given S-expressions are structurally identical.
+    \warning This is not pointer equality.
+*/
 bool operator==(sexpr const & a, sexpr const & b);
 inline bool operator==(sexpr const & a, int b) { return is_int(a) && to_int(a) == b; }
 inline bool operator==(sexpr const & a, double b) { return is_double(a) && to_double(a) == b; }