Add structs to FFI

src/frontends/lean/decl_attributes.cpp

@@ -135,7 +135,7 @@ bool decl_attributes::ok_for_inductive_type() const {
     for (entry const & e : m_entries) {
         name const & n = e.m_attr->get_name();
         if (is_system_attribute(n)) {
-            if ((n != "class" && !is_class_symbol_tracking_attribute(n)) || e.deleted())
+            if ((n != "class" && n != "ffi" && !is_class_symbol_tracking_attribute(n)) || e.deleted())
                 return false;
         }
     }

src/frontends/lean/structure_cmd.cpp

@@ -108,6 +108,25 @@ buffer<name> get_structure_fields(environment const & env, name const & S) {
     return fields;
 }
 
+buffer<std::tuple<name,expr>> get_structure_field_types(environment const & env, name const & S) {
+    lean_assert(is_structure_like(env, S));
+    buffer<std::tuple<name,expr>> fields;
+    level_param_names ls; unsigned nparams; inductive::intro_rule intro;
+    std::tie(ls, nparams, intro) = get_structure_info(env, S);
+    expr intro_type = inductive::intro_rule_type(intro);
+    unsigned i = 0;
+    while (is_pi(intro_type)) {
+        if (i >= nparams)
+            fields.push_back(std::make_tuple(deinternalize_field_name(binding_name(intro_type)),
+                                             binding_domain(intro_type)));
+        i++;
+        auto local = mk_local(mk_fresh_name(), binding_name(intro_type),
+                              binding_domain(intro_type), binding_info(intro_type));
+        intro_type = instantiate(binding_body(intro_type), local);
+    }
+    return fields;
+}
+
 bool is_structure(environment const & env, name const & S) {
     if (!is_structure_like(env, S))
         return false;

src/frontends/lean/structure_cmd.h

@@ -12,6 +12,8 @@ namespace lean {
 environment structure_cmd(parser & p, cmd_meta const & meta);
 environment class_cmd(parser & p, cmd_meta const & meta);
 buffer<name> get_structure_fields(environment const & env, name const & S);
+ buffer<std::tuple<name,expr>> get_structure_field_types(environment const & env, name const & S);
+
 void register_structure_cmd(cmd_table & r);
 /** \brief Return true iff \c S is a structure created with the structure command */
 bool is_structure(environment const & env, name const & S);

src/library/vm/vm.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "util/small_object_allocator.h"
 #include "util/sexpr/option_declarations.h"
 #include "util/shared_mutex.h"
+#include "frontends/lean/structure_cmd.h"
 #include "library/constants.h"
 #include "library/kernel_serializer.h"
 #include "library/trace.h"
@@ -1047,8 +1048,8 @@ vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_cfun
     m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_arity(arity), m_cfn(fn) {}
 
 vm_decl_cell::vm_decl_cell(name const & n, unsigned idx,
-                           unique_ptr<vm_cfun_sig> sig, vm_cfunction fn):
-    m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_arity(sig->arity()), m_sig(std::move(sig)), m_cfn(fn) {}
+                           unique_ptr<vm_ffi_call> sig, unsigned arity, vm_cfunction fn):
+    m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_arity(arity), m_sig(std::move(sig)), m_cfn(fn) {}
 
 vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code,
                            list<vm_local_info> const & args_info, optional<pos_info> const & pos,
@@ -1145,11 +1146,17 @@ void declare_vm_cases_builtin(name const & n, char const * i, vm_cases_function
     g_vm_cases_builtins->insert(n, std::make_tuple(i, fn));
 }
 
+struct vm_ffi_struct {
+    ffi_type m_struct;
+    buffer<ffi_type *> m_fields;
+};
+
 /** \brief VM function/constant declarations are stored in an environment extension. */
 struct vm_decls : public environment_extension {
     unsigned_map<vm_decl>            m_decls;
     unsigned_map<vm_cases_function>  m_cases;
     std::unordered_map<name, vm_foreign_obj, name_hash> m_foreign;
+    std::unordered_map<name, std::shared_ptr<vm_ffi_struct>, name_hash> m_native_types;
 
     name                            m_monitor;
 
@@ -1187,6 +1194,11 @@ struct vm_decls : public environment_extension {
         m_decls.insert(idx, m_foreign[obj].get_cfun(decl, idx, c_fun, args, t));
     }
 
+    void bind_foreign_constructor(name const & decl) {
+        auto idx = get_vm_index(decl);
+        m_decls.insert(idx, _);
+    }
+
     unsigned reserve(name const & n, unsigned arity) {
         unsigned idx = get_vm_index(n);
         if (m_decls.contains(idx))
@@ -1285,6 +1297,41 @@ environment add_foreign_symbol(environment const & env, name const & obj, name c
     return update(env, ext);
 }
 
+environment add_foreign_struct(environment const & env, name const & n) {
+    auto ext = get_extension(env);
+    buffer<std::tuple<name,expr>> struct_fields = get_structure_field_types(env, n);
+    std::shared_ptr<vm_ffi_struct> m_struct = std::make_shared<vm_ffi_struct>();
+
+    ffi_type & tm_type = m_struct->m_struct;
+    buffer<ffi_type *> & tm_elements = m_struct->m_fields;
+
+    tm_type.size = tm_type.alignment = 0;
+    tm_type.type = FFI_TYPE_STRUCT;
+
+    // field_typ
+    name field; expr ftype;
+    for (auto & fn : struct_fields) {
+        std::tie(field, ftype) = fn;
+        // declaration decl = env.get({n, fn});
+        // expr t = decl.get_type();
+        // my_struct -> int_32
+        if (!is_constant(ftype))
+            throw exception("Only constant expressions are allowed in struct fields");
+        auto n = const_name(ftype);
+        tm_elements.push_back( &ext.m_native_types[n]->m_struct );
+    }
+    tm_elements.push_back( NULL );
+
+    tm_type.elements = m_struct->m_fields.data();
+
+    lean_assert(ext.m_native_types.find(n) == ext.m_native_types.end());
+
+    ext.m_native_types[n] = m_struct;
+    // ext.
+
+    return update(env, ext);
+}
+
 bool is_vm_function(environment const & env, name const & fn) {
     auto const & ext = get_extension(env);
     return ext.m_decls.contains(get_vm_index(fn)) || g_vm_builtins->contains(fn);
@@ -2946,9 +2993,19 @@ void vm_state::invoke_cfun(vm_decl const & d) {
         unique_lock<mutex> lk(m_call_stack_mtx);
         push_frame_core(0, 0, d.get_idx());
     }
-    if (d.is_ffi())
-        invoke_ffi_call(d.get_cfn(), d.get_sig());
-    else
+    if (d.is_ffi()) {
+        switch (d.get_sig().m_kind) {
+        case vm_ffi_call_kind::Ctor:
+            throw exception("not implemented");
+        case vm_ffi_call_kind::Cases:
+            throw exception("not implemented");
+        case vm_ffi_call_kind::CFun:
+            throw exception("not implemented");
+        case vm_ffi_call_kind::Field:
+            throw exception("not implemented");
+        }
+        // invoke_ffi_call(d.get_cfn(), d.get_sig());
+    } else
         invoke_fn(d.get_cfn(), d.get_arity());
     if (m_profiling) {
         unique_lock<mutex> lk(m_call_stack_mtx);

src/library/vm/vm.h

@@ -537,7 +537,20 @@ vm_instr mk_local_info_instr(unsigned idx, name const & n, optional<expr> const
 class vm_state;
 class vm_instr;
 
-struct vm_cfun_sig {
+enum class vm_ffi_call_kind { Ctor, Cases, CFun, Field };
+
+struct vm_ffi_call {
+    vm_ffi_call_kind m_kind;
+};
+
+/* used for implementing constructor, eliminator and projections of ffi structures */
+struct vm_cstruct_fields : vm_ffi_call {
+    ffi_type m_struct;
+    buffer<ffi_type*> m_fields;
+    buffer<ffi_type> m_alloc;
+};
+
+struct vm_cfun_sig : vm_ffi_call {
     buffer<ffi_type *> m_args;
     ffi_type *m_rtype;
     ffi_cif m_cif;
@@ -558,7 +571,7 @@ struct vm_decl_cell {
     list<vm_local_info>   m_args_info;
     optional<pos_info>    m_pos;
     optional<std::string> m_olean;
-    unique_ptr<vm_cfun_sig> m_sig;
+    unique_ptr<vm_ffi_call> m_sig;
     union {
         struct {
             unsigned   m_code_size;
@@ -569,7 +582,7 @@ struct vm_decl_cell {
     };
     vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn);
     vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_cfunction fn);
-    vm_decl_cell(name const & n, unsigned idx, unique_ptr<vm_cfun_sig> sig, vm_cfunction fn);
+    vm_decl_cell(name const & n, unsigned idx, unique_ptr<vm_ffi_call> sig, unsigned arity, vm_cfunction fn);
     vm_decl_cell(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code,
                  list<vm_local_info> const & args_info, optional<pos_info> const & pos,
                  optional<std::string> const & olean);
@@ -585,8 +598,8 @@ class vm_decl {
     vm_decl():m_ptr(nullptr) {}
     vm_decl(name const & n, unsigned idx, unsigned arity, vm_function fn):
         vm_decl(new vm_decl_cell(n, idx, arity, fn)) {}
-    vm_decl(name const & n, unsigned idx, unique_ptr<vm_cfun_sig> sig, vm_cfunction fn):
-        vm_decl(new vm_decl_cell(n, idx, std::move(sig), fn)) {}
+    vm_decl(name const & n, unsigned idx, unique_ptr<vm_ffi_call> sig, unsigned arity, vm_cfunction fn):
+        vm_decl(new vm_decl_cell(n, idx, std::move(sig), arity, fn)) {}
     vm_decl(name const & n, unsigned idx, unsigned arity, vm_cfunction fn):
         vm_decl(new vm_decl_cell(n, idx, arity, fn)) {}
     vm_decl(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code,
@@ -611,7 +624,7 @@ class vm_decl {
     bool is_ffi()  const { lean_assert(m_ptr); return is_cfun() && m_ptr->m_sig.get() != nullptr; }
     unsigned get_idx() const { lean_assert(m_ptr); return m_ptr->m_idx; }
     name get_name() const { lean_assert(m_ptr); return m_ptr->m_name; }
-    vm_cfun_sig const & get_sig() const { lean_assert(m_ptr && is_ffi()); return *m_ptr->m_sig; }
+    vm_ffi_call const & get_sig() const { lean_assert(m_ptr && is_ffi()); return *m_ptr->m_sig; }
     unsigned get_arity() const { lean_assert(m_ptr); return m_ptr->m_arity; }
     unsigned get_code_size() const { lean_assert(is_bytecode()); return m_ptr->m_code_size; }
     vm_instr const * get_code() const { lean_assert(is_bytecode()); return m_ptr->m_code; }
@@ -929,6 +942,7 @@ environment add_native(environment const & env, name const & n, unsigned arity,
 environment load_foreign_object(environment const & env, name const & n, std::string const & file_name);
 environment add_foreign_symbol(environment const & env, name const & obj, name const & fn,
                                std::string const & symbol);
+environment add_foreign_struct(environment const & env, name const & n);
 
 unsigned get_vm_index(name const & n);
 unsigned get_vm_index_bound();

src/library/vm/vm_ffi.cpp

@@ -20,6 +20,7 @@ Author: James King <[email protected]>, Simon Hudon
 #include "util/lean_path.h"
 #include "library/vm/vm_ffi.h"
 #include "library/vm/vm_parser.h"
+#include "frontends/lean/structure_cmd.h"
 
 namespace lean {
 
@@ -67,7 +68,13 @@ namespace lean {
         for (auto e : _args) { args.push_back(to_ffi_type(e)); }
         ffi_type * rt = to_ffi_type(_rt);
         unique_ptr<vm_cfun_sig> sig(new vm_cfun_sig(FFI_DEFAULT_ABI, *rt, std::move(args)));
-        return vm_decl(n, idx, std::move(sig), fn);
+        return vm_decl(n, idx, std::move(sig), args.size(), fn);
+    }
+
+    vm_decl vm_foreign_obj_cell::mk_ctor(name const & n, unsigned idx, string const & fun_name,
+                                          buffer<expr> const & _args, expr const & _rt) {
+
+        return vm_decl( );
     }
 
     vm_foreign_obj_cell::~vm_foreign_obj_cell() {
@@ -89,6 +96,12 @@ namespace lean {
         m_ptr->inc_ref();
     }
 
+    vm_foreign_value * vm_foreign_value::make(size_t size, void * data) {
+        auto result = new (new char[ sizeof(vm_foreign_value) + size ]) vm_foreign_value(size);
+        memcpy(result->data(), data, size);
+        return result;
+    }
+
     struct vm_ffi_attribute_data : public attr_data {
         name m_obj;
         optional<name> m_c_fun;
@@ -137,12 +150,16 @@ namespace lean {
         g_int64_name  = new name ({"foreign", "int_64"});
 
         register_system_attribute(vm_ffi_attribute(
-            *g_vm_ffi, "Registers a binding to a foreign function.",
+            *g_vm_ffi, "Registers a binding to a foreign function or structure.",
             [](environment const & env, io_state const &, name const & d, unsigned, bool) -> environment {
-                auto data = get_vm_ffi_attribute().get(env, d);
-                name sym = data->m_c_fun? *data->m_c_fun : d;
-                auto b = add_foreign_symbol(env, data->m_obj, d, sym.to_string());
-                return b;
+                if (is_structure(env, d)) {
+                    // auto struct_fields = get_structure_fields(env, d);
+                    return add_foreign_struct(env, d);
+                } else {
+                    auto ffi_attr = get_vm_ffi_attribute().get(env, d);
+                    name sym = ffi_attr->m_c_fun? *ffi_attr->m_c_fun : d;
+                    return add_foreign_symbol(env, ffi_attr->m_obj, d, sym.to_string());
+                }
             }));
     }
 

src/library/vm/vm_ffi.h

@@ -45,9 +45,25 @@ namespace lean {
         ~vm_foreign_obj() { if (m_ptr) { m_ptr->dec_ref(); } }
     };
 
-    void initialize_vm_ffi();
-
-    void finalize_vm_ffi();
+    class vm_foreign_value : public vm_external {
+    private:
+        size_t m_size;
+        vm_foreign_value(unsigned size) : m_size(size) { }
+        virtual void dealloc() override {
+            delete [] reinterpret_cast<char *>(this); }
+    public:
+        static vm_foreign_value * make(size_t size, void * data);
+        template <typename T>
+        static vm_foreign_value * make(T const & x) { return make(sizeof(T), &x); }
+        void * data() { return &m_size + 1; }
+        size_t size() const { return m_size; }
+        virtual vm_external * ts_clone(vm_clone_fn const &) override {
+            return new (new char[ sizeof(vm_foreign_value) + m_size ]) vm_foreign_value(m_size);
+        }
+        virtual vm_external * clone(vm_clone_fn const &) override {
+            return new (get_vm_allocator().allocate(sizeof(vm_foreign_value) + m_size)) vm_foreign_value(m_size);
+        }
+    };
 
     void initialize_vm_ffi();
 

tests/lean/ffi.lean

@@ -31,5 +31,9 @@ run_cmd trace "\nnext!\n"
 @[ffi foo]
 constant my_fun : uint_32 → int_64 → int_64
 
+@[ffi foo]
+structure my_basic_struct :=
+(count : uint_32) (result : int_64)
+
 
 #eval my_fun 7 3

tests/lean/vm_dynload/some_file.c

@@ -1,3 +1,7 @@
+struct my_basic_struct {
+  int count;
+  long result;
+} my_struct;
 
 long my_fun (int x, long y) {
     return x * y;