Skip to content

Move builtins into environment #8

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
TehMillhouse wants to merge 2 commits into from
Closed

Move builtins into environment #8

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
505600f
chore(library/compiler): move builtins into the environment
TehMillhouse Feb 8, 2019
aa1f7e9
fix(library/vm): unary op dummies copy-paste error
TehMillhouse Feb 8, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
167 changes: 112 additions & 55 deletions src/library/compiler/builtin.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,116 +2,170 @@
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: Leonardo de Moura
Authors: Leonardo de Moura, Max Wagner
*/
#include <unordered_map>
#include <string>
#include "util/list.h"
#include "kernel/expr.h"
#include "library/compiler/util.h"

namespace lean {
struct builtin_decl {
expr m_type;
unsigned m_arity;
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,
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) {

struct native_decl {
expr m_ll_type;
unsigned m_arity;
std::string m_cname;
bool m_borrowed_res;
list<bool> m_borrowed_args;
list<bool> m_used_args;

native_decl() {}
native_decl(expr const & ll_type, unsigned arity, std::string cname, bool bres, list<bool> const & bargs,
list<bool> const & used_args) :
m_ll_type(ll_type), m_arity(arity), m_cname(cname), m_borrowed_res(bres), m_borrowed_args(bargs), m_used_args(used_args) {
}
};

typedef std::unordered_map<name, builtin_decl, name_hash_fn> builtin_map;
typedef name_map<native_decl> native_decl_map;
static native_decl_map * g_initial_native_decls;

bool is_builtin_constant(name const & c) {
return g_initial_native_decls->contains(c);
}

static builtin_map * g_builtin_decls = nullptr;
struct native_decls_ext : public environment_extension {
native_decl_map m_decls;

native_decls_ext() {
g_initial_native_decls->for_each([&](name const & n, native_decl const & d) {
m_decls.insert(n, d);
});
}
};

struct native_decls_reg {
unsigned m_ext_id;
native_decls_reg() {
std::shared_ptr<native_decls_ext> decl_reg = std::make_shared<native_decls_ext>();
m_ext_id = environment::register_extension(decl_reg);
}
};

static native_decls_reg * g_ext = nullptr;

static environment update(environment const & env, native_decls_ext const & ext) {
return env.update(g_ext->m_ext_id, std::make_shared<native_decls_ext>(ext));
}

void register_builtin(name const & n, expr const & type, unsigned arity, char const * cname,

void register_builtin(name const & n, expr const & ll_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, used_args)));
lean_assert(g_initial_native_decls->find(n) == nullptr);
g_initial_native_decls->insert(n, native_decl(ll_type, arity, cname, borrowed_res, borrowed_arg, used_args));
}

