max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/compiler/emit_cpp): emit function headers

Browse source
This commit is contained in:
Leonardo de Moura 2019-01-25 13:27:21 -08:00
parent 2016e1bce5
commit b36b4f0d80
3 changed files with 159 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

166
src/library/compiler/emit_cpp.cpp
View file

@ -4,11 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <fstream>
#include <iostream>
#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<module_name> 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<name> 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<name> 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<name> 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<expr> 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<module_name> 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<name> 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<module_name> 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;
}));
}

2
src/library/compiler/emit_cpp.h
View file

@ -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<module_name> const & deps);
void print_cpp_code(std::ostream & out, environment const & env, module_name const & m, list<module_name> const & deps);
void initialize_emit_cpp();
void finalize_emit_cpp();

1
src/library/compiler/llnf.h
View file

@ -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); }