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

feat(library/compiler): avoid cnstr_set_scalar when possible

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-06 10:49:58 -08:00
parent fbc6c47094
commit d103ff70fe
4 changed files with 39 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -194,8 +194,8 @@ class emit_bytecode_fn {
buffer<expr> args;
expr const & fn = get_app_args(e, args);
lean_assert(is_llnf_reuse(fn));
unsigned cidx, nusizes, ssz;
is_llnf_reuse(fn, cidx, nusizes, ssz);
unsigned cidx, nusizes, ssz; bool updt_cidx;
is_llnf_reuse(fn, cidx, nusizes, ssz, updt_cidx);
if (ssz != 0 || nusizes != 0) throw_no_unboxed_support();
compile_args(args.size(), args.data(), bpz, m);
emit(mk_reuse_instr(cidx, get_app_num_args(e) - 1));

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

@ -475,13 +475,16 @@ struct emit_fn_fn {
void emit_reuse(expr const & x, expr const & fn, buffer<expr> const & args) {
lean_assert(!args.empty());
unsigned cidx, num_usizes, num_bytes;
lean_verify(is_llnf_reuse(fn, cidx, num_usizes, num_bytes));
bool updt_cidx;
lean_verify(is_llnf_reuse(fn, cidx, num_usizes, num_bytes, updt_cidx));
expr const & o = args[0];
m_out << "if (lean::is_scalar("; emit_fvar(o); m_out <<")) {\n";
m_out << " "; emit_alloc_cnstr(x, cidx, args.size()-1, num_usizes, num_bytes);
m_out << "} else {\n";
m_out << " "; emit_lhs(x); emit_fvar(o); m_out << ";\n";
m_out << " lean::cnstr_set_tag("; emit_fvar(o); m_out << ", " << cidx << ");\n";
if (updt_cidx) {
m_out << " lean::cnstr_set_tag("; emit_fvar(o); m_out << ", " << cidx << ");\n";
}
m_out << "}\n";
emit_cnstr_sets(x, args.size()-1, args.data()+1);
}

34
src/library/compiler/llnf.cpp
View file

@ -70,6 +70,25 @@ static bool is_llnf_ternary_primitive(expr const & e, name const & prefix, unsig
return true;
}
static bool is_llnf_quaternary_primitive(expr const & e, name const & prefix, unsigned & i1, unsigned & i2, unsigned & i3, unsigned & i4) {
if (!is_constant(e)) return false;
name const & n4 = const_name(e);
if (!is_internal_name(n4)) return false;
if (n4.is_atomic() || !n4.is_numeral()) return false;
i4 = n4.get_numeral().get_small_value();
name const & n3 = n4.get_prefix();
if (!is_internal_name(n3)) return false;
if (n3.is_atomic() || !n3.is_numeral()) return false;
i3 = n3.get_numeral().get_small_value();
name const & n2 = n3.get_prefix();
if (n2.is_atomic() || !n2.is_numeral()) return false;
i2 = n2.get_numeral().get_small_value();
name const & n1 = n2.get_prefix();
if (n1.is_atomic() || !n1.is_numeral() || n1.get_prefix() != prefix) return false;
i1 = n1.get_numeral().get_small_value();
return true;
}
/*
A constructor object contains a header, then a sequence of pointers to other Lean objects,
a sequence of `usize` (i.e., `size_t`) scalar values, and a sequence of other scalar values.
@ -88,9 +107,16 @@ scalar fields.
expr mk_llnf_cnstr(unsigned cidx, unsigned num_usizes, unsigned num_bytes) { return mk_constant(name(name(name(*g_cnstr, cidx), num_usizes), num_bytes)); }
bool is_llnf_cnstr(expr const & e, unsigned & cidx, unsigned & num_usizes, unsigned & num_bytes) { return is_llnf_ternary_primitive(e, *g_cnstr, cidx, num_usizes, num_bytes); }
/* The `_reuse.<cidx>.<num_usizes>.<num_bytes>` is similar to `_cnstr.<cidx>.<num_usize>.<num_bytes>`, but it takes an extra argument: a memory cell that may be reused. */
expr mk_llnf_reuse(unsigned cidx, unsigned num_usizes, unsigned num_bytes) { return mk_constant(name(name(name(*g_reuse, cidx), num_usizes), num_bytes)); }
bool is_llnf_reuse(expr const & e, unsigned & cidx, unsigned & num_usizes, unsigned & num_bytes) { return is_llnf_ternary_primitive(e, *g_reuse, cidx, num_usizes, num_bytes); }
/* The `_reuse.<cidx>.<num_usizes>.<num_bytes>.<updt_cidx>` is similar to `_cnstr.<cidx>.<num_usize>.<num_bytes>`, but it takes an extra argument: a memory cell that may be reused. */
expr mk_llnf_reuse(unsigned cidx, unsigned num_usizes, unsigned num_bytes, bool updt_cidx) {
return mk_constant(name(name(name(name(*g_reuse, cidx), num_usizes), num_bytes), updt_cidx));
}
bool is_llnf_reuse(expr const & e, unsigned & cidx, unsigned & num_usizes, unsigned & num_bytes, bool & updt_cidx) {
unsigned aux;
bool r = is_llnf_quaternary_primitive(e, *g_reuse, cidx, num_usizes, num_bytes, aux);
updt_cidx = aux;
return r;
}
expr mk_llnf_reset(unsigned n) { return mk_constant(name(*g_reset, n)); }
bool is_llnf_reset(expr const & e, unsigned & n) { return is_llnf_unary_primitive(e, *g_reset, n); }
@ -570,7 +596,7 @@ class to_llnf_fn {
}
j++;
}
r = mk_app(mk_app(mk_llnf_reuse(k_info.m_cidx, k_info.m_num_usizes, k_info.m_scalar_sz), r), obj_args);
r = mk_app(mk_app(mk_llnf_reuse(k_info.m_cidx, k_info.m_num_usizes, k_info.m_scalar_sz, m_cinfo.m_cidx != k_info.m_cidx), r), obj_args);
unsigned uidx = 0;
unsigned offset = 0;
j = nparams;

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

@ -18,7 +18,7 @@ optional<pair<environment, comp_decl>> mk_boxed_version(environment env, name co
bool is_llnf_apply(expr const & e);
bool is_llnf_closure(expr const & e);
bool is_llnf_cnstr(expr const & e, unsigned & cidx, unsigned & nusize, unsigned & ssz);
bool is_llnf_reuse(expr const & e, unsigned & cidx, unsigned & nusize, unsigned & ssz);
bool is_llnf_reuse(expr const & e, unsigned & cidx, unsigned & nusize, unsigned & ssz, bool & updt_cidx);
bool is_llnf_reset(expr const & e, unsigned & n);
bool is_llnf_proj(expr const & e, unsigned & idx);
bool is_llnf_sproj(expr const & e, unsigned & sz, unsigned & n, unsigned & offset);
@ -33,7 +33,7 @@ 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_reuse(expr const & e) { unsigned d1, d2, d3; bool u; return is_llnf_reuse(e, d1, d2, d3, u); }
inline bool is_llnf_reset(expr const & e) { unsigned i; return is_llnf_reset(e, i); }
inline bool is_llnf_proj(expr const & e) { unsigned d; return is_llnf_proj(e, d); }
inline bool is_llnf_sproj(expr const & e) { unsigned d1, d2, d3; return is_llnf_sproj(e, d1, d2, d3); }