From cc8c11976899911a2e2ec258a5bfb1dd6d28a300 Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Sat, 25 May 2019 21:38:59 -0400 Subject: [PATCH 01/11] Add ffi test case for structs --- tests/lean/ffi.lean | 4 ++++ tests/lean/vm_dynload/some_file.c | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/tests/lean/ffi.lean b/tests/lean/ffi.lean index e9679144af..46f681f11b 100644 --- a/tests/lean/ffi.lean +++ b/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 diff --git a/tests/lean/vm_dynload/some_file.c b/tests/lean/vm_dynload/some_file.c index 28d0da2491..b6ccb43cff 100644 --- a/tests/lean/vm_dynload/some_file.c +++ b/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; From 04aac9830d13c393b10f4705606236c2c829f9de Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Sat, 25 May 2019 22:14:06 -0400 Subject: [PATCH 02/11] Modify src/library/vm/vm_ffi.cpp Rename a poorly named variable. --- src/library/vm/vm_ffi.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/library/vm/vm_ffi.cpp b/src/library/vm/vm_ffi.cpp index a423f82e5f..d24f36fe23 100644 --- a/src/library/vm/vm_ffi.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -137,11 +137,11 @@ 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()); + auto ffi_attr = get_vm_ffi_attribute().get(env, d); + name sym = ffi_attr->m_c_fun? *ffi_attr->m_c_fun : d; + auto b = add_foreign_symbol(env, ffi_attr->m_obj, d, sym.to_string()); return b; })); } From b376cc236ba2a7ecb816981a4f56be2bf062b785 Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Sun, 26 May 2019 17:52:15 -0400 Subject: [PATCH 03/11] Add vm_ffi_attribute_struct The idea here is that when we register the `ffi` attribute we'll case match on the expresssion: if it's a function definition use the function attribute, if it's a structure then use this one. --- src/library/vm/vm_ffi.cpp | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/library/vm/vm_ffi.cpp b/src/library/vm/vm_ffi.cpp index d24f36fe23..87e0687621 100644 --- a/src/library/vm/vm_ffi.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -125,6 +125,25 @@ namespace lean { return static_cast(get_system_attribute(*g_vm_ffi)); } + struct vm_ffi_attribute_struct : public attr_struct { + name m_obj; + optional m_c_struct; + // TODO: Find the type for Lean struct fields, build a Map + std::vector<> m_c_struct_fields; + vm_ffi_attribute_struct() {} + vm_ffi_attrivute_struct(name const & obj, + optional const & c_struct, + std::vector<> const & c_struct_fields) : + m_obj(obj), m_c_struct(c_struct), m_c_struct_fields(c_struct_fields) {} + virtual unsigned hash() const override { return m_obj.hash(); } + void write(serializer & s) const { s << m_obj << m_c_struct << m_c_struct_fields; } + void read(deserializer & d) { + d >> m_obj >> m_c_struct >> m_c_struct_fields + } + void parse(abstract_parser & p) override { + } + }; + void initialize_vm_ffi() { g_vm_ffi = new name("ffi"); g_uint8_name = new name ({"foreign", "uint_8"}); From 1da2dd653a73838f22a6da39b9d7d74b2a39dfa2 Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Sat, 1 Jun 2019 13:54:52 -0400 Subject: [PATCH 04/11] Remove parse method from ffi_attribute_struct We should be able to get the Lean struct definition from the environment without parsing the attribute field. --- src/library/vm/vm_ffi.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/library/vm/vm_ffi.cpp b/src/library/vm/vm_ffi.cpp index 87e0687621..61b3c2775c 100644 --- a/src/library/vm/vm_ffi.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -140,8 +140,6 @@ namespace lean { void read(deserializer & d) { d >> m_obj >> m_c_struct >> m_c_struct_fields } - void parse(abstract_parser & p) override { - } }; void initialize_vm_ffi() { From a197b58c3dbda830d49ac8c6776edbc7a4dd3d00 Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Sat, 1 Jun 2019 15:29:07 -0400 Subject: [PATCH 05/11] Get struct fields from environment WIP --- src/library/vm/vm_ffi.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/library/vm/vm_ffi.cpp b/src/library/vm/vm_ffi.cpp index 61b3c2775c..e222d43454 100644 --- a/src/library/vm/vm_ffi.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -156,6 +156,7 @@ namespace lean { register_system_attribute(vm_ffi_attribute( *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 struct_fields = environment_structure_fields(env, env.get(d)); auto ffi_attr = get_vm_ffi_attribute().get(env, d); name sym = ffi_attr->m_c_fun? *ffi_attr->m_c_fun : d; auto b = add_foreign_symbol(env, ffi_attr->m_obj, d, sym.to_string()); From 2f9b90db4c9265b5434c3b2ee428b8b4effa06cf Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Sat, 1 Jun 2019 16:06:22 -0400 Subject: [PATCH 06/11] Remove vm_ffi_attribute_struct Also start pulling in the struct definition from the vm --- src/library/vm/vm_ffi.cpp | 32 ++++++++++---------------------- 1 file changed, 10 insertions(+), 22 deletions(-) diff --git a/src/library/vm/vm_ffi.cpp b/src/library/vm/vm_ffi.cpp index e222d43454..a5503c9230 100644 --- a/src/library/vm/vm_ffi.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -125,23 +125,6 @@ namespace lean { return static_cast(get_system_attribute(*g_vm_ffi)); } - struct vm_ffi_attribute_struct : public attr_struct { - name m_obj; - optional m_c_struct; - // TODO: Find the type for Lean struct fields, build a Map - std::vector<> m_c_struct_fields; - vm_ffi_attribute_struct() {} - vm_ffi_attrivute_struct(name const & obj, - optional const & c_struct, - std::vector<> const & c_struct_fields) : - m_obj(obj), m_c_struct(c_struct), m_c_struct_fields(c_struct_fields) {} - virtual unsigned hash() const override { return m_obj.hash(); } - void write(serializer & s) const { s << m_obj << m_c_struct << m_c_struct_fields; } - void read(deserializer & d) { - d >> m_obj >> m_c_struct >> m_c_struct_fields - } - }; - void initialize_vm_ffi() { g_vm_ffi = new name("ffi"); g_uint8_name = new name ({"foreign", "uint_8"}); @@ -156,11 +139,16 @@ namespace lean { register_system_attribute(vm_ffi_attribute( *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 struct_fields = environment_structure_fields(env, env.get(d)); - auto ffi_attr = get_vm_ffi_attribute().get(env, d); - name sym = ffi_attr->m_c_fun? *ffi_attr->m_c_fun : d; - auto b = add_foreign_symbol(env, ffi_attr->m_obj, d, sym.to_string()); - return b; + auto v = to_env(env); + auto n = to_name(d); + if (is_structure(v, d)) { + auto struct_fields = get_structure_fields(v, 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; + auto b = add_foreign_symbol(env, ffi_attr->m_obj, d, sym.to_string()); + return b; + } })); } From 136867ea514381df416fea64917e0498dedbe9b6 Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Sat, 1 Jun 2019 16:12:23 -0400 Subject: [PATCH 07/11] Add missing include to vm_ffi.cpp --- src/library/vm/vm_ffi.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/library/vm/vm_ffi.cpp b/src/library/vm/vm_ffi.cpp index a5503c9230..7bab472aa2 100644 --- a/src/library/vm/vm_ffi.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -20,6 +20,7 @@ Author: James King , 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 { @@ -139,10 +140,8 @@ namespace lean { register_system_attribute(vm_ffi_attribute( *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 v = to_env(env); - auto n = to_name(d); - if (is_structure(v, d)) { - auto struct_fields = get_structure_fields(v, d); + if (is_structure(env, d)) { + auto struct_fields = get_structure_fields(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; From 0a637001d0fa441d7a4be0f15bef114809dfe116 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Sun, 2 Jun 2019 21:33:44 -0400 Subject: [PATCH 08/11] add vm foreign values [skip ci] --- src/library/vm/vm_ffi.cpp | 6 ++++++ src/library/vm/vm_ffi.h | 20 ++++++++++++++++++++ 2 files changed, 26 insertions(+) diff --git a/src/library/vm/vm_ffi.cpp b/src/library/vm/vm_ffi.cpp index 7bab472aa2..70313e01c2 100644 --- a/src/library/vm/vm_ffi.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -90,6 +90,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 m_c_fun; diff --git a/src/library/vm/vm_ffi.h b/src/library/vm/vm_ffi.h index 593da019a9..f07d2a7b4d 100644 --- a/src/library/vm/vm_ffi.h +++ b/src/library/vm/vm_ffi.h @@ -45,6 +45,26 @@ namespace lean { ~vm_foreign_obj() { if (m_ptr) { m_ptr->dec_ref(); } } }; + 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(this); } + public: + static vm_foreign_value * make(size_t size, void * data); + template + 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(); void finalize_vm_ffi(); From c0a447854204a7338b43d877db1c554614a467c3 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Sun, 2 Jun 2019 22:36:16 -0400 Subject: [PATCH 09/11] make different kinds of call for ffi structures [skip ci] --- src/library/vm/vm.h | 17 +++++++++++++++-- src/library/vm/vm_ffi.h | 4 ---- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 87b67fbc7b..cec54a464e 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -537,7 +537,20 @@ vm_instr mk_local_info_instr(unsigned idx, name const & n, optional const class vm_state; class vm_instr; -struct vm_cfun_sig { +enum class vm_ffi_call_kind { Ctor, Cases, CFun }; + +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 m_fields; + buffer m_alloc; +}; + +struct vm_cfun_sig : vm_ffi_call { buffer m_args; ffi_type *m_rtype; ffi_cif m_cif; @@ -558,7 +571,7 @@ struct vm_decl_cell { list m_args_info; optional m_pos; optional m_olean; - unique_ptr m_sig; + unique_ptr m_sig; union { struct { unsigned m_code_size; diff --git a/src/library/vm/vm_ffi.h b/src/library/vm/vm_ffi.h index f07d2a7b4d..fe0136b1d6 100644 --- a/src/library/vm/vm_ffi.h +++ b/src/library/vm/vm_ffi.h @@ -69,8 +69,4 @@ namespace lean { void finalize_vm_ffi(); - void initialize_vm_ffi(); - - void finalize_vm_ffi(); - } From ad33c2b189652b4e006a0f509cca22fd1c869c83 Mon Sep 17 00:00:00 2001 From: J Kenneth King Date: Tue, 18 Jun 2019 21:36:24 -0400 Subject: [PATCH 10/11] Modify src/library/vm/vm.cpp [skip ci] Added add_foreign_struct to create an ffi_type definition to tell libffi about a user struct type --- src/library/vm/vm.cpp | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 0e62cc4cd2..3a35edecf7 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -1285,6 +1285,31 @@ 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) { + buffer struct_fields = get_structure_fields(env, n); + ffi_type tm_type; + ffi_type * tm_elements[struct_fields.size() + 1]; + + tm_type.size = tm_type.alignment = 0; + tm_type.type = FFI_TYPE_STRUCT; + tm_type.elements = &tm_elements; + + // TODO: iterate over struct_fields, fetching the vm_obj from the + // environment and adding the appropriate ffi_type to tm_elements + // for it + for (auto & fn : struct_fields) { + declaration decl = env.get(fn); + expr t = decl.get_type(); + if (!is_constant(t)) + throw exception("Only constant expressions are allowed in struct fields"); + auto n = const_name(t); + // TODO: map n to ffi_type and add pointer to tm_elements + } + tm_elements[struct_fields.size() + 1] = NULL; + + // TODO: Add tm_type to the environment +} + 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); From 87a9e0b2357f294e3b04ecd3a7b74dfd023ec1d8 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Mon, 8 Jul 2019 21:42:21 -0400 Subject: [PATCH 11/11] add struct signature to `vm_decls` [skip ci] --- src/frontends/lean/decl_attributes.cpp | 2 +- src/frontends/lean/structure_cmd.cpp | 19 +++++++ src/frontends/lean/structure_cmd.h | 2 + src/library/vm/vm.cpp | 70 +++++++++++++++++++------- src/library/vm/vm.h | 11 ++-- src/library/vm/vm_ffi.cpp | 14 ++++-- tests/lean/ffi.lean | 2 +- 7 files changed, 90 insertions(+), 30 deletions(-) diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index efeaf738d7..5b4e042d41 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/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; } } diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 4085c337b9..d6e1002824 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -108,6 +108,25 @@ buffer get_structure_fields(environment const & env, name const & S) { return fields; } +buffer> get_structure_field_types(environment const & env, name const & S) { + lean_assert(is_structure_like(env, S)); + buffer> 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; diff --git a/src/frontends/lean/structure_cmd.h b/src/frontends/lean/structure_cmd.h index 644e7e244f..c9edb5a68c 100644 --- a/src/frontends/lean/structure_cmd.h +++ b/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 get_structure_fields(environment const & env, name const & S); + buffer> 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); diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 3a35edecf7..42ee569a64 100644 --- a/src/library/vm/vm.cpp +++ b/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 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 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 const & args_info, optional 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 m_fields; +}; + /** \brief VM function/constant declarations are stored in an environment extension. */ struct vm_decls : public environment_extension { unsigned_map m_decls; unsigned_map m_cases; std::unordered_map m_foreign; + std::unordered_map, 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)) @@ -1286,28 +1298,38 @@ environment add_foreign_symbol(environment const & env, name const & obj, name c } environment add_foreign_struct(environment const & env, name const & n) { - buffer struct_fields = get_structure_fields(env, n); - ffi_type tm_type; - ffi_type * tm_elements[struct_fields.size() + 1]; + auto ext = get_extension(env); + buffer> struct_fields = get_structure_field_types(env, n); + std::shared_ptr m_struct = std::make_shared(); + + ffi_type & tm_type = m_struct->m_struct; + buffer & tm_elements = m_struct->m_fields; tm_type.size = tm_type.alignment = 0; tm_type.type = FFI_TYPE_STRUCT; - tm_type.elements = &tm_elements; - // TODO: iterate over struct_fields, fetching the vm_obj from the - // environment and adding the appropriate ffi_type to tm_elements - // for it + // field_typ + name field; expr ftype; for (auto & fn : struct_fields) { - declaration decl = env.get(fn); - expr t = decl.get_type(); - if (!is_constant(t)) + 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(t); - // TODO: map n to ffi_type and add pointer to tm_elements + auto n = const_name(ftype); + tm_elements.push_back( &ext.m_native_types[n]->m_struct ); } - tm_elements[struct_fields.size() + 1] = NULL; + tm_elements.push_back( NULL ); - // TODO: Add tm_type to the environment + 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) { @@ -2971,9 +2993,19 @@ void vm_state::invoke_cfun(vm_decl const & d) { unique_lock 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 lk(m_call_stack_mtx); diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index cec54a464e..a0d4f4b8ff 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -537,7 +537,7 @@ vm_instr mk_local_info_instr(unsigned idx, name const & n, optional const class vm_state; class vm_instr; -enum class vm_ffi_call_kind { Ctor, Cases, CFun }; +enum class vm_ffi_call_kind { Ctor, Cases, CFun, Field }; struct vm_ffi_call { vm_ffi_call_kind m_kind; @@ -582,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 sig, vm_cfunction fn); + vm_decl_cell(name const & n, unsigned idx, unique_ptr sig, unsigned arity, vm_cfunction fn); vm_decl_cell(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code, list const & args_info, optional const & pos, optional const & olean); @@ -598,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 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 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, @@ -624,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; } @@ -942,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(); diff --git a/src/library/vm/vm_ffi.cpp b/src/library/vm/vm_ffi.cpp index 70313e01c2..2f46c20bbb 100644 --- a/src/library/vm/vm_ffi.cpp +++ b/src/library/vm/vm_ffi.cpp @@ -68,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 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 const & _args, expr const & _rt) { + + return vm_decl( ); } vm_foreign_obj_cell::~vm_foreign_obj_cell() { @@ -147,12 +153,12 @@ namespace lean { *g_vm_ffi, "Registers a binding to a foreign function or structure.", [](environment const & env, io_state const &, name const & d, unsigned, bool) -> environment { if (is_structure(env, d)) { - auto struct_fields = get_structure_fields(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; - auto b = add_foreign_symbol(env, ffi_attr->m_obj, d, sym.to_string()); - return b; + return add_foreign_symbol(env, ffi_attr->m_obj, d, sym.to_string()); } })); } diff --git a/tests/lean/ffi.lean b/tests/lean/ffi.lean index 46f681f11b..c9ec71c28d 100644 --- a/tests/lean/ffi.lean +++ b/tests/lean/ffi.lean @@ -33,7 +33,7 @@ constant my_fun : uint_32 → int_64 → int_64 @[ffi foo] structure my_basic_struct := -(count : uint_32) (result int_64) +(count : uint_32) (result : int_64) #eval my_fun 7 3