From b36b4f0d80de25937a6db2e652a61c2ea803e4ce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Jan 2019 13:27:21 -0800 Subject: [PATCH] feat(library/compiler/emit_cpp): emit function headers --- src/library/compiler/emit_cpp.cpp | 166 ++++++++++++++++++++++++++++-- src/library/compiler/emit_cpp.h | 2 +- src/library/compiler/llnf.h | 1 + 3 files changed, 159 insertions(+), 10 deletions(-) diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp index c6c8f821f3..17c74d828e 100644 --- a/src/library/compiler/emit_cpp.cpp +++ b/src/library/compiler/emit_cpp.cpp @@ -4,11 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include +#include #include "runtime/utf8.h" #include "library/attribute_manager.h" #include "library/module.h" +#include "library/compiler/llnf.h" +#include "library/compiler/name_mangling.h" #include "library/compiler/emit_cpp.h" +#include "library/compiler/builtin.h" namespace lean { struct cppname_attr_data : public attr_data { @@ -64,23 +67,168 @@ environment emit_cpp(environment const & env, comp_decls const & ds) { return update(env, ext); } -void print_cpp_code(std::ofstream & out, environment const & env, module_name const & m, list const & deps) { +static std::string to_cpp_type(expr const & e) { + if (is_constant(e)) { + if (e == mk_enf_object_type() || e == mk_enf_neutral_type()) { + return "obj*"; + } else if (const_name(e) == get_uint8_name()) { + return "unsigned char"; + } else if (const_name(e) == get_uint16_name()) { + return "unsigned short"; + } else if (const_name(e) == get_uint32_name()) { + return "unsigned"; + } else if (const_name(e) == get_uint64_name()) { + return "unsigned long long"; + } else if (const_name(e) == get_usize_name()) { + return "size_t"; + } + } + throw exception("unknown type"); +} + +static void open_namespaces_core(std::ostream & out, name const & p) { + if (p.is_anonymous()) return; + open_namespaces_core(out, p.get_prefix()); + lean_assert(p.is_string()); + out << "namespace " << p.get_string().to_std_string() << " {\n"; +} + +/* If `n` has the attribute [cppname], and the "cppname" is hierarchical, then + we must put `n` code inside of a namespace. */ +static void open_namespaces_for(std::ostream & out, environment const & env, name const & n) { + optional c = get_cppname_for(env, n); + if (!c || c->is_atomic()) return; + open_namespaces_core(out, c->get_prefix()); +} + +static void close_namespaces_for(std::ostream & out, environment const & env, name const & n) { + optional c = get_cppname_for(env, n); + if (!c || c->is_atomic()) return; + name p = c->get_prefix(); + while (!p.is_anonymous()) { + out << "}"; + p = p.get_prefix(); + } + out << "\n"; +} + +static std::string to_base_cpp_name(environment const & env, name const & n) { + if (optional c = get_cppname_for(env, n)) { + lean_assert(c->is_string()); + return c->get_string().to_std_string(); + } else { + return mangle(n); + } +} + +static expr get_result_type(expr type) { + while (is_pi(type)) { + type = binding_body(type); + } + return type; +} + +static void emit_fn_header(std::ostream & out, environment const & env, name const & n, bool arg_names) { + open_namespaces_for(out, env, n); + expr type = get_constant_ll_type(env, n); + out << to_cpp_type(get_result_type(type)) << " " << to_base_cpp_name(env, n); + if (is_pi(type)) { + out << "("; + bool first = true; + while (is_pi(type)) { + if (first) + first = false; + else + out << ", "; + out << to_cpp_type(binding_domain(type)); + if (arg_names) { + out << " "; + out << binding_name(type); + } + type = binding_body(type); + } + out << ")"; + } + out << ";\n"; + close_namespaces_for(out, env, n); +} + +/* Auxiliary function for `collect_dependencies`. */ +static void collect_constant(expr const & e, name_set & deps) { + lean_assert(is_constant(e)); + if (!is_llnf_op(e) && !is_builtin_constant(const_name(e)) && e != mk_enf_neutral()) { + deps.insert(const_name(e)); + } +} + +/* Collect declarations used by `e` in `deps`. */ +static void collect_dependencies(environment const & env, expr e, name_set & deps) { + while (true) { + switch (e.kind()) { + case expr_kind::Lambda: + e = binding_body(e); + break; + case expr_kind::Let: + collect_dependencies(env, let_value(e), deps); + e = let_body(e); + break; + case expr_kind::App: + if (is_cases_on_app(env, e)) { + buffer args; + get_app_args(e, args); + for (expr const & arg : args) + collect_dependencies(env, arg, deps); + } else { + collect_constant(get_app_fn(e), deps); + } + return; + case expr_kind::Const: + collect_constant(e, deps); + return; + default: + return; + } + } +} + +/* Emit function headers of all functions/constants declared in the current module, + and their direct dependencies. */ +static void emit_fn_headers(std::ostream & out, environment const & env) { + comp_decls ds = get_extension(env).m_code; + name_set todo; + for (comp_decl const & d : ds) { + if (!todo.contains(d.fst())) { + todo.insert(d.fst()); + collect_dependencies(env, d.snd(), todo); + } + } + todo.for_each([&](name const & n) { emit_fn_header(out, env, n, false); }); +} + +static void emit_file_header(std::ostream & out, module_name const & m, list const & deps) { out << "// Lean compiler output\n"; out << "// Module: " << m << "\n"; out << "// Imports:"; for (module_name const & d : deps) out << " " << d; out << "\n"; - comp_decls ds = get_extension(env).m_code; - for (comp_decl const & d : ds) { - out << "// " << d.fst(); - if (optional c = get_cppname_for(env, d.fst())) out << " ==> " << *c; - out << "\n"; - } + out << "#include \"runtime/object.h\"\n"; + out << "typedef lean::object obj;\n"; +} + +void print_cpp_code(std::ostream & out, environment const & env, module_name const & m, list const & deps) { + emit_file_header(out, m, deps); + emit_fn_headers(out, env); } void initialize_emit_cpp() { g_ext = new emit_cpp_ext_reg(); register_system_attribute(cppname_attr("cppname", "name to be used by C++ code generator", - [](environment const & env, io_state const &, name const &, unsigned, bool persistent) { + [](environment const & env, io_state const &, name const & n, unsigned, bool persistent) { if (!persistent) throw exception("invalid [cppname] attribute, must be persistent"); + if (n.is_anonymous()) throw exception("invalid [cppname] attribute, argument is missing"); + name it = n; + while (!it.is_anonymous()) { + if (!it.is_string()) throw exception("invalid [cppname] attribute, identifier cannot be numeric"); + it = it.get_prefix(); + } return env; })); } diff --git a/src/library/compiler/emit_cpp.h b/src/library/compiler/emit_cpp.h index 69fe4cbd94..d6ab8bd1bb 100644 --- a/src/library/compiler/emit_cpp.h +++ b/src/library/compiler/emit_cpp.h @@ -11,7 +11,7 @@ Author: Leonardo de Moura namespace lean { environment emit_cpp(environment const & env, comp_decls const & ds); -void print_cpp_code(std::ofstream & out, environment const & env, module_name const & m, list const & deps); +void print_cpp_code(std::ostream & out, environment const & env, module_name const & m, list const & deps); void initialize_emit_cpp(); void finalize_emit_cpp(); diff --git a/src/library/compiler/llnf.h b/src/library/compiler/llnf.h index 9f6f0765f3..c4f7708ad8 100644 --- a/src/library/compiler/llnf.h +++ b/src/library/compiler/llnf.h @@ -31,6 +31,7 @@ bool is_llnf_box(expr const & e, unsigned & n); bool is_llnf_inc(expr const & e); bool is_llnf_dec(expr const & e); +bool is_llnf_op(expr const & e); inline bool is_llnf_cnstr(expr const & e) { unsigned d1, d2, d3; return is_llnf_cnstr(e, d1, d2, d3); } inline bool is_llnf_reuse(expr const & e) { unsigned d1, d2, d3; return is_llnf_reuse(e, d1, d2, d3); } inline bool is_llnf_reset(expr const & e) { unsigned i; return is_llnf_reset(e, i); }