feat(runtime/thunk): add runtime support for thunks

We did not use constructor objects for implementing thunks because we
wanted to use `atomic<object *>` to implement the cached result.

src/runtime/object.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include "runtime/object.h"
 #include "runtime/utf8.h"
+#include "runtime/apply.h"
 
 namespace lean {
 size_t obj_byte_size(object * o) {
@@ -19,6 +20,7 @@ size_t obj_byte_size(object * o) {
     case object_kind::ScalarArray:     return sarray_byte_size(o);
     case object_kind::String:          return string_byte_size(o);
     case object_kind::MPZ:             return sizeof(mpz_object);
+    case object_kind::Thunk:           return sizeof(thunk_object);
     case object_kind::External:        lean_unreachable();
     }
     lean_unreachable();
@@ -32,6 +34,7 @@ size_t obj_header_size(object * o) {
     case object_kind::ScalarArray:     return sizeof(sarray_object);
     case object_kind::String:          return sizeof(string_object);
     case object_kind::MPZ:             return sizeof(mpz_object);
+    case object_kind::Thunk:           return sizeof(thunk_object);
     case object_kind::External:        lean_unreachable();
     }
     lean_unreachable();
@@ -99,6 +102,11 @@ void del(object * o) {
             free(o); break;
         case object_kind::MPZ:
             dealloc_mpz(o); break;
+        case object_kind::Thunk:
+            dec_ref(to_thunk(o)->m_closure, todo);
+            if (object * v = to_thunk(o)->m_value) dec_ref(v, todo);
+            free(o);
+            break;
         case object_kind::External:
             dealloc_external(o); break;
         }

src/runtime/object.h

@@ -24,7 +24,7 @@ inline void * alloca(size_t s) {
 #endif
 }
 
-enum class object_kind { Constructor, Closure, Array, ScalarArray, String, MPZ, External };
+enum class object_kind { Constructor, Closure, Array, ScalarArray, String, MPZ, Thunk, External };
 
 /* The reference counter is a uintptr_t, because at deletion time, we use this field to implement
    a linked list of objects to be deleted. */
@@ -108,6 +108,12 @@ struct mpz_object : public object {
         object(object_kind::MPZ), m_value(v) {}
 };
 
+struct thunk_object : public object {
+    object *         m_closure;
+    atomic<object *> m_value;
+    thunk_object(object * c);
+};
+
 /* Base class for wrapping external_object data.
    For example, we use it to wrap the Lean environment object. */
 struct external_object : public object {
@@ -153,6 +159,7 @@ inline bool is_array(object * o) { return get_kind(o) == object_kind::Array; }
 inline bool is_sarray(object * o) { return get_kind(o) == object_kind::ScalarArray; }
 inline bool is_string(object * o) { return get_kind(o) == object_kind::String; }
 inline bool is_mpz(object * o) { return get_kind(o) == object_kind::MPZ; }
+inline bool is_thunk(object * o) { return get_kind(o) == object_kind::Thunk; }
 inline bool is_external(object * o) { return get_kind(o) == object_kind::External; }
 
 /* Casting */
@@ -162,6 +169,7 @@ inline array_object * to_array(object * o) { lean_assert(is_array(o)); return st
 inline sarray_object * to_sarray(object * o) { lean_assert(is_sarray(o)); return static_cast<sarray_object*>(o); }
 inline string_object * to_string(object * o) { lean_assert(is_string(o)); return static_cast<string_object*>(o); }
 inline mpz_object * to_mpz(object * o) { lean_assert(is_mpz(o)); return static_cast<mpz_object*>(o); }
+inline thunk_object * to_thunk(object * o) { lean_assert(is_thunk(o)); return static_cast<thunk_object*>(o); }
 inline external_object * to_external(object * o) { lean_assert(is_external(o)); return static_cast<external_object*>(o); }
 
 /* The memory associated with all Lean objects but `mpz_object` and `external_object` can be deallocated using `free`.
@@ -320,6 +328,30 @@ inline void sarray_set_size(object * o, size_t sz) {
 inline object * alloc_mpz(mpz const & m) { return new mpz_object(m); }
 inline mpz const & mpz_value(object * o) { return to_mpz(o)->m_value; }
 
+/* Thunks */
+
+inline thunk_object::thunk_object(object * c):
+    object(object_kind::Thunk), m_closure(c), m_value(nullptr) {
+    /* Remark: the implementation relies on the fact that nullptr is not a valid lean object. */
+    lean_assert(is_closure(c));
+    inc_ref(c);
+}
+
+inline object * alloc_thunk(object * c) {
+    return new (malloc(sizeof(thunk_object))) thunk_object(c); // NOLINT
+}
+
+object * apply_1(object * f, object * a1);
+
+inline object * thunk_get(object * t) {
+   if (object * r = to_thunk(t)->m_value)
+       return r;
+   object * r = apply_1(to_thunk(t)->m_closure, box(0));
+   lean_assert(r != nullptr); /* Closure must return a valid lean object */
+   to_thunk(t)->m_value = r;
+   return r;
+}
+
 /* String */
 inline object * alloc_string(size_t size, size_t capacity, size_t len) {
     return new (malloc(sizeof(string_object) + capacity)) string_object(size, capacity, len); // NOLINT

src/tests/util/CMakeLists.txt

@@ -1,3 +1,6 @@
+add_executable(object object.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
+target_link_libraries(object ${EXTRA_LIBS})
+add_exec_test(object "object")
 add_executable(name name.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
 target_link_libraries(name ${EXTRA_LIBS})
 add_exec_test(name "name")

src/tests/util/object.cpp

@@ -0,0 +1,78 @@
+/*
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <iostream>
+#include "util/test.h"
+#include "util/object_ref.h"
+#include "util/init_module.h"
+using namespace lean;
+
+object * f(object *) {
+    std::cout << "executing f...\n";
+    return box(10);
+}
+
+static void tst1() {
+    object_ref c(alloc_closure(f, 1, 0));
+    object_ref t(alloc_thunk(c.raw()));
+    object * r1 = thunk_get(t.raw());
+    object * r2 = thunk_get(t.raw());
+    std::cout << "thunk value: " << unbox(r1) << "\n";
+    std::cout << "thunk value: " << unbox(r2) << "\n";
+}
+
+static unsigned g_g_counter = 0;
+
+object * g(object *) {
+    g_g_counter++;
+    return box(g_g_counter);
+}
+
+static void tst2() {
+    object_ref c(alloc_closure(g, 1, 0));
+    object * r1 = apply_1(c.raw(), box(0));
+    object * r2 = apply_1(c.raw(), box(0));
+    lean_assert(unbox(r1) == 1);
+    lean_assert(unbox(r2) == 2);
+    object_ref t(alloc_thunk(c.raw()));
+    object * r3 = thunk_get(t.raw());
+    object * r4 = thunk_get(t.raw());
+    lean_assert(unbox(r3) == 3);
+    lean_assert(unbox(r4) == 3);
+}
+
+static unsigned g_h_counter = 0;
+
+object * h(object *) {
+    g_h_counter++;
+    return box(0);
+}
+
+/* Make sure box(0) is not mistaken by cached value has not been initialized yet.
+
+   The thunk implementation relies on the fact that nullptr is not a scalar nor a valid
+   Lean object. */
+static void tst3() {
+    object_ref c(alloc_closure(h, 1, 0));
+    object_ref t(alloc_thunk(c.raw()));
+    lean_assert(g_h_counter == 0);
+    object * r3 = thunk_get(t.raw());
+    lean_assert(g_h_counter == 1);
+    object * r4 = thunk_get(t.raw());
+    lean_assert(g_h_counter == 1);
+    lean_assert(unbox(r3) == 0);
+    lean_assert(unbox(r4) == 0);
+}
+
+int main() {
+    save_stack_info();
+    initialize_util_module();
+    tst1();
+    tst2();
+    tst3();
+    finalize_util_module();
+    return has_violations() ? 1 : 0;
+}