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

feat(library/compiler/emit_cpp): use new extern_attribute module

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-11 11:03:56 -08:00
parent 1856a319e5
commit befa53ec70
4 changed files with 77 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/init/data/uint.lean
View file

@ -21,14 +21,12 @@ def uint8.add (a b : uint8) : uint8 := ⟨a.val + b.val⟩
def uint8.sub (a b : uint8) : uint8 := ⟨a.val - b.val⟩
@[extern cpp inline "#1 * #2"]
def uint8.mul (a b : uint8) : uint8 := ⟨a.val * b.val⟩
@[extern cpp inline "#1 == 0 ? 0 : #1 / #2"]
@[extern cpp inline "#2 == 0 ? 0 : #1 / #2"]
def uint8.div (a b : uint8) : uint8 := ⟨a.val / b.val⟩
@[extern cpp inline "#1 == 0 ? 0 : #1 % #2"]
@[extern cpp inline "#2 == 0 ? 0 : #1 % #2"]
def uint8.mod (a b : uint8) : uint8 := ⟨a.val % b.val⟩
def uint8.modn (a : uint8) (n : nat) : uint8 := ⟨a.val %ₙ n⟩
@[extern cpp inline "#1 < #2"]
def uint8.lt (a b : uint8) : Prop := a.val < b.val
@[extern cpp inline "#1 <= #2"]
def uint8.le (a b : uint8) : Prop := a.val ≤ b.val
instance : has_zero uint8 := ⟨uint8.of_nat 0⟩
@ -43,14 +41,17 @@ instance : has_lt uint8 := ⟨uint8.lt⟩
instance : has_le uint8 := ⟨uint8.le⟩
instance : inhabited uint8 := ⟨0⟩
@[extern cpp inline "#1 == #2"]
def uint8.dec_eq (a b : uint8) : decidable (a = b) :=
uint8.cases_on a $ λ n, uint8.cases_on b $ λ m,
if h : n = m then is_true (h ▸ rfl) else is_false (λ h', uint8.no_confusion h' (λ h', absurd h' h))
@[extern cpp inline "#1 < #2"]
def uint8.dec_lt (a b : uint8) : decidable (a < b) :=
uint8.cases_on a $ λ n, uint8.cases_on b $ λ m,
infer_instance_as (decidable (n < m))
@[extern cpp inline "#1 <= #2"]
def uint8.dec_le (a b : uint8) : decidable (a ≤ b) :=
uint8.cases_on a $ λ n, uint8.cases_on b $ λ m,
infer_instance_as (decidable (n <= m))

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