void register_builtin(name const & n, expr const & type, char const * cname,
void register_builtin(name const & n, expr const & ll_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, used_args);
unsigned arity = get_arity(ll_type);
return register_builtin(n, ll_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 & ll_type, char const * cname, list<bool> const & borrowed_arg, list<bool> const & used_args) {
return register_builtin(n, ll_type, cname, false, borrowed_arg, used_args);
}

void register_builtin(name const & n, expr const & type, char const * cname, list<bool> const & borrowed_arg) {
unsigned arity = get_arity(type);
void register_builtin(name const & n, expr const & ll_type, char const * cname, list<bool> const & borrowed_arg) {
unsigned arity = get_arity(ll_type);
buffer<bool> used_args;
used_args.resize(arity, true);
return register_builtin(n, type, cname, false, borrowed_arg, to_list(used_args));
return register_builtin(n, ll_type, cname, false, borrowed_arg, to_list(used_args));
}

void register_builtin(name const & n, expr const & type, unsigned arity, char const * cname) {
void register_builtin(name const & n, expr const & ll_type, unsigned arity, char const * cname) {
buffer<bool> borrowed;
borrowed.resize(arity, false);
buffer<bool> used_args;
used_args.resize(arity, true);
return register_builtin(n, type, arity, cname, false, to_list(borrowed), to_list(used_args));
return register_builtin(n, ll_type, arity, cname, false, to_list(borrowed), to_list(used_args));
}

void register_builtin(name const & n, expr const & type, char const * cname) {
unsigned arity = get_arity(type);
return register_builtin(n, type, arity, cname);
void register_builtin(name const & n, expr const & ll_type, char const * cname) {
unsigned arity = get_arity(ll_type);
return register_builtin(n, ll_type, arity, cname);
}

bool is_builtin_constant(name const & c) {
return g_builtin_decls->find(c) != g_builtin_decls->end();
static inline native_decls_ext const & get_ext(environment const & env) {
return static_cast<native_decls_ext const & >(env.get_extension(g_ext->m_ext_id));
}

environment add_native_constant_decl(environment const & env, name const & n, expr const & ll_type, std::string cname,
bool bres, list<bool> const & bargs, list<bool> const & used_args) {
native_decl d(ll_type, get_arity(ll_type), cname, bres, bargs, used_args);
native_decls_ext ext = get_ext(env);
ext.m_decls.insert(n, d);
return update(env, ext);
}

void for_each_native_constant(environment const & env, std::function<void(name const & n)> const & f) {
auto ext = get_ext(env);
ext.m_decls.for_each([&](name const & n, native_decl const & _) { f(n); });
}

optional<name> get_builtin_cname(name const & c) {
auto it = g_builtin_decls->find(c);
if (it == g_builtin_decls->end())

static inline native_decl const * get_native_constant_core(environment const & env, name const & n) {
auto ext = get_ext(env);
return ext.m_decls.find(n);
}

optional<name> get_native_constant_cname(environment const & env, name const & c) {
auto d = get_native_constant_core(env, c);
if (d == nullptr)
return optional<name>();
return optional<name>(it->second.m_cname);
return optional<name>(d->m_cname);
}

optional<expr> get_builtin_constant_ll_type(name const & c) {
auto it = g_builtin_decls->find(c);
if (it == g_builtin_decls->end())
bool is_native_constant(environment const & env, name const & c) {
return get_native_constant_core(env, c) != nullptr;
}

optional<expr> get_native_constant_ll_type(environment const & env, name const & c) {
auto d = get_native_constant_core(env, c);
if (d == nullptr)
return none_expr();
return some_expr(it->second.m_type);
return some_expr(d->m_ll_type);
}

optional<unsigned> get_builtin_constant_arity(name const & c) {
auto it = g_builtin_decls->find(c);
if (it == g_builtin_decls->end())
optional<unsigned> get_native_constant_arity(environment const & env, name const & c) {
auto d = get_native_constant_core(env, c);
if (d == nullptr)
return optional<unsigned>();
return optional<unsigned>(it->second.m_arity);
return optional<unsigned>(d->m_arity);
}

bool get_builtin_borrowed_info(name const & c, buffer<bool> & borrowed_args, bool & borrowed_res) {
auto it = g_builtin_decls->find(c);
if (it == g_builtin_decls->end())
bool get_native_borrowed_info(environment const & env, name const & c, buffer<bool> &borrowed_args, bool &borrowed_res) {
auto d = get_native_constant_core(env, c);
if (d == nullptr)
return false;

to_buffer(it->second.m_borrowed_args, borrowed_args);
borrowed_res = it->second.m_borrowed_res;
to_buffer(d->m_borrowed_args, borrowed_args);
borrowed_res = d->m_borrowed_res;
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())
bool get_native_used_args(environment const & env, name const & c, buffer<bool> &used_args) {
auto d = get_native_constant_core(env, c);
if (d == nullptr)
return false;

to_buffer(it->second.m_used_args, used_args);
to_buffer(d->m_used_args, used_args);
return true;
}

void initialize_builtin() {
g_builtin_decls = new builtin_map();
g_initial_native_decls = new native_decl_map();

expr o = mk_enf_object_type();
expr u8 = mk_constant(get_uint8_name());
Expand Down Expand Up @@ -327,9 +381,12 @@ void initialize_builtin() {
register_builtin(name({"lean", "name", "mk_string"}), o_o_o, "lean::name_mk_string");
register_builtin(name({"lean", "name", "mk_numeral"}), o_o_o, "lean::name_mk_numeral");
register_builtin(name({"lean", "name", "dec_eq"}), o_o_u8, "lean::name_dec_eq", bb);

g_ext = new native_decls_reg();
}

void finalize_builtin() {
delete g_builtin_decls;
delete g_ext;
delete g_initial_native_decls;
}
}
24 changes: 15 additions & 9 deletions src/library/compiler/builtin.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,21 +2,27 @@
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: Leonardo de Moura
Authors: Leonardo de Moura, Max Wagner
*/
#pragma once
#include <string>
#include "kernel/expr.h"
namespace lean {
bool is_native_constant(environment const & env, name const & c);
bool is_builtin_constant(name const & c);
optional<name> get_builtin_cname(name const & c);
optional<expr> get_builtin_constant_ll_type(name const & c);
optional<unsigned> get_builtin_constant_arity(name const & c);
/* Return true if `c` is a builtin, and store in borrowed_args and
optional<name> get_native_constant_cname(environment const & env, name const & c);
optional <expr> get_native_constant_ll_type(environment const & env, name const & c);
optional<unsigned> get_native_constant_arity(environment const & env, name const & c);
/* Return true if `c` is a native constant, 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);
bool get_native_borrowed_info(environment const & env, name const & c, buffer<bool> & borrowed_args, bool & borrowed_res);
/* Return true if `c` is a native constant, and store in used_args a bit mask specifying
which arguments the builtin implementation takes as argument. */
bool get_native_used_args(environment const & env, name const & c, buffer<bool> & used_args);

environment add_native_constant_decl(environment const & env, name const & n, expr const & ll_type, std::string cname,
bool bres, list<bool> const & bargs, list<bool> const & used_args);
void for_each_native_constant(environment const & env, std::function<void(name const & n)> const & f);
void initialize_builtin();
void finalize_builtin();
}
8 changes: 4 additions & 4 deletions src/library/compiler/compiler.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -133,9 +133,9 @@ environment compile(environment const & env, options const & opts, names const &
}
}

if (length(cs) == 1 && is_builtin_constant(head(cs))) {
/* Generate boxed version for builtin constant if needed */
unsigned arity = *get_builtin_constant_arity(head(cs));
if (length(cs) == 1 && is_native_constant(env, head(cs))) {
/* Generate boxed version for native constant if needed */
unsigned arity = *get_native_constant_arity(env, head(cs));
if (optional<pair<environment, comp_decl>> p = mk_boxed_version(env, head(cs), arity)) {
/* Remark: we don't need boxed version for the bytecode */
return emit_cpp(p->first, comp_decls(p->second));
Expand All @@ -145,7 +145,7 @@ environment compile(environment const & env, options const & opts, names const &
}

for (name const & c : cs) {
lean_assert(!is_builtin_constant(c));
lean_assert(!is_native_constant(env, c));
if (!env.get(c).is_definition() || has_synthetic_sorry(env.get(c).get_value())) {
return env;
}
Expand Down
27 changes: 16 additions & 11 deletions src/library/compiler/emit_cpp.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -159,9 +159,9 @@ static void emit_fn_decl(std::ostream & out, environment const & env, name const
}

/* Auxiliary function for `collect_dependencies`. */
static void collect_constant(expr const & e, name_set & deps) {
static void collect_constant(environment const &env, expr const & e, name_set & deps) {
lean_assert(is_constant(e));
if (!is_llnf_op(e) && !is_builtin_constant(const_name(e)) && !is_enf_neutral(e) && !is_enf_unreachable(e)) {
if (!is_llnf_op(e) && !is_native_constant(env, const_name(e)) && !is_enf_neutral(e) && !is_enf_unreachable(e)) {
deps.insert(const_name(e));
}
}
Expand All @@ -186,13 +186,13 @@ static void collect_dependencies(environment const & env, expr e, name_set & dep
} else if (is_llnf_closure(get_app_fn(e))) {
buffer<expr> args;
get_app_args(e, args);
collect_constant(args[0], deps);
collect_constant(env, args[0], deps);
} else {
collect_constant(get_app_fn(e), deps);
collect_constant(env, get_app_fn(e), deps);
}
return;
case expr_kind::Const:
collect_constant(e, deps);
collect_constant(env, e, deps);
return;
default:
return;
Expand All @@ -211,9 +211,14 @@ static void emit_fn_decls(std::ostream & out, environment const & env) {
all_decls.insert(d.fst());
collect_dependencies(env, d.snd(), all_decls);
}
for_each_native_constant(env, [&](const name &n) {
if (!is_builtin_constant(n))
mod_decls.insert(n);
all_decls.insert(n);
});
all_decls.for_each([&](name const & n) {
emit_fn_decl(out, env, n, mod_decls.contains(n));
});
});
}

static optional<comp_decl> has_main_fn(environment const & env) {
Expand Down Expand Up @@ -314,7 +319,7 @@ struct emit_fn_fn {
void emit_constant(expr const & c) {
lean_assert(is_constant(c));
lean_assert(!is_enf_unreachable(c));
if (optional<name> n = get_builtin_cname(const_name(c)))
if (optional<name> n = get_native_constant_cname(m_env, const_name(c)))
m_out << *n;
else if (is_enf_neutral(c))
emit_unit();
Expand Down Expand Up @@ -561,9 +566,9 @@ struct emit_fn_fn {
m_out << ");\n";
}

void emit_builtin(expr const & x, expr const & fn, buffer<expr> const & args) {
void emit_native_constant(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_verify(get_native_used_args(m_env, const_name(fn), used_args));
lean_assert(used_args.size() == args.size());
emit_lhs(x);
emit_constant(fn);
Expand Down Expand Up @@ -621,8 +626,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 if (is_native_constant(m_env, const_name(fn))) {
emit_native_constant(x, fn, args);
} else {
/* Regular function application. */
emit_lhs(x);
Expand Down
2 changes: 1 addition & 1 deletion src/library/compiler/ll_infer_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -147,7 +147,7 @@ class ll_infer_type_fn {
}

expr infer_constant(expr const & e) {
if (optional<expr> type = get_builtin_constant_ll_type(const_name(e))) {
if (optional<expr> type = get_native_constant_ll_type(env(), const_name(e))) {
return *type;
} else if (is_constructor(env(), const_name(e))) {
return infer_constructor_type(e);
Expand Down
Loading