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

feat(library/compiler): register extern constants into the new IR

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-17 17:12:51 -07:00
parent 66d4995c56
commit c9bcd4990c
11 changed files with 514 additions and 81 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/lean/compiler/ir/basic.lean
View file

@ -340,7 +340,7 @@ bs.hmmap $ λ b, match b with
inductive Decl
| fdecl (f : FunId) (xs : Array Param) (ty : IRType) (b : FnBody)
| extern (f : FunId) (xs : Array Param) (ty : IRType) (ext : ExternEntry)
| extern (f : FunId) (xs : Array Param) (ty : IRType) (ext : ExternAttrData)
namespace Decl
@ -363,6 +363,9 @@ end Decl
@[export lean.ir.mk_decl_core] def mkDecl (f : FunId) (xs : Array Param) (ty : IRType) (b : FnBody) : Decl := Decl.fdecl f xs ty b
@[export lean.ir.mk_extern_decl_core] def mkExternDecl (f : FunId) (xs : Array Param) (ty : IRType) (e : ExternAttrData) : Decl :=
Decl.extern f xs ty e
/-- `Expr.isPure e` return `true` Iff `e` is in the `λPure` fragment. -/
def Expr.isPure : Expr → Bool
| (Expr.ctor _ _) := true

4
library/init/lean/compiler/ir/compilerm.lean
View file

@ -103,6 +103,10 @@ def getDecl (n : Name) : CompilerM Decl :=
do (some decl) ← findDecl n | throw ("unknown declaration '" ++ toString n ++ "'"),
pure decl
@[export lean.ir.add_decl_core]
def addDeclAux (env : Environment) (decl : Decl) : Environment :=
declMapExt.addEntry env decl
def addDecl (decl : Decl) : CompilerM Unit :=
modifyEnv (λ env, declMapExt.addEntry env decl)

4
src/library/compiler/compiler.cpp
View file

