From 9031c42df2c21409977663718f64751ee605fd0e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 Sep 2013 14:30:35 -0700
Subject: [PATCH] Add coding style and notes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 README.md    |   1 +
 doc/style.md | 158 +++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 159 insertions(+)
 create mode 100644 doc/style.md

diff --git a/README.md b/README.md
index d4deeb201..d2db69f83 100644
--- a/README.md
+++ b/README.md
@@ -48,3 +48,4 @@ Miscellaneous
 
 - [Testing and Code Coverage](doc/make/coverage.md)
 - Building Doxygen Documentation: `doxygen src/Doxyfile`
+- [Coding style](doc/style.md)
diff --git a/doc/style.md b/doc/style.md
new file mode 100644
index 000000000..85c6ddac1
--- /dev/null
+++ b/doc/style.md
@@ -0,0 +1,158 @@
+Coding Style
+============
+
+[C++11](http://en.wikipedia.org/wiki/C%2B%2B11) features
+--------------------------------------------------------
+
+We make extensive use of new features in the C++ 11 standard.
+Developers must be familiar with the standard to be able to understand
+the code.
+Here are some of the features that are extensively used.
+
+- Type inference (aka `auto` keyword).
+- Initializer lists.
+- Lambda functions and expressions.
+- `nullptr` constant.
+- Strongly typed enumerations.
+- Right angle bracket.
+- Thread local storage.
+- Threading facilities.
+- Tuple types.
+
+Comments
+--------
+
+The comments in the Lean codebase contain
+[Doxygen](http://www.stack.nl/~dimitri/doxygen/) commands.
+Doxygen is the de facto standard tool for generating documentation from
+annotated C++ sources.
+
+Namespaces
+----------
+
+All code is in the `lean` namespace. Each frontend is stored in a
+separate nested namespace. For example, the SMT 2.0 frontend is stored
+in the `lean::smt` namespace.
+
+Exception: some debugging functions are stored outside of the `lean`
+namespace. These functions are called `print` and are meant to be used
+when debugging Lean using `gdb`.
+
+Smart pointers
+--------------
+
+We only use `std::shared_ptr` template for class `C` only if we expect
+to create only a few objects (< 1000) of class `C`. Otherwise, we
+implement our own intrusive smart pointer. For example, the class
+`expr` is an intrusive smart pointer to `expr_cell`. We may have
+millions of `expr` objects. We say it is intrusive because the
+reference counter is stored in `expr_cell`.
+
+We use `std::unique_ptr` to make sure unique resources will be freed
+correctly.
+
+Idioms
+------
+
+We use some popular C++ idioms:
+
+- [Pimpl](http://c2.com/cgi/wiki?PimplIdiom)
+- [RAII](http://en.wikipedia.org/wiki/Resource_Acquisition_Is_Initialization) Resource Acquisition Is Initialization
+
+Formatting
+----------
+
+* We use 4 spaces for indentation.
+
+* Class, method, and function names are lower case
+We use `_` for composite names. Example: `type_checker`.
+
+* Class/struct fields should start with the prefix `m_`.
+
+Example:
+
+     class point {
+         int m_x;
+         int m_y;
+     public:
+         ...
+     };
+
+* We do **not** use the `#ifndef-#define-#endif` idiom for header files.
+Instead we use `#pragma once`.
+
+* We write `type const & v` instead of `const type & v`.
+
+* We use `const` extensively.
+
+* `if-then-else`
+
+The following forms are acceptable:
+
+     if (cond) {
+         ...
+     } else {
+         ...
+     }
+
+and
+
+     if (cond)
+        statement1;
+     else
+        statement2;
+
+In *exceptional cases*, we also use
+
+     if (cond) statement;
+
+and
+
+     if (cond) statement1; else stament2;
+
+* `if-then-else-if-else`
+
+The following forms are acceptable:
+
+     if (cond) {
+         ...
+     } else if (cond) {
+         ...
+     } else {
+         ...
+     }
+
+and
+
+     if (cond)
+         statement1;
+     else if (cond)
+         statement2;
+     else
+         statement3;
+
+* We frequently format code using extra spaces
+
+For example, we write
+
+    environment const & m_env;
+    cache               m_cache;
+    normalizer          m_normalizer;
+    volatile bool       m_interrupted;
+
+instead of
+
+    environment const & m_env;
+    cache m_cache;
+    normalizer m_normalizer;
+    volatile bool m_interrupted;
+
+* We use the macro `lean_assert` for assertions.
+The macro `lean_assert` is extensively used when writing unit tests.
+
+* Spaces in expressions
+We write `a == b` instead of `a==b`.
+Similarly, we write `x < y + 1` instead of `x<y+1`.
+
+
+