doc(doc/examples/compiler): new example

doc/examples/compiler/README.md

@@ -0,0 +1,21 @@
+In this example, we use the Lean C++ code generator to construct a simple program.
+Our project contains two files:
+- `test.lean`: a simple Lean program
+- `main.cpp`: a C++ frontend for invoking the function `foo` defined at `test.lean`.
+
+1- Generate `test.cpp`. Remark: we must have the file `leanpkg.path` in the current directory.
+```
+../../../bin/lean --cpp=test.cpp test.lean
+```
+
+2- Generate `test` program using `g++` or `clang++`
+```
+g++ -o test --std=c++11 -I ../../../src test.cpp main.cpp ../../../bin/libleanstatic.a -lgmp -pthread
+```
+Remark: if you built `libleanstatic.a` using jemalloc, you also need to include option `-ljemalloc` in the previous step.
+
+3- Execute test program
+```
+./test 100
+```
+It should produce `Result: 5050`

doc/examples/compiler/leanpkg.path

@@ -0,0 +1,2 @@
+builtin_path
+path .

doc/examples/compiler/main.cpp

@@ -0,0 +1,29 @@
+#include <iostream>
+#include "runtime/init_module.h"
+#include "runtime/object.h"
+typedef lean::object obj;
+/* Initialization function for the module `test.lean` */
+void initialize_test();
+/* C++ header for the function `foo` at `test.lean` */
+obj* l_foo(obj*);
+
+int main(int argc, char ** argv) {
+    if (argc != 2) {
+        std::cerr << "incorrect number of arguments\n";
+        return 1;
+    }
+    /* Initialize Lean runtime */
+    lean::initialize_runtime_module();
+    /* Initialize module `test.lean` */
+    initialize_test();
+    /* Convert the first argument into a Lean `nat` object */
+    unsigned n = std::atoi(argv[1]);
+    obj * v = lean::mk_nat_obj(n);
+    /* Invoke `foo` defined at `test.lean` */
+    obj * r = l_foo(v);
+    /* Result is a Lean string */
+    std::cout << "Result: " << lean::string_cstr(r) << "\n";
+    /* We use `lean::dec` to consume/dispose the result value. */
+    lean::dec(r);
+    return 0;
+}

doc/examples/compiler/test.lean

@@ -0,0 +1,5 @@
+def Sum (xs : list nat) : nat :=
+xs.foldl (+) 0
+
+def foo (n : nat) : string :=
+to_string $ Sum (list.iota n)