@ -17,6 +17,7 @@ Author: Leonardo de Moura
#include "library/compiler/llnf_code.h"
#include "library/compiler/builtin.h"
#include "library/compiler/export_attribute.h"
#include "library/compiler/extern_attribute.h"
namespace lean {
static std::string to_cpp_type(expr const & e) {
@ -273,6 +274,7 @@ static char const * get_scalar_type_from_size(unsigned i) {
struct emit_fn_fn {
std::ostream & m_out;
name m_cpp{"cpp"};
name_generator m_ngen;
environment m_env;
local_ctx m_lctx;
@ -289,8 +291,12 @@ struct emit_fn_fn {
return m_lctx.get_local_decl(x).get_type() == mk_enf_object_type();
}
void emit_unit(std::ostream & out) {
out << "lean::box(0)";
}
void emit_unit() {
m_out << "lean::box(0)";
emit_unit(m_out);
}
void emit_constant(expr const & c) {
@ -304,11 +310,15 @@ struct emit_fn_fn {
m_out << to_cpp_name(m_env, const_name(c));
}
void emit_fvar(expr const & x) {
void emit_fvar(std::ostream & out, expr const & x) {
lean_assert(is_fvar(x));
name const & id = fvar_name(x);
lean_assert(id.is_numeral());
m_out << "x_" << id.get_numeral();
out << "x_" << id.get_numeral();
}
void emit_fvar(expr const & x) {
emit_fvar(m_out, x);
}
void emit_lbl(expr const & jp) {
@ -360,11 +370,15 @@ struct emit_fn_fn {
m_out << ";\n";
}
void emit_arg(expr const & arg) {
void emit_arg(std::ostream & out, expr const & arg) {
if (is_fvar(arg))
emit_fvar(arg);
emit_fvar(out, arg);
else
emit_unit();
emit_unit(out);
}
void emit_arg(expr const & arg) {
emit_arg(m_out, arg);
}
void emit_args(unsigned sz, expr const * args) {
@ -374,6 +388,12 @@ struct emit_fn_fn {
}
}
string_ref arg_to_string_ref(expr const & arg) {
std::ostringstream out;
emit_arg(out, arg);
return string_ref(out.str());
}
void emit_apply(expr const & x, buffer<expr> const & args) {
lean_assert(args.size() > 0);
expr const & f = args[0];
@ -543,21 +563,16 @@ struct emit_fn_fn {
m_out << ");\n";
}
void emit_native_constant(expr const &x, expr const &fn, buffer<expr> const &args) {
buffer<bool> used_args;
lean_verify(get_native_used_args(m_env, const_name(fn), used_args));
lean_assert(used_args.size() == args.size());
void emit_native_constant(expr const & x, expr const & fn, buffer<expr> const & args) {
emit_lhs(x);
emit_constant(fn);
m_out << "(";
bool first = true;
for (unsigned i = 0; i < args.size(); i++) {
if (used_args[i]) {
if (first) first = false; else m_out << ", ";
emit_arg(args[i]);
}
string_refs arg_strs;
unsigned i = args.size();
while (i > 0) {
--i;
arg_strs = string_refs(arg_to_string_ref(args[i]), arg_strs);
}
m_out << ");\n";
emit_extern_call(m_out, m_env, m_cpp, const_name(fn), arg_strs);
m_out << ";\n";
}
void emit_instr(local_decl const & d) {

36
src/library/compiler/extern_attribute.cpp
View file

@ -8,6 +8,9 @@ Authors: Leonardo de Moura
#include "util/object_ref.h"
#include "library/util.h"
#include "library/attribute_manager.h"
#include "library/compiler/builtin.h" // TODO(Leo): delete
void initialize_init_lean_extern();
namespace lean {
object* mk_adhoc_ext_entry_core(object*);
@ -16,6 +19,7 @@ object* mk_std_ext_entry_core(object*, object*);
object* mk_foreign_ext_entry_core(object*, object*);
object* mk_extern_call_core(object*, object*, object*);
object* mk_extern_attr_data_core(object*, object*);
object* mk_extern_call_core(object*, object*, object*);
typedef object_ref extern_entry;
typedef list_ref<extern_entry> extern_entries;
@ -113,7 +117,39 @@ extern_attr const & get_extern_attr() {
return static_cast<extern_attr const &>(get_system_attribute("extern"));
}
bool emit_extern_call_core(std::ostream & out, environment const & env, name const & backend, name const & fn, string_refs const & attrs) {
if (std::shared_ptr<extern_attr_data> const & data = get_extern_attr().get(env, fn)) {
extern_attr_data_value const & v = data->m_value;
inc(v.raw()); inc(backend.raw()); inc(attrs.raw());
object * r = mk_extern_call_core(v.raw(), backend.raw(), attrs.raw());
if (is_scalar(r)) return false;
object * s = cnstr_get(r, 0);
out << string_cstr(s);
dec(r);
return true;
} else {
return false;
}
}
void emit_extern_call(std::ostream & out, environment const & env, name const & backend, name const & fn, string_refs const & attrs) {
if (emit_extern_call_core(out, env, backend, fn, attrs))
return;
/* TODO(Leo): delete the following backward compatibility code */
name _fn = *get_native_constant_cname(env, fn);
out << _fn << "(";
bool first = true;
string_refs it = attrs;
while (!empty(it)) {
if (first) first = false; else out << ", ";
out << string_cstr(head(it).raw());
it = tail(it);
}
out << ")";
}
void initialize_extern_attribute() {
initialize_init_lean_extern(); // Lean module initialization
register_system_attribute(extern_attr("extern", "builtin and foreign functions",
[](environment const & env, io_state const &, name const &, unsigned, bool persistent) {
if (!persistent) throw exception("invalid [extern] attribute, it must be persistent");

3
src/library/compiler/extern_attribute.h
View file

@ -7,7 +7,8 @@ Authors: Leonardo de Moura
#pragma once
#include "kernel/environment.h"
namespace lean {
string_ref mk_extern_call(environment const & env, string_ref const & backend, string_refs const & attrs);
bool emit_extern_call_core(std::ostream & out, environment const & env, name const & backend, name const & fn, string_refs const & attrs);
void emit_extern_call(std::ostream & out, environment const & env, name const & backend, name const & fn, string_refs const & attrs);
void initialize_extern_attribute();
void finalize_extern_attribute();
}