@ -28,6 +28,7 @@ Author: Leonardo de Moura
#include "library/compiler/export_attribute.h"
#include "library/compiler/extern_attribute.h"
#include "library/compiler/struct_cases_on.h"
#include "library/compiler/ir.h"
namespace lean {
static name * g_codegen = nullptr;
@ -173,8 +174,9 @@ environment compile(environment const & env, options const & opts, names cs) {
if (length(cs) == 1 && is_extern_constant(env, head(cs))) {
/* Generate boxed version for extern/native constant if needed. */
environment new_env = ir::add_extern(env, head(cs));
unsigned arity = *get_extern_constant_arity(env, head(cs));
if (optional<pair<environment, comp_decl>> p = mk_boxed_version(env, head(cs), arity)) {
if (optional<pair<environment, comp_decl>> p = mk_boxed_version(new_env, head(cs), arity)) {
/* Remark: we don't need boxed version for the bytecode. */
return save_llnf_code(p->first, comp_decls(p->second));
} else {

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

@ -27,7 +27,6 @@ object* get_extern_entry_for_core(object*, object*);
typedef object_ref extern_entry;
typedef list_ref<extern_entry> extern_entries;
typedef object_ref extern_attr_data_value;
extern_entry mk_adhoc_ext_entry(name const & backend) {
inc(backend.raw());
@ -133,6 +132,15 @@ extern_attr const & get_extern_attr() {
return static_cast<extern_attr const &>(get_system_attribute("extern"));
}
optional<extern_attr_data_value> get_extern_attr_data(environment const & env, name const & fn) {
if (std::shared_ptr<extern_attr_data> const & data = get_extern_attr().get(env, fn)) {
extern_attr_data_value const & v = data->m_value;
return optional<extern_attr_data_value>(v);
} else {
return optional<extern_attr_data_value>();
}
}
optional<std::string> get_extern_name_for(environment const & env, name const & backend, name const & fn) {
if (std::shared_ptr<extern_attr_data> const & data = get_extern_attr().get(env, fn)) {
extern_attr_data_value const & v = data->m_value;

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

@ -11,6 +11,8 @@ namespace lean {
bool is_extern_constant(environment const & env, name const & c);
optional<expr> get_extern_constant_ll_type(environment const & env, name const & c);
optional<unsigned> get_extern_constant_arity(environment const & env, name const & c);
typedef object_ref extern_attr_data_value;
optional<extern_attr_data_value> get_extern_attr_data(environment const & env, name const & c);
/* Return true if `c` is an extern constant, and store in borrowed_args and
borrowed_res which arguments/results are marked as borrowed. */
bool get_extern_borrowed_info(environment const & env, name const & c, buffer<bool> & borrowed_args, bool & borrowed_res);

80
src/library/compiler/ir.cpp
View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "library/trace.h"
#include "library/compiler/util.h"
#include "library/compiler/llnf.h"
#include "library/compiler/extern_attribute.h"
namespace lean {
namespace ir {
@ -38,9 +39,11 @@ object * mk_jmp_core(object * j, object * ys);
extern object * mk_unreachable_core;
object * mk_alt_core(object * n, object * cidx, object * size, object * usize, object * ssize, object * b);
object * mk_decl_core(object * f, object * xs, uint8 ty, object * b);
object * mk_extern_decl_core(object * f, object * xs, uint8 ty, object * ext_entry);
object * decl_to_string_core(object * d);
object * compile_core(object * env, object * opts, object * decls);
object * log_to_string_core(object * log);
object * add_decl_core(object * env, object * decl);
/*
inductive IRType
| float | uint8 | uint16 | uint32 | uint64 | usize
@ -61,62 +64,57 @@ typedef object_ref decl;
arg mk_var_arg(var_id const & id) { inc(id.raw()); return arg(mk_var_arg_core(id.raw())); }
arg mk_irrelevant_arg() { return arg(mk_irrelevant_arg_core); }
param mk_param(var_id const & x, type ty) {
inc(x.raw());
uint8 borrowed = false;
return param(mk_param_core(x.raw(), borrowed, static_cast<uint8>(ty)));
return param(mk_param_core(x.to_obj_arg(), borrowed, static_cast<uint8>(ty)));
}
expr mk_ctor(name const & n, unsigned cidx, unsigned size, unsigned usize, unsigned ssize, buffer<arg> const & ys) {
inc(n.raw());
return expr(mk_ctor_expr_core(n.raw(), mk_nat_obj(cidx), mk_nat_obj(size), mk_nat_obj(usize), mk_nat_obj(ssize), to_array(ys)));
return expr(mk_ctor_expr_core(n.to_obj_arg(), mk_nat_obj(cidx), mk_nat_obj(size), mk_nat_obj(usize), mk_nat_obj(ssize), to_array(ys)));
}
expr mk_proj(unsigned i, var_id const & x) { inc(x.raw()); return expr(mk_proj_expr_core(mk_nat_obj(i), x.raw())); }
expr mk_uproj(unsigned i, var_id const & x) { inc(x.raw()); return expr(mk_uproj_expr_core(mk_nat_obj(i), x.raw())); }
expr mk_sproj(unsigned i, unsigned o, var_id const & x) { inc(x.raw()); return expr(mk_sproj_expr_core(mk_nat_obj(i), mk_nat_obj(o), x.raw())); }
expr mk_fapp(fun_id const & c, buffer<arg> const & ys) { inc(c.raw()); return expr(mk_fapp_expr_core(c.raw(), to_array(ys))); }
expr mk_papp(fun_id const & c, buffer<arg> const & ys) { inc(c.raw()); return expr(mk_papp_expr_core(c.raw(), to_array(ys))); }
expr mk_app(var_id const & x, buffer<arg> const & ys) { inc(x.raw()); return expr(mk_app_expr_core(x.raw(), to_array(ys))); }
expr mk_num_lit(nat const & v) { inc(v.raw()); return expr(mk_num_expr_core(v.raw())); }
expr mk_str_lit(string_ref const & v) { inc(v.raw()); return expr(mk_str_expr_core(v.raw())); }
expr mk_proj(unsigned i, var_id const & x) { return expr(mk_proj_expr_core(mk_nat_obj(i), x.to_obj_arg())); }
expr mk_uproj(unsigned i, var_id const & x) { return expr(mk_uproj_expr_core(mk_nat_obj(i), x.to_obj_arg())); }
expr mk_sproj(unsigned i, unsigned o, var_id const & x) { return expr(mk_sproj_expr_core(mk_nat_obj(i), mk_nat_obj(o), x.to_obj_arg())); }
expr mk_fapp(fun_id const & c, buffer<arg> const & ys) { return expr(mk_fapp_expr_core(c.to_obj_arg(), to_array(ys))); }
expr mk_papp(fun_id const & c, buffer<arg> const & ys) { return expr(mk_papp_expr_core(c.to_obj_arg(), to_array(ys))); }
expr mk_app(var_id const & x, buffer<arg> const & ys) { return expr(mk_app_expr_core(x.to_obj_arg(), to_array(ys))); }
expr mk_num_lit(nat const & v) { return expr(mk_num_expr_core(v.to_obj_arg())); }
expr mk_str_lit(string_ref const & v) { return expr(mk_str_expr_core(v.to_obj_arg())); }
fn_body mk_vdecl(var_id const & x, type ty, expr const & e, fn_body const & b) {
inc(x.raw()); inc(e.raw()), inc(b.raw());
return fn_body(mk_vdecl_core(x.raw(), static_cast<uint8>(ty), e.raw(), b.raw()));
return fn_body(mk_vdecl_core(x.to_obj_arg(), static_cast<uint8>(ty), e.to_obj_arg(), b.to_obj_arg()));
}
fn_body mk_jdecl(jp_id const & j, buffer<param> const & xs, expr const & v, fn_body const & b) {
inc(j.raw()); inc(v.raw()); inc(b.raw());
return fn_body(mk_jdecl_core(j.raw(), to_array(xs), v.raw(), b.raw()));
return fn_body(mk_jdecl_core(j.to_obj_arg(), to_array(xs), v.to_obj_arg(), b.to_obj_arg()));
}
fn_body mk_uset(var_id const & x, unsigned i, var_id const & y, fn_body const & b) {
inc(x.raw()); inc(y.raw()); inc(b.raw());
return fn_body(mk_uset_core(x.raw(), mk_nat_obj(i), y.raw(), b.raw()));
return fn_body(mk_uset_core(x.to_obj_arg(), mk_nat_obj(i), y.to_obj_arg(), b.to_obj_arg()));
}
fn_body mk_sset(var_id const & x, unsigned i, unsigned o, var_id const & y, type ty, fn_body const & b) {
inc(x.raw()); inc(y.raw()); inc(b.raw());
return fn_body(mk_sset_core(x.raw(), mk_nat_obj(i), mk_nat_obj(o), y.raw(), static_cast<uint8>(ty), b.raw()));
return fn_body(mk_sset_core(x.to_obj_arg(), mk_nat_obj(i), mk_nat_obj(o), y.to_obj_arg(), static_cast<uint8>(ty), b.to_obj_arg()));
}
fn_body mk_ret(arg const & x) { inc(x.raw()); return fn_body(mk_ret_core(x.raw())); }
fn_body mk_ret(arg const & x) { return fn_body(mk_ret_core(x.to_obj_arg())); }
fn_body mk_unreachable() { return fn_body(mk_unreachable_core); }
alt mk_alt(name const & n, unsigned cidx, unsigned size, unsigned usize, unsigned ssize, fn_body const & b) {
inc(n.raw()); inc(b.raw());
return alt(mk_alt_core(n.raw(), mk_nat_obj(cidx), mk_nat_obj(size), mk_nat_obj(usize), mk_nat_obj(ssize), b.raw()));
return alt(mk_alt_core(n.to_obj_arg(), mk_nat_obj(cidx), mk_nat_obj(size), mk_nat_obj(usize), mk_nat_obj(ssize), b.to_obj_arg()));
}
fn_body mk_case(name const & tid, var_id const & x, buffer<alt> const & alts) {
inc(tid.raw()); inc(x.raw());
return fn_body(mk_case_core(tid.raw(), x.raw(), to_array(alts)));
return fn_body(mk_case_core(tid.to_obj_arg(), x.to_obj_arg(), to_array(alts)));
}
fn_body mk_jmp(jp_id const & j, buffer<arg> const & ys) {
inc(j.raw());
return fn_body(mk_jmp_core(j.raw(), to_array(ys)));
return fn_body(mk_jmp_core(j.to_obj_arg(), to_array(ys)));
}
decl mk_decl(fun_id const & f, buffer<param> const & xs, type ty, fn_body const & b) {
inc(f.raw()); inc(b.raw());
return decl(mk_decl_core(f.raw(), to_array(xs), static_cast<uint8>(ty), b.raw()));
return decl(mk_decl_core(f.to_obj_arg(), to_array(xs), static_cast<uint8>(ty), b.to_obj_arg()));
}
decl mk_extern_decl(fun_id const & f, buffer<param> const & xs, type ty, extern_attr_data_value const & v) {
return decl(mk_extern_decl_core(f.to_obj_arg(), to_array(xs), static_cast<uint8>(ty), v.to_obj_arg()));
}
std::string decl_to_string(decl const & d) {
inc(d.raw());
string_ref r(decl_to_string_core(d.raw()));
string_ref r(decl_to_string_core(d.to_obj_arg()));
return r.to_std_string();
}
environment add_decl(environment const & env, decl const & d) {
return environment(add_decl_core(env.to_obj_arg(), d.to_obj_arg()));
}
}
class to_ir_fn {
@ -468,6 +466,22 @@ public:
to_ir_fn(environment const & env):m_st(env) {}
ir::decl operator()(comp_decl const & d) { return to_ir_decl(d); }
/* Convert extern constant into a IR.Decl */
ir::decl operator()(name const & fn) {
lean_assert(is_extern_constant(env(), fn));
buffer<ir::param> xs;
unsigned arity = *get_extern_constant_arity(env(), fn);
expr type = get_constant_ll_type(env(), fn);
for (unsigned i = 0; i < arity; i++) {
lean_assert(is_pi(type));
xs.push_back(ir::mk_param(ir::var_id(i), to_ir_type(binding_domain(type))));
type = binding_body(type);
}
ir::type result_type = to_ir_type(type);
extern_attr_data_value attr = *get_extern_attr_data(env(), fn);
return ir::mk_extern_decl(fn, xs, result_type, attr);
}
};
namespace ir {
@ -503,5 +517,9 @@ environment compile(environment const & env, options const & opts, comp_decls co
return new_env;
}
}
environment add_extern(environment const & env, name const & fn) {
return ir::add_decl(env, to_ir_fn(env)(fn));
}
}
}

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

@ -14,5 +14,6 @@ typedef object_ref decl;
std::string decl_to_string(decl const & d);
void test(decl const & d);
environment compile(environment const & env, options const & opts, comp_decls const & decls);
environment add_extern(environment const & env, name const & fn);
}
}

66
src/stage0/init/lean/compiler/ir/basic.cpp generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: init.lean.compiler.ir.basic
// Imports: init.lean.name init.lean.kvmap init.lean.format init.data.array.default
// Imports: init.data.array.default init.lean.name init.lean.extern init.lean.kvmap init.lean.format
#include "runtime/object.h"
#include "runtime/apply.h"
typedef lean::object obj; typedef lean::usize usize;
@ -143,6 +143,7 @@ obj* l_Lean_IR_reshape(obj*, obj*);
obj* l_Lean_IR_JoinPointId_Lean_HasFormat(obj*);
obj* l_Array_hmmapAux___main___at_Lean_IR_mmodifyJPs___spec__1___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*);
uint8 l_Array_isEqv___at_Lean_IR_args_alphaEqv___spec__1(obj*, obj*, obj*);
obj* l_Lean_IR_mkExternDecl___boxed(obj*, obj*, obj*, obj*);
namespace lean {
namespace ir {
obj* mk_case_core(obj*, obj*, obj*);
@ -180,6 +181,10 @@ obj* nat_add(obj*, obj*);
}
obj* l_Array_isEqv___at_Lean_IR_args_alphaEqv___spec__1___boxed(obj*, obj*, obj*);
uint8 l_Lean_IR_CtorInfo_isScalar(obj*);
namespace lean {
namespace ir {
obj* mk_extern_decl_core(obj*, obj*, uint8, obj*);
}}
obj* l_Array_isEqv___at_Lean_IR_FnBody_alphaEqv___main___spec__1___lambda__1___boxed(obj*, obj*, obj*);
namespace lean {
uint8 nat_dec_eq(obj*, obj*);
@ -2567,17 +2572,19 @@ return x_7;
obj* _init_l_Lean_IR_Decl_Inhabited() {
_start:
{
obj* x_0; obj* x_1; obj* x_2; uint8 x_3; obj* x_4; obj* x_5;
obj* x_0; obj* x_1; obj* x_2; uint8 x_3; obj* x_4; obj* x_5; obj* x_6;
x_0 = lean::mk_nat_obj(0ul);
x_1 = lean::mk_empty_array(x_0);
x_2 = lean::box(0);
x_3 = 6;
x_4 = lean::alloc_cnstr(1, 2, 1);
lean::cnstr_set(x_4, 0, x_2);
lean::cnstr_set(x_4, 1, x_1);
lean::cnstr_set_scalar(x_4, sizeof(void*)*2, x_3);
x_5 = x_4;
return x_5;
x_4 = lean::box(12);
x_5 = lean::alloc_cnstr(0, 3, 1);
lean::cnstr_set(x_5, 0, x_2);
lean::cnstr_set(x_5, 1, x_1);
lean::cnstr_set(x_5, 2, x_4);
lean::cnstr_set_scalar(x_5, sizeof(void*)*3, x_3);
x_6 = x_5;
return x_6;
}
}
obj* l_Lean_IR_Decl_name___main(obj* x_0) {
@ -2653,19 +2660,10 @@ return x_1;
uint8 l_Lean_IR_Decl_resultType___main(obj* x_0) {
_start:
{
if (lean::obj_tag(x_0) == 0)
{
uint8 x_1;
x_1 = lean::cnstr_get_scalar<uint8>(x_0, sizeof(void*)*3);
return x_1;
}
else
{
uint8 x_2;
x_2 = lean::cnstr_get_scalar<uint8>(x_0, sizeof(void*)*2);
return x_2;
}
}
}
obj* l_Lean_IR_Decl_resultType___main___boxed(obj* x_0) {
_start:
@ -2720,6 +2718,31 @@ x_5 = lean::ir::mk_decl_core(x_0, x_1, x_4, x_3);
return x_5;
}
}
namespace lean {
namespace ir {
obj* mk_extern_decl_core(obj* x_0, obj* x_1, uint8 x_2, obj* x_3) {
_start:
{
obj* x_4; obj* x_5;
x_4 = lean::alloc_cnstr(1, 3, 1);
lean::cnstr_set(x_4, 0, x_0);
lean::cnstr_set(x_4, 1, x_1);
lean::cnstr_set(x_4, 2, x_3);
lean::cnstr_set_scalar(x_4, sizeof(void*)*3, x_2);
x_5 = x_4;
return x_5;
}
}
}}
obj* l_Lean_IR_mkExternDecl___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
_start:
{
uint8 x_4; obj* x_5;
x_4 = lean::unbox(x_2);
x_5 = lean::ir::mk_extern_decl_core(x_0, x_1, x_4, x_3);
return x_5;
}
}
uint8 l_Lean_IR_Expr_isPure___main(obj* x_0) {
_start:
{
@ -8064,22 +8087,25 @@ x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_IR_FnBody_beq___boxed),
return x_0;
}
}
obj* initialize_init_data_array_default(obj*);
obj* initialize_init_lean_name(obj*);
obj* initialize_init_lean_extern(obj*);
obj* initialize_init_lean_kvmap(obj*);
obj* initialize_init_lean_format(obj*);
obj* initialize_init_data_array_default(obj*);
static bool _G_initialized = false;
obj* initialize_init_lean_compiler_ir_basic(obj* w) {
if (_G_initialized) return w;
_G_initialized = true;
if (io_result_is_error(w)) return w;
w = initialize_init_data_array_default(w);
if (io_result_is_error(w)) return w;
w = initialize_init_lean_name(w);
if (io_result_is_error(w)) return w;
w = initialize_init_lean_extern(w);
if (io_result_is_error(w)) return w;
w = initialize_init_lean_kvmap(w);
if (io_result_is_error(w)) return w;
w = initialize_init_lean_format(w);
if (io_result_is_error(w)) return w;
w = initialize_init_data_array_default(w);
if (io_result_is_error(w)) return w;
l_Lean_IR_VarId_HasToString___closed__1 = _init_l_Lean_IR_VarId_HasToString___closed__1();
lean::mark_persistent(l_Lean_IR_VarId_HasToString___closed__1);

405
src/stage0/init/lean/compiler/ir/compilerm.cpp generated
View file

@ -24,10 +24,12 @@ obj* l_RBNode_setBlack___main___rarg(obj*);
obj* l_Lean_IR_declMapExt___elambda__2___rarg___boxed(obj*, obj*);
obj* l_Lean_IR_logMessage___rarg(obj*, obj*, obj*, obj*, obj*);
extern "C" uint8 lean_name_dec_eq(obj*, obj*);
obj* l_Lean_IR_findDecl_x_27(obj*, obj*, obj*, obj*);
obj* l_Lean_IR_containsDecl(obj*, obj*, obj*);
obj* l_Lean_IR_LogEntry_fmt___main(obj*);
extern obj* l_Array_empty___closed__1;
obj* l_Lean_IR_logMessage___boxed(obj*);
obj* l_Array_mfindAux___main___at_Lean_IR_findDecl_x_27___spec__1___boxed(obj*, obj*, obj*);
obj* l_Lean_Format_pretty(obj*, obj*);
obj* l_Lean_IR_mkDeclMapExtension___closed__1;
extern obj* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__2;
@ -68,6 +70,7 @@ obj* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_IR_mkDeclMapExtension
obj* l_Lean_IR_log(obj*, obj*, obj*);
obj* l_Lean_IR_mkDeclMapExtension(obj*);
obj* l_Lean_IR_tracePrefixOptionName;
obj* l_Array_anyMAux___main___at_Lean_IR_containsDecl_x_27___spec__1___boxed(obj*, obj*, obj*);
extern "C" usize lean_name_hash_usize(obj*);
extern obj* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
obj* l_Lean_PersistentEnvExtension_getState___rarg(obj*, obj*);
@ -91,6 +94,10 @@ uint8 nat_dec_lt(obj*, obj*);
obj* l_Array_miterateAux___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__10___boxed(obj*, obj*, obj*, obj*);
obj* l_Lean_IR_logDecls(obj*, obj*, obj*, obj*);
extern obj* l_Char_HasRepr___closed__1;
namespace lean {
namespace ir {
obj* add_decl_core(obj*, obj*);
}}
obj* l_Lean_SMap_empty___at_Lean_IR_mkDeclMapExtension___spec__1;
obj* l_Lean_IR_declMapExt;
obj* l_AssocList_contains___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__3___boxed(obj*, obj*);
@ -111,11 +118,13 @@ obj* l_Lean_IR_LogEntry_fmt(obj*);
obj* l___private_init_lean_compiler_ir_compilerm_3__logMessageIfAux___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
uint8 l_AssocList_contains___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__3(obj*, obj*);
obj* l_Array_mforAux___main___at_Lean_IR_addDecls___spec__1(obj*, obj*, obj*, obj*);
obj* l_Array_mfindAux___main___at_Lean_IR_findDecl_x_27___spec__1(obj*, obj*, obj*);
uint8 l___private_init_lean_compiler_ir_compilerm_1__isLogEnabledFor(obj*, obj*);
obj* l_RBNode_ins___main___at_Lean_IR_mkDeclMapExtension___spec__5(obj*, obj*, obj*);
obj* l_Array_miterateAux___main___at_Lean_IR_Log_format___spec__1___boxed(obj*, obj*, obj*, obj*);
obj* l_Lean_IR_declMapExt___elambda__1(obj*);
extern obj* l_Lean_SMap_insert___main___at_Lean_Environment_add___spec__1___closed__2;
obj* l_Lean_IR_getDecl_x_27(obj*, obj*, obj*, obj*);
obj* l___private_init_lean_compiler_ir_compilerm_4__mkEntryArray(obj*);
obj* l_AssocList_replace___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__7(obj*, obj*, obj*);
extern obj* l_Lean_Format_sbracket___closed__3;
@ -126,9 +135,11 @@ namespace lean {
usize usize_modn(usize, obj*);
}
obj* l_HashMapImp_find___at_Lean_IR_findDecl___spec__3___boxed(obj*, obj*);
obj* l_Lean_IR_getDecl_x_27___boxed(obj*, obj*, obj*, obj*);
obj* l___private_init_lean_compiler_ir_compilerm_2__logDeclsAux___boxed(obj*, obj*, obj*, obj*, obj*);
obj* l_mkHashMapImp___rarg(obj*);
obj* l_Lean_IR_modifyEnv(obj*, obj*, obj*);
obj* l_Lean_IR_containsDecl_x_27(obj*, obj*, obj*, obj*);
obj* l_Lean_IR_containsDecl___boxed(obj*, obj*, obj*);
obj* l___private_init_lean_compiler_ir_compilerm_3__logMessageIfAux___rarg(obj*, obj*, obj*, obj*, obj*);
uint8 l_HashMapImp_contains___at_Lean_IR_containsDecl___spec__2(obj*, obj*);
@ -145,6 +156,8 @@ obj* l_Lean_IR_logMessageIf___rarg(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_IR_declMapExt___elambda__2___boxed(obj*);
obj* l_AssocList_find___main___at_Lean_IR_findDecl___spec__4___boxed(obj*, obj*);
obj* l_List_foldl___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__8___boxed(obj*, obj*, obj*);
obj* l_Lean_IR_findDecl_x_27___boxed(obj*, obj*, obj*, obj*);
uint8 l_Array_anyMAux___main___at_Lean_IR_containsDecl_x_27___spec__1(obj*, obj*, obj*);
obj* l_Lean_IR_addDecl(obj*, obj*, obj*);
obj* l_Lean_Name_append___main(obj*, obj*);
namespace lean {
@ -155,6 +168,7 @@ obj* l_Lean_IR_mkDeclMapExtension___lambda__1(uint8, obj*, obj*);
obj* l_RBNode_find___main___at_Lean_IR_findDecl___spec__2___boxed(obj*, obj*);
obj* l_Array_mforAux___main___at_Lean_IR_addDecls___spec__1___boxed(obj*, obj*, obj*, obj*);
obj* l_List_foldl___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__8(obj*, obj*, obj*);
obj* l_Lean_IR_containsDecl_x_27___boxed(obj*, obj*, obj*, obj*);
obj* l_RBNode_insert___at_Lean_IR_mkDeclMapExtension___spec__4(obj*, obj*, obj*);
obj* l_Array_miterateAux___main___at_Lean_IR_LogEntry_fmt___main___spec__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
_start:
@ -2692,31 +2706,33 @@ return x_6;
obj* _init_l_Lean_IR_mkDeclMapExtension___closed__1() {
_start:
{
obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; uint8 x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; uint8 x_11; obj* x_12; obj* x_13;
obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; uint8 x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; uint8 x_12; obj* x_13; obj* x_14;
x_0 = lean::box(0);
x_1 = lean::mk_string("IRDecls");
x_2 = lean_name_mk_string(x_0, x_1);
x_3 = lean::mk_nat_obj(0ul);
x_4 = lean::mk_empty_array(x_3);
x_5 = 6;
x_6 = lean::alloc_cnstr(1, 2, 1);
lean::cnstr_set(x_6, 0, x_0);
lean::cnstr_set(x_6, 1, x_4);
lean::cnstr_set_scalar(x_6, sizeof(void*)*2, x_5);
x_7 = x_6;
x_8 = l_Lean_SMap_empty___at_Lean_IR_mkDeclMapExtension___spec__1;
x_9 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_IR_mkDeclMapExtension___lambda__1___boxed), 3, 0);
x_10 = lean::alloc_closure(reinterpret_cast<void*>(l___private_init_lean_compiler_ir_compilerm_4__mkEntryArray), 1, 0);
x_11 = 0;
x_12 = lean::alloc_cnstr(0, 5, 1);
lean::cnstr_set(x_12, 0, x_2);
lean::cnstr_set(x_12, 1, x_8);
lean::cnstr_set(x_12, 2, x_7);
lean::cnstr_set(x_12, 3, x_9);
lean::cnstr_set(x_12, 4, x_10);
lean::cnstr_set_scalar(x_12, sizeof(void*)*5, x_11);
x_13 = x_12;
return x_13;
x_6 = lean::box(12);
x_7 = lean::alloc_cnstr(0, 3, 1);
lean::cnstr_set(x_7, 0, x_0);
lean::cnstr_set(x_7, 1, x_4);
lean::cnstr_set(x_7, 2, x_6);
lean::cnstr_set_scalar(x_7, sizeof(void*)*3, x_5);
x_8 = x_7;
x_9 = l_Lean_SMap_empty___at_Lean_IR_mkDeclMapExtension___spec__1;
x_10 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_IR_mkDeclMapExtension___lambda__1___boxed), 3, 0);
x_11 = lean::alloc_closure(reinterpret_cast<void*>(l___private_init_lean_compiler_ir_compilerm_4__mkEntryArray), 1, 0);
x_12 = 0;
x_13 = lean::alloc_cnstr(0, 5, 1);
lean::cnstr_set(x_13, 0, x_2);
lean::cnstr_set(x_13, 1, x_9);
lean::cnstr_set(x_13, 2, x_8);
lean::cnstr_set(x_13, 3, x_10);
lean::cnstr_set(x_13, 4, x_11);
lean::cnstr_set_scalar(x_13, sizeof(void*)*5, x_12);
x_14 = x_13;
return x_14;
}
}
obj* l_Lean_IR_mkDeclMapExtension(obj* x_0) {
@ -3250,6 +3266,18 @@ lean::dec(x_1);
return x_3;
}
}
namespace lean {
namespace ir {
obj* add_decl_core(obj* x_0, obj* x_1) {
_start:
{
obj* x_2; obj* x_3;
x_2 = l_Lean_IR_declMapExt;
x_3 = l_Lean_PersistentEnvExtension_addEntry___rarg(x_2, x_0, x_1);
return x_3;
}
}
}}
obj* l_Lean_IR_addDecl(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
@ -3419,6 +3447,345 @@ lean::dec(x_1);
return x_3;
}
}
obj* l_Array_mfindAux___main___at_Lean_IR_findDecl_x_27___spec__1(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
obj* x_3; uint8 x_4;
x_3 = lean::array_get_size(x_1);
x_4 = lean::nat_dec_lt(x_2, x_3);
lean::dec(x_3);
if (x_4 == 0)
{
obj* x_7;
lean::dec(x_2);
x_7 = lean::box(0);
return x_7;
}
else
{
obj* x_8; obj* x_9; uint8 x_10;
x_8 = lean::array_fget(x_1, x_2);
x_9 = l_Lean_IR_Decl_name___main(x_8);
x_10 = lean_name_dec_eq(x_9, x_0);
lean::dec(x_9);
if (x_10 == 0)
{
obj* x_13; obj* x_14;
lean::dec(x_8);
x_13 = lean::mk_nat_obj(1ul);
x_14 = lean::nat_add(x_2, x_13);
lean::dec(x_2);
x_2 = x_14;
goto _start;
}
else
{
obj* x_18;
lean::dec(x_2);
x_18 = lean::alloc_cnstr(1, 1, 0);
lean::cnstr_set(x_18, 0, x_8);
return x_18;
}
}
}
}
obj* l_Lean_IR_findDecl_x_27(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
_start:
{
obj* x_4; obj* x_5;
x_4 = lean::mk_nat_obj(0ul);
x_5 = l_Array_mfindAux___main___at_Lean_IR_findDecl_x_27___spec__1(x_0, x_1, x_4);
if (lean::obj_tag(x_5) == 0)
{
obj* x_6; obj* x_8; obj* x_9; obj* x_11; obj* x_12; obj* x_14; obj* x_15;
x_6 = lean::cnstr_get(x_3, 1);
if (lean::is_exclusive(x_3)) {
lean::cnstr_release(x_3, 0);
x_8 = x_3;
} else {
lean::inc(x_6);
lean::dec(x_3);
x_8 = lean::box(0);
}
x_9 = lean::cnstr_get(x_6, 0);
lean::inc(x_9);
x_11 = l_Lean_IR_declMapExt;
x_12 = l_Lean_PersistentEnvExtension_getState___rarg(x_11, x_9);
lean::dec(x_9);
x_14 = l_Lean_SMap_find___main___at_Lean_IR_findDecl___spec__1(x_12, x_0);
if (lean::is_scalar(x_8)) {
x_15 = lean::alloc_cnstr(0, 2, 0);
} else {
x_15 = x_8;
}
lean::cnstr_set(x_15, 0, x_14);
lean::cnstr_set(x_15, 1, x_6);
return x_15;
}
else
{
obj* x_16; obj* x_18; obj* x_19;
x_16 = lean::cnstr_get(x_3, 1);
if (lean::is_exclusive(x_3)) {
lean::cnstr_release(x_3, 0);
x_18 = x_3;
} else {
lean::inc(x_16);
lean::dec(x_3);
x_18 = lean::box(0);
}
if (lean::is_scalar(x_18)) {
x_19 = lean::alloc_cnstr(0, 2, 0);
} else {
x_19 = x_18;
}
lean::cnstr_set(x_19, 0, x_5);
lean::cnstr_set(x_19, 1, x_16);
return x_19;
}
}
}
obj* l_Array_mfindAux___main___at_Lean_IR_findDecl_x_27___spec__1___boxed(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
obj* x_3;
x_3 = l_Array_mfindAux___main___at_Lean_IR_findDecl_x_27___spec__1(x_0, x_1, x_2);
lean::dec(x_0);
lean::dec(x_1);
return x_3;
}
}
obj* l_Lean_IR_findDecl_x_27___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
_start:
{
obj* x_4;
x_4 = l_Lean_IR_findDecl_x_27(x_0, x_1, x_2, x_3);
lean::dec(x_0);
lean::dec(x_1);
lean::dec(x_2);
return x_4;
}
}
uint8 l_Array_anyMAux___main___at_Lean_IR_containsDecl_x_27___spec__1(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
obj* x_3; uint8 x_4;
x_3 = lean::array_get_size(x_1);
x_4 = lean::nat_dec_lt(x_2, x_3);
lean::dec(x_3);
if (x_4 == 0)
{
uint8 x_7;
lean::dec(x_2);
x_7 = 0;
return x_7;
}
else
{
obj* x_8; obj* x_9; uint8 x_11;
x_8 = lean::array_fget(x_1, x_2);
x_9 = l_Lean_IR_Decl_name___main(x_8);
lean::dec(x_8);
x_11 = lean_name_dec_eq(x_9, x_0);
lean::dec(x_9);
if (x_11 == 0)
{
obj* x_13; obj* x_14;
x_13 = lean::mk_nat_obj(1ul);
x_14 = lean::nat_add(x_2, x_13);
lean::dec(x_2);
x_2 = x_14;
goto _start;
}
else
{
lean::dec(x_2);
return x_11;
}
}
}
}
obj* l_Lean_IR_containsDecl_x_27(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
_start:
{
obj* x_4; uint8 x_5;
x_4 = lean::mk_nat_obj(0ul);
x_5 = l_Array_anyMAux___main___at_Lean_IR_containsDecl_x_27___spec__1(x_0, x_1, x_4);
if (x_5 == 0)
{
obj* x_6; obj* x_8; obj* x_9; obj* x_11; obj* x_12; uint8 x_14; obj* x_15; obj* x_16;
x_6 = lean::cnstr_get(x_3, 1);
if (lean::is_exclusive(x_3)) {
lean::cnstr_release(x_3, 0);
x_8 = x_3;
} else {
lean::inc(x_6);
lean::dec(x_3);
x_8 = lean::box(0);
}
x_9 = lean::cnstr_get(x_6, 0);
lean::inc(x_9);
x_11 = l_Lean_IR_declMapExt;
x_12 = l_Lean_PersistentEnvExtension_getState___rarg(x_11, x_9);
lean::dec(x_9);
x_14 = l_Lean_SMap_contains___main___at_Lean_IR_containsDecl___spec__1(x_12, x_0);
x_15 = lean::box(x_14);
if (lean::is_scalar(x_8)) {
x_16 = lean::alloc_cnstr(0, 2, 0);
} else {
x_16 = x_8;
}
lean::cnstr_set(x_16, 0, x_15);
lean::cnstr_set(x_16, 1, x_6);
return x_16;
}
else
{
obj* x_17; obj* x_19; uint8 x_20; obj* x_21; obj* x_22;
x_17 = lean::cnstr_get(x_3, 1);
if (lean::is_exclusive(x_3)) {
lean::cnstr_release(x_3, 0);
x_19 = x_3;
} else {
lean::inc(x_17);
lean::dec(x_3);
x_19 = lean::box(0);
}
x_20 = 1;
x_21 = lean::box(x_20);
if (lean::is_scalar(x_19)) {
x_22 = lean::alloc_cnstr(0, 2, 0);
} else {
x_22 = x_19;
}
lean::cnstr_set(x_22, 0, x_21);
lean::cnstr_set(x_22, 1, x_17);
return x_22;
}
}
}
obj* l_Array_anyMAux___main___at_Lean_IR_containsDecl_x_27___spec__1___boxed(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
uint8 x_3; obj* x_4;
x_3 = l_Array_anyMAux___main___at_Lean_IR_containsDecl_x_27___spec__1(x_0, x_1, x_2);
x_4 = lean::box(x_3);
lean::dec(x_0);
lean::dec(x_1);
return x_4;
}
}
obj* l_Lean_IR_containsDecl_x_27___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
_start:
{
obj* x_4;
x_4 = l_Lean_IR_containsDecl_x_27(x_0, x_1, x_2, x_3);
lean::dec(x_0);
lean::dec(x_1);
lean::dec(x_2);
return x_4;
}
}
obj* l_Lean_IR_getDecl_x_27(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
_start:
{
obj* x_4;
x_4 = l_Lean_IR_findDecl_x_27(x_0, x_1, x_2, x_3);
if (lean::obj_tag(x_4) == 0)
{
obj* x_5;
x_5 = lean::cnstr_get(x_4, 0);
lean::inc(x_5);
if (lean::obj_tag(x_5) == 0)
{
obj* x_7; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_15; obj* x_16; obj* x_17;
x_7 = lean::cnstr_get(x_4, 1);
if (lean::is_exclusive(x_4)) {
lean::cnstr_release(x_4, 0);
x_9 = x_4;
} else {
lean::inc(x_7);
lean::dec(x_4);
x_9 = lean::box(0);
}
x_10 = l_Lean_Name_toString___closed__1;
x_11 = l_Lean_Name_toStringWithSep___main(x_10, x_0);
x_12 = l_Lean_IR_getDecl___closed__1;
x_13 = lean::string_append(x_12, x_11);
lean::dec(x_11);
x_15 = l_Char_HasRepr___closed__1;
x_16 = lean::string_append(x_13, x_15);
if (lean::is_scalar(x_9)) {
x_17 = lean::alloc_cnstr(1, 2, 0);
} else {
x_17 = x_9;
lean::cnstr_set_tag(x_9, 1);
}
lean::cnstr_set(x_17, 0, x_16);
lean::cnstr_set(x_17, 1, x_7);
return x_17;
}
else
{
obj* x_19; obj* x_21; obj* x_22; obj* x_25;
lean::dec(x_0);
x_19 = lean::cnstr_get(x_4, 1);
if (lean::is_exclusive(x_4)) {
lean::cnstr_release(x_4, 0);
x_21 = x_4;
} else {
lean::inc(x_19);
lean::dec(x_4);
x_21 = lean::box(0);
}
x_22 = lean::cnstr_get(x_5, 0);
lean::inc(x_22);
lean::dec(x_5);
if (lean::is_scalar(x_21)) {
x_25 = lean::alloc_cnstr(0, 2, 0);
} else {
x_25 = x_21;
}
lean::cnstr_set(x_25, 0, x_22);
lean::cnstr_set(x_25, 1, x_19);
return x_25;
}
}
else
{
obj* x_27; obj* x_29; obj* x_31; obj* x_32;
lean::dec(x_0);
x_27 = lean::cnstr_get(x_4, 0);
x_29 = lean::cnstr_get(x_4, 1);
if (lean::is_exclusive(x_4)) {
x_31 = x_4;
} else {
lean::inc(x_27);
lean::inc(x_29);
lean::dec(x_4);
x_31 = lean::box(0);
}
if (lean::is_scalar(x_31)) {
x_32 = lean::alloc_cnstr(1, 2, 0);
} else {
x_32 = x_31;
}
lean::cnstr_set(x_32, 0, x_27);
lean::cnstr_set(x_32, 1, x_29);
return x_32;
}
}
}
obj* l_Lean_IR_getDecl_x_27___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
_start:
{
obj* x_4;
x_4 = l_Lean_IR_getDecl_x_27(x_0, x_1, x_2, x_3);
lean::dec(x_1);
lean::dec(x_2);
return x_4;
}
}
obj* initialize_init_control_reader(obj*);
obj* initialize_init_lean_environment(obj*);
obj* initialize_init_lean_compiler_ir_basic(obj*);

