From ed1b101dd23755338c6e7661652adad2197906e5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 5 Feb 2019 16:50:12 -0800
Subject: [PATCH] doc(doc/examples/compiler): new example

---
 doc/examples/compiler/README.md    | 21 +++++++++++++++++++++
 doc/examples/compiler/leanpkg.path |  2 ++
 doc/examples/compiler/main.cpp     | 29 +++++++++++++++++++++++++++++
 doc/examples/compiler/test.lean    |  5 +++++
 4 files changed, 57 insertions(+)
 create mode 100644 doc/examples/compiler/README.md
 create mode 100644 doc/examples/compiler/leanpkg.path
 create mode 100644 doc/examples/compiler/main.cpp
 create mode 100644 doc/examples/compiler/test.lean

diff --git a/doc/examples/compiler/README.md b/doc/examples/compiler/README.md
new file mode 100644
index 0000000000..6b41ac38a0
--- /dev/null
+++ b/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`
diff --git a/doc/examples/compiler/leanpkg.path b/doc/examples/compiler/leanpkg.path
new file mode 100644
index 0000000000..2cbfd2b51b
--- /dev/null
+++ b/doc/examples/compiler/leanpkg.path
@@ -0,0 +1,2 @@
+builtin_path
+path .
diff --git a/doc/examples/compiler/main.cpp b/doc/examples/compiler/main.cpp
new file mode 100644
index 0000000000..a4d9a76764
--- /dev/null
+++ b/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;
+}
diff --git a/doc/examples/compiler/test.lean b/doc/examples/compiler/test.lean
new file mode 100644
index 0000000000..27b10fea60
--- /dev/null
+++ b/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)