feat(library/compiler): thunk support

src/library/compiler/builtin.cpp

@@ -16,9 +16,11 @@ struct builtin_decl {
     char const *      m_cname;
     bool              m_borrowed_res;
     list<bool>        m_borrowed_args;
+    list<bool>        m_used_args;
     builtin_decl() {}
-    builtin_decl(expr const & type, unsigned arity, char const * cname, bool bres, list<bool> const & bargs):
-        m_type(type), m_arity(arity), m_cname(cname), m_borrowed_res(bres), m_borrowed_args(bargs) {
+    builtin_decl(expr const & type, unsigned arity, char const * cname, bool bres, list<bool> const & bargs,
+                 list<bool> const & used_args):
+        m_type(type), m_arity(arity), m_cname(cname), m_borrowed_res(bres), m_borrowed_args(bargs), m_used_args(used_args) {
     }
 };
 
@@ -26,24 +28,37 @@ typedef std::unordered_map<name, builtin_decl, name_hash> builtin_map;
 
 static builtin_map * g_builtin_decls = nullptr;
 
-void register_builtin(name const & n, expr const & type, unsigned arity, char const * cname, bool borrowed_res, list<bool> const & borrowed_arg) {
+void register_builtin(name const & n, expr const & type, unsigned arity, char const * cname,
+                      bool borrowed_res, list<bool> const & borrowed_arg,
+                      list<bool> const & used_args) {
     lean_assert(g_builtin_decls->find(n) == g_builtin_decls->end());
-    g_builtin_decls->insert(mk_pair(n, builtin_decl(type, arity, cname, borrowed_res, borrowed_arg)));
+    g_builtin_decls->insert(mk_pair(n, builtin_decl(type, arity, cname, borrowed_res, borrowed_arg, used_args)));
 }
 
-void register_builtin(name const & n, expr const & type, char const * cname, bool borrowed_res, list<bool> const & borrowed_arg) {
+void register_builtin(name const & n, expr const & type, char const * cname,
+                      bool borrowed_res, list<bool> const & borrowed_arg,
+                      list<bool> const & used_args) {
     unsigned arity = get_arity(type);
-    return register_builtin(n, type, arity, cname, borrowed_res, borrowed_arg);
+    return register_builtin(n, type, arity, cname, borrowed_res, borrowed_arg, used_args);
+}
+
+void register_builtin(name const & n, expr const & type, char const * cname, list<bool> const & borrowed_arg, list<bool> const & used_args) {
+    return register_builtin(n, type, cname, false, borrowed_arg, used_args);
 }
 
 void register_builtin(name const & n, expr const & type, char const * cname, list<bool> const & borrowed_arg) {
-    return register_builtin(n, type, cname, false, borrowed_arg);
+    unsigned arity = get_arity(type);
+    buffer<bool> used_args;
+    used_args.resize(arity, true);
+    return register_builtin(n, type, cname, false, borrowed_arg, to_list(used_args));
 }
 
 void register_builtin(name const & n, expr const & type, unsigned arity, char const * cname) {
     buffer<bool> borrowed;
     borrowed.resize(arity, false);
-    return register_builtin(n, type, arity, cname, false, to_list(borrowed));
+    buffer<bool> used_args;
+    used_args.resize(arity, true);
+    return register_builtin(n, type, arity, cname, false, to_list(borrowed), to_list(used_args));
 }
 
 void register_builtin(name const & n, expr const & type, char const * cname) {
@@ -86,6 +101,15 @@ bool get_builtin_borrowed_info(name const & c, buffer<bool> & borrowed_args, boo
     return true;
 }
 
+bool get_builtin_used_args(name const & c, buffer<bool> & used_args) {
+    auto it = g_builtin_decls->find(c);
+    if (it == g_builtin_decls->end())
+        return false;
+
+    to_buffer(it->second.m_used_args, used_args);
+    return true;
+}
+
 void initialize_builtin() {
     g_builtin_decls = new builtin_map();
 
@@ -98,6 +122,7 @@ void initialize_builtin() {
     expr o_o         = mk_arrow(o, o);
     expr o_o_o       = mk_arrow(o, o_o);
     expr o_o_o_o     = mk_arrow(o, o_o_o);
+    expr o_o_o_o_o   = mk_arrow(o, o_o_o_o);
 
     expr o_u8        = mk_arrow(o, u8);
     expr o_u8_u8_o_o = mk_arrow(o, mk_arrow(u8, mk_arrow(u8, o_o)));
@@ -148,6 +173,10 @@ void initialize_builtin() {
     list<bool> bc{true, false};
     list<bool> bbb{true, true, true};
     list<bool> bccc{true, false, false, false};
+    list<bool> bbcc{true, true, false, false};
+
+    list<bool> xu{false, true};
+    list<bool> xxuu{false, false, true, true};
 
     /* nat builtin functions */
     register_builtin(name({"nat", "add"}), o_o_o, "lean::nat_add", bb);
@@ -280,6 +309,13 @@ void initialize_builtin() {
     register_builtin(name({"usize", "dec_eq"}), us_us_o, "lean::usize_dec_eq");
     register_builtin(name({"usize", "dec_lt"}), us_us_o, "lean::usize_dec_lt");
     register_builtin(name({"usize", "dec_le"}), us_us_o, "lean::usize_dec_le");
+
+    /* thunk builtin functions */
+    register_builtin(name({"thunk", "mk"}), o_o_o, "lean::mk_thunk", bc, xu);
+    register_builtin(name({"thunk", "pure"}), o_o_o, "lean::thunk_pure", bc, xu);
+    register_builtin(name({"thunk", "get"}), o_o_o, "lean::thunk_get", bb, xu);
+    register_builtin(name({"thunk", "bind"}), o_o_o_o_o, "lean::thunk_get", bb, xu);
+    register_builtin(name({"thunk", "map"}), o_o_o_o_o, "lean::thunk_bind", bbcc, xxuu);
 }
 
 void finalize_builtin() {

src/library/compiler/builtin.h

@@ -14,6 +14,9 @@ optional<unsigned> get_builtin_constant_arity(name const & c);
 /* Return true if `c` is a builtin, and store in borrowed_args and
    borrowed_res which arguments/results are marked as borrowed. */
 bool get_builtin_borrowed_info(name const & c, buffer<bool> & borrowed_args, bool & borrowed_res);
+/* Return true if `c` is a builtin, and store in used_args a bit mask specifying
+   which arguments the builtin implementation takes as argument. */
+bool get_builtin_used_args(name const & c, buffer<bool> & used_args);
 void initialize_builtin();
 void finalize_builtin();
 }

src/library/compiler/emit_cpp.cpp

@@ -549,6 +549,23 @@ struct emit_fn_fn {
         m_out << ");\n";
     }
 
+    void emit_builtin(expr const & x, expr const & fn, buffer<expr> const & args) {
+        buffer<bool> used_args;
+        lean_verify(get_builtin_used_args(const_name(fn), used_args));
+        lean_assert(used_args.size() == args.size());
+        emit_lhs(x);
+        emit_constant(fn);
+        m_out << "(";
+        bool first = true;
+        for (unsigned i = 0; i < args.size(); i++) {
+            if (used_args[i]) {
+                if (first) first = false; else m_out << ", ";
+                emit_arg(args[i]);
+            }
+        }
+        m_out << ");\n";
+    }
+
     void emit_instr(local_decl const & d) {
         expr x = d.mk_ref();
         expr val = *d.get_value();
@@ -593,6 +610,8 @@ struct emit_fn_fn {
                 emit_unbox(x, fn, args[0]);
             } else if (is_llnf_box(fn)) {
                 emit_box(x, fn, args[0]);
+            } else if (is_builtin_constant(const_name(fn))) {
+                emit_builtin(x, fn, args);
             } else {
                 /* Regular function application. */
                 emit_lhs(x);

src/library/compiler/util.cpp

@@ -384,7 +384,7 @@ bool is_runtime_builtin_type(name const & n) {
         n == get_uint32_name() ||
         n == get_uint64_name() ||
         n == get_usize_name()  ||
-        // n == get_thunk_name()  ||  TODO(Leo): enable
+        n == get_thunk_name()  ||
         // n == get_task_name()   ||  TODO(Leo): enable
         // n == get_array_name()  ||  TODO(Leo): enable
         n == get_nat_name()    ||
@@ -401,12 +401,13 @@ bool is_runtime_scalar_type(name const & n) {
 }
 
 bool is_runtime_builtin_cnstr(name const & n) {
-    // TODO(Leo): add array type constructors, thunk constructor,
+    // TODO(Leo): add array type constructors, task constructor,
     // universe level constructors, and expression constructors.
 
     /* Remark: we don't need to include `nat.zero` and `nat.zero` because
        they are converted into literals or addition. */
     return
+        n == get_thunk_mk_name() ||
         n == get_string_mk_name() ||
         n == get_string_iterator_mk_name() ||
         n == get_int_of_nat_name() ||

src/library/constants.cpp

@@ -266,6 +266,7 @@ name const * g_tactic_triv = nullptr;
 name const * g_tactic_mk_inj_eq = nullptr;
 name const * g_task = nullptr;
 name const * g_thunk = nullptr;
+name const * g_thunk_mk = nullptr;
 name const * g_trans_rel_left = nullptr;
 name const * g_trans_rel_right = nullptr;
 name const * g_true = nullptr;
@@ -552,6 +553,7 @@ void initialize_constants() {
     g_tactic_mk_inj_eq = new name{"tactic", "mk_inj_eq"};
     g_task = new name{"task"};
     g_thunk = new name{"thunk"};
+    g_thunk_mk = new name{"thunk", "mk"};
     g_trans_rel_left = new name{"trans_rel_left"};
     g_trans_rel_right = new name{"trans_rel_right"};
     g_true = new name{"true"};
@@ -839,6 +841,7 @@ void finalize_constants() {
     delete g_tactic_mk_inj_eq;
     delete g_task;
     delete g_thunk;
+    delete g_thunk_mk;
     delete g_trans_rel_left;
     delete g_trans_rel_right;
     delete g_true;
@@ -1125,6 +1128,7 @@ name const & get_tactic_triv_name() { return *g_tactic_triv; }
 name const & get_tactic_mk_inj_eq_name() { return *g_tactic_mk_inj_eq; }
 name const & get_task_name() { return *g_task; }
 name const & get_thunk_name() { return *g_thunk; }
+name const & get_thunk_mk_name() { return *g_thunk_mk; }
 name const & get_trans_rel_left_name() { return *g_trans_rel_left; }
 name const & get_trans_rel_right_name() { return *g_trans_rel_right; }
 name const & get_true_name() { return *g_true; }

src/library/constants.h

@@ -268,6 +268,7 @@ name const & get_tactic_triv_name();
 name const & get_tactic_mk_inj_eq_name();
 name const & get_task_name();
 name const & get_thunk_name();
+name const & get_thunk_mk_name();
 name const & get_trans_rel_left_name();
 name const & get_trans_rel_right_name();
 name const & get_true_name();

src/library/constants.txt

@@ -261,6 +261,7 @@ tactic.triv
 tactic.mk_inj_eq
 task
 thunk
+thunk.mk
 trans_rel_left
 trans_rel_right
 true

src/library/vm/CMakeLists.txt

@@ -1,2 +1,2 @@
 add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp
-  vm_int.cpp vm_uint.cpp init_module.cpp)
+  vm_int.cpp vm_uint.cpp vm_thunk.cpp init_module.cpp)

src/library/vm/init_module.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_aux.h"
 #include "library/vm/vm_io.h"
 #include "library/vm/vm_string.h"
+#include "library/vm/vm_thunk.h"
 
 namespace lean {
 void initialize_vm_core_module() {
@@ -21,9 +22,11 @@ void initialize_vm_core_module() {
     initialize_vm_io();
     initialize_vm_string();
     initialize_vm_uint();
+    initialize_vm_thunk();
 }
 
 void finalize_vm_core_module() {
+    finalize_vm_thunk();
     finalize_vm_uint();
     finalize_vm_string();
     finalize_vm_io();

src/library/vm/vm_thunk.cpp

@@ -0,0 +1,27 @@
+/*
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/vm/vm.h"
+namespace lean {
+static vm_obj dummy_binary_op(vm_obj const &, vm_obj const &) {
+    throw exception("thunk support has not been implemented in the old VM");
+}
+
+static vm_obj dummy_quad_op(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &) {
+    throw exception("thunk support has not been implemented in the old VM");
+}
+
+void initialize_vm_thunk() {
+    DECLARE_VM_BUILTIN(name({"thunk", "mk"}),         dummy_binary_op);
+    DECLARE_VM_BUILTIN(name({"thunk", "get"}),        dummy_binary_op);
+    DECLARE_VM_BUILTIN(name({"thunk", "pure"}),       dummy_binary_op);
+    DECLARE_VM_BUILTIN(name({"thunk", "bind"}),       dummy_quad_op);
+    DECLARE_VM_BUILTIN(name({"thunk", "map"}),        dummy_quad_op);
+}
+
+void finalize_vm_thunk() {
+}
+}

src/library/vm/vm_thunk.h

@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+namespace lean {
+void initialize_vm_thunk();
+void finalize_vm_thunk();
+}

src/library/vm/vm_uint.cpp

@@ -6,11 +6,11 @@ Author: Leonardo de Moura
 */
 #include "library/vm/vm.h"
 namespace lean {
-vm_obj dummy_unary_op(vm_obj const &, vm_obj const &) {
+static vm_obj dummy_unary_op(vm_obj const &, vm_obj const &) {
     throw exception("uint support has not been implemented in the old VM");
 }
 
-vm_obj dummy_binary_op(vm_obj const &, vm_obj const &) {
+static vm_obj dummy_binary_op(vm_obj const &, vm_obj const &) {
     throw exception("uint support has not been implemented in the old VM");
 }