From 8bccfc23dabac82b9e34de41faaf7d9e9af3dda0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 31 May 2016 18:45:14 -0700
Subject: [PATCH] feat(library/vm): add example of C function invoking Lean
 closure

---
 library/init/nat.lean     |  5 +++++
 src/library/constants.cpp |  4 ++++
 src/library/constants.h   |  1 +
 src/library/constants.txt |  1 +
 src/library/vm/vm_nat.cpp | 21 +++++++++++++++++++++
 5 files changed, 32 insertions(+)

diff --git a/library/init/nat.lean b/library/init/nat.lean
index f2b25723de..684877560b 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -276,6 +276,11 @@ namespace nat
 
   theorem sub_lt_succ_iff_true [simp] (a b : ℕ) : a - b < succ a ↔ true :=
   iff_true_intro !sub_lt_succ
+
+  definition repeat {A : Type} (f : nat → A → A) : nat → A → A
+  | 0         a := a
+  | (succ n)  a := f n (repeat n a)
+
 end nat
 
 protected definition nat.is_inhabited [instance] : inhabited nat :=
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 7384a58e62..30421d23ec 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -131,6 +131,7 @@ name const * g_nat_decidable_le = nullptr;
 name const * g_nat_decidable_lt = nullptr;
 name const * g_nat_cases_on = nullptr;
 name const * g_nat_rec_on = nullptr;
+name const * g_nat_repeat = nullptr;
 name const * g_nat_no_confusion = nullptr;
 name const * g_nat_no_confusion_type = nullptr;
 name const * g_nat_has_zero = nullptr;
@@ -444,6 +445,7 @@ void initialize_constants() {
     g_nat_decidable_lt = new name{"nat", "decidable_lt"};
     g_nat_cases_on = new name{"nat", "cases_on"};
     g_nat_rec_on = new name{"nat", "rec_on"};
+    g_nat_repeat = new name{"nat", "repeat"};
     g_nat_no_confusion = new name{"nat", "no_confusion"};
     g_nat_no_confusion_type = new name{"nat", "no_confusion_type"};
     g_nat_has_zero = new name{"nat_has_zero"};
@@ -758,6 +760,7 @@ void finalize_constants() {
     delete g_nat_decidable_lt;
     delete g_nat_cases_on;
     delete g_nat_rec_on;
+    delete g_nat_repeat;
     delete g_nat_no_confusion;
     delete g_nat_no_confusion_type;
     delete g_nat_has_zero;
@@ -1071,6 +1074,7 @@ name const & get_nat_decidable_le_name() { return *g_nat_decidable_le; }
 name const & get_nat_decidable_lt_name() { return *g_nat_decidable_lt; }
 name const & get_nat_cases_on_name() { return *g_nat_cases_on; }
 name const & get_nat_rec_on_name() { return *g_nat_rec_on; }
+name const & get_nat_repeat_name() { return *g_nat_repeat; }
 name const & get_nat_no_confusion_name() { return *g_nat_no_confusion; }
 name const & get_nat_no_confusion_type_name() { return *g_nat_no_confusion_type; }
 name const & get_nat_has_zero_name() { return *g_nat_has_zero; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 1ae4bed802..c4d64872b8 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -133,6 +133,7 @@ name const & get_nat_decidable_le_name();
 name const & get_nat_decidable_lt_name();
 name const & get_nat_cases_on_name();
 name const & get_nat_rec_on_name();
+name const & get_nat_repeat_name();
 name const & get_nat_no_confusion_name();
 name const & get_nat_no_confusion_type_name();
 name const & get_nat_has_zero_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 6bf7fa9893..d2c8b96188 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -126,6 +126,7 @@ nat.decidable_le
 nat.decidable_lt
 nat.cases_on
 nat.rec_on
+nat.repeat
 nat.no_confusion
 nat.no_confusion_type
 nat_has_zero
diff --git a/src/library/vm/vm_nat.cpp b/src/library/vm/vm_nat.cpp
index ed354b0a0f..d55c364b05 100644
--- a/src/library/vm/vm_nat.cpp
+++ b/src/library/vm/vm_nat.cpp
@@ -180,6 +180,26 @@ static vm_obj nat_to_string(vm_obj const & a) {
     return to_obj(out.str());
 }
 
+static vm_obj nat_repeat(vm_obj const &, vm_obj const & f, vm_obj const & n, vm_obj const & a) {
+    if (is_simple(n)) {
+        unsigned _n = cidx(n);
+        vm_obj   r  = a;
+        for (unsigned i = 0; i < _n ; i++) {
+            r = invoke(f, mk_vm_simple(i), r);
+        }
+        return r;
+    } else {
+        mpz _n = to_mpz(n);
+        mpz i(0);
+        vm_obj r = a;
+        while (i < _n) {
+            r = invoke(f, mk_vm_nat(i), r);
+            i++;
+        }
+        return r;
+    }
+}
+
 void initialize_vm_nat() {
     declare_vm_builtin(get_nat_succ_name(),              nat_succ);
     declare_vm_builtin(get_nat_add_name(),               nat_add);
@@ -196,6 +216,7 @@ void initialize_vm_nat() {
     declare_vm_builtin(get_nat_no_confusion_name(),      5, nat_no_confusion);
     declare_vm_builtin(get_nat_no_confusion_type_name(), 3, nat_no_confusion);
     declare_vm_builtin(get_nat_to_string_name(),         nat_to_string);
+    declare_vm_builtin(get_nat_repeat_name(),            nat_repeat);
 }
 
 void finalize_vm_nat() {