16
src/stage0/init/lean/compiler/ir/default.cpp generated
View file

@ -56,17 +56,19 @@ obj* l_Array_hmmapAux___main___at___private_init_lean_compiler_ir_default_1__com
obj* _init_l_Array_hmmapAux___main___at___private_init_lean_compiler_ir_default_1__compileAux___spec__1___closed__1() {
_start:
{
obj* x_0; obj* x_1; obj* x_2; uint8 x_3; obj* x_4; obj* x_5;
obj* x_0; obj* x_1; obj* x_2; uint8 x_3; obj* x_4; obj* x_5; obj* x_6;
x_0 = lean::mk_nat_obj(0ul);
x_1 = lean::mk_empty_array(x_0);
x_2 = lean::box(0);
x_3 = 6;
x_4 = lean::alloc_cnstr(1, 2, 1);
lean::cnstr_set(x_4, 0, x_2);
lean::cnstr_set(x_4, 1, x_1);
lean::cnstr_set_scalar(x_4, sizeof(void*)*2, x_3);
x_5 = x_4;
return x_5;
x_4 = lean::box(12);
x_5 = lean::alloc_cnstr(0, 3, 1);
lean::cnstr_set(x_5, 0, x_2);
lean::cnstr_set(x_5, 1, x_1);
lean::cnstr_set(x_5, 2, x_4);
lean::cnstr_set_scalar(x_5, sizeof(void*)*3, x_3);
x_6 = x_5;
return x_6;
}
}
obj* l_Array_hmmapAux___main___at___private_init_lean_compiler_ir_default_1__compileAux___spec__1(obj* x_0, obj* x_1) {

2
src/stage0/init/lean/compiler/ir/format.cpp generated
View file

@ -2832,7 +2832,7 @@ x_41 = lean::cnstr_get(x_1, 0);
lean::inc(x_41);
x_43 = lean::cnstr_get(x_1, 1);
lean::inc(x_43);
x_45 = lean::cnstr_get_scalar<uint8>(x_1, sizeof(void*)*2);
x_45 = lean::cnstr_get_scalar<uint8>(x_1, sizeof(void*)*3);
lean::dec(x_1);
x_47 = l_Lean_Name_toString___closed__1;
x_48 = l_Lean_Name_toStringWithSep___main(x_47, x_41);