feat(library/vm): add example of C function invoking Lean closure

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 :=

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; }

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();

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

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() {